From: Anders Mörtberg <mortberg@chalmers.se>
Date: Thu, 19 Mar 2015 07:58:38 +0000 (+0100)
Subject: Add 0 and 1 to parser and resolver
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=6cdd503bcefad949ec54cb9c1505991667d96742;p=cubicaltt.git

Add 0 and 1 to parser and resolver
---

diff --git a/Exp.cf b/Exp.cf
index cb62399..92a2da4 100644
--- 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 81e94ed..f24dd7f 100644
--- 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