Implement dependent paths (PathP's)

src/Elab.hs

@@ -15,9 +15,11 @@ import Elab.Eval
 
 import qualified Presyntax.Presyntax as P
 
-import Syntax
 import Prettyprinter
 
+import Syntax.Pretty
+import Syntax
+
 infer :: P.Expr -> ElabM (Term, NFType)
 infer (P.Span ex a b) = withSpan a b $ infer ex
 
@@ -28,10 +30,16 @@ infer (P.Var t) = do
 
 infer (P.App p f x) = do
   (f, f_ty) <- infer f
-  (d, r, w) <- isPiType p f_ty
-  x <- check x d
-  x_nf <- eval x
-  pure (App p (w f) x, r x_nf)
+  porp <- isPiType p f_ty
+  case porp of
+    It'sProd d r w -> do
+      x <- check x d
+      x_nf <- eval x
+      pure (App p (w f) x, r x_nf)
+    It'sPath li le ri wp -> do
+      x <- check x VI
+      x_nf <- eval x
+      pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
 
 infer (P.Proj1 x) = do
   (tm, ty) <- infer x
@@ -61,12 +69,23 @@ check tm (VPi P.Im dom (Closure var rng)) =
     Lam P.Im var <$> check tm (rng (VVar (Bound var)))
 
 check (P.Lam p v b) ty = do
-  (d, r, wp) <- isPiType p ty
-  assume (Bound v) d $
-    wp . Lam P.Im v <$> check b (r (VVar (Bound v)))
+  porp <- isPiType p =<< forceIO ty
+  case porp of
+    It'sProd d r wp -> do
+      assume (Bound v) d $
+        wp . Lam p v <$> check b (r (VVar (Bound v)))
+    It'sPath li le ri wp -> do
+      tm <- assume (Bound v) VI $
+        Lam P.Ex v <$> check b (li (VVar (Bound v)))
+      tm_nf <- eval tm
+      unify (tm_nf @@ VI0) le
+        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
+      unify (tm_nf @@ VI1) ri
+        `catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
+      pure (wp (PathIntro (quote (fun li)) tm))
 
 check (P.Pair a b) ty = do
-  (d, r, wp) <- isSigmaType ty
+  (d, r, wp) <- isSigmaType =<< forceIO ty
   a <- check a d
   a_nf <- eval a
   b <- check b (r a_nf)
@@ -99,15 +118,33 @@ isSort VTypeω               = pure ()
 isSort vt@(VNe HMeta{} _)   = unify vt VType
 isSort vt = liftIO . throwIO $ NotEqual vt VType
 
-isPiType :: P.Plicity -> NFType -> ElabM (Value, NFType -> NFType, Term -> Term)
-isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (d, k, id)
+data ProdOrPath
+  = It'sProd { prodDmn  :: NFType
+             , prodRng  :: NFType -> NFType
+             , prodWrap :: Term -> Term
+             }
+  | It'sPath { pathLine  :: NFType -> NFType
+             , pathLeft  :: Value
+             , pathRight :: Value
+             , pathWrap  :: Term -> Term
+             }
+
+isPiType :: P.Plicity -> NFType -> ElabM ProdOrPath
+isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (It'sProd d k id)
+isPiType P.Ex (VPath li le ri) = pure (It'sPath (li @@) le ri id)
+isPiType P.Ex (VPi P.Im d (Closure _ k)) = do
+  meta <- newMeta d
+  porp <- isPiType P.Ex (k meta)
+  pure $ case porp of
+    It'sProd d r w -> It'sProd d r (\f -> w (App P.Im f (quote meta)))
+    It'sPath l x y w -> It'sPath l x y (\f -> w (App P.Im f (quote meta)))
 isPiType p t = do
   dom <- newMeta VType
   name <- newName
   assume (Bound name) dom $ do
     rng <- newMeta VType
     wp <- isConvertibleTo t (VPi p dom (Closure name (const rng)))
-    pure (dom, const rng, wp)
+    pure (It'sProd dom (const rng) wp)
 
 isSigmaType :: NFType -> ElabM (Value, NFType -> NFType, Term -> Term)
 isSigmaType (VSigma d (Closure _ k)) = pure (d, k, id)
@@ -138,8 +175,9 @@ checkStatement (P.Defn name rhs) k = do
       tm_nf <- eval tm
       define (Defined name) ty tm_nf k
     Just (ty_nf, nm) -> do
-      unless (nm == VVar (Defined name)) . liftIO . throwIO $
-        Redefinition (Defined name)
+      case nm of
+        VVar (Defined n') | n' == name -> pure ()
+        _ -> liftIO . throwIO $ Redefinition (Defined name)
 
       rhs <- check rhs ty_nf
       rhs_nf <- eval rhs
@@ -183,4 +221,7 @@ checkProgram [] k = k
 checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
 
 newtype Redefinition = Redefinition { getRedefName :: Name }
-  deriving (Show, Typeable, Exception)
+  deriving (Show, Typeable, Exception)
+
+data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
+  deriving (Show, Typeable, Exception)

src/Elab/Eval.hs

@@ -7,8 +7,10 @@ import Control.Monad.Reader
 import Control.Exception
 
 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.Sequence (Seq)
 import Data.Traversable
 import Data.Set (Set)
 import Data.Typeable
@@ -16,31 +18,34 @@ import Data.Foldable
 import Data.IORef
 import Data.Maybe
 
-import {-# SOURCE #-} Elab.WiredIn
 import Elab.Monad
 
 import Presyntax.Presyntax (Plicity(..))
 
+import Syntax.Pretty
 import Syntax
 
 import System.IO.Unsafe
-import Syntax.Pretty
+
+import {-# SOURCE #-} Elab.WiredIn
+import Prettyprinter
 
 eval :: Term -> ElabM Value
-eval t = asks (flip evalWithEnv t)
+eval t = asks (flip eval' t)
 
 forceIO :: MonadIO m => Value -> m Value
 forceIO vl@(VNe (HMeta (MV _ cell)) args) = do
   solved <- liftIO $ readIORef cell
   case solved of
-    Just vl -> forceIO $ foldl applProj vl (reverse args)
+    Just vl -> forceIO $ foldl applProj vl args
     Nothing -> pure vl
 forceIO x = pure x
 
 applProj :: Value -> Projection -> Value
-applProj fun (PApp p arg) = vApp p fun arg
-applProj fun PProj1 = vProj1 fun
-applProj fun PProj2 = vProj2 fun
+applProj fun (PApp p arg)     = vApp p fun arg
+applProj fun (PIElim l x y i) = ielim l x y fun i
+applProj fun PProj1           = vProj1 fun
+applProj fun PProj2           = vProj2 fun
 
 force :: Value -> Value
 force = unsafePerformIO . forceIO
@@ -53,11 +58,12 @@ zonkIO (VNe hd sp) = do
     HMeta (MV _ cell) -> do
       solved <- liftIO $ readIORef cell
       case solved of
-        Just vl -> zonkIO $ foldl applProj vl (reverse sp')
+        Just vl -> zonkIO $ foldl applProj vl sp'
         Nothing -> pure $ VNe hd sp'
     hd -> pure $ VNe hd sp'
   where
     zonkSp (PApp p x) = PApp p <$> zonkIO x
+    zonkSp (PIElim l x y i) = PIElim <$> zonkIO l <*> zonkIO x <*> zonkIO y <*> zonkIO i
     zonkSp PProj1 = pure PProj1
     zonkSp PProj2 = pure PProj2
 zonkIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (zonk . k))
@@ -65,6 +71,9 @@ zonkIO (VPi p d (Closure s k)) = VPi p <$> zonkIO d <*> pure (Closure s (zonk .
 zonkIO (VSigma d (Closure s k)) = VSigma <$> zonkIO d <*> pure (Closure s (zonk . k))
 zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
 
+zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y
+zonkIO (VLine line f) = VLine <$> zonkIO line <*> zonkIO f
+
 -- Sorts
 zonkIO VType = pure VType
 zonkIO VTypeω = pure VTypeω
@@ -80,55 +89,65 @@ zonkIO (VINot x) = inot <$> zonkIO x
 zonk :: Value -> Value
 zonk = unsafePerformIO . zonkIO
 
-evalWithEnv :: ElabEnv -> Term -> Value
-evalWithEnv env (Ref x) =
+eval' :: ElabEnv -> Term -> Value
+eval' env (Ref x) =
   case Map.lookup x (getEnv env) of
     Just (_, vl) -> vl
     _ -> error "variable not in scope when evaluating"
-evalWithEnv env (App p f x) = vApp p (evalWithEnv env f) (evalWithEnv env x)
+eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
-evalWithEnv env (Lam p s t) =
+eval' env (Lam p s t) =
   VLam p $ Closure s $ \a ->
-    evalWithEnv env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t
+    eval' env { getEnv = Map.insert (Bound 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 (Bound s) (error "type of abs", a) (getEnv env))} t
 
-evalWithEnv env (Pi p s d t) =
-  VPi p (evalWithEnv env d) $ Closure s $ \a ->
-    evalWithEnv env { getEnv = (Map.insert (Bound s) (error "type of abs", a) (getEnv env))} t
+eval' _ (Meta m) = VNe (HMeta m) mempty
 
-evalWithEnv _ (Meta m) = VNe (HMeta m) []
+eval' env (Sigma s d t) =
+  VSigma (eval' env d) $ Closure s $ \a ->
+    eval' env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t
 
-evalWithEnv env (Sigma s d t) =
-  VSigma (evalWithEnv env d) $ Closure s $ \a ->
-    evalWithEnv env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t
+eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
 
-evalWithEnv e (Pair a b) = VPair (evalWithEnv e a) (evalWithEnv e b) 
+eval' e (Proj1 a) = vProj1 (eval' e a)
+eval' e (Proj2 a) = vProj2 (eval' e a)
 
-evalWithEnv e (Proj1 a) = vProj1 (evalWithEnv e a)
-evalWithEnv e (Proj2 a) = vProj2 (evalWithEnv e a)
+eval' _ Type = VType
+eval' _ Typeω = VTypeω
+eval' _ I = VI
+eval' _ I0 = VI0
+eval' _ I1 = VI1
 
-evalWithEnv _ Type = VType
-evalWithEnv _ Typeω = VTypeω
-evalWithEnv _ I = VI
-evalWithEnv _ I0 = VI0
-evalWithEnv _ I1 = VI1
+eval' e (IAnd x y) = iand (eval' e x) (eval' e y)
+eval' e (IOr x y) = ior (eval' e x) (eval' e y)
+eval' e (INot x) = inot (eval' e x)
 
-evalWithEnv e (IAnd x y) = iand (evalWithEnv e x) (evalWithEnv e y)
-evalWithEnv e (IOr x y) = ior (evalWithEnv e x) (evalWithEnv e y)
-evalWithEnv e (INot x) = inot (evalWithEnv e x)
+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 f) = VLine (eval' e p) (eval' e f)
 
 vApp :: Plicity -> Value -> Value -> Value
-vApp p (VLam p' k) arg = assert (p == p') $ clCont k arg
-vApp p (VNe h sp) arg  = VNe h (PApp p arg:sp)
+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 _ x _             = error $ "can't apply " ++ show x
 
+(@@) :: Value -> Value -> Value
+(@@) = vApp Ex
+infixl 9 @@
+
 vProj1 :: Value -> Value
 vProj1 (VPair a _) = a
-vProj1 (VNe h sp) = VNe h (PProj1:sp)
+vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
 vProj1 x = error $ "can't proj1 " ++ show x
 
 vProj2 :: Value -> Value
 vProj2 (VPair _ b) = b
-vProj2 (VNe h sp)  = VNe h (PProj2:sp)
+vProj2 (VNe h sp)  = VNe h (sp Seq.:|> PProj2)
 vProj2 x = error $ "can't proj2 " ++ show x
 
 data NotEqual = NotEqual Value Value
@@ -141,8 +160,13 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
 
   go (VNe x a) (VNe x' a')
     | x == x', length a == length a' =
-      traverse_ (uncurry unify'Spine) (zip a a')
-    | otherwise = fail
+      traverse_ (uncurry unify'Spine) (Seq.zip a a')
+  
+  go (VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs =
+    case force i of
+      VI0 -> unify' x rhs
+      VI1 -> unify' y rhs
+      _   -> fail
 
   go (VLam p (Closure _ k)) vl = do
     t <- VVar . Bound <$> newName
@@ -171,6 +195,23 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go VI VI   = pure ()
   go VI0 VI0 = pure ()
   go VI1 VI1 = pure ()
+  
+  go (VINot x)   (VINot y)     = unify' x y
+  go (VIAnd x y) (VIAnd x' y') = unify' x x' *> unify' y y'
+  go (VIOr x y)  (VIOr x' y')  = unify' x x' *> unify' y y'
+
+  go (VPath l x y) (VPath l' x' y') = do
+    unify' l l'
+    unify' x x'
+    unify' y y'
+  
+  go (VLine l p) p' = do
+    n <- VVar . Bound <$> newName
+    unify (p @@ n) (ielim l (l @@ VI0) (l @@ VI1) p' n)
+
+  go p' (VLine l p) = do
+    n <- VVar . Bound <$> newName
+    unify (ielim l (l @@ VI0) (l @@ VI1) p' n) (p @@ n)
 
   go _ _ = fail
 
@@ -182,6 +223,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   unify'Spine PProj1 PProj1 = pure ()
   unify'Spine PProj2 PProj2 = pure ()
 
+  unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
+
   unify'Spine _ _ = fail
 
 unify :: Value -> Value -> ElabM ()
@@ -191,8 +234,17 @@ isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
 VPi Im d (Closure _v k) `isConvertibleTo` ty = do
   meta <- newMeta d
   cont <- k meta `isConvertibleTo` ty
-  pure (\f -> cont (App Ex f (quote meta)))
+  pure (\f -> cont (App Im f (quote meta)))
 VType `isConvertibleTo` VTypeω = pure id
+
+VPi p d (Closure _ k) `isConvertibleTo` VPi p' d' (Closure _ k') | p == p' = do
+  wp <- d' `isConvertibleTo` d
+  n <- newName
+  wp_n <- eval (Lam Ex n (wp (Ref (Bound n))))
+
+  wp' <- k (VVar (Bound n)) `isConvertibleTo` k' (wp_n @@ VVar (Bound n))
+  pure (\f -> Lam p n (wp' (App p f (wp (Ref (Bound n))))))
+
 isConvertibleTo a b = do
   unify' a b
   pure id
@@ -210,7 +262,7 @@ newMeta _dom = do
       Bound{} -> Just (PApp Ex (VVar n))
       _ -> Nothing
 
-  pure (VNe (HMeta m) (catMaybes t))
+  pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
 
 newName :: MonadIO m => m T.Text
 newName = liftIO $ do
@@ -221,14 +273,14 @@ _nameCounter :: IORef Int
 _nameCounter = unsafePerformIO $ newIORef 0
 {-# NOINLINE _nameCounter #-}
 
-solveMeta :: MV -> [Projection] -> Value -> ElabM ()
+solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
 solveMeta m@(MV _ cell) sp rhs = do
   env <- ask
-  liftIO $ putStrLn (showValue (VNe (HMeta m) sp) ++ " ≡? " ++ showValue rhs)
   names <- checkSpine Set.empty sp
   checkScope (Set.fromList (Bound <$> names)) rhs
+    `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
   let tm = quote rhs
-      lam = evalWithEnv env $ foldr (Lam Ex) tm names
+      lam = eval' env $ foldr (Lam Ex) tm names
   liftIO . atomicModifyIORef' cell $ \case
     Just _ -> error "filled cell in solvedMeta"
     Nothing -> (Just lam, ())
@@ -245,6 +297,7 @@ checkScope scope (VNe h sp) =
     traverse_ checkProj sp
   where
     checkProj (PApp _ t) = checkScope scope t
+    checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
     checkProj PProj1 = pure ()
     checkProj PProj2 = pure ()
 
@@ -272,12 +325,15 @@ 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
 
-checkSpine :: Set Name -> [Projection] -> ElabM [T.Text]
-checkSpine scope (PApp Ex (VVar n@(Bound t)):xs)
+checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
+checkScope s (VLine _ line) = checkScope s line
+
+checkSpine :: Set Name -> Seq Projection -> ElabM [T.Text]
+checkSpine scope (PApp Ex (VVar n@(Bound t)) Seq.:<| xs)
   | n `Set.member` scope = liftIO . throwIO $ NonLinearSpine n
   | otherwise = (t:) <$> checkSpine scope xs
-checkSpine _     (p:_) = liftIO . throwIO $ SpineProj p
-checkSpine _     [] = pure []
+checkSpine _     (p Seq.:<| _) = liftIO . throwIO $ SpineProj p
+checkSpine _     Seq.Empty = pure []
 
 newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
   deriving (Show, Typeable, Exception)

src/Elab/Monad.hs

@@ -49,7 +49,6 @@ assumes nm ty = local go where
            , whereBound = maybe (whereBound x) (\l -> Map.union (Map.fromList (zip nm (repeat l))) (whereBound x)) (currentSpan x)
            }
 
