cubical.cabal

@@ -46,9 +46,8 @@ 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 -rtsopts
+  ghc-options:         -Wall -Wextra -Wno-name-shadowing
+

src/Debug.hs

@@ -1,45 +0,0 @@
-{-# 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,7 +4,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE EmptyCase #-}
 module Elab where
 
 import Control.Arrow (Arrow(first))
@@ -15,7 +14,6 @@ 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)
@@ -33,6 +31,7 @@ import Prettyprinter
 
 import Syntax.Pretty
 import Syntax
+import Data.Maybe (fromMaybe)
 
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
@@ -55,10 +54,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 (VEqStrict VI phi VI1)
+      x <- check x (VIsOne phi)
       pure (App P.Ex (w f) x, a)
     It'sPartialP phi a w -> do
-      x <- check x (VEqStrict VI phi VI1)
+      x <- check x (VIsOne phi)
       x_nf <- eval x
       pure (App P.Ex (w f) x, a @@ x_nf)
 
@@ -102,17 +101,20 @@ check (P.Lam p v b) ty = do
 
       tm_nf <- eval tm
 
-      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)
+      unify (tm_nf @@ VI0) le
+        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
+
+      unify (tm_nf @@ VI1) ri
+        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
 
       pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
     It'sPartial phi a wp ->
-      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
+      assume (Bound v 0) (VIsOne phi) $ \var ->
         wp . Lam p var <$> check b a
 
     It'sPartialP phi a wp ->
-      assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
+      assume (Bound v 0) (VIsOne phi) $ \var ->
         wp . Lam p var <$> check b (a @@ VVar var)
 
 check (P.Pair a b) ty = do
@@ -145,36 +147,54 @@ check (P.Let items body) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
-  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)))
+  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)
     pure (n, (phi, head rhses))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
 
