max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-25 09:25:45 -08:00
parent d6f778bec4
commit e3fb7010f1
8 changed files with 42 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/compiler/foreign/main.lean
View file

@ -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;

2
tests/compiler/lazylist.lean
View file

@ -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

8
tests/lean/run/1385.lean
View file

@ -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

12
tests/lean/run/def12.lean
View file

@ -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 α

34
tests/lean/run/depElim1.lean
View file

@ -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

10
tests/lean/run/fun.lean
View file

@ -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

6
tests/lean/run/optParam.lean
View file

@ -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

4
tests/lean/zipper.lean
View file

@ -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 α