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

chore(tests): fix do syntax in tests

Browse source
This commit is contained in:
Sebastian Ullrich 2019-06-30 13:04:34 +02:00
parent 642dd9f63b
commit c299e6c0e6
20 changed files with 204 additions and 204 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/bench/binarytrees.lean
View file

@ -40,22 +40,22 @@ partial def depth : Nat -> Nat -> List (Nat × Nat × Task UInt32)
def main : List String → IO UInt32
| [s] := do
let n := s.toNat,
let maxN := Nat.max (minN + 2) n,
let stretchN := maxN + 1,
let n := s.toNat;
let maxN := Nat.max (minN + 2) n;
let stretchN := maxN + 1;
-- stretch memory tree
let c := check (make $ UInt32.ofNat stretchN),
out "stretch tree" stretchN c,
let c := check (make $ UInt32.ofNat stretchN);
out "stretch tree" stretchN c;
-- allocate a long lived tree
let long := make $ UInt32.ofNat maxN,
let long := make $ UInt32.ofNat maxN;
-- allocate, walk, and deallocate many bottom-up binary trees
let vs := (depth minN maxN), -- `using` (parList $ evalTuple3 r0 r0 rseq)
vs.mmap (λ ⟨m,d,i⟩, out (toString m ++ "\t trees") d i.get),
vs.mmap (λ ⟨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),
out "long lived tree" maxN (check long);
pure 0
| _ := pure 1

12
tests/bench/qsort.lean
View file

@ -10,7 +10,7 @@ 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"),
unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted");
checkSortedAux (i+1)
else
pure ()
@ -54,10 +54,10 @@ qsortAux lt as 0 (UInt32.ofNat (as.size - 1))
def main (xs : List String) : IO Unit :=
do
let n := xs.head.toNat,
n.mfor $ λ _,
let n := xs.head.toNat;
n.mfor $ λ _;
n.mfor $ λ i, do
let xs := mkRandomArray i (UInt32.ofNat i) Array.empty,
let xs := qsort xs (λ a b, a < b),
--IO.println xs,
let xs := mkRandomArray i (UInt32.ofNat i) Array.empty;
let xs := qsort xs (λ a b, a < b);
--IO.println xs;
checkSortedAux xs 0

12
tests/bench/rbmap_checkpoint.lean
View file

@ -81,11 +81,11 @@ def myLen : List Tree → Nat → Nat
def main (xs : List String) : IO UInt32 :=
do
[n, freq] ← pure xs | throw "invalid input",
let n := n.toNat,
let freq := freq.toNat,
let freq := if freq == 0 then 1 else freq,
let mList := mkMap n freq,
let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0,
[n, freq] ← pure xs | throw "invalid input";
let n := n.toNat;
let freq := freq.toNat;
let freq := if freq == 0 then 1 else freq;
let mList := mkMap n freq;
let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0;
IO.println (toString (myLen mList 0) ++ " " ++ toString v) *>
pure 0

12
tests/bench/rbmap_checkpoint2.lean
View file

@ -81,11 +81,11 @@ def myLen : List Tree → Nat → Nat
def main (xs : List String) : IO UInt32 :=
do
[n, freq] ← pure xs | throw "invalid input",
let n := n.toNat,
let freq := freq.toNat,
let freq := if freq == 0 then 1 else freq,
let mList := mkMap n freq,
let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0,
[n, freq] ← pure xs | throw "invalid input";
let n := n.toNat;
let freq := freq.toNat;
let freq := if freq == 0 then 1 else freq;
let mList := mkMap n freq;
let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0;
IO.println (toString (myLen mList 0) ++ " " ++ toString v) *>
pure 0

38
tests/bench/unionfind.lean
View file

