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