]> Git — Sourcephile - tmp/julm/symantic.git/blob - src/Symantic/Syntaxes.hs
7b491bbef2cbfd95760bfeb4e6eec8d107fa9b5a
[tmp/julm/symantic.git] / src / Symantic / Syntaxes.hs
1 {-# LANGUAGE AllowAmbiguousTypes #-}
2 {-# LANGUAGE ConstraintKinds #-}
3 {-# LANGUAGE DataKinds #-}
4 {-# LANGUAGE EmptyDataDeriving #-}
5 {-# LANGUAGE PolyKinds #-}
6 {-# LANGUAGE QuantifiedConstraints #-}
7 {-# LANGUAGE RankNTypes #-}
8 {-# LANGUAGE UndecidableInstances #-}
9 {-# LANGUAGE UndecidableSuperClasses #-}
10 {-# LANGUAGE ViewPatterns #-}
11 {-# LANGUAGE NoMonomorphismRestriction #-}
12 {-# OPTIONS_GHC -Wno-missing-signatures #-}
13 {-# OPTIONS_GHC -Wno-orphans #-}
14
15 -- {-# OPTIONS_GHC -Wno-monomorphism-restriction #-}
16
17 module Symantic.Syntaxes where
18
19 import Control.Arrow (left)
20 import Data.Either (Either (..))
21 import Data.Eq (Eq (..))
22 import Data.Function (fix, ($), (.))
23 import Data.Int (Int)
24 import Data.Kind (Type)
25 import Data.Maybe (Maybe (..))
26 import Data.Monoid (Monoid (..))
27 import Data.Void (Void)
28 import Symantic.Semantics.Forall (Forall (..), PerSyntax, PerSyntaxable (..))
29 import Symantic.Syntaxes.Classes (Instantiable (..), Syntaxes, Unabstractable)
30 import Symantic.Syntaxes.Classes qualified as Sym
31 import Text.Show (Show (..))
32 import Type.Reflection (eqTypeRep, typeRep, (:~~:) (..))
33 import Prelude (error)
34
35 import Symantic
36 import Symantic.Typer ()
37
38 parse ::
39 forall syns prov finalSyns.
40 finalSyns ~ (Instantiable ': Unabstractable ': syns) =>
41 (forall k. ProvenanceKindOf (Ty @k) prov) =>
42 (forall k. ProvenanceKindOf (Var @k) prov) =>
43 Show prov =>
44 Monoid prov =>
45 Syntaxes finalSyns (Forall finalSyns) =>
46 Parsers finalSyns finalSyns prov =>
47 TermAST prov ->
48 Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov '[])
49 parse ast = unParser (fix openParser ast) CtxTyZ
50 where
51 openParser final (BinTree0 e) = parsers @finalSyns @finalSyns @prov final e
52 -- Instantiable and Unabstractable are always required.
53 openParser final (BinTree2 fT xT) = Parser $ \ctx -> do
54 TermVT fTy (f :: OpenTerm finalSyns fVS a2b) <- unParser (final fT) ctx
55 TermVT xTy (a :: OpenTerm finalSyns aVS a) <- unParser (final xT) ctx
56 case fTy of
57 SkipTyProv
58 TyApp
59 { tyAppFun =
60 SkipTyProv
61 TyApp
62 { tyAppFun = TyConst{tyConst = eqTypeRep (typeRep @(->)) -> Just HRefl}
63 , tyAppArg = fxTy
64 }
65 , tyAppArg = rTy
66 } -> do
67 let (fxTy', xTy') = appendVars fxTy xTy
68 mgu <- (perSyntax . ErrorParserInstantiableUnify) `left` unifyType mempty fxTy' xTy'
69 let fxTy'' = subst mgu fxTy'
70 let xTy'' = subst mgu xTy'
71 case eqTy fxTy'' xTy'' of
72 Nothing -> Left $ perSyntax $ ErrorParserInstantiableArgumentMismatch (TyVT fxTy'') (TyVT xTy'')
73 Just HRefl ->
74 normalizeVarsTy rTy $ \case
75 -- TyApp (TyApp _c qr') tr' ->
76 rTy' ->
77 Right $ TermVT rTy' (f .@ a)
78 _ -> Left $ perSyntax $ ErrorParserInstantiableNotAFunction (TyVT fTy)
79 data instance ErrorParser prov Instantiable
80 = ErrorParserInstantiableArgumentMismatch (TyVT prov) (TyVT prov)
81 | ErrorParserInstantiableNotAFunction (TyVT prov)
82 | ErrorParserInstantiableUnify (ErrorUnify prov)
83 deriving (Show)
84
85 -- * Class 'Parsers'
86 class Parsers syns finalSyns prov where
87 parsers :: OpenParser finalSyns prov
88 instance PerSyntaxable finalSyns Unabstractable => Parsers '[] finalSyns prov where
89 parsers _final tok = Parser $ \_ctx ->
90 Left $ perSyntax $ ErrorParserUnabstractableInvalid tok
91 data instance ErrorParser prov Unabstractable
92 = ErrorParserUnabstractableInvalid (TokenTerm prov)
93 deriving (Show)
94 instance
95 ( TokenParser syn finalSyns prov
96 , Parsers syns finalSyns prov
97 ) =>
98 Parsers (syn ': syns) finalSyns prov
99 where
100 parsers final = tokenParser @syn @finalSyns (parsers @syns @finalSyns final) final
101
102 -- ** Type 'OpenParser'
103 type OpenParser syns prov =
104 Show prov =>
105 Monoid prov =>
106 {-final-} (TermAST prov -> Parser syns prov) ->
107 TokenTerm prov ->
108 Parser syns prov
109
110 -- ** Class 'TokenParser'
111 class TokenParser syn finalSyns prov where
112 tokenParser ::
113 {-next-} (TokenTerm prov -> Parser finalSyns prov) ->
114 OpenParser finalSyns prov
115 instance
116 ( Syntaxes finalSyns (Forall finalSyns)
117 ) =>
118 TokenParser Instantiable finalSyns prov
119 where
120 tokenParser next _final = next
121 data instance ErrorParser prov (AbstractableTy (Ty prov '[]))
122 = ErrorParserAbstractableUnknown Name
123 | ErrorParserAbstractableNotAType (TyVT prov)
124 deriving (Show)
125 instance
126 ( Syntaxes finalSyns (Forall finalSyns)
127 , forall sem. Syntaxes finalSyns sem => Unabstractable sem
128 , forall sem. Syntaxes finalSyns sem => Instantiable sem
129 , PerSyntaxable finalSyns (AbstractableTy (Ty prov '[]))
130 , forall k. ProvenanceKindOf (Ty @k) prov
131 ) =>
132 TokenParser (AbstractableTy (Ty prov '[])) finalSyns prov
133 where
134 tokenParser _next _final (TokenTermVar varName) = Parser go
135 where
136 go :: forall vs. CtxTy prov vs Void -> Either (PerSyntax finalSyns (ErrorParser prov)) (TermVT finalSyns prov vs)
137 go CtxTyZ = Left $ perSyntax $ ErrorParserAbstractableUnknown varName
138 go (CtxTyS n ty _) | n == varName = Right $ TermVT ty V
139 go (CtxTyS _n _typ tys) = do
140 TermVT ty ot <- go tys
141 Right $ TermVT ty (W ot)
142 tokenParser _next final (TokenTermAbst argName (TyT (argTy :: Ty prov '[] a)) bT) =
143 Parser $ \ctx ->
144 case eqTy (monoTy @Type @prov) (kindOf argTy) of
145 Nothing -> Left $ perSyntax $ ErrorParserAbstractableNotAType (TyVT argTy)
146 Just HRefl -> do
147 TermVT resTy (res :: OpenTerm syn bVS res) <-
148 unParser (final bT) (CtxTyS argName argTy ctx)
149 let argTy' = allocVarsR (lenVar resTy) argTy
150 Right $
151 TermVT (argTy' ~> resTy) $
152 case res of
153 E d -> E (Sym.const .@ d)
154 V -> E Sym.id
155 W e -> E Sym.const `appOpenTerm` e
156 N e -> e
157 tokenParser next _final e = next e
158 instance
159 ( Syntaxes finalSyns (Forall finalSyns)
160 , forall sem. Syntaxes finalSyns sem => Addable sem
161 ) =>
162 TokenParser Addable finalSyns prov
163 where
164 tokenParser next _final = \case
165 TokenTermAtom s
166 | Right (i :: Int) <- safeRead s ->
167 Parser $ \ctx ->
168 Right
169 $ TermVT
170 (tyOfTypeRep (lenVar ctx) (typeRep @Int))
171 $ E
172 $ Forall @_ @Int
173 $ lit i
174 TokenTermAtom "neg" -> Parser $ \_ctx ->
175 Right $ TermVT (monoTy @Int ~> monoTy @Int) $ E neg
176 TokenTermAtom "add" -> Parser $ \_ctx ->
177 Right $ TermVT (monoTy @Int ~> monoTy @Int ~> monoTy @Int) $ E add
178 ast -> next ast
179 instance
180 ( Syntaxes syns (Forall syns)
181 , forall sem. Syntaxes syns sem => Unabstractable sem
182 ) =>
183 TokenParser Unabstractable syns prov
184 where
185 tokenParser next _final = \case
186 TokenTermAtom "id" -> Parser $ \_ctx ->
187 Right $ TermVT (aTy @'[] ~> aTy) $ E Sym.id
188 TokenTermAtom "(<*>)" -> Parser $ \_ctx ->
189 Right $
190 TermVT ((aTy ~> bTy ~> cTy @'[]) ~> (aTy ~> bTy) ~> aTy ~> cTy) $
191 E Sym.ap
192 TokenTermAtom "const" -> Parser $ \_ctx ->
193 Right $ TermVT (aTy ~> bTy @'[] ~> aTy) $ E Sym.const
194 TokenTermAtom "(.)" -> Parser $ \_ctx ->
195 Right $ TermVT ((bTy ~> cTy @'[]) ~> (aTy ~> bTy) ~> aTy ~> cTy) $ E (Sym..)
196 TokenTermAtom "flip" -> Parser $ \_ctx ->
197 Right $ TermVT ((aTy ~> bTy ~> cTy @'[]) ~> bTy ~> aTy ~> cTy) $ E (Sym.flip)
198 TokenTermAtom "($)" -> Parser $ \_ctx ->
199 Right $ TermVT ((aTy ~> bTy @'[]) ~> aTy ~> bTy) $ E (Sym.$)
200 tok -> next tok
201
202 -- * Class 'Addable'
203 class Addable sem where
204 lit :: Int -> sem Int
205 neg :: sem (Int -> Int)
206 add :: sem (Int -> Int -> Int)
207 data instance ErrorParser prov Addable
208 deriving (Show)
209
210 -- * Class 'Mulable'
211 class Mulable sem where
212 mul :: sem Int -> sem Int -> sem Int
213 instance (forall sem. Syntaxes syn sem => Addable sem) => Addable (Forall syn) where
214 lit n = Forall (lit n)
215 neg = Forall neg
216 add = Forall add
217 instance (forall sem. Syntaxes syn sem => Mulable sem) => Mulable (Forall syn) where
218 mul (Forall a) (Forall b) = Forall (mul a b)
219
220 --
221 -- Parsing
222 --
223
224 -- tree0Parser :: (forall sem. syn sem => Addable sem, syn (Forall syn)) => Either ErrMsg (Forall syn Int)
225 -- tree0Parser = unParser $ parse tree0Print
226
227 -- parseMulable ::
228 -- forall syn prov.
229 -- ( forall sem. syn sem => Mulable sem
230 -- , forall sem. syn sem => Addable sem
231 -- , syn (Forall syn)
232 -- ) =>
233 -- Monoid prov =>
234 -- Show prov =>
235 -- (TermAST prov -> Parser syn prov) ->
236 -- TermAST prov -> Parser syn prov
237 -- parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "mul")) aT) bT) =
238 -- Parser $ \ctx -> do
239 -- case (final aT, final bT) of
240 -- (Parser aE, Parser bE) -> do
241 -- TermVT aTy (Forall a :: Forall syn a) <- aE ctx
242 -- case eqTy aTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar aTy} of
243 -- Nothing -> Left "TypeError: Mulable 1"
244 -- Just HRefl -> do
245 -- TermVT bTy (Forall b :: Forall syn b) <- bE ctx
246 -- case eqTy bTy TyConst{tyConst = Const{constType = typeRep @Int, constMeta = mempty::prov}, tyConstLen = lenVar bTy} of
247 -- Nothing -> Left "TypeError: Mulable 2"
248 -- Just HRefl -> do
249 -- Right $ TermVT aTy (Forall @_ @a $ mul a b)
250 -- parseMulable final t = parseAddable final t
251
252 --
253 -- Printing
254 --
255
256 printConst n = Printer (BinTree0 (TokenTermAtom n))
257
258 instance Sym.Unabstractable (Printer prov) where
259 ap = printConst "(<*>)"
260 const = printConst "const"
261 id = printConst "id"
262 (.) = printConst "(.)"
263 flip = printConst "flip"
264 ($) = printConst "($)"
265 instance Addable (Printer prov) where
266 lit n = Printer $ BinTree0 (TokenTermAtom (show n))
267 neg = printConst "neg"
268 add = printConst "add"
269 instance Mulable (Printer prov) where
270 mul = print2 "mul"
271 instance Instantiable (Printer prov) where
272 Printer f .@ Printer a = Printer $ BinTree2 f a
273 instance (Monoid prov) => AbstractableTy (Ty prov '[]) (Printer prov) where
274 lamTy xTy (f :: Printer prov a -> Printer prov b) =
275 Printer $
276 BinTree0
277 ( TokenTermAbst
278 "x"
279 (TyT xTy)
280 (unPrinter (f (Printer (BinTree0 (TokenTermVar "x")))))
281 )
282
283 -- * Type 'FinalSyntaxes'
284 type FinalSyntaxes prov = '[AbstractableTy (Ty prov '[]), Addable]
285
286 -- tree0 = lit 0
287 tree0 = add .@ lit 8 .@ (neg .@ (add .@ lit 1 .@ lit 2))
288
289 -- tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
290 tree2 = fun @() (\x -> add .@ x .@ lit 0)
291 tree3 = fun @() (\x -> add .@ x .@ x)
292 tree4 = Sym.ap .@ add .@ Sym.id
293 tree0Print = print tree0
294
295 -- tree1Print = print tree1
296 tree2Print = print tree2
297 tree3Print = print tree3
298 tree4Print = print tree4
299
300 tree0ParsePrint :: TermAST ()
301 tree0ParsePrint = case parse @(FinalSyntaxes ()) @() tree0Print of
302 Left e -> error $ show e
303 Right (TermVT _ty (unE -> Forall sem)) -> print sem
304
305 -- tree1ParsePrint :: TermAST ()
306 -- tree1ParsePrint = case parse @(FinalSyntaxes ()) @() tree1Print of
307 -- Left e -> error e
308 -- Right (TermVT _ty (unE -> Forall sem)) -> print sem
309
310 tree2ParsePrint :: TermAST ()
311 tree2ParsePrint = case parse @(FinalSyntaxes ()) @() tree2Print of
312 Left e -> error $ show e
313 Right (TermVT _ty (unE -> Forall sem)) -> print sem
314
315 tree3ParsePrint :: TermAST ()
316 tree3ParsePrint = case parse @(FinalSyntaxes ()) @() tree3Print of
317 Left e -> error $ show e
318 Right (TermVT _ty (unE -> Forall sem)) -> print sem
319
320 tree3ParsePrint' :: TermAST ()
321 tree3ParsePrint' = case parse @(FinalSyntaxes ()) @() tree3ParsePrint of
322 Left e -> error $ show e
323 Right (TermVT _ty (unE -> Forall sem)) -> print sem
324
325 tree4ParsePrint :: TermAST ()
326 tree4ParsePrint = case parse @(FinalSyntaxes ()) @() tree4Print of
327 Left e -> error $ show e
328 Right (TermVT _ty (unE -> Forall sem)) -> print sem