From c055ffa6042442b70f99f5dec4d1931d6502a506 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Mon, 30 Mar 2015 17:06:08 +0200 Subject: [PATCH] bugfix in simplify, conv; extended prelude --- Eval.hs | 15 +++++++-------- examples/prelude.ctt | 23 +++++++++++++++++++++++ 2 files changed, 30 insertions(+), 8 deletions(-) diff --git a/Eval.hs b/Eval.hs index bf127b0..a1021c6 100644 --- a/Eval.hs +++ b/Eval.hs @@ -140,7 +140,7 @@ eval rho v = case v of Snd a -> sndVal (eval rho a) Where t decls -> eval (Def decls rho) t Con name ts -> VCon name (map (eval rho) ts) - PCon name a ts phi -> + PCon name a ts phi -> pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi) Split{} -> Ter v rho Sum{} -> Ter v rho @@ -295,15 +295,14 @@ trans i v0 v1 = case (v0,v1) of Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi Nothing -> error $ "trans: missing path constructor " ++ c ++ " in " ++ show v0 + (VGlue a ts,_) -> transGlue i a ts v1 + (VComp VU a es,_) -> transU i a es v1 _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 (Ter (Sum _ _ nass) env,VComp b w ws) -> comp k v01 (trans i v0 w) ws' where v01 = v0 `face` (i ~> 1) -- b is vi0 and independent of j k = fresh (v0,v1,Atom i) transp alpha w = trans i (v0 `face` alpha) (w @@ k) ws' = mapWithKey transp ws - - (VGlue a ts,_) -> transGlue i a ts v1 - (VComp VU a es,_) -> transU i a es v1 _ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0 ++ "\n and v1 = " ++ show v1 @@ -716,15 +715,15 @@ simplify :: Int -> Name -> Val -> Val simplify k j v = case v of VTrans p u | isIndep k j (p @@ j) -> simplify k j u VComp a u ts -> - let (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts + let (indep,ts') = Map.partition (\t -> isIndep k j (t @@ j)) ts in if Map.null ts' then simplify k j u else VComp a u ts' VCompElem a es u us -> - let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es + let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es us' = intersection us es' in if Map.null es' then simplify k j u else VCompElem a es' u us' VElimComp a es u -> - let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es - u' = simplify k j u + let (indep,es') = Map.partition (\e -> isIndep k j (e @@ j)) es + u' = simplify k j u in if Map.null es' then u' else case u' of VCompElem _ _ w _ -> simplify k j w _ -> VElimComp a es' u' diff --git a/examples/prelude.ctt b/examples/prelude.ctt index da11540..f772009 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -68,3 +68,26 @@ constSquare (A : U) (a : A) (p : Id A a a) : Square A a a p a a p p p = (i = 1) -> p @ (j /\ k), (j = 0) -> p @ (i \/ - k), (j = 1) -> p @ (i /\ k)] + +prop (A : U) : U = (a b : A) -> Id A a b +set (A : U) : U = (a b : A) -> prop (Id A a b) + +propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q = + comp A a [ (i=0) -> h a a + , (i=1) -> h a b + , (j=0) -> h a (p @ i) + , (j=1) -> h a (q @ i)] + +propIsProp (A : U) (f g : prop A) : Id (prop A) f g = + \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i + +setIsProp (A : U) (f g : set A) : Id (set A) f g = + \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i + +IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U = + IdP ( P (p @ i)) u0 u1 + +lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A) + (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 = + (pP (p @ i) (transport ( P (p @ i /\ j)) b0) + (transport ( P (p @ i \/ -j)) b1)) @ i \ No newline at end of file -- 2.34.1