Allow computing past 'case'

It's possible to move many elimination forms into 'case', unsticking
computations.

Additionally: Prove that T² ≃ S¹ × S¹

intro.tt

@@ -893,4 +893,58 @@ poSusp_to_Susp_to_poSusp {A} = \case
   push x i -> refl
 
 Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)
-Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
+Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
+
+data T2 : Type where
+  baseT : T2
+  pathOne i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
+  pathTwo i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
+  square i j : T2 [
+      (j = i0) -> pathTwo i,
+      (j = i1) -> pathTwo i,
+      (i = i0) -> pathOne j,
+      (i = i1) -> pathOne j
+    ]
+
+torusToCircs : T2 -> S1 * S1
+torusToCircs = \case
+  baseT -> (base, base)
+  pathOne i -> (loop i, base)
+  pathTwo i -> (base, loop i)
+  square i j -> (loop i, loop j)
+
+circsToTorus : ((x : S1) * S1) -> T2
+circsToTorus pair = go pair.1 pair.2
+  where
+    baseCase : S1 -> T2
+    baseCase = \case
+      base -> baseT
+      loop j -> pathTwo j
+
+    loopCase : Path baseCase baseCase
+    loopCase i = \case
+      base -> pathOne i
+      loop j -> square i j
+
+    go : S1 -> S1 -> T2
+    go = \case
+      base -> baseCase
+      loop i -> loopCase i
+
+torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
+torusToCircsToTorus = \case
+  baseT -> refl
+  pathOne i -> refl
+  pathTwo i -> refl
+  square i j -> refl
+
+postulate
+  exerciseForTomorrow : {A : Type} -> A
+
+circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
+circsToTorusToCircs = exerciseForTomorrow
+
+TorusIsTwoCircles : Path T2 (S1 * S1)
+TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
+  theIso : Iso T2 (S1 * S1)
+  theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)

src/Elab.hs

@@ -31,6 +31,7 @@ import Prettyprinter
 
 import Syntax.Pretty
 import Syntax
+import Data.Maybe (fromMaybe)
 
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
@@ -226,11 +227,12 @@ check (P.LamCase pats) ty =
                 let
                   base = appDummies (VVar <$> dummies) ty rhs_nf
                   sys = boundaryFormulas (drop a dummies ++ getBoundaryNames boundary) (getBoundaryMap boundary)
-                
+
                 for_ (Map.toList sys) \(formula, side) -> do
                   let rhs = cases @@ side
                   for_ (truthAssignments formula mempty) $ \i -> do
-                    let vl = foldl (\v n -> vApp P.Ex v (snd (i Map.! n))) base (getBoundaryNames boundary)
+                    let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary)
+                        lookup n = fromMaybe VI0 (snd <$> (Map.lookup n i))
                     unify vl rhs
                       `withNote` vcat [ pretty "These must be the same because of the face"
                                       , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
@@ -253,7 +255,7 @@ check (P.LamCase pats) ty =
       n <- newName
       (p, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
       checkPatterns rng ((p, t):acc) xs k
-    
+
     appDummies (v:vl) (VPi p _ (Closure _ r)) x = appDummies vl (r v) (vApp p x v)
     appDummies [] _ x = x
     appDummies vs t _ = error (show (vs, t))
@@ -507,7 +509,7 @@ checkStatement (P.Data name tele retk constrs) k =
   do
     checkTeleRetk True tele retk \kind tele undef -> do
       kind_nf <- eval kind
-      defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' -> 
+      defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
         checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
   where
     makeProj (x, p, _) = PApp p (VVar x)
@@ -546,7 +548,7 @@ checkStatement (P.Data name tele retk constrs) k =
       unify ret' ret
       closed_nf <- eval closed
       defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
-    
+
     checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
       (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
         t <- check return VTypeω
@@ -569,7 +571,7 @@ checkStatement (P.Data name tele retk constrs) k =
           phi <- checkFormula f
           t <- check t ret
           pure (phi, (quote phi, t))
-        
+
         system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd faces))) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices)
 
         unify (foldr ior VI0 (map fst faces)) (totalProp indices)

