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

chore(tests/playground): fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-10 11:36:39 -07:00
parent c9cd693b8e
commit 3ef8845163
4 changed files with 18 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/playground/task_test.lean
View file

@ -1,20 +1,20 @@
def g (x : Nat) : Nat :=
dbgTrace ("g: " ++ toString x) $ λ _,
dbgTrace ("g: " ++ toString x) $ fun _ =>
x + 1
def f1 (x : Nat) : Nat :=
dbgSleep 1000 $ λ _,
dbgTrace ("f1: " ++ toString x) $ λ _,
dbgSleep 1000 $ fun _ =>
dbgTrace ("f1: " ++ toString x) $ fun _ =>
g (x + 1)
def f2 (x : Nat) : Nat :=
dbgSleep 100 $ λ _,
dbgTrace ("f2: " ++ toString x) $ λ _,
dbgSleep 100 $ fun _ =>
dbgTrace ("f2: " ++ toString x) $ fun _ =>
g x
def main (xs : List String) : IO UInt32 :=
let t1 := Task.mk $ (λ _, f1 xs.head.toNat) in
let t2 := Task.mk $ (λ _, f2 xs.head.toNat) in
dbgSleep 1000 $ λ _,
let t1 := Task.mk $ (fun _ => f1 xs.head.toNat) in
let t2 := Task.mk $ (fun _ => f2 xs.head.toNat) in
dbgSleep 1000 $ fun _ =>
IO.println (toString t1.get ++ " " ++ toString t2.get) *>
pure 0

8
tests/playground/task_test2.lean
View file

@ -1,12 +1,12 @@
def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat :=
n.repeat (λ r,
dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ λ _,
xs.foldl (+) r)
n.repeat (fun r =>
dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ fun _ =>
xs.foldl (fun a b => a + b) r)
0
def main (xs : List String) : IO UInt32 :=
let ys := (List.replicate xs.head.toNat 1) in
let ts : List (Task Nat) := (List.iota 10).map (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) in
let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in
let ns : List Nat := ts.map Task.get in
IO.println (">> " ++ toString ns) *>
pure 0

6
tests/playground/task_test3.lean
View file

@ -1,12 +1,12 @@
def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat :=
n.repeat (λ r,
n.repeat (fun r =>
-- dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ λ _,
xs.foldl (+) (r+i))
xs.foldl (fun a b => a + b) (r+i))
0
def main (xs : List String) : IO UInt32 :=
let ys := (List.replicate xs.head.toNat 1) in
let ts : List (Task Nat) := (List.iota 10).map (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) in
let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in
let ns : List Nat := ts.map Task.get in
IO.println (">> " ++ toString ns) *>
pure 0

6
tests/playground/task_test4.lean
View file

@ -1,12 +1,12 @@
def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat :=
n.repeat (λ r,
n.repeat (fun r =>
let s := (">> [" ++ toString i ++ "] " ++ toString r) in
xs.foldl (+) (r + s.length))
xs.foldl (fun a b => a + b) (r + s.length))
0
def main (xs : List String) : IO UInt32 :=
let ys := (List.replicate xs.head.toNat 1) in
let ts : List (Task Nat) := (List.iota 10).map (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) in
let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in
let ns : List Nat := ts.map Task.get in
IO.println (">> " ++ toString ns) *>
pure 0