From: Anders Date: Fri, 20 Mar 2015 09:41:17 +0000 (+0100) Subject: Add support for multiple bindings of dimensions X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=56bf08e9545d7c76f84203737b5388ddea57e31d;p=cubicaltt.git Add support for multiple bindings of dimensions --- diff --git a/Exp.cf b/Exp.cf index 2bf3b0c..e45460b 100644 --- a/Exp.cf +++ b/Exp.cf @@ -23,7 +23,7 @@ NoWhere. ExpWhere ::= Exp ; Let. Exp ::= "let" "{" [Decl] "}" "in" Exp ; Lam. Exp ::= "\\" [PTele] "->" Exp ; -Path. Exp ::= "<" AIdent ">" Exp ; +Path. Exp ::= "<" [AIdent] ">" Exp ; Fun. Exp1 ::= Exp2 "->" Exp1 ; Pi. Exp1 ::= [PTele] "->" Exp1 ; Sigma. Exp1 ::= [PTele] "*" Exp1 ; @@ -74,4 +74,4 @@ PTele. PTele ::= "(" Exp ":" Exp ")" ; terminator nonempty PTele "" ; position token AIdent ((letter|'_')(letter|digit|'\''|'_')*) ; -terminator AIdent "" ; \ No newline at end of file +separator AIdent "" ; \ No newline at end of file diff --git a/Resolver.hs b/Resolver.hs index ce03e90..176a981 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -150,6 +150,13 @@ lam (a,t) e = CTT.Lam a <$> resolveExp t <*> local (insertVar a) e lams :: [(Ident,Exp)] -> Resolver Ter -> Resolver Ter lams = flip $ foldr lam +path :: AIdent -> Resolver Ter -> Resolver Ter +path i e = CTT.Path (C.Name (unAIdent i)) <$> local (insertName i) e + +paths :: [AIdent] -> Resolver Ter -> Resolver Ter +paths [] _ = throwError "Empty path lambda" +paths xs e = foldr path e xs + bind :: (Ter -> Ter) -> (Ident,Exp) -> Resolver Ter -> Resolver Ter bind f (x,t) e = f <$> lam (x,t) e @@ -173,7 +180,7 @@ resolveExp e = case e of U -> return CTT.U Var x -> resolveVar x App t s -> resolveApps x xs - where (x,xs) = unApps t [s] + where (x,xs) = unApps t [s] Sigma ptele b -> do tele <- flattenPTele ptele binds CTT.Sigma tele (resolveExp b) @@ -190,8 +197,7 @@ resolveExp e = case e of Let decls e -> do (rdecls,names) <- resolveDecls decls CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e) - Path i e -> - CTT.Path (C.Name (unAIdent i)) <$> local (insertName i) (resolveExp e) + Path is e -> paths is (resolveExp e) AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi resolveWhere :: ExpWhere -> Resolver Ter diff --git a/examples/nat.ctt b/examples/nat.ctt index 73357f6..627d842 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -114,7 +114,7 @@ Square (A : U) (a0 a1 : A) (u : Id A a0 a1) = IdP ( (IdP ( A) (u @ i) (v @ i))) r0 r1 testSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p = - comp A a + comp A a [(i = 0) -> p @ (j \/ - k), (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k),