Reimplement #eval

library/init/data/repr.lean

@@ -129,7 +129,7 @@ instance : HasRepr Substring :=
 ⟨fun s => String.quote s.toString ++ ".toSubstring"⟩
 
 instance : HasRepr String.Iterator :=
-⟨fun it => it.remainingToString.quote ++ ".mkIterator"⟩
+⟨fun ⟨s, pos⟩ => "(String.Iterator.mk " ++ repr s ++ " " ++ repr pos ++ ")"⟩
 
 instance (n : Nat) : HasRepr (Fin n) :=
 ⟨fun f => repr (Fin.val f)⟩

library/init/data/string/basic.lean

@@ -257,17 +257,6 @@ def prevn : Iterator → Nat → Iterator
 | it, i+1 => prevn it.prev i
 end Iterator
 
-private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat
-| i, r@(line, col) =>
-  if atEnd s i then r
-  else
-    let c := s.get i;
-    if c = '\n' then lineColumnAux (s.next i) (line+1, 0)
-    else lineColumnAux (s.next i) (line, col+1)
-
-def lineColumn (s : String) (pos : Pos) : Nat × Nat :=
-lineColumnAux s 0 (1, 0)
-
 partial def offsetOfPosAux (s : String) (pos : Pos) : Pos → Nat → Nat
 | i, offset =>
   if i == pos || s.atEnd i then offset

src/frontends/lean/builtin_cmds.cpp

