Add more tests

diff --git a/Eval.hs b/Eval.hs
index fc8b0bd32cc1244b313b876ea812abe15f6ac42f..35c3801e4a027721fa46cc4ee2e9f8293972a081 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -394,7 +394,8 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid??
            else VComp a u (Map.map (VPath i) ts)
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
     VPCon{} -> VComp a u (Map.map (VPath i) ts)
-    _ -> error "comp ter sum"
+    VComp{} -> VComp a u (Map.map (VPath i) ts) 
+    _ -> error $ "comp ter sum" ++ show u
 
 compNeg :: Name -> Val -> Val -> System Val -> Val
 compNeg i a u ts = comp i a u (ts `sym` i)

diff --git a/Resolver.hs b/Resolver.hs
index de375672bf7b838c25672ec76b4d39d008b4d822..a13817f8084814a2f68a973858e7352504341ccb 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -281,11 +281,12 @@ resolveLabel cs (PLabel n vdecl t0 t1) =
                           <*> local (insertIdents cs) (resolveExp t0)
                           <*> local (insertIdents cs) (resolveExp t1)
 
-piToFam :: Exp -> Resolver Ter
-piToFam (Fun a b)    = lam ("_",a) $ resolveExp b
-piToFam (Pi ptele b) = do
+piToFam :: ((Int,Int),String) -> Exp -> Resolver Ter
+piToFam _ (Fun a b)    = lam ("_",a) $ resolveExp b
+piToFam _ (Pi ptele b) = do
   (x,a):tele <- flattenPTele ptele
   lam (x,a) (binds CTT.Pi tele (resolveExp b))
+piToFam (l,n) _ = throwError $ "Pi type expected in " ++ n ++ " at " ++ show l
 
 -- Resolve Data or Def or Split declarations
 resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])
@@ -308,7 +309,7 @@ resolveDecl d = case d of
     loc  <- getLoc l
     a    <- binds CTT.Pi tele' (resolveExp t)
     let vars = map fst tele'
-    fam  <- local (insertVars vars) $ piToFam t
+    fam  <- local (insertVars vars) $ piToFam (l,f) t
     brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs)
     body <- lams tele' (return $ CTT.Split f loc fam brs')
     return ((f,(a,body)),[(f,Variable)])

diff --git a/examples/circle.ctt b/examples/circle.ctt
index be59ff2a0b2954b1032f1d297f3429899068031c..db62a60cef1503350199489e1682780a1f72ae42 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -21,9 +21,25 @@ winding (p : loopS1) : Z = transport rem zeroZ
   where
     rem : Id U Z Z = <i> helix (p @ i)
 
+-- All of these should be equal to "posZ (suc zero)":
 loop2 : loopS1 = compId S1 base base base loop' loop'
 loop2' : loopS1 = compId' S1 base base base loop' loop'
 loop2'' : loopS1 = compId'' S1 base base loop' base loop'
 
+mLoop : (x : S1) -> Id S1 x x = split
+  base -> loop'
+  loop @ i -> (constSquare S1 base loop') @ i
 
-test : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ 
\ No newline at end of file
+  -- <i> let rem : S1 -> S1 = split
+  --           base -> loop' @ i
+  --           loop @ j -> ((constSquare S1 base loop') @ j) @ i
+  --     in rem x
+
+mult (x : S1) : S1 -> S1 = split
+  base -> x
+  loop @ i -> (mLoop x) @ i
+
+square (x : S1) : S1 = mult x x
+
+doubleLoop (l : loopS1) : loopS1 = <i> square (l @ i)
+tripleLoop (l : loopS1) : loopS1 = <i> mult (l @ i) (square (l @ i))
\ No newline at end of file

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 8733fe7f5121cab597c8eb069bd5791866f3aed8..1b2153515d6f4be76fa302023286c5baa5671569 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -66,29 +66,6 @@ kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
 --                         (k ~> 0,p @@ i),
 --                         (k ~> 1,(s @@ j) @@ i)]
 
-
-
---         u
---    a0 ----- a1
---    |        |
--- r0 |        | r1
---    |        |
---    b0 ----- b1
---         v
-
-Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
-               (b0 b1 : A) (v : Id A b0 b1)
-               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
-  = 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 = 0) -> <k> p @ (j \/ - k),
-      (i = 1) -> <k> p @ (j /\ k),
-      (j = 0) -> <k> p @ (i \/ - k),
-      (j = 1) -> <k> p @ (i /\ k)]
-
-
 test (A : U) (a b : A) (p : Id A a b) : Id A a a =
   <i> p @ (i /\ -i)
 

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 4abdb03cd214fc3f59aaef443e3d52d233ef75fd..c3bd9f6ec42bb499760bd9556a7513faac75c7d1 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -60,3 +60,10 @@ Square (A : U) (a0 a1 : A) (u : Id A a0 a1)
                (b0 b1 : A) (v : Id A b0 b1)
                (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U
   = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
+
+constSquare (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 = 0) -> <k> p @ (j \/ - k),
+      (i = 1) -> <k> p @ (j /\ k),
+      (j = 0) -> <k> p @ (i \/ - k),
+      (j = 1) -> <k> p @ (i /\ k)]