Check in more experiments I had locally

* Remove [φ] since it's the same thing as φ ≡s i1

* Change the type of comp to reflect that the returned element agrees
  with the sides on i1.

cubical.cabal

@@ -46,8 +46,9 @@ executable cubical
                      , Elab.WiredIn
                      , Elab.Eval.Formula
 
+                     , Debug
+
   build-tool-depends:  alex:alex >= 3.2.4 && < 4.0
                     ,  happy:happy >= 1.19.12 && < 2.0
 
-  ghc-options:         -Wall -Wextra -Wno-name-shadowing
-
+  ghc-options:         -Wall -Wextra -Wno-name-shadowing -rtsopts

src/Debug.hs

@@ -0,0 +1,45 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE BangPatterns #-}
+#undef RELEASE
+module Debug where
+
+import qualified Debug.Trace as D
+
+#if defined(RELEASE)
+import GHC.Exts
+#endif
+
+import GHC.Stack
+import Prettyprinter
+import qualified Data.Text.Lazy as T
+import Data.Text.Prettyprint.Doc.Render.Text (renderLazy)
+
+traceDoc :: Doc a -> b -> b
+
+#if defined(RELEASE)
+type DebugCallStack = (() :: Constraint)
+traceDoc !_ v = v
+#else
+type DebugCallStack = HasCallStack
+traceDoc x = D.trace (T.unpack (renderLazy (layoutPretty defaultLayoutOptions x)))
+#endif
+
+trace :: Pretty a => a -> b -> b
+trace x = traceDoc (pretty x)
+
+traceWith :: Pretty a => String -> a -> b -> b
+traceWith s x = traceDoc (pretty s <+> pretty x)
+
+traceId :: Pretty a => a -> a
+traceId x = traceDoc (pretty x) x
+
+traceWithId :: Pretty a => String -> a -> a
+traceWithId s x = traceWith s x x
+
+traceDocM :: (Applicative m) => Doc a -> m ()
+traceDocM x = traceDoc x (pure ())
+
+traceM :: (Applicative m, Pretty a) => a -> m ()
+traceM = traceDocM . pretty

src/Elab.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE EmptyCase #-}
 module Elab where
 
 import Control.Arrow (Arrow(first))
@@ -14,6 +15,7 @@ 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.Maybe (fromMaybe)
 import Data.Traversable
 import Data.Text (Text)
 import Data.Map (Map)
@@ -53,10 +55,10 @@ infer (P.App p f x) = do
       x_nf <- eval x
       pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
     It'sPartial phi a w -> do
-      x <- check x (VIsOne phi)
+      x <- check x (VEqStrict VI phi VI1)
       pure (App P.Ex (w f) x, a)
     It'sPartialP phi a w -> do
-      x <- check x (VIsOne phi)
+      x <- check x (VEqStrict VI phi VI1)
       x_nf <- eval x
       pure (App P.Ex (w f) x, a @@ x_nf)
 
@@ -100,20 +102,17 @@ check (P.Lam p v b) ty = do
 
       tm_nf <- eval tm
 
-      unify (tm_nf @@ VI0) le
-        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
-
-      unify (tm_nf @@ VI1) ri
-        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
+      unify (tm_nf @@ VI0) le `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI0)
+      unify (tm_nf @@ VI1) ri `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI1)
 
       pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
     It'sPartial phi a wp ->
-      assume (Bound v 0) (VIsOne phi) $ \var ->
+      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
         wp . Lam p var <$> check b a
 
     It'sPartialP phi a wp ->
-      assume (Bound v 0) (VIsOne phi) $ \var ->
+      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
         wp . Lam p var <$> check b (a @@ VVar var)
 
 check (P.Pair a b) ty = do
@@ -146,54 +145,36 @@ check (P.Let items body) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
-  let dom_q = quote dom
-  eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
-    phi <- checkFormula (P.condF formula)
-    rhses <-
-        case P.condV formula of
-          Just t -> assume (Bound t 0) (VIsOne phi) $ \var -> do
-            env <- ask
-            for (truthAssignments phi (getEnv env)) $ \e -> do
-              let env' = env{ getEnv = e }
-              (Just var,) <$> check rhs (eval' env' dom_q)
-          Nothing -> do
-            env <- ask
-            for (truthAssignments phi (getEnv env)) $ \e -> do
-              let env' = env{ getEnv = e }
-              (Nothing,) <$> check rhs (eval' env' dom_q)
+  env <- ask
+  eqns <- for bs \(formula, rhs) -> do
+    (phi, fv) <- checkFormula formula
+    n <- newName
+    rhses <- for (truthAssignments phi (getEnv env)) $ \e -> do
+      let env' = env{ getEnv = e }
+      local (const env') $
+        check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n)))
     pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
 
