Rename things such that symantic-document is neater when used with import qualified.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Grammar.hs
index b1a3b7efb12649e8dd89511b5586b54eeec47213..8260ab5fa118d461d6a63327db0ff9e3a98532ff 100644 (file)
@@ -1,3 +1,5 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
@@ -5,119 +7,283 @@ module Language.Symantic.Typing.Grammar where
 
 import Control.Applicative (Applicative(..))
 import Data.List (foldl1')
-import Data.Proxy
+import Data.Map.Strict (Map)
+import Data.Maybe (fromMaybe)
+import Data.Semigroup (Semigroup(..))
 import Data.String (IsString(..))
-import Data.Text (Text)
 import qualified Data.Char as Char
-import qualified Data.Kind as K
+import qualified Data.Map.Strict as Map
 import qualified Data.Text as Text
 
-import Language.Symantic.Parsing
+import Language.Symantic.Grammar as G
+import Language.Symantic.Typing.Kind
+import Language.Symantic.Typing.Variable
+import Language.Symantic.Typing.List
+import Language.Symantic.Typing.Module
+import Language.Symantic.Typing.Type
 
--- * Type 'TyName'
-newtype TyName = TyName Text
- deriving (Eq, Ord, Show)
-instance IsString TyName where
-       fromString = TyName . fromString
+-- * Type 'AST_Type'
+-- | /Abstract Syntax Tree/ of 'Token_Type'.
+type AST_Type src = BinTree (Token_Type src)
+
+-- ** Type 'Token_Type'
+data Token_Type src
+ =   Token_Type_Const (TypeTLen src)
+ |   Token_Type_Var   (At src NameVar)
+ -- deriving (Eq, Show)
+instance Source src => Eq (Token_Type src) where
+       Token_Type_Const (TypeTLen x) == Token_Type_Const (TypeTLen y) = x LenZ == y LenZ
+       Token_Type_Var (At _ x) == Token_Type_Var (At _ y) = x == y
+       _ == _ = False
+instance (Source src, Show (TypeT src '[])) => Show (Token_Type src) where
+       showsPrec p (Token_Type_Const x) =
+               showParen (p >= 10) $
+               showString "Token_Type_Const" .
+               showChar ' ' . showsPrec 10 x
+       showsPrec p (Token_Type_Var (At _ x)) =
+               showParen (p >= 10) $
+               showString "Token_Type_Var" .
+               showChar ' ' . showsPrec 10 x
+
+-- * Type 'ModulesTy'
+type ModulesTy src = Map (Mod NameTy) (TypeTLen src)
 
-{-
--- * Type 'Token_Type'
-type Token_Type = Type () '[] ()
--- data Token_Type
+-- ** Type 'TypeTLen'
+-- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
+--
+-- Useful to build a 'ModulesTy' which can be used
+-- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
+newtype TypeTLen src = TypeTLen (forall vs. Len vs -> TypeT src vs)
+instance Source src => Eq (TypeTLen src) where
+       TypeTLen x == TypeTLen y = x LenZ == y LenZ
+instance (Source src, Show (TypeT src '[])) => Show (TypeTLen src) where
+       showsPrec p (TypeTLen t) = showsPrec p $ t LenZ
 
+typeTLen ::
+ forall c src.
+ Source src =>
+ Constable c =>
+ KindInjP (Ty_of_Type (K c)) =>
+ K c ~ Type_of_Ty (Ty_of_Type (K c)) =>
+ src ->
+ TypeTLen src
+typeTLen src =
+       TypeTLen $ \len -> TypeT $
+               TyConst src len $
+               constKiInj @(K c) @c $
+               kindInjP @(Ty_of_Type (K c)) noSource
+
+-- ** Class 'ModulesTyInj'
+-- | Derive a 'ModulesTy' from the given type-level list
+-- of 'Proxy'-fied /type constants/.
+class ModulesTyInj ts where
+       modulesTyInj :: Source src => ModulesTy src
+instance ModulesTyInj '[] where
+       modulesTyInj = Map.empty
 instance
- ( Compile_TyNameR TyName cs rs
- , Inj_TyConst cs K.Type
- ) => Compile_TyNameR TyName cs (Proxy K.Type ': rs) where
-       compile_TyNameR _rs src (TyName "Type") k = k (tySourced @K.Type src)
-       compile_TyNameR _rs src raw k = compile_TyNameR (Proxy @rs) src raw k
-instance Show_TyConst cs => Show_TyConst (Proxy K.Type ': cs) where
-       show_TyConst TyConstZ{} = "Type"
-       show_TyConst (TyConstS c) = show_TyConst c
--}
+ ( KindInjP (Ty_of_Type (K c))
+ , K c ~ Type_of_Ty (Ty_of_Type (K c))
+ , Constable c
+ , ModulesTyInj ts
+ ) => ModulesTyInj (Proxy c ': ts) where
+       modulesTyInj =
+               Map.insert
+                (nameTyOf $ Proxy @c)
+                (typeTLen @c noSource) $
+               modulesTyInj @ts
 
--- * Type 'AST_Type'
-type AST_Type src = BinTree (EToken src '[Proxy K.Type])
 
-data instance TokenT ss (Proxy K.Type)
- = Token_Type_Name TyName
+-- * Class 'Gram_Mod'
+class
+ ( Gram_Char g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ ) => Gram_Mod g where
+       g_PathMod :: CF g PathMod
+       g_PathMod = rule "PathMod" $
+               infixrG
+                (pure <$> g_NameMod)
+                (op <$ char '.')
+               where op = (<>)
+       g_NameMod :: CF g NameMod
+       g_NameMod = rule "NameMod" $
+               NameMod . Text.pack <$> identG
+               where
+               identG = (:) <$> headG <*> many (cfOf tailG)
+               headG = unicat $ Unicat Char.UppercaseLetter
+               tailG :: Terminal g Char
+               tailG =
+                       unicat Unicat_Letter <+>
+                       unicat Unicat_Number
 
-deriving instance Eq_Token   ss => Eq   (TokenT ss (Proxy K.Type))
-deriving instance Show_Token ss => Show (TokenT ss (Proxy K.Type))
+deriving instance Gram_Mod g => Gram_Mod (CF g)
+instance Gram_Mod EBNF
+instance Gram_Mod RuleEBNF
+
+-- * Class 'Gram_Type_Name'
+class
+ ( Gram_Char g
+ , Gram_Rule g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_RegL g
+ , Gram_CF g
+ , Gram_Comment g
+ , Gram_Op g
+ , Gram_Mod g
+ ) => Gram_Type_Name g where
+       g_ModNameTy :: CF g (Mod NameTy)
+       g_ModNameTy = rule "ModNameTy" $
+               lexeme $
+                       g_ModNameTyId <+>
+                       parens g_ModNameTyOp
+       
+       g_ModNameTyId :: CF g (Mod NameTy)
+       g_ModNameTyId = rule "ModNameTyId" $
+               Mod
+                <$> option [] (try $ g_PathMod <* char '.')
+                <*> g_NameTyId
+       g_NameTyId :: CF g NameTy
+       g_NameTyId = rule "NameTyId" $
+               NameTy . Text.pack <$> identTyG
+               where
+               identTyG = (:) <$> headTyG <*> many (cfOf tailTyG)
+               headTyG = unicat $ Unicat Char.UppercaseLetter
+               tailTyG :: Terminal g Char
+               tailTyG =
+                       unicat Unicat_Letter <+>
+                       unicat Unicat_Number
+       
+       g_ModNameTyOp :: CF g (Mod NameTy)
+       g_ModNameTyOp = rule "ModNameTyOp" $
+               Mod
+                <$> option [] (try $ g_PathMod <* char '.')
+                <*> g_NameTyOp
+       g_NameTyOp :: CF g NameTy
+       g_NameTyOp = rule "NameTyOp" $
+               NameTy . Text.pack <$> many (cfOf okG)
+               where
+               okG :: Terminal g Char
+               okG = choice (unicat <$>
+                        [ Unicat_Symbol
+                        , Unicat_Punctuation
+                        , Unicat_Mark
+                        ]) `but` koG
+               koG = choice (char <$> ['(', ')', '`', '\'', '[', ']'])
+
+deriving instance Gram_Type_Name g => Gram_Type_Name (CF g)
+instance Gram_Type_Name EBNF
+instance Gram_Type_Name RuleEBNF
 
 -- * Class 'Gram_Type'
 -- | Read an 'AST_Type' from a textual source.
 class
- ( Alt g
- , Alter g
- , App g
- , Try g
- , Gram_CF g
+ ( Gram_Source src g
+ , Gram_Char g
  , Gram_Rule g
- , Gram_Terminal g
- , Gram_Lexer g
+ , Gram_Alt g
+ , Gram_Try g
+ , Gram_App g
+ , Gram_AltApp g
+ , Gram_CF g
+ , Gram_Comment g
  , Gram_Op g
- , Gram_Meta (Text_of_Source src) g
- , Inj_Source (Text_of_Source src) src
+ , Gram_Type_Name g
+ , Gram_Error (Error_Type src) g
+ , Gram_State (Imports NameTy, ModulesTy src) g
+ , Constable (->)
+ , Constable []
+ , Constable (,)
  ) => Gram_Type src g where
        g_type :: CF g (AST_Type src)
-       g_type = rule "type" $ g_type_fun
+       g_type = rule "Type" $ g_type_fun
        g_type_fun :: CF g (AST_Type src)
-       g_type_fun = rule "type_fun" $
-               infixrG g_type_list (sourceG $ op <$ symbol "->")
-               where op src = BinTree1 . BinTree1 (BinTree0 $ inj_EToken src $ Token_Type_Name "(->)")
+       g_type_fun = rule "TypeFun" $
+               infixrG g_type_list (source $ op <$ symbol "->")
+               where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(->) src)
        -- TODO: maybe not harcoding g_type_list and g_type_tuple2
        g_type_list :: CF g (AST_Type src)
-       g_type_list = rule "type_list" $
-               sourceG $ inside f
-                (symbol "[") (optional (g_type)) (symbol "]")
+       g_type_list = rule "TypeList" $
+               source $ inside mk
+                (symbol "[") (optional g_type) (symbol "]")
                 (const <$> g_type_tuple2)
                where
-               n src = BinTree0 $ inj_EToken src $ Token_Type_Name "[]"
-               f Nothing  src = n src
-               f (Just a) src = BinTree1 (n src) a
+               mk Nothing  src = tok src
+               mk (Just a) src = BinTree2 (tok src) a
+               tok = BinTree0 . Token_Type_Const . typeTLen @[]
        g_type_tuple2 :: CF g (AST_Type src)
-       g_type_tuple2 = rule "type_tuple2" $
-               try (parens (infixrG g_type (sourceG $ op <$ symbol ","))) <+> g_type_app
-               where op src = BinTree1 . BinTree1 (BinTree0 $ inj_EToken src $ Token_Type_Name "(,)")
+       g_type_tuple2 = rule "TypeTuple2" $
+               try (parens (infixrG (g_type) (source $ op <$ symbol ","))) <+> (g_type_app)
+               where op src = BinTree2 . BinTree2 (BinTree0 $ Token_Type_Const $ typeTLen @(,) src)
        g_type_app :: CF g (AST_Type src)
-       g_type_app = rule "type_app" $
-               foldl1' BinTree1 <$> some g_type_atom
+       g_type_app = rule "TypeApp" $
+               foldl1' BinTree2 <$> some (g_type_atom)
        g_type_atom :: CF g (AST_Type src)
-       g_type_atom = rule "type_atom" $
+       g_type_atom = rule "TypeAtom" $
                try (parens g_type) <+>
-               g_type_name <+>
-               g_type_symbol
-       g_type_name :: CF g (AST_Type src)
-       g_type_name = rule "type_name" $
-               sourceG $ lexeme $
-               (\c cs src -> BinTree0 $ inj_EToken src $ Token_Type_Name $ fromString $ c:cs)
-                <$> unicat (Unicat Char.UppercaseLetter)
+               g_type_const <+>
+               g_type_var
+       g_type_const :: CF g (AST_Type src)
+       g_type_const = rule "TypeConst" $
+               lexeme $ catch $ source $ getBefore $
+               (\n (impsTy, modsTy) src -> BinTree0 . Token_Type_Const <$> readTyName impsTy modsTy src n)
+                <$> g_ModNameTy
+       g_type_var :: CF g (AST_Type src)
+       g_type_var = rule "TypeVar" $
+               lexeme $ source $
+               (\n ns src -> BinTree0 $ Token_Type_Var $ At src $ fromString $ n:ns)
+                <$> unicat (Unicat Char.LowercaseLetter)
                 <*> many (choice $ unicat <$> [Unicat_Letter, Unicat_Number])
-       g_type_symbol :: CF g (AST_Type src)
-       g_type_symbol = rule "type_symbol" $
-               sourceG $ (f <$>) $
-               parens $ many $ cf_of_Terminal $ choice g_ok `but` choice g_ko
-               where
-               f s src = BinTree0 $ inj_EToken src $ (Token_Type_Name) $
-                       TyName $ Text.concat ["(", Text.pack s, ")"]
-               g_ok = unicat <$>
-                [ Unicat_Symbol
-                , Unicat_Punctuation
-                , Unicat_Mark
-                ]
-               g_ko = char <$> ['(', ')', '`']
 
 deriving instance Gram_Type src g => Gram_Type src (CF g)
 instance
- ( Inj_Source (Text_of_Source src) src
+ ( Gram_Source src EBNF
+ , Constable (->)
+ , Constable (,)
+ , Constable []
  ) => Gram_Type src EBNF
 instance
- ( Inj_Source (Text_of_Source src) src
- ) => Gram_Type src RuleDef
+ ( Gram_Source src RuleEBNF
+ , Constable (->)
+ , Constable (,)
+ , Constable []
+ ) => Gram_Type src RuleEBNF
+
+-- | Lookup a 'TyConst' or 'Type' synonym
+-- associated with given 'NameTy' in given 'ModulesTy',
+-- building it for a @vs@ of given 'Len'.
+readTyName ::
+ Source src =>
+ Imports NameTy ->
+ ModulesTy src -> src -> Mod NameTy ->
+ Either (Error_Type src) (TypeTLen src)
+readTyName is ms src name@(m `Mod` n) =
+       let m' = fromMaybe m $ lookupImports FixyInfix name is in
+       case Map.lookup (m' `Mod` n) ms of
+        Just t -> Right t
+        Nothing -> Left $ Error_Type_Constant_unknown $ At src name
+
+-- * Type 'Error_Type'
+data Error_Type src
+ =   Error_Type_Constant_unknown (At src (Mod NameTy))
+ |   Error_Type_Con_Kind         (Con_Kind src)
+ deriving (Eq, Show)
+instance ErrorInj (Error_Type src) (Error_Type src) where
+       errorInj = id
+instance ErrorInj (Con_Kind src) (Error_Type src) where
+       errorInj = Error_Type_Con_Kind
 
 -- | List of the rules of 'Gram_Type'.
-gram_type :: Gram_Type src g => [CF g (AST_Type src)]
+gram_type :: Gram_Type () g => [CF g (AST_Type ())]
 gram_type =
  [ g_type
  , g_type_fun
@@ -125,6 +291,7 @@ gram_type =
  , g_type_tuple2
  , g_type_app
  , g_type_atom
- , g_type_name
- , g_type_symbol
+ , g_type_const
+ , g_type_var
+ -- , g_type_symbol
  ]