From f879cdb12feea1b2587ca339dc96d0e3f41affb2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 14 Feb 2019 15:32:19 -0800
Subject: [PATCH] test(tests/playground): add new example in Lean and OCaml

@kha I wrote a simple test in Lean and OCaml. Right now, the numbers on
my machine are

arith_eval.ml         8.13 secs
arith_eval_nat.lean   10.71 secs

OCaml is computing with machine boxed integers, and we are computing
with `nat`. Our version is more expensive since we have to check
whether the number is small or big, and whether the result needs to be a
mpz value or not.

Almost half of our runtime is spent deallocating the big object returned
by `mk_expr`. The deferred free feature does not help here because
we don't deallocate the object in the end but as we execute `eeval`.
So, we perform many small invocations to `del`. None of them take
long, but the overall cost is super high. I can use a different strategy
where `del(o)` just updates the `g_to_free` list, and we deallocate
at most `LEAN_DEFERRED_FREE_QUOTA` at each allocation. The current
deferred free approach would also work if we could use the borrowed
annotations in `eeval`. In this case, we would not delete the input
expression as we evaluate it.

As an experiment, I manually added a `lean::inc` before invoking
`eeval`. The idea was prevent memory deallocation. With this
modification, the program runs in 5.87 secs.

BTW, I also wrote a version using uint32 (arith_eval_uint32.lean),
but the current compiler generates poor code for it.
I know how to fix the performance problem.
---
 tests/playground/arith_eval.ml          | 19 +++++++++++++++++++
 tests/playground/arith_eval_nat.lean    | 19 +++++++++++++++++++
 tests/playground/arith_eval_uint32.lean | 22 ++++++++++++++++++++++
 3 files changed, 60 insertions(+)
 create mode 100644 tests/playground/arith_eval.ml
 create mode 100644 tests/playground/arith_eval_nat.lean
 create mode 100644 tests/playground/arith_eval_uint32.lean

diff --git a/tests/playground/arith_eval.ml b/tests/playground/arith_eval.ml
new file mode 100644
index 0000000000..9c6bb753db
--- /dev/null
+++ b/tests/playground/arith_eval.ml
@@ -0,0 +1,19 @@
+type expr =
+| Var of int
+| Val of int
+| Add of expr * expr;;
+
+let dec n =
+  if n == 0 then 0 else n - 1;;
+
+let rec mk_expr n v =
+  if n == 0 then Val v
+  else Add (mk_expr (n-1) (v+1), mk_expr (n-1) (dec v));;
+
+let rec eeval e =
+ match e with
+ | Val n -> n
+ | Var x -> 0
+ | Add (l, r) -> eeval l + eeval r;;
+
+Printf.printf "%8d\n" (eeval (mk_expr 26 1));;
diff --git a/tests/playground/arith_eval_nat.lean b/tests/playground/arith_eval_nat.lean
new file mode 100644
index 0000000000..a3554eba73
--- /dev/null
+++ b/tests/playground/arith_eval_nat.lean
@@ -0,0 +1,19 @@
+inductive Expr
+| Var : nat → Expr
+| Val : nat → Expr
+| Add : Expr → Expr → Expr
+
+open Expr nat
+
+def mk_expr : nat → nat → Expr
+| 0        v := Val v
+| (succ n) v := Add (mk_expr n (v+1)) (mk_expr n (v-1))
+
+def eval : Expr → nat
+| (Var x) := 0
+| (Val v) := v
+| (Add l r) := eval l + eval r
+
+def main : io uint32 :=
+io.println' (to_string $ eval (mk_expr 26 1)) *>
+pure 0
diff --git a/tests/playground/arith_eval_uint32.lean b/tests/playground/arith_eval_uint32.lean
new file mode 100644
index 0000000000..e78e69681e
--- /dev/null
+++ b/tests/playground/arith_eval_uint32.lean
@@ -0,0 +1,22 @@
+inductive Expr
+| Var : uint32 → Expr
+| Val : uint32 → Expr
+| Add : Expr → Expr → Expr
+
+open Expr
+
+def dec (n : uint32) : uint32 :=
+if n = 0 then 0 else n-1
+
+def mk_expr : uint32 → uint32 → Expr | n v :=
+if n = 0 then Val v
+else Add (mk_expr (n-1) (v+1)) (mk_expr (n-1) (dec v))
+
+def eval : Expr → uint32
+| (Var x) := 0
+| (Val v) := v
+| (Add l r) := eval l + eval r
+
+def main : io uint32 :=
+io.println' (to_string $ eval (mk_expr 26 1)) *>
+pure 0