added app of a formula

diff --git a/Exp.cf b/Exp.cf
index 5fee375ce5f8d92b1e2c8710fdb67b77951d6244..5a4a1e73411cd0ea2deddc958cf25b7f9e62b732 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -29,7 +29,7 @@ Pi.         Exp1 ::= [PTele] "->" Exp1 ;
 Sigma.      Exp1 ::= [PTele] "*" Exp1 ;
 App.        Exp2 ::= Exp2 Exp3 ;
 Var.        Exp3 ::= AIdent ;
-AppFormula. Exp3 ::= Exp3 "@" Name ;
+AppFormula. Exp3 ::= Exp3 "@" Formula ;
 U.          Exp3 ::= "U" ;
 Fst.        Exp3 ::= Exp3 ".1" ;
 Snd.        Exp3 ::= Exp3 ".2" ;
@@ -38,6 +38,14 @@ Trans.      Exp3 ::= "transport" ;
 Pair.       Exp3 ::= "(" Exp "," Exp ")" ;
 coercions Exp 3 ;
 
+
+Conj.     Formula  ::= Formula "|" Formula1 ;
+Disj.     Formula1 ::= Formula1 "&" Formula2 ;
+Neg.      Formula2 ::= "-" Formula2 ;
+Atom.     Formula2 ::= Name ;
+coercions Formula 2 ;
+
+
 -- Branches
 Branch.   Branch ::= AIdent [AIdent] "->" ExpWhere ;
 separator Branch ";" ;

diff --git a/Resolver.hs b/Resolver.hs
index 968dfc3dd2b405b8abbe04c9149265b40698d689..8dc871933120769dd453dcb0328452343e7cfd7c 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -166,11 +166,20 @@ resolveExp e = case e of
     (rdecls,names) <- resolveDecls decls
     CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e)
   Path i e -> CTT.Path <$> resolveName i <*> resolveExp e 
-  AppFormula e n -> CTT.AppFormula <$> resolveExp e <*> (C.Atom <$> resolveName n)
+  AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
     
 resolveWhere :: ExpWhere -> Resolver Ter
 resolveWhere = resolveExp . unWhere
 
+resolveFormula :: Formula -> Resolver C.Formula
+resolveFormula (Atom i)       = C.Atom <$> resolveName i
+resolveFormula (Neg phi)      = C.negFormula <$> resolveFormula phi
+resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi
+                                <*> resolveFormula psi
+resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi
+                                <*> resolveFormula psi
+
+
 resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Binder],Ter))
 resolveBranch (Branch (AIdent (_,lbl)) args e) = do
     binders <- mapM resolveAIdent args

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 58dad5dc07e1c485b93eb78988e60dfa5b0217b7..8f831fcc322c63e93c627ffa6cea20cc43b70b9a 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -53,4 +53,12 @@ test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id
   where
   rem : (n : nat) -> Id nat (idnat n) n = split
     zero -> refl nat zero
-    suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
\ No newline at end of file
+    suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
+
+-- subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
+--   transport (mapOnPath A U P a b p) e
+
+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) = <?0> (p @ ?0,<?1> p @ ?0 & ?1)
\ No newline at end of file