Adapted HITs

diff --git a/CTT.hs b/CTT.hs
index 01f727b9efedf8173e21077aea4bdd5e952f6458..1e9f5dedcf39a4394c597bf618575920a60444cb 100644 (file)
--- 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 5e847c71475c69a70c13dcb90fb10616741a82b5..5e7f27a240d3634765477c73ca55f6c85e7c0b4f 100644 (file)
--- 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 56758aca9862381dc8842e1305e8523134ef54d2..16d70c72c1479b61f95a2e0244b02dfb41809ad1 100644 (file)
--- 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 da38d53ec9e2d2804cce0997d8e0163cf1de1079..c7bea5fa10017ae8d476b26cbc4ccf21ce14b5e5 100644 (file)
--- 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\r
   Just as -> return (as,r)\r
   Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)\r
+getLblType c (Ter (HSum _ _ cas) r) = case lookupLabel c cas of\r
+  Just as -> return (as,r)\r
+  Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)\r
 getLblType c u = throwError ("expected a data type for the constructor "\r
                              ++ c ++ " but got " ++ show u)\r
 \r
@@ -148,6 +151,10 @@ check a t = case (a,t) of
   (VU,Pi f)       -> checkFam f\r
   (VU,Sigma f)    -> checkFam f\r
   (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
+    OLabel _ tele -> checkTele tele\r
+    PLabel _ tele is ts ->\r
+      throwError $ "check: no path constructor allowed in " ++ show t\r
+  (VU,HSum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
     OLabel _ tele -> checkTele tele\r
     PLabel _ tele is ts -> do\r
       checkTele tele\r
@@ -171,6 +178,14 @@ check a t = case (a,t) of
        then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
                       | (brc, lbl) <- zip ces cas ]\r
        else throwError "case branches does not match the data type"\r
+  (VPi va@(Ter (HSum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
+    check VU ty\r
+    rho <- asks env\r
+    unlessM (a === eval rho ty) $ throwError "check: split annotations"\r
+    if map labelName cas == map branchName ces\r
+       then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
+                      | (brc, lbl) <- zip ces cas ]\r
+       else throwError "case branches does not match the data type"\r
   (VPi a f,Lam x a' t)  -> do\r
     check VU a'\r
     ns <- asks names\r
@@ -409,11 +424,11 @@ infer e = case e of
   --   check a0 t\r
   --   return a1\r
   Comp a t0 ps -> do\r
-    checkPath (constPath VU) a\r
+    (va0, va1) <- checkPath (constPath VU) a\r
     va <- evalTyping a\r
-    check (va @@ Zero) t0\r
+    check va0 t0\r
     checkPathSystem t0 va ps\r
-    return (va @@ One)\r
+    return va1\r
   -- CompElem a es u us -> do\r
   --   check VU a\r
   --   rho <- asks env\r

diff --git a/examples/int.ctt b/examples/int.ctt
index dc4ccc0e5114a9a1e0110c6e2c834342c99dc61f..3b9958ea90460d39dbb3d590c026eb02bf3d83fd 100644 (file)
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -42,4 +42,4 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split
 \r
 sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ\r
 \r
-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 fd70c8378329f040f3fe9977681502bc9a6cc07e..332d99437d5b7a7779602fde713cb3a5f39c511e 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -60,15 +60,16 @@ p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (<i>zeroP'@-i)
 
 test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1
 
-test2 : Id T p0 p1 =
- <i j> comp int (pos zero)
-    [ (i = 1) ->
-  <k> comp int
-          (comp int (zeroP {int} @ j)
-          [ (j = 1) -> <l> zeroP {int} @ -l ])
-       [ (k = 0) -> <l> comp int (pos zero)
-                           [ (l = 0) -> <m> comp int (comp int (zeroP {int} @ (j /\ m))
-                                                          [ (m = 1) -> <n> comp int (zeroP {int} @ j)
-                                                                   [ (j = 1) -> <p> zeroP {int} @ (-n \/ -p) ] ])
-                                               [ (j = 1) -> <n> comp int (zeroP {int} @ (-n /\ m))
-                                                                   [ (m = 1) -> <p> zeroP {int} @ (-n /\ -p) ] ]]]]
\ No newline at end of file
+
+-- test2 : Id T p0 p1 =
+--  <i j> comp int (pos zero)
+--     [ (i = 1) ->
+--   <k> comp int
+--           (comp int (zeroP {int} @ j)
+--           [ (j = 1) -> <l> zeroP {int} @ -l ])
+--        [ (k = 0) -> <l> comp int (pos zero)
+--                            [ (l = 0) -> <m> comp int (comp int (zeroP {int} @ (j /\ m))
+--                                                           [ (m = 1) -> <n> comp int (zeroP {int} @ j)
+--                                                                    [ (j = 1) -> <p> zeroP {int} @ (-n \/ -p) ] ])
+--                                                [ (j = 1) -> <n> comp int (zeroP {int} @ (-n /\ m))
+--                                                                    [ (m = 1) -> <p> zeroP {int} @ (-n /\ -p) ] ]]]]
\ No newline at end of file

diff --git a/examples/nat.ctt b/examples/nat.ctt
index dec9d9289168726c1be4dc293aa42589cdaf925d..f084b83f3e7f28ae4967de621bf6b2ef897db8fc 100644 (file)
--- 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
+