]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Compiling/Term/Grammar.hs
Add compileWithTyCtx.
[haskell/symantic.git] / symantic / Language / Symantic / Compiling / Term / Grammar.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DeriveFunctor #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
5 {-# LANGUAGE PolyKinds #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 {-# OPTIONS_GHC -fno-warn-orphans #-}
8 module Language.Symantic.Compiling.Term.Grammar where
9
10 import Control.Arrow (left)
11 import Control.Monad (foldM, void, (=<<))
12 import qualified Data.Char as Char
13 import qualified Data.Function as Fun
14 import Data.Map.Strict (Map)
15 import qualified Data.Map.Strict as Map
16 import Data.Proxy (Proxy(..))
17 import Data.Semigroup (Semigroup(..))
18 import Data.String (IsString(..))
19 import Data.Text (Text)
20 import qualified Data.Text as Text
21 import Prelude hiding (mod, not, any)
22
23 import Language.Symantic.Parsing
24 import Language.Symantic.Typing
25
26 -- * Type 'TeName'
27 newtype TeName = TeName Text
28 deriving (Eq, Ord, Show)
29 instance IsString TeName where
30 fromString = TeName . fromString
31
32 -- * Type 'ProTok'
33 -- | Proto 'EToken'. It's almost like a free monad,
34 -- but has a third constructor ('ProTokPi')
35 -- to require a type argument.
36 --
37 -- NOTE: this type may one day be removed
38 -- if proper type inferencing is done.
39 -- In the meantime it is used to require
40 -- term or type arguments needed to build
41 -- the 'EToken's of polymorphic terms.
42 data ProTok meta ts
43 = ProTokLam (EToken meta ts -> ProTok meta ts)
44 -- ^ Require a term argument.
45 | ProTokPi (EToken meta '[Proxy Token_Type] -> ProTok meta ts)
46 -- ^ Require a type argument.
47 | ProTok (EToken meta ts)
48 -- ^ No need for any argument.
49
50 -- | Declared here and not in @Compiling.Lambda@
51 -- to be able to use 'Token_Term_Var' in 'protok'.
52 data instance TokenT meta (ts::[*]) (Proxy (->))
53 = Token_Term_Abst TeName (EToken meta '[Proxy Token_Type]) (EToken meta ts)
54 | Token_Term_App (EToken meta ts) (EToken meta ts)
55 | Token_Term_Let TeName (EToken meta ts) (EToken meta ts)
56 | Token_Term_Var TeName
57 | Token_Term_Compose (EToken meta ts) (EToken meta ts)
58
59 -- * Class 'Tokenize'
60 type Tokenize meta ts
61 = TokenizeR meta ts ts
62
63 -- ** Type 'Tokenizers'
64 data Tokenizers meta ts
65 = Tokenizers
66 { tokenizers_prefix :: Map Mod_Path (Map TeName (ProTok_Term Unifix meta ts))
67 , tokenizers_infix :: Map Mod_Path (Map TeName (ProTok_Term Infix meta ts))
68 , tokenizers_postfix :: Map Mod_Path (Map TeName (ProTok_Term Unifix meta ts))
69 }
70 instance Semigroup (Tokenizers meta ts) where
71 x <> y =
72 Tokenizers
73 (Map.unionWith Map.union
74 (tokenizers_prefix x)
75 (tokenizers_prefix y))
76 (Map.unionWith Map.union
77 (tokenizers_infix x)
78 (tokenizers_infix y))
79 (Map.unionWith Map.union
80 (tokenizers_postfix x)
81 (tokenizers_postfix y))
82 instance Monoid (Tokenizers meta ts) where
83 mempty = Tokenizers Map.empty Map.empty Map.empty
84 mappend = (<>)
85
86 -- ** Type 'ProTok_Term'
87 data ProTok_Term fixy meta ts
88 = ProTok_Term
89 { protok_term :: meta -> ProTok meta ts
90 , protok_fixity :: fixy
91 }
92
93 tokenizers :: forall meta ts. Tokenize meta ts => Tokenizers meta ts
94 tokenizers = tokenizeR (Proxy @ts)
95
96 unProTok
97 :: ProTok meta ts
98 -> Either Error_Term_Gram (EToken meta ts)
99 unProTok (ProTok t) = Right t
100 unProTok _ = Left Error_Term_Gram_Term_incomplete
101
102 protok
103 :: Inj_Token meta ts (->)
104 => Mod TeName
105 -> Tokenizers meta ts
106 -> Either Error_Term_Gram
107 ( Maybe (ProTok_Term Unifix meta ts)
108 , ProTok_Term Infix meta ts
109 , Maybe (ProTok_Term Unifix meta ts)
110 )
111 protok (mod `Mod` tn) (Tokenizers pres ins posts) = do
112 let pre = Map.lookup mod pres >>= Map.lookup tn
113 let post = Map.lookup mod posts >>= Map.lookup tn
114 in_ <- var_or_err $ Map.lookup mod ins >>= Map.lookup tn
115 return (pre, in_, post)
116 where
117 var_or_err (Just x) = Right x
118 var_or_err Nothing =
119 case mod of
120 [] -> Right $ var infixN5
121 _ -> Left $ Error_Term_Gram_Undefined_term
122 var protok_fixity =
123 ProTok_Term
124 { protok_term = \meta -> ProTok $ inj_EToken meta $ Token_Term_Var tn
125 , protok_fixity
126 }
127
128 protok_app
129 :: Inj_Token meta ts (->)
130 => ProTok meta ts
131 -> [Either (EToken meta '[Proxy Token_Type]) (EToken meta ts)]
132 -> Either Error_Term_Gram (ProTok meta ts)
133 protok_app =
134 foldM app
135 where
136 app acc (Left typ) =
137 case acc of
138 ProTokPi g -> Right $ g typ
139 _ -> Left Error_Term_Gram_Cannot_apply_type
140 app acc (Right te) =
141 case acc of
142 ProTokLam f -> Right $ f te
143 ProTok tok@(EToken e) -> Right $
144 ProTok $ inj_EToken (meta_of e) $
145 Token_Term_App tok te
146 _ -> Left Error_Term_Gram_Cannot_apply_term
147
148 -- ** Class 'TokenizeR'
149 class TokenizeR meta (ts::[*]) (rs::[*]) where
150 tokenizeR :: Proxy rs -> Tokenizers meta ts
151 instance TokenizeR meta ts '[] where
152 tokenizeR _rs = mempty
153 instance
154 ( TokenizeT meta ts t
155 , TokenizeR meta ts rs
156 ) => TokenizeR meta ts (t ': rs) where
157 tokenizeR _ =
158 tokenizeR (Proxy @rs) <>
159 tokenizeT (Proxy @t)
160
161 -- ** Class 'TokenizeT'
162 class TokenizeT meta ts t where
163 tokenizeT :: Proxy t -> Tokenizers meta ts
164 -- tokenizeT _t = [] `Mod` []
165 tokenizeT _t = mempty
166
167 tokenizeTMod
168 :: Mod_Path
169 -> [(TeName, ProTok_Term fix meta ts)]
170 -> Map Mod_Path (Map TeName (ProTok_Term fix meta ts))
171 tokenizeTMod mod tbl = Map.singleton mod $ Map.fromList tbl
172
173 tokenize0
174 :: Inj_Token meta ts t
175 => Text -> fixity -> TokenT meta ts (Proxy t)
176 -> (TeName, ProTok_Term fixity meta ts)
177 tokenize0 n protok_fixity tok =
178 (TeName n,) ProTok_Term
179 { protok_term = \meta -> ProTok $ inj_EToken meta $ tok
180 , protok_fixity }
181
182 tokenize1
183 :: Inj_Token meta ts t
184 => Text -> fixity
185 -> (EToken meta ts -> TokenT meta ts (Proxy t))
186 -> (TeName, ProTok_Term fixity meta ts)
187 tokenize1 n protok_fixity tok =
188 (TeName n,) ProTok_Term
189 { protok_term = \meta ->
190 ProTokLam $ \a ->
191 ProTok $ inj_EToken meta $ tok a
192 , protok_fixity }
193
194 tokenize2
195 :: Inj_Token meta ts t
196 => Text -> fixity
197 -> (EToken meta ts -> EToken meta ts -> TokenT meta ts (Proxy t))
198 -> (TeName, ProTok_Term fixity meta ts)
199 tokenize2 n protok_fixity tok =
200 (TeName n,) ProTok_Term
201 { protok_term = \meta ->
202 ProTokLam $ \a -> ProTokLam $ \b ->
203 ProTok $ inj_EToken meta $ tok a b
204 , protok_fixity
205 }
206
207 tokenize3
208 :: Inj_Token meta ts t
209 => Text -> fixity
210 -> (EToken meta ts -> EToken meta ts -> EToken meta ts -> TokenT meta ts (Proxy t))
211 -> (TeName, ProTok_Term fixity meta ts)
212 tokenize3 n protok_fixity tok =
213 (TeName n,) ProTok_Term
214 { protok_term = \meta ->
215 ProTokLam $ \a -> ProTokLam $ \b -> ProTokLam $ \c ->
216 ProTok $ inj_EToken meta $ tok a b c
217 , protok_fixity
218 }
219
220 -- * Type 'Mod'
221 type Mod_Path = [Mod_Name]
222 newtype Mod_Name = Mod_Name Text
223 deriving (Eq, Ord, Show)
224 data Mod a = Mod Mod_Path a
225 deriving (Eq, Functor, Ord, Show)
226
227 -- * Class 'Gram_Name'
228 class
229 ( Alt g
230 , Alter g
231 , Alter g
232 , App g
233 , Try g
234 , Gram_CF g
235 , Gram_Op g
236 , Gram_Lexer g
237 , Gram_RegL g
238 , Gram_Rule g
239 , Gram_Terminal g
240 ) => Gram_Name g where
241 g_mod_path :: CF g Mod_Path
242 g_mod_path = rule "mod_path" $
243 infixrG
244 (pure <$> g_mod_name)
245 (op <$ char '.')
246 where op = (<>)
247 g_mod_name :: CF g Mod_Name
248 g_mod_name = rule "mod_name" $
249 (Mod_Name . Text.pack <$>) $
250 identG `minus`
251 (Fun.const
252 <$> g_term_keywords
253 <*. (any `but` g_term_idname_tail))
254 where
255 identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
256 headG = unicat $ Unicat Char.UppercaseLetter
257
258 g_term_mod_name :: CF g (Mod TeName)
259 g_term_mod_name = rule "term_mod_name" $
260 lexeme $
261 g_term_mod_idname <+>
262 parens g_term_mod_opname
263 g_term_name :: CF g TeName
264 g_term_name = rule "term_name" $
265 lexeme $
266 g_term_idname <+>
267 parens g_term_opname
268
269 g_term_mod_idname :: CF g (Mod TeName)
270 g_term_mod_idname = rule "term_mod_idname" $
271 Mod
272 <$> option [] (try $ g_mod_path <* char '.')
273 <*> g_term_idname
274 g_term_idname :: CF g TeName
275 g_term_idname = rule "term_idname" $
276 (TeName . Text.pack <$>) $
277 (identG `minus`) $
278 Fun.const
279 <$> g_term_keywords
280 <*. (any `but` g_term_idname_tail)
281 where
282 identG = (:) <$> headG <*> many (cf_of_Terminal g_term_idname_tail)
283 headG = unicat $ Unicat_Letter
284 g_term_idname_tail :: Terminal g Char
285 g_term_idname_tail = rule "term_idname_tail" $
286 unicat Unicat_Letter <+>
287 unicat Unicat_Number
288 g_term_keywords :: Reg rl g String
289 g_term_keywords = rule "term_keywords" $
290 choice $ string <$> ["in", "let"]
291
292 g_term_mod_opname :: CF g (Mod TeName)
293 g_term_mod_opname = rule "term_mod_opname" $
294 Mod
295 <$> option [] (try $ g_mod_path <* char '.')
296 <*> g_term_opname
297 g_term_opname :: CF g TeName
298 g_term_opname = rule "term_opname" $
299 (TeName . Text.pack <$>) $
300 (symG `minus`) $
301 Fun.const
302 <$> g_term_keysyms
303 <*. (any `but` g_term_opname_ok)
304 where
305 symG = some $ cf_of_Terminal g_term_opname_ok
306 g_term_opname_ok :: Terminal g Char
307 g_term_opname_ok = rule "term_opname_ok" $
308 choice (unicat <$>
309 [ Unicat_Symbol
310 , Unicat_Punctuation
311 , Unicat_Mark
312 ]) `but` koG
313 where
314 koG = choice (char <$> ['(', ')', '`', '\'', ',', '[', ']'])
315 g_term_keysyms :: Reg rl g String
316 g_term_keysyms = rule "term_keysyms" $
317 choice $ string <$> ["\\", "->", "="]
318
319 deriving instance Gram_Name g => Gram_Name (CF g)
320 instance Gram_Name EBNF
321 instance Gram_Name RuleDef
322
323 -- * Class 'Gram_Term_Type'
324 class
325 ( Alt g
326 , Alter g
327 , App g
328 , Gram_CF g
329 , Gram_Lexer g
330 , Gram_Meta meta g
331 , Gram_Rule g
332 , Gram_Terminal g
333 , Gram_Name g
334 , Gram_Type meta g
335 ) => Gram_Term_Type meta g where
336 g_term_abst_decl
337 :: CF g (TeName, TokType meta)
338 g_term_abst_decl = rule "term_abst_decl" $
339 parens $ (,)
340 <$> g_term_name
341 <* symbol ":"
342 <*> g_type
343
344 deriving instance Gram_Term_Type meta g => Gram_Term_Type meta (CF g)
345 instance Gram_Term_Type meta EBNF
346 instance Gram_Term_Type meta RuleDef
347
348 -- * Class 'Gram_Error'
349 class Gram_Error g where
350 term_unError :: CF g (Either Error_Term_Gram a) -> CF g a
351 deriving instance Gram_Error g => Gram_Error (CF g)
352 instance Gram_Error EBNF where
353 term_unError (CF (EBNF g)) = CF $ EBNF g
354 instance Gram_Error RuleDef where
355 term_unError (CF (RuleDef (EBNF g))) =
356 CF $ RuleDef $ EBNF g
357
358 -- ** Type 'Error_Term_Gram'
359 data Error_Term_Gram
360 = Error_Term_Gram_Fixity Error_Fixity
361 | Error_Term_Gram_Cannot_apply_term
362 | Error_Term_Gram_Cannot_apply_type
363 | Error_Term_Gram_Undefined_term
364 | Error_Term_Gram_Term_incomplete
365 deriving (Eq, Show)
366
367 -- * Class 'Gram_Term'
368 class
369 ( Alt g
370 , Alter g
371 , App g
372 , Gram_CF g
373 , Gram_Lexer g
374 , Gram_Meta meta g
375 , Gram_Rule g
376 , Gram_Terminal g
377 , Gram_Error g
378 , Gram_Term_AtomsR meta ts ts g
379 , Gram_Name g
380 , Gram_Term_Type meta g
381 , Gram_Type meta g
382 ) => Gram_Term ts meta g where
383 -- | Wrap 'g_term_abst'. Useful to modify body's scope.
384 g_term_abst_args_body
385 :: CF g [(TeName, TokType meta)]
386 -> CF g (EToken meta ts)
387 -> CF g ([(TeName, TokType meta)], EToken meta ts)
388 g_term_abst_args_body args body = (,) <$> args <*> body
389 term_tokenizers :: CF g (Tokenizers meta ts -> a) -> CF g a
390
391 g_term
392 :: Inj_Tokens meta ts '[Proxy (->)]
393 => CF g (EToken meta ts)
394 g_term = rule "term" $
395 choice
396 [ try g_term_abst
397 , g_term_operators
398 , g_term_let
399 ]
400 g_term_operators
401 :: Inj_Tokens meta ts '[Proxy (->)]
402 => CF g (EToken meta ts)
403 g_term_operators = rule "term_operators" $
404 term_unError $
405 term_unError $
406 left Error_Term_Gram_Fixity <$>
407 operators
408 (Right <$> g_term_app)
409 (term_unError $ metaG $ term_tokenizers $ op_prefix <$> g_term_op_prefix)
410 (term_unError $ metaG $ term_tokenizers $ op_infix <$> g_term_op_infix)
411 (term_unError $ metaG $ term_tokenizers $ op_postfix <$> g_term_op_postfix)
412 where
413 g_backquote :: Gram_Terminal g' => g' Char
414 g_backquote = char '`'
415 op_infix name toks meta = do
416 (_pre, in_, _post) <- protok name toks
417 return $
418 (protok_fixity in_,) $ \ma mb -> do
419 a <- ma
420 b <- mb
421 unProTok =<< protok_term in_ meta `protok_app` [Right a, Right b]
422 op_prefix name toks meta = do
423 (pre, _in_, _post) <- protok name toks
424 case pre of
425 Just p ->
426 Right $ (protok_fixity p,) $ (=<<) $ \a ->
427 unProTok =<< protok_term p meta `protok_app` [Right a]
428 Nothing -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedPrefix
429 op_postfix name toks meta = do
430 (_pre, _in_, post) <- protok name toks
431 case post of
432 Just p ->
433 Right $ (protok_fixity p,) $ (=<<) $ \a ->
434 unProTok =<< protok_term p meta `protok_app` [Right a]
435 Nothing -> Left $ Error_Term_Gram_Fixity Error_Fixity_NeedPostfix
436 g_term_op_postfix :: CF g (Mod TeName)
437 g_term_op_postfix = rule "term_op_postfix" $
438 lexeme $
439 g_backquote *> g_term_mod_idname <+> -- <* (cf_of_Terminal $ Gram.Term (pure ' ') `but` g_backquote)
440 g_term_mod_opname
441 g_term_op_infix :: CF g (Mod TeName)
442 g_term_op_infix = rule "term_op_infix" $
443 lexeme $
444 between g_backquote g_backquote g_term_mod_idname <+>
445 g_term_mod_opname
446 g_term_op_prefix :: CF g (Mod TeName)
447 g_term_op_prefix = rule "term_op_prefix" $
448 lexeme $
449 g_term_mod_idname <* g_backquote <+>
450 g_term_mod_opname
451 g_term_app
452 :: Inj_Tokens meta ts '[Proxy (->)]
453 => CF g (EToken meta ts)
454 g_term_app = rule "term_app" $
455 term_unError $
456 (\a as -> unProTok =<< protok_app a as)
457 <$> g_term_atom_proto
458 <*> many (try g_term_atom)
459 g_term_atom
460 :: Inj_Tokens meta ts '[Proxy (->)]
461 => CF g (Either (EToken meta '[Proxy Token_Type])
462 (EToken meta ts))
463 g_term_atom = rule "term_atom" $
464 (Left <$ char '@' <*> g_type) <+>
465 (Right <$> term_unError (unProTok <$> g_term_atom_proto))
466 g_term_atom_proto
467 :: Inj_Tokens meta ts '[Proxy (->)]
468 => CF g (ProTok meta ts)
469 g_term_atom_proto =
470 choice $
471 try <$> gs_term_atomsR (Proxy @ts) <>
472 [ try $
473 metaG $ ((\(_, in_, _) -> protok_term in_) <$>) $
474 term_unError $
475 term_tokenizers $
476 protok <$> g_term_mod_name
477 , ProTok <$> g_term_group
478 ]
479 g_term_group
480 :: Inj_Tokens meta ts '[Proxy (->)]
481 => CF g (EToken meta ts)
482 g_term_group = rule "term_group" $ parens g_term
483 g_term_abst
484 :: Inj_Tokens meta ts '[Proxy (->)]
485 => CF g (EToken meta ts)
486 g_term_abst = rule "term_abst" $
487 metaG $
488 ((\(xs, te) meta ->
489 foldr (\(x, ty_x) ->
490 inj_EToken meta .
491 Token_Term_Abst x ty_x) te xs) <$>) $
492 g_term_abst_args_body
493 (symbol "\\" *> some g_term_abst_decl <* symbol "->")
494 g_term
495 g_term_let
496 :: Inj_Tokens meta ts '[Proxy (->)]
497 => CF g (EToken meta ts)
498 g_term_let = rule "term_let" $
499 metaG $
500 (\name args bound body meta ->
501 inj_EToken meta $
502 Token_Term_Let name
503 (foldr (\(x, ty_x) ->
504 inj_EToken meta . Token_Term_Abst x ty_x) bound args) body)
505 <$ symbol "let"
506 <*> g_term_name
507 <*> many g_term_abst_decl
508 <* symbol "="
509 <*> g_term
510 <* symbol "in"
511 <*> g_term
512
513 deriving instance
514 ( Gram_Term ts meta g
515 , Gram_Term_AtomsR meta ts ts (CF g)
516 ) => Gram_Term ts meta (CF g)
517 instance
518 Gram_Term_AtomsR meta ts ts EBNF =>
519 Gram_Term ts meta EBNF where
520 term_tokenizers (CF (EBNF g)) = CF $ EBNF g
521 instance
522 Gram_Term_AtomsR meta ts ts RuleDef =>
523 Gram_Term ts meta RuleDef where
524 term_tokenizers (CF (RuleDef (EBNF g))) =
525 CF $ RuleDef $ EBNF g
526
527 -- ** Class 'Gram_Term_AtomsR'
528 class Gram_Term_AtomsR meta (ts::[*]) (rs::[*]) g where
529 gs_term_atomsR :: Proxy rs -> [CF g (ProTok meta ts)]
530 instance Gram_Term_AtomsR meta ts '[] g where
531 gs_term_atomsR _rs = []
532 instance
533 ( Gram_Term_AtomsT meta ts t g
534 , Gram_Term_AtomsR meta ts rs g
535 ) => Gram_Term_AtomsR meta ts (t ': rs) g where
536 gs_term_atomsR _ =
537 gs_term_atomsT (Proxy @t) <>
538 gs_term_atomsR (Proxy @rs)
539
540 -- ** Class 'Gram_Term_AtomsT'
541 class Gram_Term_AtomsT meta ts t g where
542 gs_term_atomsT :: Proxy t -> [CF g (ProTok meta ts)]
543 gs_term_atomsT _t = []
544 instance Gram_Term_AtomsT meta ts t RuleDef
545
546 gram_term
547 :: forall g.
548 ( Gram_Term '[Proxy (->), Proxy Integer] () g
549 ) => [CF g ()]
550 gram_term =
551 [ ue g_term
552 , ue g_term_operators
553 , ue g_term_app
554 , ug g_term_atom
555 , ue g_term_group
556 , ue g_term_abst
557 , void (g_term_abst_decl::CF g (TeName, TokType ()))
558 , ue g_term_let
559 , void g_term_mod_name
560 , void g_term_name
561 , void g_term_idname
562 , void $ cf_of_Terminal g_term_idname_tail
563 , void $ cf_of_Reg g_term_keywords
564 , void g_term_mod_opname
565 , void g_term_opname
566 , void $ cf_of_Terminal g_term_opname_ok
567 , void $ cf_of_Reg g_term_keysyms
568 ] where
569 ue :: CF g (EToken () '[Proxy (->), Proxy Integer]) -> CF g ()
570 ue = (() <$)
571 -- uf :: CF g (ProTok () '[Proxy (->)]) -> CF g ()
572 -- uf = (() <$)
573 ug :: CF g (Either (EToken () '[Proxy Token_Type])
574 (EToken () '[Proxy (->), Proxy Integer])) -> CF g ()
575 ug = (() <$)