From: Simon Huber <hubsim@gmail.com>
Date: Tue, 24 Mar 2015 10:41:59 +0000 (+0100)
Subject: pairs now associate to the right
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4aab64254d87eac44a8b53b859700c531611e43c;p=cubicaltt.git

pairs now associate to the right
---

diff --git a/Exp.cf b/Exp.cf
index 074fc15..9204e56 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -39,8 +39,9 @@ Comp.       Exp3 ::= "comp" ;
 Glue.       Exp3 ::= "glue" ;
 GlueElem.   Exp3 ::= "glueElem" ;
 System.     Exp3 ::= "[" [Side] "]" ;
-Pair.       Exp3 ::= "(" Exp "," Exp ")" ;
+Pair.       Exp3 ::= "(" Exp "," [Exp] ")" ;
 coercions Exp 3 ;
+separator nonempty Exp "," ;
 
 Dir0.       Dir ::= "0" ;
 Dir1.       Dir ::= "1" ;
diff --git a/Resolver.hs b/Resolver.hs
index a656f1d..091eedd 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -204,7 +204,10 @@ resolveExp e = case e of
     lams tele (resolveExp t)
   Fst t         -> CTT.Fst <$> resolveExp t
   Snd t         -> CTT.Snd <$> resolveExp t
-  Pair t0 t1    -> CTT.Pair <$> resolveExp t0 <*> resolveExp t1
+  Pair t0 ts    -> do
+    e  <- resolveExp t0
+    es <- mapM resolveExp ts
+    return $ foldr1 CTT.Pair (e:es)
   Let decls e   -> do
     (rdecls,names) <- resolveDecls decls
     CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
diff --git a/examples/bool.ctt b/examples/bool.ctt
index 8e24510..c796767 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -13,7 +13,7 @@ negK : (b : bool) -> Id bool (neg (neg b)) b = split
   false -> refl bool false
 
 negEq : Id U bool bool =
-  <i> glue bool [ (i = 0) -> (bool,(neg,(neg,(negK,negK)))) ]
+  <i> glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]
 
 test : bool = transport negEq true
 
@@ -37,7 +37,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
 
 boolEqF2 : Id U bool F2 =
  -- <i> glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))]
-  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
+ isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
   
 negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
 
diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index cb0f4b6..3a76ac9 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -36,4 +36,4 @@ inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
-      <i> glue B [ (i = 0) -> (A,(f,(g,(s,t)))) ]
+      <i> glue B [ (i = 0) -> (A,f,g,s,t) ]