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

chore: move tests to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-23 14:05:40 -07:00
parent 3de97ddc27
commit 8cb1ff206c
18 changed files with 77 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
doc/examples/compiler/test.lean
View file

@ -1,3 +1,4 @@
def main (n : List String) : IO UInt32 :=
do IO.println (toString n);
#lang lean4
def main (n : List String) : IO UInt32 := do
IO.println (toString n)
pure 0

3
tests/bench/binarytrees.lean
View file

@ -1,3 +1,4 @@
#lang lean4
inductive Tree
| Nil
| Node (l r : Tree) : Tree
@ -53,7 +54,7 @@ def main : List String → IO UInt32
-- allocate, walk, and deallocate many bottom-up binary trees
let vs := (depth minN maxN); -- `using` (parList $ evalTuple3 r0 r0 rseq)
vs.forM (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
vs.forM (fun (m, d, i) => out (toString m ++ "\t trees") d i.get);
-- confirm the the long-lived binary tree still exists
out "long lived tree" maxN (check long);

1
tests/bench/const_fold.lean
View file

@ -1,3 +1,4 @@
#lang lean4
inductive Expr
| Var : Nat → Expr
| Val : Nat → Expr

13
tests/bench/deriv.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/- Benchmark for new code generator -/
inductive Expr
| Val : Int → Expr
@ -52,10 +53,10 @@ def ln : Expr → Expr
def d (x : String) : Expr → Expr
| Val _ => Val 0
| Var y => if x = y then Val 1 else Val 0
| Add f g => add (d f) (d g)
| Mul f g => add (mul f (d g)) (mul g (d f))
| Pow f g => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
| Ln f => mul (d f) (pow f (Val (-1)))
| Add f g => add (d x f) (d x g)
| Mul f g => add (mul f (d x g)) (mul g (d x f))
| Pow f g => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
| Ln f => mul (d x f) (pow f (Val (-1)))
def count : Expr → UInt32
| Val _ => 1
@ -65,7 +66,7 @@ def count : Expr → UInt32
| Pow f g => count f + count g
| Ln f => count f
def Expr.toString : Expr → String
protected def Expr.toString : Expr → String
| Val n => toString n
| Var x => x
| Add f g => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@ -78,7 +79,7 @@ instance : HasToString Expr :=
def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
| 0, x => pure x
| m@(n+1), x => f (s - m) x >>= nestAux n
| m@(n+1), x => f (s - m) x >>= nestAux s f n
def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
nestAux n f n e

18
tests/bench/qsort.lean
View file

@ -1,3 +1,4 @@
#lang lean4
abbrev Elem := UInt32
def badRand (seed : Elem) : Elem :=
@ -10,24 +11,25 @@ def mkRandomArray : Nat → Elem → Array Elem → Array Elem
partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
| i =>
if i < a.size - 1 then do
unless (a.get! i <= a.get! (i+1)) $ throw (IO.userError "array is not sorted");
checkSortedAux (i+1)
unless (a.get! i <= a.get! (i+1)) do throw (IO.userError "array is not sorted");
checkSortedAux a (i+1)
else
pure ()
-- copied from stdlib, but with `UInt32` indices instead of `Nat` (which is more comparable to the other versions)
abbrev Idx := UInt32
instance : HasLift UInt32 Nat := ⟨UInt32.toNat⟩
prefix `↑`:max := oldCoe
macro:max "↑" x:term:max : term => `(UInt32.toNat $x)
@[specialize] private partial def partitionAux {α : Type} [Inhabited α] (lt : α → α → Bool) (hi : Idx) (pivot : α) : Array α → Idx → Idx → Idx × Array α
| as, i, j =>
if j < hi then
if lt (as.get! ↑j) pivot then
let as := as.swap! ↑i ↑j;
partitionAux as (i+1) (j+1)
partitionAux lt hi pivot as (i+1) (j+1)
else
partitionAux as i (j+1)
partitionAux lt hi pivot as i (j+1)
else
let as := as.swap! ↑i ↑hi;
(i, as)
@ -47,8 +49,8 @@ partitionAux lt hi pivot as lo lo
-- TODO: fix `partial` support in the equation compiler, it breaks if we use `let (mid, as) := partition as lt low high`
let mid := p.1;
let as := p.2;
let as := qsortAux as low mid;
qsortAux as (mid+1) high
let as := qsortAux lt as low mid;
qsortAux lt as (mid+1) high
else as
@[inline] def qsort {α : Type} [Inhabited α] (as : Array α) (lt : α → α → Bool) : Array α :=

3
tests/bench/rbmap.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -23,7 +24,7 @@ open color Nat Tree
def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ
| Leaf, b => b
| Node _ l k v r, b => fold r (f k v (fold l b))
| Node _ l k v r, b => fold f r (f k v (fold f l b))
@[inline]
def balance1 : Nat → Bool → Tree → Tree → Tree

7
tests/bench/rbmap_checkpoint.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -25,7 +26,7 @@ open color Nat Tree
def fold (f : Nat → Bool → σ → σ) : Tree → σ → σ
| Leaf, b => b
| Node _ l k v r, b => fold r (f k v (fold l b))
| Node _ l k v r, b => fold f r (f k v (fold f l b))
@[inline]
def balance1 : Nat → Bool → Tree → Tree → Tree
@ -72,7 +73,7 @@ def mkMapAux (freq : Nat) : Nat → Tree → List Tree → List Tree
| n+1, m, r =>
let m := insert m n (n % 10 = 0);
let r := if n % freq == 0 then m::r else r;
mkMapAux n m r
mkMapAux freq n m r
def mkMap (n : Nat) (freq : Nat) : List Tree :=
mkMapAux freq n Leaf []
@ -83,7 +84,7 @@ def myLen : List Tree → Nat → Nat
| [], r => r
def main (xs : List String) : IO UInt32 := do
[n, freq] ← pure xs | throw $ IO.userError "invalid input";
let [n, freq] ← pure xs | throw $ IO.userError "invalid input";
let n := n.toNat!;
let freq := freq.toNat!;
let freq := if freq == 0 then 1 else freq;

39
tests/bench/unionfind.lean
View file

@ -1,8 +1,9 @@
#lang lean4
def StateT' (m : Type → Type) (σ : Type) (α : Type) := σ → m (α × σ)
namespace StateT'
variables {m : Type → Type} [Monad m] {σ : Type} {α β : Type}
@[inline] protected def pure (a : α) : StateT' m σ α := fun s => pure (a, s)
@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do (a, s') ← x s; f a s'
@[inline] protected def bind (x : StateT' m σ α) (f : α → StateT' m σ β) : StateT' m σ β := fun s => do let (a, s') ← x s; f a s'
@[inline] def read : StateT' m σ σ := fun s => pure (s, s)
@[inline] def write (s' : σ) : StateT' m σ Unit := fun s => pure ((), s')
@[inline] def updt (f : σ → σ) : StateT' m σ Unit := fun s => pure ((), f s)
@ -15,11 +16,11 @@ namespace ExceptT'
variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type}
@[inline] protected def pure (a : α) : ExceptT' m ε α := (pure (Except.ok a) : m (Except ε α))
@[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β :=
(do { v ← x; match v with
(do { let v ← x; match v with
| Except.error e => pure (Except.error e)
| Except.ok a => f a } : m (Except ε β))
@[inline] def error (e : ε) : ExceptT' m ε α := (pure (Except.error e) : m (Except ε α))
@[inline] def lift (x : m α) : ExceptT' m ε α := (do {a ← x; pure (Except.ok a) } : m (Except ε α))
@[inline] def lift (x : m α) : ExceptT' m ε α := (do {let a ← x; pure (Except.ok a) } : m (Except ε α))
instance : Monad (ExceptT' m ε) :=
{pure := @ExceptT'.pure _ _ _, bind := @ExceptT'.bind _ _ _}
end ExceptT'
@ -40,35 +41,35 @@ def run {α : Type} (x : M α) (s : ufData := ∅) : Except String α × ufData
x s
def capacity : M Nat :=
do d ← read; pure d.size
do let d ← read; pure d.size
def findEntryAux : Nat → Node → M nodeData
| 0, n => error "out of fuel"
| i+1, n =>
do s ← read;
do let s ← read;
if h : n < s.size then
do { let e := s.get ⟨n, h⟩;
if e.find = n then pure e
else do e₁ ← findEntryAux i e.find;
else do let e₁ ← findEntryAux i e.find;
updt (fun s => s.set! n e₁);
pure e₁ }
else error "invalid Node"
def findEntry (n : Node) : M nodeData :=
do c ← capacity;
do let c ← capacity;
findEntryAux c n
def find (n : Node) : M Node :=
do e ← findEntry n; pure e.find
do let e ← findEntry n; pure e.find
def mk : M Node :=
do n ← capacity;
do let n ← capacity;
updt $ fun s => s.push {find := n, rank := 1};
pure n
def union (n₁ n₂ : Node) : M Unit :=
do r₁ ← findEntry n₁;
r₂ ← findEntry n₂;
do let r₁ ← findEntry n₁;
let r₂ ← findEntry n₂;
if r₁.find = r₂.find then pure ()
else updt $ fun s =>
if r₁.rank < r₂.rank then s.set! r₁.find { find := r₂.find }
@ -83,30 +84,30 @@ def mkNodes : Nat → M Unit
| n+1 => do _ ← mk; mkNodes n
def checkEq (n₁ n₂ : Node) : M Unit :=
do r₁ ← find n₁; r₂ ← find n₂;
unless (r₁ = r₂) $ error "nodes are not equal"
do let r₁ ← find n₁; let r₂ ← find n₂;
unless (r₁ = r₂) do error "nodes are not equal"
def mergePackAux : Nat → Nat → Nat → M Unit
| 0, _, _ => pure ()
| i+1, n, d =>
do c ← capacity;
| i+1, n, d => do
let c ← capacity;
if (n+d) < c
then union n (n+d) *> mergePackAux i (n+1) d
else pure ()
def mergePack (d : Nat) : M Unit :=
do c ← capacity; mergePackAux c 0 d
do let c ← capacity; mergePackAux c 0 d
def numEqsAux : Nat → Node → Nat → M Nat
| 0, _, r => pure r
| i+1, n, r =>
do c ← capacity;
do let c ← capacity;
if n < c
then do { n₁ ← find n; numEqsAux i (n+1) (if n = n₁ then r else r+1) }
then do { let n₁ ← find n; numEqsAux i (n+1) (if n = n₁ then r else r+1) }
else pure r
def numEqs : M Nat :=
do c ← capacity;
do let c ← capacity;
numEqsAux c 0 0
def test (n : Nat) : M Nat :=

2
tests/compiler/foreign/README.md
View file

@ -6,7 +6,7 @@ The file `main.lean` contains a small Lean program that uses the exported primit
Build instructions
=====
Assuming the Lean `bin/` directory (e.g. from `build/release/stage0.5`) is in your `PATH`,
Assuming the Lean `bin/` directory (e.g. from `build/release/stage1`) is in your `PATH`,
executing `leanmake` will create the executable `build/bin/test`.
The executable `build/bin/test` should produce the output

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

@ -1,4 +1,5 @@
constant SPointed : PointedType := arbitrary _
#lang lean4
constant SPointed : PointedType
def S : Type := SPointed.type
instance : Inhabited S := ⟨SPointed.val⟩

1
tests/compiler/print_error.lean
View file

@ -1,3 +1,4 @@
#lang lean4
prelude
import Init.System.IO

3
tests/compiler/reusebug.lean
View file

@ -1,3 +1,4 @@
#lang lean4
inductive Expr
| Val : Int → Expr
| Var : String → Expr
@ -6,7 +7,7 @@ inductive Expr
open Expr
def Expr.toString : Expr → String
protected def Expr.toString : Expr → String
| Val n => toString n
| Var x => x
| Add f g => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"

5
tests/compiler/str.lean
View file

@ -1,7 +1,8 @@
#lang lean4
def showChars : Nat → String → String.Pos → IO Unit
| 0, _, _ => pure ()
| n+1, s, idx =>
unless (s.atEnd idx) $
| n+1, s, idx => do
unless s.atEnd idx do
IO.println (">> " ++ toString (s.get idx)) *>
showChars n s (s.next idx)

13
tests/compiler/t2.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/- Benchmark for new code generator -/
inductive Expr
| Val : Int → Expr
@ -52,10 +53,10 @@ def ln : Expr → Expr
def d (x : String) : Expr → Expr
| Val _ => Val 0
| Var y => if x = y then Val 1 else Val 0
| Add f g => add (d f) (d g)
| Mul f g => add (mul f (d g)) (mul g (d f))
| Pow f g => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
| Ln f => mul (d f) (pow f (Val (-1)))
| Add f g => add (d x f) (d x g)
| Mul f g => add (mul f (d x g)) (mul g (d x f))
| Pow f g => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
| Ln f => mul (d x f) (pow f (Val (-1)))
def count : Expr → Nat
| Val _ => 1
@ -65,7 +66,7 @@ def count : Expr → Nat
| Pow f g => count f + count g
| Ln f => count f
def Expr.toString : Expr → String
protected def Expr.toString : Expr → String
| Val n => toString n
| Var x => x
| Add f g => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@ -78,7 +79,7 @@ instance : HasToString Expr :=
def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
| 0, x => pure x
| m@(n+1), x => f (s - m) x >>= nestAux n
| m@(n+1), x => f (s - m) x >>= nestAux s f n
def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
nestAux n f n e

13
tests/compiler/t4.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/- Benchmark for new code generator -/
inductive Expr
| Val : Int → Expr
@ -9,7 +10,7 @@ inductive Expr
open Expr
def Expr.toString : Expr → String
protected def Expr.toString : Expr → String
| Val n => toString n
| Var x => x
| Add f g => "(" ++ Expr.toString f ++ " + " ++ Expr.toString g ++ ")"
@ -73,12 +74,12 @@ def ln : Expr → Expr
def d (x : String) : Expr → Expr
| Val _ => Val 0
| Var y => if x = y then Val 1 else Val 0
| Add f g => add (d f) (d g)
| Add f g => add (d x f) (d x g)
| Mul f g =>
-- dbgTrace (">> d (" ++ toString f ++ ", " ++ toString g ++ ")") $ fun _ =>
add (mul f (d g)) (mul g (d f))
| Pow f g => mul (pow f g) (add (mul (mul g (d f)) (pow f (Val (-1)))) (mul (ln f) (d g)))
| Ln f => mul (d f) (pow f (Val (-1)))
add (mul f (d x g)) (mul g (d x f))
| Pow f g => mul (pow f g) (add (mul (mul g (d x f)) (pow f (Val (-1)))) (mul (ln f) (d x g)))
| Ln f => mul (d x f) (pow f (Val (-1)))
def count : Expr → Nat
| Val _ => 1
@ -91,7 +92,7 @@ def count : Expr → Nat
def nestAux (s : Nat) (f : Nat → Expr → IO Expr) : Nat → Expr → IO Expr
| 0, x => pure x
| m@(n+1), x => f (s - m) x >>= nestAux n
| m@(n+1), x => f (s - m) x >>= nestAux s f n
def nest (f : Nat → Expr → IO Expr) (n : Nat) (e : Expr) : IO Expr :=
nestAux n f n e

1
tests/compiler/thunk.lean
View file

@ -1,3 +1,4 @@
#lang lean4
def compute (v : Nat) : Thunk Nat :=
⟨fun _ => let xs := List.replicate 100000 v; xs.foldl Nat.add 0⟩

7
tests/compiler/uint_fold.lean
View file

@ -1,5 +1,6 @@
@[noinline]
def h (x : Nat) : UInt32 :=
#lang lean4
@[noinline] def h (x : Nat) : UInt32 :=
UInt32.ofNat x
def f (x y : UInt32) : UInt32 :=
@ -9,7 +10,7 @@ let a2 : UInt32 := x + a1;
let a3 : UInt32 := 10;
y + a2 + h v + a3
partial def g : UInt32 → UInt32 → UInt32 | x, y =>
partial def g (x : UInt32) (y : UInt32) : UInt32 :=
if x = 0 then y else g (x-1) (y+2)
def foo : UInt8 :=

3
tests/lean/run/newfrontend1.lean
View file

@ -271,9 +271,6 @@ def altTst2 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
def altTst3 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
⟨fun {α} => StateT.failure, fun {α} => StateT.orelse⟩
def altTst4 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
⟨@StateT.failure _ _ _ _, @StateT.orelse _ _ _ _⟩
#check_failure 1 + true
/-