refactor(frontends/lua): replace lean.lua.h with util.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/extra/util.lua

@@ -0,0 +1,16 @@
+-- Extra useful functions
+
+-- Create sequence of expressions.
+-- Examples:
+--    local a, b, c = Consts("a,b,c")
+-- We can use ';', ' ', ',', tabs ad line breaks for separating the constant names
+--    local a, b, c = Consts("a b c")
+function Consts(s)
+   r = {}
+   i = 1
+   for c in string.gmatch(s, '[^ ,;\\t\\n]+') do
+      r[i] = Const(c)
+      i = i + 1
+   end
+   return unpack(r)
+end

src/frontends/lua/lean.lua.h

@@ -1,16 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-static char const * g_extra_code =
-    "function Consts(s)\n"
-    "  r = {}\n"
-    "  i = 1\n"
-    "  for c in string.gmatch(s, '[^ ,;\\t\\n]+') do\n"
-    "     r[i] = Const(c)\n"
-    "     i = i + 1\n"
-    "  end\n"
-    "  return unpack(r)\n"
-    "end\n";

src/frontends/lua/register_modules.cpp

@@ -11,7 +11,6 @@ Author: Leonardo de Moura
 #include "library/arith/register_module.h"
 #include "library/tactic/register_module.h"
 #include "frontends/lean/register_module.h"
-#include "frontends/lua/lean.lua.h"
 
 namespace lean {
 void register_modules() {
@@ -21,6 +20,5 @@ void register_modules() {
     register_arith_module();
     register_tactic_module();
     register_frontend_lean_module();
-    script_state::register_code(g_extra_code);
 }
 }

tests/lean/lua12.lean

@@ -1,14 +1,13 @@
 Variables x y z : Int
 
 (**
-
+ import("util.lua")
  local env  = get_environment()
  local plus = Const{"Int", "add"}
  local x, y = Consts("x y")
  local def  = plus(plus(x, y), iVal(1000))
  print(def, ":", env:type_check(def))
  env:add_definition("sum", def)
-
 **)
 
 Eval sum + 3

tests/lean/lua9.lean

@@ -1,6 +1,7 @@
 Variable x : Bool
 
 (**
+ import("util.lua")
  local env    = get_environment()
  local Int    = Const("Int")
  local plus   = Const{"Int", "add"}

tests/lua/big.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 f, a, b = Consts("f, a, b")
 nodes = {}
 

tests/lua/env1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 e = environment()
 assert(is_environment(e))
 e:add_uvar("M1")

tests/lua/expr2.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 f = Const("f")
 x = Const("x")
 y = Const("y")

tests/lua/expr6.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 function print_leaves(e, ctx)
    if (not e) then
       return

tests/lua/expr7.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local f, g, a, b, c, d = Consts("f, g, a, b, c, d")
 local x = Var(0)
 local y = Var(1)
@@ -16,4 +17,3 @@ assert(F:lift_free_vars(1):abstract(a):instantiate{c, d} == f(g(c, d), f(b, f(c,
 assert(F:lift_free_vars(1):abstract(a):instantiate{c, d}:abstract{c, b} == f(g(y, d), f(x, f(y, y))))
 assert(F:lift_free_vars(1):lower_free_vars(1) == F)
 assert(F:lift_free_vars(0, 1):lower_free_vars(1, 1) == F)
-

tests/lua/expr8.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local f, g, a, b, c, d = Consts("f, g, a, b, c, d")
 local N, M = Consts("N, M")
 local x = Var(0)

tests/lua/front.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local env = environment()
 print(get_options())
 parse_lean_cmds([[

tests/lua/map.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 -- This examples demonstrates that Lean objects are not very useful as Lua table keys.
 local f = Const("f")
 local m = {}

tests/lua/menv1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local menv = metavar_env()
 assert(is_metavar_env(menv))
 local m1   = menv:mk_metavar()

tests/lua/parser2.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local env = environment()
 parse_lean_cmds([[
    Variable N : Type

tests/lua/proof_state1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local ps   = proof_state()
 local env  = environment()
 local Bool = Const("Bool")
@@ -23,5 +24,3 @@ local pb   = ps:proof_builder()
 local cb   = ps:cex_builder()
 assert(not ps:is_proof_final_state())
 assert(not ps:is_cex_final_state())
-
-

tests/lua/tactic1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local ps   = proof_state()
 local env  = environment()
 local Bool = Const("Bool")

tests/lua/template1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 import("template.lua")
 local env = environment()
 parse_lean_cmds([[

tests/lua/test.sh

@@ -8,7 +8,7 @@ LEAN=$1
 NUM_ERRORS=0
 for f in `ls *.lua`; do
     echo "-- testing $f"
-    if $LEAN util.lua $f > $f.produced.out; then
+    if $LEAN extra.lua $f > $f.produced.out; then
         echo "-- worked"
     else
         echo "ERROR executing $f, produced output is at $f.produced.out"

tests/lua/test_single.sh

@@ -7,7 +7,7 @@ ulimit -s unlimited
 LEAN=$1
 f=$2
 echo "-- testing $f"
-if $LEAN util.lua $f > $f.produced.out; then
+if $LEAN extra.lua $f > $f.produced.out; then
     echo "-- worked"
     exit 0
 else

tests/lua/threads/tactic1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local env  = environment()
 local ios  = io_state()
 local Bool = Const("Bool")

tests/lua/threads/tactic2.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local env  = environment()
 local ios  = io_state()
 local Bool = Const("Bool")

tests/lua/unify1.lua

@@ -1,3 +1,4 @@
+import("util.lua")
 local f, g, a, b, c, x = Consts("f, g, a, b, c, x")
 local m1 = mk_metavar("m1")
 local m2 = mk_metavar("m2")