From: Anders <mortberg@chalmers.se>
Date: Sun, 29 Mar 2015 18:37:22 +0000 (+0200)
Subject: Fix parsing of /\
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0eadbfe6f90e12c174a86ce0303fb9bcc523185e;p=cubicaltt.git

Fix parsing of /\
---

diff --git a/Exp.cf b/Exp.cf
index 3033a2c..398ef38 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -56,7 +56,7 @@ Side.   Side ::= [Face] "->" Exp ;
 separator Side "," ;
 
 Disj.     Formula  ::= Formula "\\/" Formula1 ;
-Conj.     Formula1 ::= Formula1 "/\\ " Formula2 ; -- Why do we need a space?
+Conj.     Formula1 ::= Formula1 CIdent Formula2 ;
 Neg.      Formula2 ::= "-" Formula2 ;
 Atom.     Formula2 ::= AIdent ;
 Dir.      Formula2 ::= Dir ;
@@ -81,5 +81,7 @@ terminator Tele "" ;
 PTele.    PTele ::= "(" Exp ":" Exp ")" ;
 terminator nonempty PTele "" ;
 
-position token AIdent ((letter|'_')(letter|digit|'\''|'_')*) ;
-separator AIdent "" ;
\ No newline at end of file
+position token AIdent (letter|'_')(letter|digit|'\''|'_')* ;
+separator AIdent "" ;
+
+token CIdent '/''\\' ;
\ No newline at end of file
diff --git a/Resolver.hs b/Resolver.hs
index 40fd0ec..d2d79aa 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -258,7 +258,7 @@ resolveFormula :: Formula -> Resolver C.Formula
 resolveFormula (Dir d)        = C.Dir <$> resolveDir d
 resolveFormula (Atom i)       = C.Atom <$> resolveName i
 resolveFormula (Neg phi)      = C.negFormula <$> resolveFormula phi
-resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi
+resolveFormula (Conj phi _ psi) = C.andFormula <$> resolveFormula phi
                                 <*> resolveFormula psi
 resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi
                                 <*> resolveFormula psi
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 1566339..da11540 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -21,7 +21,7 @@ substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
 singl (A : U) (a : A) : U = (x : A) * Id A a x
 
 contrSingl (A : U) (a b : A) (p : Id A a b) :
-  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i /\ j)
+  Id (singl A a) (a,refl A a) (b,p) = <i> (p @ i,<j> p @ i/\j)
 
 J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
   (d : C a (refl A a)) (x : A) (p : Id A a x) : C x p =