@@ -40,6 +40,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/typed_expr.h"
+#include "library/compiler/ir_interpreter.h"
 
 namespace lean {
 environment section_cmd(parser & p) {
@@ -315,6 +316,62 @@ environment hide_cmd(parser & p) {
     return new_env;
 }
 
+static environment eval_cmd(parser & p) {
+    transient_cmd_scope cmd_scope(p);
+    auto pos = p.pos();
+    expr e; names ls;
+    std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false);
+    if (has_synthetic_sorry(e))
+        return p.env();
+
+    type_context_old tc(p.env(), transparency_mode::All);
+    auto type = tc.infer(e);
+
+    bool has_eval = false;
+
+    /* Check if resultant type has an instance of has_eval */
+    try {
+        expr has_eval_type = mk_app(tc, "HasEval", type);
+        optional<expr> eval_instance = tc.mk_class_instance(has_eval_type);
+        if (eval_instance) {
+            /* Modify the 'program' to (has_eval.eval e) */
+            e             = mk_app(tc, {"HasEval", "eval"}, 3, type, *eval_instance, e);
+            type          = tc.infer(e);
+            has_eval      = true;
+        }
+    } catch (exception &) {}
+
+    if (!has_eval) {
+        // NOTE: HasRepr implies HasEval
+        throw exception("result type does not have an instance of type class 'HasRepr' or 'HasEval'");
+    }
+
+    name fn_name = "_main";
+    auto new_env = compile_expr(p.env(), p.get_options(), fn_name, ls, type, e, pos);
+
+    auto out = p.mk_message(p.cmd_pos(), p.pos(), INFORMATION);
+    out.set_caption("eval result");
+    scope_traces_as_messages scope_traces(p.get_stream_name(), p.cmd_pos());
+    std::streambuf * saved_cout = std::cout.rdbuf(out.get_text_stream().get_stream().rdbuf());
+
+    // run `IO Unit`
+    object * args[] = { io_mk_world() };
+
+    if (p.profiling()) {
+        timeit timer(out.get_text_stream().get_stream(), "eval time");
+        // NOTE: no need to free `()`
+        ir::run_boxed(new_env, fn_name, &args[0]);
+    } else {
+        ir::run_boxed(new_env, fn_name, &args[0]);
+    }
+
+    std::cout.rdbuf(saved_cout);
+    out.report();
+    return p.env();
+}
+
+
+
 environment compact_tst_cmd(parser & p) {
     environment env = p.env();
     unsigned num_copies = 0;
@@ -410,6 +467,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("init_quot",         "initialize `quot` type computational rules", init_quot_cmd));
     add_cmd(r, cmd_info("import",            "import module(s)", import_cmd));
     add_cmd(r, cmd_info("hide",              "hide aliases in the current scope", hide_cmd));
+    add_cmd(r, cmd_info("#eval",             "evaluate given expression using interpreter/precompiled code", eval_cmd));
     register_decl_cmds(r);
     register_inductive_cmds(r);
     register_structure_cmd(r);

src/library/compiler/ir_interpreter.cpp

@@ -195,27 +195,33 @@ union value {
     value(object * o): m_obj(o) {}
 };
 
-object * box_t(uint64 v, type t) {
+object * box_t(value v, type t) {
     switch (t) {
         case type::Float: throw exception("floats are not supported yet");
-        case type::UInt8: return box(v);
-        case type::UInt16: return box(v);
-        case type::UInt32: return box_uint32(v);
-        case type::UInt64: return box_uint64(v);
-        case type::USize: return box_size_t(v);
-        default: lean_unreachable();
+        case type::UInt8: return box(v.m_num);
+        case type::UInt16: return box(v.m_num);
+        case type::UInt32: return box_uint32(v.m_num);
+        case type::UInt64: return box_uint64(v.m_num);
+        case type::USize: return box_size_t(v.m_num);
+        case type::Object:
+        case type::TObject:
+        case type::Irrelevant:
+            return v.m_obj;
     }
 }
 
-uint64 unbox_t(object * o, type t) {
+value unbox_t(object * o, type t) {
     switch (t) {
         case type::Float: throw exception("floats are not supported yet");
         case type::UInt8: return unbox(o);
         case type::UInt16: return unbox(o);
         case type::UInt32: return unbox_uint32(o);
         case type::UInt64: return unbox_uint64(o);
         case type::USize: return unbox_size_t(o);
-        default: lean_unreachable();
+        case type::Object:
+        case type::TObject:
+        case type::Irrelevant:
+            return o;
     }
 }
 
@@ -704,48 +710,19 @@ class interpreter {
         if (e.m_addr) {
             object ** args2 = static_cast<object **>(LEAN_ALLOCA(args.size() * sizeof(object *))); // NOLINT
             for (size_t i = 0; i < args.size(); i++) {
-                value v = eval_arg(args[i]);
                 type t = param_type(decl_params(e.m_decl)[i]);
-                switch (t) {
-                    case type::Float:
-                    case type::UInt8:
-                    case type::UInt16:
-                    case type::UInt32:
-                    case type::UInt64:
-                    case type::USize:
-                        args2[i] = box_t(v.m_num, t);
-                        break;
-                    case type::Object:
-                    case type::TObject:
-                    case type::Irrelevant:
-                        args2[i] = v.m_obj;
-                        if (e.m_boxed && param_borrow(decl_params(e.m_decl)[i])) {
-                            // NOTE: If we chose the boxed version where the IR chose the unboxed one, we need to manually increment
-                            // originally borrowed parameters because the wrapper will decrement these after the call.
-                            // Basically the wrapper is more homogeneous (removing both unboxed and borrowed parameters) than we
-                            // would need in this instance.
-                            inc(args2[i]);
-                        }
-                        break;
+                args2[i] = box_t(eval_arg(args[i]), t);
+                if (e.m_boxed && param_borrow(decl_params(e.m_decl)[i])) {
+                    // NOTE: If we chose the boxed version where the IR chose the unboxed one, we need to manually increment
+                    // originally borrowed parameters because the wrapper will decrement these after the call.
+                    // Basically the wrapper is more homogeneous (removing both unboxed and borrowed parameters) than we
+                    // would need in this instance.
+                    inc(args2[i]);
                 }
             }
             push_frame(e.m_decl, old_size);
             object * o = curry(e.m_addr, args.size(), args2);
-            switch (decl_type(e.m_decl)) {
-                case type::Float:
-                case type::UInt8:
-                case type::UInt16:
-                case type::UInt32:
-                case type::UInt64:
-                case type::USize:
-                    r = unbox_t(o, decl_type(e.m_decl));
-                    break;
-                case type::Object:
-                case type::TObject:
-                    r = o;
-                    break;
-                default: lean_unreachable();
-            }
+            r = unbox_t(o, decl_type(e.m_decl));
         } else {
             if (decl_tag(e.m_decl) == decl_kind::Extern) {
                 throw exception(sstream() << "unexpected external declaration '" << fn << "'");
@@ -760,55 +737,6 @@ class interpreter {
         pop_frame(r, decl_type(e.m_decl));
         return r;
     }
-public:
-    explicit interpreter(environment const & env) : m_env(env) {
-        lean_assert(g_interpreter == nullptr);
-        g_interpreter = this;
-    }
-    ~interpreter() {
-        for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) {
-            if (!e.m_is_scalar) {
-                dec(e.m_val.m_obj);
-            }
-        });
-        lean_assert(g_interpreter == this);
-        g_interpreter = nullptr;
-    }
-
-    uint32 run_main(int argc, char * argv[]) {
-        decl d = get_fdecl("main");
-        array_ref<param> const & params = decl_params(d);
-        if (params.size() == 2) { // List String -> IO UInt32
-            lean_object * in = lean_box(0);
-            int i = argc;
-            while (i > 0) {
-                i--;
-                lean_object * n = lean_alloc_ctor(1, 2, 0);
-                lean_ctor_set(n, 0, lean_mk_string(argv[i]));
-                lean_ctor_set(n, 1, in);
-                in = n;
-            }
-            m_arg_stack.push_back(in);
-        } else { // IO UInt32
-            lean_assert(params.size() == 1);
-        }
-        object * w = io_mk_world();
-        m_arg_stack.push_back(w);
-        push_frame(d, 0);
-        w = eval_body(decl_fun_body(d)).m_obj;
-        pop_frame(w, type::Object);
-        if (io_result_is_ok(w)) {
-            // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same
-            // representation
-            int ret = unbox(io_result_get_value(w));
-            dec_ref(w);
-            return ret;
-        } else {
-            io_result_show_error(w);
-            dec_ref(w);
-            return 1;
-        }
-    }
 
     // closure stub
     object * stub_m(object ** args) {
@@ -875,8 +803,94 @@ class interpreter {
             default: return reinterpret_cast<void *>(stub_m_aux);
         }
     }
+public:
+    explicit interpreter(environment const & env) : m_env(env) {
+        lean_assert(g_interpreter == nullptr);
+        g_interpreter = this;
+    }
+    ~interpreter() {
+        for_each(m_constant_cache, [](name const &, constant_cache_entry const & e) {
+            if (!e.m_is_scalar) {
+                dec(e.m_val.m_obj);
+            }
+        });
+        lean_assert(g_interpreter == this);
+        g_interpreter = nullptr;
+    }
+
+    object * call_boxed(name const & fn, object ** args) {
+        symbol_cache_entry e = lookup_symbol(fn);
+        unsigned n = decl_params(e.m_decl).size();
+        object * r;
+        if (e.m_addr) {
+            push_frame(e.m_decl, 0);
+            // directly call boxed function, nothing more to do
+            r = curry(e.m_addr, n, args);
+        } else {
+            // equivalent code to boxed stubs generated by the compiler: unbox args, box result, decrement borrowed args
+
+            if (decl_tag(e.m_decl) == decl_kind::Extern) {
+                throw exception(sstream() << "unexpected external declaration '" << fn << "'");
+            }
+            // evaluate args in old stack frame
+            for (unsigned i = 0; i < n; i++) {
+                type t = param_type(decl_params(e.m_decl)[i]);
+                m_arg_stack.push_back(unbox_t(args[i], t));
+                if (type_is_scalar(t)) {
+                    dec(args[i]);
+                }
+            }
+            push_frame(e.m_decl, 0);
+            r = box_t(eval_body(decl_fun_body(e.m_decl)), decl_type(e.m_decl));
+            for (size_t i = 0; i < n; i++) {
+                if (param_borrow(decl_params(e.m_decl)[i])) {
+                    dec(args[i]);
+                }
+            }
+        }
+        pop_frame(r, decl_type(e.m_decl));
+        return r;
+    }
+
+    uint32 run_main(int argc, char * argv[]) {
+        decl d = get_fdecl("main");
+        array_ref<param> const & params = decl_params(d);
+        if (params.size() == 2) { // List String -> IO UInt32
+            lean_object * in = lean_box(0);
+            int i = argc;
+            while (i > 0) {
+                i--;
+                lean_object * n = lean_alloc_ctor(1, 2, 0);
+                lean_ctor_set(n, 0, lean_mk_string(argv[i]));
+                lean_ctor_set(n, 1, in);
+                in = n;
+            }
+            m_arg_stack.push_back(in);
+        } else { // IO UInt32
+            lean_assert(params.size() == 1);
+        }
+        object * w = io_mk_world();
+        m_arg_stack.push_back(w);
+        push_frame(d, 0);
+        w = eval_body(decl_fun_body(d)).m_obj;
+        pop_frame(w, type::Object);
+        if (io_result_is_ok(w)) {
+            // NOTE: in an awesome hack, `IO Unit` works just as well because `pure 0` and `pure ()` use the same
+            // representation
+            int ret = unbox(io_result_get_value(w));
+            dec_ref(w);
+            return ret;
+        } else {
+            io_result_show_error(w);
+            dec_ref(w);
+            return 1;
+        }
+    }
 };
 
+object * run_boxed(environment const & env, name const & fn, object ** args) {
+    return interpreter(env).call_boxed(fn, args);
+}
 uint32 run_main(environment const & env, int argv, char * argc[]) {
     return interpreter(env).run_main(argv, argc);
 }

src/library/compiler/ir_interpreter.h

@@ -10,6 +10,8 @@ Author: Sebastian Ullrich
 
 namespace lean {
 namespace ir {
+/** \brief Run `n` using the "boxed" ABI, i.e. with all-owned parameters. */
+object * run_boxed(environment const & env, name const & fn, object ** args);
 uint32 run_main(environment const & env, int argv, char * argc[]);
 }
 void initialize_ir_interpreter();