-  for_ eqns $ \(n, (formula, (binding, rhs))) -> do
-    let
-      k = case binding of
-        Just v -> assume v (VIsOne formula) . const
-        Nothing -> id
-    k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
+  for_ eqns \(n, (formula, rhs)) -> do
+    for_ eqns $ \(n', (formula', rhs')) -> do
       let
-        k = case binding of
-          Just v -> assume v (VIsOne formula) . const
-          Nothing -> id
         truth = possible mempty (iand formula formula')
-        add [] = id
-        add ((~(HVar x), True):xs) = redefine x VI VI1 . add xs
-        add ((~(HVar x), False):xs) = redefine x VI VI0 . add xs
-      k $ when ((n /= n') && fst truth) . add (Map.toList (snd truth)) $ do
-        vl <- eval rhs
-        vl' <- eval rhs'
+
+      when ((n /= n') && fst truth) . for_ (truthAssignments (iand formula formula') (getEnv env)) $ \e -> do
+        let env' = env { getEnv = e }
+            vl = eval' env' rhs
+            vl' = eval' env' rhs'
         unify vl vl'
           `withNote` vsep [ pretty "These two cases must agree because they are both possible:"
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm rhs
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> prettyTm rhs'
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> pretty vl
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> pretty (zonk vl')
                           ]
-          `withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
+          `withNote` (pretty "Consider this face, where both are true:" <+> showFace False (snd truth))
 
   name <- newName
-  let
-    mkB name (Just v, b) = App P.Ex (Lam P.Ex v b) (Ref name)
-    mkB _ (Nothing, b) = b
-  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB name y)) eqns))))
+  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
 
 check (P.LamCase pats) ty =
   do
@@ -204,7 +185,7 @@ check (P.LamCase pats) ty =
         let range = Lam P.Ex name (quote (rng (VVar name)))
 
         cases <- checkPatterns range [] pats \partialPats (pat, rhs) -> do
-          checkPattern pat dom \pat wp boundary pat_nf -> do
+          checkPattern pat dom \pat wp boundary n_lams pat_nf -> do
             rhs <- check rhs (rng pat_nf)
             case boundary of
               -- If we're checking a higher constructor then we need to
@@ -226,19 +207,22 @@ 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 (VVar n) (snd <$> (Map.lookup n i))
                     unify vl rhs
+                      `withNote` (pretty "From the boundary conditions of the constructor" <+> prettyTm (quote pat_nf) <> pretty ":")
                       `withNote` vcat [ pretty "These must be the same because of the face"
-                                      , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
+                                      , indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk side)
+                                      , pretty "which is mapped to"
+                                      , indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk rhs)
                                       ]
-                      `withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
               _ -> pure ()
 
-            pure (pat, wp rhs)
+            pure (pat, n_lams, wp rhs)
         let x = wp (Lam P.Ex name (Case range (Ref name) cases))
         pure x
       _ -> do
@@ -251,9 +235,9 @@ check (P.LamCase pats) ty =
     checkPatterns _ acc [] _ = pure (reverse acc)
     checkPatterns rng acc (x:xs) k = do
       n <- newName
-      (p, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
-      checkPatterns rng ((p, t):acc) xs k
-    
+      (p, n, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
+      checkPatterns rng ((p, n, 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))
@@ -262,12 +246,16 @@ check (P.LamCase pats) ty =
     boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x
     boundaryFormulas a b = error (show (a, b))
 
+check P.Hole ty = do
+  t <- newMeta' True ty
+  pure (quote t)
+
 check exp ty = do
   (tm, has) <- switch $ infer exp
   wp <- isConvertibleTo has ty
   pure (wp tm)
 
-checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Value -> ElabM a) -> ElabM a
+checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Int -> Value -> ElabM a) -> ElabM a
 checkPattern (P.PCap var) dom cont = do
   name <- asks (Map.lookup var . nameMap)
   case name of
@@ -276,9 +264,9 @@ checkPattern (P.PCap var) dom cont = do
       (ty, wp, _) <- instantiate =<< getNfType name
       unify ty dom
       wrap <- skipLams skip
-      cont (Con name) wrap Nothing =<< eval (wp (Con name))
+      cont (Con name) wrap Nothing 0 =<< eval (wp (Con name))
     Just name -> throwElab $ NotACon name
-    Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing (VVar name)
+    Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing 0 (VVar name)
 
 checkPattern (P.PCon var args) dom cont =
   do
@@ -295,7 +283,7 @@ checkPattern (P.PCon var args) dom cont =
         con <- quote <$> getValue name
 
         bindNames args ty $ \names wrap ->
-          cont (Con name) (skip . wrap) (instBoundary xs <$> t) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names)
+          cont (Con name) (skip . wrap) (instBoundary xs <$> t) (length names) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names)
 
       Just name -> throwElab $ NotACon name
       _ -> throwElab $ NotInScope (Bound var 0)
@@ -327,13 +315,17 @@ skipLams k = do
   n <- newName
   (Lam P.Im n . ) <$> skipLams (k - 1)
 
-checkLetItems :: Map Text (Maybe NFType) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
-checkLetItems _   [] cont = cont []
+checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
+checkLetItems map   [] cont = do
+  for_ (Map.toList map) $ \case
+    (_, Nothing) -> pure ()
+    (n, Just _) -> throwElab $ DeclaredUndefined (Bound n 0)
+  cont []
 checkLetItems map (P.LetDecl v t:xs) cont = do
   t <- check t VTypeω
   t_nf <- eval t
-  assume (Defined v 0) t_nf \_ ->
-    checkLetItems (Map.insert v (Just t_nf) map) xs cont
+  assume (Defined v 0) t_nf \name ->
+    checkLetItems (Map.insert v (Just (name, t_nf)) map) xs cont
 
 checkLetItems map (P.LetBind name rhs:xs) cont = do
   case Map.lookup name map of
@@ -344,28 +336,34 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do
         checkLetItems map xs \xs ->
           cont ((name', quote ty, tm):xs)
     Just Nothing -> throwElab $ Redefinition (Defined name 0)
-    Just (Just ty_nf) -> do
+    Just (Just (name, ty_nf)) -> do
       rhs <- check rhs ty_nf
       rhs_nf <- eval rhs
-      makeLetDef (Defined name 0) ty_nf rhs_nf \name' ->
-        checkLetItems (Map.insert name Nothing map) xs \xs ->
-          cont ((name', quote ty_nf, rhs):xs)
-
-checkFormula :: P.Formula -> ElabM Value
-checkFormula P.FTop = pure VI1
-checkFormula P.FBot = pure VI0
-checkFormula (P.FAnd x y) = iand <$> checkFormula x <*> checkFormula y
-checkFormula (P.FOr x y) = ior <$> checkFormula x <*> checkFormula y
+      replaceLetDef name ty_nf rhs_nf $
+        checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs ->
+          cont ((name, quote ty_nf, rhs):xs)
+
+checkFormula :: P.Formula -> ElabM (Value, Set.Set Name)
+checkFormula P.FTop = pure (VI1, mempty)
+checkFormula P.FBot = pure (VI0, mempty)
+checkFormula (P.FAnd x y) = do
+  (x, f) <- checkFormula x
+  (y, f') <- checkFormula y
+  pure (iand x y, f <> f')
+checkFormula (P.FOr x y) = do
+  (x, f) <- checkFormula x
+  (y, f') <- checkFormula y
+  pure (ior x y, f <> f')
 checkFormula (P.FIs0 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (inot (VVar nm))
+  pure (inot (VVar nm), Set.singleton nm)
 checkFormula (P.FIs1 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (VVar nm)
+  pure (VVar nm, Set.singleton nm)
 
 isSort :: NFType -> ElabM ()
 isSort t = isSort (force t) where
@@ -427,15 +425,15 @@ isSigmaType t = isSigmaType (force t) where
       wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
       pure (dom, const rng, wp)
 
-isPartialType :: NFType -> ElabM (NFEndp, Value)
+isPartialType :: NFType -> ElabM (NFEndp, Value -> Value)
 isPartialType t = isPartialType (force t) where
-  isPartialType (VPartial phi a) = pure (phi, a)
-  isPartialType (VPartialP phi a) = pure (phi, a)
+  isPartialType (VPartial phi a) = pure (phi, const a)
+  isPartialType (VPartialP phi a) = pure (phi, (a @@))
   isPartialType t = do
     phi <- newMeta VI
     dom <- newMeta (VPartial phi VType)
-    unify t (VPartial phi dom)
-    pure (phi, dom)
+    unify t (VPartialP phi dom)
+    pure (phi, (dom @@))
 
 checkStatement :: P.Statement -> ElabM a -> ElabM a
 checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@@ -494,21 +492,21 @@ checkStatement (P.ReplNf e) k = do
   (e, _) <- infer e
   e_nf <- eval e
   h <- asks commHook
-  liftIO (h e_nf)
+  liftIO $ h . prettyVl =<< zonkIO e_nf
   k
 
 checkStatement (P.ReplTy e) k = do
-  (_, ty) <- infer e
+  (t, ty) <- infer e
   h <- asks commHook
-  liftIO (h ty)
+  liftIO (h (prettyTm t <+> colon <+> align (prettyVl (zonk ty))))
   k
 
 checkStatement (P.Data name tele retk constrs) k =
   do
-    checkTeleRetk True tele retk \kind tele undef -> do
+    checkTeleRetk tele retk \retk kind tele undef -> do
       kind_nf <- eval kind
-      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)
+      defineInternal (Defined name 0) kind_nf (\name' -> GluedVl (mkHead name') mempty (VNe (mkHead name') mempty)) \name' ->
+        checkCons retk tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
   where
     makeProj (x, p, _) = PApp p (VVar x)
 
@@ -518,26 +516,22 @@ checkStatement (P.Data name tele retk constrs) k =
       | any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
       | otherwise = HData False name
 
-    checkTeleRetk allKan [] retk cont = do
+    checkTeleRetk [] retk cont = do
       t <- check retk VTypeω
-      t_nf <- eval t
-      when allKan $ unify t_nf VType
-      cont t [] id
-    checkTeleRetk allKan ((x, p, t):xs) retk cont = do
+      r <- eval t
+      cont r t [] id
+
+    checkTeleRetk ((x, p, t):xs) retk cont = do
       (t, ty) <- infer t
       _ <- isConvertibleTo ty VTypeω
-      let
-        allKan' = case ty of
-          VType -> allKan
-          _ -> False
       t_nf <- eval t
       let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) }
-      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
+      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk xs retk \ret k xs w -> cont ret (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
 
-    checkCons _ _et [] k = k
+    checkCons _ _ _et [] k = k
 
-    checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
-      t <- check ty VTypeω
+    checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
+      t <- check ty retk
       ty_nf <- eval t
       let
         (args, ret') = splitPi ty_nf
@@ -545,11 +539,12 @@ checkStatement (P.Data name tele retk constrs) k =
         n' = map (\(x, _, y) -> (x, P.Im, y)) n
       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
+      defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons retk n ret xs k
+
+    checkCons retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
+      fibrant retk
       (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
-        t <- check return VTypeω
+        t <- check return retk
         ty_nf <- eval t
         let
           (args, ret') = splitPi ty_nf
@@ -566,17 +561,17 @@ checkStatement (P.Data name tele retk constrs) k =
         unify ret' ret
 
         faces <- envArgs args $ for faces \(f, t) -> do
-          phi <- checkFormula f
+          (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)
+        unify (foldl ior VI0 (map fst faces)) (totalProp indices)
           `withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
 
         pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
-      defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
+      defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons retk n ret xs k
 
     close []             t = t
     close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@@ -593,13 +588,13 @@ checkStatement (P.Data name tele retk constrs) k =
     makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con
     makePCon cty sp [] []         (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con
 
-    totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
+    totalProp (x:xs) = ior (VVar x) (inot (VVar x) `ior` totalProp xs)
     totalProp [] = VI0
 
-evalFix :: Name -> NFType -> Term -> ElabM Value
-evalFix name nft term = do
-  env <- ask
-  pure . fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
+    fibrant VTypeω = throwElab PathConPretype
+    fibrant VType = pure ()
+    fibrant x = error $ "not a constructor kind: " ++ show x
+
 
 checkProgram :: [P.Statement] -> ElabM a -> ElabM a
 checkProgram [] k = k
@@ -608,7 +603,7 @@ checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
 newtype Redefinition = Redefinition { getRedefName :: Name }
   deriving (Show, Typeable, Exception)
 
-data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
+data WhenCheckingEndpoint = WhenCheckingEndpoint { direction :: Name, leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
   deriving (Show, Typeable, Exception)
 
 data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
@@ -618,3 +613,10 @@ data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
 data NotACon = NotACon { theNotConstr :: Name }
   deriving          (Show, Typeable)
   deriving anyclass (Exception)
+
+data PathConPretype = PathConPretype
+  deriving          (Show, Typeable)
+  deriving anyclass (Exception)
+
+newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
+  deriving (Eq, Show, Exception)

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
@@ -21,28 +23,25 @@ import Data.Foldable
 import Data.IORef
 import Data.Maybe
 
-import Elab.Eval.Formula
+import {>n class="err">-# SOURCE #-} Elab.Eval.Formula
 import Elab.Monad
 
 import GHC.Stack
 
 import Presyntax.Presyntax (Plicity(..))
 
-import Prettyprinter
-
 import Syntax.Pretty
 import Syntax
 
-import System.IO.Unsafe
+import System.IO.Unsafe ( unsafePerformIO )
 
 import {-# SOURCE #-} Elab.WiredIn
-import Data.List (sortOn)
-import Data.Map.Strict (Map)
+import Debug (traceM, traceDocM)
+import Prettyprinter (pretty, (<+>))
 
-eval :: Term -> ElabM Value
+eval :: HasCallStack => Term -> ElabM Value
 eval t = asks (flip eval' t)
 
--- everywhere force
 zonkIO :: Value -> IO Value
 zonkIO (VNe hd sp) = do
   sp' <- traverse zonkSp sp
@@ -64,7 +63,6 @@ zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
 zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y
 zonkIO (VLine line x y f) = VLine <$> zonkIO line <*> zonkIO x <*> zonkIO y <*> zonkIO f
 
--- Sorts
 zonkIO VType = pure VType
 zonkIO VTypeω = pure VTypeω
 
@@ -76,37 +74,37 @@ zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y
 zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
 zonkIO (VINot x) = inot <$> zonkIO x
 
-zonkIO (VIsOne x) = VIsOne <$> zonkIO x
-zonkIO VItIsOne = pure VItIsOne
-
 zonkIO (VPartial x y)  = VPartial <$> zonkIO x <*> zonkIO y
 zonkIO (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y
 zonkIO (VSystem fs) = do
   t <- for (Map.toList fs) $ \(a, b) -> (,) <$> zonkIO a <*> zonkIO b
   pure (mkVSystem (Map.fromList t))
 zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c
-zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c
-zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
-zonkIO (VHComp a b c d) = hComp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
+zonkIO (VInc a b c) = incS <$> zonkIO a <*> zonkIO b <*> zonkIO c
+zonkIO (VComp a b c d) = pure $ VComp a b c d
+zonkIO (VHComp a b c d) = pure $ VHComp a b c d
 
 zonkIO (VGlueTy a phi ty e)   = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e
 zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x
 zonkIO (VUnglue a phi ty e x) = unglue   <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x
-zonkIO (VCase env t x xs) = do
-  env' <- emptyEnv
-  evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs
+zonkIO (VCase env t x xs) = pure $ VCase env t x xs
+
+zonkIO (VEqStrict a x y) = VEqStrict <$> zonkIO a <*> zonkIO x <*> zonkIO y
+zonkIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x
 
 zonkSp :: Projection -> IO Projection
 zonkSp (PApp p x) = PApp p <$> zonkIO x
 zonkSp (PIElim l x y i) = PIElim <$> zonkIO l <*> zonkIO x <*> zonkIO y <*> zonkIO i
 zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u
+zonkSp (PK a x p pr) = PK <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr
+zonkSp (PJ a x p pr y) = PJ <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr <*> zonkIO y
 zonkSp PProj1 = pure PProj1
 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
@@ -122,23 +120,22 @@ eval' env (PCon sys x) =
     Just (ty, _) -> VNe (HPCon (eval' env sys) ty x) mempty
     Nothing -> error $ "constructor " ++ show x ++ " has no type in scope"
 
-
 eval' _ (Data n x) = VNe (HData n x) mempty
 eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
 eval' env (Lam p s t) =
   VLam p $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
 
 eval' env (Pi p s d t) =
   VPi p (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t
+    eval' env { getEnv = (Map.insert s (idkT, a) (getEnv env))} t
 
 eval' _ (Meta m) = VNe (HMeta m) mempty
 
 eval' env (Sigma s d t) =
   VSigma (eval' env d) $ Closure s $ \a ->
-    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
 
 eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
 
@@ -159,15 +156,12 @@ eval' e (PathP l a b) = VPath (eval' e l) (eval' e a) (eval' e b)
 eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f) (eval' e i)
 eval' e (PathIntro p x y f) = VLine (eval' e p) (eval' e x) (eval' e y) (eval' e f)
 
-eval' e (IsOne i)  = VIsOne (eval' e i)
-eval' _ ItIsOne    = VItIsOne
-
 eval' e (Partial x y)  = VPartial (eval' e x) (eval' e y)
 eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y)
-eval' e (System fs) = VSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
+eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
 
 eval' e (Sub a phi u)   = VSub (eval' e a) (eval' e phi) (eval' e u)
-eval' e (Inc a phi u)   = VInc (eval' e a) (eval' e phi) (eval' e u)
+eval' e (Inc a phi u)   = incS (eval' e a) (eval' e phi) (eval' e u)
 eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x)
 
 eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0)
@@ -177,73 +171,131 @@ eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys)
 eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x)
 eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x)
 eval' e (Let ns x) =
-  let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns
+  let env' = foldl (\newe (n, ty, x) ->
+                      let nft = eval' newe ty
+                       in newe { getEnv = Map.insert n (nft, evalFix' newe n nft x) (getEnv newe) })
+                    e
+                    ns
    in eval' env' x
 
 eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs
 
-evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Term)] -> Value
-evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
+eval' e (EqS a x y) = VEqStrict (eval' e a) (eval' e x) (eval' e y)
+eval' e (Syntax.Refl a x) = VReflStrict (eval' e a) (eval' e x)
+eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e eq)
+eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq)
+
+idkT :: NFType
+idkT = VVar (Defined (T.pack "dunno") (negate 1))
+
+isIdkT :: NFType -> Bool
+isIdkT (VVar (Defined (T.unpack -> "dunno") (negate -> 1))) = True
+isIdkT _ = False
+
+evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value
+evalCase env rng sc [] = VCase (getEnv env) (fun rng) sc []
 
 evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
 
-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))
+evalCase env rng (VHComp a φ u u0) cases =
+  comp (fun \i -> rng (v i))
+       φ
+       (system \i is1 -> α (u @@ i @@ is1))
+       (VInc (rng a) φ (α (outS a φ (u @@ VI0) u0)))
   where
-    v = Elab.WiredIn.fill a phi u a0
+    v = Elab.WiredIn.fill (fun (const a)) φ u u0
+    α x = evalCase env rng x cases
 
-evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc
+evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc
 
-evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', k):xs)
+evalCase env rng (force -> val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs)
   | x == x'   = foldl applProj (eval' env k) sp
   | otherwise = evalCase env rng val xs
 
-evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs)
+evalCase env rng (force -> val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
   | x == x'   = foldl applProj (eval' env k) sp
   | otherwise = evalCase env rng val xs
 
+evalCase _ _ (VVar ((== trueCaseSentinel) -> True)) _ = VI1
+
 evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
 
+-- This is a great big HACK; When we see a system [ case x of ... => p
+-- ], we somehow need to make the 'case x of ...' become VI1. The way we
+-- do this is by substituting x/trueCaseSentinel in truthAssignments,
+-- and then making case trueCaseSentinel of ... => VI1 always.
+trueCaseSentinel :: Name
+trueCaseSentinel = Bound (T.pack "sentinel for true cases") (-1000)
+
+evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value
+evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, GluedVl (HVar name) mempty val) (getEnv env) } term
+
+evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value
+evalFix name nft term = do
+  t <- ask
+  pure (evalFix' t name (GluedVl (HVar name) mempty nft) term)
 
 data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
-unify' :: HasCallStack => Value -> Value -> ElabM ()
-unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
+unify' :: HasCallStack => Bool -> Value -> Value -> ElabM ()
+
+unify' cs topa@(GluedVl h sp a) topb@(GluedVl h' sp' b)
+  | h == h', length sp == length sp' =
+    traverse_ (uncurry (unify'Spine cs topa topb)) (Seq.zip sp sp')
+      `catchElab` \(_ :: SomeException) -> unify' cs a b
+
+unify' canSwitch topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
   go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
 
-  go (VNe (HPCon s _ _) _) rhs
-    | VSystem _ <- s = go (force s) rhs
+  go topa@(VNe (HPCon _ _ x) sp) topb@(VNe (HPCon _ _ y) sp')
+    | x == y = traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip sp sp')
 
-  go lhs (VNe (HPCon s _ _) _)
-    | VSystem _ <- s = go lhs (force s)
+  go (VNe (HPCon s _ _) _) rhs | Just v <- trivialSystem s = go v rhs
+  go lhs (VNe (HPCon s _ _) _) | Just v <- trivialSystem s = go lhs v
+
+  go (VCase e _ _ b) (VCase e' _ _ b') = do
+    env <- ask
+    let
+      go (_, _, a) (_, _, b)
+        | a == b = pure ()
+        | otherwise = unify' canSwitch (eval' env{getEnv=moreDefinedFrom e e' <$> e} a) (eval' env{getEnv=moreDefinedFrom e e' <$> e'} b)
+    zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
 
-  go (VNe x a) (VNe x' a')
+  go (VCase e _ _ b) y = do
+    env <- ask
+    let
+      go (_, n, a') = do
+        ns <- replicateM n (VVar <$> newName)
+        let a = foldl (vApp Ex) (eval' env{getEnv=e} a') ns
+        unify' canSwitch a y
+    traverse_ go b
+
+  go topa@(VNe x a) topb@(VNe x' a')
     | x == x', length a == length a' =
-      traverse_ (uncurry unify'Spine) (Seq.zip a a')
+      traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip a a')
 
   go (VLam p (Closure n k)) vl = do
     t <- VVar <$> newName' n
-    unify' (k t) (vApp p vl t)
+    unify' canSwitch (k t) (vApp p vl t)
 
   go vl (VLam p (Closure n k)) = do
     t <- VVar <$> newName' n
-    unify' (vApp p vl t) (k t)
+    unify' canSwitch (vApp p vl t) (k t)
 
-  go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl)
-  go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b
+  go (VPair a b) vl = unify' canSwitch a (vProj1 vl) *> unify' canSwitch b (vProj2 vl)
+  go vl (VPair a b) = unify' canSwitch (vProj1 vl) a *> unify' canSwitch (vProj2 vl) b
 
-  go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
-    t <- VVar <$> newName
-    unify' d d'
-    unify' (k t) (k' t)
+  go (VPi p d (Closure n k)) (VPi p' d' (Closure _ k')) | p == p' = do
+    t <- VVar <$> newName' n
+    unify' canSwitch d d'
+    unify' canSwitch (k t) (k' t)
 
-  go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
-    t <- VVar <$> newName
-    unify' d d'
-    unify' (k t) (k' t)
+  go (VSigma d (Closure n k)) (VSigma d' (Closure _ k')) = do
+    t <- VVar <$> newName' n
+    unify' canSwitch d d'
+    unify' canSwitch (k t) (k' t)
 
   go VType VType   = pure ()
   go VTypeω VTypeω = pure ()
@@ -251,56 +303,63 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go VI VI   = pure ()
 
   go (VPath l x y) (VPath l' x' y') = do
-    unify' l l'
-    unify' x x'
-    unify' y y'
+    unify' canSwitch l l'
+    unify' canSwitch x x'
+    unify' canSwitch y y'
 
   go (VLine l x y p) p' = do
-    n <- VVar <$> newName
-    unify' (p @@ n) (ielim l x y p' n)
+    n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
+    unify' canSwitch (p @@ n) (ielim l x y p' n)
 
   go p' (VLine l x y p) = do
     n <- VVar <$> newName
-    unify' (ielim l x y p' n) (p @@ n)
-
-  go (VIsOne x) (VIsOne y) = unify' x y
+    unify' canSwitch (ielim l x y p' n) (p @@ n)
 
-  -- IsOne is proof-irrelevant:
-  go VItIsOne _ = pure ()
-  go _ VItIsOne = pure ()
+  go (VPartial phi r) (VPartial phi' r')   = unify' canSwitch phi phi' *> unify' canSwitch r r'
+  go (VPartialP phi r) (VPartialP phi' r') = unify' canSwitch phi phi' *> unify' canSwitch r r'
 
-  go (VPartial phi r) (VPartial phi' r')   = unify' phi phi' *> unify' r r'
-  go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify' r r'
-
-  go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
-  go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+  go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')]
+  go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')]
 
   go (VComp a phi u a0) (VComp a' phi' u' a0') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+
+  go (VHComp a phi u a0) (VHComp a' phi' u' a0') =
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
-  go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs
-  go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne)
+  go (VGlueTy _ (force -> VI1) u _0) rhs = unify' canSwitch (u @@ VReflStrict VI VI1) rhs
+  go lhs (VGlueTy _ (force -> VI1) u _0) = unify' canSwitch lhs (u @@ VReflStrict VI VI1)
 
   go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
   go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
+
+  go (VUnglue a phi u a0 x) (VUnglue a' phi' u' a0' x') =
+    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (x, x')]
+
+  go (VSystem sys) rhs = goSystem (unify' canSwitch) sys rhs
+  go rhs (VSystem sys) = goSystem (flip (unify' canSwitch)) sys rhs
+
+  go (VEqStrict a x y) (VEqStrict a' x' y') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x'), (y, y')]
+  go (VReflStrict a x) (VReflStrict a' x') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x')]
+  go _ VReflStrict{} = pure ()
+  go VReflStrict{} _ = pure ()
 
-  go (VSystem sys) rhs = goSystem unify' sys rhs
-  go rhs (VSystem sys) = goSystem (flip unify') sys rhs
+  go (VINot x) (VINot y) = unify' canSwitch x y
 
-  go (VCase _ _ a b) (VCase _ _ a' b') = do
-    unify' a a'
-    let go a b = join $ unify' <$> eval (snd a) <*> eval (snd b)
-    zipWithM_ go (sortOn fst b) (sortOn fst b')
+  go x y =
+    case (toDnf x, toDnf y) of
+      (Just xs, Just ys) -> unify'Formula xs ys
+      _ ->
+        if canSwitch
+          then goDumb x y
+          else fail
 
-  go x y
-    | x == y = pure ()
-    | otherwise =
-      case (toDnf x, toDnf y) of
-        (Just xs, Just ys) -> unify'Formula xs ys
-        _ -> fail
+  goDumb (VIOr a b) (VIOr a' b') = unify' canSwitch a a' *> goDumb b b'
+  goDumb (VIAnd a b) (VIAnd a' b') = unify' canSwitch a a' *> goDumb b b'
+  goDumb x y = switch $ unify' False x y
 
   goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM ()
   goSystem k sys rhs = do
@@ -308,29 +367,58 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     env <- ask
     for_ (Map.toList sys) $ \(f, i) -> do
       let i_q = quote i
-      for (truthAssignments f (getEnv env)) $ \e ->
+      for (truthAssignments f (getEnv env)) $ \e -> do
         k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
 
   fail = throwElab $ NotEqual topa topb
+  unify'Formula x y
+    | compareDNFs x y = pure ()
+    | otherwise = fail
 
-  unify'Spine (PApp a v) (PApp a' v')
-    | a == a' = unify' v v'
+moreDefinedFrom :: Map Name (NFType, Value) -> Map Name (NFType, Value) -> (NFType, Value) -> (NFType, Value)
+moreDefinedFrom map1 map2 ours@(_, VNe (HVar name) _) =
+  case Map.lookup name map1 of
+    Just (_, VNe HVar{} _) -> map2's
+    Just (ty, x) -> (ty, x)
+    Nothing -> map2's
+  where
+    map2's = case Map.lookup name map2 of
+      Just (_, VNe HVar{} _) -> ours
+      Just (ty, x) -> (ty, x)
+      Nothing -> ours
+moreDefinedFrom _ _ ours = ours
 
-  unify'Spine PProj1 PProj1 = pure ()
-  unify'Spine PProj2 PProj2 = pure ()
+trivialSystem :: Value -> Maybe Value
+trivialSystem = go . force where
+  go VSystem{} = Nothing
+  go x = Just x
 
-  unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
-  unify'Spine (POuc a phi u) (POuc a' phi' u') =
-    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+unify'Spine :: Bool -> Value -> Value -> Projection -> Projection -> ElabM ()
+unify'Spine cs _ _ (PApp a v) (PApp a' v')
+  | a == a' = unify' cs v v'
 
-  unify'Spine _ _ = fail
+unify'Spine _ _ _ PProj1 PProj1 = pure ()
+unify'Spine _ _ _ PProj2 PProj2 = pure ()
 
-  unify'Formula x y
-    | compareDNFs x y = pure ()
-    | otherwise = fail
+unify'Spine cs _ _ (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' cs i j
+unify'Spine cs _ _ (POuc a phi u) (POuc a' phi' u') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (phi, phi'), (u, u')]
+
+unify'Spine cs _ _ (PK a x p pr) (PK a' x' p' pr') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr')]
+
+unify'Spine cs _ _ (PJ a x p pr y) (PJ a' x' p' pr' y') =
+  traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
+
+unify'Spine _ x y _ _ = throwElab (NotEqual x y)
 
 unify :: HasCallStack => Value -> Value -> ElabM ()
-unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
+unify x y = shallowly $ go x y where
+  go topa@(GluedVl h sp a) topb@(GluedVl h' sp' b)
+    | h == h', length sp == length sp' =
+      traverse_ (uncurry (unify'Spine True topa topb)) (Seq.zip sp sp')
+        `catchElab` \(_ :: SomeException) -> unify' True a b
+  go a b = unify' True a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
 
 isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
 isConvertibleTo a b = isConvertibleTo (force a) (force b) where
@@ -348,26 +436,42 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
     wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n)
     pure (\f -> Lam p n (wp' (App p f (wp (Ref n)))))
 
+  VPath a x y `isConvertibleTo` VPi Ex d (Closure _ k') = do
+    unify d VI
+    nm <- newName
+    wp <- isConvertibleTo (a @@ VVar nm) (k' (VVar nm))
+    pure (\f -> Lam Ex nm (wp (IElim (quote a) (quote x) (quote y) f (Ref nm))))
+
   isConvertibleTo a b = do
-    unify' a b
+    unify' True a b
     pure id
 
-newMeta :: Value -> ElabM Value
-newMeta dom = do
+newMeta' :: Bool -> Value -> ElabM Value
+newMeta' int dom = do
   loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan
   n <- newName
   c <- liftIO $ newIORef Nothing
-  let m = MV (getNameText n) c dom (flatten <$> loc)
+  let m = MV (getNameText n) c dom (flatten <$> loc) int
       flatten (x, (y, z)) = (x, y, z)
 
   env <- asks getEnv
 
-  t <- for (Map.toList env) $ \(n, _) -> pure $
+  t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $
     case n of
-      Bound{} -> Just (PApp Ex (VVar n))
+      Bound{} -> Just (PApp Ex (VVar n), n, t)
       _ -> Nothing
 
-  pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
+  let
+    ts = Map.fromList $ fmap (\(_, n, (t, _)) -> (n, t)) t
+    t' = fmap (\(x, _, _) -> x) t
+
+  um <- asks unsolvedMetas
+  liftIO . atomicModifyIORef um $ \um -> (Map.insert (m ts) [] um, ())
+
+  pure (VNe (HMeta (m ts)) (Seq.fromList t'))
+
+newMeta :: Value -> ElabM Value
+newMeta = newMeta' False
 
 newName :: MonadIO m => m Name
 newName = liftIO $ do
@@ -384,91 +488,103 @@ _nameCounter = unsafePerformIO $ newIORef 0
 {-# NOINLINE _nameCounter #-}
 
 solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
+solveMeta m Seq.Empty (VNe (HMeta m') Seq.Empty) | m == m' = pure ()
 solveMeta m@(mvCell -> cell) sp rhs = do
+  when (mvName m == T.pack "2801") do
+    traceM (VNe (HMeta m) sp)
+    traceM rhs
+
   env <- ask
   names <- tryElab $ checkSpine Set.empty sp
   case names of
     Right names -> do
-      checkScope (Set.fromList names) rhs
-        `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
-      let tm = quote rhs
-          lam = eval' env $ foldr (Lam Ex) tm names
-      liftIO . atomicModifyIORef' cell $ \case
-        Just _ -> error "filled cell in solvedMeta"
-        Nothing -> (Just lam, ())
-    Left (_ :: SpineProjection) -> do
+      scope <- tryElab $ checkScope m (Set.fromList names) rhs
+      case scope of
+        Right () -> do
+          let tm = quote rhs
+              lam = eval' env $ foldr (Lam Ex) tm names
+          liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
+          liftIO . atomicModifyIORef' cell $ \case
+            Just _ -> error "filled cell in solvedMeta"
+            Nothing -> (Just lam, ())
+        Left (_ :: MetaException) -> abort env
+    Left (_ :: MetaException) -> abort env
+  where
+    abort env =
       liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $
         case Map.lookup m x of
           Just qs -> Map.insert m ((sp, rhs):qs) x
           Nothing -> Map.insert m [(sp, rhs)] x
 
-checkScope :: Set Name -> Value -> ElabM ()
-checkScope scope (VNe h sp) =
+checkScope :: MV -> Set Name -> Value -> ElabM ()
+checkScope mv scope (VNe h sp) =
   do
     case h of
       HVar v@Bound{} ->
         unless (v `Set.member` scope) . throwElab $
-          NotInScope v
+          ScopeCheckingFail v
       HVar{} -> pure ()
       HCon{} -> pure ()
       HPCon{} -> pure ()
-      HMeta{} -> pure ()
+      HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv
       HData{} -> pure ()
     traverse_ checkProj sp
   where
-    checkProj (PApp _ t) = checkScope scope t
-    checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
-    checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u]
+    checkProj (PApp _ t) = checkScope mv scope t
+    checkProj (PIElim l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
+    checkProj (PK l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
+    checkProj (PJ l x y i j) = traverse_ (checkScope mv scope) [l, x, y, i, j]
+    checkProj (POuc a phi u) = traverse_ (checkScope mv scope) [a, phi, u]
     checkProj PProj1 = pure ()
     checkProj PProj2 = pure ()
 
-checkScope scope (GluedVl _ _p vl) = checkScope scope vl
+checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl
 
-checkScope scope (VLam _ (Closure n k)) =
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VLam _ (Closure n k)) =
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope scope (VPi _ d (Closure n k)) = do
-  checkScope scope d
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VPi _ d (Closure n k)) = do
+  checkScope mv scope d
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope scope (VSigma d (Closure n k)) = do
-  checkScope scope d
-  checkScope (Set.insert n scope) (k (VVar n))
+checkScope mv scope (VSigma d (Closure n k)) = do
+  checkScope mv scope d
+  checkScope mv (Set.insert n scope) (k (VVar n))
 
-checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
+checkScope mv s (VPair a b) = traverse_ (checkScope mv s) [a, b]
 
-checkScope _ VType = pure ()
-checkScope _ VTypeω = pure ()
+checkScope _ _ VType = pure ()
+checkScope _ _ VTypeω = pure ()
 
-checkScope _ VI = pure ()
-checkScope _ VI0 = pure ()
-checkScope _ VI1 = pure ()
+checkScope _ _ VI = pure ()
+checkScope _ _ VI0 = pure ()
+checkScope _ _ VI1 = pure ()
 
-checkScope s (VIAnd x y) = traverse_ (checkScope s) [x, y]
-checkScope s (VIOr x y)  = traverse_ (checkScope s) [x, y]
-checkScope s (VINot x)   = checkScope s x
+checkScope mv s (VIAnd x y) = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VIOr x y)  = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VINot x)   = checkScope mv s x
 
-checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
-checkScope s (VLine _ _ _ line)   = checkScope s line
+checkScope mv s (VPath line a b) = traverse_ (checkScope mv s) [line, a, b]
+checkScope mv s (VLine _ _ _ line)   = checkScope mv s line
 
-checkScope s (VIsOne x) = checkScope s x
-checkScope _ VItIsOne   = pure ()
+checkScope mv s (VPartial x y)  = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VPartialP x y) = traverse_ (checkScope mv s) [x, y]
+checkScope mv s (VSystem fs) =
+  for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope mv s) [x, y]
 
-checkScope s (VPartial x y)  = traverse_ (checkScope s) [x, y]
-checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
-checkScope s (VSystem fs) =
-  for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope s) [x, y]
+checkScope mv s (VSub a b c) = traverse_ (checkScope mv s) [a, b, c]
+checkScope mv s (VInc a b c) = traverse_ (checkScope mv s) [a, b, c]
+checkScope mv s (VComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
+checkScope mv s (VHComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
 
-checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c]
-checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c]
-checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
-checkScope s (VHComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
+checkScope mv s (VGlueTy a phi ty eq) = traverse_ (checkScope mv s) [a, phi, ty, eq]
+checkScope mv s (VGlue a phi ty eq inv x) = traverse_ (checkScope mv s) [a, phi, ty, eq, inv, x]
+checkScope mv s (VUnglue a phi ty eq vl) = traverse_ (checkScope mv s) [a, phi, ty, eq, vl]
 
-checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq]
-checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x]
-checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl]
+checkScope mv s (VCase _ _ v _) = checkScope mv s v
 
-checkScope s (VCase _ _ v _) = checkScope s v
+checkScope mv s (VEqStrict a x y) = traverse_ (checkScope mv s) [a, x, y]
+checkScope mv s (VReflStrict a x) = traverse_ (checkScope mv s) [a, x]
 
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@@ -477,10 +593,10 @@ checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
 checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
-newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
-  deriving (Show, Typeable, Exception)
-
-newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
+data MetaException = NonLinearSpine { getDupeName :: Name }
+                   | SpineProj { getSpineProjection :: Projection } 
+                   | CircularSolution { getCycle :: MV }
+                   | ScopeCheckingFail { outOfScope :: Name }
   deriving (Show, Typeable, Exception)
 
 substituteIO :: Map.Map Name Value -> Value -> IO Value
@@ -488,15 +604,10 @@ substituteIO sub = substituteIO . force where
   substituteIO (VNe hd sp) = do
     sp' <- traverse (substituteSp sub) sp
     case hd of
-      HMeta (mvCell -> cell) -> do
-        solved <- liftIO $ readIORef cell
-        case solved of
-          Just vl -> substituteIO $ foldl applProj vl sp'
-          Nothing -> pure $ VNe hd sp'
       HVar v ->
         case Map.lookup v sub of
           Just vl -> substituteIO $ foldl applProj vl sp'
-          Nothing -> pure $ VNe hd sp'
+          Nothing -> pure $ foldl applProj (VNe hd mempty) sp'
       hd -> pure $ VNe hd sp'
 
   substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl
@@ -509,7 +620,6 @@ substituteIO sub = substituteIO . force where
   substituteIO (VPath line x y) = VPath <$> substituteIO line <*> substituteIO x <*> substituteIO y
   substituteIO (VLine line x y f) = VLine <$> substituteIO line <*> substituteIO x <*> substituteIO y <*> substituteIO f
 
-  -- Sorts
   substituteIO VType = pure VType
   substituteIO VTypeω = pure VTypeω
 
@@ -521,16 +631,13 @@ substituteIO sub = substituteIO . force where
   substituteIO (VIOr x y) = ior <$> substituteIO x <*> substituteIO y
   substituteIO (VINot x) = inot <$> substituteIO x
 
-  substituteIO (VIsOne x) = VIsOne <$> substituteIO x
-  substituteIO VItIsOne = pure VItIsOne
-
   substituteIO (VPartial x y)  = VPartial <$> substituteIO x <*> substituteIO y
   substituteIO (VPartialP x y) = VPartialP <$> substituteIO x <*> substituteIO y
   substituteIO (VSystem fs) = do
     t <- for (Map.toList fs) $ \(a, b) -> (,) <$> substituteIO a <*> substituteIO b
     pure (mkVSystem (Map.fromList t))
   substituteIO (VSub a b c) = VSub <$> substituteIO a <*> substituteIO b <*> substituteIO c
-  substituteIO (VInc a b c) = VInc <$> substituteIO a <*> substituteIO b <*> substituteIO c
+  substituteIO (VInc a b c) = incS <$> substituteIO a <*> substituteIO b <*> substituteIO c
   substituteIO (VComp a b c d) = comp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d
   substituteIO (VHComp a b c d) = hComp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d
 
@@ -538,6 +645,8 @@ substituteIO sub = substituteIO . force where
   substituteIO (VGlue a phi ty e t x) = glueElem <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO t <*> substituteIO x
   substituteIO (VUnglue a phi ty e x) = unglue   <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO x
   substituteIO (VCase env t x xs) = VCase env <$> substituteIO t <*> substituteIO x <*> pure xs
+  substituteIO (VEqStrict a x y) = VEqStrict <$> substituteIO a <*> substituteIO x <*> substituteIO y
+  substituteIO (VReflStrict a x) = VReflStrict <$> substituteIO a <*> substituteIO x
 
 substitute :: Map Name Value -> Value -> Value
 substitute sub = unsafePerformIO . substituteIO sub
@@ -545,16 +654,23 @@ substitute sub = unsafePerformIO . substituteIO sub
 substituteSp :: Map Name Value -> Projection -> IO Projection
 substituteSp sub (PApp p x) = PApp p <$> substituteIO sub x
 substituteSp sub (PIElim l x y i) = PIElim <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i
+substituteSp sub (PK l x y i) = PK <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i
+substituteSp sub (PJ l x y i j) = PJ <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i <*> substituteIO sub j
 substituteSp sub (POuc a phi u) = POuc <$> substituteIO sub a <*> substituteIO sub phi <*> substituteIO sub u
 substituteSp _ PProj1 = pure PProj1
 substituteSp _ PProj2 = pure PProj2
 
 mkVSystem :: Map.Map Value Value -> Value
 mkVSystem vals =
-  let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in
-  case Map.lookup VI1 map' of
+  let map' = Map.fromList (Map.toList vals >>= go)
+      go (x, y) =
+        case (force x, y) of
+          (VI0, _) -> []
+          (VIOr _ _, VSystem y) -> Map.toList y >>= go
+          (a, b) -> [(a, b)]
+  in case Map.lookup VI1 map' of
     Just x -> x
-    Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map')
+    Nothing -> VSystem map'
 
 forceIO :: MonadIO m => Value -> m Value
 forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do
@@ -568,29 +684,35 @@ forceIO vl@(VSystem fs) =
     Nothing -> pure vl
 forceIO (GluedVl _ _ vl) = forceIO vl
 forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
+forceIO (VHComp line phi u a0) = hComp <$> 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
 
-applProj :: Value -> Projection -> Value
+force :: Value -> Value
+force = unsafePerformIO . forceIO
+
+applProj :: HasCallStack => 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
 applProj fun (POuc a phi u)   = outS a phi u fun
+applProj fun (PK a x p pr)    = strictK a x p pr fun
+applProj fun (PJ a x p pr y)  = strictJ a x p pr y 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
-  | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
-vApp p (VNe h sp) arg    = VNe h (sp Seq.:|> PApp p arg)
+vApp _ (VLam _ k) arg = clCont k arg
+vApp p (VNe (HData True n) _) _ | T.unpack (getNameText n) == "S1" = undefined
+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 (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
+vApp p (VCase env rng sc branches) arg =
+  VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
+    (map (projIntoCase (flip (App p) (quote arg))) branches)
+-- vApp _ (VLine _ _ _ (VLam _ k)) arg = clCont k arg
 vApp _ x _             = error $ "can't apply " ++ show (prettyTm (quote x))
 
 (@@) :: HasCallStack => Value -> Value -> Value
@@ -602,13 +724,17 @@ vProj1 (VPair a _) = a
 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 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
+vProj1 (VInc (VSigma a _) b c) = incS a b (vProj1 c)
+vProj1 (VCase env rng sc branches) =
+  VCase env rng sc (map (projIntoCase Proj1) branches)
+vProj1 x = error $ "can't proj1 " ++ show x
 
 vProj2 :: HasCallStack => Value -> Value
 vProj2 (VPair _ b) = b
 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 (VInc (VSigma _ (Closure _ r)) b c) = incS (r (vProj1 c)) b (vProj2 c)
+vProj2 (VCase env rng sc branches) =
+  VCase env rng sc (map (projIntoCase Proj2) branches)
+vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))

src/Elab/Eval/Formula.hs

@@ -2,22 +2,38 @@ module Elab.Eval.Formula where
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
+import qualified Data.Set as Set
 import Data.Map.Strict (Map)
+import Data.Set (Set)
 
 import Syntax
 
 import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
+import Elab.Eval (substitute, trueCaseSentinel)
 
 toDnf :: Value -> Maybe Value
-toDnf (VNe _ _) = Nothing
-toDnf x = toDnf x where
-  toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
-  toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
-  toDnf (VINot x) = inot <$> toDnf x
-  toDnf VI0 = pure VI0
-  toDnf VI1 = pure VI1
-  toDnf v@(VNe _ Seq.Empty) = pure v
-  toDnf _ = Nothing
+toDnf = fmap (dnf2Val . normalise) . val2Dnf where
+  val2Dnf (VNe _ _) = Nothing
+  val2Dnf x = toDnf x where
+    toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
+    toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
+    toDnf (VINot x) = inot <$> toDnf x
+    toDnf VI0 = pure VI0
+    toDnf VI1 = pure VI1
+    toDnf v@(VNe _ Seq.Empty) = pure v
+    toDnf _ = Nothing
+
+  dnf2Val xs = Set.foldl ior VI0 (Set.map (Set.foldl iand VI1) xs)
+
+type Nf = Set (Set Value)
+
+normalise :: Value -> Nf
+normalise = normaliseOr where
+  normaliseOr (VIOr x y) = Set.singleton (normaliseAnd x) <> normaliseOr y
+  normaliseOr x = Set.singleton (normaliseAnd x)
+
+  normaliseAnd (VIAnd x y) = Set.insert x (normaliseAnd y)
+  normaliseAnd x = Set.singleton x
 
 compareDNFs :: Value -> Value -> Bool
 compareDNFs (VIOr x y) (VIOr x' y') =
@@ -60,10 +76,14 @@ truthAssignments VI0 _ = []
 truthAssignments VI1 m = pure m
 truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
 truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
-truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
-truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
+truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) (sub x VI1 <$> m))
+truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) (sub x VI0 <$> m))
+truthAssignments (VCase _ _ (VNe (HVar x) _) _) m = pure (Map.insert x (VI, VVar trueCaseSentinel) m)
 truthAssignments _ m = pure m
 
+sub :: Name -> Value -> (NFType, NFEndp) -> (Value, Value)
+sub x v (a, b) = (substitute (Map.singleton x v) a, substitute (Map.singleton x v) b)
+
 idist :: Value -> Value -> Value
 idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)
 idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y)

src/Elab/Eval/Formula.hs-boot

@@ -0,0 +1,18 @@
+module Elab.Eval.Formula where
+
+import Syntax
+import Data.Map.Strict (Map)
+import Data.Set (Set)
+
+toDnf :: Value -> Maybe Value
+
+type Nf = Set (Set Value)
+
+normalise :: Value -> Nf
+compareDNFs :: Value -> Value -> Bool
+
+swap :: Ord b => b -> b -> (b, b)
+
+possible :: Map Head Bool -> Value -> (Bool, Map Head Bool)
+
+truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]

