From e3fb7010f18389e06bb163a0cc2a22050e960346 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Nov 2020 09:25:45 -0800 Subject: [PATCH] chore: fix tests --- tests/compiler/foreign/main.lean | 12 +++++------ tests/compiler/lazylist.lean | 2 +- tests/lean/run/1385.lean | 8 ++++---- tests/lean/run/def12.lean | 12 +++++------ tests/lean/run/depElim1.lean | 34 ++++++++++++++++---------------- tests/lean/run/fun.lean | 10 +++++----- tests/lean/run/optParam.lean | 6 +++--- tests/lean/zipper.lean | 4 +--- 8 files changed, 42 insertions(+), 46 deletions(-) diff --git a/tests/compiler/foreign/main.lean b/tests/compiler/foreign/main.lean index bc559a5d60..050916d15a 100644 --- a/tests/compiler/foreign/main.lean +++ b/tests/compiler/foreign/main.lean @@ -3,13 +3,13 @@ constant SPointed : PointedType def S : Type := SPointed.type instance : Inhabited S := ⟨SPointed.val⟩ -@[extern "lean_mk_S"] constant mkS (x y : UInt32) (s : @& String) : S := arbitrary _ -@[extern "lean_S_add_x_y"] constant S.addXY (s : @& S) : UInt32 := arbitrary _ -@[extern "lean_S_string"] constant S.string (s : @& S) : String := arbitrary _ +@[extern "lean_mk_S"] constant mkS (x y : UInt32) (s : @& String) : S +@[extern "lean_S_add_x_y"] constant S.addXY (s : @& S) : UInt32 +@[extern "lean_S_string"] constant S.string (s : @& S) : String -- The following 3 externs have side effects. Thus, we put them in IO. -@[extern "lean_S_global_append"] constant appendToGlobalS (str : @& String) : IO Unit := arbitrary _ -@[extern "lean_S_global_string"] constant getGlobalString : IO String := arbitrary _ -@[extern "lean_S_update_global"] constant updateGlobalS (s : @& S) : IO Unit := arbitrary _ +@[extern "lean_S_global_append"] constant appendToGlobalS (str : @& String) : IO Unit +@[extern "lean_S_global_string"] constant getGlobalString : IO String +@[extern "lean_S_update_global"] constant updateGlobalS (s : @& S) : IO Unit def main : IO Unit := do IO.println (mkS 10 20 "hello").addXY; diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean index 9c36e76917..4c0df537d4 100644 --- a/tests/compiler/lazylist.lean +++ b/tests/compiler/lazylist.lean @@ -36,7 +36,7 @@ partial def toList : LazyList α → List α | delayed as => toList as.get partial def head [Inhabited α] : LazyList α → α -| nil => arbitrary α +| nil => arbitrary | cons a as => a | delayed as => head as.get diff --git a/tests/lean/run/1385.lean b/tests/lean/run/1385.lean index 65cae3cb28..323a0fa7fe 100644 --- a/tests/lean/run/1385.lean +++ b/tests/lean/run/1385.lean @@ -10,13 +10,13 @@ inductive Op : (ishapes : List S) → (oshape : S) → Type | gemm : {m n p : Nat} → Op [[m, n], [n, p]] [m, p] def Op.f : {ishapes : List S} → {oshape : S} → Op ishapes oshape → T oshape - | [shape, _], _, binary _ => arbitrary _ - | [[m, n], [_, p]], [_, _], gemm => arbitrary _ + | [shape, _], _, binary _ => arbitrary + | [[m, n], [_, p]], [_, _], gemm => arbitrary #print Op.f def Op.f2 : {ishapes : List S} → {oshape : S} → Op ishapes oshape → T oshape - | _, _, binary _ => arbitrary _ - | _, _, gemm => arbitrary _ + | _, _, binary _ => arbitrary + | _, _, gemm => arbitrary #print Op.f2 diff --git a/tests/lean/run/def12.lean b/tests/lean/run/def12.lean index d3d731eea8..77db02a015 100644 --- a/tests/lean/run/def12.lean +++ b/tests/lean/run/def12.lean @@ -1,10 +1,8 @@ - - def diag : Bool → Bool → Bool → Nat | b, true, false => 1 | false, b, true => 2 | true, false, b => 3 -| b1, b2, b3 => arbitrary Nat +| b1, b2, b3 => arbitrary theorem diag1 (a : Bool) : diag a true false = 1 := match a with @@ -17,16 +15,16 @@ by cases a; exact rfl; exact rfl theorem diag3 (a : Bool) : diag true false a = 3 := by cases a; exact rfl; exact rfl -theorem diag4_1 : diag false false false = arbitrary Nat := +theorem diag4_1 : diag false false false = arbitrary := rfl -theorem diag4_2 : diag true true true = arbitrary Nat := +theorem diag4_2 : diag true true true = arbitrary := rfl def f : Nat → Nat → Nat | n, 0 => 0 | 0, n => 1 -| n, m => arbitrary Nat +| n, m => arbitrary theorem f_zero_right : (a : Nat) → f a 0 = 0 | 0 => rfl @@ -35,7 +33,7 @@ theorem f_zero_right : (a : Nat) → f a 0 = 0 theorem f_zero_succ (a : Nat) : f 0 (a+1) = 1 := rfl -theorem f_succ_succ (a b : Nat) : f (a+1) (b+1) = arbitrary Nat := +theorem f_succ_succ (a b : Nat) : f (a+1) (b+1) = arbitrary := rfl def app {α} : List α → List α → List α diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean index e28e0a49e5..148e9932d7 100644 --- a/tests/lean/run/depElim1.lean +++ b/tests/lean/run/depElim1.lean @@ -181,7 +181,7 @@ if worked then throwError "unexpected success" def ex0 (x : Nat) : LHS (forall (y : Nat), Pat y) -:= arbitrary _ +:= arbitrary #eval test `ex0 1 `elimTest0 #print elimTest0 @@ -191,7 +191,7 @@ def ex1 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) : × LHS (forall (a : α) (as : List α) (b : β) (bs : List β), Pat (a::as) × Pat (b::bs)) × LHS (forall (a : α) (as : List α), Pat (a::as) × Pat ([] : List β)) × LHS (forall (b : β) (bs : List β), Pat ([] : List α) × Pat (b::bs)) -:= arbitrary _ +:= arbitrary #eval test `ex1 2 `elimTest1 @@ -204,7 +204,7 @@ inductive Vec (α : Type u) : Nat → Type u def ex2 (α : Type u) (n : Nat) (xs : Vec α n) (ys : Vec α n) : LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0) × Pat (Vec.nil : Vec α 0)) × LHS (forall (n : Nat) (x : α) (xs : Vec α n) (y : α) (ys : Vec α n), Pat (inaccessible (n+1)) × Pat (Vec.cons x xs) × Pat (Vec.cons y ys)) := -arbitrary _ +arbitrary #eval test `ex2 3 `elimTest2 #print elimTest2 @@ -214,7 +214,7 @@ def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) : × LHS (forall (a : α) (b : β), Pat [a] × Pat [b]) × LHS (forall (a₁ a₂ : α) (as : List α) (b₁ b₂ : β) (bs : List β), Pat (a₁::a₂::as) × Pat (b₁::b₂::bs)) × LHS (forall (as : List α) (bs : List β), Pat as × Pat bs) -:= arbitrary _ +:= arbitrary -- set_option trace.Meta.EqnCompiler.match true -- set_option trace.Meta.EqnCompiler.matchDebug true @@ -225,7 +225,7 @@ def ex3 (α : Type u) (β : Type v) (n : Nat) (x : List α) (y : List β) : def ex4 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (Pat (inaccessible 0) × Pat (Vec.nil : Vec α 0)) × LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (inaccessible (n+1)) × Pat xs) := -arbitrary _ +arbitrary #eval test `ex4 2 `elimTest4 #print elimTest4 @@ -233,7 +233,7 @@ arbitrary _ def ex5 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (Pat Nat.zero × Pat (Vec.nil : Vec α 0)) × LHS (forall (n : Nat) (xs : Vec α (n+1)), Pat (Nat.succ n) × Pat xs) := -arbitrary _ +arbitrary #eval test `ex5 2 `elimTest5 #print elimTest5 @@ -241,7 +241,7 @@ arbitrary _ def ex6 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (Pat (inaccessible Nat.zero) × Pat (Vec.nil : Vec α 0)) × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) := -arbitrary _ +arbitrary -- set_option trace.Meta.Match.match true -- set_option trace.Meta.Match.debug true @@ -252,7 +252,7 @@ arbitrary _ def ex7 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (forall (a : α), Pat (inaccessible 1) × Pat (Vec.cons a Vec.nil)) × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) := -arbitrary _ +arbitrary #eval test `ex7 2 `elimTest7 -- #check elimTest7 @@ -274,7 +274,7 @@ elimTest7 _ (fun _ _ => Option Nat) n xs (fun a => some a) (fun _ _ => none) def ex8 (α : Type u) (n : Nat) (xs : Vec α n) : LHS (forall (a b : α), Pat (inaccessible 2) × Pat (Vec.cons a (Vec.cons b Vec.nil))) × LHS (forall (N : Nat) (XS : Vec α N), Pat (inaccessible N) × Pat XS) := -arbitrary _ +arbitrary #eval test `ex8 2 `elimTest8 #print elimTest8 @@ -296,7 +296,7 @@ structure Node : Type := def ex9 (xs : List Node) : LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t)) × LHS (forall (ys : List Node), Pat ys) := -arbitrary _ +arbitrary #eval test `ex9 1 `elimTest9 #print elimTest9 @@ -318,14 +318,14 @@ inductive Foo : Bool → Prop def ex10 (x : Bool) (y : Foo x) : LHS (Pat (inaccessible false) × Pat Foo.bar) × LHS (forall (x : Bool) (y : Foo x), Pat (inaccessible x) × Pat y) := -arbitrary _ +arbitrary #eval test `ex10 2 `elimTest10 true def ex11 (xs : List Node) : LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t)) × LHS (Pat ([] : List Node)) := -arbitrary _ +arbitrary #eval testFailure `ex11 1 `elimTest11 -- should produce error message @@ -333,7 +333,7 @@ def ex12 (x y z : Bool) : LHS (forall (x y : Bool), Pat x × Pat y × Pat true) × LHS (forall (x z : Bool), Pat false × Pat true × Pat z) × LHS (forall (y z : Bool), Pat true × Pat false × Pat z) := -arbitrary _ +arbitrary #eval testFailure `ex12 3 `elimTest12 -- should produce error message @@ -341,7 +341,7 @@ def ex13 (xs : List Node) : LHS (forall (h : Node) (t : List Node), Pat (h :: Node.mk 1 1 (Op.mk 1) :: t)) × LHS (forall (ys : List Node), Pat ys) × LHS (forall (ys : List Node), Pat ys) := -arbitrary _ +arbitrary #eval testFailure `ex13 1 `elimTest13 -- should produce error message @@ -349,7 +349,7 @@ def ex14 (x y : Nat) : LHS (Pat (val 1) × Pat (val 2)) × LHS (Pat (val 2) × Pat (val 3)) × LHS (forall (x y : Nat), Pat x × Pat y) := -arbitrary _ +arbitrary -- set_option trace.Meta.Match true @@ -369,7 +369,7 @@ def ex15 (xs : Array (List Nat)) : LHS (forall (a : Nat), Pat (ArrayLit1 [a])) × LHS (forall (a b : Nat), Pat (ArrayLit2 [a] [b])) × LHS (forall (ys : Array (List Nat)), Pat ys) := -arbitrary _ +arbitrary #eval test `ex15 1 `elimTest15 -- #check elimTest15 @@ -389,7 +389,7 @@ def ex16 (xs : List Nat) : LHS (forall (a : Nat) (xs : List Nat) (b : Nat) (as : List Nat), Pat (a :: As xs (b :: as))) × LHS (forall (a : Nat), Pat ([a])) × LHS (Pat ([] : List Nat)) := -arbitrary _ +arbitrary #eval test `ex16 1 `elimTest16 diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean index b4af8c6be4..0d059b16fb 100644 --- a/tests/lean/run/fun.lean +++ b/tests/lean/run/fun.lean @@ -1,15 +1,15 @@ open Function Bool -constant f : Nat → Bool := arbitrary _ -constant g : Nat → Nat := arbitrary _ +constant f : Nat → Bool := arbitrary +constant g : Nat → Nat := arbitrary #check f ∘ g ∘ g #check (id : Nat → Nat) -constant h : Nat → Bool → Nat := arbitrary _ +constant h : Nat → Bool → Nat := arbitrary -constant f1 : Nat → Nat → Bool := arbitrary _ -constant f2 : Bool → Nat := arbitrary _ +constant f1 : Nat → Nat → Bool := arbitrary +constant f2 : Bool → Nat := arbitrary diff --git a/tests/lean/run/optParam.lean b/tests/lean/run/optParam.lean index 382e97c35c..818d3c2623 100644 --- a/tests/lean/run/optParam.lean +++ b/tests/lean/run/optParam.lean @@ -8,10 +8,10 @@ theorem ex2 : p (x := 1) |>.2 = 1 := rfl def c {α : Type} [Inhabited α] : α × α := -(arbitrary _, arbitrary _) +(arbitrary, arbitrary) -theorem ex3 {α} [Inhabited α] : c.1 = arbitrary α := +theorem ex3 {α} [Inhabited α] : c.1 = arbitrary (α := α) := rfl -theorem ex4 {α} [Inhabited α] : c.2 = arbitrary α := +theorem ex4 {α} [Inhabited α] : c.2 = arbitrary (α := α) := rfl diff --git a/tests/lean/zipper.lean b/tests/lean/zipper.lean index 9c2410cfb1..5e1f081aa8 100644 --- a/tests/lean/zipper.lean +++ b/tests/lean/zipper.lean @@ -1,5 +1,3 @@ - - structure ListZipper (α : Type) := (xs : List α) (bs : List α) @@ -25,7 +23,7 @@ def erase : ListZipper α → ListZipper α | ⟨x::xs, bs⟩ => ⟨xs, bs⟩ def curr [Inhabited α] : ListZipper α → α -| ⟨[], bs⟩ => arbitrary _ +| ⟨[], bs⟩ => arbitrary | ⟨x::xs, bs⟩ => x def currOpt : ListZipper α → Option α