@ -45,32 +45,32 @@ do d ← read, pure d.size
def findEntryAux : Nat → Node → M nodeData
| 0 n := error "out of fuel"
| (i+1) n :=
do s ← read,
do s ← read;
if h : n < s.size then
do { let e := s.fget ⟨n, h⟩,
do { let e := s.fget ⟨n, h⟩;
if e.find = n then pure e
else do e₁ ← findEntryAux i e.find,
updt (λ s, s.set n e₁),
else do e₁ ← findEntryAux i e.find;
updt (λ s, s.set n e₁);
pure e₁ }
else error "invalid Node"
def findEntry (n : Node) : M nodeData :=
do c ← capacity,
do c ← capacity;
findEntryAux c n
def find (n : Node) : M Node :=
do e ← findEntry n, pure e.find
def mk : M Node :=
do n ← capacity,
updt $ λ s, s.push {find := n, rank := 1},
do n ← capacity;
updt $ λ s, s.push {find := n, rank := 1};
pure n
def union (n₁ n₂ : Node) : M Unit :=
do r₁ ← findEntry n₁,
r₂ ← findEntry n₂,
do r₁ ← findEntry n₁;
r₂ ← findEntry n₂;
if r₁.find = r₂.find then pure ()
else updt $ λ s,
else updt $ λ s;
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
else if r₁.rank = r₂.rank then
let s₁ := s.set r₁.find { find := r₂.find } in
@ -83,13 +83,13 @@ def mkNodes : Nat → M Unit
| (n+1) := mk *> mkNodes n
def checkEq (n₁ n₂ : Node) : M Unit :=
do r₁ ← find n₁, r₂ ← find n₂,
do r₁ ← find n₁, r₂ ← find n₂;
unless (r₁ = r₂) $ error "nodes are not equal"
def mergePackAux : Nat → Nat → Nat → M Unit
| 0 _ _ := pure ()
| (i+1) n d :=
do c ← capacity,
do c ← capacity;
if (n+d) < c
then union n (n+d) *> mergePackAux i (n+1) d
else pure ()
@ -100,23 +100,23 @@ do 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 c ← capacity;
if n < c
then do { 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 c ← capacity;
numEqsAux c 0 0
def test (n : Nat) : M Nat :=
if n < 2 then error "input must be greater than 1"
else do
mkNodes n,
mergePack 50000,
mergePack 10000,
mergePack 5000,
mergePack 1000,
mkNodes n;
mergePack 50000;
mergePack 10000;
mergePack 5000;
mergePack 1000;
numEqs
def main (xs : List String) : IO UInt32 :=

38
tests/bench/unionfind_clean.lean
View file

@ -13,32 +13,32 @@ do d ← get, pure d.size
def findEntryAux : Nat → Node → M nodeData
| 0 n := throw "out of fuel"
| (i+1) n :=
do s ← get,
do s ← get;
if h : n < s.size then
do { let e := s.fget ⟨n, h⟩,
do { let e := s.fget ⟨n, h⟩;
if e.find = n then pure e
else do e₁ ← findEntryAux i e.find,
modify (λ s, s.set n e₁),
else do e₁ ← findEntryAux i e.find;
modify (λ s, s.set n e₁);
pure e₁ }
else throw "invalid Node"
def findEntry (n : Node) : M nodeData :=
do c ← capacity,
do c ← capacity;
findEntryAux c n
def find (n : Node) : M Node :=
do e ← findEntry n, pure e.find
def mk : M Node :=
do n ← capacity,
modify $ λ s, s.push {find := n, rank := 1},
do n ← capacity;
modify $ λ s, s.push {find := n, rank := 1};
pure n
def union (n₁ n₂ : Node) : M Unit :=
do r₁ ← findEntry n₁,
r₂ ← findEntry n₂,
do r₁ ← findEntry n₁;
r₂ ← findEntry n₂;
if r₁.find = r₂.find then pure ()
else modify $ λ s,
else modify $ λ s;
if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find }
else if r₁.rank = r₂.rank then
let s₁ := s.set r₁.find { find := r₂.find } in
@ -51,13 +51,13 @@ def mkNodes : Nat → M Unit
| (n+1) := mk *> mkNodes n
def checkEq (n₁ n₂ : Node) : M Unit :=
do r₁ ← find n₁, r₂ ← find n₂,
do r₁ ← find n₁, r₂ ← find n₂;
unless (r₁ = r₂) $ throw "nodes are not equal"
def mergePackAux : Nat → Nat → Nat → M Unit
| 0 _ _ := pure ()
| (i+1) n d :=
do c ← capacity,
do c ← capacity;
if (n+d) < c
then union n (n+d) *> mergePackAux i (n+1) d
else pure ()
@ -68,23 +68,23 @@ do 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 c ← capacity;
if n < c
then do { 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 c ← capacity;
numEqsAux c 0 0
def test (n : Nat) : M Nat :=
if n < 2 then throw "input must be greater than 1"
else do
mkNodes n,
mergePack 50000,
mergePack 10000,
mergePack 5000,
mergePack 1000,
mkNodes n;
mergePack 50000;
mergePack 10000;
mergePack 5000;
mergePack 1000;
numEqs
def main (xs : List String) : IO UInt32 :=

56
tests/compiler/array_test.lean
View file

@ -7,32 +7,32 @@ a
def main : IO UInt32 :=
do
let a : Array Nat := Array.empty,
IO.println (toString a),
IO.println (toString a.sz),
let a := foo a,
IO.println (toString a),
let a := a.map (+10),
IO.println (toString a),
IO.println (toString a.sz),
let a1 := a.pop,
let a2 := a.push 100,
IO.println (toString a1),
IO.println (toString a2),
let a2 := a.pop,
IO.println a2,
IO.println $ (([1, 2, 3, 4].toArray).map (+2)).map toString,
IO.println $ ([1, 2, 3, 4].toArray.extract 1 3),
IO.println $ ([1, 2, 3, 4].toArray.extract 0 100),
IO.println $ ([1, 2, 3, 4].toArray.extract 1 1),
IO.println $ ([1, 2, 3, 4].toArray.extract 2 4),
IO.println [1,2,3,4].toArray.reverse,
IO.println ([] : List Nat).toArray.reverse,
IO.println [1,2,3].toArray.reverse,
IO.println $ [1,2,3,4].toArray.filter (λ a, a % 2 == 0),
IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 0),
IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 1),
IO.println $ [1,2,3,4].toArray.filter (>2),
IO.println $ [1,2,3,4].toArray.filter (>10),
IO.println $ [1,2,3,4].toArray.filter (>0),
let a : Array Nat := Array.empty;
IO.println (toString a);
IO.println (toString a.sz);
let a := foo a;
IO.println (toString a);
let a := a.map (+10);
IO.println (toString a);
IO.println (toString a.sz);
let a1 := a.pop;
let a2 := a.push 100;
IO.println (toString a1);
IO.println (toString a2);
let a2 := a.pop;
IO.println a2;
IO.println $ (([1, 2, 3, 4].toArray).map (+2)).map toString;
IO.println $ ([1, 2, 3, 4].toArray.extract 1 3);
IO.println $ ([1, 2, 3, 4].toArray.extract 0 100);
IO.println $ ([1, 2, 3, 4].toArray.extract 1 1);
IO.println $ ([1, 2, 3, 4].toArray.extract 2 4);
IO.println [1,2,3,4].toArray.reverse;
IO.println ([] : List Nat).toArray.reverse;
IO.println [1,2,3].toArray.reverse;
IO.println $ [1,2,3,4].toArray.filter (λ a, a % 2 == 0);
IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 0);
IO.println $ [1,2,3,4,5].toArray.filter (λ a, a % 2 == 1);
IO.println $ [1,2,3,4].toArray.filter (>2);
IO.println $ [1,2,3,4].toArray.filter (>10);
IO.println $ [1,2,3,4].toArray.filter (>0);
pure 0