src/Elab/Monad.hs

@@ -26,17 +26,19 @@ data ElabEnv =
 
           , nameMap     :: Map Text Name
           , pingPong    :: {-# UNPACK #-} !Int
-          , commHook    :: Value -> IO ()
+          , commHook    :: Doc AnsiStyle -> IO ()
 
           , currentSpan :: Maybe (P.Posn, P.Posn)
           , currentFile :: Maybe Text
 
-          , whereBound  :: Map Name (P.Posn, P.Posn)
+          , whereBound   :: Map Name (P.Posn, P.Posn)
           , definedNames :: Set Name
 
-          , boundaries :: Map Name Boundary
+          , boundaries   :: Map Name Boundary
 
           , unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)]))
+
+          , loadedFiles :: [String]
           }
 
 newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
@@ -44,7 +46,24 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
     via ReaderT ElabEnv IO
 
 emptyEnv :: IO ElabEnv
-emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty mempty <$> newIORef mempty
+emptyEnv = do
+  u <- newIORef mempty
+  pure $ ElabEnv { getEnv      = mempty
+                 , nameMap     = mempty
+                 , pingPong    = 0
+                 , commHook    = const (pure ())
+
+                 , currentSpan = Nothing
+                 , currentFile = Nothing
+
+                 , whereBound   = mempty
+                 , definedNames = mempty
+
+                 , boundaries   = mempty
+
+                 , unsolvedMetas = u
+                 , loadedFiles = []
+                 }
 
 addBoundary :: Name -> Boundary -> ElabM a -> ElabM a
 addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} )