-  for_ eqns \(n, (formula, rhs)) -> do
-    for_ eqns $ \(n', (formula', rhs')) -> do
+  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
       let
+        k = case binding of
+          Just v -> assume v (VIsOne formula) . const
+          Nothing -> id
         truth = possible mempty (iand formula formula')
-
-      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'
+        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'
         unify vl vl'
           `withNote` vsep [ pretty "These two cases must agree because they are both possible:"
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> pretty vl
-                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> pretty (zonk vl')
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm rhs
+                          , indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> prettyTm rhs'
                           ]
-          `withNote` (pretty "Consider this face, where both are true:" <+> showFace False (snd truth))
+          `withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
 
   name <- newName
-  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
+  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))))
 
 check (P.LamCase pats) ty =
   do
@@ -212,14 +232,12 @@ check (P.LamCase pats) ty =
                   let rhs = cases @@ side
                   for_ (truthAssignments formula mempty) $ \i -> do
                     let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary)
-                        lookup n = fromMaybe (VVar n) (snd <$> (Map.lookup n i))
+                        lookup n = fromMaybe VI0 (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 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk side)
-                                      , pretty "which is mapped to"
-                                      , indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk rhs)
+                                      , indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
                                       ]
+                      `withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
               _ -> pure ()
 
             pure (pat, n_lams, wp rhs)
@@ -246,10 +264,6 @@ 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
@@ -316,11 +330,7 @@ skipLams k = do
   (Lam P.Im n . ) <$> skipLams (k - 1)
 
 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 _   [] cont = cont []
 checkLetItems map (P.LetDecl v t:xs) cont = do
   t <- check t VTypeω
   t_nf <- eval t
@@ -343,27 +353,21 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do
         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.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
 checkFormula (P.FIs0 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (inot (VVar nm), Set.singleton nm)
+  pure (inot (VVar nm))
 checkFormula (P.FIs1 x) = do
   nm <- getNameFor x
   ty <- getNfType nm
   unify ty VI
-  pure (VVar nm, Set.singleton nm)
+  pure (VVar nm)
 
 isSort :: NFType -> ElabM ()
 isSort t = isSort (force t) where
@@ -425,15 +429,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 -> Value)
+isPartialType :: NFType -> ElabM (NFEndp, Value)
 isPartialType t = isPartialType (force t) where
-  isPartialType (VPartial phi a) = pure (phi, const a)
-  isPartialType (VPartialP phi a) = pure (phi, (a @@))
+  isPartialType (VPartial phi a) = pure (phi, a)
+  isPartialType (VPartialP phi a) = pure (phi, a)
   isPartialType t = do
     phi <- newMeta VI
     dom <- newMeta (VPartial phi VType)
-    unify t (VPartialP phi dom)
-    pure (phi, (dom @@))
+    unify t (VPartial 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
@@ -492,21 +496,21 @@ checkStatement (P.ReplNf e) k = do
   (e, _) <- infer e
   e_nf <- eval e
   h <- asks commHook
-  liftIO $ h . prettyVl =<< zonkIO e_nf
+  liftIO (h e_nf)
   k
 
 checkStatement (P.ReplTy e) k = do
-  (t, ty) <- infer e
+  (_, ty) <- infer e
   h <- asks commHook
-  liftIO (h (prettyTm t <+> colon <+> align (prettyVl (zonk ty))))
+  liftIO (h ty)
   k
 
 checkStatement (P.Data name tele retk constrs) k =
   do
-    checkTeleRetk tele retk \retk kind tele undef -> do
+    checkTeleRetk True tele retk \kind tele undef -> do
       kind_nf <- eval kind
-      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)
+      defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
+        checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
   where
     makeProj (x, p, _) = PApp p (VVar x)
 
@@ -516,22 +520,26 @@ checkStatement (P.Data name tele retk constrs) k =
       | any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
       | otherwise = HData False name
 
-    checkTeleRetk [] retk cont = do
+    checkTeleRetk allKan [] retk cont = do
       t <- check retk VTypeω
-      r <- eval t
-      cont r t [] id
-
-    checkTeleRetk ((x, p, t):xs) retk cont = do
+      t_nf <- eval t
+      when allKan $ unify t_nf VType
+      cont t [] id
+    checkTeleRetk allKan ((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 xs retk \ret k xs w -> cont ret (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
+      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)
 
-    checkCons _ _ _et [] k = k
+    checkCons _ _et [] k = k
 
-    checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
-      t <- check ty retk
+    checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
+      t <- check ty VTypeω
       ty_nf <- eval t
       let
         (args, ret') = splitPi ty_nf
@@ -539,12 +547,11 @@ 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 retk n ret xs k
+      defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
 
-    checkCons retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
-      fibrant retk
+    checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
       (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
-        t <- check return retk
+        t <- check return VTypeω
         ty_nf <- eval t
         let
           (args, ret') = splitPi ty_nf
@@ -561,17 +568,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 (foldl ior VI0 (map fst faces)) (totalProp indices)
+        unify (foldr 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 retk n ret xs k
+      defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
 
     close []             t = t
     close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@@ -588,13 +595,9 @@ 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 (VVar x) (inot (VVar x) `ior` totalProp xs)
+    totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
     totalProp [] = VI0
 
-    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
@@ -603,7 +606,7 @@ checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
 newtype Redefinition = Redefinition { getRedefName :: Name }
   deriving (Show, Typeable, Exception)
 
-data WhenCheckingEndpoint = WhenCheckingEndpoint { direction :: Name, leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
+data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
   deriving (Show, Typeable, Exception)
 
 data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
@@ -613,10 +616,3 @@ 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

@@ -23,25 +23,26 @@ import Data.Foldable
 import Data.IORef
 import Data.Maybe
 
-import {>n class="err">-# SOURCE #-} Elab.Eval.Formula
+import Elab.Eval.Formula
 import Elab.Monad
 
 import GHC.Stack
 
 import Presyntax.Presyntax (Plicity(..))
 
+import Prettyprinter
+
 import Syntax.Pretty
 import Syntax
 
-import System.IO.Unsafe ( unsafePerformIO )
+import System.IO.Unsafe
 
 import {-# SOURCE #-} Elab.WiredIn
-import Debug (traceM, traceDocM)
-import Prettyprinter (pretty, (<+>))
 
 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
@@ -63,6 +64,7 @@ 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ω
 
@@ -74,30 +76,30 @@ 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) = 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 (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 (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) = 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
+zonkIO (VCase env t x xs) = do
+  env' <- emptyEnv
+  evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs
 
 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
 
@@ -120,22 +122,23 @@ 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 (idkT, a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (error "type of abs", 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 (idkT, a) (getEnv env))} t
+    eval' env { getEnv = (Map.insert s (error "type of abs", 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 (idkT, a) (getEnv env) } t
+    eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
 
 eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
 
@@ -156,12 +159,15 @@ 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) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
+eval' e (System fs) = VSystem (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)   = incS (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 (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)
@@ -180,122 +186,75 @@ eval' e (Let ns x) =
 
 eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs
 
-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 _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
 
 evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
 
-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)))
+evalCase env rng (VHComp a phi u a0) cases =
+  comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases)
+         (VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases))
   where
-    v = Elab.WiredIn.fill (fun (const a)) φ u u0
-    α x = evalCase env rng x cases
+    v = Elab.WiredIn.fill (fun (const a)) phi u a0
 
 evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc
 
-evalCase env rng (force -> val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs)
+evalCase env rng (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 (force -> val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
+evalCase env rng (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' :: ElabEnv -> Name -> NFType -> Term -> Value
+evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
 
-evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value
+evalFix :: Name -> NFType -> Term -> ElabM Value
 evalFix name nft term = do
   t <- ask
-  pure (evalFix' t name (GluedVl (HVar name) mempty nft) term)
+  pure (evalFix' t name nft term)
 
 data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
-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
+unify' :: HasCallStack => Value -> Value -> ElabM ()
+unify' 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 topa@(VNe (HPCon _ _ x) sp) topb@(VNe (HPCon _ _ y) sp')
-    | x == y = traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip sp sp')
+  go (VNe (HPCon s _ _) _) rhs
+    | VSystem _ <- s = go (force s) rhs
 
-  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 lhs (VNe (HPCon s _ _) _)
+    | VSystem _ <- s = go lhs (force s)
 
-  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 (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')
+  go (VNe x a) (VNe x' a')
     | x == x', length a == length a' =
-      traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip a a')
+      traverse_ (uncurry unify'Spine) (Seq.zip a a')
 
   go (VLam p (Closure n k)) vl = do
     t <- VVar <$> newName' n
-    unify' canSwitch (k t) (vApp p vl t)
+    unify' (k t) (vApp p vl t)
 
   go vl (VLam p (Closure n k)) = do
     t <- VVar <$> newName' n
-    unify' canSwitch (vApp p vl t) (k t)
+    unify' (vApp p vl t) (k t)
 
-  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 (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 (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 (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 (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 (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
+    t <- VVar <$> newName
+    unify' d d'
+    unify' (k t) (k' t)
 
   go VType VType   = pure ()
   go VTypeω VTypeω = pure ()
@@ -303,63 +262,56 @@ unify' canSwitch topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go VI VI   = pure ()
 
   go (VPath l x y) (VPath l' x' y') = do
-    unify' canSwitch l l'
-    unify' canSwitch x x'
-    unify' canSwitch y y'
+    unify' l l'
+    unify' x x'
+    unify' y y'
 
   go (VLine l x y p) p' = do
-    n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
-    unify' canSwitch (p @@ n) (ielim l x y p' n)
+    n <- VVar <$> newName
+    unify' (p @@ n) (ielim l x y p' n)
 
   go p' (VLine l x y p) = do
     n <- VVar <$> newName
-    unify' canSwitch (ielim l x y p' n) (p @@ n)
+    unify' (ielim l x y p' n) (p @@ n)
 
-  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 (VIsOne x) (VIsOne y) = unify' x y
 
-  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')]
+  -- IsOne is proof-irrelevant:
+  go VItIsOne _ = pure ()
+  go _ VItIsOne = pure ()
 
-  go (VComp a phi u a0) (VComp a' phi' u' a0') =
-    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+  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 (VHComp a phi u a0) (VHComp a' phi' u' a0') =
-    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+  go (VComp a phi u a0) (VComp a' phi' u' a0') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
 
-  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 _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs
+  go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne)
 
   go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') =
-    traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+    traverse_ (uncurry unify') [(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' 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 ()
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
 
-  go (VINot x) (VINot y) = unify' canSwitch x y
+  go (VSystem sys) rhs = goSystem unify' sys rhs
+  go rhs (VSystem sys) = goSystem (flip unify') sys rhs
 
-  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 (VCase _ _ a b) (VCase _ _ a' b') = do
+    unify' a a'
+    let go (_, _, a) (_, _, b) = join $ unify' <$> eval a <*> eval b
+    zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
 
-  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
+  go x y
+    | x == y = pure ()
+    | otherwise =
+      case (toDnf x, toDnf y) of
+        (Just xs, Just ys) -> unify'Formula xs ys
+        _ -> fail
 
   goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM ()
   goSystem k sys rhs = do
@@ -367,58 +319,29 @@ unify' canSwitch 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 -> do
+      for (truthAssignments f (getEnv env)) $ \e ->
         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
-
-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
 
-trivialSystem :: Value -> Maybe Value
-trivialSystem = go . force where
-  go VSystem{} = Nothing
-  go x = Just x
+  unify'Spine (PApp a v) (PApp a' v')
+    | a == a' = unify' v v'
 
-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 PProj1 PProj1 = pure ()
+  unify'Spine PProj2 PProj2 = pure ()
 
-unify'Spine _ _ _ PProj1 PProj1 = pure ()
-unify'Spine _ _ _ PProj2 PProj2 = pure ()
+  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 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 _ _ = fail
 
-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'Formula x y
+    | compareDNFs x y = pure ()
+    | otherwise = fail
 
 unify :: HasCallStack => Value -> Value -> ElabM ()
-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)
+unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
 
 isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
 isConvertibleTo a b = isConvertibleTo (force a) (force b) where
@@ -436,42 +359,26 @@ 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' True a b
+    unify' a b
     pure id
 
-newMeta' :: Bool -> Value -> ElabM Value
-newMeta' int dom = do
+newMeta :: Value -> ElabM Value
+newMeta dom = do
   loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan
   n <- newName
   c <- liftIO $ newIORef Nothing
-  let m = MV (getNameText n) c dom (flatten <$> loc) int
+  let m = MV (getNameText n) c dom (flatten <$> loc)
       flatten (x, (y, z)) = (x, y, z)
 
   env <- asks getEnv
 
-  t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $
+  t <- for (Map.toList env) $ \(n, _) -> pure $
     case n of
-      Bound{} -> Just (PApp Ex (VVar n), n, t)
+      Bound{} -> Just (PApp Ex (VVar n))
       _ -> Nothing
 
-  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
+  pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
 
 newName :: MonadIO m => m Name
 newName = liftIO $ do
@@ -488,103 +395,91 @@ _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
-      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 =
+      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
       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 :: MV -> Set Name -> Value -> ElabM ()
-checkScope mv scope (VNe h sp) =
+checkScope :: Set Name -> Value -> ElabM ()
+checkScope scope (VNe h sp) =
   do
     case h of
       HVar v@Bound{} ->
         unless (v `Set.member` scope) . throwElab $
-          ScopeCheckingFail v
+          NotInScope v
       HVar{} -> pure ()
       HCon{} -> pure ()
       HPCon{} -> pure ()
-      HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv
+      HMeta{} -> pure ()
       HData{} -> pure ()
     traverse_ checkProj sp
   where
-    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 (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 PProj1 = pure ()
     checkProj PProj2 = pure ()
 
-checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl
+checkScope scope (GluedVl _ _p vl) = checkScope scope vl
 
-checkScope mv scope (VLam _ (Closure n k)) =
-  checkScope mv (Set.insert n scope) (k (VVar n))
+checkScope scope (VLam _ (Closure n k)) =
+  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 (VPi _ 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 scope (VSigma d (Closure n k)) = do
+  checkScope scope d
+  checkScope (Set.insert n scope) (k (VVar n))
 
-checkScope mv s (VPair a b) = traverse_ (checkScope mv s) [a, b]
+checkScope s (VPair a b) = traverse_ (checkScope 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 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 (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 (VPath line a b) = traverse_ (checkScope mv s) [line, a, b]
-checkScope mv s (VLine _ _ _ line)   = checkScope mv s line
+checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
+checkScope s (VLine _ _ _ line)   = checkScope s line
 
-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 (VIsOne x) = checkScope s x
+checkScope _ VItIsOne   = pure ()
 
-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 (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 (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 (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 (VCase _ _ v _) = checkScope mv s v
+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 (VEqStrict a x y) = traverse_ (checkScope mv s) [a, x, y]
-checkScope mv s (VReflStrict a x) = traverse_ (checkScope mv s) [a, x]
+checkScope s (VCase _ _ v _) = checkScope s v
 
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@@ -593,10 +488,10 @@ checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
 checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
-data MetaException = NonLinearSpine { getDupeName :: Name }
-                   | SpineProj { getSpineProjection :: Projection } 
-                   | CircularSolution { getCycle :: MV }
-                   | ScopeCheckingFail { outOfScope :: Name }
+newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
+  deriving (Show, Typeable, Exception)
+
+newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
   deriving (Show, Typeable, Exception)
 
 substituteIO :: Map.Map Name Value -> Value -> IO Value
@@ -604,10 +499,15 @@ 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 $ foldl applProj (VNe hd mempty) sp'
+          Nothing -> pure $ VNe hd sp'
       hd -> pure $ VNe hd sp'
 
   substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl
@@ -620,6 +520,7 @@ 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ω
 
@@ -631,13 +532,16 @@ 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) = incS <$> substituteIO a <*> substituteIO b <*> substituteIO c
+  substituteIO (VInc a b c) = VInc <$> 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
 
@@ -645,8 +549,6 @@ 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
@@ -654,23 +556,16 @@ 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.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
+  let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in
+  case Map.lookup VI1 map' of
     Just x -> x
-    Nothing -> VSystem map'
+    Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map')
 
 forceIO :: MonadIO m => Value -> m Value
 forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do
@@ -684,7 +579,6 @@ 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
   r <- forceIO rng
@@ -694,25 +588,24 @@ forceIO x = pure x
 force :: Value -> Value
 force = unsafePerformIO . forceIO
 
-applProj :: HasCallStack => Value -> Projection -> Value
+applProj :: Value -> Projection -> Value
 applProj fun (PApp p arg)     = vApp p fun arg
 applProj fun (PIElim l x y i) = ielim l x y fun i
 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
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
-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 (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 p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
-vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
+vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
+vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
 vApp p (VCase env rng sc branches) arg =
   VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
     (map (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
@@ -724,17 +617,24 @@ 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) = incS a b (vProj1 c)
+vProj1 (VInc (VSigma a _) b c) = VInc 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
+vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote 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) = incS (r (vProj1 c)) b (vProj2 c)
+vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (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))
+
+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 = x

src/Elab/Eval/Formula.hs

@@ -2,38 +2,22 @@ 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 = 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
+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
 
 compareDNFs :: Value -> Value -> Bool
 compareDNFs (VIOr x y) (VIOr x' y') =
@@ -76,14 +60,10 @@ 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) (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 (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 _ 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

@@ -1,18 +0,0 @@
-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,19 +26,17 @@ data ElabEnv =
 
           , nameMap     :: Map Text Name
           , pingPong    :: {-# UNPACK #-} !Int
-          , commHook    :: Doc AnsiStyle -> IO ()
+          , commHook    :: Value -> 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 }
@@ -46,24 +44,7 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
     via ReaderT ElabEnv IO
 
 emptyEnv :: IO ElabEnv
-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 = []
-                 }
+emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty mempty <$> newIORef mempty
 
 addBoundary :: Name -> Boundary -> ElabM a -> ElabM a
 addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} )
@@ -137,13 +118,10 @@ switch :: ElabM a -> ElabM a
 switch k =
   do
     depth <- asks pingPong
-    when (depth >= 128) $ error "stack overflow"
+    when (depth >= 128) $ throwElab StackOverflow
     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,37 +4,9 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ViewPatterns #-}
-{-# 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
+module Elab.WiredIn where
 
-import Control.Exception ( assert, Exception )
+import Control.Exception
 
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
@@ -43,19 +15,16 @@ 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, prettyVl)
+import Syntax.Pretty (prettyTm)
 import Syntax
 
-import System.IO.Unsafe ( unsafePerformIO )
+import System.IO.Unsafe
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -70,28 +39,25 @@ 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) ~> VSub (a @@ VI1) phi (u @@ VI1)
-
+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 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ω
@@ -100,35 +66,25 @@ wiValue WiInterval = VI
 wiValue WiI0       = VI0
 wiValue WiI1       = VI1
 
-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 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 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 WiIsOne   = fun VIsOne
+wiValue WiItIsOne = VItIsOne
 
-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 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 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 ~>
@@ -140,11 +96,6 @@ 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)
 
@@ -166,6 +117,7 @@ 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)
@@ -178,9 +130,11 @@ wiredInNames = Map.fromList
   , ("inot", WiINot)
   , ("PathP", WiPathP)
 
+  , ("IsOne", WiIsOne)
+  , ("itIs1", WiItIsOne)
+
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
-  , ("partialExt", WiPOr)
   , ("Sub", WiSub)
   , ("inS", WiInS)
   , ("outS", WiOutS)
@@ -189,19 +143,14 @@ 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
@@ -250,30 +199,24 @@ 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 (projIntoCase (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
-
+        VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
-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 :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
+outS _ (force -> VI1) u _  = u @@ VItIsOne
 
 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) = mkVSystem (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) = VSystem (fmap (outS a phi u) fs)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
-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) =
+-- 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 name) of
     VPi{} ->
       let
@@ -281,21 +224,21 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
         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) (incS (dom VI0) phi y) i
+        y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (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))
-                   (incS (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
-
+                   (VInc (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)) (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))
+        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))
        in
          VPair (w VI1) c2
 
@@ -311,7 +254,7 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> 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)]))
-            (incS (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
+            (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
 
     VGlueTy _ thePhi theTypes theEquivs ->
       let
@@ -322,20 +265,20 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
       let
         base i   = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
         phi i    = substitute (Map.singleton name i) thePhi
-        types i  = substitute (Map.singleton name i) theTypes @@ VReflStrict VI VI1
+        types i  = substitute (Map.singleton name i) theTypes @@ VItIsOne
         equivs i = substitute (Map.singleton name i) theEquivs
 
-        a i u = unglue (base i) (phi i) (types i) (equivs i) (b @@ i @@ u)
+        a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
         a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
 
         del = faceForall phi
-        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)
+        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)
 
         (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 @@ VReflStrict VI VI1) (del `ior` psi) (fun ts) (fun ps) a1'
+        (t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (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)
@@ -344,38 +287,37 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> 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)))
-              (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)
+          (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
        in b1
 
     VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
-                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))
+                            (fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
 
     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 makeSetFiller (length args) (a @@) con_type con_args phi u
-        _ -> VComp a phi u (incS (a @@ VI0) phi a0)
+          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 (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
+    VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
+    sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
 
-    _ -> VComp a phi u (incS (a @@ VI0) phi a0)
+    _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
   where
     {-# NOINLINE name #-}
-    name :: Name
     name = unsafePerformIO newName
 
     {-# NOINLINE equivVar #-}
-    equivVar :: Name
     equivVar = unsafePerformIO newName
 
-
 mapVSystem :: (Value -> Value) -> Value -> Value
 mapVSystem f (VSystem fs) = VSystem (fmap f fs)
 mapVSystem f x = f x
@@ -386,63 +328,60 @@ forceAndGlue v =
     v@VGlueTy{} -> v
     y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))
 
-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
+compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
+compHIT 0 a phi u a0 =
+  case phi of
+    VI1 -> u @@ VI1 @@ VItIsOne
+    VI0 -> compOutS (a VI0) phi u a0
+    _ -> VHComp (a VI0) phi u a0
+compHIT _ a phi u a0 = error $ unlines
+  [ "*** TODO: composition for HIT: "
+  , "domain = " ++ show (prettyTm (quote (zonk (fun a))))
+  , "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
   go _ _ Seq.Empty _ _ = Seq.Empty
   go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| 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
+    | nargs > 0 = assert (p == p') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
     | otherwise = assert (p == p') $
-      let fill = makeFiller typeArgument nargs dom phi u y
+      let fill = makeFiller 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))
+
+  makeFiller nth (VNe (HData _ n') args) phi u a0
+    | n' == typeArgument =
+      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"
+
   smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
 
   typeArgument = unsafePerformIO newName
   {-# NOINLINE typeArgument #-}
 
-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))
+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
 
 system :: (Value -> Value -> Value) -> Value
-system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "[i]" 0) \isone -> k i isone
+system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone
 
-fill :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
+fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
 fill a phi u a0 j =
   comp (line \i -> a @@ (i `iand` j))
        (phi `ior` inot j)
@@ -450,23 +389,23 @@ fill a phi u a0 j =
                                                    , (inot j, outS a phi (u @@ VI0) a0)]))
        a0
 
-hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
-hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
+hComp :: NFSort -> NFEndp -> Value -> Value -> Value
+hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
 hComp a phi u a0 = VHComp a phi u a0
 
-glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
 glueType a phi tys eqvs = VGlueTy a phi tys eqvs
 
-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 :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
 glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t 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   :: 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 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
@@ -488,28 +427,27 @@ 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)) y (f @@ x)
+fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
 
 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 = 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 ]
+equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
 
 pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
-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
+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
   pathT = VPath (fun (const (tyA VI1))) c1 c2
-  c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (incS (tyA VI0) phi (f VI0 @@ t0))
+  c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (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)) (incS (tyA VI0) phi a0)
+  path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
 
 opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
-opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
+opEquiv aT tT f phi t p a = (VInc 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))
@@ -517,76 +455,33 @@ opEquiv aT tT f phi t p a = (incS 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))
-       (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))
+    phi
+    (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
+    (VInc a phi (vProj1 aC))
 
 transp :: (NFEndp -> Value) -> Value -> Value
-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)
+transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
 
 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)
+makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
   where
-    line = fun \i -> line' (inot i)
+    line = fun \i -> substitute (Map.singleton var (inot i)) vne
     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) (incS a VI0 x) i
-    v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (incS a VI1 x) (inot i)
+    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)
 
     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))])) (incS 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))])) (VInc 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)]))
-           (incS b (ior j (inot j)) (ielim b y (f @@ x) beta y))
+           (VInc 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))))
@@ -594,7 +489,7 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
                                                                            , (k, theta1 x beta y i j)
                                                                            , (inot j, v i @@ y)
                                                                            , (j, u i @@ omega x beta y k)]))
-                                   (incS a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k)))
+                                   (VInc 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)
 
