6f852cf7af
@kha I have added `timeit` for running experiments for the paper.
We have to be careful because `timeit` may produce incorrect results
due to compiler optimizations (e.g., ground term extraction).
Here are examples that do not produce the result we expect:
```
def main : io uint32 :=
timeit "tst" (io.println' ("result " ++ to_string (tst 1000000))) *>
pure 0
```
```
def main (xs : list string) : io uint32 :=
timeit "tst" (io.println' ("result " ++ to_string (tst xs.head.to_nat))) *>
pure 0
```
11 lines
258 B
Text
11 lines
258 B
Text
def tst (n : nat) : nat :=
|
|
let xs := list.repeat 1 n in
|
|
xs.foldl (+) 0
|
|
|
|
def perf (n : nat) : io unit :=
|
|
do v ← pure $ tst n,
|
|
io.println' ("result " ++ to_string v)
|
|
|
|
def main (xs : list string) : io uint32 :=
|
|
timeit "tst" (perf xs.head.to_nat) *>
|
|
pure 0
|