From c080d426927b44afdabdb623f0842f4b800d6d74 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Sep 2020 10:16:15 -0700 Subject: [PATCH] chore: move tests to new frontend --- tests/lean/run/structInst3.lean | 2 +- tests/lean/run/structInst4.lean | 3 +-- tests/lean/run/struct_inst_typed.lean | 1 + tests/lean/run/struct_instance_in_eqn.lean | 4 ++-- tests/lean/run/structure.lean | 1 + tests/lean/run/synth1.lean | 9 +++++++-- tests/lean/run/tactic.lean | 6 ++++-- tests/lean/run/task_test.lean | 2 ++ tests/lean/run/task_test2.lean | 2 ++ tests/lean/run/termElab.lean | 3 +-- tests/lean/run/termParserAttr.lean | 3 +-- tests/lean/run/termparsertest1.lean | 1 + 12 files changed, 24 insertions(+), 13 deletions(-) diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean index a54ab755d1..2405b964bf 100644 --- a/tests/lean/run/structInst3.lean +++ b/tests/lean/run/structInst3.lean @@ -1,3 +1,4 @@ +new_frontend universes u namespace Ex1 @@ -13,7 +14,6 @@ structure C (α : Type u) extends B α := end Ex1 -new_frontend open Ex1 def c1 : C Nat := { x := 1 } diff --git a/tests/lean/run/structInst4.lean b/tests/lean/run/structInst4.lean index a0eefded0c..8e84609a7c 100644 --- a/tests/lean/run/structInst4.lean +++ b/tests/lean/run/structInst4.lean @@ -1,3 +1,4 @@ +new_frontend universes u def a : Array ((Nat × Nat) × Bool) := #[] @@ -7,8 +8,6 @@ structure Foo := (x : Array ((Nat × Nat) × Bool) := #[]) (y : Nat := 0) -new_frontend - #check (b).modifyOp (idx := 1) (fun s => 2) #check { b with [1] := 2 } diff --git a/tests/lean/run/struct_inst_typed.lean b/tests/lean/run/struct_inst_typed.lean index dcbd2d43c1..646beb5126 100644 --- a/tests/lean/run/struct_inst_typed.lean +++ b/tests/lean/run/struct_inst_typed.lean @@ -1,3 +1,4 @@ +new_frontend #check { fst := 10, snd := 20 : Nat × Nat } structure S := diff --git a/tests/lean/run/struct_instance_in_eqn.lean b/tests/lean/run/struct_instance_in_eqn.lean index 7d561bda55..44e64f92dd 100644 --- a/tests/lean/run/struct_instance_in_eqn.lean +++ b/tests/lean/run/struct_instance_in_eqn.lean @@ -1,7 +1,7 @@ +new_frontend + structure S := (x : Nat) (y : Bool) (z : Nat) (w : Nat) -set_option trace.compiler.stage1 true - def g : S → S | s@{ x := x, ..} => { s with x := x + 1 } diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean index c00bd5bdaa..97ce2dd9cc 100644 --- a/tests/lean/run/structure.lean +++ b/tests/lean/run/structure.lean @@ -1,4 +1,5 @@ import Lean +new_frontend open Lean structure S1 := diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean index 28faf0b083..c0a8face9a 100644 --- a/tests/lean/run/synth1.lean +++ b/tests/lean/run/synth1.lean @@ -1,4 +1,5 @@ import Lean.Meta +new_frontend open Lean open Lean.Meta @@ -26,14 +27,14 @@ instance coerceNatToInt : HasCoerce Nat Int := def print {α} [HasToString α] (a : α) : MetaM Unit := trace! `Meta.synthInstance (toString a) -set_option trace.Meta.synthInstance true -set_option trace.Meta.synthInstance.tryResolve false def tst1 : MetaM Unit := do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero]; r ← synthInstance inst; print r +set_option trace.Meta.synthInstance true in +set_option trace.Meta.synthInstance.tryResolve false in #eval tst1 def tst2 : MetaM Unit := @@ -46,6 +47,8 @@ do inst ← mkAppM `HasBind #[mkConst `IO]; print r; pure () +set_option trace.Meta.synthInstance true in +set_option trace.Meta.synthInstance.tryResolve false in #eval tst2 def tst3 : MetaM Unit := @@ -54,4 +57,6 @@ do inst ← mkAppM `HasBeq #[mkConst `Nat]; print r; pure () +set_option trace.Meta.synthInstance true in +set_option trace.Meta.synthInstance.tryResolve false in #eval tst3 diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean index 8a1db54e60..cbeb8e1cd2 100644 --- a/tests/lean/run/tactic.lean +++ b/tests/lean/run/tactic.lean @@ -1,4 +1,6 @@ import Lean.Meta +new_frontend + open Lean open Lean.Meta @@ -7,8 +9,6 @@ axiom simple : forall {p q : Prop}, p → q → p def print (msg : MessageData) : MetaM Unit := trace! `Meta.Tactic msg -set_option trace.Meta.Tactic true - def tst1 : MetaM Unit := do cinfo ← getConstInfo `simple; mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type; @@ -18,4 +18,6 @@ do cinfo ← getConstInfo `simple; result ← instantiateMVars mvar; print result +set_option trace.Meta.Tactic true + #eval tst1 diff --git a/tests/lean/run/task_test.lean b/tests/lean/run/task_test.lean index 3b1d6136d1..068e75be54 100644 --- a/tests/lean/run/task_test.lean +++ b/tests/lean/run/task_test.lean @@ -1,3 +1,5 @@ +new_frontend + def g (x : Nat) : Nat := dbgTrace ("g: " ++ toString x) $ fun _ => x + 1 diff --git a/tests/lean/run/task_test2.lean b/tests/lean/run/task_test2.lean index e2787a47a0..2899083c56 100644 --- a/tests/lean/run/task_test2.lean +++ b/tests/lean/run/task_test2.lean @@ -1,3 +1,5 @@ +new_frontend + def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat := n.repeat (fun r => dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ fun _ => diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean index 87de15ec89..34c30fd3d3 100644 --- a/tests/lean/run/termElab.lean +++ b/tests/lean/run/termElab.lean @@ -1,11 +1,10 @@ import Lean +new_frontend open Lean open Lean.Elab open Lean.Elab.Term -set_option trace.Elab.debug true - def tst1 : TermElabM Unit := do opt ← getOptions; stx ← `(forall (a b : Nat), Nat); diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean index 8e8f8e7597..75fe005cd7 100644 --- a/tests/lean/run/termParserAttr.lean +++ b/tests/lean/run/termParserAttr.lean @@ -1,4 +1,5 @@ import Lean +new_frontend open Lean open Lean.Elab @@ -61,8 +62,6 @@ adaptExpander $ fun stx => match_syntax stx with #eval run "#check (| id 1 |)" #eval run "#check (| id 1, id 2 |)" -new_frontend - declare_syntax_cat foo syntax "⟨|" term "|⟩" : foo diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean index 3ad94c1027..8c80fccd09 100644 --- a/tests/lean/run/termparsertest1.lean +++ b/tests/lean/run/termparsertest1.lean @@ -1,4 +1,5 @@ import Lean.Parser.Term +new_frontend open Lean open Lean.Parser