-
Notifications
You must be signed in to change notification settings - Fork 0
/
Parser.hs
50 lines (43 loc) · 1.44 KB
/
Parser.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
{-# LANGUAGE DoRec #-}
module Parser where
import Control.Applicative hiding (Const)
import Data.Parser.Grempa.Grammar
import Data.Parser.Grempa.Dynamic
import CoreTypes
import qualified Lexar as L
parseString :: String -> Formula
parseString = parse parseFunDynamic . L.lexToks
parseFunDynamic :: Parser L.Tok Formula
parseFunDynamic = mkDynamicParser constrWrapper formula
formula :: Grammar L.Tok Formula
formula = do
rec
f <- rule
[ Imp <@> f' <# L.Imp <#> f
, id <@> f']
f' <- rule
[ paren f
, ForAll <$> (UVar . L.fromTok) <@ L.Forall <#> L.var <#> f'
, Exists <$> (UVar . L.fromTok) <@ L.Exists <#> L.var <#> f'
, Equiv <@> f' <# L.Equiv <#> f'
, And <@> f' <# L.And <#> f'
, Or <@> f' <# L.Or <#> f'
, Neg <@ L.Not <#> f'
, id <@> p]
p <- rule
[ Rel <$> L.fromTok <@> L.Pred "" <# L.LPar <#> terms <# L.RPar
, (\x -> Rel (L.fromTok $ x) []) <@> L.Pred "" ]
term <- rule [ (Var . UVar . L.fromTok) <@> L.Var ""
, Const . L.fromTok <@> L.Const ""
, App <$> L.fromTok <@> L.Var "" <# L.LPar <#> terms <# L.RPar]
terms <- severalInter0 L.SemiColon term
return f
where
paren x = id <@ L.LPar <#> x <# L.RPar
{-
F = P | Q Var . F | F -> F | F /\ F | F \/ F | ~ F | Top | Bot
Q = forall | exists
P = Predicate ( Terms ) | Term `P` Term
Terms = Var | Fun ( Terms ) | Const
Var = Char
-}