From 3f0279b88c6e8164ade2e420847e9a041389a32a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Dec 2013 19:49:04 -0800 Subject: [PATCH] refactor(frontends/lua): replace lean.lua.h with util.lua Signed-off-by: Leonardo de Moura --- src/extra/util.lua | 16 ++++++++++++++++ src/frontends/lua/lean.lua.h | 16 ---------------- src/frontends/lua/register_modules.cpp | 2 -- tests/lean/lua12.lean | 3 +-- tests/lean/lua9.lean | 1 + tests/lua/big.lua | 1 + tests/lua/env1.lua | 1 + tests/lua/expr2.lua | 1 + tests/lua/expr6.lua | 1 + tests/lua/expr7.lua | 2 +- tests/lua/expr8.lua | 1 + tests/lua/{threads/util.lua => extra.lua} | 0 tests/lua/front.lua | 1 + tests/lua/map.lua | 1 + tests/lua/menv1.lua | 1 + tests/lua/parser2.lua | 1 + tests/lua/proof_state1.lua | 3 +-- tests/lua/tactic1.lua | 1 + tests/lua/template1.lua | 1 + tests/lua/test.sh | 2 +- tests/lua/test_single.sh | 2 +- tests/lua/{util.lua => threads/extra.lua} | 0 tests/lua/threads/tactic1.lua | 1 + tests/lua/threads/tactic2.lua | 1 + tests/lua/unify1.lua | 1 + 25 files changed, 36 insertions(+), 25 deletions(-) create mode 100644 src/extra/util.lua delete mode 100644 src/frontends/lua/lean.lua.h rename tests/lua/{threads/util.lua => extra.lua} (100%) rename tests/lua/{util.lua => threads/extra.lua} (100%) diff --git a/src/extra/util.lua b/src/extra/util.lua new file mode 100644 index 000000000..36c9727b0 --- /dev/null +++ b/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 diff --git a/src/frontends/lua/lean.lua.h b/src/frontends/lua/lean.lua.h deleted file mode 100644 index 6eab707e6..000000000 --- a/src/frontends/lua/lean.lua.h +++ /dev/null @@ -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"; diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp index 7a507aa59..fed9a2c6f 100644 --- a/src/frontends/lua/register_modules.cpp +++ b/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); } } diff --git a/tests/lean/lua12.lean b/tests/lean/lua12.lean index ca689edc6..f9a182c35 100644 --- a/tests/lean/lua12.lean +++ b/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 diff --git a/tests/lean/lua9.lean b/tests/lean/lua9.lean index 42a72d204..5db440564 100644 --- a/tests/lean/lua9.lean +++ b/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"} diff --git a/tests/lua/big.lua b/tests/lua/big.lua index dfd11f2b9..9ef379b39 100644 --- a/tests/lua/big.lua +++ b/tests/lua/big.lua @@ -1,3 +1,4 @@ +import("util.lua") f, a, b = Consts("f, a, b") nodes = {} diff --git a/tests/lua/env1.lua b/tests/lua/env1.lua index 85b1131ff..508eafe08 100644 --- a/tests/lua/env1.lua +++ b/tests/lua/env1.lua @@ -1,3 +1,4 @@ +import("util.lua") e = environment() assert(is_environment(e)) e:add_uvar("M1") diff --git a/tests/lua/expr2.lua b/tests/lua/expr2.lua index 9d9af4abc..e3ada5a88 100644 --- a/tests/lua/expr2.lua +++ b/tests/lua/expr2.lua @@ -1,3 +1,4 @@ +import("util.lua") f = Const("f") x = Const("x") y = Const("y") diff --git a/tests/lua/expr6.lua b/tests/lua/expr6.lua index 0179190c5..fa7be96b2 100644 --- a/tests/lua/expr6.lua +++ b/tests/lua/expr6.lua @@ -1,3 +1,4 @@ +import("util.lua") function print_leaves(e, ctx) if (not e) then return diff --git a/tests/lua/expr7.lua b/tests/lua/expr7.lua index 1926776cd..6ac159ff6 100644 --- a/tests/lua/expr7.lua +++ b/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) - diff --git a/tests/lua/expr8.lua b/tests/lua/expr8.lua index e8c4614da..f99956853 100644 --- a/tests/lua/expr8.lua +++ b/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) diff --git a/tests/lua/threads/util.lua b/tests/lua/extra.lua similarity index 100% rename from tests/lua/threads/util.lua rename to tests/lua/extra.lua diff --git a/tests/lua/front.lua b/tests/lua/front.lua index 1d45eec71..7fe1ddcfb 100644 --- a/tests/lua/front.lua +++ b/tests/lua/front.lua @@ -1,3 +1,4 @@ +import("util.lua") local env = environment() print(get_options()) parse_lean_cmds([[ diff --git a/tests/lua/map.lua b/tests/lua/map.lua index 826b411dd..30177574a 100644 --- a/tests/lua/map.lua +++ b/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 = {} diff --git a/tests/lua/menv1.lua b/tests/lua/menv1.lua index f96da0675..0ca7b442f 100644 --- a/tests/lua/menv1.lua +++ b/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() diff --git a/tests/lua/parser2.lua b/tests/lua/parser2.lua index e62d38442..e9740678c 100644 --- a/tests/lua/parser2.lua +++ b/tests/lua/parser2.lua @@ -1,3 +1,4 @@ +import("util.lua") local env = environment() parse_lean_cmds([[ Variable N : Type diff --git a/tests/lua/proof_state1.lua b/tests/lua/proof_state1.lua index 8867b1f77..903c1e3cc 100644 --- a/tests/lua/proof_state1.lua +++ b/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()) - - diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua index d6bff9cf9..bc91677b3 100644 --- a/tests/lua/tactic1.lua +++ b/tests/lua/tactic1.lua @@ -1,3 +1,4 @@ +import("util.lua") local ps = proof_state() local env = environment() local Bool = Const("Bool") diff --git a/tests/lua/template1.lua b/tests/lua/template1.lua index 17bb0c3e0..1b4312b49 100644 --- a/tests/lua/template1.lua +++ b/tests/lua/template1.lua @@ -1,3 +1,4 @@ +import("util.lua") import("template.lua") local env = environment() parse_lean_cmds([[ diff --git a/tests/lua/test.sh b/tests/lua/test.sh index 4de60d7ad..625a8f616 100755 --- a/tests/lua/test.sh +++ b/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" diff --git a/tests/lua/test_single.sh b/tests/lua/test_single.sh index 66f12f077..a94e2a90e 100755 --- a/tests/lua/test_single.sh +++ b/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 diff --git a/tests/lua/util.lua b/tests/lua/threads/extra.lua similarity index 100% rename from tests/lua/util.lua rename to tests/lua/threads/extra.lua diff --git a/tests/lua/threads/tactic1.lua b/tests/lua/threads/tactic1.lua index ebd2624be..45981dc13 100644 --- a/tests/lua/threads/tactic1.lua +++ b/tests/lua/threads/tactic1.lua @@ -1,3 +1,4 @@ +import("util.lua") local env = environment() local ios = io_state() local Bool = Const("Bool") diff --git a/tests/lua/threads/tactic2.lua b/tests/lua/threads/tactic2.lua index 93b023018..6ed016ba5 100644 --- a/tests/lua/threads/tactic2.lua +++ b/tests/lua/threads/tactic2.lua @@ -1,3 +1,4 @@ +import("util.lua") local env = environment() local ios = io_state() local Bool = Const("Bool") diff --git a/tests/lua/unify1.lua b/tests/lua/unify1.lua index 63978af4d..1408a2fdb 100644 --- a/tests/lua/unify1.lua +++ b/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")