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

chore(tests): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-17 10:46:35 -07:00
parent a3c0e2bb36
commit 40943f84f3
16 changed files with 52 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/bench/deriv.lean
View file

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

4
tests/compiler/append.lean
View file

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

8
tests/compiler/array_test.lean
View file

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

6
tests/compiler/array_test2.lean
View file

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

4
tests/compiler/bytearray_bug.lean
View file

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

2
tests/compiler/expr.lean
View file

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

4
tests/compiler/map_big.lean
View file

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

2
tests/compiler/partial.lean
View file

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

6
tests/compiler/str.lean
View file

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

2
tests/compiler/t2.lean
View file

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

2
tests/compiler/t4.lean
View file

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

2
tests/compiler/thunk.lean
View file

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

10
tests/compiler/uint_fold.lean
View file

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

2
tests/lean/run/deriv.lean
View file

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

36
tests/lean/run/new_compiler.lean
View file

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

12
tests/lean/string_imp2.lean
View file

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