10
tests/compiler/array_test2.lean
View file

@ -7,9 +7,9 @@ let a1 := [2, 3, 5].toArray in
let a2 := [4, 7, 9].toArray in
let a3 := [4, 7, 8].toArray in
do
check (Array.isEqv a1 a2 (λ v w, v % 2 == w % 2)),
check (!Array.isEqv a1 a3 (λ v w, v % 2 == w % 2)),
check (a1 ++ a2 == [2, 3, 5, 4, 7, 9].toArray),
check (a1.any (>4)),
check (!a1.any (>10)),
check (Array.isEqv a1 a2 (λ v w, v % 2 == w % 2));
check (!Array.isEqv a1 a3 (λ v w, v % 2 == w % 2));
check (a1 ++ a2 == [2, 3, 5, 4, 7, 9].toArray);
check (a1.any (>4));
check (!a1.any (>10));
check (a1.all (<10))

14
tests/compiler/lazylist.lean
View file

@ -114,14 +114,14 @@ def iota (i : Nat := 0) : LazyList Nat :=
LazyList.iterate Nat.succ i
def tst : LazyList String :=
do x ← [1, 2, 3].toLazy,
y ← [2, 3, 4].toLazy,
guard (x + y > 5),
do x ← [1, 2, 3].toLazy;
y ← [2, 3, 4].toLazy;
guard (x + y > 5);
pure (toString x ++ " + " ++ toString y ++ " = " ++ toString (x+y))
def main : IO Unit :=
do let n := 40,
IO.println $ tst.isEmpty,
IO.println $ tst.head,
IO.println $ (fib.interleave (iota.map (+100))).approx n,
do let n := 40;
IO.println $ tst.isEmpty;
IO.println $ tst.head;
IO.println $ (fib.interleave (iota.map (+100))).approx n;
IO.println $ (((iota.map (+10)).filter (λ v, v % 2 == 0)).approx n)

