]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Compiling/Read.hs
Update to lastest symantic-document
[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Read.hs
1 {-# LANGUAGE GADTs #-}
2 module Language.Symantic.Compiling.Read where
3
4 import Control.Arrow (left)
5 import qualified Data.Kind as K
6
7 import Language.Symantic.Grammar
8 import Language.Symantic.Typing
9
10 import Language.Symantic.Compiling.Term
11 import Language.Symantic.Compiling.Module
12 import Language.Symantic.Compiling.Beta
13
14 -- * Type 'ReadTerm'
15 -- | Convenient type alias for 'readTerm' and related functions.
16 type ReadTerm src ss ts =
17 Source src =>
18 SourceInj (TypeVT src) src =>
19 SourceInj (KindK src) src =>
20 SourceInj (AST_Type src) src =>
21 Constable (->) =>
22 CtxTy src ts ->
23 AST_Term src ss ->
24 Either (Error_Term src) (TermVT src ss ts)
25
26 -- | Read a 'TermVT' from and 'AST_Term'.
27 readTerm :: forall src ss ts. ReadTerm src ss ts
28 readTerm ctxTy ast = do
29 ts <- go ctxTy `traverse` ast
30 errorInj `left` betaTerms ts
31 where
32 go ::
33 forall ts'.
34 CtxTy src ts' ->
35 Token_Term src ss ->
36 Either (Error_Term src) (TermVT src ss ts')
37 go _ts (Token_Term (TermAVT te)) = Right $ TermVT te
38 go _ts (Token_TermVT te) = Right $ liftTermVT te
39 go ts (Token_Term_Var _src name) = teVar name ts
40 go _ts (Token_Term_App _src) = Right $ TermVT teApp
41 go ts (Token_Term_Abst _src name_arg ast_ty_arg ast_body) = do
42 TypeVT ty_arg <- errorInj `left` readType ast_ty_arg
43 when_EqKind (kindInj @K.Type) (kindOf ty_arg) $ \Refl ->
44 case lenVars ty_arg of
45 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT ty_arg
46 LenZ | (TypeK qa, TypeK ta) <- unQualTy ty_arg -> do
47 TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name_arg ta ts) ast_body
48 let (qa', qr') = appendVars qa qr
49 let (ta', tr') = appendVars ta tr
50 Right $
51 case (proveConstraint qa', proveConstraint qr') of
52 -- NOTE: remove provable Constraints to keep those smaller.
53 (Just Dict, Just Dict) -> TermVT $
54 Term (noConstraintLen (lenVars tr')) (ta' ~> tr') $
55 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
56 (Just Dict, Nothing) -> TermVT $
57 Term qr' (ta' ~> tr') $
58 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
59 (Nothing, Just Dict) -> TermVT $
60 Term qa' (ta' ~> tr') $
61 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
62 (Nothing, Nothing) -> TermVT $
63 Term (qa' # qr') (ta' ~> tr') $
64 TeSym $ \c -> lam $ \arg -> res (arg `CtxTeS` c)
65 go ts (Token_Term_Let _src name ast_arg ast_body) = do
66 TermVT (Term qa ta (TeSym arg)) <- readTerm ts ast_arg
67 case lenVars ta of
68 LenS{} -> Left $ Error_Term_polymorphic $ TypeVT (qa #> ta)
69 LenZ -> do
70 TermVT (Term qr tr (TeSym res)) <- readTerm (CtxTyS name ta ts) ast_body
71 let (qa', qr') = appendVars qa qr
72 let tr' = allocVarsL (lenVars ta) tr
73 Right $
74 case (proveConstraint qa', proveConstraint qr') of
75 -- NOTE: remove provable Constraints to keep those smaller.
76 (Just Dict, Just Dict) -> TermVT $
77 Term (noConstraintLen (lenVars tr')) tr' $
78 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
79 (Just Dict, Nothing) -> TermVT $
80 Term qr' tr' $
81 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
82 (Nothing, Just Dict) -> TermVT $
83 Term qa' tr' $
84 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
85 (Nothing, Nothing) -> TermVT $
86 Term (qa' # qr') tr' $
87 TeSym $ \c -> let_ (arg c) $ \a -> res (a `CtxTeS` c)
88
89 teVar ::
90 forall ss src ts.
91 Source src =>
92 NameTe -> CtxTy src ts -> Either (Error_Term src) (TermVT src ss ts)
93 teVar name CtxTyZ = Left $ Error_Term_unknown name
94 teVar name (CtxTyS n ty _) | n == name =
95 Right $ TermVT $ Term noConstraint ty $
96 TeSym $ \(te `CtxTeS` _) -> te
97 teVar name (CtxTyS _n _typ ts') = do
98 TermVT (Term q t (TeSym te)) <- teVar @ss name ts'
99 Right $ TermVT $ Term q t $
100 TeSym $ \(_ `CtxTeS` ts) -> te ts
101
102 teApp ::
103 Source src => Constable (->) =>
104 Term src ss ts '[Proxy (a::K.Type), Proxy (b::K.Type)] (() #> ((a -> b) -> a -> b))
105 teApp =
106 Term noConstraint ((a ~> b) ~> a ~> b) $
107 TeSym $ const apply
108 where
109 a :: Source src => Type src '[Proxy a, Proxy b] (a::K.Type)
110 a = tyVar "a" $ varZ
111 b :: Source src => Type src '[Proxy a, Proxy b] (b::K.Type)
112 b = tyVar "b" $ VarS varZ
113
114 -- | Reduce number of 'Token_Term_App' in given 'AST_Term' by converting them into 'BinTree2'.
115 --
116 -- NOTE: 'Token_Term_App' exists only to handle unifix operators applied to arguments.
117 reduceTeApp :: AST_Term src ss -> AST_Term src ss
118 reduceTeApp (BinTree2 x y) =
119 case reduceTeApp x of
120 BinTree0 Token_Term_App{} `BinTree2` x' -> reduceTeApp x' `BinTree2` reduceTeApp y
121 _ -> reduceTeApp x `BinTree2` reduceTeApp y
122 reduceTeApp (BinTree0 (Token_Term_Abst src n ty te)) = BinTree0 $ Token_Term_Abst src n ty (reduceTeApp te)
123 reduceTeApp (BinTree0 (Token_Term_Let src n bo te)) = BinTree0 $ Token_Term_Let src n (reduceTeApp bo) (reduceTeApp te)
124 reduceTeApp x@BinTree0{} = x
125
126 -- ** Type 'ReadTermCF'
127 -- | Like 'ReadTerm', but 'CtxTe'-free.
128 --
129 -- Useful in 'readTermWithCtx' to help GHC's type solver, which
130 -- "Cannot instantiate unification variable with a type involving foralls".
131 newtype ReadTermCF src ss
132 = ReadTermCF
133 { unReadTermCF :: forall ts. ReadTerm src ss ts }
134
135 -- | Like 'readTerm' but with given context, and no more.
136 readTermWithCtx ::
137 Foldable f =>
138 Source src =>
139 SourceInj (TypeVT src) src =>
140 SourceInj (KindK src) src =>
141 SourceInj (AST_Type src) src =>
142 Constable (->) =>
143 f (NameTe, TermT src ss '[] '[]) ->
144 AST_Term src ss ->
145 Either (Error_Term src) (TermVT src ss '[])
146 readTermWithCtx env =
147 readTermWithCtxClose $
148 readTermWithCtxPush env readTerm
149
150 -- | Like 'readTerm' but with given context.
151 readTermWithCtxPush ::
152 Foldable f =>
153 f (NameTe, TermT src ss '[] '[]) ->
154 (forall ts'. ReadTerm src ss ts') ->
155 ReadTerm src ss ts
156 readTermWithCtxPush env readTe =
157 unReadTermCF $ foldr
158 (\t (ReadTermCF r) -> ReadTermCF $ readTermWithCtxPush1 t r)
159 (ReadTermCF readTe) env
160
161 -- | Like 'readTerm' but with given 'TermT' pushed onto 'CtxTy' and 'CtxTe'.
162 readTermWithCtxPush1 ::
163 (NameTe, TermT src ss '[] '[]) ->
164 (forall ts'. ReadTerm src ss ts') ->
165 ReadTerm src ss ts
166 readTermWithCtxPush1 (n, TermT (Term qn tn (TeSym te_n))) readTe ctxTy ast = do
167 TermVT (Term q t (TeSym te)) <- readTe (CtxTyS n (qn #> tn) ctxTy) ast
168 case proveConstraint qn of
169 Nothing -> Left $ Error_Term_proofless $ TypeVT qn
170 Just Dict ->
171 Right $ TermVT $ Term q t $ TeSym $ \c ->
172 let cte = qual qn $ te_n CtxTeZ in
173 te $ cte `CtxTeS` c
174
175 -- | Close a 'ReadTerm' context.
176 readTermWithCtxClose ::
177 (forall ts'. ReadTerm src ss ts') ->
178 Source src =>
179 SourceInj (TypeVT src) src =>
180 SourceInj (KindK src) src =>
181 SourceInj (AST_Type src) src =>
182 Constable (->) =>
183 AST_Term src ss ->
184 Either (Error_Term src) (TermVT src ss '[])
185 readTermWithCtxClose readTe = readTe CtxTyZ
186
187 -- * Type 'CtxTy'
188 -- | /Typing context/
189 -- accumulating at each /lambda abstraction/
190 -- the 'Type' of the introduced variable.
191 -- It is built top-down from the closest
192 -- including /lambda abstraction/ to the farest.
193 -- It determines the 'Type's of 'CtxTe'.
194 data CtxTy src (ts::[K.Type]) where
195 CtxTyZ :: CtxTy src '[]
196 CtxTyS :: NameTe
197 -> Type src '[] t
198 -> CtxTy src ts
199 -> CtxTy src (t ': ts)
200 infixr 5 `CtxTyS`
201
202 appendCtxTy ::
203 CtxTy src ts0 ->
204 CtxTy src ts1 ->
205 CtxTy src (ts0 ++ ts1)
206 appendCtxTy CtxTyZ c = c
207 appendCtxTy (CtxTyS n t c) c' = CtxTyS n t $ appendCtxTy c c'
208
209 -- * Type 'Error_Term'
210 data Error_Term src
211 = Error_Term_unknown NameTe
212 | Error_Term_polymorphic (TypeVT src)
213 | Error_Term_qualified (TypeVT src)
214 | Error_Term_proofless (TypeVT src)
215 | Error_Term_Type (Error_Type src)
216 | Error_Term_Beta (Error_Beta src)
217 {- Error_Term_Con_Type (Con_Type src ss) -}
218 {- Error_Term_Con_Kind (Con_Kind src) -}
219 deriving (Eq, Show)
220 instance ErrorInj (Error_Type src) (Error_Term src) where
221 errorInj = Error_Term_Type
222 instance ErrorInj (Error_Beta src) (Error_Term src) where
223 errorInj = Error_Term_Beta
224 instance ErrorInj (Con_Kind src) (Error_Term src) where
225 errorInj = Error_Term_Type . errorInj
226
227 -- * Type 'SrcTe'
228 -- | A 'Source' usable when using 'readTerm'.
229 data SrcTe inp ss
230 = SrcTe_Less
231 | SrcTe_Input (Span inp)
232 | SrcTe_AST_Term (AST_Term (SrcTe inp ss) ss)
233 | SrcTe_AST_Type (AST_Type (SrcTe inp ss))
234 | SrcTe_Kind (KindK (SrcTe inp ss))
235 | SrcTe_Type (TypeVT (SrcTe inp ss))
236 | SrcTe_Term
237 deriving (Eq, Show)
238
239 type instance Source_Input (SrcTe inp ss) = inp
240
241 instance Source (SrcTe inp ss) where
242 noSource = SrcTe_Less
243 instance SourceInj (Span inp) (SrcTe inp ss) where
244 sourceInj = SrcTe_Input
245 instance SourceInj (AST_Term (SrcTe inp ss) ss) (SrcTe inp ss) where
246 sourceInj = SrcTe_AST_Term
247 instance SourceInj (AST_Type (SrcTe inp ss)) (SrcTe inp ss) where
248 sourceInj = SrcTe_AST_Type
249 instance SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss) where
250 sourceInj = SrcTe_Kind
251 instance SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss) where
252 sourceInj = SrcTe_Type