From bdcb90f823a9025a4b9cb7194ed7bd9d4abab01a Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 4 Jun 2015 11:06:40 +0200 Subject: [PATCH] Fix for neutral unglues --- CTT.hs | 22 +++++++++++++---- Eval.hs | 73 +++++++++++++++++++++++++++++++++++++-------------------- 2 files changed, 64 insertions(+), 31 deletions(-) diff --git a/CTT.hs b/CTT.hs index a0e08ee..01f727b 100644 --- a/CTT.hs +++ b/CTT.hs @@ -94,7 +94,8 @@ data Ter = App Ter Ter -- branches c1 xs1 -> M1,..., cn xsn -> Mn | Split Ident Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) - | Sum Loc Ident [Label] + | Sum Loc Ident [Label] -- TODO: should only contain OLabels + | HSum Loc Ident [Label] -- undefined and holes | Undef Loc Ter -- Location and type @@ -157,6 +158,9 @@ data Val = VU -- Composition in the universe (for now) | VCompU Val (System Val) + -- Composition for HITs; the type is constant + | VHComp Val Val (System Val) + -- GlueLine values -- | VGlueLine Val Formula Formula -- | VGlueLineElem Val Formula Formula @@ -169,9 +173,11 @@ data Val = VU | VVar Ident Val | VFst Val | VSnd Val - | VUnGlueElem Val (System Val) - | VUnGlueElemU Val (System Val) + -- VUnGlueElem val type hisos + | VUnGlueElem Val Val (System Val) + | VUnGlueElemU Val Val (System Val) | VSplit Val Val + | VSqueezeH Val Val | VApp Val Val | VAppFormula Val Formula | VLam Ident Val Val @@ -395,6 +401,7 @@ showTer v = case v of <+> hsep (map ((char '@' <+>) . showFormula) phis) Split f _ _ _ -> text f Sum _ n _ -> text n + HSum _ n _ -> text n Undef{} -> text "undefined" Hole{} -> text "?" IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] @@ -426,6 +433,7 @@ showTer1 t = case t of Hole{} -> showTer t Split{} -> showTer t Sum{} -> showTer t + HSum{} -> showTer t _ -> parens (showTer t) showDecls :: [Decl] -> Doc @@ -439,11 +447,13 @@ showVal :: Val -> Doc showVal v = case v of VU -> char 'U' Ter t@Sum{} rho -> showTer t <+> showEnv False rho + Ter t@HSum{} rho -> showTer t <+> showEnv False rho Ter t@Split{} rho -> showTer t <+> showEnv False rho Ter t rho -> showTer1 t <+> showEnv True rho VCon c us -> text c <+> showVals us VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us <+> hsep (map ((char '@' <+>) . showFormula) phis) + VHComp v0 v1 vs -> text "hComp" <+> showVals [v0,v1] <+> text (showSystem vs) VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b | otherwise -> char '(' <> showLam v @@ -457,8 +467,10 @@ showVal v = case v of VVar x _ -> text x VFst u -> showVal1 u <> text ".1" VSnd u -> showVal1 u <> text ".2" - VUnGlueElem v hs -> text "unGlueElem" <+> showVal1 v <+> text (showSystem hs) - VUnGlueElemU v es -> text "unGlueElemU" <+> showVal1 v <+> text (showSystem es) + VUnGlueElem v b hs -> text "unGlueElem" <+> showVals [v,b] + <+> text (showSystem hs) + VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b] + <+> text (showSystem es) VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2] VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) diff --git a/Eval.hs b/Eval.hs index 713e9aa..5e847c7 100644 --- a/Eval.hs +++ b/Eval.hs @@ -68,6 +68,7 @@ instance Nominal Val where VSnd u -> support u VCon _ vs -> support vs VPCon _ a vs phis -> support (a,vs,phis) + VHComp a u ts -> support (a,u,ts) VVar _ v -> support v VApp u v -> support (u,v) VLam _ u v -> support (u,v) @@ -76,8 +77,8 @@ instance Nominal Val where VGlue a ts -> support (a,ts) VGlueElem a ts -> support (a,ts) VCompU a ts -> support (a,ts) - VUnGlueElem a hs -> support (a,hs) - VUnGlueElemU a es -> support (a,es) + 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) @@ -105,6 +106,7 @@ instance Nominal Val where VSnd u -> sndVal (acti u) VCon c vs -> VCon c (acti vs) VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis) + VHComp a u us -> VHComp (acti a) (acti u) (acti us) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -112,8 +114,8 @@ instance Nominal Val where VSplit u v -> app (acti u) (acti v) VGlue a ts -> glue (acti a) (acti ts) VGlueElem a ts -> glueElem (acti a) (acti ts) - VUnGlueElem a hs -> unGlue (acti a) (acti hs) - VUnGlueElemU a es -> unGlueU (acti a) (acti es) + 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) @@ -138,6 +140,7 @@ instance Nominal Val where VSnd u -> VSnd (sw u) 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) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -145,8 +148,8 @@ instance Nominal Val where VSplit u v -> VSplit (sw u) (sw v) VGlue a ts -> VGlue (sw a) (sw ts) VGlueElem a ts -> VGlueElem (sw a) (sw ts) - VUnGlueElem a hs -> VUnGlueElem (sw a) (sw hs) - VUnGlueElemU a es -> VUnGlueElemU (sw a) (sw es) + 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) @@ -173,6 +176,7 @@ eval rho v = case v of Lam{} -> Ter v rho Split{} -> Ter v rho Sum{} -> Ter v rho + HSum{} -> Ter v rho Undef{} -> Ter v rho Hole{} -> Ter v rho IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) @@ -289,6 +293,8 @@ inferType v = case v of ty -> error $ "inferType: expected IdP type for " ++ show v ++ ", got " ++ show ty 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 @@ -304,7 +310,7 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral." pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val -pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of +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) @@ -453,11 +459,8 @@ comp i a u ts = case a of in VCon n $ comps i as env tsus else VComp (VPath i a) u (Map.map (VPath i) ts) Nothing -> error $ "comp: missing constructor in labelled sum " ++ n - VPCon{} -> compHIT i a u ts - VComp{} -> VComp (VPath i a) u (Map.map (VPath i) ts) - -- VCompElem _ _ u1 _ -> comp i a u1 ts - -- VElimComp _ _ u1 -> comp i a u1 ts _ -> 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 @@ -478,9 +481,25 @@ compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) compHIT :: Name -> Val -> Val -> System Val -> Val compHIT = undefined + +-- case u of +-- VCon n us -> case lookupLabel n nass of +-- Just as -> +-- if all isCon (elems ts) +-- then let tsus = transposeSystemAndList (Map.map unCon ts) us +-- in VCon n $ comps i as env tsus +-- else VComp (VPath i a) u (Map.map (VPath i) ts) +-- Nothing -> error $ "comp: missing constructor in labelled sum " ++ n +-- VPCon{} -> compHIT i a u ts +-- VComp{} -> VComp (VPath i a) u (Map.map (VPath i) ts) +-- _ -> error $ "comp ter sum" ++ show u + + transpHIT :: Name -> Val -> Val -> Val -transpHIT = undefined +transpHIT i a u = squeezeHIT i a u `face` (i ~> 0) +-- Given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i +-- transHIT i a u(i=0) to u(i=1) in a(1) squeezeHIT :: Name -> Val -> Val -> Val squeezeHIT = undefined @@ -517,15 +536,15 @@ glueElem v us | Map.null us = v | eps `Map.member` us = us ! eps | otherwise = VGlueElem v us -unGlue :: Val -> System Val -> Val -unGlue w hisos +unGlue :: Val -> Val -> System Val -> Val +unGlue w b hisos | Map.null hisos = w | 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 hisos + _ -> VUnGlueElem w b hisos -- transGlue :: Name -> Val -> System Val -> Val -> Val -- transGlue i b hisos wi0 = glueElem vi1'' usi1 @@ -571,9 +590,10 @@ compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) vs = mapWithKey - (\alpha wAlpha -> unGlue wAlpha (hisos `face` alpha)) ws + (\alpha wAlpha -> unGlue wAlpha + (b `face` alpha) (hisos `face` alpha)) ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlue wi0 (hisos `face` (i ~> 0)) -- in b(i0) + vi0 = unGlue wi0 (b `face` (i ~> 0)) (hisos `face` (i ~> 0)) -- in b(i0) v = fill i b vi0 vs -- in b vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) @@ -770,13 +790,13 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = ------------------------------------------------------------------------------- -- | Composition in the Universe (to be replaced as glue) -unGlueU :: Val -> System Val -> Val -unGlueU w es +unGlueU :: Val -> Val -> System Val -> Val +unGlueU w b es | Map.null es = w | eps `Map.member` es = transNegLine (es ! eps) w | otherwise = case w of VGlueElem v us -> v - _ -> VUnGlueElemU w es + _ -> VUnGlueElemU w b es compUniv :: Val -> System Val -> Val compUniv b es | Map.null es = b @@ -787,9 +807,10 @@ compUniv b es | Map.null es = b compU :: Name -> Val -> System Val -> Val -> System Val -> Val compU i b es wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) - vs = mapWithKey (\alpha wAlpha -> unGlueU wAlpha (es `face` alpha)) ws + vs = mapWithKey (\alpha wAlpha -> + unGlueU wAlpha (b `face` alpha) (es `face` alpha)) ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlueU wi0 (es `face` (i ~> 0)) -- in b(i0) + vi0 = unGlueU wi0 (b `face` (i ~> 0)) (es `face` (i ~> 0)) -- in b(i0) v = fill i b vi0 vs -- in b vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) @@ -1065,8 +1086,8 @@ instance Convertible Val where (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' + (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') @@ -1125,8 +1146,8 @@ instance Normal Val where -- 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 hs -> unGlue (normal ns u) (normal ns hs) - VUnGlueElemU u es -> unGlueU (normal ns u) (normal ns es) + 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) -- 2.34.1