From 3dea7ae0d6bbb18536a922ee2df2735809867b60 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Nov 2013 16:07:15 -0800
Subject: [PATCH] test(frontends/lean): example mixing Lean and Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/lua9.lean              | 38 +++++++++++++++++++++++++++++++
 tests/lean/lua9.lean.expected.out | 12 ++++++++++
 2 files changed, 50 insertions(+)
 create mode 100644 tests/lean/lua9.lean
 create mode 100644 tests/lean/lua9.lean.expected.out

diff --git a/tests/lean/lua9.lean b/tests/lean/lua9.lean
new file mode 100644
index 000000000..8abe33c93
--- /dev/null
+++ b/tests/lean/lua9.lean
@@ -0,0 +1,38 @@
+
+Variable x : Bool
+
+(**
+ local env    = get_environment()
+ local Int    = Const("Int")
+ local plus   = Const(name("Int", "add"))
+ local x1, x2 = Consts("x1, x2")
+ print(env:check_type(Int))
+ print(env:check_type(plus))
+ env:add_var("x1", Int)
+ env:add_var("x2", Int)
+ print(plus(x1, x2))
+ print(env:check_type(plus(x1)))
+
+ function sum(...)
+    local args = {...}
+    if #args == 0 then
+       error("sum must have at least one argument")
+    else
+       local r = args[1]
+       for i = 2, #args do
+          r = plus(r, args[i])
+       end
+       return r
+    end
+ end
+
+ local s = sum(x1, x1, x1, x2, x2)
+ print(s)
+ print(env:check_type(s))
+ env:add_definition("sum1", s)
+**)
+
+Show Environment 1
+Eval sum1
+Variable y : Bool
+
diff --git a/tests/lean/lua9.lean.expected.out b/tests/lean/lua9.lean.expected.out
new file mode 100644
index 000000000..4a3f84000
--- /dev/null
+++ b/tests/lean/lua9.lean.expected.out
@@ -0,0 +1,12 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+Type
+ℤ → ℤ → ℤ
+x1 + x2
+ℤ → ℤ
+x1 + x1 + x1 + x2 + x2
+ℤ
+Definition sum1 : ℤ := x1 + x1 + x1 + x2 + x2
+x1 + x1 + x1 + x2 + x2
+  Assumed: y