@@ -58,6 +77,9 @@ define nm vty val = defineInternal nm vty (const val)
 makeLetDef :: Name -> Value -> Value -> (Name -> ElabM a) -> ElabM a
 makeLetDef nm vty val = defineInternal nm vty (\nm -> GluedVl (HVar nm) mempty val)
 
+replaceLetDef :: Name -> Value -> Value -> ElabM a -> ElabM a
+replaceLetDef nm vty val = redefine nm vty (GluedVl (HVar nm) mempty val)
+
 assumes :: [Name] -> Value -> ([Name] -> ElabM a) -> ElabM a
 assumes nms ty k = do
   let
@@ -115,10 +137,13 @@ switch :: ElabM a -> ElabM a
 switch k =
   do
     depth <- asks pingPong
-    when (depth >= 128) $ throwElab StackOverflow
+    when (depth >= 128) $ error "stack overflow"
     local go k
   where go e = e { pingPong = pingPong e + 1 }
 
+shallowly :: ElabM a -> ElabM a
+shallowly = local (\e -> e { pingPong = 0 })
+
 newtype NotInScope = NotInScope { nameNotInScope :: Name }
   deriving          (Show, Typeable)
   deriving anyclass (Exception)

src/Elab/WiredIn.hs

@@ -4,9 +4,37 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ViewPatterns #-}
-module Elab.WiredIn where
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# OPTIONS_GHC -fno-full-laziness #-}
+module Elab.WiredIn
+       ( wiType
+       , wiValue
+       , wiredInNames
+       , NoSuchPrimitive(..)
+
+       , iand
+       , ior
+       , inot
+       , ielim
+       , incS
+       , outS
+       , comp
+       , fill
+       , hComp
+       , glueType
+       , glueElem
+       , unglue
+       , fun
+       , system
+       , strictK
+       , strictJ
+       , projIntoCase
+       )
+  where
 
-import Control.Exception
+import Control.Exception ( assert, Exception )
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
@@ -15,16 +43,19 @@ import Data.Map.Strict (Map)
 import Data.Text (Text)
 import Data.Typeable
 
+import Debug
+
 import Elab.Eval
 
 import GHC.Stack (HasCallStack)
 
+import Presyntax.Presyntax (Plicity(Im, Ex))
 import qualified Presyntax.Presyntax as P
 
-import Syntax.Pretty (prettyTm)
+import Syntax.Pretty (prettyTm, prettyVl)
 import Syntax
 
-import System.IO.Unsafe
+import System.IO.Unsafe ( unsafePerformIO )
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -39,25 +70,28 @@ wiType WiIOr      = VI ~> VI ~> VI
 wiType WiINot     = VI ~> VI
 wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
-wiType WiIsOne    = VI ~> VTypeω
-wiType WiItIsOne  = VIsOne VI1
-
 wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
+wiType WiPOr      = forAll VType \a -> dprod VI \phi -> dprod VI \psi -> VPartial phi a ~> VPartial psi a ~> VPartial (ior phi psi) a
 
 wiType WiSub      = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
 wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
 wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a
 
-wiType WiComp     = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
--- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
+wiType WiComp     = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> VSub (a @@ VI1) phi (u @@ VI1)
+
 wiType WiGlue     = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
--- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
 wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
   dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
--- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
 wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
 
