]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Read.hs
Improve handling of metadata in grammars.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Read.hs
1 {-# LANGUAGE PolyKinds #-}
2 module Language.Symantic.Typing.Read where
3
4 import Data.Map.Strict (Map)
5 import Data.Typeable
6 import qualified Data.Map.Strict as Map
7 import qualified Data.Text as Text
8
9 import Language.Symantic.Grammar
10 import Language.Symantic.Typing.List
11 import Language.Symantic.Typing.Kind
12 import Language.Symantic.Typing.Type
13 import Language.Symantic.Typing.Show ()
14 import Language.Symantic.Typing.Grammar
15 import Language.Symantic.Typing.Variable
16
17 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
18 readTy ::
19 Inj_Source (KindK src) src =>
20 Inj_Source (TypeVT src) src =>
21 Inj_Source (AST_Type src) src =>
22 Name2Type src ->
23 AST_Type src ->
24 Either (Error_Type src) (TypeVT src)
25 readTy cs ast | EVars vs <- readVars (EVars VarsZ) ast = do
26 TypeT ty <- readTyVars cs vs ast
27 Right $ TypeVT ty
28
29 -- | Read a 'Type' from an 'AST_Type', given its 'Vars'.
30 readTyVars ::
31 forall vs src.
32 Inj_Source (KindK src) src =>
33 Inj_Source (TypeVT src) src =>
34 Inj_Source (AST_Type src) src =>
35 Name2Type src ->
36 Vars src vs ->
37 AST_Type src ->
38 Either (Error_Type src) (TypeT src vs)
39 readTyVars cs vs ast@(BinTree0 (Token_Type_Const (At _src name))) =
40 read_TyConst cs (inj_Source ast) (lenVars vs) name
41 readTyVars _cs vs ast@(BinTree0 (Token_Type_Var (At _src name))) =
42 case lookupVars name vs of
43 Just (EVar v) -> Right $ TypeT $ TyVar (inj_Source ast) name v
44 Nothing -> error "[BUG] readTyVars: lookupVars failed"
45 readTyVars cs vs ast@(ast_x `BinTree2` ast_y) = do
46 TypeT ty_x <- readTyVars cs vs ast_x
47 TypeT ty_y <- readTyVars cs vs ast_y
48 when_KiFun (kindOf ty_x) $ \Refl ki_x_a _ki_x_b ->
49 when_EqKind ki_x_a (kindOf ty_y) $ \Refl ->
50 Right $ TypeT $ TyApp (inj_Source ast) ty_x ty_y
51
52 -- | Lookup a 'TyConst' associated with given 'NameTy' in given 'Name2Type',
53 -- building it for a @vs@ of given 'Len'.
54 read_TyConst ::
55 Source src =>
56 Name2Type src -> src -> Len vs -> NameTy ->
57 Either (Error_Type src) (TypeT src vs)
58 read_TyConst cs src len name =
59 case Map.lookup name cs of
60 Just (Len2Type t) -> Right $ t len
61 Nothing -> Left $ Error_Type_Constant_unknown $ At src name
62
63 -- | Return the given 'EVars' augmented by the ones used in given 'AST_Type'.
64 readVars :: Source src => EVars src -> AST_Type src -> EVars src
65 readVars evs@(EVars vs) (BinTree0 (Token_Type_Var (At _src name))) =
66 case lookupVars name vs of
67 Just{} -> evs
68 Nothing -> do
69 let kv = KiType noSource
70 let vs' = VarsS name kv vs
71 EVars vs'
72 readVars evs BinTree0{} = evs
73 readVars evs (BinTree2 x y) =
74 readVars (readVars evs x) y
75
76 -- * Type 'Name2Type'
77 type Name2Type src = Map NameTy (Len2Type src)
78
79 -- ** Type 'Len2Type'
80 -- | Like 'TypeT', but needing a @(@'Len'@ vs)@ to be built.
81 --
82 -- Useful to build a 'Name2Type' which can be used
83 -- whatever will be the @(@'Len'@ vs)@ given to 'readTyVars'.
84 data Len2Type src = Len2Type (forall vs. Len vs -> TypeT src vs)
85 instance Source src => Show (Len2Type src) where
86 showsPrec p (Len2Type t) = showsPrec p $ t LenZ
87
88 -- ** Class 'Inj_Name2Type'
89 -- | Derive a 'Name2Type' from the given type-level list
90 -- of 'Proxy'-fied /type constants/.
91 class Inj_Name2Type cs where
92 inj_Name2Type :: Source src => proxy cs -> Name2Type src
93 instance Inj_Name2Type '[] where
94 inj_Name2Type _cs = Map.empty
95 instance
96 ( Inj_KindP (Ty_of_Type (K c))
97 , K c ~ Type_of_Ty (Ty_of_Type (K c))
98 , Constable c
99 , Inj_Name2Type cs
100 ) => Inj_Name2Type (Proxy c ': cs) where
101 inj_Name2Type _cs =
102 Map.insert
103 (NameTy $ Text.pack $ show $ typeRep (Proxy @c))
104 (Len2Type $ \len -> TypeT $ TyConst noSource len $
105 inj_ConstKi @(K c) @c $
106 inj_KindP (Proxy @(Ty_of_Type (K c))) noSource) $
107 inj_Name2Type (Proxy @cs)
108
109 -- * Type 'Error_Type'
110 data Error_Type src
111 = Error_Type_Constant_unknown (At src NameTy)
112 | Error_Type_Con_Kind (Con_Kind src)
113 deriving (Eq, Show)
114 instance Inj_Error (Error_Type src) (Error_Type src) where
115 inj_Error = id
116 instance Inj_Error (Con_Kind src) (Error_Type src) where
117 inj_Error = Error_Type_Con_Kind