chore: moving tests to new frontend

@Kha The transition has begun :)
I found and fixed a few bugs, but it is going well so far.

tests/lean/run/121.lean

@@ -1,10 +1,7 @@
+new_frontend
+
 abbrev DelabM := Id
 abbrev Delab := DelabM Nat
 
-example : DelabM Nat := pure 1  -- works
-example : Delab      := pure 1  -- works
-
-new_frontend
-
 example : DelabM Nat := pure 1  -- works
 example : Delab := pure 1       -- works

tests/lean/run/125.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 class HasElems (α : Type) : Type := (elems : Array α)
 def elems (α : Type) [HasElems α] : Array α := HasElems.elems
 

tests/lean/run/1954.lean

@@ -1,2 +1,4 @@
+new_frontend
+
 def all (p : Nat → Prop) : Prop := ∀x, p x
 example {p : Nat → Prop} (h : all p) : p 0 := h 0

tests/lean/run/1968.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 inductive type
 | bv  : Nat → type
 | bit : type
@@ -7,8 +9,8 @@ open type
 -- This is a "parameterized List" where `plist f types` contains
 -- an element of Type `f tp` for each corresponding element `tp ∈ types`.
 inductive plist (f : type → Type) : List type → Type
-| nil {} : plist []
-| cons {h:type} {r:List type} : f h → plist r → plist (h::r)
+| nil {} : plist f []
+| cons {h:type} {r:List type} : f h → plist f r → plist f (h::r)
 
 -- Operations on values; the first argument contains the types of
 -- inputs, and the second for the return Type.

tests/lean/run/28.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 structure bv (w : Nat) := (u:Unit)
 
 inductive val : Type
@@ -11,24 +13,19 @@ inductive instr : Type
 | store : Unit -> Unit -> Unit -> instr
 
 structure sim (a:Type) :=
-  (runSim :
-     ∀{z:Type},
-     (IO.Error → z)  /- error continuation -/ →
-     (a → z) /- normal continuation -/ →
-     z)
+(runSim : {z:Type} → (IO.Error → z) /- error continuation -/ → (a → z) /- normal continuation -/ →  z)
 
 instance monad : Monad sim :=
-  { bind := λa b mx mf => sim.mk (λz kerr k =>
-       mx.runSim kerr (λx => (mf x).runSim kerr k))
-  , pure := λa x => sim.mk (λz _ k => k x)
-  }
+{ bind := λ mx mf => sim.mk (λ kerr k =>
+       mx.runSim kerr (λx => (mf x).runSim kerr k)),
+  pure := fun a => sim.mk $ fun _ k => k a }
 
 instance monadExcept : MonadExcept IO.Error sim :=
