refactor: more general OfNat, remove One and Zero classes

src/Init/Coe.lean

@@ -130,9 +130,8 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α :=
   Remark: one may question why we use `OfNat α` instead of `Coe Nat α`.
   Reason: `OfNat` is for implementing polymorphic numeric literals, and we may
   want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/
-instance hasOfNatOfCoe {α : Type u} {β : Type v} [OfNat α] [Coe α β] : OfNat β := {
-  ofNat := fun (n : Nat) => coe (OfNat.ofNat n : α)
-}
+instance hasOfNatOfCoe [OfNat α n] [Coe α β] : OfNat β n where
+  ofNat := coe (OfNat.ofNat n : α)
 
 @[inline] def liftCoeM {m : Type u → Type v} {n : Type u → Type w} {α β : Type u} [MonadLiftT m n] [∀ a, CoeT α a β] [Monad n] (x : m α) : n β := do
   let a ← liftM x

src/Init/Control/Id.lean

@@ -22,7 +22,7 @@ instance : Monad Id := {
 
 @[inline] protected def run (x : Id α) : α := x
 
-instance [OfNat α] : OfNat (Id α) :=
-  inferInstanceAs (OfNat α)
+instance [OfNat α n] : OfNat (Id α) n :=
+  inferInstanceAs (OfNat α n)
 
 end Id

src/Init/Data/Float.lean

@@ -44,7 +44,7 @@ def Float.lt  : Float → Float → Prop := fun a b =>
 def Float.le  : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
-instance : OfNat Float     := ⟨Float.ofNat⟩
+instance : OfNat Float n   := ⟨Float.ofNat n⟩
 instance : Add Float       := ⟨Float.add⟩
 instance : Sub Float       := ⟨Float.sub⟩
 instance : Mul Float       := ⟨Float.mul⟩

src/Init/Data/Int/Basic.lean

@@ -124,7 +124,7 @@ protected def repr : Int → String
 
 instance : Repr Int := ⟨Int.repr⟩
 instance : ToString Int := ⟨Int.repr⟩
-instance : OfNat Int := ⟨Int.ofNat⟩
+instance : OfNat Int n := ⟨Int.ofNat n⟩
 
 @[extern "lean_int_div"]
 def div : (@& Int) → (@& Int) → Int

src/Init/Data/UInt.lean

@@ -33,7 +33,7 @@ def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
 def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
 def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
 
-instance : OfNat UInt8     := ⟨UInt8.ofNat⟩
+instance : OfNat UInt8 n   := ⟨UInt8.ofNat n⟩
 instance : Add UInt8       := ⟨UInt8.add⟩
 instance : Sub UInt8       := ⟨UInt8.sub⟩
 instance : Mul UInt8       := ⟨UInt8.mul⟩
@@ -83,7 +83,7 @@ def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
 def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
 
 
-instance : OfNat UInt16     := ⟨UInt16.ofNat⟩
+instance : OfNat UInt16 n   := ⟨UInt16.ofNat n⟩
 instance : Add UInt16       := ⟨UInt16.add⟩
 instance : Sub UInt16       := ⟨UInt16.sub⟩
 instance : Mul UInt16       := ⟨UInt16.mul⟩
@@ -136,7 +136,7 @@ def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
 @[extern c inline "((uint32_t)#1)"]
 def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
 
-instance : OfNat UInt32     := ⟨UInt32.ofNat⟩
+instance : OfNat UInt32 n   := ⟨UInt32.ofNat n⟩
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
 instance : Mul UInt32       := ⟨UInt32.mul⟩
@@ -187,7 +187,7 @@ constant UInt64.shiftLeft (a b : UInt64) : UInt64
 @[extern c inline "#1 >> #2"]
 constant UInt64.shiftRight (a b : UInt64) : UInt64
 
-instance : OfNat UInt64     := ⟨UInt64.ofNat⟩
+instance : OfNat UInt64 n   := ⟨UInt64.ofNat n⟩
 instance : Add UInt64       := ⟨UInt64.add⟩
 instance : Sub UInt64       := ⟨UInt64.sub⟩
 instance : Mul UInt64       := ⟨UInt64.mul⟩
@@ -254,7 +254,7 @@ constant USize.shiftRight (a b : USize) : USize
 def USize.lt (a b : USize) : Prop := a.val < b.val
 def USize.le (a b : USize) : Prop := a.val ≤ b.val
 
-instance : OfNat USize     := ⟨USize.ofNat⟩
+instance : OfNat USize n   := ⟨USize.ofNat n⟩
 instance : Add USize       := ⟨USize.add⟩
 instance : Sub USize       := ⟨USize.sub⟩
 instance : Mul USize       := ⟨USize.mul⟩

src/Init/Notation.lean

@@ -8,6 +8,8 @@ Notation for operators defined at Prelude.lean
 prelude
 import Init.Prelude
 
+syntax[rawNatLit] "natLit! " num : term
+
 infixr:90 " ∘ "  => Function.comp
 infixr:35 " × "  => Prod
 

src/Init/Prelude.lean

@@ -344,34 +344,12 @@ instance : Inhabited Nat where
   default := Nat.zero
 
 /- For numeric literals notation -/
-class OfNat (α : Type u) where
-  ofNat : Nat → α
-
-export OfNat (ofNat)
+class OfNat (α : Type u) (n : Nat) where
+  ofNat : α
 
 @[defaultInstance]
-instance : OfNat Nat where
-  ofNat x := x
-
-class One (α : Type u) where
-  one : α
-
-instance [OfNat α] : One α where
-  one := ofNat Nat.zero.succ
-
-class Zero (α : Type u) where
-  zero : α
-
-instance [OfNat α] : Zero α where
-  zero := ofNat Nat.zero
-
-@[defaultInstance]
-instance : One Nat where
-  one := Nat.zero.succ
-
-@[defaultInstance]
-instance : Zero Nat where
-  zero := Nat.zero
+instance instOfNatDefault (n : Nat) : OfNat Nat n where
+  ofNat := n
 
 class HasLessEq (α : Type u) where LessEq : α → α → Prop
 class HasLess   (α : Type u) where Less : α → α → Prop

src/Lean/Elab/Term.lean

@@ -1266,6 +1266,11 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL
   let mvar ← mkInstMVar (mkApp2 (Lean.mkConst `OfNat [u]) typeMVar (mkNatLit val))
   return mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar (mkNatLit val) mvar
 
+@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab :=  fun stx expectedType? => do
+  match stx[1].isNatLit? with
+  | some val => return mkNatLit val
+  | none     => throwIllFormedSyntax
+
 @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
   match stx.isCharLit? with
   | some val => return mkApp (Lean.mkConst `Char.ofNat) (mkNatLit val.toNat)

tests/lean/StxQuot.lean.expected.out

@@ -2,18 +2,18 @@
 "<missing>"
 "<missing>"
 "<missing>"
-"(_kind.term._@.Init.Notation._hyg.335 <missing> \"+\" (numLit \"1\"))"
-"(_kind.term._@.Init.Notation._hyg.335 <missing> \"+\" (numLit \"1\"))"
-"(_kind.term._@.Init.Notation._hyg.335 (numLit \"1\") \"+\" (numLit \"1\"))"
+"(_kind.term._@.Init.Notation._hyg.351 <missing> \"+\" (numLit \"1\"))"
+"(_kind.term._@.Init.Notation._hyg.351 <missing> \"+\" (numLit \"1\"))"
+"(_kind.term._@.Init.Notation._hyg.351 (numLit \"1\") \"+\" (numLit \"1\"))"
 "(Term.fun \"fun\" (Term.basicFun [`a._@.UnhygienicMain._hyg.1] \"=>\" `a._@.UnhygienicMain._hyg.1))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])))]"
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 `Nat.one._@.UnhygienicMain._hyg.1])"
-"(_kind.term._@.Init.Notation._hyg.7049\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))"
+"(_kind.term._@.Init.Notation._hyg.7065\n `f._@.UnhygienicMain._hyg.1\n \"$\"\n (Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1 (numLit \"1\")]))"
 "(Term.app `f._@.UnhygienicMain._hyg.1 [`Nat.one._@.UnhygienicMain._hyg.1])"
 "(Term.proj `Nat.one._@.UnhygienicMain._hyg.1 \".\" `b._@.UnhygienicMain._hyg.1)"
-"(_kind.term._@.Init.Notation._hyg.335 (numLit \"2\") \"+\" (numLit \"1\"))"
+"(_kind.term._@.Init.Notation._hyg.351 (numLit \"2\") \"+\" (numLit \"1\"))"
 "(Command.declaration\n (Command.declModifiers [] [] [] [] [] [])\n (Command.def\n  \"def\"\n  (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n  (Command.optDeclSig [] [])\n  (Command.declValSimple \":=\" (numLit \"1\") [])))"
 "[(Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `bar._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"2\") [])))\n (Command.declaration\n  (Command.declModifiers [] [] [] [] [] [])\n  (Command.def\n   \"def\"\n   (Command.declId `foo._@.UnhygienicMain._hyg.1 [])\n   (Command.optDeclSig [] [])\n   (Command.declValSimple \":=\" (numLit \"1\") [])))]"
 "0"

tests/lean/match1.lean.expected.out

@@ -37,7 +37,7 @@ fun (x x_1 : Option Nat) =>
   | x_2, x_3 => none : Option Nat → Option Nat → Option Nat
 fun (x : Nat) =>
   (match x with 
-    | Nat.zero => id
+    | 0 => id
     | Nat.succ x_1 => id)
     x : Nat → Nat
 fun (x : Array Nat) =>

tests/lean/run/alg.lean

@@ -14,6 +14,12 @@ class CommSemigroup (α : Type u) extends Semigroup α where
 instance [CommSemigroup α] : MulComm α where
   mul_comm := CommSemigroup.mul_comm
 
+class One (α : Type u) where
+  one : α
+
+instance [One α] : OfNat α (natLit! 1) where
+  ofNat := One.one
+
 class Monoid (α : Type u) extends Semigroup α, One α where
   one_mul (a : α) : 1 * a = a
   mul_one (a : α) : a * 1 = a
@@ -35,7 +41,7 @@ class Inv (α : Type u) where
 postfix:max "⁻¹" => Inv.inv
 
 class Group (α : Type u) extends Monoid α, Inv α where
-  mul_left_inv (a : α) : a⁻¹ * a = one
+  mul_left_inv (a : α) : a⁻¹ * a = 1
 
 export Group (mul_left_inv)
 

tests/lean/run/balg.lean

@@ -1,3 +1,5 @@
+import Lean
+
 universe u
 
 structure Magma where
@@ -10,6 +12,8 @@ instance : CoeSort Magma (Type u) where
 abbrev mul {M : Magma} (a b : M) : M :=
   M.mul a b
 
+set_option pp.all true
+
 infix:70 [1] "*" => mul
 
 structure Semigroup extends Magma where
@@ -52,11 +56,11 @@ abbrev inv {G : Group} (a : G) : G :=
 
 postfix:max "⁻¹" => inv
 
-instance (G : Group) : One (coeSort G.toMagma) where
-  one := G.one
+instance (G : Group) : OfNat (coeSort G.toMagma) (natLit! 1) where
+  ofNat := G.one
 
-instance (G : Group) : One (G.toMagma.α) where
-  one := G.one
+instance (G : Group) : OfNat (G.toMagma.α) (natLit! 1) where
+  ofNat := G.one
 
 structure CommGroup extends Group where
   mul_comm (a b : α) : a * b = b * a

tests/lean/run/bigop.lean

@@ -37,8 +37,8 @@ partial def finElems : (n : Nat) → List (Fin n)
 instance {n} : Enumerable (Fin n) :=
 { elems := (finElems n).reverse }
 
-instance {n} : OfNat (Fin (Nat.succ n)) :=
-⟨Fin.ofNat⟩
+instance : OfNat (Fin (Nat.succ n)) m :=
+⟨Fin.ofNat m⟩
 
 -- Declare a new syntax category for "indexing" big operators
 declare_syntax_cat index