@@ -607,27 +502,4 @@ idEquiv a = VPair idfun idisequiv where
       VLine (fun (const a)) y (vProj1 u) $ fun \j ->
         ielim (fun (const a)) y y (vProj2 u) (iand i j)
 
-  id_fiber y = VPair y (VLine a y y (fun (const y)))
-
-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
+  id_fiber y = VPair y (VLine a y y (fun (const y)))

src/Elab/WiredIn.hs-boot

@@ -1,9 +1,8 @@
-{-# 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
+module Elab.WiredIn where
+
+import GHC.Stack.Types
 
 import Syntax
-import Debug (DebugCallStack)
 
 wiType  :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
@@ -12,20 +11,14 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp
 inot      :: NFEndp -> NFEndp
 ielim     :: NFSort -> Value -> Value -> Value -> NFEndp -> 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
+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
 
-glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
-glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
-unglue   :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
+glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
+glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
+unglue   :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
 
 fun :: (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)
+system :: (Value -> Value -> Value) -> Value

src/Main.hs

@@ -3,7 +3,6 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveAnyClass #-}
-{-# LANGUAGE NamedFieldPuns #-}
 module Main where
 
 import Control.Monad.IO.Class
@@ -12,9 +11,7 @@ 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
@@ -24,7 +21,7 @@ import Data.Foldable
 import Data.Maybe
 import Data.IORef
 
-import Debug (traceDocM)
+import Debug.Trace
 
 import Elab.Monad hiding (switch)
 import Elab.WiredIn
@@ -58,7 +55,7 @@ main = do
     Check files verbose -> do
       env <- checkFiles files
       when verbose $ dumpEnv env
-    Repl -> enterReplIn =<< emptyEnv
+    Repl -> enterReplIn =<< checkFiles ["./test.tt"]
 
 evalArgExpr :: ElabEnv -> String -> IO ()
 evalArgExpr env str =
@@ -66,7 +63,7 @@ evalArgExpr env str =
     Right e ->
       flip runElab env (do
         (e, _) <- infer e
-        liftIO . print . prettyTm . quote =<< Elab.Eval.eval e)
+        liftIO . putStrLn . show . prettyTm . quote . zonk =<< Elab.Eval.eval e)
       `catch` \e -> do
           displayExceptions' inp (e :: SomeException)
     Left e -> liftIO $ print e
@@ -74,69 +71,30 @@ evalArgExpr env str =
     inp = T.pack str
 
 enterReplIn :: ElabEnv -> IO ()
-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 }
-
-    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
+enterReplIn env = runInputT defaultSettings (loop env') where
+  env' = env { commHook = putStrLn . show . prettyTm . quote }
 
-              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
+  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
 
 checkFiles :: [String] -> IO ElabEnv
-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
+checkFiles files = runElab (go files ask) =<< emptyEnv where
+  go [] k = do
     env <- ask
     for_ (Map.toList (nameMap env)) \case
       (_, v@Defined{})
@@ -144,41 +102,34 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
         | otherwise ->
           let
             pos = fromJust (Map.lookup v (whereBound env))
-           in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
+           in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v
       _ -> pure ()
 
-    metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
+    metas <- liftIO $ readIORef (unsolvedMetas env)
     unless (Map.null metas) $ do
-      liftIO $ reportUnsolved Nothing metas
-    k
+      liftIO $ reportUnsolved metas
 
-  go n (x:xs) k = do
-    liftIO . putStrLn $ "[" ++ pad (show n) ++ "/" ++ show size ++ "] Loading " ++ x
+    k
+  go (x:xs) k = do
     code <- liftIO $ Bsl.readFile x
     case runAlex (code <> Bsl.singleton 10) parseProg of
-      Left e -> liftIO (print e) *> k
+      Left e -> liftIO $ print e *> error (show e)
       Right prog ->
-        local (\e -> e { currentFile = Just (T.pack x), loadedFiles = x:loadedFiles e }) (checkProgram prog (go (n + 1 :: Int) xs k))
+        local (\e -> e { currentFile = Just (T.pack x) }) (checkProgram prog (go 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
-  Lt.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
+  T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
 
 parser :: ParserInfo Opts
-parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
+parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
   where
     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"
@@ -208,65 +159,44 @@ displayExceptions lines =
       T.putStrLn $ squiggleUnder a b lines
   , Handler \(AttachedNote n e) -> do
       displayExceptions' lines e
-      Lt.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
-  , Handler \(WhenCheckingEndpoint dir le ri ep e) -> do
+      T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
+  , Handler \(WhenCheckingEndpoint le ri ep e) -> do
       displayExceptions' lines e
       let
         endp = case ep of
-          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"
+          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"
         ]
   , Handler \(NotEqual ta tb) -> do
-      Lt.putStrLn . render . vsep $
+      putStrLn . unlines $
         [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
-        , indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta))
-        , indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb))
+        , "  * \x1b[1mActual\x1b[0m:   " ++ showValue (zonk ta)
+        , "  * \x1b[1mExpected\x1b[0m: " ++ showValue (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 \(Elab.DeclaredUndefined n) -> do
+  , Handler \(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."
   ]
 
-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
+reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
+reportUnsolved metas = do
   for_ (Map.toList metas) \(m, p) ->  do
     case mvSpan m of
-      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)
+      Just (f, s, e) -> 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 ()
@@ -282,11 +212,14 @@ 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
-      traceDocM (viaShow t)
+      traceM (show t)
       dumpTokens

