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