From 8c24f2ae3691104a9812830457abe4e6ee65078b Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 18 Jun 2015 16:25:59 +0200 Subject: [PATCH] Make more names unqualified when importing Map and reorganization+cleaning --- CTT.hs | 8 +- Connections.hs | 46 ++++--- Eval.hs | 354 +++++++++++++++++++++++++------------------------ TypeChecker.hs | 6 +- 4 files changed, 213 insertions(+), 201 deletions(-) diff --git a/CTT.hs b/CTT.hs index 55e6af8..d58f206 100644 --- a/CTT.hs +++ b/CTT.hs @@ -4,7 +4,7 @@ module CTT where import Control.Applicative import Data.List import Data.Maybe -import Data.Map (Map,(!),filterWithKey) +import Data.Map (Map,(!),filterWithKey,elems) import qualified Data.Map as Map import Text.PrettyPrint as PP @@ -175,7 +175,7 @@ isNeutral v = case v of _ -> False isNeutralSystem :: System Val -> Bool -isNeutralSystem = any isNeutral . Map.elems +isNeutralSystem = any isNeutral . elems -- isNeutralPath :: Val -> Bool -- isNeutralPath (VPath _ v) = isNeutral v @@ -215,8 +215,8 @@ data Ctxt = Empty -- only need to affect the lists and not the whole context. type Env = (Ctxt,[Val],[Formula]) -empty :: Env -empty = (Empty,[],[]) +emptyEnv :: Env +emptyEnv = (Empty,[],[]) def :: [Decl] -> Env -> Env def ds (rho,vs,fs) = (Def ds rho,vs,fs) diff --git a/Connections.hs b/Connections.hs index 382db2b..59aaee4 100644 --- a/Connections.hs +++ b/Connections.hs @@ -4,7 +4,9 @@ module Connections where import Control.Applicative import Data.List -import Data.Map (Map,(!),keys) +import Data.Map (Map,(!),keys,fromList,toList,mapKeys,elems,intersectionWith + ,unionWith,singleton,foldWithKey,assocs,mapWithKey + ,filterWithKey,member) import Data.Set (Set,isProperSubsetOf) import qualified Data.Map as Map import qualified Data.Set as Set @@ -58,18 +60,18 @@ instance Arbitrary Dir where type Face = Map Name Dir instance Arbitrary Face where - arbitrary = Map.fromList <$> arbitrary + arbitrary = fromList <$> arbitrary showFace :: Face -> String showFace alpha = concat [ "(" ++ show i ++ " = " ++ show d ++ ")" - | (i,d) <- Map.toList alpha ] + | (i,d) <- toList alpha ] swapFace :: Face -> (Name,Name) -> Face -swapFace alpha ij = Map.mapKeys (`swapName` ij) alpha +swapFace alpha ij = mapKeys (`swapName` ij) alpha -- Check if two faces are compatible compatible :: Face -> Face -> Bool -compatible xs ys = and (Map.elems (Map.intersectionWith (==) xs ys)) +compatible xs ys = and (elems (intersectionWith (==) xs ys)) compatibles :: [Face] -> Bool compatibles [] = True @@ -81,7 +83,7 @@ allCompatible (f:fs) = map (f,) (filter (compatible f) fs) ++ allCompatible fs -- Partial composition operation meet :: Face -> Face -> Face -meet = Map.unionWith f +meet = unionWith f where f d1 d2 = if d1 == d2 then d1 else error "meet: incompatible faces" meetMaybe :: Face -> Face -> Maybe Face @@ -114,7 +116,7 @@ incomparables [] = True incomparables (x:xs) = all (not . (x `comparable`)) xs && incomparables xs (~>) :: Name -> Dir -> Face -i ~> d = Map.singleton i d +i ~> d = singleton i d eps :: Face eps = Map.empty @@ -235,8 +237,8 @@ merge a b = -- phi b = max {alpha : Face | phi alpha = b} invFormula :: Formula -> Dir -> [Face] invFormula (Dir b') b = [ eps | b == b' ] -invFormula (Atom i) b = [ Map.singleton i b ] -invFormula (NegAtom i) b = [ Map.singleton i (- b) ] +invFormula (Atom i) b = [ singleton i b ] +invFormula (NegAtom i) b = [ singleton i (- b) ] invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0 invFormula (phi :/\: psi) One = meets (invFormula phi 1) (invFormula psi 1) invFormula (phi :\/: psi) b = invFormula (negFormula phi :/\: negFormula psi) (- b) @@ -362,7 +364,7 @@ instance Nominal Formula where swap (psi1 :\/: psi2) (i,j) = swap psi1 (i,j) :\/: swap psi2 (i,j) face :: Nominal a => a -> Face -> a -face = Map.foldWithKey (\i d a -> act a (i,Dir d)) +face = foldWithKey (\i d a -> act a (i,Dir d)) -- the faces should be incomparable type System a = Map Face a @@ -374,10 +376,10 @@ showListSystem ts = | (alpha,u) <- ts ] ++ " ]" showSystem :: Show a => System a -> String -showSystem = showListSystem . Map.toList +showSystem = showListSystem . toList insertSystem :: Face -> a -> System a -> System a -insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of +insertSystem alpha v ts = case find (comparable alpha) (keys ts) of Just beta | alpha `leq` beta -> ts | otherwise -> Map.insert alpha v (Map.delete beta ts) Nothing -> Map.insert alpha v ts @@ -389,7 +391,7 @@ mkSystem :: [(Face, a)] -> System a mkSystem = flip insertsSystem Map.empty unionSystem :: System a -> System a -> System a -unionSystem us vs = insertsSystem (Map.assocs us) vs +unionSystem us vs = insertsSystem (assocs us) vs -- TODO: add some checks @@ -403,10 +405,10 @@ transposeSystemAndList tss (u:us) = -- Now we ensure that the keys are incomparable instance Nominal a => Nominal (System a) where - support s = unions (map Map.keys $ Map.keys s) - `union` support (Map.elems s) + support s = unions (map keys $ keys s) + `union` support (elems s) - act s (i, phi) = addAssocs (Map.assocs s) + act s (i, phi) = addAssocs (assocs s) where addAssocs [] = Map.empty addAssocs ((alpha,u):alphaus) = @@ -418,11 +420,11 @@ instance Nominal a => Nominal (System a) where s' (invFormula (face phi beta) d) Nothing -> insertSystem alpha (act u (i,face phi alpha)) s' - swap s ij = Map.mapKeys (`swapFace` ij) (Map.map (`swap` ij) s) + swap s ij = mapKeys (`swapFace` ij) (Map.map (`swap` ij) s) -- carve a using the same shape as the system b border :: Nominal a => a -> System b -> System a -border v = Map.mapWithKey (const . face v) +border v = mapWithKey (const . face v) shape :: System a -> System () shape = border () @@ -435,7 +437,7 @@ instance (Nominal a, Arbitrary a) => Arbitrary (System a) where arbitraryShape :: [Name] -> Gen (System ()) arbitraryShape supp = do phi <- sized $ arbFormula supp - return $ Map.fromList [(face,()) | face <- invFormula phi 0] + return $ fromList [(face,()) | face <- invFormula phi 0] sym :: Nominal a => a -> Name -> a sym a i = a `act` (i, NegAtom i) @@ -449,12 +451,12 @@ disj a (i, j) = a `act` (i, Atom i :\/: Atom j) leqSystem :: Face -> System a -> Bool alpha `leqSystem` us = - not $ Map.null $ Map.filterWithKey (\beta _ -> alpha `leq` beta) us + not $ Map.null $ filterWithKey (\beta _ -> alpha `leq` beta) us -- assumes alpha <= shape us proj :: (Nominal a, Show a) => System a -> Face -> a -proj us alpha | eps `Map.member` usalpha = usalpha ! eps - | otherwise = +proj us alpha | eps `member` usalpha = usalpha ! eps + | otherwise = error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the " ++ show alpha ++ "\nface of " ++ show us where usalpha = us `face` alpha diff --git a/Eval.hs b/Eval.hs index 501df76..444bba3 100644 --- a/Eval.hs +++ b/Eval.hs @@ -4,12 +4,15 @@ module Eval where import Data.List import Data.Maybe (fromMaybe) import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey - ,elems,intersectionWith,intersection,keys) + ,elems,intersectionWith,intersection,keys + ,member,notMember,empty) import qualified Data.Map as Map import Connections import CTT +----------------------------------------------------------------------- +-- Lookup functions look :: String -> Env -> Val look x (Upd y rho,v:vs,fs) | x == y = v @@ -18,6 +21,7 @@ look x r@(Def decls rho,vs,fs) = case lookup x decls of Just (_,t) -> eval r t Nothing -> look x (rho,vs,fs) look x (Sub _ rho,vs,_:fs) = look x (rho,vs,fs) +look x _ = error $ "look: not found " ++ show x lookType :: String -> Env -> Val lookType x (Upd y rho,VVar _ a:vs,fs) @@ -27,13 +31,15 @@ lookType x r@(Def decls rho,vs,fs) = case lookup x decls of Just (a,_) -> eval r a Nothing -> lookType x (rho,vs,fs) lookType x (Sub _ rho,vs,_:fs) = lookType x (rho,vs,fs) +lookType x _ = error $ "lookType: not found " ++ show x lookName :: Name -> Env -> Formula --- lookName i Empty = error $ "lookName: not found " ++ show i lookName i (Upd _ rho,v:vs,fs) = lookName i (rho,vs,fs) -lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs) +lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs) lookName i (Sub j rho,vs,phi:fs) | i == j = phi | otherwise = lookName i (rho,vs,fs) +lookName i _ = error $ "lookName: not found " ++ show i + ----------------------------------------------------------------------- -- Nominal instances @@ -150,9 +156,8 @@ eval rho v = case v of Undef{} -> Ter v rho Hole{} -> Ter v rho IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) - Path i t -> - let j = fresh rho - in VPath j (eval (sub (i,Atom j) rho) t) + Path i t -> let j = fresh rho + in VPath j (eval (sub (i,Atom j) rho) t) AppFormula e phi -> eval rho e @@ evalFormula rho phi Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts) Fill a t0 ts -> fillLine (eval rho a) (eval rho t0) (evalSystem rho ts) @@ -160,6 +165,9 @@ eval rho v = case v of GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) _ -> error $ "Cannot evaluate " ++ show v +evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] +evals env bts = [ (b,eval env t) | (b,t) <- bts ] + evalFormula :: Env -> Formula -> Formula evalFormula rho phi = case phi of Atom i -> lookName i rho @@ -168,9 +176,6 @@ evalFormula rho phi = case phi of phi1 :\/: phi2 -> evalFormula rho phi1 `orFormula` evalFormula rho phi2 _ -> phi -evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] -evals env bts = [ (b,eval env t) | (b,t) <- bts ] - evalSystem :: Env -> System Ter -> System Val evalSystem rho ts = let out = concat [ let betas = meetss [ invFormula (lookName i rho) d @@ -254,17 +259,79 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of _ -> VAppFormula v (toFormula phi) v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." -pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val -pcon c a@(Ter (HSum _ _ lbls) rho) us phis = case lookupPLabel c lbls of - Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps - | otherwise -> VPCon c a us phis - 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 + +------------------------------------------------------------------------------- +-- Composition and filling + +comp :: Name -> Val -> Val -> System Val -> Val +comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1) +comp i a u ts = case a of + VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts) + in VPath j $ comp i (p @@ j) (u @@ j) $ + insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts) + VSigma a f -> VPair ui1 comp_u2 + where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts) + (u1, u2) = (fstVal u, sndVal u) + fill_u1 = fill i a u1 t1s + ui1 = comp i a u1 t1s + comp_u2 = comp i (app f fill_u1) u2 t2s + VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) + VU -> glue u (Map.map (eqToEquiv . VPath i) ts) + VGlue b equivs -> compGlue i b equivs u ts + Ter (Sum _ _ nass) env -> case u of + VCon n us | all isCon (elems ts) -> case lookupLabel n nass of + Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us + in VCon n $ comps i as env tsus + Nothing -> error $ "comp: missing constructor in labelled sum " ++ n + _ -> VComp (VPath i a) u (Map.map (VPath i) ts) + Ter (HSum _ _ nass) env -> compHIT i a u ts + _ -> VComp (VPath i a) u (Map.map (VPath i) ts) + +compNeg :: Name -> Val -> Val -> System Val -> Val +compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) + +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) + +comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] +comps i [] _ [] = [] +comps i ((x,a):as) e ((ts,u):tsus) = + let v = fill i (eval e a) u ts + vi1 = comp i (eval e a) u ts + vs = comps i as (upd (x,v) e) tsus + in vi1 : vs +comps _ _ _ _ = error "comps: different lengths of types and values" + +fill :: Name -> Val -> Val -> System Val -> Val +fill i a u ts = + comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j))) + where j = fresh (Atom i,a,u,ts) + +fillNeg :: Name -> Val -> Val -> System Val -> Val +fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `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) + +-- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] +-- fills i [] _ [] = [] +-- fills i ((x,a):as) e ((ts,u):tsus) = +-- let v = fill i (eval e a) ts u +-- vs = fills i as (Upd e (x,v)) tsus +-- in v : vs +-- fills _ _ _ _ = error "fills: different lengths of types and values" + ----------------------------------------------------------- --- Transport +-- Transport and squeeze (defined using comp) + +trans :: Name -> Val -> Val -> Val +trans i v0 v1 = comp i v0 v1 empty + +transNeg :: Name -> Val -> Val -> Val +transNeg i a u = trans i (a `sym` i) u transLine :: Val -> Val -> Val transLine u v = trans i (u @@ i) v @@ -274,16 +341,6 @@ transNegLine :: Val -> Val -> Val transNegLine u v = transNeg i (u @@ i) v where i = fresh (u,v) -trans :: Name -> Val -> Val -> Val -trans i v0 v1 = comp i v0 v1 Map.empty - -transNeg :: Name -> Val -> Val -> Val -transNeg i a u = trans i (a `sym` i) u - -transFill, transFillNeg :: Name -> Val -> Val -> Val -transFill i a u = fill i a u Map.empty -transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i - transps :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] transps i [] _ [] = [] transps i ((x,a):as) e (u:us) = @@ -293,16 +350,22 @@ transps i ((x,a):as) e (u:us) = in vi1 : vs transps _ _ _ _ = error "transps: different lengths of types and values" +transFill :: Name -> Val -> Val -> Val +transFill i a u = fill i a u empty + +transFillNeg :: Name -> Val -> Val -> Val +transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i + -- Given u of type a "squeeze i a u" connects in the direction i -- trans i a u(i=0) to u(i=1) squeeze :: Name -> Val -> Val -> Val squeeze i a u = comp i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] - where j = fresh (Atom i,a,u) + where j = fresh (Atom i,a,u) ui1 = u `face` (i ~> 1) squeezeFill :: Name -> Val -> Val -> Val squeezeFill i a u = fill i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] - where j = fresh (Atom i,a,u) + where j = fresh (Atom i,a,u) ui1 = u `face` (i ~> 1) squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] @@ -318,71 +381,18 @@ squeezes _ _ _ _ = error "squeezes: different lengths of types and values" -- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u -- where j = fresh (Atom i,a,u) -------------------------------------------------------------------------------- --- Composition - -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) - -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) - -fill :: Name -> Val -> Val -> System Val -> Val -fill i a u ts = - comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j))) - where j = fresh (Atom i,a,u,ts) - -fillNeg :: Name -> Val -> Val -> System Val -> Val -fillNeg i a u ts = (fill 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) = - let v = fill i (eval e a) u ts - vi1 = comp i (eval e a) u ts - vs = comps i as (upd (x,v) e) tsus - in vi1 : vs -comps _ _ _ _ = error "comps: different lengths of types and values" - -comp :: Name -> Val -> Val -> System Val -> Val -comp i a u ts | eps `Map.member` ts = (ts ! eps) `face` (i ~> 1) -comp i a u ts = case a of - VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts) - in VPath j $ comp i (p @@ j) (u @@ j) $ - insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts) - VSigma a f -> VPair ui1 comp_u2 - where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts) - (u1, u2) = (fstVal u, sndVal u) - fill_u1 = fill i a u1 t1s - ui1 = comp i a u1 t1s - comp_u2 = comp i (app f fill_u1) u2 t2s - VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts) - VU -> glue u (Map.map (eqToEquiv . VPath i) ts) - VGlue b equivs -> compGlue i b equivs u ts - Ter (Sum _ _ nass) env -> case u of - VCon n us | all isCon (elems ts) -> case lookupLabel n nass of - Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us - in VCon n $ comps i as env tsus - Nothing -> error $ "comp: missing constructor in labelled sum " ++ n - _ -> VComp (VPath i a) u (Map.map (VPath i) ts) - Ter (HSum _ _ nass) env -> compHIT i a u ts - _ -> VComp (VPath i a) u (Map.map (VPath i) ts) - -compNeg :: Name -> Val -> Val -> System Val -> Val -compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) - --- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] --- fills i [] _ [] = [] --- fills i ((x,a):as) e ((ts,u):tsus) = --- let v = fill i (eval e a) ts u --- vs = fills i as (Upd e (x,v)) tsus --- in v : vs --- fills _ _ _ _ = error "fills: different lengths of types and values" ------------------------------------------------------------------------------- --- | HIT +-- | HITs + +pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val +pcon c a@(Ter (HSum _ _ lbls) rho) us phis = case lookupPLabel c lbls of + Just (tele,is,ts) | eps `member` vs -> vs ! eps + | otherwise -> VPCon c a us phis + 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 compHIT :: Name -> Val -> Val -> System Val -> Val compHIT i a u us @@ -417,8 +427,9 @@ squeezeHIT i a@(Ter (HSum _ _ nass) env) u = _ -> error $ "squeezeHIT: neutral " ++ show u hComp :: Val -> Val -> System Val -> Val -hComp a u us | eps `Map.member` us = (us ! eps) @@ One - | otherwise = VHComp a u us +hComp a u us | eps `member` us = (us ! eps) @@ One + | otherwise = VHComp a u us + ------------------------------------------------------------------------------- -- | Glue @@ -429,6 +440,7 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One -- t : (y : b) (w : fiber a b f y) -> s y = w -- with fiber a b f y = (x : a) * (f x = y) +-- Extraction functions for getting a, f, s and t: equivDom :: Val -> Val equivDom = fstVal @@ -469,72 +481,27 @@ equivIsCenter = sndVal . sndVal . sndVal -- ,(j ~> 1, inv (edown x))] -- t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv --- Every path in the universe induces an equivalence -eqToEquiv :: Val -> Val -eqToEquiv e = VPair e1 (VPair f (VPair s t)) - where e1 = e @@ One - (i,j,x,y,w,ev) = (Name "i",Name "j",Var "x",Var "y",Var "w",Var "E") - inv t = Path i $ AppFormula t (NegAtom i) - evinv = inv ev - (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a) - eenv = upd ("E",e) empty - -- eplus : e0 -> e1 - eplus z = Comp ev z Map.empty - -- eminus : e1 -> e0 - eminus z = Comp evinv z Map.empty - -- NB: edown is *not* transNegFill - eup z = Fill ev z Map.empty - edown z = Fill evinv z Map.empty - f = Ter (Lam "x" ev1 (eminus x)) eenv - -- g = Ter (Lam "y" ev0 (eplus y)) eenv - etasys z0 = mkSystem [(j ~> 1, inv (eup z0)) - ,(j ~> 0, edown (eplus z0))] - -- eta : (y : e0) -> eminus (eplus y) = y - eta z0 = Path j $ Comp evinv (eplus z0) (etasys z0) - etaSquare z0 = Fill evinv (eplus z0) (etasys z0) - s = Ter (Lam "y" ev0 $ Pair (eplus y) (eta y)) eenv - (a,p) = (Fst w,Snd w) -- a : e1 and p : eminus a = y - phisys l = mkSystem [ (l ~> 0, inv (edown a)) - , (l ~> 1, eup y)] - psi l = Comp ev (AppFormula p (Atom l)) (phisys l) - phi l = Fill ev (AppFormula p (Atom l)) (phisys l) - tsys = mkSystem - [ (j ~> 0, edown (psi i)) - , (j ~> 1, inv $ eup y) - , (i ~> 0, inv $ phi j) - , (i ~> 1, etaSquare y) - ] - -- encode act on terms using Path and AppFormula - psi' formula = AppFormula (Path j $ psi j) formula - tprinc = psi' (Atom i :\/: Atom j) - t2 = Comp evinv tprinc tsys - t2inv = AppFormula (inv (Path i t2)) (Atom i) - fibtype = Sigma (Lam "x" ev1 $ IdP (Path (Name "_") ev0) (eminus x) y) - t = Ter (Lam "y" ev0 $ Lam "w" fibtype $ Path i $ - Pair (psi' (NegAtom i)) (Path j t2inv)) eenv - - glue :: Val -> System Val -> Val -glue b ts | eps `Map.member` ts = equivDom (ts ! eps) - | otherwise = VGlue b ts +glue b ts | eps `member` ts = equivDom (ts ! eps) + | otherwise = VGlue b ts glueElem :: Val -> System Val -> Val -glueElem v us | eps `Map.member` us = us ! eps - | otherwise = VGlueElem v us +glueElem v us | eps `member` us = us ! eps + | otherwise = VGlueElem v us unGlue :: Val -> Val -> System Val -> Val unGlue w b equivs - | eps `Map.member` equivs = app (equivFun (equivs ! eps)) w - | otherwise = case w of - VGlueElem v us -> v - _ -> VUnGlueElem w b equivs + | eps `member` equivs = app (equivFun (equivs ! eps)) w + | otherwise = case w of + VGlueElem v us -> v + _ -> VUnGlueElem w b equivs compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b equivs wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) - vs = mapWithKey - (\alpha wAlpha -> unGlue wAlpha - (b `face` alpha) (equivs `face` alpha)) ws + vs = mapWithKey (\alpha wAlpha -> + unGlue wAlpha (b `face` alpha) (equivs `face` alpha)) + ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs vi0 = unGlue wi0 (b `face` (i ~> 0)) (equivs `face` (i ~> 0)) -- in b(i0) @@ -542,8 +509,8 @@ compGlue i b equivs wi0 ws = glueElem vi1'' usi1'' vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) equivsI1 = equivs `face` (i ~> 1) - equivs' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) equivs - equivs'' = filterWithKey (\alpha _ -> alpha `Map.notMember` equivs') equivsI1 + equivs' = filterWithKey (\alpha _ -> i `notMember` alpha) equivs + equivs'' = filterWithKey (\alpha _ -> alpha `notMember` equivs') equivsI1 us' = mapWithKey (\gamma isoG -> fill i (equivDom isoG) (wi0 `face` gamma) (ws `face` gamma)) @@ -568,18 +535,18 @@ compGlue i b equivs wi0 ws = glueElem vi1'' usi1'' gradLemma (bi1 `face` gamma) isoG ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma)) (vi1' `face` gamma)) - equivs'' + equivs'' vsi1' = Map.map constPath $ border vi1' equivs' `unionSystem` vsi1 vi1'' = compLine (constPath bi1) vi1' (Map.map snd uls'' `unionSystem` vsi1') - usi1'' = Map.mapWithKey (\gamma _ -> - if gamma `Map.member` usi1' then usi1' ! gamma - else fst (uls'' ! gamma)) - equivsI1 - + usi1'' = mapWithKey (\gamma _ -> + if gamma `member` usi1' + then usi1' ! gamma + else fst (uls'' ! gamma)) + equivsI1 -- 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) @@ -618,21 +585,63 @@ pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us' -- L-path p between v and f u. gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val) gradLemma b e us v = (u,VPath j $ tau `sym` j) - where i:j:_ = freshs (b,e,us,v) + where i:j:_ = freshs (b,e,us,v) (a,f,s,t) = (equivDom e,equivFun e,equivCenter e,equivIsCenter e) - g y = fstVal (app s y) -- g : b -> a - eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b - us' = mapWithKey - (\alpha uAlpha -> - let fuAlpha = app (f `face` alpha) uAlpha - in app (app (t `face` alpha) fuAlpha) - (VPair uAlpha (constPath fuAlpha))) us + g y = fstVal (app s y) -- g : b -> a + eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b + us' = mapWithKey (\alpha uAlpha -> + let fuAlpha = app (f `face` alpha) uAlpha + in app (app (t `face` alpha) fuAlpha) + (VPair uAlpha (constPath fuAlpha))) + us theta = fill i a (g v) (Map.map (fstVal . (@@ i)) us') - u = theta `face` (i ~> 1) - vs = insertsSystem - [(j ~> 0, app f theta),(j ~> 1, v)] - (Map.map ((@@ j) . sndVal . (@@ i)) us') - tau = comp i b (eta v @@ j) vs + u = theta `face` (i ~> 1) + vs = insertsSystem [(j ~> 0, app f theta),(j ~> 1, v)] + (Map.map ((@@ j) . sndVal . (@@ i)) us') + tau = comp i b (eta v @@ j) vs + +-- Every path in the universe induces an equivalence +eqToEquiv :: Val -> Val +eqToEquiv e = VPair e1 (VPair f (VPair s t)) + where (i,j,x,y,w,ev) = (Name "i",Name "j",Var "x",Var "y",Var "w",Var "E") + e1 = e @@ One + inv t = Path i $ AppFormula t (NegAtom i) + evinv = inv ev + (ev0,ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a) + eenv = upd ("E",e) emptyEnv + -- eplus : e0 -> e1 + eplus z = Comp ev z empty + -- eminus : e1 -> e0 + eminus z = Comp evinv z empty + -- NB: edown is *not* transNegFill + eup z = Fill ev z empty + edown z = Fill evinv z empty + f = Ter (Lam "x" ev1 (eminus x)) eenv + -- g = Ter (Lam "y" ev0 (eplus y)) eenv + etasys z0 = mkSystem [(j ~> 1, inv (eup z0)) + ,(j ~> 0, edown (eplus z0))] + -- eta : (y : e0) -> eminus (eplus y) = y + eta z0 = Path j $ Comp evinv (eplus z0) (etasys z0) + etaSquare z0 = Fill evinv (eplus z0) (etasys z0) + s = Ter (Lam "y" ev0 $ Pair (eplus y) (eta y)) eenv + (a,p) = (Fst w,Snd w) -- a : e1 and p : eminus a = y + phisys l = mkSystem [ (l ~> 0, inv (edown a)) + , (l ~> 1, eup y)] + psi l = Comp ev (AppFormula p (Atom l)) (phisys l) + phi l = Fill ev (AppFormula p (Atom l)) (phisys l) + tsys = mkSystem + [ (j ~> 0, edown (psi i)) + , (j ~> 1, inv $ eup y) + , (i ~> 0, inv $ phi j) + , (i ~> 1, etaSquare y) ] + -- encode act on terms using Path and AppFormula + psi' formula = AppFormula (Path j $ psi j) formula + tprinc = psi' (Atom i :\/: Atom j) + t2 = Comp evinv tprinc tsys + t2inv = AppFormula (inv (Path i t2)) (Atom i) + fibtype = Sigma (Lam "x" ev1 $ IdP (Path (Name "_") ev0) (eminus x) y) + t = Ter (Lam "y" ev0 $ Lam "w" fibtype $ Path i $ + Pair (psi' (NegAtom i)) (Path j t2inv)) eenv ------------------------------------------------------------------------------- -- | Conversion @@ -722,6 +731,7 @@ instance Convertible a => Convertible (System a) where instance Convertible Formula where conv _ phi psi = dnf phi == dnf psi + ------------------------------------------------------------------------------- -- | Normalization diff --git a/TypeChecker.hs b/TypeChecker.hs index 4348503..ad26bc3 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -27,8 +27,8 @@ data TEnv = } deriving (Eq) verboseEnv, silentEnv :: TEnv -verboseEnv = TEnv [] 0 empty True -silentEnv = TEnv [] 0 empty False +verboseEnv = TEnv [] 0 emptyEnv True +silentEnv = TEnv [] 0 emptyEnv False -- Trace function that depends on the verbosity flag trace :: String -> Typing () @@ -289,7 +289,7 @@ mkEquiv vb = eval rho $ Sigma $ Lam "s" (Pi (Lam "y" b $ fib)) $ Pi (Lam "y" b $ Pi (Lam "w" fib $ IdP (Path (Name "_") fib) (App s y) w)) where [a,b,f,x,y,s,w] = map Var ["a","b","f","x","y","s","w"] - rho = upd ("b",vb) empty + rho = upd ("b",vb) emptyEnv fib = Sigma (Lam "x" a $ IdP (Path (Name "_") b) (App f x) y) checkEquiv :: Val -> Ter -> Typing () -- 2.34.1