From 0514fff481882401a39e0d7c3eded96fa24cb1b7 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 2 Nov 2023 20:01:34 +0100
Subject: [PATCH] =?UTF-8?q?represent=20=E2=84=95=20constants=20directly?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

instead of as huge `succ (succ (succ ⋯))` terms
---
 lib/Quox/Displace.idr            |  2 +-
 lib/Quox/Equal.idr               | 28 +++++++++++++++-------------
 lib/Quox/FreeVars.idr            |  4 ++--
 lib/Quox/Parser/FromParser.idr   |  2 +-
 lib/Quox/Parser/Parser.idr       |  6 +++---
 lib/Quox/Parser/Syntax.idr       | 14 ++++++--------
 lib/Quox/Syntax/Term/Base.idr    | 14 ++++++--------
 lib/Quox/Syntax/Term/Pretty.idr  | 16 +++-------------
 lib/Quox/Syntax/Term/Subst.idr   |  4 ++--
 lib/Quox/Syntax/Term/Tighten.idr |  8 ++++----
 lib/Quox/Typechecker.idr         |  4 ++--
 lib/Quox/Untyped/Erase.idr       | 18 +++++++++---------
 lib/Quox/Untyped/Scheme.idr      |  8 +++-----
 lib/Quox/Untyped/Syntax.idr      | 24 ++++++------------------
 lib/Quox/Whnf/Interface.idr      | 23 ++++++++++++++++-------
 lib/Quox/Whnf/Main.idr           | 17 ++++++++++++++---
 tests/Tests/Equal.idr            |  4 ++--
 tests/Tests/Parser.idr           | 23 +++++++++--------------
 18 files changed, 104 insertions(+), 115 deletions(-)

diff --git a/lib/Quox/Displace.idr b/lib/Quox/Displace.idr
index 14a3ce5..3ac9907 100644
--- a/lib/Quox/Displace.idr
+++ b/lib/Quox/Displace.idr
@@ -28,7 +28,7 @@ parameters (k : Universe)
       Eq (doDisplaceDS ty) (doDisplace l) (doDisplace r) loc
     doDisplace (DLam body loc) = DLam (doDisplaceDS body) loc
     doDisplace (NAT loc) = NAT loc
-    doDisplace (Zero loc) = Zero loc
+    doDisplace (Nat n loc) = Nat n loc
     doDisplace (Succ p loc) = Succ (doDisplace p) loc
     doDisplace (STRING loc) = STRING loc
     doDisplace (Str s loc) = Str s loc
diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr
index 33892c1..7055181 100644
--- a/lib/Quox/Equal.idr
+++ b/lib/Quox/Equal.idr
@@ -279,27 +279,29 @@ namespace Term
   compare0' defs ctx sg nat@(NAT {}) s t = local_ Equal $
     case (s, t) of
       -- ---------------
-      --  Γ ⊢ 0 = 0 ⇐ ℕ
-      (Zero {}, Zero {}) => pure ()
+      --  Γ ⊢ n = n ⇐ ℕ
+      (Nat x {}, Nat y {}) => unless (x == y) $ clashT s.loc ctx nat s t
 
       --      Γ ⊢ s = t ⇐ ℕ
       -- -------------------------
       --  Γ ⊢ succ s = succ t ⇐ ℕ
-      (Succ s' {}, Succ t' {}) => compare0 defs ctx sg nat s' t'
+      (Succ s'   {}, Succ t'   {}) => compare0 defs ctx sg nat s' t'
+      (Nat (S x) {}, Succ t'   {}) => compare0 defs ctx sg nat (Nat x s.loc) t'
+      (Succ s'   {}, Nat (S y) {}) => compare0 defs ctx sg nat s' (Nat y t.loc)
 
       (E e, E f) => ignore $ Elim.compare0 defs ctx sg e f
 
-      (Zero {}, Succ {}) => clashT s.loc ctx nat s t
-      (Zero {}, E _)     => clashT s.loc ctx nat s t
-      (Succ {}, Zero {}) => clashT s.loc ctx nat s t
-      (Succ {}, E _)     => clashT s.loc ctx nat s t
-      (E _,     Zero {}) => clashT s.loc ctx nat s t
-      (E _,     Succ {}) => clashT s.loc ctx nat s t
+      (Nat 0 {}, Succ  {}) => clashT s.loc ctx nat s t
+      (Nat 0 {}, E _)      => clashT s.loc ctx nat s t
+      (Succ  {}, Nat 0 {}) => clashT s.loc ctx nat s t
+      (Succ  {}, E _)      => clashT s.loc ctx nat s t
+      (E _,      Nat 0 {}) => clashT s.loc ctx nat s t
+      (E _,      Succ  {}) => clashT s.loc ctx nat s t
 
-      (Zero {}, t) => wrongType t.loc ctx nat t
-      (Succ {}, t) => wrongType t.loc ctx nat t
-      (E _,     t) => wrongType t.loc ctx nat t
-      (s,       _) => wrongType s.loc ctx nat s
+      (Nat 0 {}, t) => wrongType t.loc ctx nat t
+      (Succ  {}, t) => wrongType t.loc ctx nat t
+      (E _,      t) => wrongType t.loc ctx nat t
+      (s,        _) => wrongType s.loc ctx nat s
 
   compare0' defs ctx sg str@(STRING {}) s t = local_ Equal $
     case (s, t) of
diff --git a/lib/Quox/FreeVars.idr b/lib/Quox/FreeVars.idr
index 929eb71..00ff22d 100644
--- a/lib/Quox/FreeVars.idr
+++ b/lib/Quox/FreeVars.idr
@@ -191,7 +191,7 @@ HasFreeVars (Term d) where
   fv (Eq      {ty, l, r, _}) = fvD ty <+> fv l <+> fv r
   fv (DLam    {body, _})     = fvD body
   fv (NAT     {})            = none
-  fv (Zero    {})            = none
+  fv (Nat     {})            = none
   fv (Succ    {p, _})        = fv p
   fv (STRING  {})            = none
   fv (Str     {})            = none
@@ -269,7 +269,7 @@ HasFreeDVars Term where
   fdv (Eq      {ty, l, r, _}) = fdv @{DScope} ty <+> fdv l <+> fdv r
   fdv (DLam    {body, _})     = fdv @{DScope} body
   fdv (NAT     {})            = none
-  fdv (Zero    {})            = none
+  fdv (Nat     {})            = none
   fdv (Succ    {p, _})        = fdv p
   fdv (STRING  {})            = none
   fdv (Str     {})            = none
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 0979915..8b312e4 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -189,7 +189,7 @@ mutual
         <*> pure loc
 
     NAT loc => pure $ NAT loc
-    Zero loc => pure $ Zero loc
+    Nat n loc => pure $ Nat n loc
     Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
 
     STRING loc => pure $ STRING loc
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index b687cba..030c2ec 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -296,11 +296,11 @@ termArg fname = withLoc fname $
   <|> [|Enum enumType|]
   <|> [|Tag tag|]
   <|> const <$> boxTerm fname
-  <|> NAT  <$ res "ℕ"
-  <|> Zero <$ res "zero"
+  <|> NAT    <$ res "ℕ"
+  <|> Nat 0  <$ res "zero"
+  <|> [|Nat nat|]
   <|> STRING <$ res "String"
   <|> [|Str strLit|]
-  <|> [|fromNat nat|]
   <|> [|V qname displacement|]
   <|> const <$> tupleTerm fname
 
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index d6c13a6..2b7e19c 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -86,7 +86,7 @@ namespace PTerm
       | DApp PTerm PDim Loc
 
       | NAT Loc
-      | Zero Loc | Succ PTerm Loc
+      | Nat Nat Loc | Succ PTerm Loc
 
       | STRING Loc  -- "String" is a reserved word in idris
       | Str String Loc
@@ -110,6 +110,10 @@ namespace PTerm
       | CaseBox PatVar PTerm Loc
     %name PCaseBody body
 
+  public export %inline
+  Zero : Loc -> PTerm
+  Zero = Nat 0
+
 %runElab deriveMutual ["PTerm", "PCaseBody"] [Eq, Ord, Show, PrettyVal]
 
 export
@@ -130,7 +134,7 @@ Located PTerm where
   (DLam    _ _           loc).loc = loc
   (DApp    _ _           loc).loc = loc
   (NAT                   loc).loc = loc
-  (Zero                  loc).loc = loc
+  (Nat     _             loc).loc = loc
   (Succ    _             loc).loc = loc
   (STRING                loc).loc = loc
   (Str     _             loc).loc = loc
@@ -219,12 +223,6 @@ Located PTopLevel where
   (PLoad _ loc).loc = loc
 
 
-public export
-fromNat : Nat -> Loc -> PTerm
-fromNat 0     loc = Zero loc
-fromNat (S k) loc = Succ (fromNat k loc) loc
-
-
 public export
 PFile : Type
 PFile = List PTopLevel
diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 8ec1838..994b4ea 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -88,8 +88,7 @@ mutual
 
     ||| natural numbers (temporary until 𝐖 gets added)
     NAT : (loc : Loc) -> Term d n
-    -- [todo] can these be elims?
-    Zero : (loc : Loc) -> Term d n
+    Nat : (val : Nat) -> (loc : Loc) -> Term d n
     Succ : (p : Term d n) -> (loc : Loc) -> Term d n
 
     ||| strings
@@ -324,10 +323,9 @@ public export %inline
 BVT : (i : Nat) -> (0 _ : LT i n) => (loc : Loc) -> Term d n
 BVT i loc = E $ BV i loc
 
-public export
-makeNat : Nat -> Loc -> Term d n
-makeNat 0 loc = Zero loc
-makeNat (S k) loc = Succ (makeNat k loc) loc
+public export %inline
+Zero : Loc -> Term d n
+Zero = Nat 0
 
 public export %inline
 enum : List TagVal -> Loc -> Term d n
@@ -379,7 +377,7 @@ Located (Term d n) where
   (Eq _ _ _ loc).loc    = loc
   (DLam _ loc).loc      = loc
   (NAT loc).loc         = loc
-  (Zero loc).loc        = loc
+  (Nat _ loc).loc       = loc
   (STRING loc).loc      = loc
   (Str _ loc).loc       = loc
   (Succ _ loc).loc      = loc
@@ -442,7 +440,7 @@ Relocatable (Term d n) where
   setLoc loc (Eq ty l r _) = Eq ty l r loc
   setLoc loc (DLam body _) = DLam body loc
   setLoc loc (NAT _) = NAT loc
-  setLoc loc (Zero _) = Zero loc
+  setLoc loc (Nat n _) = Nat n loc
   setLoc loc (Succ p _) = Succ p loc
   setLoc loc (STRING _) = STRING loc
   setLoc loc (Str s _) = Str s loc
diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index ecb5821..a2629de 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -450,19 +450,9 @@ prettyTerm dnames tnames s@(DLam {}) =
   prettyLambda dnames tnames s
 
 prettyTerm dnames tnames (NAT _) = natD
-prettyTerm dnames tnames (Zero _) = hl Syntax "0"
-prettyTerm dnames tnames (Succ p _) = do
-  succD <- succD
-  let succ : Doc opts -> Eff Pretty (Doc opts)
-      succ t = prettyAppD succD [t]
-      toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
-      toNat s with (pushSubsts' s)
-        _ | Zero _   = pure $ Right 0
-        _ | Succ d _ = bitraverse succ (pure . S) =<<
-                       toNat (assert_smaller s d)
-        _ | s'       = map Left . withPrec Arg $
-                       prettyTerm dnames tnames $ assert_smaller s s'
-  either succ (hl Syntax . text . show . S) =<< toNat p
+prettyTerm dnames tnames (Nat n _) = hl Syntax $ pshow n
+prettyTerm dnames tnames (Succ p _) =
+  prettyAppD !succD [!(withPrec Arg $ prettyTerm dnames tnames p)]
 
 prettyTerm dnames tnames (STRING _) = stringD
 prettyTerm dnames tnames (Str s _) = prettyStrLit s
diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 8610b78..b85ffd4 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -274,8 +274,8 @@ mutual
       nclo $ DLam (body // th // ph) loc
     pushSubstsWith _ _ (NAT loc) =
       nclo $ NAT loc
-    pushSubstsWith _ _ (Zero loc) =
-      nclo $ Zero loc
+    pushSubstsWith _ _ (Nat n loc) =
+      nclo $ Nat n loc
     pushSubstsWith th ph (Succ n loc) =
       nclo $ Succ (n // th // ph) loc
     pushSubstsWith _ _ (STRING loc) =
diff --git a/lib/Quox/Syntax/Term/Tighten.idr b/lib/Quox/Syntax/Term/Tighten.idr
index 83ea7e0..de45d98 100644
--- a/lib/Quox/Syntax/Term/Tighten.idr
+++ b/lib/Quox/Syntax/Term/Tighten.idr
@@ -63,8 +63,8 @@ mutual
     DLam <$> tightenDS p body <*> pure loc
   tightenT' p (NAT loc) =
     pure $ NAT loc
-  tightenT' p (Zero loc) =
-    pure $ Zero loc
+  tightenT' p (Nat n loc) =
+    pure $ Nat n loc
   tightenT' p (Succ s loc) =
     Succ <$> tightenT p s <*> pure loc
   tightenT' p (STRING loc) =
@@ -188,8 +188,8 @@ mutual
     DLam <$> dtightenDS p body <*> pure loc
   dtightenT' p (NAT loc) =
     pure $ NAT loc
-  dtightenT' p (Zero loc) =
-    pure $ Zero loc
+  dtightenT' p (Nat n loc) =
+    pure $ Nat n loc
   dtightenT' p (Succ s loc) =
     Succ <$> dtightenT p s <*> pure loc
   dtightenT' p (STRING loc) =
diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr
index 2273a08..a477c3e 100644
--- a/lib/Quox/Typechecker.idr
+++ b/lib/Quox/Typechecker.idr
@@ -190,7 +190,7 @@ mutual
 
   check' ctx sg t@(NAT {}) ty = toCheckType ctx sg t ty
 
-  check' ctx sg (Zero {}) ty = do
+  check' ctx sg (Nat {}) ty = do
     expectNAT !(askAt DEFS) ctx SZero ty.loc ty
     pure $ zeroFor ctx
 
@@ -276,7 +276,7 @@ mutual
     throw $ NotType t.loc ctx t
 
   checkType' ctx (NAT {}) u = pure ()
-  checkType' ctx t@(Zero {}) u = throw $ NotType t.loc ctx t
+  checkType' ctx t@(Nat {}) u = throw $ NotType t.loc ctx t
   checkType' ctx t@(Succ {}) u = throw $ NotType t.loc ctx t
 
   checkType' ctx (STRING loc) u = pure ()
diff --git a/lib/Quox/Untyped/Erase.idr b/lib/Quox/Untyped/Erase.idr
index 349d9fd..2aa40cf 100644
--- a/lib/Quox/Untyped/Erase.idr
+++ b/lib/Quox/Untyped/Erase.idr
@@ -189,9 +189,9 @@ eraseTerm ctx ty (DLam body loc) = do
 eraseTerm ctx _ s@(NAT {}) =
   throw $ CompileTimeOnly ctx s
 
--- 0 ⤋ 0 ⇐ ℕ
-eraseTerm _ _ (Zero loc) =
-  pure $ Zero loc
+-- n ⤋ n ⇐ ℕ
+eraseTerm _ _ (Nat n loc) =
+  pure $ Nat n loc
 
 --       s ⤋ s' ⇐ ℕ
 -- -----------------------
@@ -438,7 +438,7 @@ eraseElim ctx (DCloE (Sub term th)) =
 
 export
 uses : Var n -> Term n -> Nat
-uses i (F _ _) = 0
+uses i (F {}) = 0
 uses i (B j _) = if i == j then 1 else 0
 uses i (Lam x body _) = uses (VS i) body
 uses i (App fun arg _) = uses i fun + uses i arg
@@ -448,16 +448,16 @@ uses i (Snd pair _) = uses i pair
 uses i (Tag tag _) = 0
 uses i (CaseEnum tag cases _) =
   uses i tag + foldl max 0 (map (assert_total uses i . snd) cases)
-uses i (Absurd _) = 0
-uses i (Zero _) = 0
+uses i (Absurd {}) = 0
+uses i (Nat {}) = 0
 uses i (Succ nat _) = uses i nat
 uses i (CaseNat nat zer suc _) = uses i nat + max (uses i zer) (uses' suc)
   where uses' : CaseNatSuc n -> Nat
         uses' (NSRec  _ _ s) = uses (VS (VS i)) s
         uses' (NSNonrec _ s) = uses (VS i) s
-uses i (Str _ _) = 0
+uses i (Str {}) = 0
 uses i (Let x rhs body _) = uses i rhs + uses (VS i) body
-uses i (Erased _) = 0
+uses i (Erased {}) = 0
 
 export
 inlineable : U.Term n -> Bool
@@ -482,7 +482,7 @@ trimLets (CaseEnum tag cases loc) =
   CaseEnum (trimLets tag)
            (map (map $ \c => trimLets $ assert_smaller cases c) cases) loc
 trimLets (Absurd loc) = Absurd loc
-trimLets (Zero loc) = Zero loc
+trimLets (Nat n loc) = Nat n loc
 trimLets (Succ nat loc) = Succ (trimLets nat) loc
 trimLets (CaseNat nat zer suc loc) =
   CaseNat (trimLets nat) (trimLets zer) (trimLets' suc) loc
diff --git a/lib/Quox/Untyped/Scheme.idr b/lib/Quox/Untyped/Scheme.idr
index d0fd2de..a005d4c 100644
--- a/lib/Quox/Untyped/Scheme.idr
+++ b/lib/Quox/Untyped/Scheme.idr
@@ -200,13 +200,11 @@ toScheme xs (CaseEnum tag cases _) =
 toScheme xs (Absurd _) =
   pure $ Q "absurd"
 
-toScheme xs (Zero _) =
-  pure $ N 0
+toScheme xs (Nat n _) =
+  pure $ N n
 
 toScheme xs (Succ nat _) =
-  case !(toScheme xs nat) of
-    N n => pure $ N $ S n
-    s   => pure $ L ["+", s, N 1]
+  pure $ L ["+", !(toScheme xs nat), N 1]
 
 toScheme xs (CaseNat nat zer (NSRec p ih suc) _) =
   freshInBC [< p, ih] $ \[< p, ih] =>
diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr
index 0548293..b8b6abb 100644
--- a/lib/Quox/Untyped/Syntax.idr
+++ b/lib/Quox/Untyped/Syntax.idr
@@ -39,7 +39,7 @@ data Term where
   ||| empty match
   Absurd : Loc -> Term n
 
-  Zero : Loc -> Term n
+  Nat : (val : Nat) -> Loc -> Term n
   Succ : (nat : Term n) -> Loc -> Term n
   CaseNat : (nat : Term n) ->
             (zer : Term n) ->
@@ -76,7 +76,7 @@ Located (Term n) where
   (Tag _ loc).loc         = loc
   (CaseEnum _ _ loc).loc  = loc
   (Absurd loc).loc        = loc
-  (Zero loc).loc          = loc
+  (Nat _ loc).loc         = loc
   (Succ _ loc).loc        = loc
   (CaseNat _ _ _ loc).loc = loc
   (Str _ loc).loc         = loc
@@ -198,16 +198,6 @@ sucCaseArm (NSRec x ih s) = pure $
 sucCaseArm (NSNonrec x s) = pure $
   MkPrettyCaseArm !(sucPat x) [x] s
 
-private covering
-prettyNat : {opts : LayoutOpts} ->
-            BContext n -> Term n -> Eff Pretty (Either Nat (Doc opts))
-prettyNat xs (Zero _) = pure $ Left 0
-prettyNat xs (Succ n _) =
-  case !(withPrec Arg $ prettyNat xs n) of
-    Left n    => pure $ Left $ S n
-    Right doc => map Right $ parensIfM App $ sep [!succD, doc]
-prettyNat xs s = map Right $ prettyTerm xs s
-
 prettyTerm _  (F x _) = prettyFree x
 prettyTerm xs (B i _) = prettyTBind $ xs !!! i
 prettyTerm xs (Lam x body _) =
@@ -229,11 +219,9 @@ prettyTerm xs (CaseEnum tag cases _) =
   prettyCase xs prettyTag tag $
     map (\(t, rhs) => MkPrettyCaseArm t [] rhs) $ toList cases
 prettyTerm xs (Absurd _) = hl Syntax "absurd"
-prettyTerm xs (Zero _) = hl Tag "0"
+prettyTerm xs (Nat n _) = hl Tag $ pshow n
 prettyTerm xs (Succ nat _) =
-  case !(prettyNat xs nat) of
-    Left  n   => hl Tag $ pshow $ S n
-    Right doc => prettyApp' !succD [< doc]
+  prettyApp' !succD [< !(prettyTerm xs nat)]
 prettyTerm xs (CaseNat nat zer suc _) =
   prettyCase xs pure nat [MkPrettyCaseArm !zeroD [] zer, !(sucCaseArm suc)]
 prettyTerm xs (Str s _) =
@@ -298,8 +286,8 @@ CanSubstSelf Term where
       CaseEnum (tag // th) (map (assert_total mapSnd (// th)) cases) loc
     Absurd loc =>
       Absurd loc
-    Zero loc =>
-      Zero loc
+    Nat n loc =>
+      Nat n loc
     Succ nat loc =>
       Succ (nat // th) loc
     CaseNat nat zer suc loc =>
diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index b3f7331..efc51f9 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -84,11 +84,18 @@ isTagHead _                          = False
 ||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
 public export %inline
 isNatHead : Elim {} -> Bool
-isNatHead (Ann (Zero {}) (NAT {}) _) = True
+isNatHead (Ann (Nat  {}) (NAT {}) _) = True
 isNatHead (Ann (Succ {}) (NAT {}) _) = True
 isNatHead (Coe {})                   = True
 isNatHead _                          = False
 
+||| a natural constant, with or without an annotation
+public export %inline
+isNatConst : Term d n -> Bool
+isNatConst (Nat {})               = True
+isNatConst (E (Ann (Nat {}) _ _)) = True
+isNatConst _                      = False
+
 ||| an expression like `[s] ∷ [π. A]`
 public export %inline
 isBoxHead : Elim {} -> Bool
@@ -122,7 +129,7 @@ isTyCon (Tag     {}) = False
 isTyCon (Eq      {}) = True
 isTyCon (DLam    {}) = False
 isTyCon (NAT     {}) = True
-isTyCon (Zero    {}) = False
+isTyCon (Nat     {}) = False
 isTyCon (Succ    {}) = False
 isTyCon (STRING  {}) = True
 isTyCon (Str     {}) = False
@@ -169,7 +176,7 @@ canPushCoe sg (Tag     {}) _         = False
 canPushCoe sg (Eq      {}) _         = True
 canPushCoe sg (DLam    {}) _         = False
 canPushCoe sg (NAT     {}) _         = True
-canPushCoe sg (Zero    {}) _         = False
+canPushCoe sg (Nat     {}) _         = False
 canPushCoe sg (Succ    {}) _         = False
 canPushCoe sg (STRING  {}) _         = True
 canPushCoe sg (Str     {}) _         = False
@@ -235,9 +242,11 @@ mutual
   ||| 2. an annotated elimination
   |||    (the annotation is redundant in a checkable context)
   ||| 3. a closure
+  ||| 4. `succ` applied to a natural constant
   public export
   isRedexT : RedexTest Term
-  isRedexT _    _  (CloT  {}) = True
-  isRedexT _    _  (DCloT {}) = True
-  isRedexT defs sg (E {e, _}) = isAnn e || isRedexE defs sg e
-  isRedexT _    _  _          = False
+  isRedexT _    _  (CloT  {})  = True
+  isRedexT _    _  (DCloT {})  = True
+  isRedexT defs sg (E {e, _})  = isAnn e || isRedexE defs sg e
+  isRedexT _    _  (Succ p {}) = isNatConst p
+  isRedexT _    _  _           = False
diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr
index 3d7f94b..e636adf 100644
--- a/lib/Quox/Whnf/Main.idr
+++ b/lib/Quox/Whnf/Main.idr
@@ -113,8 +113,13 @@ CanWhnf Elim Interface.isRedexE where
       Left _ =>
         let ty = sub1 ret nat in
         case nat of
-          Ann (Zero _) (NAT _) _ =>
+          Ann (Nat 0 _) (NAT _) _ =>
             whnf defs ctx sg $ Ann zer ty zer.loc
+          Ann (Nat (S n) succLoc) (NAT natLoc) _ =>
+            let nn = Ann (Nat n succLoc) (NAT natLoc) succLoc
+                tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
+            in
+            whnf defs ctx sg $ Ann tm ty caseLoc
           Ann (Succ n succLoc) (NAT natLoc) _ =>
             let nn = Ann n (NAT natLoc) succLoc
                 tm = subN suc [< nn, CaseNat pi piIH nn ret zer suc caseLoc]
@@ -236,13 +241,19 @@ CanWhnf Term Interface.isRedexT where
   whnf _ _ _ t@(Eq      {}) = pure $ nred t
   whnf _ _ _ t@(DLam    {}) = pure $ nred t
   whnf _ _ _ t@(NAT     {}) = pure $ nred t
-  whnf _ _ _ t@(Zero    {}) = pure $ nred t
-  whnf _ _ _ t@(Succ    {}) = pure $ nred t
+  whnf _ _ _ t@(Nat     {}) = pure $ nred t
   whnf _ _ _ t@(STRING  {}) = pure $ nred t
   whnf _ _ _ t@(Str     {}) = pure $ nred t
   whnf _ _ _ t@(BOX     {}) = pure $ nred t
   whnf _ _ _ t@(Box     {}) = pure $ nred t
 
+  whnf _ _ _ (Succ p loc) =
+    case nchoose $ isNatConst p of
+      Left _ => case p of
+        Nat p _               => pure $ nred $ Nat (S p) loc
+        E (Ann (Nat p _) _ _) => pure $ nred $ Nat (S p) loc
+      Right nc => pure $ Element (Succ p loc) $ ?cc
+
   -- s ∷ A ⇝ s   (in term context)
   whnf defs ctx sg (E e) = do
     Element e enf <- whnf defs ctx sg e
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
index 61926b0..60f71ad 100644
--- a/tests/Tests/Equal.idr
+++ b/tests/Tests/Equal.idr
@@ -486,11 +486,11 @@ tests = "equality & subtyping" :- [
     testEq "caseω 4 return ℕ of {0 ⇒ 0; succ n ⇒ n} = 3" $
       equalT empty
         (^NAT)
-        (E $ ^CaseNat Any Zero (^Ann (^makeNat 4) (^NAT))
+        (E $ ^CaseNat Any Zero (^Ann (^Nat 4) (^NAT))
           (SN $ ^NAT)
           (^Zero)
           (SY [< "n", ^BN Unused] $ ^BVT 1))
-        (^makeNat 3)
+        (^Nat 3)
   ],
 
   todo "pair types",
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index d74a65d..299c905 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -284,12 +284,10 @@ tests = "parser" :- [
   "naturals" :- [
     parseMatch term "ℕ" `(NAT _),
     parseMatch term "Nat" `(NAT _),
-    parseMatch term "zero" `(Zero _),
+    parseMatch term "zero" `(Nat 0 _),
     parseMatch term "succ n" `(Succ (V "n" {}) _),
-    parseMatch term "3"
-      `(Succ (Succ (Succ (Zero _) _) _) _),
-    parseMatch term "succ (succ 1)"
-      `(Succ (Succ (Succ (Zero _) _) _) _),
+    parseMatch term "3" `(Nat 3 _),
+    parseMatch term "succ (succ 1)" `(Succ (Succ (Nat 1 _) _) _),
     parseFails term "succ succ 5",
     parseFails term "succ"
   ],
@@ -299,12 +297,9 @@ tests = "parser" :- [
       `(BOX (PQ One _) (NAT _) _),
     parseMatch term "[ω. ℕ × ℕ]"
       `(BOX (PQ Any _) (Sig (Unused _) (NAT _) (NAT _) _) _),
-    parseMatch term "[a]"
-      `(Box (V "a" {}) _),
-    parseMatch term "[0]"
-      `(Box (Zero _) _),
-    parseMatch term "[1]"
-      `(Box (Succ (Zero _) _) _)
+    parseMatch term "[a]" `(Box (V "a" {}) _),
+    parseMatch term "[0]" `(Box (Nat 0 _) _),
+    parseMatch term "[1]" `(Box (Nat 1 _) _)
   ],
 
   "coe" :- [
@@ -389,13 +384,13 @@ tests = "parser" :- [
         (CaseNat (V "a" {}) (PV "n'" _, PQ Zero _, Unused _, V "b" {}) _) _),
     parseMatch term "caseω n return ℕ of { succ _, 1.ih ⇒ ih; zero ⇒ 0; }"
       `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
-        (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
+        (CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
     parseMatch term "caseω n return ℕ of { succ _, ω.ih ⇒ ih; zero ⇒ 0; }"
       `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
-        (CaseNat (Zero _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _),
+        (CaseNat (Nat 0 _) (Unused _, PQ Any _, PV "ih" _, V "ih" {}) _) _),
     parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }"
       `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
-        (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
+        (CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
     parseFails term "caseω n return A of { zero ⇒ a }",
     parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
   ],