src/Elab/Eval.hs

@@ -13,7 +13,9 @@ import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
 import qualified Data.Set as Set
 import qualified Data.Text as T
+import Data.Map.Strict (Map)
 import Data.Sequence (Seq)
+import Data.List (sortOn)
 import Data.Traversable
 import Data.Set (Set)
 import Data.Typeable
@@ -36,10 +38,10 @@ import Syntax
 import System.IO.Unsafe
 
 import {-# SOURCE #-} Elab.WiredIn
-import Data.List (sortOn)
-import Data.Map.Strict (Map)
+import Control.Arrow (second)
+import Debug.Trace
 
-eval :: Term -> ElabM Value
+eval :: HasCallStack => Term -> ElabM Value
 eval t = asks (flip eval' t)
 
 -- everywhere force
@@ -106,7 +108,7 @@ zonkSp PProj2 = pure PProj2
 zonk :: Value -> Value
 zonk = unsafePerformIO . zonkIO
 
-eval' :: ElabEnv -> Term -> Value
+eval' :: HasCallStack => ElabEnv -> Term -> Value
 eval' env (Ref x) =
   case Map.lookup x (getEnv env) of
     Just (_, vl) -> vl
@@ -187,11 +189,11 @@ evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (
 
 evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
 
-evalCase env rng (VHComp a phi u a0) cases = 
+evalCase env rng (VHComp a phi u a0) cases =
   comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases)
          (VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases))
   where
-    v = Elab.WiredIn.fill a phi u a0
+    v = Elab.WiredIn.fill (fun (const a)) phi u a0
 
 evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc
 
@@ -570,9 +572,13 @@ forceIO (GluedVl _ _ vl) = forceIO vl
 forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
 forceIO (VCase env rng v vs) = do
   env' <- liftIO emptyEnv
-  evalCase env'{getEnv=env} . (@@) <$> forceIO rng <*> forceIO v <*> pure vs
+  r <- forceIO rng
+  evalCase env'{getEnv=env} (r @@) <$> forceIO v <*> pure vs
 forceIO x = pure x
 
+force :: Value -> Value
+force = unsafePerformIO . forceIO
+
 applProj :: Value -> Projection -> Value
 applProj fun (PApp p arg)     = vApp p fun arg
 applProj fun (PIElim l x y i) = ielim l x y fun i
@@ -580,9 +586,6 @@ applProj fun (POuc a phi u)   = outS a phi u fun
 applProj fun PProj1           = vProj1 fun
 applProj fun PProj2           = vProj2 fun
 
-force :: Value -> Value
-force = unsafePerformIO . forceIO
-
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
   | p == p'   = clCont k arg
@@ -591,6 +594,9 @@ vApp p (VNe h sp) arg    = VNe h (sp Seq.:|> PApp p arg)
 vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
 vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
 vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
+vApp p (VCase env rng sc branches) arg =
+  VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
+    (map (second (projIntoCase (flip (App p) (quote arg)))) branches)
 vApp _ x _             = error $ "can't apply " ++ show (prettyTm (quote x))
 
 (@@) :: HasCallStack => Value -> Value -> Value
@@ -603,6 +609,8 @@ vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
 vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl)
 vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
 vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c)
+vProj1 (VCase env rng sc branches) =
+  VCase env (fun \x -> let VSigma a _ = rng @@ x in a) sc (map (second (projIntoCase Proj1)) branches)
 vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
 
 vProj2 :: HasCallStack => Value -> Value
@@ -611,4 +619,11 @@ vProj2 (VNe h sp)  = VNe h (sp Seq.:|> PProj2)
 vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl)
 vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
 vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c)
-vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
+vProj2 (VCase env rng sc branches) =
+  VCase env (fun \x -> let VSigma _ (Closure _ r) = rng @@ x in r (vProj1 x)) sc (map (second (projIntoCase Proj2)) branches)
+vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
+
+projIntoCase :: (Term -> Term) -> Term -> Term
+projIntoCase f (Lam p x r) = Lam p x (projIntoCase f r)
+projIntoCase f (PathIntro l a b r) = PathIntro l a b (projIntoCase f r)
+projIntoCase f x = f x

