Implement proper inductive types

intro.tt

@@ -152,13 +152,7 @@ IsOne : I -> Pretype
 -- The value itIs1 witnesses the fact that i1 = i1.
 itIs1 : IsOne i1
 
--- Furthermore, if either of i or j are one, then so is (i or j).
-isOneL : {i : I} {j : I} -> IsOne i -> IsOne (ior i j)
-isOneR : {i : I} {j : I} -> IsOne j -> IsOne (ior i j)
-
 {-# PRIMITIVE itIs1 #-}
-{-# PRIMITIVE isOneL #-}
-{-# PRIMITIVE isOneR #-}
 
 -- Partial elements
 -------------------
@@ -579,24 +573,24 @@ involToIso {A} f inv = (f, inv, inv)
 --
 -- We define it here.
 
-Bool : Type
-{-# PRIMITIVE Bool #-}
+data Bool : Type where
+  true : Bool
+  false : Bool
 
-true, false : Bool
-{-# PRIMITIVE true #-}
-{-# PRIMITIVE false #-}
+not : Bool -> Bool
+not = \case
+  true -> false
+  false -> true
 
--- Pattern matching for booleans: If a proposition holds for true and
--- for false, then it holds for every bool.
 elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b
-{-# PRIMITIVE if elimBool #-}
+elimBool P x y = \case
+  true -> x
+  false -> y
 
--- Non-dependent elimination of booleans
 if : {A : Type} -> A -> A -> Bool -> A
-if {A} = elimBool (\b -> A)
-
-not : Bool -> Bool
-not = if false true
+if x y = \case
+  true -> x
+  false -> y
 
 -- By pattern matching it suffices to prove (not (not true)) ≡ true and
 -- not (not false) ≡ false. Since not (not true) computes to true (resp.
@@ -686,4 +680,13 @@ pathIsHom {A} {B} {f} {g} =
   let
     theIso : Iso (Path f g) (Hom f g)
     theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
-  in univalence (IsoToEquiv theIso)
+  in univalence (IsoToEquiv theIso)
+
+data List (A : Type) : Type where
+  nil : List A
+  cons : A -> List A -> List A
+
+map : {A : Type} {B : Type} -> (A -> B) -> List A -> List B
+map f = \case
+  nil -> nil
+  cons x xs -> cons (f x) (map f xs)

src/Elab.hs

@@ -2,13 +2,17 @@
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DerivingStrategies #-}
 module Elab where
 
+import Control.Arrow (Arrow(first))
 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.Traversable
 import Data.Text (Text)
 import Data.Map (Map)
@@ -190,11 +194,79 @@ check (P.LamSystem bs) ty = do
     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
+  porp <- isPiType P.Ex ty
+  case porp of
+    It'sProd dom rng wp -> do
+      name <- newName
+      liftIO . print $ show pats
+      cases <- for pats $ \(pat, rhs) -> do
+        checkPattern pat dom \pat wp -> do
+          pat_nf <- eval pat
+          rhs <- check rhs (rng pat_nf)
+          pure (pat, wp rhs)
+      pure (wp (Lam P.Ex name (Case (Ref name) cases)))
+    _ -> do
+      dom <- newMeta VTypeω
+      n <- newName' (Bound (T.singleton 'x') 0)
+      assume n dom \_ -> do
+        rng <- newMeta VTypeω
+        throwElab $ NotEqual (VPi P.Ex dom (Closure n (const rng))) ty
+
 check exp ty = do
   (tm, has) <- switch $ infer exp
   wp <- isConvertibleTo has ty
   pure (wp tm)
 
+checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> ElabM a) -> ElabM a
+checkPattern (P.PCap var) dom cont = do
+  name <- asks (Map.lookup var . nameMap)
+  case name of
+    Just name@(ConName _ _ skip arity) -> do
+      unless (arity == 0) $ throwElab $ UnsaturatedCon name
+      ty <- instantiate =<< getNfType name
+      _ <- isConvertibleTo ty dom
+      wrap <- skipLams skip
+      cont (Con name) wrap
+    Just name -> throwElab $ NotACon name
+    Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name)
+checkPattern (P.PCon var args) dom cont =
+  do
+    name <- asks (Map.lookup var . nameMap)
+    case name of
+      Just name@(ConName _ _ nskip arity) -> do
+        unless (arity == length args) $ throwElab $ UnsaturatedCon name
+        ty <- instantiate =<< getNfType name
+        _ <- isConvertibleTo (skipBinders arity ty) dom
+        skip <- skipLams nskip
+        bindNames args ty $ \_ wrap ->
+          cont (Con name) (skip . wrap)
+      Just name -> throwElab $ NotACon name
+      _ -> throwElab $ NotInScope (Bound var 0)
+  where
+    skipBinders :: Int -> NFType -> NFType
+    skipBinders 0 t = t
+    skipBinders n (VPi _ _ (Closure v r)) = skipBinders (n - 1) (r (VVar v))
+    skipBinders _ _ = error $ "constructor type is wrong?"
+
+    bindNames (n:ns) (VPi p d (Closure _ r)) k =
+      assume (Bound n 0) d \n -> bindNames ns (r (VVar n)) \ns w ->
+        k (n:ns) (Lam p n . w)
+    bindNames [] _ k = k [] id
+    bindNames xs t _ = error $ show (xs, t)
+
+instantiate :: NFType -> ElabM NFType
+instantiate (VPi P.Im d (Closure _ k)) = do
+  t <- newMeta d
+  instantiate (k t)
+instantiate x = pure x
+
+skipLams :: Int -> ElabM (Term -> Term)
+skipLams 0 = pure id
+skipLams k = do
+  n <- newName
+  (Lam P.Im n . ) <$> skipLams (k - 1)
+
 checkLetItems :: Map Text (Maybe NFType) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
 checkLetItems _   [] cont = cont []
 checkLetItems map (P.LetDecl v t:xs) cont = do
@@ -333,7 +405,7 @@ checkStatement (P.Defn name rhs) k = do
       when t $ throwElab (Redefinition (Defined name 0))
 
       rhs <- check rhs ty_nf
-      rhs_nf <- eval rhs
+      rhs_nf <- evalFix (Defined name 0) ty_nf rhs
       makeLetDef (Defined name 0) ty_nf rhs_nf $ \name ->
         local (\e -> e { definedNames = Set.insert name (definedNames e) }) k
 
@@ -371,6 +443,58 @@ checkStatement (P.ReplTy e) k = do
   liftIO (h ty)
   k
 
+checkStatement (P.Data name tele retk constrs) k =
+  do
+    checkTeleRetk True tele retk \kind tele -> do
+      kind_nf <- eval kind
+      defineInternal (Bound name 0) kind_nf (\name' -> VNe (HData name') mempty) \name' -> do
+        checkCons tele (VNe (HData name') (Seq.fromList (map makeProj tele))) constrs k
+  where
+    makeProj (x, p, _) = PApp p (VVar x)
+
+    checkTeleRetk allKan [] retk cont = do
+      t <- check retk VTypeω
+      t_nf <- eval t
+      when allKan $ unify t_nf VType
+      cont t []
+    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
+      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs -> cont (Pi p nm t k) ((nm, p, t_nf):xs)
+
+    checkCons _ _et [] k = k
+
+    checkCons n ret ((x, ty):xs) k = do
+      t <- check ty VTypeω
+      ty_nf <- eval t
+      let
+        (args, ret') = splitPi ty_nf
+        closed = close n t
+        n' = map (\(x, _, y) -> (x, P.Im, y)) n
+      unify ret' ret
+      closed_nf <- eval closed
+      defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
+
+    close []             t = t
+    close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
+
+    splitPi (VPi p y (Closure x k)) = first ((x, p, y):) $ splitPi (k (VVar x))
+    splitPi t = ([], t)
+
+    makeCon cty sp []              [] con = VNe (HCon cty con) sp
+    makeCon cty sp ((nm, p, _):xs) ys con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) xs ys con
+    makeCon cty sp [] ((nm, p, _):ys) con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) [] ys con
+
+evalFix :: Name -> NFType -> Term -> ElabM Value
+evalFix name nft term = do
+  env <- ask
+  pure . fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
+
 checkProgram :: [P.Statement] -> ElabM a -> ElabM a
 checkProgram [] k = k
 checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
@@ -380,3 +504,11 @@ newtype Redefinition = Redefinition { getRedefName :: Name }
 
 data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
   deriving (Show, Typeable, Exception)
+
+data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
+  deriving          (Show, Typeable)
+  deriving anyclass (Exception)
+
+data NotACon = NotACon { theNotConstr :: Name }
+  deriving          (Show, Typeable)
+  deriving anyclass (Exception)

src/Elab/Eval.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE TupleSections #-}
 module Elab.Eval where
 
+import Control.Arrow (Arrow(second))
 import Control.Monad.Reader
 import Control.Exception
 
@@ -51,7 +52,7 @@ forceIO vl@(VSystem fs) =
     Just x -> forceIO x
     Nothing -> pure vl
 forceIO (GluedVl _ _ vl) = forceIO vl
-forceIO (VComp line phi u a0) = comp line <$> forceIO phi <*> pure u <*> pure a0
+forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
 forceIO x = pure x
 
 applProj :: Value -> Projection -> Value
@@ -99,8 +100,6 @@ zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
 zonkIO (VINot x) = inot <$> zonkIO x
 
 zonkIO (VIsOne x) = VIsOne <$> zonkIO x
-zonkIO (VIsOne1 x) = VIsOne1 <$> zonkIO x
-zonkIO (VIsOne2 x) = VIsOne2 <$> zonkIO x
 zonkIO VItIsOne = pure VItIsOne
 
 zonkIO (VPartial x y)  = VPartial <$> zonkIO x <*> zonkIO y
@@ -115,11 +114,7 @@ zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO
 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 VBool = pure VBool
-zonkIO VTt = pure VTt
-zonkIO VFf = pure VFf
-zonkIO (VIf a b c d) = elimBool <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
+zonkIO (VCase x xs) = VCase <$> zonkIO x <*> traverse (\(x, y) -> (x,) <$> zonkIO y) xs
 
 zonkSp :: Projection -> IO Projection
 zonkSp (PApp p x) = PApp p <$> zonkIO x
@@ -143,6 +138,13 @@ eval' env (Ref x) =
   case Map.lookup x (getEnv env) of
     Just (_, vl) -> vl
     _ -> VNe (HVar x) mempty
+
+eval' env (Con x) =
+  case Map.lookup x (getEnv env) of
+    Just (ty, _) -> VNe (HCon ty x) mempty
+    Nothing -> error $ "constructor " ++ show x ++ " has no type in scope"
+
+eval' _ (Data x) = VNe (HData x) mempty
 eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
 eval' env (Lam p s t) =
@@ -179,8 +181,6 @@ eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f
 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' e (IsOne1 i) = VIsOne1 (eval' e i)
-eval' e (IsOne2 i) = VIsOne2 (eval' e i)
 eval' _ ItIsOne    = VItIsOne
 
 eval' e (Partial x y)  = VPartial (eval' e x) (eval' e y)
@@ -200,10 +200,15 @@ eval' e (Let ns x) =
   let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns
    in eval' env' x
 
-eval' e (If a b c d) = elimBool (eval' e a) (eval' e b) (eval' e c) (eval' e d)
-eval' _ Bool = VBool
-eval' _ Tt = VTt
-eval' _ Ff = VFf
+eval' e (Case sc xs) = evalCase e (eval' e sc) xs
+
+evalCase :: ElabEnv -> Value -> [(Term, Term)] -> Value
+evalCase _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
+evalCase env sc ((Ref _, k):_) = eval' env k @@ sc
+evalCase env (force -> val@(VNe (HCon _ x) sp)) ((Con x', k):xs)
+  | x == x'   = foldl applProj (eval' env k) sp
+  | otherwise = evalCase env val xs
+evalCase env sc xs = VCase sc (map (second (eval' env)) xs)
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
@@ -291,10 +296,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   -- IsOne is proof-irrelevant:
   go VItIsOne _ = pure ()
   go _ VItIsOne = pure ()
-  go VIsOne1{} _ = pure ()
-  go _ VIsOne1{} = pure ()
-  go VIsOne2{} _ = pure ()
-  go _ VIsOne2{} = pure ()
 
   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'
@@ -317,10 +318,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VSystem sys) rhs = goSystem unify' sys rhs
   go rhs (VSystem sys) = goSystem (flip unify') sys rhs
 
-  go VTt VTt = pure ()
-  go VFf VFf = pure ()
-  go VBool VBool = pure ()
-
   go x y
     | x == y = pure ()
     | otherwise =
@@ -356,7 +353,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     | otherwise = fail
 
 unify :: HasCallStack => Value -> Value -> ElabM ()
-unify a b = unify' 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,7 +433,9 @@ checkScope scope (VNe h sp) =
         unless (v `Set.member` scope) . throwElab $
           NotInScope v
       HVar{} -> pure ()
+      HCon{} -> pure ()
       HMeta{} -> pure ()
+      HData{} -> pure ()
     traverse_ checkProj sp
   where
     checkProj (PApp _ t) = checkScope scope t
@@ -475,8 +474,6 @@ checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
 checkScope s (VLine _ _ _ line)   = checkScope s line
 
 checkScope s (VIsOne x) = checkScope s x
-checkScope s (VIsOne1 x) = checkScope s x
-checkScope s (VIsOne2 x) = checkScope s x
 checkScope _ VItIsOne   = pure ()
 
 checkScope s (VPartial x y)  = traverse_ (checkScope s) [x, y]
@@ -492,10 +489,7 @@ 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 s (VIf a b c d) = traverse_ (checkScope s) [a, b, c, d]
-checkScope _ VBool = pure ()
-checkScope _ VTt = pure ()
-checkScope _ VFf = pure ()
+checkScope s (VCase v xs) = checkScope s v *> traverse_ (checkScope s . snd) xs
 
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)

src/Elab/Monad.hs

@@ -169,3 +169,4 @@ throwElab = liftIO . throwIO
 incName :: Name -> Name -> Name
 incName (Bound x _) n = Bound x (getNameNum n + 1)
 incName (Defined x _) n = Defined x (getNameNum n + 1)
+incName (ConName x _ s a) n = ConName x (getNameNum n + 1) s a

src/Elab/WiredIn.hs

@@ -17,13 +17,14 @@ import Data.Typeable
 
 import Elab.Eval
 
+import GHC.Stack (HasCallStack)
+
 import qualified Presyntax.Presyntax as P
 
+import Syntax.Pretty (prettyTm)
 import Syntax
 
 import System.IO.Unsafe
-import Syntax.Pretty (prettyTm)
-import GHC.Stack (HasCallStack)
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -40,8 +41,6 @@ wiType WiPathP    = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
 wiType WiIsOne    = VI ~> VTypeω
 wiType WiItIsOne  = VIsOne VI1
-wiType WiIsOne1   = forAll VI \i -> forAll VI \j -> VIsOne i ~> VIsOne (ior i j)
-wiType WiIsOne2   = forAll VI \i -> forAll VI \j -> VIsOne j ~> VIsOne (ior i j)
 
 wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
@@ -59,11 +58,6 @@ wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T"
 -- {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 WiBool   = VType
-wiType WiTrue   = VBool
-wiType WiFalse  = VBool
-wiType WiIf     = dprod' "A" (VBool ~> VType) \a -> a @@ VTt ~> a @@ VFf ~> dprod' "b" VBool \b -> a @@ b
-
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
 wiValue WiPretype  = VTypeω
@@ -79,8 +73,6 @@ wiValue WiPathP     = fun \a -> fun \x -> fun \y -> VPath a x y
 
 wiValue WiIsOne   = fun VIsOne
 wiValue WiItIsOne = VItIsOne
-wiValue WiIsOne1  = forallI \_ -> forallI \_ -> fun VIsOne1
-wiValue WiIsOne2  = forallI \_ -> forallI \_ -> fun VIsOne2
 
 wiValue WiPartial  = fun \phi -> fun \r -> VPartial phi r
 wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
@@ -93,11 +85,6 @@ wiValue WiGlue     = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a ph
 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 WiBool   = VBool
-wiValue WiTrue   = VTt
-wiValue WiFalse  = VFf
-wiValue WiIf     = fun \a -> fun \b -> fun \c -> fun \d -> elimBool a b c d
-
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
 infixr 7 ~>
@@ -142,8 +129,6 @@ wiredInNames = Map.fromList
 
   , ("IsOne", WiIsOne)
   , ("itIs1", WiItIsOne)
-  , ("isOneL", WiIsOne1)
-  , ("isOneR", WiIsOne2)
 
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
@@ -155,11 +140,6 @@ wiredInNames = Map.fromList
   , ("Glue", WiGlue)
   , ("glue", WiGlueElem)
   , ("unglue", WiUnglue)
-
-  , ("Bool", WiBool)
-  , ("true", WiTrue)
-  , ("false", WiFalse)
-  , ("if", WiIf)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -215,6 +195,7 @@ 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 x xs -> VCase x (fmap (fmap (flip (ielim line left right) i)) xs)
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
 outS :: NFSort -> NFEndp -> Value -> Value -> Value
@@ -228,7 +209,7 @@ outS a phi u  (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
 outS _ _ _ v             = error $ "can't outS " ++ show (prettyTm (quote v))
 
 -- Composition
-comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
+comp :: NFLine -> NFEndp -> Value -> Value -> Value
 comp _ VI1 u _ = u @@ VI1 @@ VItIsOne
 comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
   case force $ a @@ VVar (Bound (T.pack "i") 0) of
@@ -253,7 +234,7 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> 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 
+       in
          VPair c1 c2
 
     VPath{} ->
@@ -312,11 +293,40 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
     VType -> VGlueTy a0 phi (system \_ _ -> mkVSystem (Map.fromList [(phi, u @@ VI1 @@ VItIsOne)]))
                             (system \_ _  -> mkVSystem (Map.fromList [(phi, makeEquiv (\j -> (u @@ inot j)))]))
 
-    -- fibrancy structure of the booleans is trivial
-    VBool{} -> a0
+    VNe HData{} args ->
+      case force a0 of
+        VNe (HCon con_type con_name) con_args ->
+          VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u
+        _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
 
     _ -> VComp a phi u (VInc (a @@ VI0) phi 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') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
+    | otherwise = assert (p == p') $
+      let fill = makeFiller nargs dom phi u y
+       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 (Bound _ (negate -> 10))) args) phi u a0 =
+    fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
+  makeFiller _ _ _ _ a0 = fun (const a0)
+
+  makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
+  makeDomain _ = error "somebody smuggled something that smells"
+
+  smuggle x = VNe (HData (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x))
+
 compOutS :: NFSort -> NFEndp -> Value -> Value -> Value
 compOutS a b c d = compOutS a b c (force d) where
   compOutS _ _hi _0 vl@VComp{}    = vl
@@ -412,10 +422,3 @@ makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem m
         ielim (fun (const a)) y y (vProj2 u) (iand i j)
 
   id_fiber y = VPair y (VLine a y y (fun (const y)))
-
-elimBool :: NFSort -> Value -> Value -> Value -> Value
-elimBool prop x y bool =
-  case force bool of
-    VTt -> x
-    VFf -> y
-    _ -> VIf prop x y bool

src/Elab/WiredIn.hs-boot

@@ -1,7 +1,6 @@
 module Elab.WiredIn where
 
 import Syntax
-import GHC.Stack
 
 wiType  :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
@@ -11,10 +10,8 @@ inot      :: NFEndp -> NFEndp
 ielim     :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
 
 outS :: NFSort -> NFEndp -> Value -> Value -> Value
-comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
+comp :: NFLine -> NFEndp -> Value -> Value -> Value
 
 glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
 glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
-unglue   :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
-
-elimBool :: NFSort -> Value -> Value -> Value -> Value
+unglue   :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value

src/Presyntax/Lexer.x

@@ -152,10 +152,12 @@ variableOrKeyword (AlexPn _ l c, _, s, _) size =
   case T.unpack text of
     "as" -> pure (Token TokAs l c)
     "in" -> pure (Token TokIn l c)
+    "data" -> pure (Token TokData l c)
 
     "postulate" -> laidOut TokPostulate l c
     "let"       -> laidOut TokLet l c
     "where"     -> laidOut TokWhere l c
+    "case"      -> laidOut TokCase l c
 
     _ -> pure (Token (TokVar text) l c)
 

src/Presyntax/Parser.y

@@ -59,6 +59,8 @@ import Debug.Trace
 
   'let'       { Token TokLet _ _ }
   'in'        { Token TokIn _ _ }
+  'data'      { Token TokData _ _ }
+  'case'      { Token TokCase _ _ }
   'where'     { Token TokWhere _ _ }
 
   '&&'        { Token TokAnd _ _ }
@@ -79,6 +81,7 @@ Exp :: { Expr }
 Exp
   : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
   | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
+  | '\\' 'case' START CaseList END       { span $1 $5 $ LamCase $4 }
   | '(' 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 }
@@ -142,11 +145,32 @@ LetList :: { [LetItem] }
   | LetItem             { [$1] }
   | LetItem ';' LetList { $1:$3 }
 
+CaseItem :: { (Pattern, Expr) }
+  : Pattern '->' Exp { ($1, $3) }
+  
+CaseList :: { [(Pattern, Expr)] }
+  : CaseItem                { [$1] }
+  | CaseItem Semis CaseList { $1:$3 }
+
+Pattern :: { Pattern }
+  : PatVarList { makePattern $1 }
+
+PatVarList :: { (Posn, Posn, [Text]) }
+  : var            { (startPosn $1, endPosn $1, [getVar $1]) }
+  | var PatVarList { case $2 of (_, end, xs) -> (startPosn $1, end, getVar $1:xs) }
+
 Statement :: { Statement }
   : VarList ':' Exp                  { spanSt $1 $3 $ Decl (thd $1) $3 }
   | var LhsList '=' Rhs              { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
   | '{-#' Pragma '#-}'               { spanSt $1 $3 $ $2 }
   | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 }
+  | 'data' var Parameters ':' Exp 'where' START Postulates END
+    { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 }
+
+Parameters :: { [(Text, Plicity, Expr)] }
+  : {- empty -}                    { [] }
+  | '(' var ':' Exp ')' Parameters { (getVar $2, Ex, $4):$6 }
+  | '{' var ':' Exp '}' Parameters { (getVar $2, Im, $4):$6 }
 
 Rhs :: { Expr }
   : Exp                           { $1 }
@@ -242,10 +266,12 @@ instance HasPosn (Posn, Posn, a) where
 thd :: (a, b, c) -> c
 thd (x, y, z) = z
 
-
 span s e ex = Span ex (startPosn s) (endPosn e)
 spanSt s e ex = SpanSt ex (startPosn s) (endPosn e)
 
 getVar (Token (TokVar s) _ _) = s
 getVar _ = error "getVar non-var"
+
+makePattern (_, _, [x]) = PCap x
+makePattern (_, _, (x:xs)) = PCon x xs
 }

src/Presyntax/Presyntax.hs

@@ -21,6 +21,7 @@ data Expr
   | Proj2 Expr
 
   | LamSystem [(Condition, Expr)]
+  | LamCase [(Pattern, Expr)]
   | Let [LetItem] Expr
 
   | Span Expr Posn Posn
@@ -44,6 +45,11 @@ data Formula
   | FBot
   deriving (Eq, Show, Ord)
 
+data Pattern
+  = PCon Text [Text]
+  | PCap Text
+  deriving (Eq, Show, Ord)
+
 data Statement
   = Decl    [Text] Expr
   | Defn    Text Expr
@@ -54,6 +60,8 @@ data Statement
   | ReplNf Expr -- REPL eval
   | ReplTy Expr -- REPL :t
 
+  | Data Text [(Text, Plicity, Expr)] Expr [(Text, Expr)]
+
   | SpanSt Statement Posn Posn
   deriving (Eq, Show, Ord)
 

src/Presyntax/Tokens.hs

@@ -44,7 +44,10 @@ data TokenClass
 
   | TokAs
   | TokWhere
+  | TokCase
+
   | TokPostulate
+  | TokData
 
   | TokSemi
   deriving (Eq, Show, Ord)
@@ -80,6 +83,8 @@ tokSize TokIn = 2
 tokSize TokLStart = 0
 tokSize TokLEnd = 0
 tokSize TokWhere = length "where"
+tokSize TokData = length "data"
+tokSize TokCase = length "case"
 tokSize TokPostulate = length "postulate"
 
 data Token

src/Syntax.hs

@@ -3,6 +3,8 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 module Syntax where
 
+import Control.Arrow (Arrow(second))
+
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq
 import qualified Data.Set as Set
@@ -30,8 +32,6 @@ data WiredIn
 
   | WiIsOne   -- Proposition associated with an element of the interval
   | WiItIsOne -- 1 = 1
-  | WiIsOne1  -- i j -> [i] -> [ior i j]
-  | WiIsOne2  -- i j -> [j] -> [ior i j]
 
   | WiPartial  -- (φ : I) -> Type           -> Typeω
   | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
@@ -47,15 +47,12 @@ data WiredIn
   | 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
-
-  | WiBool
-  | WiTrue
-  | WiFalse
-  | WiIf
   deriving (Eq, Show, Ord)
 
 data Term
   = Ref  Name
+  | Con  Name
+  | Data Name
   | App  Plicity Term Term
   | Lam  Plicity Name Term
   | Pi   Plicity Name Term Term
@@ -84,8 +81,6 @@ data Term
   --   ~~~~~~~~~ not printed at all
 
   | IsOne Term
-  | IsOne1 Term
-  | IsOne2 Term
   | ItIsOne
 
   | Partial  Term Term
@@ -103,8 +98,7 @@ data Term
   | Glue Term Term Term Term Term Term
   | Unglue Term Term Term Term Term
 
-  -- ugly. TODO: proper inductive types
-  | Bool | Tt | Ff | If Term Term Term Term
+  | Case Term [(Term, Term)]
   deriving (Eq, Show, Ord, Data)
 
 data MV =
@@ -130,7 +124,14 @@ instance Data MV where
 data Name
   = Bound   {getNameText :: Text, getNameNum :: !Int}
   | Defined {getNameText :: Text, getNameNum :: !Int}
-  deriving (Eq, Show, Ord, Data)
+  | ConName {getNameText :: Text, getNameNum :: !Int, conSkip :: !Int, conArity :: !Int}
+  deriving (Show, Data)
+
+instance Eq Name where
+  x == y = getNameText x == getNameText y && getNameNum x == getNameNum y
+
+instance Ord Name where
+  compare x y = getNameText x `compare` getNameText y <> getNameNum x `compare` getNameNum y
 
 type NFType = Value
 type NFEndp = Value
@@ -160,8 +161,6 @@ data Value
 
   | VIsOne NFEndp
   | VItIsOne
-  | VIsOne1 NFEndp
-  | VIsOne2 NFEndp
 
   | VPartial  NFEndp Value
   | VPartialP NFEndp Value
@@ -176,10 +175,7 @@ data Value
   | VGlue   NFSort NFEndp NFPartial NFPartial NFPartial Value
   | VUnglue NFSort NFEndp NFPartial NFPartial Value
 
-  | VBool
-  | VTt
-  | VFf
-  | VIf Value Value Value Value
+  | VCase Value [(Term, Value)]
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
@@ -187,8 +183,10 @@ pattern VVar x = VNe (HVar x) Seq.Empty
 
 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 (HVar v)   = Ref v
+  goHead (HMeta m)  = Meta m
+  goHead (HCon _ v) = Con v
+  goHead (HData v)  = Data 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)
@@ -232,8 +230,6 @@ quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names
 quoteWith names (VLine p x y f)  = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
 
 quoteWith names (VIsOne v)  = IsOne (quoteWith names v)
-quoteWith names (VIsOne1 v) = IsOne1 (quoteWith names v)
-quoteWith names (VIsOne2 v) = IsOne2 (quoteWith names v)
 quoteWith _     VItIsOne    = ItIsOne
 
 quoteWith names (VPartial x y)  = Partial (quoteWith names x) (quoteWith names y)
@@ -247,15 +243,10 @@ quoteWith names (VGlueTy a phi t e)    = GlueTy (quoteWith names a) (quoteWith n
 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 _ames VBool         = Bool
-quoteWith _ames VTt           = Tt
-quoteWith _ames VFf           = Ff
-quoteWith names (VIf a b c d) = If (quoteWith names a) (quoteWith names b) (quoteWith names c) (quoteWith names d)
+quoteWith names (VCase v xs) = Case (quoteWith names v) (map (second (quoteWith names)) xs)
 
 alwaysShort :: Value -> Bool
-alwaysShort VBool{} = True
-alwaysShort VTt{} = True
-alwaysShort VFf{} = True
+alwaysShort (VNe HCon{} _) = True
 alwaysShort VVar{} = True
 alwaysShort _ = False
 
@@ -288,8 +279,35 @@ instance Ord Closure where
 
 data Head
   = HVar Name
+  | HCon Value Name
   | HMeta MV
-  deriving (Eq, Show, Ord)
+  | HData Name
+  deriving (Show)
+
+instance Eq Head where
+  HVar x == HVar y = x == y
+  HCon _ x == HCon _ y = x == y
+  HMeta x == HMeta y = x == y
+  HData x == HData y = x == y
+  _ == _ = False
+
+instance Ord Head where
+  compare x y =
+    case x of
+      HVar n -> case y of
+        HVar n' -> compare n n'
+        _ -> LT
+      HCon _ n -> case y of
+        HVar _ -> GT
+        HCon _ n' -> compare n n'
+        _ -> LT
+      HMeta n -> case y of
+        HMeta n' -> compare n n'
+        HData _ -> LT
+        _ -> GT
+      HData n -> case y of
+        HData n' -> compare n n'
+        _ -> GT
 
 data Projection
   = PApp   Plicity Value
@@ -297,4 +315,4 @@ data Projection
   | PProj1
   | PProj2
   | POuc   NFSort NFEndp Value
-  deriving (Eq, Show, Ord)
+  deriving (Eq, Show, Ord)

src/Syntax/Pretty.hs

@@ -21,8 +21,7 @@ import Prettyprinter
 import Syntax
 
 instance Pretty Name where
-  pretty (Bound x _)   = pretty x
-  pretty (Defined x _) = pretty x
+  pretty = pretty . getNameText
 
 prettyTm :: Term -> Doc AnsiStyle
 prettyTm = prettyTm . everywhere (mkT beautify) where
@@ -30,6 +29,8 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
     case T.uncons (getNameText v) of
       Just ('.', w) -> keyword (pretty w)
       _ -> pretty v
+  prettyTm (Con v) = keyword (pretty v)
+  prettyTm (Data v) = operator (pretty v)
 
   prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
   prettyTm (App Ex f x) = parenFun f <+> parenArg x
@@ -75,21 +76,19 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
   prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
     go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
 
+  prettyTm (Case x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (prettyCase xs)
+
   prettyTm x = error (show x)
 
+  prettyCase = vsep . map go where
+    go (x, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs
+
   beautify (PathP l x y)       = toFun "PathP" [l, x, y]
   beautify (IElim _ _ _ f i)   = App Ex f i
   beautify (PathIntro _ _ _ f) = f
 
   beautify (IsOne phi)  = toFun "IsOne" [phi]
   beautify ItIsOne      = Ref (Bound (T.pack ".1=1") 0)
-  beautify (IsOne1 phi) = toFun "isOne1" [phi]
-  beautify (IsOne2 phi) = toFun "isOne2" [phi]
-
-  beautify Bool         = Ref (Bound (T.pack ".Bool") 0)
-  beautify Tt           = Ref (Bound (T.pack ".true") 0)
-  beautify Ff           = Ref (Bound (T.pack ".false") 0)
-  beautify (If a b c d) = toFun "if" [a, b, c, d]
 
   beautify (Lam Ex v (App Ex f (Ref v')))
     | v == v', v `Set.notMember` freeVars f = f
@@ -119,8 +118,6 @@ parenArg :: Term -> Doc AnsiStyle
 parenArg x@App{} = parens (prettyTm x)
 parenArg x@IElim{} = parens (prettyTm x)
 parenArg x@IsOne{} = parens $ prettyTm x
-parenArg x@IsOne1{} = parens $ prettyTm x
-parenArg x@IsOne2{} = parens $ prettyTm x
 parenArg x@Partial{} = parens $ prettyTm x
 parenArg x@PartialP{} = parens $ prettyTm x
 
@@ -161,6 +158,8 @@ 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 Data{} = mempty
 freeVars Type{} = mempty
 freeVars Typeω{} = mempty
 freeVars I{} = mempty
@@ -177,8 +176,6 @@ 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 (IsOne1 a) = Set.unions $ map freeVars [a]
-freeVars (IsOne2 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]
@@ -191,7 +188,4 @@ freeVars (Comp 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 Bool{} = mempty
-freeVars Tt{} = mempty
-freeVars Ff{} = mempty
-freeVars (If x y z a) = Set.unions $ map freeVars [x, y, z, a]
+freeVars (Case x y) = freeVars x <> foldMap (freeVars . snd) y