-
 getNameText :: Name -> Text
 getNameText (Bound x) = x
 getNameText (Defined x) = x
@@ -129,4 +128,12 @@ seeAlso k nm = do
 catchElab :: Exception e => ElabM a -> (e -> ElabM a) -> ElabM a
 catchElab k h = do
   env <- ask
-  liftIO $ runElab k env `catch` \e -> runElab (h e) env
+  liftIO $ runElab k env `catch` \e -> runElab (h e) env
+
+tryElab :: Exception e => ElabM a -> ElabM (Either e a)
+tryElab k = do
+  env <- ask
+  liftIO $ (Right <$> runElab k env) `catch` \e -> pure (Left e)
+  
+throwElab :: Exception e => e -> ElabM a
+throwElab = liftIO . throwIO

src/Elab/WiredIn.hs

@@ -13,6 +13,7 @@ import Control.Exception
 import Data.Typeable
 import qualified Presyntax.Presyntax as P
 import Elab.Eval
+import qualified Data.Sequence as Seq
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -25,6 +26,7 @@ wiType WiI1       = VI
 wiType WiIAnd      = VI ~> VI ~> VI
 wiType WiIOr       = VI ~> VI ~> VI
 wiType WiINot      = VI ~> VI
+wiType WiPathP     = dprod (VI ~> VTypeω) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
@@ -37,6 +39,7 @@ wiValue WiI1       = VI1
 wiValue WiIAnd      = fun \x -> fun \y -> iand x y
 wiValue WiIOr       = fun \x -> fun \y -> ior x y
 wiValue WiINot      = fun inot
