some fixes to inductive types

intro.tt

@@ -682,11 +682,56 @@ pathIsHom {A} {B} {f} {g} =
     theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
   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)
+data Nat : Type where
+  zero : Nat
+  succ : Nat -> Nat
+
+data Int : Type where
+  pos : Nat -> Int
+  neg : Nat -> Int
+
+sucZ : Int -> Int
+sucZ = \case
+  pos n -> pos (succ n)
+  neg n ->
+    let suc_neg : Nat -> Int
+        suc_neg = \case
+          zero -> pos zero
+          succ n -> neg n
+     in suc_neg n
+
+predZ : Int -> Int
+predZ = \case
+  pos n ->
+    let pred_pos : Nat -> Int
+        pred_pos = \case
+          zero -> neg zero
+          succ n -> pos n
+     in pred_pos n
+  neg n -> neg (succ n)
+
+sucEquiv : isIso sucZ
+sucEquiv = 
+  let
+    sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
+    sucPredZ = \case
+      pos n ->
+        let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
+            k = \case
+              zero -> refl
+              succ n -> refl
+         in k n
+      neg n -> refl
+    predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
+    predSucZ = \case
+      pos n -> refl
+      neg n ->
+        let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
+            k = \case
+              zero -> refl
+              succ n -> refl
+         in k n
+   in (predZ, sucPredZ, predSucZ)
+
+intPath : Path Int Int
+intPath = univalence (IsoToEquiv (sucZ, sucEquiv))

src/Elab.hs

@@ -199,13 +199,12 @@ check (P.LamCase pats) ty = do
   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
+        checkPattern pat dom \pat wp pat_nf -> do
           rhs <- check rhs (rng pat_nf)
           pure (pat, wp rhs)
-      pure (wp (Lam P.Ex name (Case (Ref name) cases)))
+      let x = wp (Lam P.Ex name (Case (Ref name) cases))
+      pure x
     _ -> do
       dom <- newMeta VTypeω
       n <- newName' (Bound (T.singleton 'x') 0)
@@ -218,29 +217,29 @@ check exp ty = do
   wp <- isConvertibleTo has ty
   pure (wp tm)
 
-checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> ElabM a) -> ElabM a
+checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Value -> 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
+      (ty, wp) <- instantiate =<< getNfType name
+      unify ty dom
       wrap <- skipLams skip
-      cont (Con name) wrap
+      cont (Con name) wrap =<< eval (wp (Con name))
     Just name -> throwElab $ NotACon name
-    Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name)
+    Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) (VVar 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
+        (ty, wp) <- instantiate =<< getNfType name
         _ <- isConvertibleTo (skipBinders arity ty) dom
         skip <- skipLams nskip
-        bindNames args ty $ \_ wrap ->
-          cont (Con name) (skip . wrap)
+        bindNames args ty $ \names wrap ->
+          cont (Con name) (skip . wrap) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp (Con name)) names)
       Just name -> throwElab $ NotACon name
       _ -> throwElab $ NotInScope (Bound var 0)
   where
@@ -255,11 +254,12 @@ checkPattern (P.PCon var args) dom cont =
     bindNames [] _ k = k [] id
     bindNames xs t _ = error $ show (xs, t)
 
-instantiate :: NFType -> ElabM NFType
+instantiate :: NFType -> ElabM (NFType, Term -> Term)
 instantiate (VPi P.Im d (Closure _ k)) = do
   t <- newMeta d
-  instantiate (k t)
-instantiate x = pure x
+  (ty, w) <- instantiate (k t)
+  pure (ty, \inner -> App P.Im (w inner) (quote t))
+instantiate x = pure (x, id)
 
 skipLams :: Int -> ElabM (Term -> Term)
 skipLams 0 = pure id
@@ -445,18 +445,20 @@ checkStatement (P.ReplTy e) k = do
 
 checkStatement (P.Data name tele retk constrs) k =
   do
-    checkTeleRetk True tele retk \kind tele -> do
+    checkTeleRetk True tele retk \kind tele undef -> 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
+      defineInternal (Defined name 0) kind_nf (\name' -> VNe (HData name') mempty) \name' -> 
+        checkCons tele (VNe (HData name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
   where
     makeProj (x, p, _) = PApp p (VVar x)
 
+    markAsDef x e = e { definedNames = Set.insert x (definedNames e) }
+
     checkTeleRetk allKan [] retk cont = do
       t <- check retk VTypeω
       t_nf <- eval t
       when allKan $ unify t_nf VType
-      cont t []
+      cont t [] id
     checkTeleRetk allKan ((x, p, t):xs) retk cont = do
       (t, ty) <- infer t
       _ <- isConvertibleTo ty VTypeω
@@ -465,7 +467,8 @@ checkStatement (P.Data name tele retk constrs) k =
           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)
+      let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) }
+      assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
 
     checkCons _ _et [] k = k
 

src/Elab/Eval.hs

@@ -6,7 +6,6 @@
 {-# LANGUAGE TupleSections #-}
 module Elab.Eval where
 
-import Control.Arrow (Arrow(second))
 import Control.Monad.Reader
 import Control.Exception
 
@@ -114,7 +113,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 (VCase x xs) = VCase <$> zonkIO x <*> traverse (\(x, y) -> (x,) <$> zonkIO y) xs
+zonkIO (VCase x xs) = VCase <$> zonkIO x <*> pure xs
 
 zonkSp :: Projection -> IO Projection
 zonkSp (PApp p x) = PApp p <$> zonkIO x
@@ -203,12 +202,12 @@ eval' e (Let ns x) =
 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 _ 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)
+evalCase _ sc xs = VCase sc xs
 
 vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
@@ -489,7 +488,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 (VCase v xs) = checkScope s v *> traverse_ (checkScope s . snd) xs
+checkScope s (VCase v _) = checkScope s v
 
 checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
 checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)

src/Elab/WiredIn.hs

@@ -195,7 +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)
+        VCase x xs -> VCase x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
         _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
 
 outS :: NFSort -> NFEndp -> Value -> Value -> Value

src/Syntax.hs

@@ -3,8 +3,6 @@
 {-# 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
@@ -175,7 +173,7 @@ data Value
   | VGlue   NFSort NFEndp NFPartial NFPartial NFPartial Value
   | VUnglue NFSort NFEndp NFPartial NFPartial Value
 
-  | VCase Value [(Term, Value)]
+  | VCase Value [(Term, Term)]
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
@@ -243,7 +241,7 @@ 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 names (VCase v xs) = Case (quoteWith names v) (map (second (quoteWith names)) xs)
+quoteWith names (VCase v xs) = Case (quoteWith names v) xs
 
 alwaysShort :: Value -> Bool
 alwaysShort (VNe HCon{} _) = True

src/Syntax/Pretty.hs

@@ -39,7 +39,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
   prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
   prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
 
-  prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
+  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)
@@ -73,16 +73,20 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
   prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
   prettyTm (INot x) = operator (pretty '~') <> prettyTm x
 
-  prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
+  prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where
     go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
 
-  prettyTm (Case x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (prettyCase xs)
+  prettyTm (Case x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line)
+  prettyTm (Let xs e) = align $ keyword (pretty "let") <+> braces (line <> indent 2 (prettyLet xs) <> line) <+> keyword (pretty "in") <+> prettyTm e
 
   prettyTm x = error (show x)
 
-  prettyCase = vsep . map go where
+  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
@@ -126,6 +130,7 @@ 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