-  { throw := λa err => sim.mk (λz kerr _k => kerr err)
-  , catch := λa m handle => sim.mk (λz kerr k =>
+{ throw := λ err => sim.mk (λ kerr _k => kerr err),
+  catch := λ m handle => sim.mk (λ kerr k =>
       let kerr' := λerr => (handle err).runSim kerr k;
       m.runSim kerr' k)
-  }.
+  }
 
 def f : sim val := throw (IO.userError "ASDF")
 def g : sim Unit := throw (IO.userError "ASDF")

tests/lean/run/34.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 partial def foo : ∀ (n : Nat), StateM Unit Unit
 | n =>
   if n == 0 then pure () else

tests/lean/run/CoeNew.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 universes u v w
 
 instance boolToNat : Coe Bool Nat :=
@@ -15,7 +17,6 @@ structure ConstantFunction (α β : Type) :=
 instance constantFunctionCoe {α β : Type} : CoeFun (ConstantFunction α β) (fun _ => α → β) :=
 { coe := fun c => c.f }
 
-new_frontend
 set_option pp.implicit true
 
 #synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Nat

tests/lean/run/DefEqAssignBug.lean

@@ -1,4 +1,7 @@
 import Lean.Meta
+
+new_frontend
+
 open Lean
 open Lean.Meta
 

tests/lean/run/IO_test.lean

@@ -2,6 +2,8 @@ prelude
 import Init.System.IO
 import Init.Data.List.Control
 
+new_frontend
+
 open IO.FS
 
 instance : HasRepr UInt8 := ⟨ toString ⟩

tests/lean/run/Reformat.lean

@@ -1,6 +1,6 @@
 /-! Parse and reformat file -/
 import Lean.PrettyPrinter
-
+new_frontend
 open Lean
 open Lean.Elab
 open Lean.Elab.Term

tests/lean/run/Reid1.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 structure ConstantFunction (α β : Type) :=
 (f : α → β)
 (h : ∀ a₁ a₂, f a₁ = f a₂)
@@ -13,8 +15,6 @@ def myFun' (α : Type) : ConstantFunction α (Option α) :=
 { f := fun a => none,
   h := fun a₁ a₂ => rfl }
 
-new_frontend
-
 set_option pp.all true
 
 #check myFun 3       -- works

tests/lean/run/Reparen.lean

@@ -1,6 +1,6 @@
 /-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
 import Lean.Parser
-
+new_frontend
 open Lean
 open Lean.Format
 
@@ -44,8 +44,6 @@ IO.println f;
 when (stx != stx') $
   throwError "reparenthesization failed"
 
-new_frontend
-
 open Lean
 
 syntax:80 term " ^~ " term:80 : term

tests/lean/run/anonymous_ctor_error_msg.lean

@@ -1,10 +1,10 @@
+new_frontend
+
 structure Foo := (n : Nat)
 
 def Foo.sum (xs : List Foo) : Foo :=
 xs.foldl (λ s x => ⟨s.n + x.n⟩) ⟨0⟩
 
-new_frontend
-
 #check
 let x1 := ⟨1⟩;
 let x2 := ⟨2⟩;

tests/lean/run/array1.lean

@@ -1,3 +1,4 @@
+new_frontend
 #check @Array.mk
 
 def v : Array Nat := @Array.mk Nat 10 (fun ⟨i, _⟩ => i)
@@ -5,8 +6,10 @@ def v : Array Nat := @Array.mk Nat 10 (fun ⟨i, _⟩ => i)
 def w : Array Nat :=
 (mkArray 9 1).push 3
 
+#check @Array.casesOn
+
 def f : Fin w.sz → Nat :=
-Array.casesOn w (fun _ f => f)
+@Array.casesOn _ (fun w => Fin w.sz → Nat)  w (fun _ f => f)
 
 def arraySum (a : Array Nat) : Nat :=
 a.foldl Nat.add 0
@@ -46,10 +49,10 @@ def tst : IO (List Nat) :=
 
 #eval tst
 
-#eval #[1, 3, 6, 2].getMax? (fun a b => a < b)
-#eval #[].getMax? (fun (a b : Nat) => a < b)
-#eval #[1, 8].getMax? (fun a b => a < b)
-#eval #[8, 1].getMax? (fun a b => a < b)
+#eval #[1, 3, 6, 2].getMax? (fun a b => decide $ a < b)
+#eval #[].getMax? (fun (a b : Nat) => decide $ a < b)
+#eval #[1, 8].getMax? (fun a b => decide $ a < b)
+#eval #[8, 1].getMax? (fun a b => decide $ a < b)
 
 #eval #[1, 6, 5, 3, 8, 2, 0].partition fun x => x % 2 == 0
 

tests/lean/run/backtrackable_estate.lean

@@ -1,4 +1,5 @@
 import Init.System.IO
+new_frontend
 
 structure MyState :=
 (bs : Nat := 0) -- backtrackable state

tests/lean/run/bigmul.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 @[noinline] def f (x : Nat) :=
 1000000000000000000000000000000
 

tests/lean/run/bigop.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 def Seq (α : Type) := List α
 
 def BigBody (β α) :=  α × (β → β → β) × Bool × β
@@ -11,7 +13,7 @@ r.foldr (applyBig ∘ body) idx
 
 def bigop := @reducebig
 
-def iota : Nat → Nat → List Nat
+partial def iota : Nat → Nat → List Nat
 | m, 0   => []
 | m, n+1 => m :: iota (m+1) n
 
@@ -26,11 +28,11 @@ instance : Enumerable Bool :=
 instance {α β} [Enumerable α] [Enumerable β]: Enumerable (α × β) :=
 { elems := do a ← Enumerable.elems α; b ← Enumerable.elems β; pure (a, b) }
 
-def finElemsAux (n : Nat) : forall (i : Nat), i < n → List (Fin n)
+partial def finElemsAux (n : Nat) : (i : Nat) → i < n → List (Fin n)
 | 0,   h => [⟨0, h⟩]
-| i+1, h => ⟨i+1, h⟩ :: finElemsAux i (Nat.ltOfSuccLt h)
+| i+1, h => ⟨i+1, h⟩ :: finElemsAux n i (Nat.ltOfSuccLt h)
 
-def finElems : forall (n : Nat), List (Fin n)
+partial def finElems : (n : Nat) → List (Fin n)
 | 0     => []
 | (n+1) => finElemsAux (n+1) n (Nat.ltSuccSelf n)
 
@@ -40,8 +42,6 @@ instance {n} : Enumerable (Fin n) :=
 instance {n} : HasOfNat (Fin (Nat.succ n)) :=
 ⟨Fin.ofNat⟩
 
-new_frontend
-
 -- Declare a new syntax category for "indexing" big operators
 declare_syntax_cat index
 syntax term:51 "≤" ident "<" term : index

tests/lean/run/borrowBug.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 @[noinline] def g (x : Nat) : Nat × Nat := (x, x)
 @[noinline] def p (x : Nat) : Bool := x > 10
 

tests/lean/run/catchThe.lean

@@ -1,4 +1,5 @@
 import Lean.Meta
+new_frontend
 open Lean
 open Lean.Meta
 

tests/lean/run/check.lean

@@ -1,3 +1,4 @@
+new_frontend
 --
 
 #check And.intro

tests/lean/run/closure1.lean

@@ -1,12 +1,13 @@
 import Lean
+new_frontend
 open Lean
 open Lean.Meta
 
 universes u
 
 inductive Vec (α : Type u) : Nat → Type u
-| nil      : Vec 0
-| cons {n} : α → Vec n → Vec (n+1)
+| nil      : Vec α 0
+| cons {n} : α → Vec α n → Vec α (n+1)
 
 set_option trace.Meta.debug true
 

tests/lean/run/coeIssue1.lean

@@ -1,5 +1,6 @@
 -- From @joehendrix
 -- The imul doesn't type check as Lean won't try to coerce from a reg (bv 64) to a expr (bv ?u)
+new_frontend
 
 inductive MCType
 | bv : Nat → MCType
@@ -35,8 +36,6 @@ to synthesize the instance.
 -/
 def sext {s:Nat} (x : Expr (bv s)) (n:Nat) : Expr (bv (s+n)) := Expr.sextC x (s+n)
 
-new_frontend
-
 open MCType
 
 variables {u:Nat} (e : Expr (bv 64))

tests/lean/run/coeIssue2.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 structure A :=
 (a : Nat)
 
@@ -8,9 +10,8 @@ structure C :=
 (a : Nat)
 
 instance : Coe A B := ⟨fun s => ⟨s.1⟩⟩
-instance : Coe A C := ⟨fun s => ⟨s.1⟩⟩
 
-new_frontend
+instance : Coe A C := ⟨fun s => ⟨s.1⟩⟩
 
 def f {α} (a b : α) := a
 def forceB {α} (b : B) (a : α) := a

tests/lean/run/coeIssue3.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 structure Var : Type := (name : String)
 instance Var.nameCoe : Coe String Var := ⟨Var.mk⟩
 
@@ -7,13 +9,11 @@ structure B : Type := (u : Unit)
 def a : A := A.mk ()
 def b : B := B.mk ()
 
-def Foo.chalk : A → List Var → Unit := λ _ _ => ()
-def Bar.chalk : B → Unit := λ _ => ()
+def Foo.chalk : A → List Var → Unit := fun _ _ => ()
+def Bar.chalk : B → Unit := fun _ => ()
 
 instance listCoe {α β} [Coe α β] : Coe (List α) (List β) :=
-⟨fun as => as.map (fun a => coe a)⟩
-
-new_frontend
+⟨fun as => as.map fun a => coe a⟩
 
 open Foo
 open Bar

tests/lean/run/coeIssues4.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 def f : List Int → Bool := fun _ => true
 
 def ex3 : IO Bool :=
@@ -13,8 +15,6 @@ instance : Coe Nat Expr := ⟨Expr.val⟩
 
 def foo : Expr → Expr := fun e => e
 
-new_frontend
-
 def ex1 : Bool :=
 f [1, 2, 3]  -- Works
 

tests/lean/run/coeSort2.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 universe u
 
 structure Group :=
@@ -6,8 +8,6 @@ structure Group :=
 instance GroupToType : CoeSort Group (Type u) :=
 CoeSort.mk (fun g => g.carrier)
 
-new_frontend
-
 variable (g : Group.{1})
 
 #check fun (a b : g) => g.mul a b

tests/lean/run/compiler_proj_bug.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 structure S :=
 (a : Nat) (h : a > 0) (b : Nat)
 

tests/lean/run/core.lean

@@ -1,4 +1,5 @@
 import Lean.CoreM
+new_frontend
 open Lean
 open Lean.Core
 

tests/lean/run/coroutine.lean

@@ -1,202 +0,0 @@
-universes u v w r s
-
-inductive coroutineResultCore (coroutine : Type (max u v w)) (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
-| done     : β → coroutineResultCore
-| yielded  : δ → coroutine → coroutineResultCore
-
-/--
-   Asymmetric coroutines `coroutine α δ β` takes inputs of Type `α`, yields elements of Type `δ`,
-   and produces an element of Type `β`.
-
-   Asymmetric coroutines are so called because they involve two types of control transfer operations:
-   one for resuming/invoking a coroutine and one for suspending it, the latter returning
-   control to the coroutine invoker. An asymmetric coroutine can be regarded as subordinate
-   to its caller, the relationship between them being similar to that between a called and
-   a calling routine.
- -/
-inductive coroutine (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
-| mk    : (α → coroutineResultCore coroutine α δ β) → coroutine
-
-abbrev coroutineResult (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) :=
-coroutineResultCore (coroutine α δ β) α δ β
-
-namespace coroutine
-variables {α : Type u} {δ : Type v} {β γ : Type w}
-
-export coroutineResultCore (done yielded)
-
-/-- `resume c a` resumes/invokes the coroutine `c` with input `a`. -/
-@[inline] def resume : coroutine α δ β → α → coroutineResult α δ β
-| mk k,   a => k a
-
-@[inline] protected def pure (b : β) : coroutine α δ β :=
-mk $ fun _ => done b
-
-/-- Read the input argument passed to the coroutine.
-    Remark: should we use a different Name? I added an instance [MonadReader] later. -/
-@[inline] protected def read : coroutine α δ α :=
-mk $ fun a => done a
-
-/-- Run nested coroutine with transformed input argument. Like `ReaderT.adapt`, but
-    cannot change the input Type. -/
-@[inline] protected def adapt (f : α → α) (c : coroutine α δ β) : coroutine α δ β :=
-mk $ fun a => c.resume (f a)
-
-/-- Return the control to the invoker with Result `d` -/
-@[inline] protected def yield (d : δ) : coroutine α δ PUnit :=
-mk $ fun a => yielded d (coroutine.pure ⟨⟩)
-
-/-
-TODO(Leo): following relations have been commented because Lean4 is currently
-accepting non-terminating programs.
-
-/-- Auxiliary relation for showing that bind/pipe terminate -/
-inductive directSubcoroutine : coroutine α δ β → coroutine α δ β → Prop
-| mk : ∀ (k : α → coroutineResult α δ β) (a : α) (d : δ) (c : coroutine α δ β), k a = yielded d c → directSubcoroutine c (mk k)
-
-theorem directSubcoroutineWf : WellFounded (@directSubcoroutine α δ β) :=
-by {
-  constructor, intro c,
-  apply @coroutine.ind _ _ _
-          (fun c => Acc directSubcoroutine c)
-          (fun r => ∀ (d : δ) (c : coroutine α δ β), r = yielded d c → Acc directSubcoroutine c),
-  { intros k ih, dsimp at ih, Constructor, intros c' h, cases h, apply ih hA hD, assumption },
-  { intros, contradiction },
-  { intros d c ih d₁ c₁ Heq, injection Heq, subst c, assumption }
-}
-
-/-- Transitive closure of directSubcoroutine. It is not used here, but may be useful when defining
-    more complex procedures. -/
-def subcoroutine : coroutine α δ β → coroutine α δ β → Prop :=
-Tc directSubcoroutine
-
-theorem subcoroutineWf : WellFounded (@subcoroutine α δ β) :=
-Tc.wf directSubcoroutineWf
-
--- Local instances for proving termination by well founded relation
-
-def bindWfInst : HasWellFounded (Σ' a : coroutine α δ β, (β → coroutine α δ γ)) :=
-{ r  := Psigma.Lex directSubcoroutine (fun _ => emptyRelation),
-  wf := Psigma.lexWf directSubcoroutineWf (fun _ => emptyWf) }
-
-def pipeWfInst : HasWellFounded (Σ' a : coroutine α δ β, coroutine δ γ β) :=
-{ r  := Psigma.Lex directSubcoroutine (fun _ => emptyRelation),
-  wf := Psigma.lexWf directSubcoroutineWf (fun _ => emptyWf) }
-
-local attribute [instance] wfInst₁ wfInst₂
-
-open wellFoundedTactics
-
--/
-
-/- TODO: remove `unsafe` keyword after we restore well-founded recursion -/
-
-@[inlineIfReduce] protected unsafe def bind : coroutine α δ β → (β → coroutine α δ γ) → coroutine α δ γ
-| mk k,   f => mk $ fun a =>
-    match k a, rfl : ∀ (n : _), n = k a → _ with
-    | done b, _      => coroutine.resume (f b) a
-    | yielded d c, h =>
-      -- have directSubcoroutine c (mk k), { apply directSubcoroutine.mk k a d, rw h },
-      yielded d (bind c f)
---  usingWellFounded { decTac := unfoldWfRel >> processLex (tactic.assumption) }
-
-unsafe def pipe : coroutine α δ β → coroutine δ γ β → coroutine α γ β
-| mk k₁,   mk k₂   => mk $ fun a =>
-  match k₁ a, rfl : ∀ (n : _), n = k₁ a → _ with
-  | done b, h        => done b
-  | yielded d k₁', h =>
-    match k₂ d with
-    | done b        => done b
-    | yielded r k₂' =>
-      -- have directSubcoroutine k₁' (mk k₁), { apply directSubcoroutine.mk k₁ a d, rw h },
-      yielded r (pipe k₁' k₂')
--- usingWellFounded { decTac := unfoldWfRel >> processLex (tactic.assumption) }
-
-private unsafe def finishAux (f : δ → α) : coroutine α δ β → α → List δ → List δ × β
-| mk k,   a, ds =>
-  match k a with
-  | done b       => (ds.reverse, b)
-  | yielded d k' => finishAux k' (f d) (d::ds)
-
-/-- Run a coroutine to completion, feeding back yielded items after transforming them with `f`. -/
-unsafe def finish (f : δ → α) : coroutine α δ β → α → List δ × β :=
-fun k a => finishAux f k a []
-
-unsafe instance : Monad (coroutine α δ) :=
-{ pure := @coroutine.pure _ _,
-  bind := @coroutine.bind _ _ }
-
-unsafe instance : MonadReaderOf α (coroutine α δ) :=
-{ read := @coroutine.read _ _ }
-
-end coroutine
-
-/-- Auxiliary class for lifiting `yield` -/
-class monadCoroutine (α : outParam (Type u)) (δ : outParam (Type v)) (m : Type w → Type r) :=
-(yield : δ → m PUnit)
-
-instance (α : Type u) (δ : Type v) : monadCoroutine α δ (coroutine α δ) :=
-{ yield  := coroutine.yield }
-
-instance monadCoroutineTrans (α : Type u) (δ : Type v) (m : Type w → Type r) (n : Type w → Type s)
-                               [monadCoroutine α δ m] [MonadLift m n] : monadCoroutine α δ n :=
-{ yield := fun d => monadLift (monadCoroutine.yield d : m _) }
-
-export monadCoroutine (yield)
-
-open coroutine
-
-namespace ex1
-
-inductive tree (α : Type u)
-| leaf  : tree
-| Node  : tree → α → tree → tree
-
-/-- Coroutine as generators/iterators -/
-unsafe def visit {α : Type v} : tree α → coroutine Unit α Unit
-| tree.leaf         => pure ()
-| tree.Node l a r   => do
-  visit l;
-  yield a;
-  visit r
-
-unsafe def tst {α : Type} [HasToString α] (t : tree α) : IO Unit :=
-do c  ← pure $ visit t;
-   (yielded v₁ c) ← pure (resume c ()) | throw $ IO.userError "failed";
-   (yielded v₂ c) ← pure (resume c ()) | throw $ IO.userError "failed";
-   IO.println $ toString v₁;
-   IO.println $ toString v₂;
-   pure ()
-
--- #eval tst (tree.Node (tree.Node (tree.Node tree.leaf 5 tree.leaf) 10 (tree.Node tree.leaf 20 tree.leaf)) 30 tree.leaf)
-
-end ex1
-
-namespace ex2
-
-unsafe def ex : StateT Nat (coroutine Nat String) Unit :=
-do
-  x ← read;
-  y ← get;
-  set (y+5);
-  yield ("1) val: " ++ toString (x+y));
-  x ← read;
-  y ← get;
-  yield ("2) val: " ++ toString (x+y));
-  pure ()
-
-unsafe def tst2 : IO Unit :=
-do let c := StateT.run ex 5;
-   (yielded r c₁) ← pure $ resume c 10 | throw $ IO.userError "failed";
-   IO.println r;
-   (yielded r c₂) ← pure $ resume c₁ 20 | throw $ IO.userError "failed";
-   IO.println r;
-   (done _) ← pure $ resume c₂ 30 | throw $ IO.userError "failed";
-   (yielded r c₃) ← pure $ resume c₁ 100 | throw $ IO.userError "failed";
-   IO.println r;
-   IO.println "done";
-   pure ()
-
--- #eval tst2
-
-end ex2

tests/lean/run/csimp_type_error.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 namespace scratch
 
 inductive type