From a1ee1930644ca12e2b21ee8e38fbb6ad5a11a04d Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 4 Jun 2015 18:03:22 +0200 Subject: [PATCH] Added fill as a term and comp is now genComp --- CTT.hs | 16 ++++------------ Eval.hs | 20 ++++++++++++++++++++ Exp.cf | 2 +- Resolver.hs | 7 ++----- TypeChecker.hs | 9 +++++++++ 5 files changed, 36 insertions(+), 18 deletions(-) diff --git a/CTT.hs b/CTT.hs index 1e9f5de..3dbe30c 100644 --- a/CTT.hs +++ b/CTT.hs @@ -105,8 +105,9 @@ data Ter = App Ter Ter | IdP Ter Ter Ter | Path Name Ter | AppFormula Ter Formula - -- Kan Composition + -- Kan composition and filling | Comp Ter Ter (System Ter) + | Fill Ter Ter (System Ter) -- | Trans Ter Ter -- Composition in the Universe -- | CompElem Ter (System Ter) Ter (System Ter) @@ -183,15 +184,6 @@ data Val = VU | VLam Ident Val Val deriving Eq --- data HIso = Iso Val Val Val Val Val --- | Eq Val --- deriving (Eq,Show) - --- toHIso :: Val -> HIso --- toHIso (VPair a (VPair f (VPair g (VPair s t)))) = Iso a f g s t --- toHIso v = Eq v --- toHIso _ = error "toHIso" - isNeutral :: Val -> Bool isNeutral v = case v of Ter Undef{} _ -> True @@ -407,8 +399,8 @@ showTer v = case v of IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e AppFormula e phi -> showTer1 e <+> char '@' <+> showFormula phi - Comp e0 e1 es -> text "comp" <+> showTers [e0,e1] - <+> text (showSystem es) + Comp e t ts -> text "comp" <+> showTers [e,t] <+> text (showSystem ts) + Fill e t ts -> text "fill" <+> showTers [e,t] <+> text (showSystem ts) -- Trans e0 e1 -> text "transport" <+> showTers [e0,e1] Glue a ts -> text "glue" <+> showTer1 a <+> text (showSystem ts) GlueElem a ts -> text "glueElem" <+> showTer1 a <+> text (showSystem ts) diff --git a/Eval.hs b/Eval.hs index 3144eef..db7827e 100644 --- a/Eval.hs +++ b/Eval.hs @@ -159,6 +159,7 @@ eval rho v = case v of 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) Glue a ts -> glue (eval rho a) (evalSystem rho ts) GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) _ -> error $ "Cannot evaluate " ++ show v @@ -443,6 +444,25 @@ hisoFun :: Val -> Val hisoFun (VPair _ (VPair f _)) = f hisoFun x = error $ "HisoFun: Not an hiso: " ++ show x +-- -- Every line in the universe induces an hiso +-- eqToIso :: Val -> Val +-- eqToIso e = VPair e0 (VPair f (VPair g (VPair s t))) +-- where e0 = e @@ Zero +-- (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E") +-- evinv = Path "i" $ AppFormula ev (NegAtom i) +-- (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) +-- eenv = upd ("E",e) empty +-- (eplus z,eminus z) = (Comp ev z Map.empty,Comp evinv z Map.empty) +-- (eup z,edown z) = (Comp ) +-- f = Ter (Lam x ev1 (eminus x)) eenv +-- g = Ter (Lam y ev0 (eplus y)) eenv +-- -- s : (y : b) -> f (g y) = y +-- ssys = mkSystem [(j ~> 0, transFill j (e @@ j) b) +-- ,(j ~> 1, transFillNeg j (e @@ j) +-- (trans j (e @@ j) b))]) +-- s = Ter (Lam y ev0 $ Path j $ Comp einv +-- ) eenv + -- eqToIso :: Name -> Val -> Val -- eqToIso i u = VPair a (VPair f (VPair g (VPair s t))) -- where a = u `face` (i ~> 1) diff --git a/Exp.cf b/Exp.cf index 0c0dcf3..718647d 100644 --- a/Exp.cf +++ b/Exp.cf @@ -33,7 +33,7 @@ App. Exp2 ::= Exp2 Exp3 ; IdP. Exp3 ::= "IdP" Exp4 Exp4 Exp4 ; Trans. Exp3 ::= "transport" Exp4 Exp4 ; Comp. Exp3 ::= "comp" Exp4 Exp4 System ; -GenComp. Exp3 ::= "genComp" Exp4 Exp4 System ; +Fill. Exp3 ::= "fill" Exp4 Exp4 System ; Glue. Exp3 ::= "glue" Exp4 System ; -- GlueElem. Exp3 ::= "glueElem" Exp4 System ; -- CompElem. Exp3 ::= "compElem" Exp4 System Exp4 System ; diff --git a/Resolver.hs b/Resolver.hs index 60c9ebc..734d5c9 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -204,11 +204,8 @@ resolveExp e = case e of _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi Trans x y -> CTT.Comp <$> resolveExp x <*> resolveExp y <*> pure Map.empty IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z - Comp u v ts -> CTT.Comp <$> (CTT.Path (C.Name "_") <$> resolveExp u) - <*> resolveExp v <*> resolveSystem ts - - GenComp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts - + Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts + Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts Glue u ts -> do rs <- resolveSystem ts let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True diff --git a/TypeChecker.hs b/TypeChecker.hs index c94f8ab..82f51bf 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -429,6 +429,15 @@ infer e = case e of check va0 t0 checkPathSystem t0 va ps return va1 + Fill a t0 ps -> do + (va0, va1) <- checkPath (constPath VU) a + va <- evalTyping a + check va0 t0 + checkPathSystem t0 va ps + vt <- evalTyping t0 + rho <- asks env + let vps = evalSystem rho ps + return (VIdP va vt (compLine va vt vps)) -- CompElem a es u us -> do -- check VU a -- rho <- asks env -- 2.34.1