Add support for multiple bindings of dimensions

diff --git a/Exp.cf b/Exp.cf
index 2bf3b0c83537f92569f86faebca9908629cca4e2..e45460b02e2f580129f266452a6dcf1236ef1ed0 100644 (file)
--- 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 ce03e9089eca690ab6747fbe298710edc909b7df..176a98158e292a473d416216fd53f8721fbd4c0d 100644 (file)
--- 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 73357f64e4b656c2d60412dec4873b0d28ec3ef8..627d8425a694286bcb4afad9066e4cc863eefd01 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -114,7 +114,7 @@ Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
   = IdP (<i> (IdP (<j> 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 =
-  <i> <j> comp A a
+  <i j> comp A a
      [(i = 0) -> <k> p @ (j \/ - k),
       (i = 1) -> <k> p @ (j /\ k),
       (j = 0) -> <k> p @ (i \/ - k),