From e2190e68b3ffc5b0ce7919c151eac34c3ff08395 Mon Sep 17 00:00:00 2001 From: Anders 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 = 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 + -- 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 = square (l @ i) +tripleLoop (l : loopS1) : loopS1 = 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 ( (IdP ( 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 = - comp A a - [(i = 0) -> p @ (j \/ - k), - (i = 1) -> p @ (j /\ k), - (j = 0) -> p @ (i \/ - k), - (j = 1) -> p @ (i /\ k)] - - test (A : U) (a b : A) (p : Id A a b) : Id A a a = 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 ( (IdP ( 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 = + comp A a + [(i = 0) -> p @ (j \/ - k), + (i = 1) -> p @ (j /\ k), + (j = 0) -> p @ (i \/ - k), + (j = 1) -> p @ (i /\ k)] -- 2.34.1