From b7e6342a8b4f9853176753fcdcd39ddd913ffe1a Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Wed, 18 Mar 2015 23:48:11 +0100 Subject: [PATCH] added app of a formula --- Exp.cf | 10 +++++++++- Resolver.hs | 11 ++++++++++- examples/nat.ctt | 10 +++++++++- 3 files changed, 28 insertions(+), 3 deletions(-) diff --git a/Exp.cf b/Exp.cf index 5fee375..5a4a1e7 100644 --- 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 968dfc3..8dc8719 100644 --- 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 58dad5d..8f831fc 100644 --- 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) = (p @ ?0, p @ ?0 & ?1) \ No newline at end of file -- 2.34.1