Add 0 and 1 to parser and resolver

diff --git a/Exp.cf b/Exp.cf
index cb623997a8d1dc3a94e48a6b92823ffc4b9b7c28..92a2da4d2b62c9e26d01ee1258686caf3bcbf439 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -42,6 +42,8 @@ Disj.     Formula  ::= Formula "|" Formula1 ;
 Conj.     Formula1 ::= Formula1 "&" Formula2 ;
 Neg.      Formula2 ::= "-" Formula2 ;
 Atom.     Formula2 ::= AIdent ;
+Dir0.     Formula2 ::= "0" ;
+Dir1.     Formula2 ::= "1" ;
 coercions Formula 2 ;
 
 -- Branches

diff --git a/Resolver.hs b/Resolver.hs
index 81e94edd30bfb07941fd4417918fd2e44148afce..f24dd7f5cac68d2b8e212d559e450c573087758b 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -180,6 +180,8 @@ resolveWhere :: ExpWhere -> Resolver Ter
 resolveWhere = resolveExp . unWhere
 
 resolveFormula :: Formula -> Resolver C.Formula
+resolveFormula Dir0           = return $ C.Dir 0
+resolveFormula Dir1           = return $ C.Dir 1
 resolveFormula (Atom i)       = C.Atom <$> resolveName i
 resolveFormula (Neg phi)      = C.negFormula <$> resolveFormula phi
 resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi