From: Simon Huber Date: Wed, 18 Mar 2015 23:54:52 +0000 (+0100) Subject: added transport X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0100fea387bcb4127b83089f067b2f595678ee20;p=cubicaltt.git added transport --- diff --git a/Eval.hs b/Eval.hs index 936f59f..8915535 100644 --- a/Eval.hs +++ b/Eval.hs @@ -30,7 +30,7 @@ lookName :: Name -> Env -> Formula lookName i (Pair rho _) = lookName i rho lookName i (Def _ rho) = lookName i rho lookName i (Sub rho (j,phi)) | i == j = phi - | otherwise = lookName i rho + | otherwise = lookName i rho ----------------------------------------------------------------------- -- Nominal instances @@ -47,15 +47,16 @@ instance Nominal Val where 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 (VSPair 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 (VApp u v) = support (u,v) + support (VAppFormula u phi) = support (u,phi) + support (VSplit u v) = support (u,v) act u (i, phi) = let acti :: Nominal a => a -> a @@ -68,8 +69,9 @@ instance Nominal Val where VComp a v ts -> comp (acti a) (acti v) (acti ts) VIdP a u v -> VIdP (acti a) (acti u) (acti v) VPath j v | j `notElem` sphi -> VPath j (acti v) - | otherwise -> VPath k (v `swap` (j,k)) + | otherwise -> VPath k (v `swap` (j,k)) where k = fresh (v, Atom i, phi) + VTrans u v -> trans' (acti u) (acti v) VSigma a f -> VSigma (acti a) (acti f) VSPair u v -> VSPair (acti u) (acti v) VFst u -> VFst (acti u) @@ -91,6 +93,7 @@ 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) VSPair u v -> VSPair (sw u) (sw v) VFst u -> VFst (sw u) @@ -103,7 +106,7 @@ instance Nominal Val where ----------------------------------------------------------------------- -- The evaluator - + eval :: Env -> Ter -> Val eval rho v = case v of U -> VU @@ -121,14 +124,13 @@ eval rho v = case v of Sum pr lbls -> Ter (Sum pr lbls) rho Undef l -> error $ "eval: undefined at " ++ show l IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) - Path i t -> + Path i t -> let j = fresh rho in VPath j (eval (Sub rho (i,Atom j)) t) - Trans u v -> case eval rho u of - VPath i u0 -> trans i u0 (eval rho v) - u0 -> VTrans u0 (eval rho v) + Trans u v -> trans' (eval rho u) (eval rho v) AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi) --- Comp + +-- Comp evalFormula :: Env -> Formula -> Formula evalFormula rho phi = case phi of @@ -165,13 +167,18 @@ v @@ phi = VAppFormula v (toFormula phi) ----------------------------------------------------------- -- Transport +trans' :: Val -> Val -> Val +trans' u v = case u of + VPath i u0 -> trans i u0 v + u0 -> VTrans u0 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) ts' = mkSystem [(j ~> 0,u),(j ~> 1,v)] in VPath j $ genComp i (a @@ j) (w @@ j) ts' - (VSigma a f,u) -> + (VSigma a f,u) -> let (u1,u2) = (fstVal u,sndVal u) fill_u1 = transFill i a u1 ui1 = trans i a u1 @@ -244,7 +251,7 @@ comps _ _ _ _ = error "comps: different lengths of types and values" conv :: Int -> Val -> Val -> Bool conv k u v | u == v = True | otherwise = let j = fresh (u,v) in case (u,v) of - (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> + (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> let v = mkVar k (eval e a) in conv (k+1) (eval (Pair e (x,v)) u) (eval (Pair e' (x',v)) u') (Ter (Lam x a u) e,u') -> @@ -274,7 +281,10 @@ conv k u v | u == v = True (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c' (VPath i a,VPath i' a') -> conv k (a `swap` (i,j)) (a' `swap` (i',j)) (VPath i a,p') -> conv k (a `swap` (i,j)) (p' @@ j) - (p,VPath i' a') -> conv k (p @@ j) (a' `swap` (i',j)) + (p,VPath i' a') -> conv k (p @@ j) (a' `swap` (i',j)) + (VTrans p u,v) | isIndep k j (p @@ j) -> conv k u v + (u,VTrans p v) | isIndep k j (p @@ j) -> conv k u v + (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u' -- VAppformula -- VTrans -- VComp @@ -282,3 +292,6 @@ conv k u v | u == v = True convEnv :: Int -> Env -> Env -> Bool convEnv k e e' = and $ zipWith (conv k) (valOfEnv e) (valOfEnv e') + +isIndep :: Int -> Name -> Val -> Bool +isIndep k i u = conv k u (u `face` (i ~> 0)) diff --git a/TypeChecker.hs b/TypeChecker.hs index 0595e37..13ca00b 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -156,7 +156,8 @@ check a t = case (a,t) of (VU,IdP a e0 e1) -> case a of Path i b -> do rho <- asks env - when (i `elem` support rho) (throwError (show i ++ " is already declared")) + when (i `elem` support rho) + (throwError (show i ++ " is already declared")) local (addSub (i,Atom i)) $ check VU b check (eval (Sub rho (i,Dir 0)) b) e0 check (eval (Sub rho (i,Dir 1)) b) e1 @@ -169,7 +170,8 @@ check a t = case (a,t) of _ -> throwError ("IdP expects a path but got " ++ show a) (VIdP p a b,Path i e) -> do rho <- asks env - when (i `elem` support rho) (throwError (show i ++ " is already declared")) + when (i `elem` support rho) + (throwError (show i ++ " is already declared")) local (addSub (i,Atom i)) $ check (p @@ i) e _ -> do v <- infer t @@ -234,7 +236,20 @@ infer e = case e of t <- infer e case t of VIdP a _ _ -> return $ a @@ phi - _ -> throwError (show e ++ " is not a path") + _ -> throwError (show e ++ " is not a path") + Trans p t -> case p of + Path i a -> do + rho <- asks env + when (i `elem` support rho) + (throwError $ show i ++ " is already declared") + local (addSub (i,Atom i)) $ check VU a + check (eval (Sub rho (i,Dir 0)) a) t + return $ (eval (Sub rho (i,Dir 1)) a) + _ -> do + b <- infer p + case b of + VIdP (VPath _ VU) _ b1 -> return b1 + _ -> throwError $ "transport expects a path but got " ++ show p _ -> throwError ("infer " ++ show e) checks :: (Tele,Env) -> [Ter] -> Typing () diff --git a/examples/nat.ctt b/examples/nat.ctt index 8f831fc..5c36a48 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -55,10 +55,13 @@ test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id zero -> refl nat zero suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n) --- subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = --- transport (mapOnPath A U P a b p) e +subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = + transport (mapOnPath A U P a b p) e + +substRefl (A : U) (P : A -> U) (a : A) (e : P a) : Id (P a) (subst A P a a (refl A a) e) e = + refl (P a) e singl (A : U) (a : A) : U = (x : A) * Id A a x contrSingl (A : U) (a b : A) (p : Id A a b) : - Id (singl A a) (a,refl A a) (b,p) = (p @ ?0, p @ ?0 & ?1) \ No newline at end of file + Id (singl A a) (a,refl A a) (b,p) = (p @ ?0, p @ ?0 & ?1)