From 49f580f190cea71b603756bcd6adcb111ba4f552 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 12 Jan 2019 14:14:52 +0100
Subject: [PATCH] feat(library/compiler/builtin,frontends/lean/vm_elaborator):
 add temporary `expr.local` primitive

This makes it possible (or at least much easier) to interface with old
parser/elaborator code using local_consts for e.g. `def` parameters.
---
 library/init/lean/elaborator.lean    | 3 +++
 src/frontends/lean/vm_elaborator.cpp | 7 ++++++-
 src/library/compiler/builtin.cpp     | 7 ++++---
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 79524dd2a5..7277fdf4c7 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -17,6 +17,9 @@ constant environment : Type
 constant environment.empty : environment
 constant environment.contains : environment → name → bool
 
+-- deprecated constructor
+constant expr.local : name → name → expr → binder_info → expr
+
 namespace elaborator
 -- TODO(Sebastian): move
 -- TODO(Sebastian): should be its own monad?
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index de16b51d41..7f96c75b98 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -297,7 +297,7 @@ expr to_expr(vm_obj const & o) {
         case 0:
             return mk_bvar(nat(vm_nat_to_mpz1(cfield(o, 0))));
         case 1:
-            return mk_local(to_name(cfield(o, 0)), to_name(cfield(o, 0)), expr(), mk_binder_info());
+            return mk_local(to_name(cfield(o, 0)), to_name(cfield(o, 1)), to_expr(cfield(o, 2)), to_binder_info(cfield(o, 3)));
         case 2:
             return mk_metavar(to_name(cfield(o, 0)), to_expr(cfield(o, 1)));
         case 3:
@@ -465,7 +465,12 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
     return mk_vm_constructor(0, vm_out, to_obj(log));
 }
 
+vm_obj vm_expr_local(vm_obj const & vm_pp_name, vm_obj const & vm_name, vm_obj const & vm_type, vm_obj const & vm_binder_info) {
+    return mk_vm_constructor(1, vm_pp_name, vm_name, vm_type, vm_binder_info);
+}
+
 void initialize_vm_elaborator() {
+    DECLARE_VM_BUILTIN(name({"lean", "expr", "local"}), vm_expr_local);
     DECLARE_VM_BUILTIN(name({"lean", "environment", "empty"}), vm_environment_empty);
     DECLARE_VM_BUILTIN(name({"lean", "environment", "contains"}), vm_environment_contains);
     DECLARE_VM_BUILTIN(name({"lean", "elaborator", "elaborate_command"}), vm_elaborate_command);
diff --git a/src/library/compiler/builtin.cpp b/src/library/compiler/builtin.cpp
index d79e13bba0..f0a4f6a5e5 100644
--- a/src/library/compiler/builtin.cpp
+++ b/src/library/compiler/builtin.cpp
@@ -162,9 +162,10 @@ void initialize_builtin() {
     register_builtin(name({"io", "prim", "handle", "get_line"}), o_o_o, "io_prim_handle_get_line", bc);
 
     // interface to old elaborator
-    register_builtin(name({"lean", "environment", "empty"}), o, "lean_environment_empty", {});
-    register_builtin(name({"lean", "environment", "contains"}), o_o_o, "lean_environment_contains", bb);
-    register_builtin(name({"lean", "elaborator", "elaborate_command"}), o_o_o_o, "lean_elaborator_elaborate_command", bbb);
+    register_builtin(name({"lean", "expr", "local"}), mk_arrow(o, o_o_o_o), "lean_expr_local");
+    register_builtin(name({"lean", "environment", "empty"}), o, "lean_environment_empty");
+    register_builtin(name({"lean", "environment", "contains"}), o_o_o, "lean_environment_contains");
+    register_builtin(name({"lean", "elaborator", "elaborate_command"}), o_o_o_o, "lean_elaborator_elaborate_command");
 }
 
 void finalize_builtin() {