src/Presyntax/Lexer.x

@@ -7,8 +7,6 @@ import qualified Data.Text as T
 
 import Presyntax.Tokens
 
-import Debug.Trace
-
 }
 
 %wrapper "monadUserState-bytestring"
@@ -34,14 +32,13 @@ tokens :-
 
 <0> \\                            { always TokLambda }
 <0> "->"                          { always TokArrow }
-<0> "_"                           { always TokUnder }
 
 <0> \(                            { always TokOParen }
 <0> \{                            { always TokOBrace }
 <0> \[                            { always TokOSquare }
 
 <0> \)                            { always TokCParen }
-<0> \}                            { closeBrace }
+<0> \}                            { always TokCBrace }
 <0> \]                            { always TokCSquare }
 
 <0> \;                            { always TokSemi }
@@ -74,7 +71,6 @@ tokens :-
 -- layout: indentation of the next token is context for offside rule
 <layout> {
   \n ;
-  \{ { openBrace }
   () { startLayout }
 }
 
@@ -149,20 +145,6 @@ startLayout (AlexPn _ line col, _, _, _) _ = do
     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
@@ -183,4 +165,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 FlexibleContexts, FlexibleInstances, ViewPatterns #-}
+{-# LANGUAGE FlexibleInstances, ViewPatterns #-}
 module Presyntax.Parser where
 
 import qualified Data.Text as T
@@ -50,7 +50,6 @@ import Debug.Trace
   '\\'        { Token TokLambda _ _ }
   
   '->'        { Token TokArrow _ _ }
-  '_'         { Token TokUnder _ _ }
   ':'         { Token TokColon _ _ }
   ';'         { Token TokSemi  _ _ }
   '='         { Token TokEqual _ _ }
@@ -81,8 +80,8 @@ import Debug.Trace
 Exp :: { Expr }
 Exp
   : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
-  | '\\' MaybeLambdaList '[' Faces ']'   { span $1 $5 $ makeLams $2 $ LamSystem $4 }
-  | '\\' 'case' Block(CaseList)          { span $1 $3 $ LamCase (thd $3) }
+  | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
+  | '\\' 'case' START CaseList END       { span $1 $5 $ LamCase $4 }
   | '(' 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 }
@@ -90,7 +89,8 @@ Exp
   | '(' var ':' Exp ')' '*'  Exp         { span $1 $7 $ Sigma (getVar $2) $4 $7 }
   | ExpApp '*' Exp                       { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
 
-  | 'let' Block(LetList) 'in' Exp        { span $1 $4 $ Let (thd $2) $4 }
+  | 'let' START LetList END 'in' Exp     { span $1 $6 $ Let $3 $6 }
+  | 'let' START LetList END Exp          { span $1 $5 $ Let $3 $5 }
 
   | ExpApp                               { $1 }
 
@@ -110,7 +110,6 @@ Tuple :: { Expr }
 
 Atom :: { Expr }
   : var           { span $1 $1 $ Var (getVar $1) }
-  | '_'           { span $1 $1 $ Hole }
   | '(' Tuple ')' { span $1 $3 $ $2 }
 
 ProdTail :: { Expr }
@@ -124,9 +123,7 @@ 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 }
@@ -152,8 +149,7 @@ CaseItem :: { (Pattern, Expr) }
   : Pattern '->' Exp { ($1, $3) }
   
 CaseList :: { [(Pattern, Expr)] }
-  :                         { [] }
-  | CaseItem                { [$1] }
+  : CaseItem                { [$1] }
   | CaseItem Semis CaseList { $1:$3 }
 
 Pattern :: { Pattern }
@@ -167,14 +163,12 @@ 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' 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) }
+  | '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 }
 
 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
@@ -219,6 +213,18 @@ 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 }
@@ -244,10 +250,6 @@ 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,7 +10,6 @@ data Plicity
 
 data Expr
   = Var Text