+wiValue WiPathP     = fun \a -> fun \x -> fun \y -> VPath a x y
 
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure "_" (const b))
@@ -45,19 +48,26 @@ infixr 7 ~>
 fun :: (Value -> Value) -> Value
 fun k = VLam P.Ex $ Closure "x" (k . force)
 
+forallI :: (Value -> Value) -> Value
+forallI k = VLam P.Im $ Closure "x" (k . force)
+
 dprod :: Value -> (Value -> Value) -> Value
 dprod a b = VPi P.Ex a (Closure "x" b)
 
+forAll :: Value -> (Value -> Value) -> Value
+forAll a b = VPi P.Im a (Closure "x" b)
+
 wiredInNames :: Map Text WiredIn
 wiredInNames = Map.fromList
-  [ ("pretype", WiPretype)
-  , ("type", WiType)
-  , ("interval", WiInterval)
+  [ ("Pretype", WiPretype)
+  , ("Type", WiType)
+  , ("Interval", WiInterval)
   , ("i0", WiI0)
   , ("i1", WiI1)
   , ("iand", WiIAnd)
   , ("ior",  WiIOr)
   , ("inot", WiINot)
+  , ("PathP", WiPathP)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -90,4 +100,11 @@ inot = \case
   VIOr x y -> VIAnd (inot x) (inot y)
   VIAnd x y -> VIOr (inot x) (inot y)
   VINot x -> x
-  x -> VINot x
+  x -> VINot x
+
+ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value
+ielim _line _left _right fn i =
+  case force fn of
+    VLine _ fun -> fun @@ i
+    VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i)
+    _ -> error $ "can't ielim " ++ show fn

src/Elab/WiredIn.hs-boot

@@ -6,4 +6,5 @@ wiType  :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
 
 iand, ior :: Value -> Value -> Value
-inot :: Value -> Value
+inot :: Value -> Value
+ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value

src/Main.hs

@@ -46,7 +46,7 @@ main = do
 
 enterReplIn :: ElabEnv -> IO ()
 enterReplIn env = runInputT defaultSettings (loop env') where
-  env' = env { commHook = T.putStrLn . render . prettyTm . quote }
+  env' = env { commHook = T.putStrLn . render . prettyTm . quote . zonk }
 
   loop :: ElabEnv -> InputT IO ()
   loop env = do
@@ -113,6 +113,21 @@ displayExceptions lines =
   , Handler \(SeeAlso a b e) -> do
       displayExceptions' lines e
       T.putStrLn $ squiggleUnder a b lines
+  , Handler \(AttachedNote n e) -> do
+      displayExceptions' lines e
+      T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
+  , Handler \(WhenCheckingEndpoint le ri ep e) -> do
+      displayExceptions' lines e
+      let
+        endp = case ep of
+          VI0 -> T.pack "left"
+          VI1 -> T.pack "right"
+          _ -> T.pack $ show (prettyTm (quote ep))
+      T.putStrLn . T.unlines $
+        [ "\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram"
+        , "\t " <> render (prettyTm (quote le)) <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> render (prettyTm (quote ri))
+        , "\x1b[1;32mnote\x1b[0m: the " <> endp <> " endpoint is incorrect"
+        ]
   , Handler \(NotEqual ta tb) -> do
       putStrLn . unlines $
         [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
@@ -123,9 +138,6 @@ displayExceptions lines =
       putStrLn $ "Unknown primitive: " ++ T.unpack x
   , Handler \(NotInScope x) -> do
       putStrLn $ "Variable not in scope: " ++ show x
-  , Handler \(AttachedNote n e) -> do
-      displayExceptions' lines e
-      T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
   ]
 
 displayExceptions' :: Exception e => Text -> e -> IO ()

src/Presyntax/Parser.y

@@ -1,4 +1,5 @@
 {
+{-# LANGUAGE FlexibleInstances #-}
 module Presyntax.Parser where
 
 import qualified Data.Text as T
@@ -57,18 +58,33 @@ import Prelude hiding (span)
 
 Exp :: { Expr }
 Exp
-  : Exp ExpProj                       { span $1 $2 $ App Ex $1 $2 }
-  | Exp '{' Exp '}'                   { span $1 $4 $ App Im $1 $3 }
+  : '\\' LambdaList '->' Exp          { span $1 $4 $ makeLams $2 $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 }
 
-  | '\\' LambdaList '->' Exp          { span $1 $4 $ makeLams $2 $4 }
-  | '(' VarList ':' Exp ')' ProdTail  { span $1 $6 $ makePis Ex (thd $2) $4 $6 }
-  | '{' VarList ':' Exp '}' ProdTail  { span $1 $6 $ makePis Im (thd $2) $4 $6 }
-  | ExpProj '->' Exp                  { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
+  | '(' var ':' Exp ')' '*'  Exp      { span $1 $7 $ Sigma (getVar $2) $4 $7 }
+  | ExpApp '*' Exp                    { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
+
+  | ExpApp                            { $1 }
+
+ExpApp :: { Expr }
+  : ExpApp ExpProj         { span $1 $2 $ App Ex $1 $2 }
+  | ExpApp '{' Exp '}'     { span $1 $4 $ App Im $1 $3 }
+  | ExpProj                { $1 }
+
+ExpProj :: { Expr }
+  : ExpProj '.1' { span $1 $2 $ Proj1 $1 }
+  | ExpProj '.2' { span $1 $2 $ Proj2 $1 }
+  | Atom         { $1 }
 
-  | '(' VarList ':' Exp ')' '*'  Exp  { span $1 $7 $ makeSigmas (thd $2) $4 $7 }
-  | ExpProj '*' Exp                   { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
+Tuple :: { Expr }
+  : Exp           { $1 }
+  | Exp ',' Tuple { span $1 $3 $ Pair $1 $3 }
 
-  | ExpProj                           { $1 }
+Atom :: { Expr }
+  : var           { span $1 $1 $ Var (getVar $1) }
+  | '(' Tuple ')' { span $1 $3 $ $2 }
 
 ProdTail :: { Expr }
   : '(' VarList ':' Exp ')' ProdTail  { span $1 $6 $ makePis Ex (thd $2) $4 $6 }
@@ -87,21 +103,8 @@ LhsList :: { [(Plicity, Text)] }
   | LambdaList { $1 }
 
 VarList :: { (Posn, Posn, [Text]) }
-  : var         { (startPosn $1, endPosn $1, [getVar $1]) }
-  | var VarList { case $2 of (_, end, xs) -> (startPosn $1, end, getVar $1:xs) }
-
-ExpProj :: { Expr }
-  : ExpProj '.1' { span $1 $2 $ Proj1 $1 }
-  | ExpProj '.2' { span $1 $2 $ Proj2 $1 }
-  | Atom         { $1 }
-
-Atom :: { Expr }
-  : var           { span $1 $1 $ Var (getVar $1) }
-  | '(' Tuple ')' { span $1 $3 $ $2 }
-
-Tuple :: { Expr }
-  : Exp           { $1 }
-  | Exp ',' Tuple { span $1 $3 $ Pair $1 $3 }
+  : var             { (startPosn $1, endPosn $1, [getVar $1]) }
+  | var ',' VarList { case $3 of (_, end, xs) -> (startPosn $1, end, getVar $1:xs) }
 
 Statement :: { Statement }
   : VarList ':' Exp     { spanSt $1 $3 $ Decl (thd $1) $3 }

src/Syntax.hs

@@ -9,6 +9,8 @@ import qualified Data.Text as T
 import Data.IORef (IORef)
 import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
 
 data WiredIn
   = WiType
@@ -19,6 +21,7 @@ data WiredIn
   | WiIAnd
   | WiIOr
   | WiINot
+  | WiPathP
   deriving (Eq, Show, Ord)
 
 data Term
@@ -40,6 +43,14 @@ data Term
   | IAnd Term Term
   | IOr  Term Term
   | INot Term
+
+  | PathP     Term Term Term
+  -- ^ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
+  | IElim     Term Term Term Term Term
+  -- ^ IElim : {A : I -> Type} {x : A i0} {y : A i1} (p : PathP A x y) (i : I) -> A i
+  | PathIntro Term Term
+  -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
+  --   ~~~~~~~~~ not printed at all
   deriving (Eq, Show, Ord)
 
 data MV =
@@ -60,9 +71,10 @@ data Name
   deriving (Eq, Show, Ord)
 
 type NFType = Value
+type NFEndp = Value
 
 data Value
-  = VNe    Head            [Projection]
+  = VNe    Head            (Seq Projection)
   | VLam   Plicity         Closure
   | VPi    Plicity Value   Closure
   | VSigma Value   Closure
@@ -75,17 +87,21 @@ data Value
   | VIAnd Value Value
   | VIOr  Value Value
   | VINot Value
+
+  | VPath Value Value Value
+  | VLine Value Value
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
-pattern VVar x = VNe (HVar x) []
+pattern VVar x = VNe (HVar x) Seq.Empty
 
 quoteWith :: Set Text -> Value -> Term
-quoteWith names (VNe h sp) = foldl goSpine (goHead h) (reverse sp) where
+quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
   goHead (HVar v) = Ref v
   goHead (HMeta m) = Meta m
 
-  goSpine t (PApp p v) = App p t (quoteWith 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 PProj1 = Proj1 t
   goSpine t PProj2 = Proj2 t
 
@@ -111,6 +127,9 @@ 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 names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
+quoteWith names (VLine p f)      = PathIntro (quoteWith names p) (quoteWith names f)
+
 refresh :: Set Text -> Text -> Text
 refresh s n
   | T.singleton '_' == n = n
@@ -143,7 +162,8 @@ data Head
   deriving (Eq, Show, Ord)
 
 data Projection
-  = PApp Plicity Value
+  = PApp   Plicity Value
+  | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
   deriving (Eq, Show, Ord)

src/Syntax/Pretty.hs

@@ -56,6 +56,10 @@ prettyTm (IAnd x y) = prettyTm x <+> operator (pretty "&&") <+> prettyTm y
 prettyTm (IOr x y) = prettyTm x <+> operator (pretty "||") <+> prettyTm y
 prettyTm (INot x) = operator (pretty '~') <> prettyTm x
 
+prettyTm (PathP l x y) = keyword (pretty "PathP") <+> parenArg l <+> parenArg x <+> parenArg y
+prettyTm (IElim _ _ _ f i) = prettyTm (App Ex f i)
+prettyTm (PathIntro _ f) = prettyTm f
+
 keyword :: Doc AnsiStyle -> Doc AnsiStyle
 keyword = annotate (color Magenta)
 
@@ -64,6 +68,7 @@ operator = annotate (color Yellow)
 
 parenArg :: Term -> Doc AnsiStyle
 parenArg x@App{} = parens (prettyTm x)
+parenArg x@IElim{} = parens (prettyTm x)
 parenArg x = prettyDom x
 
 prettyDom :: Term -> Doc AnsiStyle
@@ -73,6 +78,7 @@ 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

test.tt

@@ -1,6 +1,8 @@
-{-# PRIMITIVE pretype Pretype #-}
+{-# PRIMITIVE Type #-}
+{-# PRIMITIVE Pretype #-}
+
 I : Pretype
-{-# PRIMITIVE interval I #-}
+{-# PRIMITIVE Interval I #-}
 
 i0 : I
 i1 : I
@@ -14,4 +16,31 @@ ior : I -> I -> I
 {-# PRIMITIVE ior #-}
 
 inot : I -> I
-{-# PRIMITIVE inot #-}
+{-# PRIMITIVE inot #-}
+
+PathP : (A : I -> Pretype) -> A i0 -> A i1 -> Type
+{-# PRIMITIVE PathP #-}
+
+Path : {A : Pretype} -> A -> A -> Type
+Path {A} = PathP (\i -> A)
+
+refl : {A : Pretype} {x : A} -> Path x x
+refl {A} {x} i = x
+
+sym : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
+sym p i = p (inot i)
+
+the : (A : Pretype) -> A -> A
+the A x = x
+
+iElim : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
+iElim p i = p i
+
+Singl : (A : Type) -> A -> Type
+Singl A x = (y : A) * Path x y
+
+isContr : Type -> Type
+isContr A = (x : A) * ((y : A) -> Path x y)
+
+singContr : {A : Type} {a : A} -> isContr (Singl A a)
+singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))