src/Elab/WiredIn.hs

@@ -216,7 +216,7 @@ outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
 comp _a VI1 u _a0 =  u @@ VI1 @@ VItIsOne
 comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
-  case force $ a @@ VVar compVar of
+  case force (a @@ VVar name) of
     VPi{} ->
       let
         plic i = let VPi p _ _ = force (a @@ i)              in p
@@ -263,9 +263,9 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
       in
       let
         base i   = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
-        phi i    = substitute (Map.singleton compVar i) thePhi
-        types i  = substitute (Map.singleton compVar i) theTypes @@ VItIsOne
-        equivs i = substitute (Map.singleton compVar i) theEquivs
+        phi i    = substitute (Map.singleton name i) thePhi
+        types i  = substitute (Map.singleton name i) theTypes @@ VItIsOne
+        equivs i = substitute (Map.singleton name i) theEquivs
 
         a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
         a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
@@ -295,7 +295,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
        in b1
 
     VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
-                            (fun' "is1" \_ -> mapVSystem makeEquiv (u @@ VVar equivVar @@ VItIsOne))
+                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
 
     VNe (HData False _) Seq.Empty -> a0
     VNe (HData False _) args ->
@@ -303,13 +303,19 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
         VNe (HCon con_type con_name) con_args ->
           VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u
         _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
-    
+
     VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0
 
     VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
     sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
 
     _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
+  where
+    {-# NOINLINE name #-}
+    name = unsafePerformIO newName
+
+    {-# NOINLINE equivVar #-}
+    equivVar = unsafePerformIO newName
 
 mapVSystem :: (Value -> Value) -> Value -> Value
 mapVSystem f (VSystem fs) = VSystem (fmap f fs)
@@ -321,7 +327,12 @@ forceAndGlue v =
     v@VGlueTy{} -> v
     y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))
 
-compHIT :: Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
+compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
+compHIT 0 a phi u a0 =
+  case phi of
+    VI1 -> u @@ VI1 @@ VItIsOne
+    VI0 -> compOutS (a VI0) phi u a0
+    _ -> VHComp (a VI0) phi u a0
 compHIT _ a phi u a0 = error $ unlines
   [ "*** TODO: composition for HIT: "
   , "domain = " ++ show (prettyTm (quote (zonk (fun a))))
@@ -357,6 +368,9 @@ compConArgs total_args fam = go total_args where
 
   smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
 
+  typeArgument = unsafePerformIO newName
+  {-# NOINLINE typeArgument #-}
+
 compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
 compOutS a b c d = compOutS a b c (force d) where
   compOutS _ _hi _0 vl@VComp{}   = vl
@@ -447,10 +461,10 @@ contr a aC phi u =
 transp :: (NFEndp -> Value) -> Value -> Value
 transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
 
-makeEquiv :: Value -> Value
-makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
+makeEquiv :: Name -> Value -> Value
+makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
   where
-    line = fun \i -> substitute (Map.singleton equivVar (inot i)) argh
+    line = fun \i -> substitute (Map.singleton var (inot i)) vne
     a = line @@ VI0
     b = line @@ VI1
 
@@ -487,14 +501,4 @@ idEquiv a = VPair idfun idisequiv where
       VLine (fun (const a)) y (vProj1 u) $ fun \j ->
         ielim (fun (const a)) y y (vProj2 u) (iand i j)
 
-  id_fiber y = VPair y (VLine a y y (fun (const y)))
-
--- magic variables (:vomit:)
-compVar :: Name -- direction of composition
-compVar = Bound (T.pack "_comp_dir") (negate 1)
-
-equivVar :: Name --  direction of equivalence
-equivVar = Bound (T.pack "_equiv_dir") (negate 2)
-
-typeArgument :: Name -- marker for type arguments in composition
-typeArgument = Bound (T.pack "_comp_con_tyarg") (negate 3)
+  id_fiber y = VPair y (VLine a y y (fun (const y)))