-  | Hole
 
   | App Plicity Expr Expr
   | Pi  Plicity Text Expr Expr
@@ -21,7 +20,7 @@ data Expr
   | Proj1 Expr
   | Proj2 Expr
 
-  | LamSystem [(Formula, Expr)]
+  | LamSystem [(Condition, Expr)]
   | LamCase [(Pattern, Expr)]
   | Let [LetItem] Expr
 
@@ -33,6 +32,10 @@ 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,7 +9,6 @@ data TokenClass
 
   | TokLambda
   | TokArrow
-  | TokUnder
 
   | TokOParen
   | TokOBrace
@@ -71,7 +70,6 @@ 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,4 +1,3 @@
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE BlockArguments #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DeriveDataTypeable #-}
@@ -29,9 +28,11 @@ 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)
@@ -39,19 +40,11 @@ data WiredIn
 
   | WiComp  --    {A : I -> Type} {phi : I}
             -- -> ((i : I) -> Partial phi (A i)
-            -- -> (A i0)[phi -> u i0] -> A i1
+            -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u 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
@@ -86,6 +79,9 @@ 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
 
@@ -103,11 +99,6 @@ data Term
   | Unglue Term 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 =
@@ -115,8 +106,6 @@ data MV =
      , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
      , mvType :: NFType
      , mvSpan :: Maybe (Text, Posn, Posn)
-     , mvInteraction :: Bool
-     , mvContext :: Map Name NFType
      }
 
 instance Eq MV where