66
tests/compiler/rbmap.lean
View file

@ -8,29 +8,29 @@ def depth {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
m.depth Nat.max
def tst1 : IO Unit :=
do let Map := RBMap String Nat (λ a b, a < b),
let m : Map := {},
let m := m.insert "hello" 0,
let m := m.insert "world" 1,
check (m.find "hello" == some 0),
check (m.find "world" == some 1),
let m := m.erase "hello",
check (m.find "hello" == none),
check (m.find "world" == some 1),
do let Map := RBMap String Nat (λ a b, a < b);
let m : Map := {};
let m := m.insert "hello" 0;
let m := m.insert "world" 1;
check (m.find "hello" == some 0);
check (m.find "world" == some 1);
let m := m.erase "hello";
check (m.find "hello" == none);
check (m.find "world" == some 1);
pure ()
def tst2 : IO Unit :=
do let Map := RBMap Nat Nat (λ a b, a < b),
let m : Map := {},
let n : Nat := 10000,
let m := n.fold (λ i (m : Map), m.insert i (i*10)) m,
check (m.all (λ k v, v == k*10)),
check (sz m == n),
IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m)),
let m := (n/2).fold (λ i (m : Map), m.erase (2*i)) m,
check (m.all (λ k v, v == k*10)),
check (sz m == n / 2),
IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m)),
do let Map := RBMap Nat Nat (λ a b, a < b);
let m : Map := {};
let n : Nat := 10000;
let m := n.fold (λ i (m : Map), m.insert i (i*10)) m;
check (m.all (λ k v, v == k*10));
check (sz m == n);
IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m));
let m := (n/2).fold (λ i (m : Map), m.erase (2*i)) m;
check (m.all (λ k v, v == k*10));
check (sz m == n / 2);
IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m));
pure ()
abbrev Map := RBMap Nat Nat (λ a b, a < b)
@ -38,25 +38,25 @@ abbrev Map := RBMap Nat Nat (λ a b, a < b)
def mkRandMap (max : Nat) : Nat → Map → Array (Nat × Nat) → IO (Map × Array (Nat × Nat))
| 0 m a := pure (m, a)
| (n+1) m a := do
k ← IO.rand 0 max,
v ← IO.rand 0 max,
k ← IO.rand 0 max;
v ← IO.rand 0 max;
if m.find k == none then do
let m := m.insert k v,
let a := a.push (k, v),
let m := m.insert k v;
let a := a.push (k, v);
mkRandMap n m a
else
mkRandMap n m a
def tst3 (seed : Nat) (n : Nat) (max : Nat) : IO Unit :=
do IO.setRandSeed seed,
(m, a) ← mkRandMap max n {} Array.empty,
check (sz m == a.size),
check (a.all (λ ⟨k, v⟩, m.find k == some v)),
IO.println ("tst3 size: " ++ toString a.size),
let m := a.iterate m (λ i ⟨k, v⟩ m, if i.val % 2 == 0 then m.erase k else m),
check (sz m == a.size / 2),
a.miterate () (λ i ⟨k, v⟩ _, when (i.val % 2 == 1) (check (m.find k == some v))),
IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m)),
do IO.setRandSeed seed;
(m, a) ← mkRandMap max n {} Array.empty;
check (sz m == a.size);
check (a.all (λ ⟨k, v⟩, m.find k == some v));
IO.println ("tst3 size: " ++ toString a.size);
let m := a.iterate m (λ i ⟨k, v⟩ m, if i.val % 2 == 0 then m.erase k else m);
check (sz m == a.size / 2);
a.miterate () (λ i ⟨k, v⟩ _, when (i.val % 2 == 1) (check (m.find k == some v)));
IO.println ("tst3 after, depth: " ++ toString (depth m) ++ ", size: " ++ toString (sz m));
pure ()
def main (xs : List String) : IO Unit :=

4
tests/compiler/reusebug.lean
View file

@ -23,6 +23,6 @@ def add (a b : Expr) : Expr :=
addAux a b
def main (xs : List String) : IO UInt32 :=
do let x := Var "x",
IO.println (add (Val 1) (Add (Mul (Val 2) x) x)),
do let x := Var "x";
IO.println (add (Val 1) (Add (Mul (Val 2) x) x));
pure 0

10
tests/compiler/t2.lean
View file

