From e2190e68b3ffc5b0ce7919c151eac34c3ff08395 Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Thu, 26 Mar 2015 18:15:04 +0100
Subject: [PATCH] Add more tests

---
 Eval.hs              |  3 ++-
 Resolver.hs          |  9 +++++----
 examples/circle.ctt  | 18 +++++++++++++++++-
 examples/nat.ctt     | 23 -----------------------
 examples/prelude.ctt |  7 +++++++
 5 files changed, 31 insertions(+), 29 deletions(-)

diff --git a/Eval.hs b/Eval.hs
index fc8b0bd..35c3801 100644
--- 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 de37567..a13817f 100644
--- 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 be59ff2..db62a60 100644
--- 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 8733fe7..1b21535 100644
--- 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 4abdb03..c3bd9f6 100644
--- 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)]
-- 
2.34.1