From 0e3f53db68dc291141268e890ce17ee39bc8014c Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Thu, 4 Jun 2015 12:49:29 +0200 Subject: [PATCH] Adapted HITs --- CTT.hs | 7 ++-- Eval.hs | 80 +++++++++++++++++++++++++++++++------------- Resolver.hs | 5 +-- TypeChecker.hs | 21 ++++++++++-- examples/int.ctt | 2 +- examples/integer.ctt | 25 +++++++------- examples/nat.ctt | 3 ++ 7 files changed, 99 insertions(+), 44 deletions(-) diff --git a/CTT.hs b/CTT.hs index 01f727b..1e9f5de 100644 --- a/CTT.hs +++ b/CTT.hs @@ -177,7 +177,7 @@ data Val = VU | VUnGlueElem Val Val (System Val) | VUnGlueElemU Val Val (System Val) | VSplit Val Val - | VSqueezeH Val Val + -- | VHSqueeze Val Val Formula | VApp Val Val | VAppFormula Val Formula | VLam Ident Val Val @@ -207,8 +207,8 @@ isNeutral v = case v of VUnGlueElemU{} -> True _ -> False --- isNeutralSystem :: System Val -> Bool --- isNeutralSystem = any isNeutralPath . Map.elems +isNeutralSystem :: System Val -> Bool +isNeutralSystem = any isNeutral . Map.elems -- isNeutralPath :: Val -> Bool -- isNeutralPath (VPath _ v) = isNeutral v @@ -454,6 +454,7 @@ showVal v = case v of 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) + -- VHSqueeze a u phi -> text "hSqueeze" <+> showVals [a,u] <+> showFormula phi VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b | otherwise -> char '(' <> showLam v diff --git a/Eval.hs b/Eval.hs index 5e847c7..5e7f27a 100644 --- a/Eval.hs +++ b/Eval.hs @@ -69,6 +69,7 @@ instance Nominal Val where VCon _ vs -> support vs VPCon _ a vs phis -> support (a,vs,phis) VHComp a u ts -> support (a,u,ts) + -- VHSqueeze a u phi -> support (a,u,phi) VVar _ v -> support v VApp u v -> support (u,v) VLam _ u v -> support (u,v) @@ -106,7 +107,8 @@ 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) + VHComp a u us -> hComp (acti a) (acti u) (acti us) + -- VHSqueeze a u phi -> hSqueeze (acti a) (acti u) (acti phi) VVar x v -> VVar x (acti v) VAppFormula u psi -> acti u @@ acti psi VApp u v -> app (acti u) (acti v) @@ -141,6 +143,7 @@ instance Nominal Val where 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) + -- VHSqueeze a u phi -> VHSqueeze (sw a) (sw u) (sw phi) VVar x v -> VVar x (sw v) VAppFormula u psi -> VAppFormula (sw u) (sw psi) VApp u v -> VApp (sw u) (sw v) @@ -225,13 +228,13 @@ app u v = case (u,v) of (Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of Just (PBranch _ xs is t) -> eval (subs (zip is phis) (upds (zip xs us) e)) t _ -> error $ "app: missing case in split for " ++ c - (Ter (Split _ _ ty hbr) e,VComp a w ws) -> case eval e ty of + (Ter (Split _ _ ty hbr) e,VHComp a w ws) -> case eval e ty of VPi _ f -> let j = fresh (e,v) wsj = Map.map (@@ j) ws w' = app u w ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj -- a should be constant - in comp j (app f (fill j (a @@ j) w wsj)) w' ws' + in comp j (app f (fill j a w wsj)) w' ws' _ -> error $ "app: Split annotation not a Pi type " ++ show u (Ter Split{} _,_) | isNeutral v -> VSplit u v -- (Ter Split{} _,VCompElem _ _ w _) -> app u w @@ -386,10 +389,34 @@ transps _ _ _ _ = error "transps: different lengths of types and values" -- Given u of type a "squeeze i a u" connects in the direction i -- trans i a u(i=0) to u(i=1) squeeze :: Name -> Val -> Val -> Val -squeeze i a u = comp i a ui0 $ mkSystem [ (j ~> 0, transFill i a ui0) - , (j ~> 1, u) ] +squeeze i a u = comp i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] where j = fresh (Atom i,a,u) - ui0 = u `face` (i ~> 0) + ui1 = u `face` (i ~> 1) + +squeezeFill :: Name -> Val -> Val -> Val +squeezeFill i a u = fill i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ] + where j = fresh (Atom i,a,u) + ui1 = u `face` (i ~> 1) + + +squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] +squeezes i [] _ [] = [] +squeezes i ((x,a):as) e (u:us) = + let v = squeezeFill i (eval e a) u + vi1 = squeeze i (eval e a) u + vs = squeezes i as (upd (x,v) e) us + in vi1 : vs +squeezes _ _ _ _ = error "squeezes: different lengths of types and values" + +-- squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] +-- squeezes i xas rho us = comps i xas (rho `disj` (i,j)) +-- squeezes i [] _ [] = [] +-- squeezes i ((x,a):as) e (u:us) = +-- let v = squeeze i (eval e a) u +-- vs = squeezes i as (upd (x,v) e) us +-- in v : vs +-- squeezes _ _ _ _ = error "squeezes: different lengths of types and values" + -- squeezeNeg :: Name -> Val -> Val -> Val -- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u @@ -479,29 +506,36 @@ compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i) -- | HIT 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 - +compHIT i a u us + | isNeutral u || isNeutralSystem us = + VComp (VPath i a) u (Map.map (VPath i) us) + | otherwise = + hComp (a `face` (i ~> 1)) (transpHIT i a u) $ + mapWithKey (\alpha uAlpha -> + VPath i $ squeezeHIT i (a `face` alpha) uAlpha) us transpHIT :: Name -> Val -> Val -> Val 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 +-- 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 +squeezeHIT i a@(Ter (HSum _ _ nass) env) u = case u of + VCon n us -> case lookupLabel n nass of + Just as -> VCon n (squeezes i as env us) + Nothing -> error $ "squeezeHIT: missing constructor in labelled sum " ++ n + VPCon c _ ws0 phis -> case lookupLabel c nass of + Just as -> VPCon c (a `face` (i ~> 1)) (squeezes i as env ws0) phis + Nothing -> error $ "squeezeHIT: missing path constructor " ++ c + VHComp _ v vs -> + hComp (a `face` (i ~> 1)) (transpHIT i a v) $ + mapWithKey (\alpha vAlpha -> + VPath i $ squeezeHIT i (a `face` alpha) (vAlpha @@ i)) vs + _ -> error $ "squeezeHIT: neutral " ++ show u + +hComp :: Val -> Val -> System Val -> Val +hComp a u us | eps `Map.member` us = (us ! eps) @@ One + | otherwise = VHComp a u us ------------------------------------------------------------------------------- -- | Glue diff --git a/Resolver.hs b/Resolver.hs index 56758ac..16d70c7 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -297,9 +297,10 @@ resolveDecl d = case d of a <- binds CTT.Pi tele' (return CTT.U) let cs = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ] let pcs = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ] + let sum = if null pcs then CTT.Sum else CTT.HSum d <- lams tele' $ local (insertVar f) $ - CTT.Sum <$> getLoc l <*> pure f - <*> mapM (resolveLabel (cs ++ pcs)) sums + sum <$> getLoc l <*> pure f + <*> mapM (resolveLabel (cs ++ pcs)) sums return ((f,(a,d)),(f,Variable):cs ++ pcs) DeclSplit (AIdent (l,f)) tele t brs -> do let tele' = flattenTele tele diff --git a/TypeChecker.hs b/TypeChecker.hs index da38d53..c7bea5f 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -96,6 +96,9 @@ getLblType :: LIdent -> Val -> Typing (Tele, Env) getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of Just as -> return (as,r) Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas) +getLblType c (Ter (HSum _ _ cas) r) = case lookupLabel c cas of + Just as -> return (as,r) + Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas) getLblType c u = throwError ("expected a data type for the constructor " ++ c ++ " but got " ++ show u) @@ -148,6 +151,10 @@ check a t = case (a,t) of (VU,Pi f) -> checkFam f (VU,Sigma f) -> checkFam f (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of + OLabel _ tele -> checkTele tele + PLabel _ tele is ts -> + throwError $ "check: no path constructor allowed in " ++ show t + (VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of OLabel _ tele -> checkTele tele PLabel _ tele is ts -> do checkTele tele @@ -171,6 +178,14 @@ check a t = case (a,t) of then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va | (brc, lbl) <- zip ces cas ] else throwError "case branches does not match the data type" + (VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do + check VU ty + rho <- asks env + unlessM (a === eval rho ty) $ throwError "check: split annotations" + if map labelName cas == map branchName ces + then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va + | (brc, lbl) <- zip ces cas ] + else throwError "case branches does not match the data type" (VPi a f,Lam x a' t) -> do check VU a' ns <- asks names @@ -409,11 +424,11 @@ infer e = case e of -- check a0 t -- return a1 Comp a t0 ps -> do - checkPath (constPath VU) a + (va0, va1) <- checkPath (constPath VU) a va <- evalTyping a - check (va @@ Zero) t0 + check va0 t0 checkPathSystem t0 va ps - return (va @@ One) + return va1 -- CompElem a es u us -> do -- check VU a -- rho <- asks env diff --git a/examples/int.ctt b/examples/int.ctt index dc4ccc0..3b9958e 100644 --- a/examples/int.ctt +++ b/examples/int.ctt @@ -42,4 +42,4 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ -ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file +ZSet : set Z = corrhedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file diff --git a/examples/integer.ctt b/examples/integer.ctt index fd70c83..332d994 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -60,15 +60,16 @@ p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (zeroP'@-i) test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1 -test2 : Id T p0 p1 = - comp int (pos zero) - [ (i = 1) -> - comp int - (comp int (zeroP {int} @ j) - [ (j = 1) -> zeroP {int} @ -l ]) - [ (k = 0) -> comp int (pos zero) - [ (l = 0) -> comp int (comp int (zeroP {int} @ (j /\ m)) - [ (m = 1) -> comp int (zeroP {int} @ j) - [ (j = 1) ->

zeroP {int} @ (-n \/ -p) ] ]) - [ (j = 1) -> comp int (zeroP {int} @ (-n /\ m)) - [ (m = 1) ->

zeroP {int} @ (-n /\ -p) ] ]]]] \ No newline at end of file + +-- test2 : Id T p0 p1 = +-- comp int (pos zero) +-- [ (i = 1) -> +-- comp int +-- (comp int (zeroP {int} @ j) +-- [ (j = 1) -> zeroP {int} @ -l ]) +-- [ (k = 0) -> comp int (pos zero) +-- [ (l = 0) -> comp int (comp int (zeroP {int} @ (j /\ m)) +-- [ (m = 1) -> comp int (zeroP {int} @ j) +-- [ (j = 1) ->

zeroP {int} @ (-n \/ -p) ] ]) +-- [ (j = 1) -> comp int (zeroP {int} @ (-n /\ m)) +-- [ (m = 1) ->

zeroP {int} @ (-n /\ -p) ] ]]]] \ No newline at end of file diff --git a/examples/nat.ctt b/examples/nat.ctt index dec9d92..f084b83 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -1,6 +1,7 @@ module nat where import prelude +import newhedberg data nat = zero | suc (n : nat) @@ -54,3 +55,5 @@ natDec : (n m:nat) -> dec (Id nat n m) = split (sucInj n m) (natDec n m)) -- natSet : set nat = hedberg nat natDec +natSet : set nat = corrhedberg nat natDec + -- 2.34.1