From 2728606117b88e20578bbdc19af3f0299235ee82 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 24 Mar 2015 16:00:22 +0100 Subject: [PATCH] added compElem and elimComp (still buggy) --- CTT.hs | 83 ++++++++----- Eval.hs | 289 ++++++++++++++++++++++++++++++++----------- Exp.cf | 2 + Resolver.hs | 8 ++ TypeChecker.hs | 91 +++++++++++--- examples/bool.ctt | 19 +++ examples/nat.ctt | 3 - examples/prelude.ctt | 3 + 8 files changed, 374 insertions(+), 124 deletions(-) diff --git a/CTT.hs b/CTT.hs index 562ddb9..d713c18 100644 --- a/CTT.hs +++ b/CTT.hs @@ -71,6 +71,9 @@ data Ter = App Ter Ter -- Kan Composition | Comp Ter Ter (System Ter) | Trans Ter Ter + -- Composition in the Universe + | CompElem Ter (System Ter) Ter (System Ter) + | ElimComp Ter (System Ter) Ter -- Glue | Glue Ter (System Ter) | GlueElem Ter (System Ter) @@ -111,6 +114,10 @@ data Val = VU | VGlue Val (System Val) | VGlueElem Val (System Val) + -- Universe Composition Values + | VCompElem Val (System Val) Val (System Val) + | VElimComp Val (System Val) Val + -- Neutral values: | VVar Ident Val | VFst Val @@ -122,15 +129,17 @@ data Val = VU isNeutral :: Val -> Bool isNeutral v = case v of - VVar _ _ -> True - VFst v -> isNeutral v - VSnd v -> isNeutral v - VSplit _ v -> isNeutral v - VApp v _ -> isNeutral v - VAppFormula v _ -> isNeutral v - VComp a u ts -> isNeutralComp a u ts - VTrans a u -> isNeutralTrans a u -- isNeutral a || isNeutralComp (a @@ 0) u Map.empty - _ -> False + VVar _ _ -> True + VFst v -> isNeutral v + VSnd v -> isNeutral v + VSplit _ v -> isNeutral v + VApp v _ -> isNeutral v + VAppFormula v _ -> isNeutral v + VComp a u ts -> isNeutralComp a u ts + VTrans a u -> isNeutralTrans a u + VCompElem _ _ u _ -> isNeutral u + VElimComp _ _ u -> isNeutral u + _ -> False isNeutralSystem :: System Val -> Bool isNeutralSystem = any isNeutral . Map.elems @@ -237,27 +246,32 @@ instance Show Ter where showTer :: Ter -> Doc showTer v = case v of - U -> char 'U' - App e0 e1 -> showTer e0 <+> showTer1 e1 - Pi e0 -> text "Pi" <+> showTer e0 - Lam x t e -> char '\\' <> text x <+> text "->" <+> showTer e - Fst e -> showTer e <> text ".1" - Snd e -> showTer e <> text ".2" - Sigma e0 -> text "Sigma" <+> showTer e0 - Pair e0 e1 -> parens (showTer1 e0 <> comma <> showTer1 e1) - Where e d -> showTer e <+> text "where" <+> showDecls d - Var x -> text x - Con c es -> text c <+> showTers es - Split l _ _ -> text "split" <+> showLoc l - Sum _ n _ -> text "sum" <+> text n - Undef _ -> text "undefined" - 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) - Trans e0 e1 -> text "transport" <+> showTers [e0,e1] - Glue a ts -> text "glue" <+> showTer a <+> text (showSystem ts) - GlueElem a ts -> text "glueElem" <+> showTer a <+> text (showSystem ts) + U -> char 'U' + App e0 e1 -> showTer e0 <+> showTer1 e1 + Pi e0 -> text "Pi" <+> showTer e0 + Lam x t e -> char '\\' <> text x <+> text "->" <+> showTer e + Fst e -> showTer e <> text ".1" + Snd e -> showTer e <> text ".2" + Sigma e0 -> text "Sigma" <+> showTer e0 + Pair e0 e1 -> parens (showTer1 e0 <> comma <> showTer1 e1) + Where e d -> showTer e <+> text "where" <+> showDecls d + Var x -> text x + Con c es -> text c <+> showTers es + Split l _ _ -> text "split" <+> showLoc l + Sum _ n _ -> text "sum" <+> text n + Undef _ -> text "undefined" + 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) + 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) + CompElem a es t ts -> text "compElem" <+> showTer1 a <+> text (showSystem es) + <+> showTer1 t <+> text (showSystem ts) + ElimComp a es t -> text "elimComp" <+> showTer1 a <+> text (showSystem es) + <+> showTer1 t showTers :: [Ter] -> Doc showTers = hsep . map showTer1 @@ -296,8 +310,13 @@ showVal v = case v of VAppFormula v phi -> showVal1 v <+> char '@' <+> showFormula phi VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs) VTrans v0 v1 -> text "trans" <+> showVals [v0,v1] - VGlue a ts -> text "glue" <+> showVal a <+> text (showSystem ts) - VGlueElem a ts -> text "glueElem" <+> showVal a <+> text (showSystem ts) + VGlue a ts -> text "glue" <+> showVal1 a <+> text (showSystem ts) + VGlueElem a ts -> text "glueElem" <+> showVal1 a <+> text (showSystem ts) + VCompElem a es t ts -> text "compElem" <+> showVal1 a <+> text (showSystem es) + <+> showVal1 t <+> text (showSystem ts) + VElimComp a es t -> text "elimComp" <+> showVal1 a <+> text (showSystem es) + <+> showVal1 t + showVal1 v = case v of VU -> char 'U' VCon c [] -> text c diff --git a/Eval.hs b/Eval.hs index 6d52524..eef1410 100644 --- a/Eval.hs +++ b/Eval.hs @@ -4,9 +4,10 @@ module Eval where import Data.List import Data.Maybe (fromMaybe) import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey - ,elems,intersectionWith,keys) + ,elems,intersectionWith,intersection,keys) import qualified Data.Map as Map +import Debug.Trace import Connections import CTT @@ -46,24 +47,26 @@ instance Nominal Env where swap e ij = mapEnv (`swap` ij) (`swap` ij) e instance Nominal Val where - support VU = [] - support (Ter _ e) = support e - support (VPi v1 v2) = support [v1,v2] - support (VComp a u ts) = support (a,u,ts) - support (VIdP a v0 v1) = support [a,v0,v1] - support (VPath i v) = i `delete` support v - support (VTrans u v) = support (u,v) - support (VSigma u v) = support (u,v) - support (VPair u v) = support (u,v) - support (VFst u) = support u - support (VSnd u) = support u - support (VCon _ vs) = support vs - support (VVar _ v) = support v - support (VApp u v) = support (u,v) - support (VAppFormula u phi) = support (u,phi) - support (VSplit u v) = support (u,v) - support (VGlue a ts) = support (a,ts) - support (VGlueElem a ts) = support (a,ts) + support VU = [] + support (Ter _ e) = support e + support (VPi v1 v2) = support [v1,v2] + support (VComp a u ts) = support (a,u,ts) + support (VIdP a v0 v1) = support [a,v0,v1] + support (VPath i v) = i `delete` support v + support (VTrans u v) = support (u,v) + support (VSigma u v) = support (u,v) + support (VPair u v) = support (u,v) + support (VFst u) = support u + support (VSnd u) = support u + support (VCon _ vs) = support vs + support (VVar _ v) = support v + support (VApp u v) = support (u,v) + support (VAppFormula u phi) = support (u,phi) + support (VSplit u v) = support (u,v) + support (VGlue a ts) = support (a,ts) + support (VGlueElem a ts) = support (a,ts) + support (VCompElem a es u us) = support (a,es,u,us) + support (VElimComp a es u) = support (a,es,u) act u (i, phi) = let acti :: Nominal a => a -> a @@ -90,30 +93,34 @@ 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) + 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) = let sw :: Nominal a => a -> a sw u = swap u ij in case u of - VU -> VU - Ter t e -> Ter t (sw e) - VPi a f -> VPi (sw a) (sw f) + VU -> VU + Ter t e -> Ter t (sw e) + VPi a f -> VPi (sw a) (sw f) 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) - VSnd u -> VSnd (sw u) - VCon c vs -> VCon c (sw vs) - VVar x v -> VVar x (sw v) - VAppFormula u psi -> VAppFormula (sw u) (sw psi) - VApp u v -> VApp (sw u) (sw v) - VSplit u v -> VSplit (sw u) (sw v) - VGlue a ts -> VGlue (sw a) (sw ts) - VGlueElem a ts -> VGlueElem (sw a) (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) + VSnd u -> VSnd (sw u) + VCon c vs -> VCon c (sw vs) + VVar x v -> VVar x (sw v) + VAppFormula u psi -> VAppFormula (sw u) (sw psi) + VApp u v -> VApp (sw u) (sw v) + VSplit u v -> VSplit (sw u) (sw v) + VGlue a ts -> VGlue (sw a) (sw ts) + VGlueElem a ts -> VGlueElem (sw a) (sw ts) + 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 @@ -143,6 +150,9 @@ eval rho v = case v of 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) + 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) evalFormula :: Env -> Formula -> Formula evalFormula rho phi = case phi of @@ -230,7 +240,11 @@ transLine :: Val -> Val -> Val transLine u v = trans i (u @@ i) v where i = fresh (u,v) -trans, transNeg :: Name -> Val -> Val -> Val +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 = case (v0,v1) of (VIdP a u v,w) -> let j = fresh (Atom i, v0, w) @@ -247,8 +261,11 @@ trans i v0 v1 = case (v0,v1) of Just as -> VCon n $ transps i as env us Nothing -> error $ "comp: missing constructor in labelled sum " ++ n ++ " v0 = " ++ show v0 _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 - (VGlue a ts,_) -> transGlue i a ts v1 + (VGlue a ts,_) -> transGlue i a ts v1 + (VComp VU a es,_) -> transU i a es v1 _ | otherwise -> error "trans not implemented" + +transNeg :: Name -> Val -> Val -> Val transNeg i a u = trans i (a `sym` i) u transFill, transFillNeg :: Name -> Val -> Val -> Val @@ -366,6 +383,11 @@ comps _ _ _ _ = error "comps: different lengths of types and values" -- i is independent of a and u comp :: Name -> Val -> Val -> System Val -> Val +comp i a u ts | trace ("comp: \n a = " ++ show a + ++ "\n u = " ++ show u + ++ "\n ts = " ++ show ts + ++ "\n support ts = " ++ show (support ts)) + False = undefined comp i a u ts | eps `Map.member` ts = (ts ! eps) `face` (i ~> 1) comp i a u ts | i `notElem` support ts = u comp i a u ts | not (Map.null indep) = comp i a u ts' @@ -384,6 +406,7 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid?? _ | isNeutral a || isNeutralSystem ts || isNeutral u -> VComp a u (Map.map (VPath i) ts) VGlue b hisos -> compGlue i b hisos u ts + VComp VU a es -> compU i a es u ts Ter (Sum _ _ nass) env -> case u of VCon n us -> case lookup n nass of Just as -> VCon n $ comps i as env tsus @@ -391,9 +414,46 @@ comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid?? Nothing -> error $ "comp: missing constructor in labelled sum " ++ n _ -> error "comp ter sum" + compNeg :: Name -> Val -> Val -> System Val -> Val compNeg i a u ts = comp i a 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 = genFill 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" + +------------------------------------------------------------------------------- +-- | Glue +-- +-- An hiso for a type b is a five-tuple: (a,f,g,r,s) where +-- a : U +-- f : a -> b +-- g : b -> a +-- s : forall (y : b), f (g y) = y +-- t : forall (x : a), g (f x) = x + +hisoDom :: Val -> Val +hisoDom (VPair a _) = a +hisoDom x = error $ "HisoDom: Not an hiso: " ++ show x + +hisoFun :: Val -> Val +hisoFun (VPair _ (VPair f _)) = f +hisoFun x = error $ "HisoFun: Not an hiso: " ++ show x + +glue :: Val -> System Val -> Val +glue b ts | Map.null ts = b + | eps `Map.member` ts = hisoDom (ts ! eps) + | otherwise = VGlue b ts + +glueElem :: Val -> System Val -> Val +glueElem v us | Map.null us = v + | eps `Map.member` us = us ! eps + | otherwise = VGlueElem v us + unGlue :: System Val -> Val -> Val unGlue hisos w | Map.null hisos = w @@ -435,41 +495,115 @@ pathComp i a u u' us = VPath j $ genComp i a (u `face` (i ~> 0)) us' --- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] --- fills i [] _ [] = [] --- fills i ((x,a):as) e ((ts,u):tsus) = --- let v = genFill 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" - ------------------------------------------------------------------------------- --- | Glue --- --- An hiso for a type b is a five-tuple: (a,f,g,r,s) where --- a : U --- f : a -> b --- g : b -> a --- s : forall (y : b), f (g y) = y --- t : forall (x : a), g (f x) = x - -hisoDom :: Val -> Val -hisoDom (VPair a _) = a -hisoDom x = error $ "HisoDom: Not an hiso: " ++ show x - -hisoFun :: Val -> Val -hisoFun (VPair _ (VPair f _)) = f -hisoFun x = error $ "HisoFun: Not an hiso: " ++ show x +-- | Composition in the Universe + +compElem :: Val -> System Val -> Val -> System Val -> Val +compElem a es u us | 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 | Map.null es = u + | eps `Map.member` es = transNegLine (es ! eps) u + | otherwise = VElimComp a es u + +--compU i (Kan j VU ejs b) ws wi0 = +compU :: Name -> Val -> System Val -> Val -> System Val -> Val +compU i a es w0 ws = + let unkan alpha = elimComp (a `face` alpha) (es `face` alpha) + + vs = mapWithKey unkan ws + v0 = elimComp a es w0 -- in a + v1 = comp i a v0 vs -- in a + + us1' = mapWithKey (\gamma eGamma -> + comp i (eGamma @@ Zero) (w0 `face` gamma) + (ws `face` gamma)) es + ls' = mapWithKey (\gamma _ -> pathUniv i (es `proj` gamma) + (ws `face` gamma) (w0 `face` gamma)) + es + + v1' = compLine a v1 ls' + in compElem a es v1' us1' + + +transU :: Name -> Val -> System Val -> Val -> Val +transU i a es wi0 = + let unkan alpha = elimComp (a `face` alpha) (es `face` alpha) + + vi0 = unkan (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, sigma gamma (i1)) | gamma elem es} + es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esi1 + + -- set of elements in es independent of i + es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es + + usi1' = mapWithKey (\gamma eGamma -> + trans i (eGamma @@ Zero) (wi0 `face` gamma)) es' + + ls' = mapWithKey (\gamma _ -> + pathUniv i (es `proj` gamma) Map.empty (wi0 `face` gamma)) + es' + + vi1' = compLine ai1 vi1 ls' + + uls'' = mapWithKey (\gamma _ -> -- TODO: proj or "!" ? + -- eqLemma (es `proj` (gamma `meet` (i ~> 1))) + 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 + + + +-- 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. +-- TODO: adapt? +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 = genComp i (e @@ Zero) ui0 us + ws = mapWithKey (\alpha uAlpha -> + transFill j (ej `face` alpha) uAlpha) + us + wi0 = transFill j (ej `face` (i ~> 0)) ui0 + wi1 = genComp i ej wi0 ws + wi1' = transFill j (ej `face` (i ~> 1)) ui1 + xi1 = genComp j (ej `face` (i ~> 1)) ui1 + (mkSystem [(k ~> 1, wi1'), (k ~> 0, 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 -> + transFill i (ei `face` alpha) uAlpha) ts + theta = genFillNeg i ei a vs + t = genCompNeg i ei a vs + theta' = transFill i ei t + ws = insertSystem (j ~> 1) theta' $ + insertSystem (j ~> 0) theta $ vs + theta'' = genComp i ei t ws -glue :: Val -> System Val -> Val -glue b ts | Map.null ts = b - | eps `Map.member` ts = hisoDom (ts ! eps) - | otherwise = VGlue b ts - -glueElem :: Val -> System Val -> Val -glueElem v us | Map.null us = v - | eps `Map.member` us = us ! eps - | otherwise = VGlueElem v us ------------------------------------------------------------------------------- -- | Conversion @@ -526,6 +660,9 @@ instance Convertible Val where (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts') (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos') (VGlueElem u us,VGlueElem u' us') -> conv k (u,us) (u',us') + (VCompElem a es u us,VCompElem a' es' u' us') -> + conv k (a,es,u,us) (a',es',u',us') + (VElimComp a es u,VElimComp a' es' u') -> conv k (a,es,u) (a',es',u') _ -> False simplify :: Int -> Name -> Val -> Val @@ -534,6 +671,16 @@ simplify k j v = case v of VComp a u ts -> let (ts',indep) = Map.partition (\t -> isIndep k j (t @@ j)) ts in if Map.null ts' then simplify k j u else VComp a u ts' + VCompElem a es u us -> + let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es + us' = intersection us es' + in if Map.null es' then simplify k j u else VCompElem a es' u us' + VElimComp a es u -> + let (es',indep) = Map.partition (\e -> isIndep k j (e @@ j)) es + u' = simplify k j u + in if Map.null es' then u' else case u' of + VCompElem _ _ w _ -> simplify k j w + _ -> VElimComp a es' u' _ -> v instance Convertible Env where diff --git a/Exp.cf b/Exp.cf index 9204e56..37c62a9 100644 --- a/Exp.cf +++ b/Exp.cf @@ -38,6 +38,8 @@ Trans. Exp3 ::= "transport" ; Comp. Exp3 ::= "comp" ; Glue. Exp3 ::= "glue" ; GlueElem. Exp3 ::= "glueElem" ; +CompElem. Exp3 ::= "compElem" ; +ElimComp. Exp3 ::= "elimComp" ; System. Exp3 ::= "[" [Side] "]" ; Pair. Exp3 ::= "(" Exp "," [Exp] ")" ; coercions Exp 3 ; diff --git a/Resolver.hs b/Resolver.hs index 091eedd..3c36ef3 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -184,6 +184,14 @@ resolveApps Glue (u:ts:xs) = do resolveApps GlueElem (u:ts:xs) = do let c = CTT.GlueElem <$> resolveExp u <*> resolveSystem ts CTT.mkApps <$> c <*> mapM resolveExp xs +resolveApps CompElem (a:es:t:ts:xs) = do + let c = CTT.CompElem <$> resolveExp a <*> resolveSystem es + <*> resolveExp t <*> resolveSystem ts + CTT.mkApps <$> c <*> mapM resolveExp xs +resolveApps ElimComp (a:es:t:xs) = do + let c = CTT.ElimComp <$> resolveExp a <*> resolveSystem es + <*> resolveExp t + CTT.mkApps <$> c <*> mapM resolveExp xs resolveApps x xs = CTT.mkApps <$> resolveExp x <*> mapM resolveExp xs resolveExp :: Exp -> Resolver Ter diff --git a/TypeChecker.hs b/TypeChecker.hs index 897f374..7d247ea 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TupleSections #-} module TypeChecker where import Data.Either @@ -5,7 +6,8 @@ import Data.Function import Data.List import Data.Maybe import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey - ,elems,intersectionWith,keys,intersectionWithKey) + ,elems,intersectionWith,keys,intersectionWithKey + ,intersection) import qualified Data.Map as Map import Data.Monoid hiding (Sum) import Control.Monad @@ -310,30 +312,83 @@ infer e = case e of (a0,a1) <- checkPath (constPath VU) p check a0 t return a1 - Comp a t0 ts -> do + Comp a t0 ps -> do check VU a rho <- asks env let va = eval rho a check va t0 - - -- check rho alpha |- t_alpha : a alpha - sequence $ elems $ - mapWithKey (\alpha talpha -> - local (faceEnv alpha) $ do - rhoAlpha <- asks env - (a0,_) <- checkPath (constPath (va `face` alpha)) talpha - k <- asks index - unless (conv k a0 (eval rhoAlpha t0)) - (throwError ("incompatible system with " ++ show t0)) - ) ts - - -- check that the system is compatible - k <- asks index - unless (isCompSystem k (evalSystem rho ts)) - (throwError ("Incompatible system " ++ show ts)) + checkPathSystem t0 va ps + return va + CompElem a es u us -> do + check VU a + rho <- asks env + k <- asks index + let va = eval rho a + ts <- checkPathSystem a VU es + let ves = evalSystem rho es + unless (keys es == keys us) + (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us)) + check va u + let vu = eval rho u + sequence_ $ elems $ intersectionWith check ts us + let vus = evalSystem rho us + unless (isCompSystem k vus) + (throwError ("Incompatible system " ++ show vus)) + sequence_ $ elems $ intersectionWithKey (\alpha eA vuA -> + unless (conv k (transNegLine eA vuA) (vu `face` alpha)) + (throwError $ "Malformed compElem: " ++ show us) + ) ves vus + return $ compLine VU va ves + ElimComp a es u -> do + check VU a + rho <- asks env + let va = eval rho a + checkPathSystem a VU es + let ves = evalSystem rho es + check (compLine VU va ves) u return va _ -> throwError ("infer " ++ show e) +-- Return system us such that: +-- rhoalpha |- p_alpha : Id (va alpha) (t0 rhoalpha) ualpha +-- Moreover, check that the system ps is compatible. +checkPathSystem :: Ter -> Val -> System Ter -> Typing (System Val) +checkPathSystem t0 va ps = do + -- TODO: make this nicer!! + -- Also return the evaluated ps + k <- asks index + let alist = Map.toList $ mapWithKey (\alpha pAlpha -> + local (faceEnv alpha) $ do + rhoAlpha <- asks env + (a0,a1) <- checkPath (constPath (va `face` alpha)) pAlpha + unless (conv k a0 (eval rhoAlpha t0)) + (throwError ("incompatible system with " ++ show t0)) + return a1 + ) ps + rho <- asks env + unless (isCompSystem k (evalSystem rho ps)) + (throwError ("Incompatible system " ++ show ps)) + Map.fromList <$> sequence [ (alpha,) <$> t | (alpha,t) <- alist ] + +-- checkGlueElem vu ts us = do +-- unless (keys ts == keys us) +-- (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us)) +-- rho <- asks env +-- k <- asks index +-- sequence_ $ elems $ intersectionWithKey +-- (\alpha vt u -> check (hisoDom vt) u) ts us +-- let vus = evalSystem rho us +-- sequence_ $ elems $ intersectionWithKey +-- (\alpha vt vAlpha -> do +-- unless (conv k (app (hisoFun vt) vAlpha) (vu `face` alpha)) +-- (throwError $ "Image of glueElem component " ++ show vAlpha ++ +-- " doesn't match " ++ show vu)) ts vus +-- unless (isCompSystem k vus) +-- (throwError $ "Incompatible system " ++ show vus) + +--inferCompElem :: Ter -> System Ter + + -- Check that a term is a path and output the source and target checkPath :: Val -> Ter -> Typing (Val,Val) checkPath v (Path i a) = do diff --git a/examples/bool.ctt b/examples/bool.ctt index c796767..82792ea 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -1,6 +1,7 @@ module bool where import prelude +import nat data bool = true | false @@ -53,3 +54,21 @@ F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2 negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2 +F2EqBoolComp : Id U F2 bool = + compId U F2 bool bool F2EqBool negEq + +test2 : bool = transport F2EqBoolComp one + +negNegEq : Id U bool bool = + compId U bool bool bool negEq negEq + + +test3 : bool = transport negNegEq true + +test4 : Id U bool bool = negNegEq @ i + +kanBool : Id U bool bool = + kan U bool bool bool bool negEq negEq negEq + +-- > negNegEq +-- EVAL: glue (sum bool) [ (?0 = 0) -> ((sum bool),(((split bool_L7_C1),(((split bool_L7_C1),(((split bool_L11_C1),(split bool_L11_C1)))))))) ] diff --git a/examples/nat.ctt b/examples/nat.ctt index f33aa0a..19c20fe 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -48,9 +48,6 @@ test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = comp A (p @ i) [ ] -compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = - comp A (p @ i) [ (i = 1) -> q ] - kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c) (r : Id A b d) : Id A c d = comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ] diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 3a76ac9..67db0e4 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -33,6 +33,9 @@ defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) : inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i +compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = + comp A (p @ i) [ (i = 1) -> q ] + isoId (A B : U) (f : A -> B) (g : B -> A) (s : (y:B) -> Id B (f (g y)) y) (t : (x:A) -> Id A (g (f x)) x) : Id U A B = -- 2.34.1