@@ -170,6 +159,9 @@ data Value
   | VPath NFLine Value Value
   | VLine NFLine Value Value Value
 
+  | VIsOne NFEndp
+  | VItIsOne
+
   | VPartial  NFEndp Value
   | VPartialP NFEndp Value
   | VSystem (Map Value Value)
@@ -185,16 +177,13 @@ data Value
   | VUnglue NFSort NFEndp NFPartial NFPartial Value
 
   | 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 :: Bool -> Set Name -> Value -> Term
-quoteWith short names (VNe h sp) = foldl goSpine (goHead h) sp where
+quoteWith :: Set Name -> Value -> Term
+quoteWith 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
@@ -204,89 +193,74 @@ quoteWith short 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
-      VLam{} -> PCon (quote sys) v
-      s -> constantly (length sp) s
+      _ -> PCon (quote sys) v
   goHead (HData x v) = Data x v
 
-  goSpine t (PApp p v) = App p t (quoteWith short names v)
+  goSpine t (PApp p v) = App p t (quoteWith 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 short names n
+  constantly 0 n = quoteWith names n
   constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) 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 _ Seq.Empty x) = quoteWith names x
 
-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 (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 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 (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 (VLam p (Closure n k)) =
+quoteWith names (VLam p (Closure n k)) =
   let n' = refresh Nothing names n
-   in Lam p n' (quoteWith short (Set.insert n' names) (k (VVar n')))
+   in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
 
-quoteWith short names (VPi p d (Closure n k)) =
+quoteWith names (VPi p d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Pi p n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
+   in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
 
-quoteWith short names (VSigma d (Closure n k)) =
+quoteWith names (VSigma d (Closure n k)) =
   let n' = refresh (Just d) names n
-   in Sigma n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
+   in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
 
-quoteWith short names (VPair a b) = Pair (quoteWith short names a) (quoteWith short names b)
-quoteWith _ _ VType = Type
-quoteWith _ _ VTypeω = Typeω
+quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
+quoteWith _ VType = Type
+quoteWith _ VTypeω = Typeω
 
-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 _ 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 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 (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 (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 (VIsOne v)  = IsOne (quoteWith names v)
+quoteWith _     VItIsOne    = ItIsOne
 
-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 (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 (VCase _ rng v xs) = Case (quoteWith short names rng) (quoteWith short names v) xs
+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 (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)
+quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
 
 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
@@ -297,7 +271,7 @@ refresh x s n
   | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
 
 quote :: Value -> Term
-quote = quoteWith True mempty
+quote = quoteWith mempty
 
 data Closure
   = Closure
@@ -322,31 +296,15 @@ data Head
   | HPCon Value Value Name
   | HMeta MV
   | HData Bool Name
-  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
+  deriving (Eq, Ord, Show)
 
 data Projection
   = PApp   Plicity Value
   | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
-  | POuc  NFSort NFEndp Value
-  | PK    NFSort Value NFSort Value
-  | PJ    NFSort Value NFSort Value Value
+  | POuc   NFSort NFEndp 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,14 +1,17 @@
-{-# 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 Lazy
+import qualified Data.Text.Lazy as L
+import qualified Data.Set as Set
 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(..))
 
@@ -18,216 +21,190 @@ import Prettyprinter
 import Syntax
 
 instance Pretty Name where
-  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
+  pretty = pretty . getNameText
 
-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 :: 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)
 
-prettyVl' :: Bool -> Value -> Doc AnsiStyle
-prettyVl' b = prettyTm' b . quoteWith True mempty
+  prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
+  prettyTm (App Ex f x) = parenFun f <+> parenArg x
 
-instance Pretty Term where
-  pretty = unAnnotate . prettyTm
+  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 :: Term -> Doc AnsiStyle
-prettyTm = prettyTm' printImplicits
+  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"
+
+  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
+
+  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
+
+  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 Value where
-  pretty = unAnnotate . prettyVl
+  prettyTm (System (Map.null -> True)) = braces mempty
 
-prettyVl :: Value -> Doc AnsiStyle
-prettyVl = prettyVl' printImplicits
+  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
 
-printImplicits :: Bool
-#if defined(RELEASE)
-printImplicits = False
-#else
-printImplicits = True
-#endif
+  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
 
-render :: Doc AnsiStyle -> Lazy.Text
-render = renderLazy . layoutSmart defaultLayoutOptions
+  prettyTm x = error (show x)
 
-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
+  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)
+
+  beautify (Lam Ex v (App Ex f (Ref v')))
+    | v == v', v `Set.notMember` freeVars f = f
+
+  beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0]
+  beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty
+
+  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]
+
+  beautify (GlueTy _ I1 (Lam _ _ a) _) = 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
+
+  toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a
 
 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 (\(_, _, y) -> freeVars y) y

stack.yaml

@@ -1,5 +1,67 @@
+# 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/8.yaml
+  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.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: 565720
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
-    sha256: 76bf8992ff8dfe6eda9c02f81866138c2369344d5011ab39ae403457c4448b03
+    size: 563098
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
+    sha256: 395775c03e66a4286f134d50346b0b6f1432131cf542886252984b4cfa5fef69
   original:
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml