From 3757b26dc28fa72dbe0558e67c07dc2bae94fd74 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Oct 2020 17:30:48 -0700
Subject: [PATCH] chore: move to new frontend

---
 src/Init/Data/Fin/Basic.lean |  61 ++++++++++---------
 src/Init/Data/UInt.lean      | 111 ++++++++++++++++++++---------------
 2 files changed, 95 insertions(+), 77 deletions(-)

diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 22921e0d15..1f97c55c80 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -9,53 +10,55 @@ import Init.Data.Nat.Bitwise
 import Init.Coe
 
 open Nat
-structure Fin (n : Nat) := (val : Nat) (isLt : val < n)
+structure Fin (n : Nat) :=
+  (val : Nat)
+  (isLt : val < n)
 
 namespace Fin
 
 instance coeToNat {n} : Coe (Fin n) Nat :=
-⟨fun v => v.val⟩
+  ⟨fun v => v.val⟩
 
 protected def lt {n} (a b : Fin n) : Prop :=
-a.val < b.val
+  a.val < b.val
 
 protected def le {n} (a b : Fin n) : Prop :=
-a.val ≤ b.val
+  a.val ≤ b.val
 
 instance {n} : HasLess (Fin n)    := ⟨Fin.lt⟩
 instance {n} : HasLessEq (Fin n)  := ⟨Fin.le⟩
 
 instance decLt {n} (a b : Fin n) :  Decidable (a < b) :=
-Nat.decLt _ _
+  Nat.decLt ..
 
 instance decLe {n} (a b : Fin n) : Decidable (a ≤ b) :=
-Nat.decLe _ _
+  Nat.decLe ..
 
 def elim0.{u} {α : Sort u} : Fin 0 → α
-| ⟨_, h⟩ => absurd h (notLtZero _)
+  | ⟨_, h⟩ => absurd h (notLtZero _)
 
 variable {n : Nat}
 
 def ofNat {n : Nat} (a : Nat) : Fin (succ n) :=
-⟨a % succ n, Nat.modLt _ (Nat.zeroLtSucc _)⟩
+  ⟨a % succ n, Nat.modLt _ (Nat.zeroLtSucc _)⟩
 
 def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
-⟨a % n, Nat.modLt _ h⟩
+  ⟨a % n, Nat.modLt _ h⟩
 
-private theorem mlt {n b : Nat} : ∀ {a}, n > a → b % n < n
-| 0,   h => Nat.modLt _ h
-| a+1, h =>
-  have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
-  Nat.modLt _ this
+private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
+  | 0,   h => Nat.modLt _ h
+  | a+1, h =>
+    have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
+    Nat.modLt _ this
 
 protected def add : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
 
 protected def mul : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
 
 protected def sub : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
 
 /-
 Remark: mod/div/modn/land/lor can be defined without using (% n), but
@@ -64,19 +67,19 @@ needed to boostrap Lean.
 -/
 
 protected def mod : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a % b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a % b) % n, mlt h⟩
 
 protected def div : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a / b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(a / b) % n, mlt h⟩
 
 protected def modn : Fin n → Nat → Fin n
-| ⟨a, h⟩, m => ⟨(a % m) % n, mlt h⟩
+  | ⟨a, h⟩, m => ⟨(a % m) % n, mlt h⟩
 
 def land : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
 
 def lor : Fin n → Fin n → Fin n
-| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
+  | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
 
 instance : HasZero (Fin (succ n)) := ⟨⟨0, succPos n⟩⟩
 instance : HasOne (Fin (succ n))  := ⟨ofNat 1⟩
@@ -88,23 +91,23 @@ instance : HasDiv (Fin n)         := ⟨Fin.div⟩
 instance : HasModN (Fin n)        := ⟨Fin.modn⟩
 
 theorem eqOfVeq : ∀ {i j : Fin n}, (val i) = (val j) → i = j
-| ⟨iv, ilt₁⟩, ⟨.(iv), ilt₂⟩, rfl => rfl
+  | ⟨iv, ilt₁⟩, ⟨_, _⟩, rfl => rfl
 
 theorem veqOfEq : ∀ {i j : Fin n}, i = j → (val i) = (val j)
-| ⟨iv, ilt⟩, .(_), rfl => rfl
+  | ⟨iv, ilt⟩, _, rfl => rfl
 
 theorem neOfVne {i j : Fin n} (h : val i ≠ val j) : i ≠ j :=
-fun h' => absurd (veqOfEq h') h
+  fun h' => absurd (veqOfEq h') h
 
 theorem vneOfNe {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
-fun h' => absurd (eqOfVeq h') h
+  fun h' => absurd (eqOfVeq h') h
 
 theorem modnLt : ∀ {m : Nat} (i : Fin n), m > 0 → (i %ₙ m).val < m
-| m, ⟨a, h⟩, hp =>  Nat.ltOfLeOfLt (modLe _ _) (modLt _ hp)
+  | m, ⟨a, h⟩, hp =>  Nat.ltOfLeOfLt (modLe _ _) (modLt _ hp)
 
 end Fin
 
 open Fin
 
-instance (n : Nat) : DecidableEq (Fin n) :=
-fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩
+instance (n : Nat) : DecidableEq (Fin n) := fun i j =>
+  decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩
diff --git a/src/Init/Data/UInt.lean b/src/Init/Data/UInt.lean
index e1af60c2ac..964b714485 100644
--- a/src/Init/Data/UInt.lean
+++ b/src/Init/Data/UInt.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -11,7 +12,7 @@ open Nat
 
 def uint8Sz : Nat := 256
 structure UInt8 :=
-(val : Fin uint8Sz)
+  (val : Fin uint8Sz)
 
 @[extern "lean_uint8_of_nat"]
 def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
@@ -50,29 +51,31 @@ instance : HasLess UInt8     := ⟨UInt8.lt⟩
 instance : HasLessEq UInt8   := ⟨UInt8.le⟩
 instance : Inhabited UInt8   := ⟨0⟩
 
-
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 == #2"]
 def UInt8.decEq (a b : UInt8) : Decidable (a = b) :=
-UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
-  if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 < #2"]
 def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
-UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n < m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 <= #2"]
 def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
-UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n <= m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance : DecidableEq UInt8 := UInt8.decEq
-instance UInt8.hasDecidableLt (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
-instance UInt8.hasDecidableLe (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
+instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
+instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
 
 def uint16Sz : Nat := 65536
 structure UInt16 :=
-(val : Fin uint16Sz)
+  (val : Fin uint16Sz)
 
 @[extern "lean_uint16_of_nat"]
 def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
@@ -111,28 +114,31 @@ instance : HasLess UInt16     := ⟨UInt16.lt⟩
 instance : HasLessEq UInt16   := ⟨UInt16.le⟩
 instance : Inhabited UInt16   := ⟨0⟩
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 == #2"]
 def UInt16.decEq (a b : UInt16) : Decidable (a = b) :=
-UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
-  if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 < #2"]
 def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
-UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n < m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 <= #2"]
 def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
-UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n <= m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance : DecidableEq UInt16 := UInt16.decEq
-instance UInt16.hasDecidableLt (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
-instance UInt16.hasDecidableLe (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
+instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
+instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
 
 def uint32Sz : Nat := 4294967296
 structure UInt32 :=
-(val : Fin uint32Sz)
+  (val : Fin uint32Sz)
 
 @[extern "lean_uint32_of_nat"]
 def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
@@ -179,20 +185,23 @@ instance : HasLess UInt32     := ⟨UInt32.lt⟩
 instance : HasLessEq UInt32   := ⟨UInt32.le⟩
 instance : Inhabited UInt32   := ⟨0⟩
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 == #2"]
 def UInt32.decEq (a b : UInt32) : Decidable (a = b) :=
-UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
-  if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 < #2"]
 def UInt32.decLt (a b : UInt32) : Decidable (a < b) :=
-UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n < m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 <= #2"]
 def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
-UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n <= m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 @[extern c inline "#1 << #2"]
 constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
@@ -200,12 +209,12 @@ constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
 constant UInt32.shiftRight (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
 
 instance : DecidableEq UInt32 := UInt32.decEq
-instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
-instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
+instance (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
+instance (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
 
 def uint64Sz : Nat := 18446744073709551616
 structure UInt64 :=
-(val : Fin uint64Sz)
+  (val : Fin uint64Sz)
 
 @[extern "lean_uint64_of_nat"]
 def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
@@ -261,31 +270,34 @@ instance : Inhabited UInt64   := ⟨0⟩
 @[extern c inline "(uint64_t)#1"]
 def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 == #2"]
 def UInt64.decEq (a b : UInt64) : Decidable (a = b) :=
-UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
-  if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 < #2"]
 def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
-UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n < m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 <= #2"]
 def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
-UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n <= m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance : DecidableEq UInt64 := UInt64.decEq
-instance UInt64.hasDecidableLt (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
-instance UInt64.hasDecidableLe (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
+instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
+instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
 
 def usizeSz : Nat := (2:Nat) ^ System.Platform.numBits
 structure USize :=
-(val : Fin usizeSz)
+  (val : Fin usizeSz)
 
 theorem usizeSzGt0 : usizeSz > 0 :=
-Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
+  Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
 
 @[extern "lean_usize_of_nat"]
 def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usizeSzGt0⟩
@@ -336,24 +348,27 @@ instance : HasLess USize     := ⟨USize.lt⟩
 instance : HasLessEq USize   := ⟨USize.le⟩
 instance : Inhabited USize   := ⟨0⟩
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 == #2"]
 def USize.decEq (a b : USize) : Decidable (a = b) :=
-USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
-  if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 < #2"]
 def USize.decLt (a b : USize) : Decidable (a < b) :=
-USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n < m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
 
+set_option bootstrap.gen_matcher_code false in
 @[extern c inline "#1 <= #2"]
 def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
-USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
-  inferInstanceAs (Decidable (n <= m))
+  match a, b with
+  | ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
 
 instance : DecidableEq USize := USize.decEq
-instance USize.hasDecidableLt (a b : USize) : Decidable (a < b) := USize.decLt a b
-instance USize.hasDecidableLe (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
+instance (a b : USize) : Decidable (a < b) := USize.decLt a b
+instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
 
 theorem USize.modnLt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u %ₙ m) < m
-| ⟨u⟩, h => Fin.modnLt u h
+  | ⟨u⟩, h => Fin.modnLt u h