@ -85,14 +85,14 @@ nestAux n f n e
def deriv (i : Nat) (f : Expr) : IO Expr :=
do
let d := d "x" f,
IO.println (toString (i+1) ++ " count: " ++ (toString $ count d)),
let d := d "x" f;
IO.println (toString (i+1) ++ " count: " ++ (toString $ count d));
pure d
def main (xs : List String) : IO UInt32 :=
do let x := Var "x",
let f := pow x x,
nest deriv 9 f,
do let x := Var "x";
let f := pow x x;
nest deriv 9 f;
pure 0
-- setOption profiler True

14
tests/compiler/t4.lean
View file

@ -98,16 +98,16 @@ nestAux n f n e
def deriv (i : Nat) (f : Expr) : IO Expr :=
do
let d := d "x" f,
IO.println (toString (i+1) ++ " count: " ++ (toString $ count d)),
IO.println (toString d),
let d := d "x" f;
IO.println (toString (i+1) ++ " count: " ++ (toString $ count d));
IO.println (toString d);
pure d
def main (xs : List String) : IO UInt32 :=
do let x := Var "x",
let f := add x (mul x (mul x (add x x))),
IO.println f,
nest deriv 3 f,
do let x := Var "x";
let f := add x (mul x (mul x (add x x)));
IO.println f;
nest deriv 3 f;
pure 0
-- setOption profiler True

8
tests/ir/lirc.lean
View file

@ -3,11 +3,11 @@ import init.Lean.Ir.lirc
open Lean.Ir IO
def main : IO Unit :=
do args ← IO.cmdlineArgs,
do args ← IO.cmdlineArgs;
unless (args.length = 1) $
IO.fail "Error: incorrect number of arguments, expected `lirc file.Lean`",
let fname := args.head,
input ← Fs.readFile fname,
IO.fail "Error: incorrect number of arguments, expected `lirc file.Lean`";
let fname := args.head;
input ← Fs.readFile fname;
match lirc input {mainProc := some "main"} with
| Except.ok r := Fs.writeFile (fname ++ ".cpp") r
| Except.error e := IO.fail (toString e)

4
tests/lean/repr_issue.lean
View file