+wiType WiSEq   = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
+wiType WiSRefl = forAll' "A" VTypeω \a -> forAll' "x" a \x -> VEqStrict a x x
+wiType WiSK    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (VEqStrict a x x ~> VTypeω) \bigp -> (bigp @@ VReflStrict a x) ~> dprod' "p" (VEqStrict a x x) \p -> bigp @@ p
+wiType WiSJ    = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (dprod' "y" a \y -> VEqStrict a x y ~> VTypeω) \bigp -> bigp @@ x @@ VReflStrict a x ~> forAll' "y" a \y -> dprod' "p" (VEqStrict a x y) \p -> bigp @@ y @@ p
+
+wiType WiLineToEquiv = dprod' "P" (VI ~> VType) \a -> equiv (a @@ VI0) (a @@ VI1)
+
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
 wiValue WiPretype  = VTypeω
@@ -66,25 +100,35 @@ wiValue WiInterval = VI
 wiValue WiI0       = VI0
 wiValue WiI1       = VI1
 
-wiValue WiIAnd      = fun \x -> fun \y -> iand x y
-wiValue WiIOr       = fun \x -> fun \y -> ior x y
-wiValue WiINot      = fun inot
-wiValue WiPathP     = fun \a -> fun \x -> fun \y -> VPath a x y
+wiValue WiIAnd      = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> iand i j
+wiValue WiIOr       = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> ior i j
+wiValue WiINot      = fun' "x" inot
+wiValue WiPathP     = functions [(Ex, "A"), (Ex, "x"), (Ex, "y")] \[a, x, y] -> VPath a x y
 
-wiValue WiIsOne   = fun VIsOne
-wiValue WiItIsOne = VItIsOne
+wiValue WiPartial  = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartial phi a
+wiValue WiPartialP = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartialP phi a
+wiValue WiPOr      = functions [(Im, "A"), (Ex, "phi"), (Ex, "psi"), (Ex, "a"), (Ex, "b")] \[_, phi, psi, a, b] -> mkVSystem (Map.fromList [(phi, a), (psi, b)])
 
-wiValue WiPartial  = fun \phi -> fun \r -> VPartial phi r
-wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
-wiValue WiSub      = fun \a -> fun \phi -> fun \u -> VSub a phi u
-wiValue WiInS      = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
-wiValue WiOutS     = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
-wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x
+wiValue WiSub      = functions [(Ex, "A"), (Ex, "phi"), (Ex, "u")] \[a, phi, u] -> VSub a phi u
+wiValue WiInS      = functions [(Im, "A"), (Im, "phi"), (Ex, "u")] \[a, phi, u] -> incS a phi u
+wiValue WiOutS     = functions [(Im, "A"), (Im, "phi"), (Im, "u"), (Ex, "u0")] \[a, phi, u, x] -> outS a phi u x
+wiValue WiComp     = fun' "A" \a -> forallI \phi -> fun' "u" \u -> fun' "u0" \x -> incS (a @@ VI1) phi (comp a phi u x)
 
 wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
 wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
 wiValue WiUnglue   = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x
 
+wiValue WiSEq   = forallI \a -> fun \x -> fun \y -> VEqStrict a x y
+wiValue WiSRefl = forallI \a -> forallI \x -> VReflStrict a x
+wiValue WiSK    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> fun \p -> strictK a x bigp pr p
+wiValue WiSJ    = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y -> fun \p -> strictJ a x bigp pr y p
+
+wiValue WiLineToEquiv = fun \l ->
+  GluedVl
+    (HVar (Defined "lineToEquiv" (-1)))
+    (Seq.fromList [(PApp P.Ex l)])
+    (makeEquiv' ((l @@) . inot))
+
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
 infixr 7 ~>
@@ -96,6 +140,11 @@ line k = VLam P.Ex $ Closure (Bound "i" 0) (k . force)
 fun' :: String -> (Value -> Value) -> Value
 fun' x k = VLam P.Ex $ Closure (Bound (T.pack x) 0) (k . force)
 
+functions :: [(P.Plicity, String)] -> ([Value] -> Value) -> Value
+functions args cont = go args [] where
+  go [] acc = cont (reverse acc)
+  go ((p, x):xs) acc = VLam p $ Closure (Bound (T.pack x) 0) \arg -> go xs (arg:acc)
+
 forallI :: (Value -> Value) -> Value
 forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)
 
@@ -117,7 +166,6 @@ forAll' n a b = VPi P.Im a (Closure (Bound (T.pack n) 0) b)
 forAll :: Value -> (Value -> Value) -> Value
 forAll = forAll' "x"
 
-
 wiredInNames :: Map Text WiredIn
 wiredInNames = Map.fromList
   [ ("Pretype", WiPretype)
@@ -130,11 +178,9 @@ wiredInNames = Map.fromList
   , ("inot", WiINot)
   , ("PathP", WiPathP)
 
-  , ("IsOne", WiIsOne)
-  , ("itIs1", WiItIsOne)
-
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
+  , ("partialExt", WiPOr)
   , ("Sub", WiSub)
   , ("inS", WiInS)
   , ("outS", WiOutS)
@@ -143,14 +189,19 @@ wiredInNames = Map.fromList
   , ("Glue", WiGlue)
   , ("glue", WiGlueElem)
   , ("unglue", WiUnglue)
+
+  , ("Eq_s", WiSEq)
+  , ("refl_s", WiSRefl)
+  , ("K_s", WiSK)
+  , ("J_s", WiSJ)
+
+  , ("lineToEquiv", WiLineToEquiv)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
   deriving (Show, Typeable)
   deriving anyclass (Exception)
 
--- Interval operations
-
 iand, ior :: Value -> Value -> Value
 iand x = case force x of
   VI1 -> id
@@ -191,6 +242,7 @@ ielim line left right (GluedVl h sp vl) i =
 ielim line left right fn i =
   case force fn of
     VLine _ _ _ fun -> fun @@ i
+    VLam _ (Closure _ k) -> k i
     x -> case force i of
       VI1 -> right
       VI0 -> left
@@ -198,46 +250,52 @@ ielim line left right fn i =
         VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
         VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
         VInc (VPath _ _ _) _ u -> ielim line left right u i
-        VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
+
+        VCase env r x xs -> VCase env r x (fmap (projIntoCase (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
+
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
-outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
-outS _ (force -> VI1) u _  = u @@ VItIsOne
+incS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value
+incS _ _ (force -> VNe h (sp Seq.:|> POuc _ _ _))
+  = VNe h sp
+incS a phi u = VInc a phi u
+
+outS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
+outS _ (force -> VI1) u _  = u @@ VReflStrict VI VI1
 
 outS _ _phi _ (VInc _ _ x) = x
 outS _ VI0 _  x            = x
 
-outS a phi u  (GluedVl x sp vl) = GluedVl x (sp Seq.:|> POuc a phi u) (outS a phi u vl)
-outS a phi u  (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
-outS a phi u (VSystem fs) = VSystem (fmap (outS a phi u) fs)
+outS a phi u (GluedVl x sp vl) = GluedVl x (sp Seq.:|> POuc a phi u) (outS a phi u vl)
+outS a phi u (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
+outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
--- Composition
-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 (Bound (T.pack "i") (negate 1)) of
+comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
+comp _a (force -> VI1) u _a0 =  u @@ VI1 @@ VReflStrict VI VI1
+comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
+  case force (a @@ VVar name) of
     VPi{} ->
       let
         plic i = let VPi p _ _ = force (a @@ i)              in p
         dom  i = let VPi _ d _ = force (a @@ i)              in d
         rng  i = let VPi _ _ (Closure _ r) =  force (a @@ i) in r
 
-        y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
+        y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (incS (dom VI0) phi y) i
         ybar i y = y' (inot i) y
        in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
               comp (line \i -> rng i (ybar i arg))
                    phi
                    (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
-                   (VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
+                   (incS (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
+
     VSigma{} ->
       let
         dom i = let VSigma d _             = force (a @@ i) in d
         rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r
 
-        w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i
-        -- c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0))
-        c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
+        w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (incS (dom VI0) phi (vProj1 a0)) i
+        c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (incS (rng VI0 (w VI0)) phi (vProj2 a0))
        in
          VPair (w VI1) c2
 
@@ -253,7 +311,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
             (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
                                                         , (j, v' i)
                                                         , (inot j, u' i)]))
-            (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
+            (incS (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
 
     VGlueTy _ thePhi theTypes theEquivs ->
       let
@@ -263,21 +321,21 @@ 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 (Bound "i" (negate 1)) i) thePhi
-        types i  = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes @@ VItIsOne
-        equivs i = substitute (Map.singleton (Bound "i" (negate 1)) i) theEquivs
+        phi i    = substitute (Map.singleton name i) thePhi
+        types i  = substitute (Map.singleton name i) theTypes @@ VReflStrict VI VI1
+        equivs i = substitute (Map.singleton name i) theEquivs
 
-        a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
+        a i u = unglue (base i) (phi i) (types i) (equivs i) (b @@ i @@ u)
         a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
 
         del = faceForall phi
-        a1' = comp (line base)  psi (system a) (VInc (base VI0) psi a0)
-        t1' = comp (line (const (types VI0))) psi (line (b @@)) (VInc (base VI0) psi b0)
+        a1' = comp (line base)  psi (system a) (incS (base VI0) psi a0)
+        t1' = comp (line (const (types VI0))) psi (line (b @@)) (incS (base VI0) psi b0)
 
         (omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
         omega = outS omega_t psi omega_rep omega_st
 
-        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
+        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VReflStrict VI VI1) (del `ior` psi) (fun ts) (fun ps) a1'
         t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
 
         (t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
@@ -286,30 +344,37 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
         ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
 
         a1 = comp
-          (fun (const (base VI1)))
-          (phi VI1 `ior` psi)
-          (system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
-                                                   , (psi, a VI1 VItIsOne)]))
-          (VInc (base VI1) (phi VI1 `ior` psi) a1')
-        b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
+              (fun (const (base VI1)))
+              (del `ior` psi)
+              (system \j _u -> mkVSystem (Map.fromList [ (del, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
+                                                       , (psi, a psi _u)
+                                                       ]))
+              (incS (base VI1) (phi VI1 `ior` psi) a1')
+        b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) (incS (base VI1) (ior (del `ior` psi) (inot del `iand` inot psi)) a1)
        in b1
 
     VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
-                            (fun' "is1" \_ -> mapVSystem makeEquiv (u @@ VVar (Bound (T.pack "_equivLine_") (negate 3)) @@ VItIsOne))
+                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))
 
     VNe (HData False _) Seq.Empty -> a0
     VNe (HData False _) args ->
       case force a0 of
         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
+          VNe (HCon con_type con_name) $ compConArgs makeSetFiller (length args) (a @@) con_type con_args phi u
+        _ -> VComp a phi u (incS (a @@ VI0) phi a0)
+
+    VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
+
+    _ -> VComp a phi u (incS (a @@ VI0) phi a0)
+  where
+    {-# NOINLINE name #-}
+    name :: Name
+    name = unsafePerformIO newName
 
-    VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
-    sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
+    {-# NOINLINE equivVar #-}
+    equivVar :: Name
+    equivVar = unsafePerformIO newName
 
-    _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
 
 mapVSystem :: (Value -> Value) -> Value -> Value
 mapVSystem f (VSystem fs) = VSystem (fmap f fs)
@@ -321,52 +386,63 @@ 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 _ a phi u a0 = error $ unlines
-  [ "*** TODO: composition for HIT: "
-  , "domain = " ++ show (prettyTm (quote (zonk (fun a))))
-  , "phi = " ++ show (prettyTm (quote (zonk phi)))
-  , "u = " ++ show (prettyTm (quote (zonk u)))
-  , "a0 = " ++ show (prettyTm (quote (zonk a0)))
-  ]
-
-
-compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection
-compConArgs total_args fam = go total_args where
+compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
+compHIT name n a phi u a0 =
+  case force phi of
+    VI1 -> u @@ VI1 @@ VReflStrict VI VI1
+    VI0 | n == 0    -> outS (a VI0) phi u a0
+        | regular   -> a0
+        | otherwise -> transHit name a VI0 (outS (a VI0) phi u a0)
+    x -> go n a x u a0
+  where
+    go 0 a phi u a0 = VHComp (a VI0) phi u a0
+    go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
+
+    regular = a VI0 == a VI1
+
+compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
+            -> Int
+            -> (Value -> Value)
+            -> Value
+            -> Seq.Seq Projection
+            -> t1 -> t2
+            -> Seq.Seq Projection
+compConArgs makeFiller total_args fam = go total_args where
   go _ _ Seq.Empty _ _ = Seq.Empty
   go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u
-    | nargs > 0 = assert (p == p') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
+    | nargs > 0 = assert (p == p') $
+        PApp p' (nthArg (total_args - nargs) (fam VI1)) Seq.:<| go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
     | otherwise = assert (p == p') $
-      let fill = makeFiller nargs dom phi u y
+      let fill = makeFiller typeArgument nargs dom phi u y
        in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u
   go _ _ _ _ _ = error $ "invalid constructor"
 
-  nthArg i (VNe hd s) =
-    case s Seq.!? i of
-      Just (PApp _ t) -> t
-      _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
-  nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs)
-  nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
+  smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
 
-  makeFiller nth (VNe (HData _ (Bound _ (negate -> 10))) args) phi u a0 =
-    fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
-  makeFiller _ _ _ _ a0 = fun (const a0)
-
-  makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
-  makeDomain _ = error "somebody smuggled something that smells"
+  typeArgument = unsafePerformIO newName
+  {-# NOINLINE typeArgument #-}
 
-  smuggle x = VNe (HData False (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x))
-
-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
-  compOutS _ _hi _0 (VInc _ _ x) = x
-  compOutS a phi a0 v = outS a phi a0 v
+makeSetFiller :: Name -> Int -> Value -> NFEndp -> Value -> Value -> Value
+makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0
+  | n' == typeArgument =
+    fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
+  where
+    makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
+    makeDomain _ = error "somebody smuggled something that smells"
+makeSetFiller _ _ _ _ _ a0 = fun (const a0)
+
+nthArg :: Int -> Value -> Value
+nthArg i (force -> VNe hd s) =
+  case s Seq.!? i of
+    Just (PApp _ t) -> t
+    _ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
+nthArg i (force -> VSystem vs) = VSystem (fmap (nthArg i) vs)
+nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
 
 system :: (Value -> Value -> Value) -> Value
-system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone
+system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "[i]" 0) \isone -> k i isone
 
-fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
+fill :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
 fill a phi u a0 j =
   comp (line \i -> a @@ (i `iand` j))
        (phi `ior` inot j)
@@ -374,23 +450,23 @@ fill a phi u a0 j =
                                                    , (inot j, outS a phi (u @@ VI0) a0)]))
        a0
 
-hComp :: NFSort -> NFEndp -> Value -> Value -> Value
-hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
+hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
+hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
 hComp a phi u a0 = VHComp a phi u a0
 
-glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
 glueType a phi tys eqvs = VGlueTy a phi tys eqvs
 
-glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
-glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
+glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
+glueElem _a _phi _tys _eqvs _t (force -> VInc _ _ (force -> VUnglue _ _ _ _ vl)) = vl
 glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
 
-unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
-unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
-unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ _ vl) = vl
+unglue   :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
+unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VReflStrict VI VI1) @@ x
+unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ t vl) = outS _a _phi (t @@ VReflStrict VI VI1) vl
 unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
 unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
--- Definition of equivalences
 
 faceForall :: (NFEndp -> NFEndp) -> Value
 faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
@@ -412,27 +488,28 @@ isContr :: Value -> Value
 isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y
 
 fiber :: NFSort -> NFSort -> Value -> Value -> Value
-fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
+fiber a b f y = exists' "x" a \x -> VPath (line (const b)) y (f @@ x)
 
 isEquiv :: NFSort -> NFSort -> Value -> Value
 isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
 
 equiv :: NFSort -> NFSort -> Value
-equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
+equiv a b = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f" (a ~> b) \f -> isEquiv a b f where
+  sp = Seq.fromList [ PApp P.Ex a, PApp P.Ex b ]
 
 pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
-pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
+pres tyT tyA f phi t t0 = (incS pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
   pathT = VPath (fun (const (tyA VI1))) c1 c2
-  c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
+  c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (incS (tyA VI0) phi (f VI0 @@ t0))
   c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0
 
   a0 = f VI0 @@ t0
   v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
 
-  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
+  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) (incS (tyA VI0) phi a0)
 
 opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
-opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
+opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
   fn = vProj1 f
   ty  = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x)
   v   = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))
@@ -440,33 +517,76 @@ opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u
 contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value
 contr a aC phi u =
   comp (line (const a))
-    phi
-    (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
-    (VInc a phi (vProj1 aC))
+       (ior phi (inot phi))
+       (system \i is1 -> mkVSystem $ Map.fromList [ (phi, ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
+                                                  , (inot phi, vProj1 aC)
+                                                  ])
+       (incS a phi (vProj1 aC))
 
 transp :: (NFEndp -> Value) -> Value -> Value
-transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
+transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line VI0) VI0 a0)
+
+gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
+gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (line VI0) VI0 a0)
+
+transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
+transHit name line phi x = transHit name line phi (force x) where
+  transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (outS (line VI0) phi u u0))
+  transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
+    x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+    (_, force -> VNe hd (length -> nargs)) = unPi con_type
+    ourType = case hd of
+      HData True n' -> n' == name
+      _ -> False
+
+  transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
+    x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
+    rec = transHit name line phi
+    (_, force -> VNe hd (length -> nargs)) = unPi con_type
+    ourType = case hd of
+      HData True n' -> n' == name
+      _ -> False
+
+  transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
+  transHit _ line phi a0 = gtrans line phi a0
+
+transFill :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
+transFill name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where
+
+transSqueeze :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
+transSqueeze name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)
+
+makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value
+makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
+  | n' == typeArgument = fun (transFill thedata (makeDomain args) phi a0)
+  where
+    makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
+    makeDomain _ = error "somebody smuggled something that smells"
+makeTransFiller _ _ _ _ _ _ a0 = fun (const 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 = makeEquiv' \x -> substitute (Map.singleton var x) vne
+
+makeEquiv' :: (NFEndp -> Value) -> Value
+makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
   where
-    line = fun \i -> substitute (Map.singleton (Bound (T.pack "_equivLine_") (negate 3)) (inot i)) argh
+    line = fun \i -> line' (inot i)
     a = line @@ VI0
     b = line @@ VI1
 
     f = fun \x -> transp (line @@) x
     g = fun \x -> transp ((line @@) . inot) x
-    u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI0 x) i
-    v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI1 x) (inot i)
+    u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) (incS a VI0 x) i
+    v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (incS a VI1 x) (inot i)
 
     fib y = VPair (g @@ y) (VLine b y (f @@ (g @@ y)) (fun (theta0 y VI1)))
-    theta0 y i j = fill line (ior j (inot j)) (system \i _ -> mkVSystem (Map.fromList [(j, v i @@ y), (inot j, u i @@ (g @@ y))])) (VInc a (ior j (inot j)) (g @@ y)) i
+    theta0 y i j = fill line (ior j (inot j)) (system \i _ -> mkVSystem (Map.fromList [(j, v i @@ y), (inot j, u i @@ (g @@ y))])) (incS a (ior j (inot j)) (g @@ y)) i
     theta1 x beta y i j =
       fill (fun ((line @@) . inot))
            (ior j (inot j))
            (system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y)
                                                    , (j, u (inot i) @@ x)]))
-           (VInc b (ior j (inot j)) (ielim b y (f @@ x) beta y))
+           (incS b (ior j (inot j)) (ielim b y (f @@ x) beta y))
            (inot i)
     omega x beta y = theta1 x beta y VI0
     delta x beta y j k = comp line (ior k (ior (inot k) (ior j (inot j))))
@@ -474,7 +594,7 @@ makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vPro
                                                                            , (k, theta1 x beta y i j)
                                                                            , (inot j, v i @@ y)
                                                                            , (j, u i @@ omega x beta y k)]))
-                                   (VInc a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k)))
+                                   (incS a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k)))
     p x beta y = VLine (exists a \x -> VPath b y (f @@ x)) (fib y) (VPair x beta) $ fun \k ->
       VPair (omega x beta y k) (VLine (VPath b y (f @@ x)) (vProj2 (fib y)) beta $ fun \j -> delta x beta y j k)
 
@@ -488,3 +608,26 @@ idEquiv a = VPair idfun idisequiv where
         ielim (fun (const a)) y y (vProj2 u) (iand i j)
 
   id_fiber y = VPair y (VLine a y y (fun (const y)))
+
+strictK :: DebugCallStack => Value -> Value -> Value -> Value -> Value -> Value
+strictK _ _ _ pr (VReflStrict _ _) = pr
+strictK a x bigp pr (VNe h sp) = VNe h (sp Seq.:|> PK a x bigp pr)
+strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
+  func = AxK (quote a) (quote x) (quote bigp) (quote pr)
+strictK a x bigp pr (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PK a x bigp pr) (strictK a x bigp pr vl)
+strictK _ _ _ _r eq = error $ "can't K " ++ show (prettyVl eq)
+
+strictJ :: DebugCallStack => Value -> Value -> Value -> Value -> Value -> Value -> Value
+strictJ _a _x _bigp pr _ (VReflStrict _ _) = pr
+strictJ a x bigp pr y (VNe h sp) = VNe h (sp Seq.:|> PJ a x bigp pr y)
+strictJ a x bigp pr y (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
+  func = AxJ (quote a) (quote x) (quote bigp) (quote pr) (quote y)
+strictJ a x bigp pr y (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PJ a x bigp pr y) (strictJ a x bigp pr y vl)
+strictJ _ _ _ _r _ eq = error $ "can't J " ++ show eq
+
+projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
+projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
+  go 0 x = fun x
+  go n (Lam p x r) = Lam p x (go (n - 1) r)
+  go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
+  go _ x = error $ show $ prettyTm x

src/Elab/WiredIn.hs-boot

@@ -1,8 +1,9 @@
-module Elab.WiredIn where
-
-import GHC.Stack.Types
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE KindSignatures #-}
+module Elab.WiredIn (wiType, wiValue, iand, ior, inot, ielim, incS, outS, comp, fill, hComp, glueType, glueElem, unglue, fun, system, strictK, strictJ, projIntoCase) where
 
 import Syntax
+import Debug (DebugCallStack)
 
 wiType  :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
@@ -11,14 +12,20 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp
 inot      :: NFEndp -> NFEndp
 ielim     :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
 
-outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
-comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
-fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value -> Value
-hComp :: NFSort -> NFEndp -> Value -> Value -> Value
+incS   :: DebugCallStack => NFSort -> NFEndp -> Value -> Value
+outS  :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
+comp  :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
+fill  :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value -> Value
+hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
 
-glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
-glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
-unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
+glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+unglue   :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
 
 fun :: (Value -> Value) -> Value
-system :: (Value -> Value -> Value) -> Value
+system :: (Value -> Value -> Value) -> Value
+
+strictK :: DebugCallStack => NFSort -> Value -> NFSort -> Value -> Value -> Value
+strictJ :: DebugCallStack => NFSort -> Value -> NFSort -> Value -> Value -> Value -> Value
+
+projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)

src/Main.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE NamedFieldPuns #-}
 module Main where
 
 import Control.Monad.IO.Class
@@ -11,7 +12,9 @@ import Control.Exception
 
 import qualified Data.ByteString.Lazy as Bsl
 import qualified Data.Text.Encoding as T
+import qualified Data.Text.Lazy.IO as Lt
 import qualified Data.Map.Strict as Map
+import qualified Data.Text.Lazy as Lt
 import qualified Data.Text.IO as T
 import qualified Data.Set as Set
 import qualified Data.Text as T
@@ -21,7 +24,7 @@ import Data.Foldable
 import Data.Maybe
 import Data.IORef
 
-import Debug.Trace
+import Debug (traceDocM)
 
 import Elab.Monad hiding (switch)
 import Elab.WiredIn
@@ -47,39 +50,93 @@ main :: IO ()
 main = do
   opts <- execParser parser
   case opts of
-    Load files -> do
+    Load files exp -> do
       env <- checkFiles files
-      enterReplIn env
+      case exp of
+        [] -> enterReplIn env
+        xs -> traverse_ (evalArgExpr env) xs
     Check files verbose -> do
       env <- checkFiles files
       when verbose $ dumpEnv env
-    Repl -> enterReplIn =<< checkFiles ["./test.tt"]
+    Repl -> enterReplIn =<< emptyEnv
+
+evalArgExpr :: ElabEnv -> String -> IO ()
+evalArgExpr env str =
+  case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseExp of
+    Right e ->
+      flip runElab env (do
+        (e, _) <- infer e
+        liftIO . print . prettyTm . quote =<< Elab.Eval.eval e)
+      `catch` \e -> do
+          displayExceptions' inp (e :: SomeException)
+    Left e -> liftIO $ print e
+  where
+    inp = T.pack str
 
 enterReplIn :: ElabEnv -> IO ()
