2 module Language.Symantic.Compiling.Read where
4 import Control.Arrow (left)
5 import qualified Data.Kind as K
7 import Language.Symantic.Grammar
8 import Language.Symantic.Typing
10 import Language.Symantic.Compiling.Grammar
11 import Language.Symantic.Compiling.Term
12 import Language.Symantic.Compiling.Beta
14 -- | Read a 'TermVT' from and 'AST_Term'.
18 Inj_Source (TypeVT src) src =>
19 Inj_Source (KindK src) src =>
20 Inj_Source (AST_Type src) src =>
25 Either (Error_Term src) (TermVT src ss ts)
26 readTe cs ast ctxTe = do
27 ts <- go ctxTe `traverse` ast
28 inj_Error `left` betasTe ts
34 Either (Error_Term src) (TermVT src ss ts')
35 go _ts (Token_Term (TermVT_CF te)) = Right $ TermVT te
36 go ts (Token_Term_Var _src name) = teVar name ts
37 go _ts (Token_Term_App _src) = Right $ TermVT teApp
38 go ts (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
39 TypeVT ty_arg <- inj_Error `left` readTy cs ast_ty_arg
40 when_EqKind (inj_Kind @K.Type) (kindOf ty_arg) $ \Refl ->
41 case lenVars ty_arg of
42 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
43 LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
44 TermVT (Term qr tr (TeSym res)) <- readTe cs ast_body (CtxTyS name_arg ta ts)
45 let (qa', qr') = appendVars qa qr
46 let (ta', tr') = appendVars ta tr
47 Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') (ta' ~> tr') $
48 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
49 go ts (Token_Term_Let _src name ast_arg ast_body) = do
50 TermVT (Term qa ta (TeSym arg)) <- readTe cs ast_arg ts
52 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
54 TermVT (Term qr tr (TeSym res)) <- readTe cs ast_body $ CtxTyS name ta ts
55 let (qa', qr') = appendVars qa qr
56 let tr' = allocVarsL (lenVars ta) tr
57 Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) (qa' # qr') tr' $
58 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
63 NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
64 teVar name CtxTyZ = Left $ Error_Term_unbound name
65 teVar name (CtxTyS n ty _) | n == name =
66 Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) noConstraint ty $
67 TeSym $ \(te `CtxTeS` _) -> te
68 teVar name (CtxTyS _n _typ ts') = do
69 TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
70 Right $ TermVT $ Term @_ @_ @_ @_ @(_ #> _) q t $
71 TeSym $ \(_ `CtxTeS` ts) -> te ts
74 Source src => Constable (->) =>
75 Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] ((a -> b) -> a -> b)
77 Term noConstraint ((a ~> b) ~> a ~> b) $
80 a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)
82 b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)
83 b = tyVar "b" $ VarS varZ
85 -- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.
87 -- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.
88 reduceTeApp :: AST_Term src ss -> AST_Term src ss
89 reduceTeApp (BinTree2 x y) =
91 BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y
92 _ -> reduceTeApp x `BinTree2` reduceTeApp y
93 reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)
94 reduceTeApp (BinTree0 (Token_Term_Let src n bo te)) = BinTree0 $ Token_Term_Let src n (reduceTeApp bo) (reduceTeApp te)
95 reduceTeApp x@BinTree0{} = x
99 -- accumulating at each /lambda abstraction/
100 -- the 'Type' of the introduced variable.
101 -- It is built top-down from the closest
102 -- including /lambda abstraction/ to the farest.
103 data CtxTy src (ts::[K.Type]) where
104 CtxTyZ :: CtxTy src '[]
108 -> CtxTy src (t ': ts)
114 -> CtxTy src (ts0 ++ ts1)
115 appendCtxTy CtxTyZ c = c
116 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
118 -- * Type 'Error_Term'
120 = Error_Term_unbound NameTe
121 | Error_Term_polymorphic (TypeVT src)
122 | Error_Term_qualified (TypeVT src)
123 | Error_Term_Type (Error_Type src)
124 | Error_Term_Beta (Error_Beta src)
125 {- Error_Term_Con_Type (Con_Type src ss) -}
126 {- Error_Term_Con_Kind (Con_Kind src) -}
128 instance Inj_Error (Error_Type src) (Error_Term src) where
129 inj_Error = Error_Term_Type
130 instance Inj_Error (Error_Beta src) (Error_Term src) where
131 inj_Error = Error_Term_Beta
132 instance Inj_Error (Con_Kind src) (Error_Term src) where
133 inj_Error = Error_Term_Type . inj_Error
139 | SrcTe_AST_Term (AST_Term (SrcTe txt ss) ss)
140 | SrcTe_AST_Type (AST_Type (SrcTe txt ss))
141 | SrcTe_Kind (KindK (SrcTe txt ss))
142 | SrcTe_Type (TypeVT (SrcTe txt ss))
146 type instance Text_of_Source (SrcTe txt ss) = txt
148 instance Source (SrcTe txt ss) where
149 noSource = SrcTe_Less
150 instance Inj_Source txt (SrcTe txt ss) where
151 inj_Source = SrcTe_Text
152 instance Inj_Source (AST_Term (SrcTe txt ss) ss) (SrcTe txt ss) where
153 inj_Source = SrcTe_AST_Term
154 instance Inj_Source (AST_Type (SrcTe txt ss)) (SrcTe txt ss) where
155 inj_Source = SrcTe_AST_Type
156 instance Inj_Source (KindK (SrcTe txt ss)) (SrcTe txt ss) where
157 inj_Source = SrcTe_Kind
158 instance Inj_Source (TypeVT (SrcTe txt ss)) (SrcTe txt ss) where
159 inj_Source = SrcTe_Type