@ -1,7 +1,7 @@
def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
catch (do modify $ λ a : Array Nat, a.set 0 33,
catch (do modify $ λ a : Array Nat, a.set 0 33;
throw "error")
(λ _, do a ← get, pure $ a.get 0)
(λ _, do a ← get; pure $ a.get 0)
def ex₁ : StateT (Array Nat) (ExceptT String Id) Nat :=
foo

46
tests/lean/run/coroutine.lean
View file

@ -156,16 +156,16 @@ inductive tree (α : Type u)
unsafe def visit {α : Type v} : tree α → coroutine Unit α Unit
| tree.leaf := pure ()
| (tree.Node l a r) := do
visit l,
yield a,
visit l;
yield a;
visit r
unsafe def tst {α : Type} [HasToString α] (t : tree α) : ExceptT String IO Unit :=
do c ← pure $ visit t,
(yielded v₁ c) ← pure $ resume c (),
(yielded v₂ c) ← pure $ resume c (),
IO.println $ toString v₁,
IO.println $ toString v₂,
do c ← pure $ visit t;
(yielded v₁ c) ← pure $ resume c ();
(yielded v₂ c) ← pure $ resume c ();
IO.println $ toString v₁;
IO.println $ toString v₂;
pure ()
-- #eval tst (tree.Node (tree.Node (tree.Node tree.leaf 5 tree.leaf) 10 (tree.Node tree.leaf 20 tree.leaf)) 30 tree.leaf)
@ -176,25 +176,25 @@ namespace ex2
unsafe def ex : StateT Nat (coroutine Nat String) Unit :=
do
x ← read,
y ← get,
set (y+5),
yield ("1) val: " ++ toString (x+y)),
x ← read,
y ← get,
yield ("2) val: " ++ toString (x+y)),
x ← read;
y ← get;
set (y+5);
yield ("1) val: " ++ toString (x+y));
x ← read;
y ← get;
yield ("2) val: " ++ toString (x+y));
pure ()
unsafe def tst2 : ExceptT String IO Unit :=
do let c := StateT.run ex 5,
(yielded r c₁) ← pure $ resume c 10,
IO.println r,
(yielded r c₂) ← pure $ resume c₁ 20,
IO.println r,
(done _) ← pure $ resume c₂ 30,
(yielded r c₃) ← pure $ resume c₁ 100,
IO.println r,
IO.println "done",
do let c := StateT.run ex 5;
(yielded r c₁) ← pure $ resume c 10;
IO.println r;
(yielded r c₂) ← pure $ resume c₁ 20;
IO.println r;
(done _) ← pure $ resume c₂ 30;
(yielded r c₃) ← pure $ resume c₁ 100;
IO.println r;
IO.println "done";
pure ()
-- #eval tst2

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

@ -84,13 +84,13 @@ unsafe def nest (f : Expr → IO Expr) : Nat → Expr → IO Expr
unsafe def deriv (f : Expr) : IO Expr :=
do
let d := d "x" f,
IO.print "count: ",
IO.println (count f),
let d := d "x" f;
IO.print "count: ";
IO.println (count f);
pure d
unsafe def main : IO Unit :=
do let x := Var "x",
let f := pow x x,
nest deriv 9 f,
do let x := Var "x";
let f := pow x x;
nest deriv 9 f;
pure ()

28
tests/lean/run/ext_eff.lean
View file

@ -120,9 +120,9 @@ inductive State (σ : Type) : Type → Type
@[inline] def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get
@[inline] def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s)
instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
⟨λ α x, do st ← eff.get,
let ⟨a, s'⟩ := x.run st,
eff.put s',
⟨λ α x, do st ← eff.get;
let ⟨a, s'⟩ := x.run st;
eff.put s';
pure a⟩
@[inline] def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=
@ -169,7 +169,7 @@ instance : HasRepr IO.error :=
| IO.error.other s := "IO.error.other " ++ repr s⟩
@[inline] def eff.catchIO {effs α} [member IO effs] (x : eff effs α) (catch : IO.error → eff effs α) : eff effs α :=
x.interpose IO pure (λ β x k, do ex ← monadLift x.try,
x.interpose IO pure (λ β x k, do ex ← monadLift x.try;
match ex with
| Except.ok b := k b
| Except.error e := catch e)
@ -185,12 +185,12 @@ eff.catchIO (Except.ok <$> x) (pure ∘ Except.error)
-- handle IO exceptions before State
def test1 :=
let tf : Bool → eff [IO] _ := λ (x : Bool), Reader.run x $ State.run ([] : List String) $ eff.tryIo $
do modify (λ xs, "begin"::xs),
x ← read,
r ← monadLift $ exfn x,
modify (λ xs, "end"::xs),
do modify (λ xs, "begin"::xs);
x ← read;
r ← monadLift $ exfn x;
modify (λ xs, "end"::xs);
pure r in
do repr <$> eff.runM (tf tt) >>= IO.println,
do repr <$> eff.runM (tf tt) >>= IO.println;
repr <$> eff.runM (tf ff) >>= IO.println
#eval test1
@ -198,12 +198,12 @@ def test1 :=
-- handle IO exceptions after State
def test2 :=
let tf : Bool → eff [IO] _ := λ (x : Bool), Reader.run x $ eff.tryIo $ State.run ([] : List String) $
do modify (λ xs, "begin"::xs),
x ← read,
r ← monadLift $ exfn x,
modify (λ xs, "end"::xs),
do modify (λ xs, "begin"::xs);
x ← read;
r ← monadLift $ exfn x;
modify (λ xs, "end"::xs);
pure r in
do repr <$> eff.runM (tf tt) >>= IO.println,
do repr <$> eff.runM (tf tt) >>= IO.println;
repr <$> eff.runM (tf ff) >>= IO.println
#eval test2

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

@ -134,9 +134,9 @@ inductive State (σ : Type) : Type → Type
@[inline] meta def eff.get {σ effs} [member (State σ) effs] : eff effs σ := eff.send State.get
@[inline] meta def eff.put {σ effs} [member (State σ) effs] (s : σ) : eff effs Unit := eff.send (State.put s)
meta instance {σ effs} [member (State σ) effs] : MonadState σ (eff effs) :=
⟨λ α x, do st ← eff.get,
let ⟨a, s'⟩ := x.run st,
eff.put s',
⟨λ α x, do st ← eff.get;
let ⟨a, s'⟩ := x.run st;
eff.put s';
pure a⟩
meta def State.run {σ effs α} (st : σ) : eff (State σ :: effs) α → eff effs (α × σ) :=

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

@ -42,5 +42,5 @@ first-order unification.
-/
def foo2 : StateT δ (StateT σ Id) σ :=
do s : σ ← monadLift (get : StateT σ Id σ),
do s : σ ← monadLift (get : StateT σ Id σ);
pure s