feat(extra): replace parse_lean_tpl with improved parse_template, that is based on macros

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

src/extra/parse_lean_tpl.lua

@@ -1,53 +0,0 @@
--- Parse a template expression string 'str'.
--- The string 'str' contains placeholders of the form 'a::i', where 'i' is a numeral.
--- The placeholders are replaced with values from the array 'args'.
--- See 'test' function for an example.
-function parse_lean_tpl(str, args, env, opts, fmt)
-   assert(type(str) == "string")
-   assert(type(args) == "table")
-   assert(env == nil or is_environment(env))
-   if #args == 0 then
-      return parse_lean(str, env, opts, fmt)
-   else
-      -- Create the string "fun (a::1 : type-of-args[1]) ... (a::n : type-of-args[n]), $str",
-      -- where n is the size of args
-      local tbl = {"fun"}
-      for i = 1, #args do
-         table.insert(tbl, " (a::")
-         table.insert(tbl, i)
-         table.insert(tbl, " : ")
-         table.insert(tbl, tostring(env:infer_type(args[i])))
-         table.insert(tbl, ")")
-      end
-      table.insert(tbl, ", ")
-      table.insert(tbl, str)
-      local new_str = table.concat(tbl)
-      local r = parse_lean(new_str, env, opts, fmt)
-      for i = 1, #args do
-         assert(r:is_lambda())
-         local n, d, body = r:fields()
-         r = body:instantiate(args[i])
-      end
-      return r
-   end
-end
-
-local test = function()
-   local env  = environment()
-   -- Load environment with some definitions
-   parse_lean_cmds([[
-        Variables a b : Real
-        Variable  f : Real -> Real
-        Variable  g : Real -> Real -> Real
-]], env)
-   local a, b, g = Consts("a, b, g")
-   local t1      = parse_lean_tpl("a::1 + (f a::2) - 10 + a::2", {a, g(b, a)}, env)
-   print(t1)
-   local t2      = parse_lean_tpl("f (a::1 + 1)", {g(b, b)}, env)
-   print(t2)
-end
-
-if not pcall(debug.getlocal, 4, 1) then
-   -- Main file
-   test()
-end

src/extra/template.lua

@@ -0,0 +1,31 @@
+-- Parse a template expression string 'str'.
+-- The string 'str' may contain placeholders of the form '% i', where 'i' is a numeral.
+-- The placeholders are replaced with values from the array 'arg_array'.
+local arg_array = {}
+
+-- We implement this feature using macros available in Lean.
+macro("%",
+      { macro_arg.Int },
+      function (env, i)
+         if i <= 0 then
+            error("invalid template argument reference %" .. i .. ", first argument is 1")
+         elseif i > #arg_array then
+            error("invalid template argument reference %" .. i .. ", only " .. tostring(#arg_array) .. " argument(s) were provided")
+         else
+            return arg_array[i]
+         end
+      end
+)
+
+-- Parse a template.
+-- Example:
+--    r = parse_template("%1 + %2 + %1", {Const("a"), Const("b")})
+--    print(r)
+--    >> a + b + a
+function parse_template(str, args, env, opts, fmt)
+   assert(type(str)  == "string")
+   assert(type(args) == "table")
+   assert(env == nil or is_environment(env))
+   arg_array = args
+   return parse_lean(str, env, opts, fmt)
+end

tests/lua/template1.lua

@@ -0,0 +1,16 @@
+import("template.lua")
+local env = environment()
+parse_lean_cmds([[
+   Variables a b c : Int
+   Variables f : Int -> Int
+]], env)
+local a, b, c = Consts("a, b, c")
+print(parse_template("%1 + f %2 + %1 + %1", {a, b}, env))
+assert(tostring(parse_template("%1 + f %2 + %1 + %1", {a, b}, env)) == "Int::add (Int::add (Int::add a (f b)) a) a")
+assert(not pcall(function() print(parse_template("%1 + f %2 + %1 + %1", {a}, env)) end))
+print(parse_template("%1 + f %2 + %3 + f (f %1)", {a, b, c}, env))
+print(parse_template("%1 + f %2 + 10 + f (f %1)", {a, b, c}, env))
+assert(tostring(parse_template("%1 + f %2 + 10 + f (f %1)", {a, b, c}, env)) == "Int::add (Int::add (Int::add a (f b)) (nat_to_int 10)) (f (f a))")
+set_formatter(lean_formatter(env))
+print(parse_template("%1 + f %2 + %3 + f (f %1)", {a, b, c}, env))
+assert(tostring(parse_template("%1 + f %2 + %3 + f (f %1)", {a, b, c}, env)) == "a + f b + c + f (f a)")