From 0792d7900ab6713851c8d80576d1fdecde9189c5 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 26 Jul 2016 16:53:35 +0200 Subject: [PATCH] rename Eq to Id --- CTT.hs | 24 ++++++------ Eval.hs | 70 ++++++++++++++++----------------- Exp.cf | 6 +-- Resolver.hs | 6 +-- TypeChecker.hs | 12 +++--- examples/eq.ctt | 102 ++++++++++++++++++++++++------------------------ 6 files changed, 110 insertions(+), 110 deletions(-) diff --git a/CTT.hs b/CTT.hs index f974c4b..de3c8c7 100644 --- a/CTT.hs +++ b/CTT.hs @@ -119,10 +119,10 @@ data Ter = Pi Ter | Glue Ter (System Ter) | GlueElem Ter (System Ter) | UnGlueElem Ter (System Ter) - -- Eq - | Eq Ter Ter Ter - | EqPair Ter (System Ter) - | EqJ Ter Ter Ter Ter Ter Ter + -- Id + | Id Ter Ter Ter + | IdPair Ter (System Ter) + | IdJ Ter Ter Ter Ter Ter Ter deriving Eq -- For an expression t, returns (u,ts) where u is no application and t = u ts @@ -167,9 +167,9 @@ data Val = VU -- Composition for HITs; the type is constant | VHComp Val Val (System Val) - -- Eq - | VEq Val Val Val - | VEqPair Val (System Val) + -- Id + | VId Val Val Val + | VIdPair Val (System Val) -- Neutral values: | VVar Ident Val @@ -181,7 +181,7 @@ data Val = VU | VAppFormula Val Formula | VLam Ident Val Val | VUnGlueElemU Val Val (System Val) - | VEqJ Val Val Val Val Val Val + | VIdJ Val Val Val Val Val Val deriving Eq isNeutral :: Val -> Bool @@ -198,7 +198,7 @@ isNeutral v = case v of VAppFormula{} -> True VUnGlueElemU{} -> True VUnGlueElem{} -> True - VEqJ{} -> True + VIdJ{} -> True _ -> False isNeutralSystem :: System Val -> Bool @@ -383,9 +383,9 @@ showTer v = case v of Glue a ts -> text "Glue" <+> showTer1 a <+> text (showSystem ts) GlueElem a ts -> text "glue" <+> showTer1 a <+> text (showSystem ts) UnGlueElem a ts -> text "unglue" <+> showTer1 a <+> text (showSystem ts) - Eq a u v -> text "Eq" <+> showTers [a,u,v] - EqPair b ts -> text "eqC" <+> showTer1 b <+> text (showSystem ts) - EqJ a t c d x p -> text "eqJ" <+> showTers [a,t,c,d,x,p] + Id a u v -> text "Id" <+> showTers [a,u,v] + IdPair b ts -> text "IdC" <+> showTer1 b <+> text (showSystem ts) + IdJ a t c d x p -> text "IdJ" <+> showTers [a,t,c,d,x,p] showTers :: [Ter] -> Doc showTers = hsep . map showTer1 diff --git a/Eval.hs b/Eval.hs index 3b60833..2681214 100644 --- a/Eval.hs +++ b/Eval.hs @@ -77,9 +77,9 @@ instance Nominal Val where VUnGlueElem a ts -> support (a,ts) VCompU a ts -> support (a,ts) VUnGlueElemU a b es -> support (a,b,es) - VEqPair u us -> support (u,us) - VEq a u v -> support (a,u,v) - VEqJ a u c d x p -> support [a,u,c,d,x,p] + VIdPair u us -> support (u,us) + VId a u v -> support (a,u,v) + VIdJ a u c d x p -> support [a,u,c,d,x,p] act u (i, phi) | i `notElem` support u = u | otherwise = @@ -114,10 +114,10 @@ instance Nominal Val where VUnGlueElem a ts -> unglueElem (acti a) (acti ts) VUnGlueElemU a b es -> unGlueU (acti a) (acti b) (acti es) VCompU a ts -> compUniv (acti a) (acti ts) - VEqPair u us -> VEqPair (acti u) (acti us) - VEq a u v -> VEq (acti a) (acti u) (acti v) - VEqJ a u c d x p -> - eqJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p) + VIdPair u us -> VIdPair (acti u) (acti us) + VId a u v -> VId (acti a) (acti u) (acti v) + VIdJ a u c d x p -> + idJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -148,10 +148,10 @@ instance Nominal Val where VUnGlueElem a ts -> VUnGlueElem (sw a) (sw ts) VUnGlueElemU a b es -> VUnGlueElemU (sw a) (sw b) (sw es) VCompU a ts -> VCompU (sw a) (sw ts) - VEqPair u us -> VEqPair (sw u) (sw us) - VEq a u v -> VEq (sw a) (sw u) (sw v) - VEqJ a u c d x p -> - VEqJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p) + VIdPair u us -> VIdPair (sw u) (sw us) + VId a u v -> VId (sw a) (sw u) (sw v) + VIdJ a u c d x p -> + VIdJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p) ----------------------------------------------------------------------- -- The evaluator @@ -189,9 +189,9 @@ eval rho@(_,_,_,Nameless os) v = case v of Glue a ts -> glue (eval rho a) (evalSystem rho ts) GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) UnGlueElem a ts -> unglueElem (eval rho a) (evalSystem rho ts) - Eq a r s -> VEq (eval rho a) (eval rho r) (eval rho s) - EqPair b ts -> VEqPair (eval rho b) (evalSystem rho ts) - EqJ a t c d x p -> eqJ (eval rho a) (eval rho t) (eval rho c) + Id a r s -> VId (eval rho a) (eval rho r) (eval rho s) + IdPair b ts -> VIdPair (eval rho b) (evalSystem rho ts) + IdJ a t c d x p -> idJ (eval rho a) (eval rho t) (eval rho c) (eval rho d) (eval rho x) (eval rho p) _ -> error $ "Cannot evaluate " ++ show v @@ -280,7 +280,7 @@ inferType v = case v of VComp a _ _ -> a @@ One -- VUnGlueElem _ b _ -> b -- This is wrong! Store the type?? VUnGlueElemU _ b _ -> b - VEqJ _ _ c _ x p -> app (app c x) p + VIdJ _ _ c _ x p -> app (app c x) p _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -307,15 +307,15 @@ comp i a u ts = case a of VPathP p v0 v1 -> let j = fresh (Atom i,a,u,ts) in VPLam j $ comp i (p @@ j) (u @@ j) $ insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts) - VEq b v0 v1 -> case u of - VEqPair r _ | all isEqPair (elems ts) -> + VId b v0 v1 -> case u of + VIdPair r _ | all isIdPair (elems ts) -> let j = fresh (Atom i,a,u,ts) - VEqPair z _ @@@ phi = z @@ phi - sys (VEqPair _ ws) = ws + VIdPair z _ @@@ phi = z @@ phi + sys (VIdPair _ ws) = ws w = VPLam j $ comp i b (r @@ j) $ insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@@ j) ts) - in VEqPair w (joinSystem (Map.map sys (ts `face` (i ~> 1)))) + in VIdPair w (joinSystem (Map.map sys (ts `face` (i ~> 1)))) _ -> VComp (VPLam i a) u (Map.map (VPLam i) ts) VSigma a f -> VPair ui1 comp_u2 where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts) @@ -424,20 +424,20 @@ squeezes i xas e us = comps j xas (e `disj` (i,j)) us' ------------------------------------------------------------------------------- --- | Eq +-- | Id -eqJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val -eqJ a v c d x p = case p of - VEqPair w ws -> comp i (app (app c (w @@ i)) w') d +idJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val +idJ a v c d x p = case p of + VIdPair w ws -> comp i (app (app c (w @@ i)) w') d (border d (shape ws)) - where w' = VEqPair (VPLam j $ w @@ (Atom i :/\: Atom j)) + where w' = VIdPair (VPLam j $ w @@ (Atom i :/\: Atom j)) (insertSystem (i ~> 0) v ws) i:j:_ = freshs [a,v,c,d,x,p] - _ -> VEqJ a v c d x p + _ -> VIdJ a v c d x p -isEqPair :: Val -> Bool -isEqPair VEqPair{} = True -isEqPair _ = False +isIdPair :: Val -> Bool +isIdPair VIdPair{} = True +isIdPair _ = False ------------------------------------------------------------------------------- @@ -884,9 +884,9 @@ instance Convertible Val where (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') - (VEqPair v vs,VEqPair v' vs') -> conv ns (v,vs) (v',vs') - (VEq a u v,VEq a' u' v') -> conv ns (a,u,v) (a',u',v') - (VEqJ a u c d x p,VEqJ a' u' c' d' x' p') -> + (VIdPair v vs,VIdPair v' vs') -> conv ns (v,vs) (v',vs') + (VId a u v,VId a' u' v') -> conv ns (a,u,v) (a',u',v') + (VIdJ a u c d x p,VIdJ a' u' c' d' x' p') -> conv ns [a,u,c,d,x,p] [a',u',c',d',x',p'] _ -> False @@ -955,9 +955,9 @@ instance Normal Val where VSplit u t -> VSplit (normal ns u) (normal ns t) VApp u v -> app (normal ns u) (normal ns v) VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi) - VEq a u v -> VEq (normal ns a) (normal ns u) (normal ns v) - VEqPair u us -> VEqPair (normal ns u) (normal ns us) - VEqJ a u c d x p -> eqJ (normal ns a) (normal ns u) (normal ns c) + VId a u v -> VId (normal ns a) (normal ns u) (normal ns v) + VIdPair u us -> VIdPair (normal ns u) (normal ns us) + VIdJ a u c d x p -> idJ (normal ns a) (normal ns u) (normal ns c) (normal ns d) (normal ns x) (normal ns p) _ -> v diff --git a/Exp.cf b/Exp.cf index 29cfb0e..f93cc81 100644 --- a/Exp.cf +++ b/Exp.cf @@ -42,9 +42,9 @@ Fill. Exp3 ::= "fill" Exp4 Exp4 System ; Glue. Exp3 ::= "Glue" Exp4 System ; GlueElem. Exp3 ::= "glue" Exp4 System ; UnGlueElem. Exp3 ::= "unglue" Exp4 System ; -Eq. Exp3 ::= "Eq" Exp4 Exp4 Exp3 ; -EqPair. Exp3 ::= "eqC" Exp4 System ; -EqJ. Exp3 ::= "eqJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ; +Id. Exp3 ::= "Id" Exp4 Exp4 Exp3 ; +IdPair. Exp3 ::= "idC" Exp4 System ; +IdJ. Exp3 ::= "idJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ; Fst. Exp4 ::= Exp4 ".1" ; Snd. Exp4 ::= Exp4 ".2" ; Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; diff --git a/Resolver.hs b/Resolver.hs index 9cd9890..c61f65d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -219,9 +219,9 @@ resolveExp e = case e of Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts UnGlueElem u ts -> CTT.UnGlueElem <$> resolveExp u <*> resolveSystem ts - Eq a u v -> CTT.Eq <$> resolveExp a <*> resolveExp u <*> resolveExp v - EqPair u ts -> CTT.EqPair <$> resolveExp u <*> resolveSystem ts - EqJ a t c d x p -> CTT.EqJ <$> resolveExp a <*> resolveExp t <*> resolveExp c + Id a u v -> CTT.Id <$> resolveExp a <*> resolveExp u <*> resolveExp v + IdPair u ts -> CTT.IdPair <$> resolveExp u <*> resolveSystem ts + IdJ a t c d x p -> CTT.IdJ <$> resolveExp a <*> resolveExp t <*> resolveExp c <*> resolveExp d <*> resolveExp x <*> resolveExp p _ -> do modName <- asks envModule diff --git a/TypeChecker.hs b/TypeChecker.hs index 8b74327..7a038de 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -215,12 +215,12 @@ check a t = case (a,t) of check va u vu <- evalTyping u checkGlueElemU vu ves us - (VU,Eq a a0 a1) -> do + (VU,Id a a0 a1) -> do check VU a va <- evalTyping a check va a0 check va a1 - (VEq va va0 va1,EqPair w ts) -> do + (VId va va0 va1,IdPair w ts) -> do check (VPathP (constPath va) va0 va1) w vw <- evalTyping w checkSystemWith ts $ \alpha tAlpha -> @@ -498,21 +498,21 @@ infer e = case e of checks (bs,nu) es mapM_ checkFormula phis return va - EqJ a u c d x p -> do + IdJ a u c d x p -> do check VU a va <- evalTyping a check va u vu <- evalTyping u - let refu = VEqPair (constPath vu) $ mkSystem [(eps,vu)] + let refu = VIdPair (constPath vu) $ mkSystem [(eps,vu)] rho <- asks env let z = Var "z" - ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Eq a u z) U + ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Id a u z) U check ctype c vc <- evalTyping c check (app (app vc vu) refu) d check va x vx <- evalTyping x - check (VEq va vu vx) p + check (VId va vu vx) p vp <- evalTyping p return (app (app vc vx) vp) _ -> throwError ("infer " ++ show e) diff --git a/examples/eq.ctt b/examples/eq.ctt index 34f0ea6..d093797 100644 --- a/examples/eq.ctt +++ b/examples/eq.ctt @@ -2,80 +2,80 @@ module eq where import prelude -refEq (A : U) (a : A) : Eq A a a = - eqC ( a) [ -> a ] +refId (A : U) (a : A) : Id A a a = + idC ( a) [ -> a ] -JJ (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) - (x : A) (p : Eq A a x) : C x p - = eqJ A a C d x p +JJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a)) + (x : A) (p : Id A a x) : C x p + = idJ A a C d x p -JJref (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) - : C a (refEq A a) - = eqJ A a C d a (refEq A a) +JJref (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a)) + : C a (refId A a) + = idJ A a C d a (refId A a) -JJEq (A : U) (a : A) (C : (x : A) -> Eq A a x -> U) (d : C a (refEq A a)) - : Eq (C a (refEq A a)) d (JJ A a C d a (refEq A a)) - = refEq (C a (refEq A a)) d +JJId (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refId A a)) + : Id (C a (refId A a)) d (JJ A a C d a (refId A a)) + = refId (C a (refId A a)) d -substEq (A : U) (F : A -> U) (a b : A) (p : Eq A a b) (e : F a) : F b = - JJ A a (\ (x : A) (_ : Eq A a x) -> F x) e b p +substId (A : U) (F : A -> U) (a b : A) (p : Id A a b) (e : F a) : F b = + JJ A a (\ (x : A) (_ : Id A a x) -> F x) e b p -substEqRef (A : U) (F : A -> U) (a : A) (e : F a) : F a = - substEq A F a a (refEq A a) e +substIdRef (A : U) (F : A -> U) (a : A) (e : F a) : F a = + substId A F a a (refId A a) e -transEq (A : U) (a b c : A) (p : Eq A a b) (q : Eq A b c) : Eq A a c = - substEq A (\ (z : A) -> Eq A a z) b c q p +transId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = + substId A (\ (z : A) -> Id A a z) b c q p -transEqRef (A : U) (a b : A) (p : Eq A a b): Eq A a b = - transEq A a a b (refEq A a) p +transIdRef (A : U) (a b : A) (p : Id A a b): Id A a b = + transId A a a b (refId A a) p -eqToId (A : U) (a b : A) (p : Eq A a b) : Id A a b = - eqJ A a (\ (b : A) (p : Eq A a b) -> Id A a b) +idToPath (A : U) (a b : A) (p : Id A a b) : Path A a b = + idJ A a (\ (b : A) (p : Id A a b) -> Path A a b) ( a) b p -idToEq (A : U) (a b : A) (p : Id A a b) : Eq A a b = --- eqC p [] - J A a (\ (b : A) (p : Id A a b) -> Eq A a b) - (refEq A a) b p +idToId (A : U) (a b : A) (p : Path A a b) : Id A a b = +-- idC p [] + J A a (\ (b : A) (p : Path A a b) -> Id A a b) + (refId A a) b p -idToEqRef (A : U) (a : A) : Id (Eq A a a) (refEq A a) (idToEq A a a (<_> a)) = - JEq A a (\ (b : A) (p : Id A a b) -> Eq A a b) (refEq A a) +idToIdRef (A : U) (a : A) : Path (Id A a a) (refId A a) (idToId A a a (<_> a)) = + JEq A a (\ (b : A) (p : Path A a b) -> Id A a b) (refId A a) -eqToIdRef (A : U) (a : A) : Id (Id A a a) (<_> a) (eqToId A a a (refEq A a)) = +idToPathRef (A : U) (a : A) : Path (Path A a a) (<_> a) (idToPath A a a (refId A a)) = a -idToEqToId (A : U) (a b : A) (p : Id A a b) : - Id (Id A a b) p (eqToId A a b (idToEq A a b p)) = - J A a (\ (b : A) (p : Id A a b) -> - Id (Id A a b) p (eqToId A a b (idToEq A a b p))) - ( eqToId A a a (idToEqRef A a @ j)) b p +idToIdToPath (A : U) (a b : A) (p : Path A a b) : + Path (Path A a b) p (idToPath A a b (idToId A a b p)) = + J A a (\ (b : A) (p : Path A a b) -> + Path (Path A a b) p (idToPath A a b (idToId A a b p))) + ( idToPath A a a (idToIdRef A a @ j)) b p lem (A : U) (a : A) : - Id (Eq A a a) (refEq A a) (idToEq A a a (eqToId A a a (refEq A a))) = - compId (Eq A a a) - (refEq A a) (idToEq A a a (<_> a)) (idToEq A a a (eqToId A a a (refEq A a))) - (idToEqRef A a) ( idToEq A a a (eqToIdRef A a @ k)) - -eqToIdToEq (A : U) (a b : A) (p : Eq A a b) : - Id (Eq A a b) p (idToEq A a b (eqToId A a b p)) = - eqJ A a (\ (b : A) (p : Eq A a b) -> - Id (Eq A a b) p (idToEq A a b (eqToId A a b p))) + Path (Id A a a) (refId A a) (idToId A a a (idToPath A a a (refId A a))) = + compPath (Id A a a) + (refId A a) (idToId A a a (<_> a)) (idToId A a a (idToPath A a a (refId A a))) + (idToIdRef A a) ( idToId A a a (idToPathRef A a @ k)) + +idToPathToId (A : U) (a b : A) (p : Id A a b) : + Path (Id A a b) p (idToId A a b (idToPath A a b p)) = + idJ A a (\ (b : A) (p : Id A a b) -> + Path (Id A a b) p (idToId A a b (idToPath A a b p))) (lem A a) b p -------------------------------------------------------------------------------- -- Some tests -mop (A B : U) (f : A -> B) (u v : A) (p : Eq A u v) : Eq B (f u) (f v) = - JJ A u (\ (v : A) (p : Eq A u v) -> Eq B (f u) (f v)) - (refEq B (f u)) v p +mop (A B : U) (f : A -> B) (u v : A) (p : Id A u v) : Id B (f u) (f v) = + JJ A u (\ (v : A) (p : Id A u v) -> Id B (f u) (f v)) + (refId B (f u)) v p -mopComp (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v) - : Eq C (g (f u)) (g (f v)) = mop A C (\ (x : A) -> g (f x)) u v p +mopComp (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Id A u v) + : Id C (g (f u)) (g (f v)) = mop A C (\ (x : A) -> g (f x)) u v p -mopComp' (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Eq A u v) - : Eq C (g (f u)) (g (f v)) = mop B C g (f u) (f v) (mop A B f u v p) +mopComp' (A B C : U) (f : A -> B) (g : B -> C) (u v : A) (p : Id A u v) + : Id C (g (f u)) (g (f v)) = mop B C g (f u) (f v) (mop A B f u v p) -superMop (A B : U) (f : A -> B) (u v : A) (p : Id A u v) : Eq B (f u) (f v) = - eqC ( f (p @ i)) [ ] +superMop (A B : U) (f : A -> B) (u v : A) (p : Path A u v) : Id B (f u) (f v) = + idC ( f (p @ i)) [ ] -- 2.34.1