From: Anders Mörtberg <mortberg@chalmers.se>
Date: Mon, 20 Apr 2015 08:34:29 +0000 (+0200)
Subject: Fix the way @ binds (it is now like normal application)
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=1a15bbf1d7c8c891ecd63d19c4209b4039ef4f7a;p=cubicaltt.git

Fix the way @ binds (it is now like normal application)
---

diff --git a/Exp.cf b/Exp.cf
index 9aff9a0..0daa71e 100644
--- a/Exp.cf
+++ b/Exp.cf
@@ -28,6 +28,7 @@ Path.       Exp  ::= "<" [AIdent] ">" Exp ;
 Fun.        Exp1 ::= Exp2 "->" Exp1 ;
 Pi.         Exp1 ::= [PTele] "->" Exp1 ;
 Sigma.      Exp1 ::= [PTele] "*" Exp1 ;
+AppFormula. Exp2 ::= Exp2 "@" Formula ;
 App.        Exp2 ::= Exp2 Exp3 ;
 IdP.        Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Trans.      Exp3 ::= "transport" Exp4 Exp4 ;
@@ -38,7 +39,6 @@ CompElem.   Exp3 ::= "compElem" Exp4 System Exp4 System ;
 ElimComp.   Exp3 ::= "elimComp" Exp4 System Exp4 ;
 Fst.        Exp4 ::= Exp4 ".1" ;
 Snd.        Exp4 ::= Exp4 ".2" ;
-AppFormula. Exp5 ::= Exp5 "@" Formula ;
 Pair.       Exp5 ::= "(" Exp "," [Exp] ")" ;
 Var.        Exp5 ::= AIdent ;
 PCon.       Exp5 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi
diff --git a/examples/circle.ctt b/examples/circle.ctt
index 44da52b..3bd1961 100644
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -33,11 +33,11 @@ loop2'' : loopS1 = compId'' S1 base base loop1 base loop1
 
 mLoop : (x : S1) -> Id S1 x x = split
   base -> loop1
-  loop @ i -> (constSquare S1 base loop1) @ i
+  loop @ i -> constSquare S1 base loop1 @ i
 
 mult (x : S1) : S1 -> S1 = split
   base -> x
-  loop @ i -> (mLoop x) @ i
+  loop @ i -> mLoop x @ i
 
 square (x : S1) : S1 = mult x x
 
diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt
index 4b6b085..4a501a5 100644
--- a/examples/higherhit.ctt
+++ b/examples/higherhit.ctt
@@ -12,7 +12,7 @@ data S1 = base
 
 foo : S1 = base
 
-loop' : Id S1 base base = <i> (loop {S1}) @ i
+loop' : Id S1 base base = <i> loop {S1} @ i
 
 
 -- new
@@ -42,11 +42,9 @@ data setTrunc (A : U)
        , (j=0) -> a
        , (j=1) -> b]
 
--- TODO: fix parsing: no parentheses should be necessary
-
 setTruncSet (A : U) : set (setTrunc A) =
    \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
-     <i j> (setTr {setTrunc A} a b p q) @ i @ j
+     <i j> setTr {setTrunc A} a b p q @ i @ j
 
 
 setTruncRec (A : U)
diff --git a/examples/interval.ctt b/examples/interval.ctt
index ca455da..813a881 100644
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -10,4 +10,4 @@ fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
   where htpy (x : A) : I -> B = split
           zero    -> f x
           one     -> g x
-          seg @ i -> (p x) @ i
+          seg @ i -> p x @ i
diff --git a/examples/susp.ctt b/examples/susp.ctt
index 1224b14..5d219ce 100644
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -22,19 +22,19 @@ path : bool -> Id S1 base base = split
 s1ToCircle : sone -> S1 = split
   north   -> base
   south   -> base
-  merid b @ i -> (path b) @ i
+  merid b @ i -> path b @ i
 
-m0 : Id sone north south = <i> (merid{sone} false) @ i
+m0 : Id sone north south = <i> merid{sone} false @ i
 
-m1 : Id sone north south = <i> (merid{sone} true) @ i
+m1 : Id sone north south = <i> merid{sone} true @ i
 
 invm1 : Id sone south north = inv sone north south m1
 
 circleToS1 : S1 -> sone = split
   base -> north
-  loop @ i -> (compId sone north south north m0 invm1) @ i
+  loop @ i -> compId sone north south north m0 invm1 @ i
 
-merid1 (b:bool) : Id sone north south = <i>(merid{sone} b)@ i
+merid1 (b:bool) : Id sone north south = <i> merid{sone} b @ i
 
 oc (x:S1) : S1 = s1ToCircle (circleToS1 x)
 
@@ -52,7 +52,7 @@ lemSquare (A:U) (a b : A) (m0 m1 : Id A a b) :
 coid : (x : sone) -> Id sone (co x) x = split
  north -> refl sone north
  south -> m1
- merid b @ i  -> (ind b) @ i
+ merid b @ i  -> ind b @ i
   where
     F (x:sone) : U = Id sone (co x) x
 
@@ -69,7 +69,7 @@ s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle
 ptU : U = (X : U) * X
 
 lemPt (A :U) (B:U) (p:Id U A B) (a:A) : Id ptU (A,a) (B,transport p a) =
- <i> (p @ i,transport (<j>p @ (i/\j)) a)
+ <i> (p @ i,transport (<j> p @ (i/\j)) a)
 
 Omega (X:ptU) : ptU = (Id X.1 X.2 X.2,refl X.1 X.2)
 
@@ -87,7 +87,7 @@ s1ToCId (p: Id sone north north) : Id S1 base base
  = <i> transport s1EqCircle (p @ i)
 
 s1ToCIdInv (p : Id S1 base base) : Id sone north north
- = <i> (transport (<j> s1EqCircle @(-j)) (p @ i))
+ = <i> (transport (<j> s1EqCircle @ -j) (p @ i))
 
 loop1S :  Id sone north north = s1ToCIdInv loop1