From: Simon Huber Date: Mon, 31 Aug 2015 14:19:16 +0000 (+0200) Subject: Added Eq types with definitional equality for J X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=63d12c97842bc9c6692b928a9b31050cae709a1a;p=cubicaltt.git Added Eq types with definitional equality for J --- diff --git a/CTT.hs b/CTT.hs index 944c51c..f974c4b 100644 --- a/CTT.hs +++ b/CTT.hs @@ -119,6 +119,10 @@ data Ter = Pi Ter | Glue Ter (System Ter) | GlueElem Ter (System Ter) | UnGlueElem Ter (System Ter) + -- Eq + | Eq Ter Ter Ter + | EqPair Ter (System Ter) + | EqJ Ter Ter Ter Ter Ter Ter deriving Eq -- For an expression t, returns (u,ts) where u is no application and t = u ts @@ -163,6 +167,10 @@ data Val = VU -- Composition for HITs; the type is constant | VHComp Val Val (System Val) + -- Eq + | VEq Val Val Val + | VEqPair Val (System Val) + -- Neutral values: | VVar Ident Val | VOpaque Ident Val @@ -173,23 +181,25 @@ data Val = VU | VAppFormula Val Formula | VLam Ident Val Val | VUnGlueElemU Val Val (System Val) + | VEqJ Val Val Val Val Val Val deriving Eq isNeutral :: Val -> Bool isNeutral v = case v of - Ter Undef{} _ -> True - Ter Hole{} _ -> True - VVar{} -> True - VOpaque{} -> True - VComp{} -> True - VFst{} -> True - VSnd{} -> True - VSplit{} -> True - VApp{} -> True - VAppFormula{} -> True - VUnGlueElemU{} -> True - VUnGlueElem{} -> True - _ -> False + Ter Undef{} _ -> True + Ter Hole{} _ -> True + VVar{} -> True + VOpaque{} -> True + VComp{} -> True + VFst{} -> True + VSnd{} -> True + VSplit{} -> True + VApp{} -> True + VAppFormula{} -> True + VUnGlueElemU{} -> True + VUnGlueElem{} -> True + VEqJ{} -> True + _ -> False isNeutralSystem :: System Val -> Bool isNeutralSystem = any isNeutral . elems @@ -373,6 +383,9 @@ showTer v = case v of Glue a ts -> text "Glue" <+> showTer1 a <+> text (showSystem ts) GlueElem a ts -> text "glue" <+> showTer1 a <+> text (showSystem ts) UnGlueElem a ts -> text "unglue" <+> showTer1 a <+> text (showSystem ts) + Eq a u v -> text "Eq" <+> showTers [a,u,v] + EqPair b ts -> text "eqC" <+> showTer1 b <+> text (showSystem ts) + EqJ a t c d x p -> text "eqJ" <+> showTers [a,t,c,d,x,p] showTers :: [Ter] -> Doc showTers = hsep . map showTer1 diff --git a/Connections.hs b/Connections.hs index 077d575..4d8b524 100644 --- a/Connections.hs +++ b/Connections.hs @@ -403,6 +403,11 @@ unionSystem :: System a -> System a -> System a unionSystem us vs = insertsSystem (assocs us) vs +joinSystem :: System (System a) -> System a +joinSystem tss = mkSystem $ + [ (alpha `meet` beta,t) | (alpha,ts) <- assocs tss, (beta,t) <- assocs ts ] + + -- TODO: add some checks transposeSystemAndList :: System [a] -> [b] -> [(System a,b)] transposeSystemAndList _ [] = [] diff --git a/Eval.hs b/Eval.hs index 90d862f..3b60833 100644 --- a/Eval.hs +++ b/Eval.hs @@ -77,6 +77,9 @@ instance Nominal Val where VUnGlueElem a ts -> support (a,ts) VCompU a ts -> support (a,ts) VUnGlueElemU a b es -> support (a,b,es) + VEqPair u us -> support (u,us) + VEq a u v -> support (a,u,v) + VEqJ a u c d x p -> support [a,u,c,d,x,p] act u (i, phi) | i `notElem` support u = u | otherwise = @@ -111,6 +114,10 @@ instance Nominal Val where VUnGlueElem a ts -> unglueElem (acti a) (acti ts) VUnGlueElemU a b es -> unGlueU (acti a) (acti b) (acti es) VCompU a ts -> compUniv (acti a) (acti ts) + VEqPair u us -> VEqPair (acti u) (acti us) + VEq a u v -> VEq (acti a) (acti u) (acti v) + VEqJ a u c d x p -> + eqJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p) -- This increases efficiency as it won't trigger computation. swap u ij@(i,j) = @@ -141,7 +148,10 @@ instance Nominal Val where VUnGlueElem a ts -> VUnGlueElem (sw a) (sw ts) VUnGlueElemU a b es -> VUnGlueElemU (sw a) (sw b) (sw es) VCompU a ts -> VCompU (sw a) (sw ts) - + VEqPair u us -> VEqPair (sw u) (sw us) + VEq a u v -> VEq (sw a) (sw u) (sw v) + VEqJ a u c d x p -> + VEqJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p) ----------------------------------------------------------------------- -- The evaluator @@ -179,6 +189,10 @@ eval rho@(_,_,_,Nameless os) v = case v of Glue a ts -> glue (eval rho a) (evalSystem rho ts) GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts) UnGlueElem a ts -> unglueElem (eval rho a) (evalSystem rho ts) + Eq a r s -> VEq (eval rho a) (eval rho r) (eval rho s) + EqPair b ts -> VEqPair (eval rho b) (evalSystem rho ts) + EqJ a t c d x p -> eqJ (eval rho a) (eval rho t) (eval rho c) + (eval rho d) (eval rho x) (eval rho p) _ -> error $ "Cannot evaluate " ++ show v evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] @@ -266,6 +280,7 @@ inferType v = case v of VComp a _ _ -> a @@ One -- VUnGlueElem _ b _ -> b -- This is wrong! Store the type?? VUnGlueElemU _ b _ -> b + VEqJ _ _ c _ x p -> app (app c x) p _ -> error $ "inferType: not neutral " ++ show v (@@) :: ToFormula a => Val -> a -> Val @@ -292,6 +307,16 @@ comp i a u ts = case a of VPathP p v0 v1 -> let j = fresh (Atom i,a,u,ts) in VPLam j $ comp i (p @@ j) (u @@ j) $ insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts) + VEq b v0 v1 -> case u of + VEqPair r _ | all isEqPair (elems ts) -> + let j = fresh (Atom i,a,u,ts) + VEqPair z _ @@@ phi = z @@ phi + sys (VEqPair _ ws) = ws + w = VPLam j $ comp i b (r @@ j) $ + insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] + (Map.map (@@@ j) ts) + in VEqPair w (joinSystem (Map.map sys (ts `face` (i ~> 1)))) + _ -> VComp (VPLam i a) u (Map.map (VPLam i) 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) @@ -398,6 +423,23 @@ squeezes i xas e us = comps j xas (e `disj` (i,j)) us' us' = [ (mkSystem [(i ~> 1, u `face` (i ~> 1))],u) | u <- us ] +------------------------------------------------------------------------------- +-- | Eq + +eqJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val +eqJ a v c d x p = case p of + VEqPair w ws -> comp i (app (app c (w @@ i)) w') d + (border d (shape ws)) + where w' = VEqPair (VPLam j $ w @@ (Atom i :/\: Atom j)) + (insertSystem (i ~> 0) v ws) + i:j:_ = freshs [a,v,c,d,x,p] + _ -> VEqJ a v c d x p + +isEqPair :: Val -> Bool +isEqPair VEqPair{} = True +isEqPair _ = False + + ------------------------------------------------------------------------------- -- | HITs @@ -842,7 +884,11 @@ instance Convertible Val where (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') - _ -> False + (VEqPair v vs,VEqPair v' vs') -> conv ns (v,vs) (v',vs') + (VEq a u v,VEq a' u' v') -> conv ns (a,u,v) (a',u',v') + (VEqJ a u c d x p,VEqJ a' u' c' d' x' p') -> + conv ns [a,u,c,d,x,p] [a',u',c',d',x',p'] + _ -> False instance Convertible Ctxt where conv _ _ _ = True @@ -909,6 +955,10 @@ instance Normal Val where VSplit u t -> VSplit (normal ns u) (normal ns t) VApp u v -> app (normal ns u) (normal ns v) VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi) + VEq a u v -> VEq (normal ns a) (normal ns u) (normal ns v) + VEqPair u us -> VEqPair (normal ns u) (normal ns us) + VEqJ a u c d x p -> eqJ (normal ns a) (normal ns u) (normal ns c) + (normal ns d) (normal ns x) (normal ns p) _ -> v instance Normal (Nameless a) where diff --git a/Exp.cf b/Exp.cf index d5afd2f..29cfb0e 100644 --- a/Exp.cf +++ b/Exp.cf @@ -42,6 +42,9 @@ Fill. Exp3 ::= "fill" Exp4 Exp4 System ; Glue. Exp3 ::= "Glue" Exp4 System ; GlueElem. Exp3 ::= "glue" Exp4 System ; UnGlueElem. Exp3 ::= "unglue" Exp4 System ; +Eq. Exp3 ::= "Eq" Exp4 Exp4 Exp3 ; +EqPair. Exp3 ::= "eqC" Exp4 System ; +EqJ. Exp3 ::= "eqJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ; Fst. Exp4 ::= Exp4 ".1" ; Snd. Exp4 ::= Exp4 ".2" ; Pair. Exp5 ::= "(" Exp "," [Exp] ")" ; diff --git a/Resolver.hs b/Resolver.hs index 0871c89..9cd9890 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -219,6 +219,10 @@ resolveExp e = case e of Glue u ts -> CTT.Glue <$> resolveExp u <*> resolveSystem ts GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts UnGlueElem u ts -> CTT.UnGlueElem <$> resolveExp u <*> resolveSystem ts + Eq a u v -> CTT.Eq <$> resolveExp a <*> resolveExp u <*> resolveExp v + EqPair u ts -> CTT.EqPair <$> resolveExp u <*> resolveSystem ts + EqJ a t c d x p -> CTT.EqJ <$> resolveExp a <*> resolveExp t <*> resolveExp c + <*> resolveExp d <*> resolveExp x <*> resolveExp p _ -> do modName <- asks envModule throwError ("Could not resolve " ++ show e ++ " in module " ++ modName) diff --git a/TypeChecker.hs b/TypeChecker.hs index 2427e02..8b74327 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -215,6 +215,22 @@ check a t = case (a,t) of check va u vu <- evalTyping u checkGlueElemU vu ves us + (VU,Eq a a0 a1) -> do + check VU a + va <- evalTyping a + check va a0 + check va a1 + (VEq va va0 va1,EqPair w ts) -> do + check (VPathP (constPath va) va0 va1) w + vw <- evalTyping w + checkSystemWith ts $ \alpha tAlpha -> + local (faceEnv alpha) $ do + check (va `face` alpha) tAlpha + vtAlpha <- evalTyping tAlpha + unlessM (vw `face` alpha === constPath vtAlpha) $ + throwError "malformed eqC" + rho <- asks env + checkCompSystem (evalSystem rho ts) -- Not needed _ -> do v <- infer t unlessM (v === a) $ @@ -338,6 +354,8 @@ mkEquiv va = eval rho $ checkEquiv :: Val -> Ter -> Typing () checkEquiv va equiv = check (mkEquiv va) equiv +checkIso :: Val -> Ter -> Typing () +checkIso vb iso = check (mkIso vb) iso checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do @@ -480,6 +498,23 @@ infer e = case e of checks (bs,nu) es mapM_ checkFormula phis return va + EqJ a u c d x p -> do + check VU a + va <- evalTyping a + check va u + vu <- evalTyping u + let refu = VEqPair (constPath vu) $ mkSystem [(eps,vu)] + rho <- asks env + let z = Var "z" + ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Eq a u z) U + check ctype c + vc <- evalTyping c + check (app (app vc vu) refu) d + check va x + vx <- evalTyping x + check (VEq va vu vx) p + vp <- evalTyping p + return (app (app vc vx) vp) _ -> throwError ("infer " ++ show e) -- Not used since we have U : U