natural numbers

lib/Quox/Equal.idr

@@ -61,6 +61,9 @@ isTyCon (Enum  {}) = True
 isTyCon (Tag   {}) = False
 isTyCon (Eq    {}) = True
 isTyCon (DLam  {}) = False
+isTyCon Nat        = True
+isTyCon Zero       = False
+isTyCon (Succ  {}) = False
 isTyCon (E     {}) = True
 isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
@@ -79,6 +82,8 @@ sameTyCon (Enum {}) (Enum {}) = True
 sameTyCon (Enum {}) _         = False
 sameTyCon (Eq   {}) (Eq   {}) = True
 sameTyCon (Eq   {}) _         = False
+sameTyCon Nat       Nat       = True
+sameTyCon Nat       _         = False
 sameTyCon (E    {}) (E    {}) = True
 sameTyCon (E    {}) _         = False
 
@@ -107,6 +112,9 @@ parameters (defs : Definitions' q g)
       Tag  {}         => pure False
       Eq   {}         => pure True
       DLam {}         => pure False
+      Nat             => pure False
+      Zero            => pure False
+      Succ {}         => pure False
       E    (s :# _)   => isSubSing s
       E    _          => pure False
 
@@ -218,6 +226,31 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
         -- Γ ⊢ e = f : Eq [i ⇒ A] s t
         pure ()
 
+      compare0' ctx Nat s t = local {mode := Equal} $
+        case (s, t) of
+          -- ---------------
+          --  Γ ⊢ 0 = 0 : ℕ
+          (Zero, Zero) => pure ()
+
+          --      Γ ⊢ m = n : ℕ
+          -- -------------------------
+          --  Γ ⊢ succ m = succ n : ℕ
+          (Succ m, Succ n) => compare0 ctx Nat m n
+
+          (E e, E f) => Elim.compare0 ctx e f
+
+          (Zero,   Succ _) => clashT ctx Nat s t
+          (Zero,   E _)    => clashT ctx Nat s t
+          (Succ _, Zero)   => clashT ctx Nat s t
+          (Succ _, E _)    => clashT ctx Nat s t
+          (E _,    Zero)   => clashT ctx Nat s t
+          (E _,    Succ _) => clashT ctx Nat s t
+
+          (Zero,   t) => wrongType ctx Nat t
+          (Succ _, t) => wrongType ctx Nat t
+          (E _,    t) => wrongType ctx Nat t
+          (s,      _) => wrongType ctx Nat s
+
       compare0' ctx ty@(E _) s t = do
         -- a neutral type can only be inhabited by neutral values
         -- e.g. an abstract value in an abstract type, bound variables, …
@@ -290,6 +323,11 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       -- a runtime coercion
       unless (tags1 == tags2) $ clashTy ctx s t
 
+    compareType' ctx Nat Nat =
+      -- ------------
+      --  Γ ⊢ ℕ <: ℕ
+      pure ()
+
     compareType' ctx (E e) (E f) = do
       -- no fanciness needed here cos anything other than a neutral
       -- has been inlined by whnf
@@ -311,6 +349,7 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
       pure $ sub1 res (s :# arg)
     computeElimType ctx (CasePair {pair, ret, _}) _ = pure $ sub1 ret pair
     computeElimType ctx (CaseEnum {tag, ret, _}) _ = pure $ sub1 ret tag
+    computeElimType ctx (CaseNat {nat, ret, _}) _ = pure $ sub1 ret nat
     computeElimType ctx (f :% p) ne = do
       (ty, _, _) <- expectEqE defs ctx !(computeElimType ctx f (noOr1 ne))
       pure $ dsub1 ty p
@@ -401,6 +440,21 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, IsQty q)}
             Nothing  => throwError $ TagNotIn t (fromList $ keys arms)
       compare0' ctx e@(CaseEnum {}) f _ _ = clashE ctx e f
 
+      compare0' ctx (CaseNat epi epi' e eret ezer esuc)
+                    (CaseNat fpi fpi' f fret fzer fsuc) ne nf =
+        local {mode := Equal} $ do
+          compare0 ctx e f
+          ety <- computeElimType ctx e (noOr1 ne)
+          compareType (extendTy zero eret.name ety ctx) eret.term fret.term
+          compare0 ctx (sub1 eret (Zero :# Nat)) ezer fzer
+          let [< p, ih] = esuc.names
+          compare0 (extendTyN [< (epi, p, Nat), (epi', ih, eret.term)] ctx)
+                   (weakT eret.term)
+                   esuc.term fsuc.term
+          expectEqualQ epi  fpi
+          expectEqualQ epi' fpi'
+      compare0' ctx e@(CaseNat {}) f _ _ = clashE ctx e f
+
       compare0' ctx (s :# a) (t :# b) _ _ =
           Term.compare0 ctx !(bigger a b) s t
         where

lib/Quox/Parser/FromParser.idr

@@ -14,6 +14,8 @@ import public Control.Monad.Reader
 import System.File
 import System.Path
 
+%hide Context.(<$>)
+%hide Context.(<*>)
 
 public export
 0 Defs : Type
@@ -118,6 +120,17 @@ mutual
         <*> fromPTermTScope ds ns [< r] ret
         <*> assert_total fromPTermEnumArms ds ns arms
 
+    Nat => pure Nat
+    Zero => pure Zero
+    Succ n => [|Succ $ fromPTermWith ds ns n|]
+
+    Case pi nat (r, ret) (CaseNat zer (s, pi', ih, suc)) =>
+      Prelude.map E $ Base.CaseNat pi pi'
+        <$> fromPTermElim ds ns nat
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> fromPTermWith ds ns zer
+        <*> fromPTermTScope ds ns [< s, ih] suc
+
     Enum strs =>
       let set = SortedSet.fromList strs in
       if length strs == length (SortedSet.toList set) then

lib/Quox/Parser/Lexer.idr

@@ -195,6 +195,8 @@ reserved =
    Word "δ" `Or` Word "dfun",
    Word "ω" `Or` Sym "#",
    Sym "★" `Or` Word "Type",
+   Word "ℕ" `Or` Word "Nat",
+   Word1 "zero", Word1 "succ",
    Word1 "def",
    Word1 "def0",
    Word "defω" `Or` Word "def#",

lib/Quox/Parser/Parser.idr

@@ -116,6 +116,10 @@ qty = terminal "expecting quantity" $
   \case Nat 0 => Just Zero; Nat 1 => Just One; Reserved "ω" => Just Any
         _ => Nothing
 
+export
+zero : Grammar True ()
+zero = terminal "expecting 0" $ guard . (== Nat 0)
+
 
 public export
 AllReserved : List (a, String) -> Type
@@ -125,6 +129,7 @@ export
 symbols : (lst : List (a, String)) -> (0 _ : AllReserved lst) =>
           Grammar True a
 symbols []                 = fail "no symbols found"
+symbols [(x, str)]         = x <$ res str
 symbols ((x, str) :: rest) = x <$ res str <|> symbols rest
 
 export
@@ -185,11 +190,24 @@ mutual
   caseBody : Grammar True PCaseBody
   caseBody = braces $
         [|CasePair (pairPat <* darr) (term <* optSemi)|]
+    <|> CaseNat <$> zeroCase <* resC ";" <*> succCase <* optSemi
+    <|> flip CaseNat <$> succCase <* resC ";" <*> zeroCase <* optSemi
     <|> [|CaseEnum $ semiSep [|MkPair tag (darr *> term)|]|]
   where
     optSemi = optional $ res ";"
     pairPat = parens [|MkPair bname (resC "," *> bname)|]
 
+    zeroCase : Grammar True PTerm
+    zeroCase = (resC "zero" <|> zero) *> darr *> term
+
+    succCase : Grammar True (BName, PQty, BName, PTerm)
+    succCase = do
+      resC "succ"
+      n   <- bname
+      ih  <- option (Zero, Nothing) $ bracks [|MkPair qty (resC "." *> bname)|]
+      rhs <- darr *> term
+      pure $ (n, fst ih, snd ih, rhs)
+
   private covering
   bindTerm : Grammar True PTerm
   bindTerm = pi <|> sigma
@@ -199,7 +217,7 @@ mutual
     pi, sigma : Grammar True PTerm
     pi = [|makePi (qty <* res ".") domain (resC "→" *> term)|]
     where
-      makePi : Three -> (BName, PTerm) -> PTerm -> PTerm
+      makePi : PQty -> (BName, PTerm) -> PTerm -> PTerm
       makePi q (x, s) t = Pi q x s t
       domain = binderHead <|> [|(Nothing,) aTerm|]
 
@@ -228,6 +246,7 @@ mutual
   appTerm : Grammar True PTerm
   appTerm = resC "★"    *> [|TYPE nat|]
         <|> resC "Eq"   *> [|Eq (bracks optBinderTerm) aTerm aTerm|]
+        <|> resC "succ" *> [|Succ aTerm|]
         <|> [|apply aTerm (many appArg)|]
   where
     data PArg = TermArg PTerm | DimArg PDim
@@ -245,9 +264,16 @@ mutual
   aTerm : Grammar True PTerm
   aTerm = [|Enum $ braces $ commaSep bareTag|]
       <|> [|TYPE universe|]
+      <|> Nat  <$ resC "ℕ"
+      <|> Zero <$ resC "zero"
+      <|> (nat <&> \n => fromNat n :# Nat)
       <|> [|V name|]
       <|> [|Tag tag|]
       <|> foldr1 Pair <$> parens (commaSep1 term)
+  where
+    fromNat : Nat -> PTerm
+    fromNat 0     = Zero
+    fromNat (S k) = Succ $ fromNat k
 
   private covering
   optBinderTerm : Grammar True (BName, PTerm)

lib/Quox/Parser/Syntax.idr

@@ -51,6 +51,9 @@ namespace PTerm
       | DLam BName PTerm
       | (:%) PTerm PDim
 
+      | Nat
+      | Zero | Succ PTerm
+
       | V PName
       | (:#) PTerm PTerm
     %name PTerm s, t
@@ -59,6 +62,7 @@ namespace PTerm
     data PCaseBody =
         CasePair (BName, BName) PTerm
       | CaseEnum (List (TagVal, PTerm))
+      | CaseNat PTerm (BName, PQty, BName, PTerm)
     %name PCaseBody body
 
 %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show]
@@ -143,6 +147,9 @@ mutual
            (toPTermWith ds ns l) (toPTermWith ds ns r)
       DLam (S [< i] body) =>
         DLam (Just $ show i) $ toPTermWith (ds :< baseStr i) ns body.term
+      Nat => Nat
+      Zero => Zero
+      Succ n => Succ $ toPTermWith ds ns n
       E e =>
         toPTermWith ds ns e
 
@@ -172,8 +179,14 @@ mutual
                 toPTermWith ds (ns :< baseStr x :< baseStr y) body.term)
       CaseEnum qty tag (S [< r] ret) arms =>
         Case qty (toPTermWith ds ns tag)
-             (Just $ show r, toPTermWith ds (ns :< baseStr r) ret.term)
+             (Just $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term)
              (CaseEnum $ mapSnd (toPTermWith ds ns) <$> SortedMap.toList arms)
+      CaseNat qtyNat qtyIH nat (S [< r] ret) zer (S [< p, ih] suc) =>
+        Case qtyNat (toPTermWith ds ns nat)
+             (Just $ baseStr r, toPTermWith ds (ns :< baseStr r) ret.term)
+             (CaseNat (toPTermWith ds ns zer)
+                      (Just $ baseStr p, qtyIH, Just $ baseStr ih,
+                       toPTermWith ds (ns :< baseStr p :< baseStr ih) suc.term))
       fun :% arg =>
         toPTermWith ds ns fun :% toPDimWith ds arg
       tm :# ty =>

lib/Quox/Reduce.idr

@@ -66,6 +66,12 @@ isTagHead : Elim {} -> Bool
 isTagHead (Tag t :# Enum _) = True
 isTagHead _ = False
 
+public export %inline
+isNatHead : Elim {} -> Bool
+isNatHead (Zero   :# Nat) = True
+isNatHead (Succ n :# Nat) = True
+isNatHead _ = False
+
 public export %inline
 isE : Term {} -> Bool
 isE (E _) = True
@@ -89,6 +95,8 @@ mutual
     isRedexE defs pair || isPairHead pair
   isRedexE defs (CaseEnum {tag, _}) =
     isRedexE defs tag || isTagHead tag
+  isRedexE defs (CaseNat {nat, _}) =
+    isRedexE defs nat || isNatHead nat
   isRedexE defs (f :% _) =
     isRedexE defs f || isDLamHead f
   isRedexE defs (t :# a) =
@@ -148,6 +156,21 @@ mutual
         Right nt =>
           pure $ Element (CaseEnum pi tag ret arms) $ tagnf `orNo` nt
 
+    whnf defs (CaseNat pi piIH nat ret zer suc) = do
+      Element nat natnf <- whnf defs nat
+      case nchoose $ isNatHead nat of
+        Left _ =>
+          let ty = sub1 ret nat in
+          case nat of
+            Zero :# Nat => whnf defs (zer :# ty)
+            Succ n :# Nat =>
+              let nn = n :# Nat
+                  tm = subN suc [nn, CaseNat pi piIH nn ret zer suc]
+              in
+              whnf defs $ tm :# ty
+        Right nn =>
+          pure $ Element (CaseNat pi piIH nat ret zer suc) $ natnf `orNo` nn
+
     whnf defs (f :% p) = do
       Element f fnf <- whnf defs f
       case nchoose $ isDLamHead f of
@@ -181,6 +204,9 @@ mutual
     whnf _ t@(Tag  {}) = pure $ nred t
     whnf _ t@(Eq   {}) = pure $ nred t
     whnf _ t@(DLam {}) = pure $ nred t
+    whnf _    Nat      = pure $ nred Nat
+    whnf _    Zero     = pure $ nred Zero
+    whnf _ t@(Succ {}) = pure $ nred t
 
     whnf defs (E e) = do
       Element e enf <- whnf defs e

lib/Quox/Syntax/Term/Base.idr

@@ -75,6 +75,12 @@ mutual
     ||| equality term
     DLam : (body : DScopeTerm q d n) -> Term q d n
 
+    ||| natural numbers (temporary until 𝐖 gets added)
+    Nat  : Term q d n
+    -- [todo] can these be elims?
+    Zero : Term q d n
+    Succ : (p : Term q d n) -> Term q d n
+
     ||| elimination
     E : (e : Elim q d n) -> Term q d n
 
@@ -111,6 +117,13 @@ mutual
                (arms : CaseEnumArms q d n) ->
                Elim q d n
 
+    ||| nat matching
+    CaseNat : (qty, qtyIH : q) -> (nat : Elim q d n) ->
+              (ret : ScopeTerm q d n) ->
+              (zero : Term q d n) ->
+              (succ : ScopeTermN 2 q d n) ->
+              Elim q d n
+
     ||| dim application
     (:%) : (fun : Elim q d n) -> (arg : Dim d) -> Elim q d n
 

lib/Quox/Syntax/Term/Pretty.idr

@@ -11,8 +11,8 @@ import Data.Vect
 %default total
 
 
-private %inline
+export %inline
-typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD :
+typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD :
   Pretty.HasEnv m => m (Doc HL)
 typeD   = hlF Syntax $ ifUnicode "★" "Type"
 arrowD  = hlF Syntax $ ifUnicode "→" "->"
@@ -22,9 +22,10 @@ lamD    = hlF Syntax $ ifUnicode "λ" "fun"
 eqndD   = hlF Syntax $ ifUnicode "≡" "=="
 dlamD   = hlF Syntax $ ifUnicode "δ" "dfun"
 annD    = hlF Syntax $ ifUnicode "∷" "::"
+natD    = hlF Syntax $ ifUnicode "ℕ" "Nat"
 
-private %inline
+export %inline
-eqD, colonD, commaD, caseD, returnD, ofD, dotD : Doc HL
+eqD, colonD, commaD, caseD, returnD, ofD, dotD, zeroD, succD : Doc HL
 eqD     = hl Syntax "Eq"
 colonD  = hl Syntax ":"
 commaD  = hl Syntax ","
@@ -32,6 +33,8 @@ caseD   = hl Syntax "case"
 ofD     = hl Syntax "of"
 returnD = hl Syntax "return"
 dotD    = hl Delim "."
+zeroD   = hl Syntax "zero"
+succD   = hl Syntax "succ"
 
 
 export
@@ -157,6 +160,16 @@ export
 prettyTagBare : TagVal -> Doc HL
 prettyTagBare t = hl Tag $ quoteTag t
 
+export
+toNatLit : Term q d n -> Maybe Nat
+toNatLit Zero     = Just 0
+toNatLit (Succ n) = [|S $ toNatLit n|]
+toNatLit _        = Nothing
+
+private
+eterm : Term q d n -> Exists (Term q d)
+eterm = Evidence n
+
 
 parameters (showSubsts : Bool)
  mutual
@@ -201,6 +214,14 @@ parameters (showSubsts : Bool)
     prettyM (DLam (S i t)) =
       let GotDLams {names, body, _} = getDLams' i t.term Refl in
       prettyLams (Just !dlamD) D (toSnocList' names) body
+    prettyM Nat = natD
+    prettyM Zero = pure $ hl Syntax "0"
+    prettyM (Succ n) =
+      case toNatLit n of
+        Just n  => pure $ hl Syntax $ pretty $ S n
+        Nothing => do
+          n <- withPrec Arg $ prettyM n
+          parensIfM App $ succD <++> n
     prettyM (E e) = prettyM e
     prettyM (CloT s th) =
       if showSubsts then
@@ -231,6 +252,14 @@ parameters (showSubsts : Bool)
     prettyM (CaseEnum pi t (S [< r] ret) arms) =
       prettyCase pi t r ret.term
         [([<], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
+    prettyM (CaseNat pi pi' nat (S [< r] ret) zer (S [< s, ih] suc)) =
+      prettyCase pi nat r ret.term
+        [([<],       zeroD,    eterm zer),
+         ([< s, ih], !succPat, eterm suc.term)]
+      where
+        succPat : m (Doc HL)
+        succPat = pure $
+          hsep [succD, !(pretty0M s), bracks !(pretty0M $ MkWithQty pi' ih)]
     prettyM (e :% d) =
       let GotDArgs {fun, args, _} = getDArgs' e [d] in
       prettyApps (Just "@") fun args

lib/Quox/Syntax/Term/Subst.idr

@@ -268,6 +268,9 @@ mutual
       nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph)
     pushSubstsWith th ph (DLam body) =
       nclo $ DLam (body // th // ph)
+    pushSubstsWith _ _ Nat = nclo Nat
+    pushSubstsWith _ _ Zero = nclo Zero
+    pushSubstsWith th ph (Succ n) = nclo $ Succ $ n // th // ph
     pushSubstsWith th ph (E e) =
       let Element e nc = pushSubstsWith th ph e in nclo $ E e
     pushSubstsWith th ph (CloT s ps) =
@@ -291,6 +294,9 @@ mutual
     pushSubstsWith th ph (CaseEnum pi t r arms) =
       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
                (map (\b => b // th // ph) arms)
+    pushSubstsWith th ph (CaseNat pi pi' n r z s) =
+      nclo $ CaseNat pi pi' (n // th // ph) (r // th // ph)
+               (z // th // ph) (s // th // ph)
     pushSubstsWith th ph (f :% d) =
       nclo $ (f // th // ph) :% (d // th)
     pushSubstsWith th ph (s :# a) =

lib/Quox/Typechecker.idr

@@ -166,6 +166,16 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- then Ψ | Γ ⊢ σ · (δ i ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
+  check' ctx sg Nat ty = toCheckType ctx sg Nat ty
+
+  check' ctx sg Zero ty = do
+    expectNat !ask ctx ty
+    pure $ zeroFor ctx
+
+  check' ctx sg (Succ n) ty = do
+    expectNat !ask ctx ty
+    checkC ctx sg n Nat
+
   check' ctx sg (E e) ty = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx sg e
@@ -229,6 +239,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
   checkType' ctx t@(DLam {}) u =
     throwError $ NotType ctx t
 
+  checkType' ctx Nat u = pure ()
+  checkType' ctx Zero u = throwError $ NotType ctx Zero
+  checkType' ctx t@(Succ _) u = throwError $ NotType ctx t
+
   checkType' ctx (E e) u = do
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- inferC ctx szero e
@@ -328,6 +342,36 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
       else throwError $ BadCaseQtys ctx $
              map (\(qs, t, s) => (qs, Tag t, s)) lst
 
+  infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
+    -- if 1 ≤ π
+    expectCompatQ one pi
+    -- if Ψ | Γ ⊢ σ · n ⇒ ℕ ⊳ Σn
+    nres <- inferC ctx sg n
+    expectNat !ask ctx nres.type
+    -- if Ψ | Γ, n : ℕ ⊢₀ A ⇐ Type
+    checkTypeC (extendTy zero ret.name Nat ctx) ret.term Nothing
+    -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
+    zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
+    -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
+    -- with Σz = Σs, (ρ₁ + ρ₂) ≤ πσ
+    let [< p, ih] = suc.names
+        pisg      = pi * sg.fst
+        sucCtx    = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
+        sucType   = substCaseNatRet ret
+    sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
+    unless (zerout == sucout) $ do
+      let sucp = Succ $ FT $ unq p
+          suc  = subN suc [F $ unq ih, F $ unq p]
+      throwError $ BadCaseQtys ctx [(zerout, Zero, zer), (sucout, sucp, suc)]
+    expectCompatQ qih pi'
+    -- [fixme] better error here
+    expectCompatQ (qp + qih) pisg
+    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz
+    pure $ InfRes {
+      type = sub1 ret n,
+      qout = pi * nres.qout + zerout
+    }
+
   infer' ctx sg (fun :% dim) = do
     -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun

lib/Quox/Typing.idr

@@ -44,6 +44,10 @@ substCasePairRet dty retty =
   let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
   retty.term // (arg ::: shift 2)
 
+public export
+substCaseNatRet : ScopeTerm q d n -> Term q d (2 + n)
+substCaseNatRet retty = retty.term // (Succ (BVT 1) :# Nat ::: shift 2)
+
 
 parameters {auto _ : HasErr q m} (defs : Definitions' q _)
   export covering %inline
@@ -83,6 +87,12 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
       Eq {ty, l, r, _} => pure (ty, l, r)
       _                => throwError $ ExpectedEq ctx (s // th)
 
+    export covering %inline
+    expectNat_ : Term q d2 n -> m ()
+    expectNat_ s = case fst !(whnfT s) of
+      Nat => pure ()
+      _   => throwError $ ExpectedNat ctx (s // th)
+
 
   -- [fixme] refactor this stuff
 
@@ -117,6 +127,12 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
       let Val d = ctx.dimLen; Val n = ctx.termLen in
       expectEq_ ctx id
 
+    export covering %inline
+    expectNat : Term q d n -> m ()
+    expectNat =
+      let Val d = ctx.dimLen; Val n = ctx.termLen in
+      expectNat_ ctx id
+
 
   parameters (ctx : EqContext q n)
     export covering %inline
@@ -148,3 +164,9 @@ parameters {auto _ : HasErr q m} (defs : Definitions' q _)
     expectEqE t =
       let Val n = ctx.termLen in
       expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t
+
+    export covering %inline
+    expectNatE : Term q 0 n -> m ()
+    expectNatE t =
+      let Val n = ctx.termLen in
+      expectNat_ (toTyContext ctx) (shift0 ctx.dimLen) t

lib/Quox/Typing/Error.idr

@@ -17,6 +17,7 @@ data Error q
 | ExpectedSig  (TyContext q d n) (Term q d n)
 | ExpectedEnum (TyContext q d n) (Term q d n)
 | ExpectedEq   (TyContext q d n) (Term q d n)
+| ExpectedNat  (TyContext q d n) (Term q d n)
 | BadUniverse  Universe Universe
 | TagNotIn     TagVal (SortedSet TagVal)
 | BadCaseQtys  (TyContext q d n) (List (QOutput q n, Term q d n, Term q d n))
@@ -165,7 +166,7 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
 
   private
   dissectCaseQtys : TyContext q d n ->
-                    NContext n' -> List (QOutput q n', Term q d n, z) ->
+                    NContext n' -> List (QOutput q n', y, z) ->
                     List (Doc HL)
   dissectCaseQtys ctx [<]        arms = []
   dissectCaseQtys ctx (tel :< x) arms =
@@ -206,6 +207,9 @@ parameters {auto _ : (Eq q, IsQty q, PrettyHL q)} (unicode : Bool)
     ExpectedEq ctx s =>
       sep ["expected an equality type, but got", termt ctx s]
 
+    ExpectedNat ctx s =>
+      sep ["expected the type ℕ, but got", termt ctx s]
+
     BadUniverse k l =>
       sep ["the universe level", prettyUniverse k,
            "is not strictly less than", prettyUniverse l]

tests/TermImpls.idr

@@ -51,6 +51,15 @@ mutual
     DLam body1 == DLam body2 = body1.term == body2.term
     DLam {} == _ = False
 
+    Nat == Nat = True
+    Nat == _ = False
+
+    Zero == Zero = True
+    Zero == _ = False
+
+    Succ m == Succ n = m == n
+    Succ _ == _ = False
+
     E e == E f = e == f
     E _ == _ = False
 
@@ -85,6 +94,11 @@ mutual
       q1 == q2 && t1 == t2 && r1.term == r2.term && a1 == a2
     CaseEnum {} == _ = False
 
+    CaseNat q1 q1' n1 r1 z1 s1 == CaseNat q2 q2' n2 r2 z2 s2 =
+      q1 == q2 && q1' == q2' && n1 == n2 &&
+      r1.term == r2.term && z1 == z2 && s1.term == s2.term
+    CaseNat {} == _ = False
+
     (fun1 :% dim1) == (fun2 :% dim2) = fun1 == fun2 && dim1 == dim2
     (_ :% _) == _ = False
 

tests/Tests/Parser.idr

@@ -224,6 +224,15 @@ tests = "parser" :- [
     parseFails term "≡"
   ],
 
+  "naturals" :- [
+    parsesAs term "ℕ" Nat,
+    parsesAs term "Nat" Nat,
+    parsesAs term "zero" Zero,
+    parsesAs term "succ n" (Succ $ V "n"),
+    parsesAs term "3" (Succ (Succ (Succ Zero)) :# Nat),
+    parseFails term "succ"
+  ],
+
   "case" :- [
     parsesAs term
       "case1 f s return x ⇒ A x of { (l, r) ⇒ add l r }" $
@@ -251,7 +260,15 @@ tests = "parser" :- [
     parsesAs term "caseω t return A of {}" $
       Case Any (V "t") (Nothing, V "A") (CaseEnum []),
     parsesAs term "case# t return A of {}" $
-      Case Any (V "t") (Nothing, V "A") (CaseEnum [])
+      Case Any (V "t") (Nothing, V "A") (CaseEnum []),
+    parsesAs term "caseω n return A of { 0 ⇒ a; succ n' ⇒ b }" $
+      Case Any (V "n") (Nothing, V "A") $
+        CaseNat (V "a") (Just "n'", Zero, Nothing, V "b"),
+    parsesAs term "caseω n return ℕ of { succ _ [1.ih] ⇒ ih; zero ⇒ 0; }" $
+      Case Any (V "n") (Nothing, Nat) $
+        CaseNat (Zero :# Nat) (Nothing, One, Just "ih", V "ih"),
+    parseFails term "caseω n return A of { zero ⇒ a }",
+    parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
   ],
 
   "definitions" :- [

tests/Tests/Typechecker.idr

@@ -363,6 +363,18 @@ tests = "typechecker" :- [
       check_ empty01 sone (Tag "a") (enum ["b", "c"])
   ],
 
+  "enum matching" :- [
+    testTC "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'tt ⇒ 'tt } ⇒ {tt}" $
+      inferAs (ctx [< ("x", enum ["tt"])]) sone
+        (CaseEnum One (BV 0) (SN (enum ["tt"])) $
+          singleton "tt" (Tag "tt"))
+        (enum ["tt"]),
+    testTCFail "ω.x : {tt} ⊢ 1 · case1 x return {tt} of { 'ff ⇒ 'tt } ⇏" $
+      infer_ (ctx [< ("x", enum ["tt"])]) sone
+        (CaseEnum One (BV 0) (SN (enum ["tt"])) $
+          singleton "ff" (Tag "tt"))
+  ],
+
   "equalities" :- [
     testTC "1 · (δ i ⇒ a) ⇐ a ≡ a" $
       check_ empty sone (DLam $ SN $ FT "a")