From 8e82582a972b6432f3a7108c20f3d2613091d66a Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 4 Jun 2015 14:47:21 +0200 Subject: [PATCH] remove commented code --- Eval.hs | 431 +------------------------------------------------ TypeChecker.hs | 2 +- 2 files changed, 8 insertions(+), 425 deletions(-) diff --git a/Eval.hs b/Eval.hs index 5e7f27a..f7547d4 100644 --- a/Eval.hs +++ b/Eval.hs @@ -42,17 +42,6 @@ instance Nominal Ctxt where act e _ = e swap e _ = e --- instance Nominal HIso where --- support h = case h of --- Iso a f g s t -> support [a,f,g,s,t] --- Eq v -> support v --- act h iphi = case h of --- Iso a f g s t -> Iso (a `act` iphi) (f `act` iphi) (g `act` iphi) (s `act` iphi) (t `act` iphi) --- Eq v -> Eq (v `act` iphi) --- swap h ij = case h of --- Iso a f g s t -> Iso (a `swap` ij) (f`swap` ij) (g`swap` ij) (s`swap` ij) (t`swap` ij) --- Eq v -> Eq (v`swap` ij) - instance Nominal Val where support v = case v of VU -> [] @@ -61,7 +50,6 @@ instance Nominal Val where VComp a u ts -> support (a,u,ts) VIdP a v0 v1 -> support [a,v0,v1] VPath i v -> i `delete` support v - -- VTrans u v -> support (u,v) VSigma u v -> support (u,v) VPair u v -> support (u,v) VFst u -> support u @@ -69,7 +57,6 @@ instance Nominal Val where VCon _ vs -> support vs VPCon _ a vs phis -> support (a,vs,phis) VHComp a u ts -> support (a,u,ts) - -- VHSqueeze a u phi -> support (a,u,phi) VVar _ v -> support v VApp u v -> support (u,v) VLam _ u v -> support (u,v) @@ -80,10 +67,6 @@ instance Nominal Val where VCompU a ts -> support (a,ts) VUnGlueElem a b hs -> support (a,b,hs) VUnGlueElemU a b es -> support (a,b,es) - -- VGlueLine a phi psi -> support (a,phi,psi) - -- VGlueLineElem a phi psi -> support (a,phi,psi) - -- VCompElem a es u us -> support (a,es,u,us) - -- VElimComp a es u -> support (a,es,u) act u (i, phi) | i `notElem` support u = u | otherwise = @@ -100,7 +83,6 @@ instance Nominal Val where | j `notElem` sphi -> VPath j (acti v) | otherwise -> VPath k (acti (v `swap` (j,k))) where k = fresh (v,Atom i,phi) - -- VTrans u v -> transLine (acti u) (acti v) VSigma a f -> VSigma (acti a) (acti f) VPair u v -> VPair (acti u) (acti v) VFst u -> fstVal (acti u) @@ -108,7 +90,6 @@ instance Nominal Val where VCon c vs -> VCon c (acti vs) VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) VHComp a u us -> hComp (acti a) (acti u) (acti us) - -- VHSqueeze a u phi -> hSqueeze (acti a) (acti u) (acti phi) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -119,10 +100,6 @@ instance Nominal Val where VUnGlueElem a b hs -> unGlue (acti a) (acti b) (acti hs) VUnGlueElemU a b es -> unGlueU (acti a) (acti b) (acti es) VCompU a ts -> compUniv (acti a) (acti ts) - -- VGlueLine a phi psi -> glueLine (acti a) (acti phi) (acti psi) - -- VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi) - -- VCompElem a es u us -> compElem (acti a) (acti es) (acti u) (acti us) - -- VElimComp a es u -> elimComp (acti a) (acti es) (acti u) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -135,7 +112,6 @@ instance Nominal Val where VComp a v ts -> VComp (sw a) (sw v) (sw ts) VIdP a u v -> VIdP (sw a) (sw u) (sw v) VPath k v -> VPath (swapName k ij) (sw v) - -- VTrans u v -> VTrans (sw u) (sw v) VSigma a f -> VSigma (sw a) (sw f) VPair u v -> VPair (sw u) (sw v) VFst u -> VFst (sw u) @@ -143,7 +119,6 @@ instance Nominal Val where VCon c vs -> VCon c (sw vs) VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis) VHComp a u us -> VHComp (sw a) (sw u) (sw us) - -- VHSqueeze a u phi -> VHSqueeze (sw a) (sw u) (sw phi) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -154,10 +129,6 @@ instance Nominal Val where VUnGlueElem a b hs -> VUnGlueElem (sw a) (sw b) (sw hs) VUnGlueElemU a b es -> VUnGlueElemU (sw a) (sw b) (sw es) VCompU a ts -> VCompU (sw a) (sw ts) - -- VGlueLine a phi psi -> VGlueLine (sw a) (sw phi) (sw psi) - -- VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi) - -- VCompElem a es u us -> VCompElem (sw a) (sw es) (sw u) (sw us) - -- VElimComp a es u -> VElimComp (sw a) (sw es) (sw u) ----------------------------------------------------------------------- -- The evaluator @@ -186,18 +157,10 @@ eval rho v = case v of Path i t -> let j = fresh rho in VPath j (eval (sub (i,Atom j) rho) t) - -- Trans u v -> transLine (eval rho u) (eval rho v) AppFormula e phi -> eval rho e @@ evalFormula rho phi Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts) Glue a ts -> glue (eval rho a) (evalSystem rho ts) GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) - -- GlueLine a phi psi -> - -- glueLine (eval rho a) (evalFormula rho phi) (evalFormula rho psi) - -- GlueLineElem a phi psi -> - -- glueLineElem (eval rho a) (evalFormula rho phi) (evalFormula rho psi) - -- CompElem a es u us -> compElem (eval rho a) (evalSystem rho es) (eval rho u) - -- (evalSystem rho us) - -- ElimComp a es u -> elimComp (eval rho a) (evalSystem rho es) (eval rho u) _ -> error $ "Cannot evaluate " ++ show v evalFormula :: Env -> Formula -> Formula @@ -237,14 +200,6 @@ app u v = case (u,v) of in comp j (app f (fill j a w wsj)) w' ws' _ -> error $ "app: Split annotation not a Pi type " ++ show u (Ter Split{} _,_) | isNeutral v -> VSplit u v - -- (Ter Split{} _,VCompElem _ _ w _) -> app u w - -- (Ter Split{} _,VElimComp _ _ w) -> app u w - -- (VTrans (VPath i (VPi a f)) li0,vi1) -> - -- let j = fresh (u,vi1) - -- (aj,fj) = (a,f) `swap` (i,j) - -- v = transFillNeg j aj vi1 - -- vi0 = transNeg j aj vi1 - -- in trans j (app fj v) (app li0 vi0) (VComp (VPath i (VPi a f)) li0 ts,vi1) -> let j = fresh (u,vi1) (aj,fj) = (a,f) `swap` (i,j) @@ -254,19 +209,13 @@ app u v = case (u,v) of in comp j (app fj v) (app li0 vi0) (intersectionWith app tsj (border v tsj)) _ | isNeutral u -> VApp u v - -- (VCompElem _ _ u _,_) -> app u v - -- (VElimComp _ _ u,_) -> app u v _ -> error $ "app \n " ++ show u ++ "\n " ++ show v fstVal, sndVal :: Val -> Val fstVal (VPair a b) = a --- fstVal (VElimComp _ _ u) = fstVal u --- fstVal (VCompElem _ _ u _) = fstVal u fstVal u | isNeutral u = VFst u fstVal u = error $ "fstVal: " ++ show u ++ " is not neutral." sndVal (VPair a b) = b --- sndVal (VElimComp _ _ u) = sndVal u --- sndVal (VCompElem _ _ u _) = sndVal u sndVal u | isNeutral u = VSnd u sndVal u = error $ "sndVal: " ++ show u ++ " is not neutral." @@ -298,7 +247,6 @@ inferType v = case v of VComp a _ _ -> a @@ One VUnGlueElem _ b hs -> glue b hs VUnGlueElemU _ b es -> compUniv b es --- VTrans a _ -> a @@ One _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -308,8 +256,6 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of (VIdP _ a0 _,Dir 0) -> a0 (VIdP _ _ a1,Dir 1) -> a1 _ -> VAppFormula v (toFormula phi) --- (VCompElem _ _ u _) @@ phi = u @@ phi --- (VElimComp _ _ u) @@ phi = u @@ phi v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val @@ -319,7 +265,7 @@ pcon c a@(Ter (HSum _ _ lbls) rho) us phis = case lookupPLabel c lbls of where rho' = subs (zip is phis) (updsTele tele us rho) vs = evalSystem rho' ts Nothing -> error "pcon" --- pcon c a us phi = VPCon c a us phi +pcon c a us phi = VPCon c a us phi ----------------------------------------------------------- -- Transport @@ -334,41 +280,6 @@ transNegLine u v = transNeg i (u @@ i) v trans :: Name -> Val -> Val -> Val trans i v0 v1 = comp i v0 v1 Map.empty --- trans i v0 v1 | i `notElem` support v0 = v1 --- trans i v0 v1 = case (v0,v1) of --- (VIdP a u v,w) -> --- let j = fresh (Atom i,v0,w) --- ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)] --- in VPath j $ comp i (a @@ j) (w @@ j) ts' --- (VSigma a f,u) -> --- let (u1,u2) = (fstVal u,sndVal u) --- fill_u1 = transFill i a u1 --- ui1 = trans i a u1 --- comp_u2 = trans i (app f fill_u1) u2 --- in VPair ui1 comp_u2 --- (VPi{},_) -> VTrans (VPath i v0) v1 --- (Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of --- Just as -> VCon c $ transps i as env us --- Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0 --- (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of --- -- v1 should be independent of i, so i # phi --- Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis --- Nothing -> error $ "trans: missing path constructor " ++ c ++ --- " in " ++ show v0 --- _ | isNeutral w -> w --- where w = VTrans (VPath i v0) v1 --- (Ter (Sum _ _ nass) env,VElimComp _ _ u) -> trans i v0 u --- (Ter (Sum _ _ nass) env,VCompElem _ _ u _) -> trans i v0 u --- (VGlue a ts,_) -> transGlue i a ts v1 --- (VGlueLine a phi psi,_) -> transGlueLine i a phi psi v1 --- (VComp VU a es,_) -> transU i a es 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 --- _ -> error $ "trans not implemented for v0 = " ++ show v0 --- ++ "\n and v1 = " ++ show v1 transNeg :: Name -> Val -> Val -> Val transNeg i a u = trans i (a `sym` i) u @@ -398,7 +309,6 @@ squeezeFill i a u = fill i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] where j = fresh (Atom i,a,u) ui1 = u `face` (i ~> 1) - squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] squeezes i [] _ [] = [] squeezes i ((x,a):as) e (u:us) = @@ -408,16 +318,6 @@ squeezes i ((x,a):as) e (u:us) = in vi1 : vs squeezes _ _ _ _ = error "squeezes: different lengths of types and values" --- squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] --- squeezes i xas rho us = comps i xas (rho `disj` (i,j)) --- squeezes i [] _ [] = [] --- squeezes i ((x,a):as) e (u:us) = --- let v = squeeze i (eval e a) u --- vs = squeezes i as (upd (x,v) e) us --- in v : vs --- squeezes _ _ _ _ = error "squeezes: different lengths of types and values" - - -- squeezeNeg :: Name -> Val -> Val -> Val -- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u -- where j = fresh (Atom i,a,u) @@ -429,13 +329,6 @@ compLine :: Val -> Val -> System Val -> Val compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts) where i = fresh (a,u,ts) --- genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val --- genComp i a u ts | Map.null ts = trans i a u --- genComp i a u ts = comp i ai1 (trans i a u) ts' --- where ai1 = a `face` (i ~> 1) --- ts' = mapWithKey (\alpha -> squeeze i (a `face` alpha)) ts --- genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i) - fillLine :: Val -> Val -> System Val -> Val fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts) where i = fresh (a,u,ts) @@ -446,11 +339,6 @@ fill i a u ts = where j = fresh (Atom i,a,u,ts) fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i --- genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val --- genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j)) --- where j = fresh (Atom i,a,u,ts) --- genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i - comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] comps i [] _ [] = [] comps i ((x,a):as) e ((ts,u):tsus) = @@ -474,10 +362,9 @@ comp i a u ts = case a of comp_u2 = comp i (app f fill_u1) u2 t2s VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) VU -> compUniv u (Map.map (VPath i) ts) - -- VGlue u (Map.map (eqToIso i) ts) + -- VGlue u (Map.map (eqToIso i) ts) VCompU a es -> compU i a es u ts VGlue b hisos -> compGlue i b hisos u ts - -- VGlueLine b phi psi -> compGlueLine i b phi psi u ts Ter (Sum _ _ nass) env -> case u of VCon n us -> case lookupLabel n nass of Just as -> @@ -489,7 +376,6 @@ comp i a u ts = case a of _ -> error $ "comp ter sum" ++ show u Ter (HSum _ _ nass) env -> compHIT i a u ts _ -> VComp (VPath i a) u (Map.map (VPath i) ts) - -- _ -> error $ "comp: case missing for " ++ show i ++ " " ++ show a ++ " " ++ show u ++ " " ++ showSystem ts compNeg :: Name -> Val -> Val -> System Val -> Val compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) @@ -525,7 +411,7 @@ squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of Just as -> VCon n (squeezes i as env us) Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n VPCon c _ ws0 phis -> case lookupLabel c nass of - Just as -> VPCon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis + Just as -> pcon c (a `face` (i ~> 1)) (squeezes i as env ws0) (phis `face` (i ~> 1)) Nothing -> error $ "squeezeHIT: missing path constructor " ++ c VHComp _ v vs -> hComp (a `face` (i ~> 1)) (transpHIT i a v) $ @@ -535,7 +421,7 @@ squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of hComp :: Val -> Val -> System Val -> Val hComp a u us | eps `Map.member` us = (us ! eps) @@ One - | otherwise = VHComp a u us + | otherwise = VHComp a u us ------------------------------------------------------------------------------- -- | Glue @@ -576,50 +462,8 @@ unGlue w b hisos | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w | otherwise = case w of VGlueElem v us -> v - -- VElimComp _ _ v -> unGlue hisos v - -- VCompElem a es v vs -> unGlue hisos v _ -> VUnGlueElem w b hisos --- transGlue :: Name -> Val -> System Val -> Val -> Val --- transGlue i b hisos wi0 = glueElem vi1'' usi1 --- where vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) - --- vi1 = trans i b vi0 -- in b(i1) - --- hisosI1 = hisos `face` (i ~> 1) --- hisos'' = --- filterWithKey (\alpha _ -> alpha `Map.notMember` hisos) hisosI1 - --- -- set of elements in hisos independent of i --- hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos - --- us' = mapWithKey (\gamma isoG -> --- transFill i (hisoDom isoG) (wi0 `face` gamma)) --- hisos' --- usi1' = mapWithKey (\gamma isoG -> --- trans i (hisoDom isoG) (wi0 `face` gamma)) --- hisos' - --- ls' = mapWithKey (\gamma isoG -> --- VPath i $ squeeze i (b `face` gamma) --- (hisoFun isoG `app` (us' ! gamma))) --- hisos' --- bi1 = b `face` (i ~> 1) --- vi1' = compLine bi1 vi1 ls' - --- uls'' = mapWithKey (\gamma isoG -> --- gradLemma (bi1 `face` gamma) isoG (usi1' `face` gamma) --- (vi1' `face` gamma)) --- hisos'' - --- vi1'' = compLine bi1 vi1' (Map.map snd uls'') - --- usi1 = mapWithKey (\gamma _ -> --- if gamma `Map.member` usi1' --- then usi1' ! gamma --- else fst (uls'' ! gamma)) --- hisosI1 - compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) @@ -634,8 +478,7 @@ compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' hisosI1 = hisos `face` (i ~> 1) hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos - -- hisos'' = filterWithKey (\alpha _ -> not (alpha `Map.member` hisos)) hisosI1 - hisos'' = filterWithKey (\alpha _ -> not (alpha `Map.member` hisos')) hisosI1 + hisos'' = filterWithKey (\alpha _ -> alpha `Map.notMember` hisos') hisosI1 us' = mapWithKey (\gamma isoG -> fill i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma)) @@ -673,8 +516,6 @@ compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' hisosI1 - - -- assumes u and u' : A are solutions of us + (i0 -> u(i0)) -- The output is an L-path in A(i1) between u(i1) and u'(i1) pathComp :: Name -> Val -> Val -> Val -> System Val -> Val @@ -682,14 +523,13 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us' where j = fresh (Atom i,a,us,u,u') us' = insertsSystem [(j ~> 0, u), (j ~> 1, u')] us - -- Grad Lemma, takes an iso f, a system us and a value v, s.t. f us = -- border v. Outputs (u,p) s.t. border u = us and a path p between v -- and f u. gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val) gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = (u, VPath i theta'') - where i:j:_ = freshs (hiso,us,v) + where i:j:_ = freshs (b,hiso,us,v) us' = mapWithKey (\alpha uAlpha -> app (t `face` alpha) uAlpha @@ i) us gv = app g v @@ -709,118 +549,6 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = theta'' = comp j b (app f theta') xs -------------------------------------------------------------------------------- --- | GlueLine - - --- glueLine :: Val -> Formula -> Formula -> Val --- glueLine t _ (Dir Zero) = t --- glueLine t (Dir _) _ = t --- glueLine t phi (Dir One) = glue t isos --- where isos = mkSystem (map (\alpha -> (alpha,idIso (t `face` alpha))) --- (invFormula phi Zero)) --- glueLine t phi psi = VGlueLine t phi psi - --- idIso :: Val -> Val --- idIso a = VPair a $ VPair idV $ VPair idV $ VPair refl refl --- where idV = Ter (Lam "x" (Var "A") (Var "x")) (upd ("A",a) empty) --- refl = Ter (Lam "x" (Var "A") (Path (Name "i") (Var "x"))) --- (upd ("A",a) empty) - --- glueLineElem :: Val -> Formula -> Formula -> Val --- glueLineElem u (Dir _) _ = u --- glueLineElem u _ (Dir Zero) = u --- glueLineElem u phi (Dir One) = glueElem u ss --- where ss = mkSystem (map (\alpha -> (alpha,u `face` alpha)) --- (invFormula phi Zero)) --- glueLineElem u phi psi = VGlueLineElem u phi psi - --- unGlueLine :: Val -> Formula -> Formula -> Val -> Val --- unGlueLine b phi psi u = case (phi,psi,u) of --- (Dir _,_,_) -> u --- (_,Dir Zero,_) -> u --- (_,Dir One,_) -> --- let isos = mkSystem (map (\alpha -> (alpha,idIso (b `face` alpha))) --- (invFormula phi Zero)) --- in unGlue isos u --- (_,_,VGlueLineElem w _ _ ) -> w --- (_,_,_) -> error ("UnGlueLine, should be VGlueLineElem " ++ show u) - --- compGlueLine :: Name -> Val -> Formula -> Formula -> Val -> System Val -> Val --- compGlueLine i b phi psi u us = glueLineElem vm phi psi --- where fs = invFormula psi One --- ws = mapWithKey --- (\alpha -> unGlueLine (b `face` alpha) --- (phi `face` alpha) (psi `face` alpha)) us --- w = unGlueLine b phi psi u --- v = comp i b w ws - --- lss = mkSystem $ map --- (\alpha -> --- (alpha,(phi `face` alpha,b `face` alpha, --- us `face` alpha,u `face` alpha))) fs --- ls = mapWithKey (\alpha vAlpha -> --- auxGlueLine i vAlpha (v `face` alpha)) lss - --- vm = compLine b v ls - --- auxGlueLine :: Name -> (Formula,Val,System Val,Val) -> Val -> Val --- auxGlueLine i (Dir _,b,ws,wi0) vi1 = VPath j vi1 where j = fresh vi1 --- auxGlueLine i (phi,b,ws,wi0) vi1 = fillLine b vi1 ls' --- where hisos = mkSystem (map (\alpha -> --- (alpha,idIso (b `face` alpha))) (invFormula phi Zero)) --- vs = mapWithKey (\alpha -> unGlue (hisos `face` alpha)) ws --- vi0 = unGlue hisos wi0 -- in b - --- v = fill i b vi0 vs -- in b --- us' = mapWithKey (\gamma _ -> --- fill i (b `face` gamma) (wi0 `face` gamma) --- (ws `face` gamma)) --- hisos - --- ls' = mapWithKey (\gamma _ -> --- pathComp i (b `face` gamma) (v `face` gamma) --- (us' ! gamma) (vs `face` gamma)) --- hisos - --- transGlueLine :: Name -> Val -> Formula -> Formula -> Val -> Val --- transGlueLine i b phi psi u = glueLineElem vm phii1 psii1 --- where fs = filter (i `Map.notMember`) (invFormula psi One) --- phii1 = phi `face` (i ~> 1) --- psii1 = psi `face` (i ~> 1) --- phii0 = phi `face` (i ~> 0) --- psii0 = psi `face` (i ~> 0) --- bi1 = b `face` (i ~> 1) --- bi0 = b `face` (i ~> 0) --- lss = mkSystem (map (\ alpha -> --- (alpha,(face phi alpha,face b alpha,face u alpha))) fs) --- ls = mapWithKey (\alpha vAlpha -> --- auxTransGlueLine i vAlpha (v `face` alpha)) lss --- v = trans i b w --- w = unGlueLine bi0 phii0 psii0 u --- vm = compLine bi1 v ls - --- auxTransGlueLine :: Name -> (Formula,Val,Val) -> Val -> Val --- auxTransGlueLine i (Dir _,b,wi0) vi1 = VPath j vi1 where j = fresh vi1 --- auxTransGlueLine i (phi,b,wi0) vi1 = fillLine (b `face` (i ~> 1)) vi1 ls' --- where hisos = mkSystem (map (\ alpha -> --- (alpha,idIso (b `face` alpha))) (invFormula phi Zero)) --- vi0 = unGlue (hisos `face` (i ~> 0)) wi0 -- in b(i0) --- v = transFill i b vi0 -- in b - --- -- set of elements in hisos independent of i --- hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos - --- us' = mapWithKey (\gamma _ -> --- transFill i (b `face` gamma) (wi0 `face` gamma)) --- hisos' - --- ls' = mapWithKey (\gamma _ -> --- VPath i $ squeeze i (b `face` gamma) (us' ! gamma)) --- hisos' - - - ------------------------------------------------------------------------------- -- | Composition in the Universe (to be replaced as glue) @@ -851,7 +579,6 @@ compU i b es wi0 ws = glueElem vi1'' usi1'' esI1 = es `face` (i ~> 1) es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es - -- es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es)) esI1 es'' = filterWithKey (\alpha _ -> not (alpha `Map.member` es')) esI1 us' = mapWithKey (\gamma eGamma -> @@ -891,13 +618,12 @@ compU i b es wi0 ws = glueElem vi1'' usi1'' esI1 - -- Grad Lemma, takes a line eq in U, a system us and a value v, s.t. f us = -- border v. Outputs (u,p) s.t. border u = us and a path p between v -- and f u, where f is transNegLine eq gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) gradLemmaU b eq us v = (u, VPath i theta'') - where i:j:_ = freshs (eq,us,v) + where i:j:_ = freshs (b,eq,us,v) a = eq @@ One g = transLine f = transNegLine @@ -927,153 +653,17 @@ gradLemmaU b eq us v = (u, VPath i theta'') s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us theta'' = comp j b (f eq theta') xs - --- isConstPath :: Val -> Bool --- isConstPath (VPath i u) = i `notElem` support u --- isConstPath _ = False - --- compElem :: Val -> System Val -> Val -> System Val -> Val --- compElem a es u us = compElem' (Map.filter (not . isConstPath) es) --- where compElem' es | Map.null es = u --- | eps `Map.member` us = us ! eps --- | otherwise = VCompElem a es u us - --- elimComp :: Val -> System Val -> Val -> Val --- elimComp a es u = elimComp' (Map.filter (not . isConstPath) es) --- where elimComp' es | Map.null es = u --- | eps `Map.member` es = transNegLine (es ! eps) u --- | otherwise = VElimComp a es u - --- compU :: Name -> Val -> System Val -> Val -> System Val -> Val --- compU i a es w0 ws = --- let vs = mapWithKey --- (\alpha -> elimComp (a `face` alpha) (es `face` alpha)) ws --- v0 = elimComp a es w0 -- in a --- v1 = comp i a v0 vs -- in a - --- us1' = mapWithKey (\gamma eGamma -> --- comp i (eGamma @@ One) (w0 `face` gamma) --- (ws `face` gamma)) es --- ls' = mapWithKey --- (\gamma eGamma -> pathUniv i eGamma --- (ws `face` gamma) (w0 `face` gamma)) --- es - --- v1' = compLine a v1 ls' --- in compElem a es v1' us1' - --- -- Computes a homotopy between the image of the composition, and the --- -- composition of the image. Given e (an equality in U), an L-system --- -- us (in e0) and ui0 (in e0 (i0)) The output is an L(i1)-path in --- -- e1(i1) between vi1 and sigma (i1) ui1 where --- -- sigma = appEq --- -- ui1 = comp i (e 0) us ui0 --- -- vi1 = comp i (e 1) (sigma us) (sigma(i0) ui0) --- -- Moreover, if e is constant, so is the output. --- pathUniv :: Name -> Val -> System Val -> Val -> Val --- pathUniv i e us ui0 = VPath k xi1 --- where j:k:_ = freshs (Atom i,e,us,ui0) --- ej = e @@ j --- ui1 = comp i (e @@ One) ui0 us --- ws = mapWithKey (\alpha uAlpha -> --- transFillNeg j (ej `face` alpha) uAlpha) --- us --- wi0 = transFillNeg j (ej `face` (i ~> 0)) ui0 --- wi1 = comp i ej wi0 ws --- wi1' = transFillNeg j (ej `face` (i ~> 1)) ui1 --- xi1 = compNeg j (ej `face` (i ~> 1)) ui1 --- (mkSystem [(k ~> 1, wi1'), (k ~> 0, wi1)]) - --- transU :: Name -> Val -> System Val -> Val -> Val --- transU i a es wi0 = --- let vi0 = elimComp (a `face` (i ~> 0)) (es `face` (i ~> 0)) wi0 -- in a(i0) --- vi1 = trans i a vi0 -- in a(i1) - --- ai1 = a `face` (i ~> 1) --- esi1 = es `face` (i ~> 1) - --- -- gamma in es'' iff i not in the domain of gamma and (i1)gamma in es --- es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esi1 - --- -- set of faces alpha of es such i is not the domain of alpha --- es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es - --- usi1' = mapWithKey (\gamma eGamma -> --- trans i (eGamma @@ One) (wi0 `face` gamma)) es' - --- ls' = mapWithKey (\gamma _ -> --- pathUnivTrans i (es `proj` gamma) (wi0 `face` gamma)) --- -- pathUniv i (es `proj` gamma) Map.empty (wi0 `face` gamma)) --- es' - --- vi1' = compLine ai1 vi1 ls' - --- uls'' = mapWithKey (\gamma _ -> -- Should be !, not proj ? --- eqLemma (es ! (gamma `meet` (i ~> 1))) --- (usi1' `face` gamma) (vi1' `face` gamma)) es'' - --- vi1'' = compLine ai1 vi1' (Map.map snd uls'') - --- usi1 = mapWithKey (\gamma _ -> --- if gamma `Map.member` usi1' then usi1' ! gamma --- else fst (uls'' ! gamma)) esi1 --- in compElem ai1 esi1 vi1'' usi1 - - --- pathUnivTrans :: Name -> Val -> Val -> Val --- pathUnivTrans i e ui0 = VPath j xi1 --- where j = fresh (Atom i,e,ui0) --- ej = e @@ j --- wi0 = transFillNeg j (ej `face` (i ~> 0)) ui0 --- wi1 = trans i ej wi0 --- xi1 = squeezeNeg j (ej `face` (i ~> 1)) wi1 - --- -- Any equality defines an equivalence. --- eqLemma :: Val -> System Val -> Val -> (Val, Val) --- eqLemma e ts a = (t,VPath j theta'') --- where i:j:_ = freshs (e,ts,a) --- ei = e @@ i --- vs = mapWithKey (\alpha uAlpha -> --- transFillNeg i (ei `face` alpha) uAlpha) ts --- theta = fill i ei a vs --- t = comp i ei a vs --- theta' = transFillNeg i ei t --- ws = insertSystem (j ~> 1) theta' $ insertSystem (j ~> 0) theta vs --- theta'' = compNeg i ei t ws - - ------------------------------------------------------------------------------- -- | Conversion class Convertible a where conv :: [String] -> a -> a -> Bool --- isIndep :: (Nominal a, Convertible a) => [String] -> Name -> a -> Bool --- isIndep ns i u = conv ns u (u `face` (i ~> 0)) - isCompSystem :: (Nominal a, Convertible a) => [String] -> System a -> Bool isCompSystem ns ts = and [ conv ns (getFace alpha beta) (getFace beta alpha) | (alpha,beta) <- allCompatible (keys ts) ] where getFace a b = face (ts ! a) (b `minus` a) --- simplify :: [String] -> Name -> Val -> Val --- simplify ns j v = case v of --- VTrans p u | isIndep ns j (p @@ j) -> simplify ns j u --- VComp a u ts -> --- let (indep,ts') = Map.partition (\t -> isIndep ns j (t @@ j)) ts --- in if Map.null ts' then simplify ns j u else VComp a u ts' --- VCompElem a es u us -> --- let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es --- us' = intersection us es' --- in if Map.null es' then simplify ns j u else VCompElem a es' u us' --- VElimComp a es u -> --- let (indep,es') = Map.partition (\e -> isIndep ns j (e @@ j)) es --- u' = simplify ns j u --- in if Map.null es' then u' else case u' of --- VCompElem _ _ w _ -> simplify ns j w --- _ -> VElimComp a es' u' --- _ -> v - instance Convertible Val where conv ns u v | u == v = True | otherwise = @@ -1115,16 +705,12 @@ instance Convertible Val where (VPath i a,VPath i' a') -> conv ns (a `swap` (i,j)) (a' `swap` (i',j)) (VPath i a,p') -> conv ns (a `swap` (i,j)) (p' @@ j) (p,VPath i' a') -> conv ns (p @@ j) (a' `swap` (i',j)) - -- (VTrans p u,VTrans p' u') -> conv ns p p' && conv ns u u' (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x') (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u' (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' - -- (VCompElem a es u us,VCompElem a' es' u' us') -> - -- conv ns (a,es,u,us) (a',es',u',us') - -- (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u') _ -> False instance Convertible Ctxt where @@ -1177,14 +763,11 @@ instance Normal Val where VIdP a u0 u1 -> VIdP (normal ns a) (normal ns u0) (normal ns u1) VPath i u -> VPath i (normal ns u) VComp u v vs -> compLine (normal ns u) (normal ns v) (normal ns vs) - -- VTrans u v -> transLine (normal ns u) (normal ns v) VGlue u hisos -> glue (normal ns u) (normal ns hisos) VGlueElem u us -> glueElem (normal ns u) (normal ns us) VUnGlueElem u b hs -> unGlue (normal ns u) (normal ns b) (normal ns hs) VUnGlueElemU u b es -> unGlueU (normal ns u) (normal ns b) (normal ns es) VCompU u es -> compUniv (normal ns u) (normal ns es) - -- VCompElem a es u us -> compElem (normal ns a) (normal ns es) (normal ns u) (normal ns us) - -- VElimComp a es u -> elimComp (normal ns a) (normal ns es) (normal ns u) VVar x t -> VVar x t -- (normal ns t) VFst t -> fstVal (normal ns t) VSnd t -> sndVal (normal ns t) diff --git a/TypeChecker.hs b/TypeChecker.hs index c7bea5f..c94f8ab 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -372,7 +372,7 @@ checkPathSystem t0 va ps = do rhoAlpha <- asks env (a0,a1) <- checkPath (va `face` alpha) pAlpha unlessM (a0 === eval rhoAlpha t0) $ - throwError $ "Incompatible system with " ++ show t0 + throwError $ "Incompatible system " ++ showSystem ps ++ " with " ++ show t0 return a1) ps checkCompSystem (evalSystem rho ps) return v -- 2.34.1