-enterReplIn env = runInputT defaultSettings (loop env') where
-  env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk }
+enterReplIn env =
+  do
+    let env' = mkrepl env
+    envref <- newIORef env'
+    runInputT (setComplete (complete envref) defaultSettings) (loop env' envref)
+  where
+    mkrepl env = env { commHook = Lt.putStrLn . render }
 
-  loop :: ElabEnv -> InputT IO ()
-  loop env = do
-    inp <- fmap T.pack <$> getInputLine "% "
-    case inp of
-      Nothing -> pure ()
-      Just inp ->
-        case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
-          Left e -> do
-            liftIO $ print e
-            loop env
-          Right st -> do
-            env <- liftIO $
-              runElab (checkStatement st ask) env
-                `catch` \e -> do
-                  displayExceptions' inp (e :: SomeException)
-                  pure env
-            loop env
+    complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion])
+    complete c = completeWord Nothing " \n\t\r" go where
+      go w = do
+        env <- readIORef c
+        let
+          w' = T.pack w
+          words = Set.toList $ Set.filter ((w' `T.isPrefixOf`) . getNameText) (definedNames env)
+        pure (map (simpleCompletion . T.unpack . getNameText) words)
+
+    loop :: ElabEnv -> IORef ElabEnv -> InputT IO ()
+    loop env envvar = do
+      inp <- fmap T.pack <$> getInputLine "% "
+      case inp of
+        Nothing -> pure ()
+        Just inp | ":r" `T.isPrefixOf` inp -> reload env envvar
+        Just inp ->
+          case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
+            Left e -> do
+              liftIO $ print e
+              loop env envvar
+            Right st -> do
+              env <- liftIO $
+                runElab (checkStatement st ask) env
+                  `catch` \e -> do
+                    displayExceptions' inp (e :: SomeException)
+                    pure env
+
+              metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
+              unless (Map.null metas) $ do
+                liftIO $ reportUnsolved (Just inp) metas
+
+              liftIO $ writeIORef envvar env
+              loop env envvar
+
+    reload :: ElabEnv -> IORef ElabEnv -> InputT IO ()
+    reload env@ElabEnv{loadedFiles} envref = do
+      newe <- liftIO $ try $ mkrepl <$> checkFiles (reverse loadedFiles)
+      case newe of
+        Left e -> do
+          liftIO $ do displayExceptions' ":r" (e :: SomeException)
+          loop env envref
+        Right newe -> do
+          liftIO $ writeIORef envref newe
+          loop newe envref
 
 checkFiles :: [String] -> IO ElabEnv
-checkFiles files = runElab (go files ask) =<< emptyEnv where
-  go [] k = do
+checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
+  size = length files
+  sl = length (show size)
+
+  pad s
+    | length s < sl = replicate (sl - length s) ' ' ++ s
+    | otherwise = s
+
+  go _ [] k = do
     env <- ask
     for_ (Map.toList (nameMap env)) \case
       (_, v@Defined{})
@@ -87,41 +144,51 @@ checkFiles files = runElab (go files ask) =<< emptyEnv where
         | otherwise ->
           let
             pos = fromJust (Map.lookup v (whereBound env))
-           in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v
+           in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
       _ -> pure ()
 
-    metas <- liftIO $ readIORef (unsolvedMetas env)
+    metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
     unless (Map.null metas) $ do
-      liftIO $ reportUnsolved metas
-
+      liftIO $ reportUnsolved Nothing metas
     k
-  go (x:xs) k = do
+
+  go n (x:xs) k = do
+    liftIO . putStrLn $ "[" ++ pad (show n) ++ "/" ++ show size ++ "] Loading " ++ x
     code <- liftIO $ Bsl.readFile x
     case runAlex (code <> Bsl.singleton 10) parseProg of
-      Left e -> liftIO $ print e *> error (show e)
+      Left e -> liftIO (print e) *> k
       Right prog ->
-        local (\e -> e { currentFile = Just (T.pack x) }) (checkProgram prog (go xs k))
+        local (\e -> e { currentFile = Just (T.pack x), loadedFiles = x:loadedFiles e }) (checkProgram prog (go (n + 1 :: Int) xs k))
           `catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException)
 
 dumpEnv :: ElabEnv -> IO ()
 dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) ->
   let nft = fst $ getEnv env Map.! name in
-  T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
+  Lt.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
 
 parser :: ParserInfo Opts
-parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
+parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
   where
-    load  = command "load" $ info (fmap Load (some (argument str (metavar "file..."))) <**> helper) (progDesc "Check and load a list of files in the REPL")
+    load  = command "load" $
+      info ((Load <$> (some (argument str (metavar "file...")))
+                  <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
+       <**> helper) (progDesc "Check and load a list of files in the REPL")
+
+    repl  = command "load" $
+      info ((Load <$> (many (argument str (metavar "file...")))
+                  <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
+       <**> helper) (progDesc "Enter the REPL, optionally with loaded files")
+
     check = command "check" $
       info ((Check <$> some (argument str (metavar "file..."))
-                  <*> switch ( long "verbose"
-                            <> short 'v'
-                            <> help "Print the types of all declared/defined values"))
+                   <*> switch ( long "verbose"
+                             <> short 'v'
+                             <> help "Print the types of all declared/defined values"))
        <**> helper)
            (progDesc "Check a list of files")
 
 data Opts
-  = Load  { files :: [String] }
+  = Load  { files :: [String], eval :: [String] }
   | Check { files :: [String], verbose :: Bool }
   | Repl
   deriving (Eq, Show, Ord)
@@ -141,44 +208,65 @@ displayExceptions lines =
       T.putStrLn $ squiggleUnder a b lines
   , Handler \(AttachedNote n e) -> do
       displayExceptions' lines e
-      T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
-  , Handler \(WhenCheckingEndpoint le ri ep e) -> do
+      Lt.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
+  , Handler \(WhenCheckingEndpoint dir le ri ep e) -> do
       displayExceptions' lines e
       let
         endp = case ep of
-          VI0 -> T.pack "left"
-          VI1 -> T.pack "right"
-          _ -> T.pack $ show (prettyTm (quote ep))
-      T.putStrLn . T.unlines $
-        [ "\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram"
-        , "\t " <> render (prettyTm (quote le)) <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> render (prettyTm (quote ri))
-        , "\x1b[1;32mnote\x1b[0m: the " <> endp <> " endpoint is incorrect"
+          VI0 -> Lt.pack "left"
+          VI1 -> Lt.pack "right"
+          _ -> render . prettyTm $ quoteWith False mempty ep
+        left = render (prettyTm (quoteWith False mempty le))
+        right = render (prettyTm (quoteWith False mempty ri))
+      Lt.putStrLn . Lt.unlines $
+        [ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<"
+        , "\t " <> redact left <> " " <> Lt.replicate 7 (Lt.singleton '\x2500') <> " " <> redact right
+        , "      >> in the direction " <> render (pretty dir) <> ", but the " <> endp <> " endpoint is incorrect"
         ]
   , Handler \(NotEqual ta tb) -> do
-      putStrLn . unlines $
+      Lt.putStrLn . render . vsep $
         [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
-        , "  * \x1b[1mActual\x1b[0m:   " ++ showValue (zonk ta)
-        , "  * \x1b[1mExpected\x1b[0m: " ++ showValue (zonk tb)
+        , indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta))
+        , indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb))
         ]
   , Handler \(NoSuchPrimitive x) -> do
       putStrLn $ "Unknown primitive: " ++ T.unpack x
   , Handler \(NotInScope x) -> do
       putStrLn $ "Variable not in scope: " ++ show (pretty x)
-  , Handler \(DeclaredUndefined n) -> do
+  , Handler \(Elab.DeclaredUndefined n) -> do
       putStrLn $ "Name declared but not defined: " ++ show (pretty n)
+  , Handler \Elab.PathConPretype -> do
+      putStrLn $ "Pretypes can not have path constructors, either change this definition so it lands in Type or remove it."
   ]
 
-reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
-reportUnsolved metas = do
+redact :: Lt.Text -> Lt.Text
+redact x
+  | length (Lt.lines x) >= 2 = head (Lt.lines x) <> Lt.pack "\x1b[1;32m[...]\x1b[0m"
+  | otherwise = x
+
+reportUnsolved :: Foldable t => Maybe Text -> Map.Map MV (t (Seq Projection, Value)) -> IO ()
+reportUnsolved code metas = do
   for_ (Map.toList metas) \(m, p) ->  do
     case mvSpan m of
-      Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
+      Just (f, s, e) ->
+        case code of
+          Just code -> T.putStrLn $ squiggleUnder s e code
+          Nothing -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
       Nothing -> pure ()
-    T.putStrLn . render $
-      "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:"
-    for_ p \p ->
-      T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
 
+    case null p of
+      True -> do
+        Lt.putStrLn . render $ "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <> pretty '.')
+      _ -> do
+        Lt.putStrLn . render $
+          "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <+> "should satisfy:")
+        for_ p \p ->
+          Lt.putStrLn . render $ indent 2 $ prettyTm (quote (zonk (VNe (HMeta m) (fst p)))) <+> pretty '≡' <+> prettyTm (quote (snd p))
+    
+    when (mvInteraction m && not (Map.null (mvContext m))) do
+      putStrLn "Context (first 10 entries):"
+      for_ (take 10 (Map.toList (mvContext m))) \(x, t) -> unless (isIdkT t) do
+        Lt.putStrLn . render $ indent 2 $ pretty x <+> pretty ':' <+> prettyVl (zonk t)
 
 displayExceptions' :: Exception e => Text -> e -> IO ()
 displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure ()
@@ -194,14 +282,11 @@ squiggleUnder (Posn l c) (Posn l' c') file
      in T.unlines [ padding, line, padding <> squiggle ]
   | otherwise = T.unlines (take (l' - l) (drop l (T.lines file)))
 
-newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
-  deriving (Eq, Show, Exception)
-
 dumpTokens :: Alex ()
 dumpTokens = do
   t <- alexMonadScan
   case tokenClass t of
     TokEof -> pure ()
     _ -> do
-      traceM (show t)
+      traceDocM (viaShow t)
       dumpTokens

src/Presyntax/Lexer.x

@@ -7,6 +7,8 @@ import qualified Data.Text as T
 
 import Presyntax.Tokens
 
+import Debug.Trace
+
 }
 
 %wrapper "monadUserState-bytestring"
@@ -32,13 +34,14 @@ tokens :-
 
 <0> \\                            { always TokLambda }
 <0> "->"                          { always TokArrow }
+<0> "_"                           { always TokUnder }
 
 <0> \(                            { always TokOParen }
 <0> \{                            { always TokOBrace }
 <0> \[                            { always TokOSquare }
 
 <0> \)                            { always TokCParen }
-<0> \}                            { always TokCBrace }
+<0> \}                            { closeBrace }
 <0> \]                            { always TokCSquare }
 
 <0> \;                            { always TokSemi }
@@ -71,6 +74,7 @@ tokens :-
 -- layout: indentation of the next token is context for offside rule
 <layout> {
   \n ;
+  \{ { openBrace }
   () { startLayout }
 }
 
@@ -115,7 +119,7 @@ popStartCode = do
       alexSetStartCode x
 
 offsideRule :: AlexInput -> Int64 -> Alex Token
-offsideRule (AlexPn _ line col, _, s, _) size
+offsideRule (AlexPn _ line col, _, _, _) _
 --  | Lbs.null s = pure (Token TokEof line col)
   | otherwise = do
     ~(col':ctx) <- layoutColumns <$> getUserState
@@ -137,15 +141,28 @@ emptyLayout (AlexPn _ line col, _, _, _) _ = do
   pure (Token TokLEnd line col)
 
 startLayout :: AlexInput -> Int64 -> Alex Token
-startLayout (AlexPn _ line col, _, s, _) size = do
+startLayout (AlexPn _ line col, _, _, _) _ = do
   popStartCode
-  least <- leastColumn <$> getUserState
   ~(col':_) <- layoutColumns <$> getUserState
   if col' >= col
     then pushStartCode empty_layout
     else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s }
   pure (Token TokLStart line col)
 
+openBrace :: AlexInput -> Int64 -> Alex Token
+openBrace (AlexPn _ line col, _, _, _) _ = do
+  popStartCode
+  mapUserState $ \s -> s { layoutColumns = minBound:layoutColumns s }
+  pure (Token TokOBrace line col)
+
+closeBrace :: AlexInput -> Int64 -> Alex Token
+closeBrace (AlexPn _ line col, _, _, _) _ = do
+  ~(col':tail) <- layoutColumns <$> getUserState
+  if col' < 0
+    then mapUserState $ \s -> s { layoutColumns = tail }
+    else pure ()
+  pure (Token TokCBrace line col)
+
 variableOrKeyword :: AlexAction Token
 variableOrKeyword (AlexPn _ l c, _, s, _) size =
   let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in
@@ -166,4 +183,4 @@ laidOut x l c = do
   mapUserState $ \s -> s { leastColumn = c }
   pure (Token x l c)
 
-}
+}

src/Presyntax/Parser.y

@@ -1,5 +1,5 @@
 {
-{-# LANGUAGE FlexibleInstances, ViewPatterns #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, ViewPatterns #-}
 module Presyntax.Parser where
 
 import qualified Data.Text as T
@@ -50,6 +50,7 @@ import Debug.Trace
   '\\'        { Token TokLambda _ _ }
   
   '->'        { Token TokArrow _ _ }
+  '_'         { Token TokUnder _ _ }
   ':'         { Token TokColon _ _ }
   ';'         { Token TokSemi  _ _ }
   '='         { Token TokEqual _ _ }
@@ -80,8 +81,8 @@ import Debug.Trace
 Exp :: { Expr }
 Exp
   : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
-  | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
-  | '\\' 'case' START CaseList END       { span $1 $5 $ LamCase $4 }
+  | '\\' MaybeLambdaList '[' Faces ']'   { span $1 $5 $ makeLams $2 $ LamSystem $4 }
+  | '\\' 'case' Block(CaseList)          { span $1 $3 $ LamCase (thd $3) }
   | '(' var ':' Exp ')' ProdTail         { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
   | '{' var ':' Exp '}' ProdTail         { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
   | ExpApp '->' Exp                      { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
@@ -89,8 +90,7 @@ Exp
   | '(' var ':' Exp ')' '*'  Exp         { span $1 $7 $ Sigma (getVar $2) $4 $7 }
   | ExpApp '*' Exp                       { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
 
-  | 'let' START LetList END 'in' Exp     { span $1 $6 $ Let $3 $6 }
-  | 'let' START LetList END Exp          { span $1 $5 $ Let $3 $5 }
+  | 'let' Block(LetList) 'in' Exp        { span $1 $4 $ Let (thd $2) $4 }
 
   | ExpApp                               { $1 }
 
@@ -110,6 +110,7 @@ Tuple :: { Expr }
 
 Atom :: { Expr }
   : var           { span $1 $1 $ Var (getVar $1) }
+  | '_'           { span $1 $1 $ Hole }
   | '(' Tuple ')' { span $1 $3 $ $2 }
 
 ProdTail :: { Expr }
@@ -123,7 +124,9 @@ MaybeLambdaList :: { [(Plicity, Text)] }
 
 LambdaList :: { [(Plicity, Text)] }
   : var            { [(Ex, getVar $1)] }
+  | '_'            { [(Ex, T.singleton '_')] }
   | var LambdaList { (Ex, getVar $1):$2 }
+  | '_' LambdaList { (Ex, T.singleton '_'):$2 }
 
   | '{'var'}'            { [(Im, getVar $2)] }
   | '{'var'}' LambdaList { (Im, getVar $2):$4 }
@@ -149,7 +152,8 @@ CaseItem :: { (Pattern, Expr) }
   : Pattern '->' Exp { ($1, $3) }
   
 CaseList :: { [(Pattern, Expr)] }
-  : CaseItem                { [$1] }
+  :                         { [] }
+  | CaseItem                { [$1] }
   | CaseItem Semis CaseList { $1:$3 }
 
 Pattern :: { Pattern }
@@ -163,12 +167,14 @@ Statement :: { Statement }
   : VarList ':' Exp                  { spanSt $1 $3 $ Decl (thd $1) $3 }
   | var LhsList '=' Rhs              { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
   | '{-#' Pragma '#-}'               { spanSt $1 $3 $ $2 }
-  | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 }
-  | 'data' var Parameters ':' Exp 'where' START Constructors END
-    { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 }
+
+  | 'postulate' Block(Postulates)    { spanSt $1 $2 $ Postulate (thd $2) }
+  | 'data' var Parameters ':' Exp 'where' Block(Constructors)
+    { spanSt $1 $7 $ Data (getVar $2) $3 $5 (thd $7) }
 
 Constructors :: { [(Posn, Posn, Constructor)] }
-  : var ':' Exp                          { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
+  :                                      { [] }
+  | var ':' Exp                          { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
   | var PatVarList ':' Exp '[' Faces ']' { [(startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6)] }
   | var ':' Exp Semis Constructors       { (startPosn $1, endPosn $3, Point (getVar $1) $3):$5 }
   | var PatVarList ':' Exp '[' Faces ']' Semis Constructors
@@ -213,18 +219,6 @@ Pragma :: { Statement }
   : 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) }
   | 'PRIMITIVE' var     { Builtin (getVar $2) (getVar $2) }
 
-System :: { [(Condition, Expr)] }
-  : {- empty system -}            { [] }
-  | NeSystem                      { $1 }
-
-NeSystem :: { [(Condition, Expr) ]}
-  : SystemLhs '->' Exp              { [($1, $3)] }
-  | SystemLhs '->' Exp ',' NeSystem { ($1, $3):$5 }
-
-SystemLhs :: { Condition }
-  : Formula 'as' var { Condition $1 (Just (getVar $3)) }
-  | Formula          { Condition $1 Nothing }
-
 Faces :: { [(Formula, Expr)] }
   : {- empty system -}            { [] }
   | NeFaces                       { $1 }
@@ -250,6 +244,10 @@ FAtom :: { Formula }
       x -> parseError (x, ["i0", "i1"])
   }
 
+Block(p)
+  : START p END { (startPosn $1, endPosn $3, $2) }
+  | '{' p '}'   { (startPosn $1, endPosn $3, $2) }
+
 {
 lexer cont = alexMonadScan >>= cont
 

src/Presyntax/Presyntax.hs

@@ -10,6 +10,7 @@ data Plicity
 
 data Expr
   = Var Text
+  | Hole
 
   | App Plicity Expr Expr
   | Pi  Plicity Text Expr Expr
@@ -20,7 +21,7 @@ data Expr
   | Proj1 Expr
   | Proj2 Expr
 
-  | LamSystem [(Condition, Expr)]
+  | LamSystem [(Formula, Expr)]
   | LamCase [(Pattern, Expr)]
   | Let [LetItem] Expr
 
@@ -32,10 +33,6 @@ data LetItem
   | LetBind { leIName :: Text, leIVal :: Expr }
   deriving (Eq, Show, Ord)
 
-data Condition
-  = Condition { condF :: Formula, condV :: Maybe Text }
-  deriving (Eq, Show, Ord)
-
 data Formula
   = FIs1 Text
   | FIs0 Text

src/Presyntax/Tokens.hs

@@ -9,6 +9,7 @@ data TokenClass
 
   | TokLambda
   | TokArrow
+  | TokUnder
 
   | TokOParen
   | TokOBrace
@@ -70,6 +71,7 @@ tokSize TokColon = 1
 tokSize TokEqual = 1
 tokSize TokComma = 1
 tokSize TokSemi = 1
+tokSize TokUnder = 1
 tokSize TokArrow = 2
 tokSize TokPi1 = 2
 tokSize TokPi2 = 2

src/Syntax.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -28,11 +29,9 @@ data WiredIn
   | WiINot
   | WiPathP
 
-  | WiIsOne   -- Proposition associated with an element of the interval
-  | WiItIsOne -- 1 = 1
-
   | WiPartial  -- (φ : I) -> Type           -> Typeω
   | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
+  | WiPOr      -- (A : Type) (φ ψ : I) -> Partial φ A -> Partial ψ A -> Partial (ior φ ψ) A
 
   | WiSub      -- (A : Type) (φ : I) -> Partial φ A -> Typeω
   | WiInS      -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u)
@@ -40,11 +39,19 @@ data WiredIn
 
   | WiComp  --    {A : I -> Type} {phi : I}
             -- -> ((i : I) -> Partial phi (A i)
-            -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
+            -- -> (A i0)[phi -> u i0] -> A i1
 
   | WiGlue      -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
   | WiGlueElem  -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
   | WiUnglue    -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
+
+  | WiLineToEquiv -- {A : I -> Type} -> Equiv (P i0) (P i1)
+
+  -- Two-level
+  | WiSEq   -- Eq_s   : {A : Pretype} (x y : A) -> Pretype
+  | WiSRefl -- refl_s : {A : Pretype} {x : A} -> EqS {A} x x
+  | WiSK    -- K_s    : {A : Pretype} {x : A} (P : x = x -> Pretype) -> P refl -> (p : x = x) -> P p
+  | WiSJ    -- J_s   : {A : Pretype} {x : A} (P : (y : A) -> x = y -> Pretype) -> P x refl -> {y : A} -> (p : x = y) -> P y p
   deriving (Eq, Show, Ord)
 
 data Term
@@ -79,9 +86,6 @@ data Term
   -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
   --   ~~~~~~~~~ not printed at all
 
-  | IsOne Term
-  | ItIsOne
-
   | Partial  Term Term
   | PartialP Term Term
 
@@ -98,7 +102,12 @@ data Term
   | Glue Term Term Term Term Term Term
   | Unglue Term Term Term Term Term
 
-  | Case Term Term [(Term, Term)]
+  | Case Term Term [(Term, Int, Term)]
+
+  | EqS  Term Term Term
+  | Refl Term Term
+  | AxK  Term Term Term Term Term
+  | AxJ  Term Term Term Term Term Term
   deriving (Eq, Show, Ord, Data)
 
 data MV =
@@ -106,6 +115,8 @@ data MV =
      , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
      , mvType :: NFType
      , mvSpan :: Maybe (Text, Posn, Posn)
+     , mvInteraction :: Bool
+     , mvContext :: Map Name NFType
      }
 
 instance Eq MV where
@@ -159,9 +170,6 @@ data Value
   | VPath NFLine Value Value
   | VLine NFLine Value Value Value
 
-  | VIsOne NFEndp
-  | VItIsOne
-
   | VPartial  NFEndp Value
   | VPartialP NFEndp Value
   | VSystem (Map Value Value)
@@ -176,14 +184,17 @@ data Value
   | VGlue   NFSort NFEndp NFPartial NFPartial NFPartial Value
   | VUnglue NFSort NFEndp NFPartial NFPartial Value
 
-  | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Term)]
+  | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Int, Term)]
+
+  | VEqStrict   NFSort Value Value
+  | VReflStrict NFSort Value
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
 pattern VVar x = VNe (HVar x) Seq.Empty
 
-quoteWith :: Set Name -> Value -> Term
-quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
+quoteWith :: Bool -> Set Name -> Value -> Term
+quoteWith short names (VNe h sp) = foldl goSpine (goHead h) sp where
   goHead (HVar v)    = Ref v
   goHead (HMeta m)   = Meta m
   goHead (HCon _ v)  = Con v
@@ -193,74 +204,89 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
         case Map.lookup VI1 f of
           Just vl -> constantly (length sp) vl
           _ -> PCon (quote sys) v
-      _ -> PCon (quote sys) v
+      VLam{} -> PCon (quote sys) v
+      s -> constantly (length sp) s
   goHead (HData x v) = Data x v
 
-  goSpine t (PApp p v) = App p t (quoteWith names v)
+  goSpine t (PApp p v) = App p t (quoteWith short names v)
   goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
+  goSpine t (PK l x y i) = AxK (quote l) (quote x) (quote y) (quote i) t
+  goSpine t (PJ l x y i f) = AxJ (quote l) (quote x) (quote y) (quote i) (quote f) t
   goSpine t PProj1 = Proj1 t
   goSpine t PProj2 = Proj2 t
   goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
 
-  constantly 0 n = quoteWith names n
+  constantly 0 n = quoteWith short names n
   constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) x
 
-quoteWith names (GluedVl _ Seq.Empty x) = quoteWith names x
+quoteWith short names (GluedVl _ Seq.Empty x) = quoteWith short names x
+
+quoteWith short names (GluedVl h sp (VLam p (Closure n k))) =
+  quoteWith short names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
 
-quoteWith names (GluedVl h sp (VLam p (Closure n k))) =
-  quoteWith names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
+quoteWith short names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
+  quoteWith short names (VLine ty x y (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PIElim ty x y a) (k a)))))
 
-quoteWith names (GluedVl h sp vl)
-  | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
-  | True || alwaysShort vl = quoteWith names vl
-  | otherwise = quoteWith names (VNe h sp)
+quoteWith short names (GluedVl h sp vl)
+  | GluedVl _ _ inner <- vl = quoteWith short names (GluedVl h sp inner)
+  | short || alwaysShort vl = quoteWith short names vl
+  | _ Seq.:|> PIElim _ x y i <- sp =
+    case i of
+      VI0 -> quoteWith short names x
+      VI1 -> quoteWith short names y
+      _ -> quoteWith short names (VNe h sp)
+  | otherwise = quoteWith short names (VNe h sp)
 
-quoteWith names (VLam p (Closure n k)) =
+quoteWith short names (VLam p (Closure n k)) =
   let n' = refresh Nothing names n
-   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Lam p n' (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VPi p d (Closure n k)) =
+quoteWith short names (VPi p d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Pi p n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VSigma d (Closure n k)) =
+quoteWith short names (VSigma d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
+   in Sigma n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
 
-quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
-quoteWith _ VType = Type
-quoteWith _ VTypeω = Typeω
+quoteWith short names (VPair a b) = Pair (quoteWith short names a) (quoteWith short names b)
+quoteWith _ _ VType = Type
+quoteWith _ _ VTypeω = Typeω
 
-quoteWith _ VI     = I
-quoteWith _ VI0    = I0
-quoteWith _ VI1    = I1
-quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
-quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
-quoteWith names (VINot x) = INot (quoteWith names x)
+quoteWith _ _ VI     = I
+quoteWith _ _ VI0    = I0
+quoteWith _ _ VI1    = I1
+quoteWith short names (VIAnd x y) = IAnd (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VIOr x y) = IOr (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VINot x) = INot (quoteWith short names x)
 
-quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
-quoteWith names (VLine p x y f)  = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
+quoteWith short names (VPath line x y) = PathP (quoteWith short names line) (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VLine p x y f)  = PathIntro (quoteWith short names p) (quoteWith short names x) (quoteWith short names y) (quoteWith short names f)
 
-quoteWith names (VIsOne v)  = IsOne (quoteWith names v)
-quoteWith _     VItIsOne    = ItIsOne
+quoteWith short names (VPartial x y)  = Partial (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VPartialP x y) = PartialP (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith short names x, quoteWith short names y)) (Map.toList fs)))
+quoteWith short names (VSub a b c) = Sub (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
+quoteWith short names (VInc a b c) = Inc (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
+quoteWith short names (VComp a phi u a0) = Comp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
+quoteWith short names (VHComp a phi u a0) = HComp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
 
-quoteWith names (VPartial x y)  = Partial (quoteWith names x) (quoteWith names y)
-quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
-quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
-quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c)
-quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
-quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
-quoteWith names (VHComp a phi u a0) = HComp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
+quoteWith short names (VGlueTy a phi t e)    = GlueTy (quoteWith short names a) (quoteWith short names phi) (quoteWith short names t) (quoteWith short names e)
+quoteWith short names (VGlue a phi ty e t x) = Glue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names t) (quoteWith short names x)
+quoteWith short names (VUnglue a phi ty e x) = Unglue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names x)
 
-quoteWith names (VGlueTy a phi t e)    = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e)
-quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x)
-quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x)
+quoteWith short names (VCase _ rng v xs) = Case (quoteWith short names rng) (quoteWith short names v) xs
 
-quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
+quoteWith short names (VEqStrict a x y) = EqS (quoteWith short names a) (quoteWith short names x) (quoteWith short names y)
+quoteWith short names (VReflStrict a x) = Syntax.Refl (quoteWith short names a) (quoteWith short names x)
 
 alwaysShort :: Value -> Bool
 alwaysShort (VNe HCon{} _) = True
+alwaysShort (VNe HPCon{} _) = True
 alwaysShort VVar{} = True
+alwaysShort (VLine _ _ _ v) = alwaysShort v
+alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n))
+alwaysShort VHComp{} = True
 alwaysShort _ = False
 
 refresh :: Maybe Value -> Set Name -> Name -> Name
@@ -271,7 +297,7 @@ refresh x s n
   | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
 
 quote :: Value -> Term
-quote = quoteWith mempty
+quote = quoteWith True mempty
 
 data Closure
   = Closure
@@ -296,15 +322,31 @@ data Head
   | HPCon Value Value Name
   | HMeta MV
   | HData Bool Name
-  deriving (Eq, Ord, Show)
+  deriving (Ord, Show)
+
+instance Eq Head where
+  HVar x == HVar y = x == y
+  HCon _ x == HCon _ y = x == y
+  HPCon _ _ x == HPCon _ _ y = x == y
+  HMeta x == HMeta y = x == y
+  HData x y == HData x' y' = x == x' && y == y'
+  _ == _ = False
 
 data Projection
   = PApp   Plicity Value
   | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
-  | POuc   NFSort NFEndp Value
+  | POuc  NFSort NFEndp Value
+  | PK    NFSort Value NFSort Value
+  | PJ    NFSort Value NFSort Value Value
   deriving (Eq, Show, Ord)
 
 data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value }
   deriving (Eq, Show, Ord)
+
+unPi :: Value -> ([(Plicity, Value)], Value)
+unPi (VPi p d (Closure n k)) =
+  let (a, x) = unPi (k (VVar n))
+   in ((p, d):a, x)
+unPi x = ([], x)

src/Syntax/Pretty.hs

@@ -1,17 +1,14 @@
+{-# LANGUAGE LambdaCase #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE CPP #-}
 module Syntax.Pretty where
 
-import Control.Arrow (Arrow(first))
-
 import qualified Data.Map.Strict as Map
-import qualified Data.Text.Lazy as L
-import qualified Data.Set as Set
+import qualified Data.Text.Lazy as Lazy
 import qualified Data.Text as T
 import Data.Map.Strict (Map)
-import Data.Text (Text)
-import Data.Set (Set)
-import Data.Generics
 
 import Presyntax.Presyntax (Plicity(..))
 
@@ -21,190 +18,216 @@ import Prettyprinter
 import Syntax
 
 instance Pretty Name where
-  pretty = pretty . getNameText
-
-prettyTm :: Term -> Doc AnsiStyle
-prettyTm = prettyTm . everywhere (mkT beautify) where
-  prettyTm (Ref v) =
-    case T.uncons (getNameText v) of
-      Just ('.', w) -> keyword (pretty w)
-      _ -> pretty v
-  prettyTm (Con v) = keyword (pretty v)
-  prettyTm (PCon _ v) = keyword (pretty v)
-  prettyTm (Data _ v) = operator (pretty v)
-
-  prettyTm (App Im f _) = prettyTm f
-  prettyTm (App Ex f x) = parenFun f <+> parenArg x
-
-  prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
-  prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
-  prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
-
-  prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> nest 2 (prettyTm bod) where
-    unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
-    unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
-    unwindLam t = ([], t)
-
-    (al, bod) = unwindLam l
-
-    used = freeVars bod
-
-    prettyArgList (Ex, v)
-      | v `Set.member` used = pretty v
-      | otherwise = pretty "_"
-    prettyArgList (Im, v)
-      | v `Set.member` used = braces $ pretty v
-      | otherwise = pretty "_"
-
-  prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
-  prettyTm Type{}  = keyword $ pretty "Type"
-  prettyTm Typeω{} = keyword $ pretty "Typeω"
-  prettyTm I{}     = keyword $ pretty "I"
-  prettyTm I0{}    = keyword $ pretty "i0"
-  prettyTm I1{}    = keyword $ pretty "i1"
+  pretty x = pretty (getNameText x) -- <> pretty '\'' <> pretty (getNameNum x)
+
+prettyTm' :: Bool -> Term -> Doc AnsiStyle
+prettyTm' implicits = go True 0 where
+  go t p =
+    \case
+      Ref v    -> pretty v
+      Con v    -> keyword $ pretty v
+      PCon _ v -> keyword $ pretty v
+      Data _ v -> keyword $ pretty v
+
+      App Im f x
+        | implicits -> parenIf (p >= arg_prec) $
+            go False fun_prec f
+        <+> braces (go False 0 x)
+        | otherwise -> go t p f
+      App Ex f x ->
+        parenIf (p >= arg_prec) $
+              go False fun_prec f
+          <+> group (go False arg_prec x)
+
+      Lam Ex v (App Ex f (Ref v')) | v == v' -> instead f
+      Lam i v t ->
+        let
+          getArgs (Lam i v t) =
+            let (as, b) = getArgs t in ((i, v):as, b)
+          getArgs (PathIntro _ _ _ (Lam _ v t)) =
+            let (as, b) = getArgs t in ((Ex, v):as, b)
+          getArgs t = ([], t)
+
+          (as, b) = getArgs (Lam i v t)
+        in
+          parenIf (p >= fun_prec) . group $
+            pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as)
+              <+> arrow
+              <+> nest 2 (go False 0 b)
+
+      Pi _ (T.unpack . getNameText -> "_") d r ->
+        parenIf (p >= fun_prec) $
+          group (go False dom_prec d)
+            <> space <> arrow <> sp
+            <> go t 0 r
+
+      Pi i x d r ->
+        let
+          c = case r of
+            Pi _ (getNameText -> x) _ _ | x /= T.pack "_" -> sp
+            _ -> space <> arrow <> sp
+        in
+          parenIf (p >= fun_prec) $
+            plic i (pretty x <+> colon <+> go False 0 d)
+              <> c <> go t 0 r
+
+      Let binds body ->
+        parenIf (p >= fun_prec) $
+          align $ keyword (pretty "let")
+              <> line
+              <> indent 2 (prettyBinds False binds)
+              <> keyword (pretty "in")
+              <+> go False 0 body
+
+      Meta MV{mvName} -> keyword (pretty '?' <> pretty mvName)
+
+      Type -> keyword (pretty "Type")
+      Typeω -> keyword (pretty "Pretype")
+
+      Sigma (T.unpack . getNameText -> "_") d r ->
+        parenIf (p >= fun_prec) $
+              go False dom_prec d
+          <+> operator (pretty "*")
+          <+> go False dom_prec r
+      Sigma v d r ->
+        parenIf (p >= fun_prec) . align $
+          group (parens (pretty v <+> colon <+> go False 0 d))
+            <+> operator (pretty "*") <+> go False dom_prec r
+
+      Pair a b -> parens $ go False 0 a <> comma <+> go False 0 b
+      Proj1 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".1")
+      Proj2 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".2")
+
+      I -> keyword (pretty "I")
+      I0 -> keyword (pretty "i0")
+      I1 -> keyword (pretty "i1")
+
+      IAnd x y -> parenIf (True || p > and_prec) $
+        go False and_prec x <+> operator (pretty "/\\") <+> go False and_prec y
+
+      IOr x y -> parenIf (True || p > or_prec) $
+        go False or_prec x <+> operator (pretty "\\/") <+> go False or_prec y
+
+      INot x -> operator (pretty "~") <> go False p x
+
+      PathP _ x y -> parenIf (p >= arg_prec) $
+        go False 0 x <+> operator (pretty "≡") <+> go False 0 y
+
+      IElim _a _x _y f i -> instead (App Ex f i)
+      PathIntro _a _x _y f -> instead f
+
+      Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
+      PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
+
+      System fs | Map.null fs -> brackets mempty
+      System fs ->
+        let
+          face (f, t) = go False 0 f <+> operator (pretty "=>") <+> go False 0 t
+        in
+          brackets (line <> nest 2 (vsep (punctuate comma (map face (Map.toList fs)))) <> line)
+
+      Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
+      Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)]
+      Ouc a phi u a0 -> apps (con "outS") [(Im, a), (Im, phi), (Im, u), (Ex, a0)]
+
+      GlueTy a phi t e -> apps (con "primGlue") [(Ex, a), (Ex, phi), (Ex, t), (Ex, e)]
+      Glue _a _phi _ty _e t im -> apps (con "glue") [(Ex, t), (Ex, im)]
+      Unglue _a _phi _ty _e t -> apps (con "unglue") [(Im, _a), (Im, _phi), (Im, _ty), (Im, _e), (Ex, t)]
+
+      Comp a phi u a0 -> apps (con "comp") [(Ex, a), (Im, phi), (Ex, u), (Ex, a0)]
+      HComp a phi u a0 -> apps (con "hcomp") [(Im, a), (Im, phi), (Ex, u), (Ex, a0)]
+
+      Case _ t cs ->
+        let
+          oneCase (c, 0, l) = go False 0 c <+> operator (pretty "=>") <+> go False 0 l
+          oneCase (c, i, l) =
+            let (args, bd) = getLams i l
+             in go False 0 c <+> hsep (map pretty args) <+> operator (pretty "=>") <+> go False 0 bd
+
+          getLams 0 x = ([], x)
+          getLams n (Lam _ v t) = let (as, b) = getLams (n - 1) t in (v:as, b)
+          getLams _ x = ([], x)
+        in
+          parenIf (p >= fun_prec) $
+            keyword (pretty "case") <+> go False 0 t <+> keyword (pretty "of")
+                <> line
+                <> indent 2 (vsep (map oneCase cs))
+
+      EqS _ x y -> parenIf (p >= arg_prec) $
+        go False 0 x <+> operator (pretty "≡S") <+> go False 0 y
+
+      Syntax.Refl _ _ -> keyword (pretty "refl")
+      Syntax.AxK _ _ bigp pr eq   -> apps (con "K_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
+      Syntax.AxJ _ _ bigp pr _ eq -> apps (con "J_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
+    where
+      sp | t         = softline
+         | otherwise = space
+
+      parenIf p x | p = parens x
+                  | otherwise = x
+
+      braceIf p x | p = braces x
+                  | otherwise = x
+
+      con x = Con (Bound (T.pack x) 0)
+
+      plic = \case
+        Ex -> parens
+        Im -> braces
+
+      arrow = operator (pretty "->")
+
+      instead = go t p
+      apps :: Term -> [(Plicity, Term)] -> Doc AnsiStyle
+      apps f xs = instead (foldl (\f (p, x) -> App p f x) f xs)
+
+prettyBinds :: Bool -> [(Name, Term, Term)] -> Doc AnsiStyle
+prettyBinds _ [] = mempty
+prettyBinds imp ((x, ty, tm):bs) =
+     pretty x <+> colon <+> align (prettyTm' imp ty)
+  <> line
+  <> pretty x <+> equals <+> align (prettyTm' imp tm)
+  <> line
+  <> prettyBinds imp bs
 
-  prettyTm (Pi Ex (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
-  prettyTm (Pi Im v d r)                 = group (braces (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
-  prettyTm (Pi Ex v d r)                 = group (parens (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
+showFace :: Bool -> Map Head Bool -> Doc AnsiStyle
+showFace imp = hsep . map go . Map.toList where
+  go (h, b) = parens $ prettyTm' imp (quoteWith False mempty (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
 
-  prettyTm (Sigma (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
-  prettyTm (Sigma v d r)                 = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
+prettyVl' :: Bool -> Value -> Doc AnsiStyle
+prettyVl' b = prettyTm' b . quoteWith True mempty
 
-  prettyTm (IAnd x y) = parens $ prettyTm x <+> operator (pretty "&&") <+> prettyTm y
-  prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
-  prettyTm (INot x) = operator (pretty '~') <> prettyTm x
+instance Pretty Term where
+  pretty = unAnnotate . prettyTm
 
-  prettyTm (System (Map.null -> True)) = braces mempty
-
-  prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where
-    go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
-
-  prettyTm (Case _ x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line)
-  prettyTm (Let xs e) = align $ keyword (pretty "let") <+> braces (line <> indent 2 (prettyLet xs) <> line) <+> keyword (pretty "in") <+> prettyTm e
-
-  prettyTm x = error (show x)
-
-  prettyCase = vcat . map go where
-    go (x, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs
-
-  prettyLet = vcat . map go where
-    go (x, t, y) = pretty x <+> align (colon <+> nest (- 1) (prettyTm t)) <> line <> pretty x <+> pretty "=" <+> prettyTm y
-
-  beautify (PathP l x y)       = toFun "PathP" [l, x, y]
-  beautify (IElim _ _ _ f i)   = App Ex f i
-  beautify (PathIntro _ _ _ f) = f
-
-  beautify (App _ (Lam _ v b) _)
-    | v `Set.notMember` freeVars b = beautify b
-
-  beautify (IsOne phi)  = toFun "IsOne" [phi]
-  beautify ItIsOne      = Ref (Bound (T.pack ".1=1") 0)
+prettyTm :: Term -> Doc AnsiStyle
+prettyTm = prettyTm' printImplicits
 
-  beautify (Lam Ex v (App Ex f (Ref v')))
-    | v == v', v `Set.notMember` freeVars f = f
+instance Pretty Value where
+  pretty = unAnnotate . prettyVl
 
-  beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0]
-  beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty
+prettyVl :: Value -> Doc AnsiStyle
+prettyVl = prettyVl' printImplicits
 
-  beautify (Partial phi a)   = toFun "Partial" [phi, a]
-  beautify (PartialP phi a)  = toFun "PartialP" [phi, a]
-  beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0]
-  beautify (HComp a phi u a0) = toFun "hcomp" [a, phi, u, a0]
-  beautify (Sub a phi u)     = toFun "Sub" [a, phi, u]
-  beautify (Inc _ _ u)       = toFun "inS" [u]
-  beautify (Ouc a phi u u0)  = toFun "outS" [a, phi, u, u0]
+printImplicits :: Bool
+#if defined(RELEASE)
+printImplicits = False
+#else
+printImplicits = True
+#endif
 
-  beautify (GlueTy a I1 _ _)    = a
-  beautify (GlueTy a b c d)     = toFun "Glue"   [a,b,c,d]
-  beautify (Glue a b c d e f)   = toFun "glue"   [a,b,c,d,e,f]
-  beautify (Unglue a b c d e)   = toFun "unglue" [a,b,c,d,e]
-  beautify x = x
+render :: Doc AnsiStyle -> Lazy.Text
+render = renderLazy . layoutSmart defaultLayoutOptions
 
-  toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a
+arg_prec, fun_prec, dom_prec, and_prec, or_prec :: Int
+dom_prec = succ fun_prec
+arg_prec = succ and_prec
+and_prec = succ or_prec
+or_prec  = succ fun_prec
+fun_prec = 1
 
 keyword :: Doc AnsiStyle -> Doc AnsiStyle
 keyword = annotate (color Magenta)
 
 operator :: Doc AnsiStyle -> Doc AnsiStyle
 operator = annotate (color Yellow)
-
-parenArg :: Term -> Doc AnsiStyle
-parenArg x@App{} = parens (prettyTm x)
-parenArg x@IElim{} = parens (prettyTm x)
-parenArg x@IsOne{} = parens $ prettyTm x
-parenArg x@Partial{} = parens $ prettyTm x
-parenArg x@PartialP{} = parens $ prettyTm x
-
-parenArg x@Sub{} = parens $ prettyTm x
-parenArg x@Inc{} = parens $ prettyTm x
-parenArg x@Ouc{} = parens $ prettyTm x
-
-parenArg x@Comp{} = parens $ prettyTm x
-parenArg x@Case{} = parens $ prettyTm x
-
-parenArg x = prettyDom x
-
-prettyDom :: Term -> Doc AnsiStyle
-prettyDom x@Pi{}    = parens (prettyTm x)
-prettyDom x@Sigma{} = parens (prettyTm x)
-prettyDom x         = parenFun x
-
-parenFun :: Term -> Doc AnsiStyle
-parenFun x@Lam{} = parens $ prettyTm x
-parenFun x@PathIntro{} = parens $ prettyTm x
-parenFun x = prettyTm x
-
-render :: Doc AnsiStyle -> Text
-render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
-
-showValue :: Value -> String
-showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm . quote
-
-showFace :: Map Head Bool -> Doc AnsiStyle
-showFace = hsep . map go . Map.toList where
-  go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
-
-freeVars :: Term -> Set Name
-freeVars (Ref v) = Set.singleton v
-freeVars (App _ f x) = Set.union (freeVars f) (freeVars x)
-freeVars (Pi _ n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
-freeVars (Lam _ n x) = n `Set.delete` freeVars x
-freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where
-  bound = Set.fromList (map (\(x, _, _) -> x) ns)
-  freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns
-freeVars Meta{} = mempty
-freeVars Con{} = mempty
-freeVars PCon{} = mempty
-freeVars Data{} = mempty
-freeVars Type{} = mempty
-freeVars Typeω{} = mempty
-freeVars I{} = mempty
-freeVars I0{} = mempty
-freeVars I1{} = mempty
-freeVars (Sigma n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
-freeVars (Pair x y) = Set.unions $ map freeVars [x, y]
-freeVars (Proj1 x) = Set.unions $ map freeVars [x]
-freeVars (Proj2 x) = Set.unions $ map freeVars [x]
-freeVars (IAnd x y) = Set.unions $ map freeVars [x, y]
-freeVars (IOr x y) = Set.unions $ map freeVars [x, y]
-freeVars (INot x) = Set.unions $ map freeVars [x]
-freeVars (PathP x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (IElim x y z a b) = Set.unions $ map freeVars [x, y, z, a, b]
-freeVars (PathIntro x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (IsOne a) = Set.unions $ map freeVars [a]
-freeVars ItIsOne{} = mempty
-freeVars (Partial x y) = Set.unions $ map freeVars [x, y]
-freeVars (PartialP x y) = Set.unions $ map freeVars [x, y]
-freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty (Map.toList fs)
-
-freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z]
-freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a]
-
-freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (HComp x y z a) = Set.unions $ map freeVars [x, y, z, a]
-
-freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a]
-freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c]
-freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c]
-freeVars (Case rng x y) = freeVars rng <> freeVars x <> foldMap (freeVars . snd) y

stack.yaml

@@ -1,67 +1,5 @@
-# This file was automatically generated by 'stack init'
-#
-# Some commonly used options have been documented as comments in this file.
-# For advanced use and comprehensive documentation of the format, please see:
-# https://docs.haskellstack.org/en/stable/yaml_configuration/
-
-# Resolver to choose a 'specific' stackage snapshot or a compiler version.
-# A snapshot resolver dictates the compiler version and the set of packages
-# to be used for project dependencies. For example:
-#
-# resolver: lts-3.5
-# resolver: nightly-2015-09-21
-# resolver: ghc-7.10.2
-#
-# The location of a snapshot can be provided as a file or url. Stack assumes
-# a snapshot provided as a file might change, whereas a url resource does not.
-#
-# resolver: ./custom-snapshot.yaml
-# resolver: https://example.com/snapshots/2018-01-01.yaml
 resolver:
-  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
 
-# User packages to be built.
-# Various formats can be used as shown in the example below.
-#
-# packages:
-# - some-directory
-# - https://example.com/foo/bar/baz-0.0.2.tar.gz
-#   subdirs:
-#   - auto-update
-#   - wai
 packages:
-- .
-# Dependency packages to be pulled from upstream that are not in the resolver.
-# These entries can reference officially published versions as well as
-# forks / in-progress versions pinned to a git hash. For example:
-#
-# extra-deps:
-# - acme-missiles-0.3
-# - git: https://github.com/commercialhaskell/stack.git
-#   commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
-#
-# extra-deps: []
-
-# Override default flag values for local packages and extra-deps
-# flags: {}
-
-# Extra package databases containing global packages
-# extra-package-dbs: []
-
-# Control whether we use the GHC we find on the path
-# system-ghc: true
-#
-# Require a specific version of stack, using version ranges
-# require-stack-version: -any # Default
-# require-stack-version: ">=2.5"
-#
-# Override the architecture used by stack, especially useful on Windows
-# arch: i386
-# arch: x86_64
-#
-# Extra directories used by stack for building
-# extra-include-dirs: [/path/to/dir]
-# extra-lib-dirs: [/path/to/dir]
-#
-# Allow a newer minor version of GHC than the snapshot specifies
-# compiler-check: newer-minor
+- .

stack.yaml.lock

@@ -6,8 +6,8 @@
 packages: []
 snapshots:
 - completed:
-    size: 563098
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
-    sha256: 395775c03e66a4286f134d50346b0b6f1432131cf542886252984b4cfa5fef69
+    size: 565720
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
+    sha256: 76bf8992ff8dfe6eda9c02f81866138c2369344d5011ab39ae403457c4448b03
   original:
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml