From 7469146b0dd73dcfbe271004edc0bc2e9156350c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Nov 2019 11:28:43 -0800
Subject: [PATCH] test: add tests for MetaM

---
 tests/lean/run/meta1.lean | 51 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 tests/lean/run/meta1.lean

diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
new file mode 100644
index 0000000000..c385b1dcc7
--- /dev/null
+++ b/tests/lean/run/meta1.lean
@@ -0,0 +1,51 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+def tstInferType (mods : List Name) (e : Expr) : IO Unit :=
+do env ← importModules mods;
+   match inferType e {} { env := env } with
+   | EStateM.Result.ok type s   => IO.println (toString e ++ " : " ++ toString type)
+   | EStateM.Result.error err _ => throw (IO.userError (toString err))
+
+def tstWHNF (mods : List Name) (e : Expr) : IO Unit :=
+do env ← importModules mods;
+   match whnf e {} { env := env } with
+   | EStateM.Result.ok type s   => IO.println (toString e ++ " ==> " ++ toString type)
+   | EStateM.Result.error err _ => throw (IO.userError (toString err))
+
+def t1 : Expr :=
+let map  := Expr.const `List.map [Level.one, Level.one];
+let nat  := Expr.const `Nat [];
+let bool := Expr.const `Bool [];
+mkApp map #[nat, bool]
+
+#eval tstInferType [`Init.Data.List] t1
+
+def t2 : Expr :=
+let prop := Expr.sort Level.zero;
+Expr.forallE `x BinderInfo.default prop prop
+
+#eval tstInferType [`Init.Core] t2
+
+def t3 : Expr :=
+let nat   := Expr.const `Nat [];
+let natLe := Expr.const `Nat.le [];
+let zero  := Expr.lit (Literal.natVal 0);
+let p     := mkApp natLe #[Expr.bvar 0, zero];
+Expr.forallE `x BinderInfo.default nat p
+
+#eval tstInferType [`Init.Data.Nat] t3
+
+def t4 : Expr :=
+let nat   := Expr.const `Nat [];
+let p     := mkApp (Expr.const `Nat.succ []) #[Expr.bvar 0];
+Expr.lam `x BinderInfo.default nat p
+
+#eval tstInferType [`Init.Core] t4
+
+def t5 : Expr :=
+let add   := Expr.const `Nat.add [];
+mkApp add #[Expr.lit (Literal.natVal 3), Expr.lit (Literal.natVal 5)]
+
+#eval tstWHNF [`Init.Data.Nat] t5