From 40943f84f3e0ba8c83a79a1f5d311a07fef32e0d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jul 2019 10:46:35 -0700 Subject: [PATCH] chore(tests): fix tests --- tests/bench/deriv.lean | 2 +- tests/compiler/append.lean | 4 ++-- tests/compiler/array_test.lean | 8 +++---- tests/compiler/array_test2.lean | 6 +++--- tests/compiler/bytearray_bug.lean | 4 ++-- tests/compiler/expr.lean | 2 +- tests/compiler/map_big.lean | 4 ++-- tests/compiler/partial.lean | 2 +- tests/compiler/str.lean | 6 +++--- tests/compiler/t2.lean | 2 +- tests/compiler/t4.lean | 2 +- tests/compiler/thunk.lean | 2 +- tests/compiler/uint_fold.lean | 10 ++++----- tests/lean/run/deriv.lean | 2 +- tests/lean/run/new_compiler.lean | 36 +++++++++++++++---------------- tests/lean/string_imp2.lean | 12 +++++------ 16 files changed, 52 insertions(+), 52 deletions(-) diff --git a/tests/bench/deriv.lean b/tests/bench/deriv.lean index fece04381c..6cda7d4f68 100644 --- a/tests/bench/deriv.lean +++ b/tests/bench/deriv.lean @@ -13,7 +13,7 @@ partial def pown : Int → Int → Int | a 0 := 1 | a 1 := a | a n := - let b := pown a (n / 2) in + let b := pown a (n / 2); b * b * (if n % 2 = 0 then 1 else a) partial def add : Expr → Expr → Expr diff --git a/tests/compiler/append.lean b/tests/compiler/append.lean index 5bb5f22ce4..e49504b706 100644 --- a/tests/compiler/append.lean +++ b/tests/compiler/append.lean @@ -1,4 +1,4 @@ def main (xs : List String) : IO Unit := -let ys1 := List.replicate 1000000 1 in -let ys2 := List.replicate 1000000 2 in +let ys1 := List.replicate 1000000 1; +let ys2 := List.replicate 1000000 2; IO.println (toString (ys1 ++ ys2).length) diff --git a/tests/compiler/array_test.lean b/tests/compiler/array_test.lean index 921e0dc80c..b783bee115 100644 --- a/tests/compiler/array_test.lean +++ b/tests/compiler/array_test.lean @@ -1,8 +1,8 @@ def foo (a : Array Nat) : Array Nat := -let a := a.push 0 in -let a := a.push 1 in -let a := a.push 2 in -let a := a.push 3 in +let a := a.push 0; +let a := a.push 1; +let a := a.push 2; +let a := a.push 3; a def main : IO UInt32 := diff --git a/tests/compiler/array_test2.lean b/tests/compiler/array_test2.lean index de5ff83c34..e5f767615e 100644 --- a/tests/compiler/array_test2.lean +++ b/tests/compiler/array_test2.lean @@ -3,9 +3,9 @@ unless b $ IO.println "failed" def main : IO Unit := -let a1 := [2, 3, 5].toArray in -let a2 := [4, 7, 9].toArray in -let a3 := [4, 7, 8].toArray in +let a1 := [2, 3, 5].toArray; +let a2 := [4, 7, 9].toArray; +let a3 := [4, 7, 8].toArray; do check (Array.isEqv a1 a2 (fun v w => v % 2 == w % 2)); check (!Array.isEqv a1 a3 (fun v w => v % 2 == w % 2)); diff --git a/tests/compiler/bytearray_bug.lean b/tests/compiler/bytearray_bug.lean index ae36209486..421a7df880 100644 --- a/tests/compiler/bytearray_bug.lean +++ b/tests/compiler/bytearray_bug.lean @@ -1,4 +1,4 @@ def main (xs : List String) : IO Unit := - let arr := (let e := ByteArray.empty in e.push (UInt8.ofNat 10)) in - let v := arr.data.get 0 in + let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10)); + let v := arr.data.get 0; IO.println v diff --git a/tests/compiler/expr.lean b/tests/compiler/expr.lean index da915526c0..19cbdade2b 100644 --- a/tests/compiler/expr.lean +++ b/tests/compiler/expr.lean @@ -2,7 +2,7 @@ import init.lean.expr open Lean def main : IO UInt32 := -let e := Expr.app (Expr.const `f []) (Expr.const `a []) in +let e := Expr.app (Expr.const `f []) (Expr.const `a []); IO.println e.dbgToString *> IO.println ("hash: " ++ toString e.hash) *> pure 0 diff --git a/tests/compiler/map_big.lean b/tests/compiler/map_big.lean index 50070aec83..06e980f200 100644 --- a/tests/compiler/map_big.lean +++ b/tests/compiler/map_big.lean @@ -1,8 +1,8 @@ def f2 (n : Nat) (xs : List Nat) : List (List Nat) := -let ys := List.replicate n 0 in +let ys := List.replicate n 0; xs.map (fun x => x :: ys) def main : IO UInt32 := -let n := 100000 in +let n := 100000; IO.println (toString (f2 n (List.replicate n 0)).length) *> pure 0 diff --git a/tests/compiler/partial.lean b/tests/compiler/partial.lean index 9ccaa06017..849c20a534 100644 --- a/tests/compiler/partial.lean +++ b/tests/compiler/partial.lean @@ -9,6 +9,6 @@ partial def contains : String → Char → Nat → Bool else contains s c (s.next i) def main : IO Unit := -let s1 := "hello" in +let s1 := "hello"; IO.println (contains s1 'a' 0) *> IO.println (contains s1 'o' 0) diff --git a/tests/compiler/str.lean b/tests/compiler/str.lean index 5abe86f525..b43bf85639 100644 --- a/tests/compiler/str.lean +++ b/tests/compiler/str.lean @@ -6,9 +6,9 @@ def showChars : Nat → String → String.Pos → IO Unit showChars n s (s.next idx) def main : IO UInt32 := -let s₁ := "hello α_world_β" in -let b : String.Pos := 0 in -let e := s₁.bsize in +let s₁ := "hello α_world_β"; +let b : String.Pos := 0; +let e := s₁.bsize; IO.println (s₁.extract b e) *> IO.println (s₁.extract (b+2) e) *> IO.println (s₁.extract (b+2) (e-1)) *> diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean index 3791e8f44c..e05832681e 100644 --- a/tests/compiler/t2.lean +++ b/tests/compiler/t2.lean @@ -13,7 +13,7 @@ partial def pown : Int → Int → Int | a 0 := 1 | a 1 := a | a n := - let b := pown a (n / 2) in + let b := pown a (n / 2); b * b * (if n % 2 = 0 then 1 else a) partial def add : Expr → Expr → Expr diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean index 10785ed045..c6b3b979a2 100644 --- a/tests/compiler/t4.lean +++ b/tests/compiler/t4.lean @@ -24,7 +24,7 @@ partial def pown : Int → Int → Int | a 0 := 1 | a 1 := a | a n := - let b := pown a (n / 2) in + let b := pown a (n / 2); b * b * (if n % 2 = 0 then 1 else a) partial def addAux : Expr → Expr → Expr diff --git a/tests/compiler/thunk.lean b/tests/compiler/thunk.lean index 98d38f2e8e..2b80fe043b 100644 --- a/tests/compiler/thunk.lean +++ b/tests/compiler/thunk.lean @@ -1,5 +1,5 @@ def compute (v : Nat) : Thunk Nat := -⟨fun _ => let xs := List.replicate 100000 v in xs.foldl Nat.add 0⟩ +⟨fun _ => let xs := List.replicate 100000 v; xs.foldl Nat.add 0⟩ @[noinline] def test (t : Thunk Nat) (n : Nat) : Nat := diff --git a/tests/compiler/uint_fold.lean b/tests/compiler/uint_fold.lean index 4c37e96c46..ce6b38d7e8 100644 --- a/tests/compiler/uint_fold.lean +++ b/tests/compiler/uint_fold.lean @@ -3,17 +3,17 @@ def h (x : Nat) : UInt32 := UInt32.ofNat x def f (x y : UInt32) : UInt32 := -let a1 : UInt32 := 128 * 100 - 100 in -let v : Nat := 10 + x.toNat in -let a2 : UInt32 := x + a1 in -let a3 : UInt32 := 10 in +let a1 : UInt32 := 128 * 100 - 100; +let v : Nat := 10 + x.toNat; +let a2 : UInt32 := x + a1; +let a3 : UInt32 := 10; y + a2 + h v + a3 partial def g : UInt32 → UInt32 → UInt32 | x y := if x = 0 then y else g (x-1) (y+2) def foo : UInt8 := -let x : UInt8 := 100 in +let x : UInt8 := 100; x + x + x def main : IO UInt32 := diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean index a504a137f7..85748a9e26 100644 --- a/tests/lean/run/deriv.lean +++ b/tests/lean/run/deriv.lean @@ -15,7 +15,7 @@ unsafe def pown : Int → Int → Int | a 0 := 1 | a 1 := a | a n := - let b := pown a (n / 2) in + let b := pown a (n / 2); b * b * (if n % 2 = 0 then 1 else a) unsafe def add : Expr → Expr → Expr diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean index 982b19dddc..2bae073b1e 100644 --- a/tests/lean/run/new_compiler.lean +++ b/tests/lean/run/new_compiler.lean @@ -6,32 +6,32 @@ set_option pp.binder_types false set_option pp.proofs true def foo (n : Nat) : Nat := -let x := Nat.zero in -let x1 := Nat.succ x in -let x2 := Nat.succ x1 in -let x3 := Nat.succ x2 in -let x4 := Nat.succ x3 in -let x5 := Nat.succ x4 in -let x6 := Nat.succ x5 in -let x7 := Nat.succ x in -let x8 := Nat.succ x7 in -let y1 := x in -let y2 := y1 in +let x := Nat.zero; +let x1 := Nat.succ x; +let x2 := Nat.succ x1; +let x3 := Nat.succ x2; +let x4 := Nat.succ x3; +let x5 := Nat.succ x4; +let x6 := Nat.succ x5; +let x7 := Nat.succ x ; +let x8 := Nat.succ x7; +let y1 := x; +let y2 := y1; y2 + n def cseTst (n : Nat) : Nat := -let y := Nat.succ ((fun x => x) n) in -let z := Nat.succ n in +let y := Nat.succ ((fun x => x) n); +let z := Nat.succ n; y + z def tst1 (n : Nat) : Nat := -let p := (Nat.succ n, n) in -let q := (p, p) in +let p := (Nat.succ n, n); +let q := (p, p); Prod.casesOn q (fun x y => Prod.casesOn x (fun z w => z)) def tst2 (n : Nat) : Nat := -let p := (fun x => Nat.succ x, Nat.zero) in -let f := fun (p : (Nat → Nat) × Nat) => p.1 in +let p := (fun x => Nat.succ x, Nat.zero) ; +let f := fun (p : (Nat → Nat) × Nat) => p.1; f p n def add' : Nat → Nat → Nat @@ -50,7 +50,7 @@ def foo3 (n : Nat) : Nat := (fun (a : Nat) => a + a + a) (n*n) def boo (a : Nat) (l : List Nat) : List Nat := -let f := @List.cons Nat in +let f := @List.cons Nat; f a (f a l) def bla (i : Nat) (h : i > 0 ∧ i ≠ 10) : Nat := diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean index 77821577c6..424dc14a49 100644 --- a/tests/lean/string_imp2.lean +++ b/tests/lean/string_imp2.lean @@ -5,21 +5,21 @@ def g (s : String) : String := s.push ' ' ++ s.push '-' def h (s : String) : String := -let it₁ := s.mkIterator in -let it₂ := it₁.next in +let it₁ := s.mkIterator; +let it₂ := it₁.next; it₁.remainingToString ++ "-" ++ it₂.remainingToString #exit -- Disabled until we implement new VM def r (s : String) : String := -let it₁ := s.mkIterator.toEnd in -let it₂ := it₁.prev in +let it₁ := s.mkIterator.toEnd; +let it₂ := it₁.prev; it₁.prevToString ++ "-" ++ it₂.prevToString def s (s : String) : String := -let it₁ := s.mkIterator.toEnd in -let it₂ := it₁.prev in +let it₁ := s.mkIterator.toEnd; +let it₂ := it₁.prev; (it₁.insert "abc").toString ++ (it₂.insert "de").toString