feat(library/init/lean/elaborator): elaborate constants

library/init/lean/elaborator.lean

@@ -293,6 +293,47 @@ def to_pexpr : syntax → elaborator_m expr
   | _ := error stx $ "unexpected node: " ++ to_string k.name)
 | stx := error stx $ "unexpected: " ++ to_string stx
 
+def old_elab_command (stx : syntax) (cmd : expr) : elaborator_m unit :=
+do cfg ← read,
+   st ← get,
+   match elaborate_command cfg.filename cmd {
+     univs := st.local_state.univs.entries,
+     vars := st.local_state.vars.entries,
+     include_vars := st.local_state.include_vars.to_list,
+     ..st} with
+   | except.ok st' := put {
+     local_state := {st.local_state with
+       univs := ordered_rbmap.of_list st'.univs,
+       vars := ordered_rbmap.of_list st'.vars,
+       include_vars := rbtree.of_list st'.include_vars,
+     },
+     ..st', ..st}
+   | except.error e := error stx e
+
+def attrs_to_pexpr (attrs : list (sep_by.elem.view attr_instance.view (option syntax_atom))) : elaborator_m expr :=
+expr.mk_capp `_ <$> attrs.mmap (λ attr,
+  expr.mk_capp (mangle_ident attr.item.name) <$> attr.item.args.mmap to_pexpr)
+
+def decl_modifiers_to_pexpr (mods : decl_modifiers.view) : elaborator_m expr := do
+  let mdata : kvmap := {},
+  let mdata := match mods.doc_comment with
+    | some {doc := some doc, ..} := mdata.set_string `doc_string doc.val
+    | _ := mdata,
+  let mdata := match mods.visibility with
+    | some (visibility.view.private _) := mdata.set_bool `private tt
+    | some (visibility.view.protected _) := mdata.set_bool `protected tt
+    | _ := mdata,
+  let mdata := mdata.set_bool `noncomputable mods.noncomputable.is_some,
+  let mdata := mdata.set_bool `meta mods.meta.is_some,
+  expr.mdata mdata <$> attrs_to_pexpr (match mods.attrs with
+    | some attrs := attrs.attrs
+    | none       := [])
+
+def ident_univ_params_to_pexpr (id : ident_univ_params.view) : expr :=
+expr.const (mangle_ident id.id) $ match id.univ_params with
+  | some params := params.params.map (level.param ∘ mangle_ident)
+  | none        := []
+
 /-- Execute `elab` and reset local state (universes, ...) after it has finished. -/
 @[specialize] def locally {m : Type → Type} [monad m] [monad_state elaborator_state m] (elab : m unit) :
   m unit := do
@@ -303,8 +344,16 @@ def to_pexpr : syntax → elaborator_m expr
 def declaration.elaborate : elaborator :=
 locally $ λ stx, do
   let decl := view «declaration» stx,
-  -- just test `to_pexpr` for now
   match decl.inner with
+  | declaration.inner.view.constant c@{sig := {params := bracketed_binders.view.simple [], type := type}, ..} := do
+    let mdata := kvmap.set_name {} `command `constant,
+    mods ← decl_modifiers_to_pexpr decl.modifiers,
+    let id := ident_univ_params_to_pexpr c.name,
+    type ← to_pexpr type.type,
+    old_elab_command stx $ expr.mdata mdata $ expr.mk_capp `_ [mods, id, type]
+  | declaration.inner.view.constant _ :=
+    error stx "declration.elaborate: unexpected input"
+  -- just test `to_pexpr` for now
   | declaration.inner.view.def_like dl@{
     val := decl_val.view.simple val,
     sig := {params := bracketed_binders.view.simple bbs}, ..} := do
@@ -508,30 +557,12 @@ def universe.elaborate : elaborator :=
   | none   := put {st with local_state := {st.local_state with univs := st.local_state.univs.insert id (level.param id)}}
   | some _ := error stx $ "a universe named '" ++ to_string id ++ "' has already been declared in this scope"
 
-def old_elab_command (stx : syntax) (cmd : expr) : elaborator_m unit :=
-do cfg ← read,
-   st ← get,
-   match elaborate_command cfg.filename cmd {
-     univs := st.local_state.univs.entries,
-     vars := st.local_state.vars.entries,
-     include_vars := st.local_state.include_vars.to_list,
-     ..st} with
-   | except.ok st' := put {
-     local_state := {st.local_state with
-       univs := ordered_rbmap.of_list st'.univs,
-       vars := ordered_rbmap.of_list st'.vars,
-       include_vars := rbtree.of_list st'.include_vars,
-     },
-     ..st', ..st}
-   | except.error e := error stx e
-
 def attribute.elaborate : elaborator :=
 λ stx, do
   let attr := view «attribute» stx,
   let mdata := kvmap.set_name {} `command `attribute,
   let mdata := mdata.set_bool `local $ attr.local.is_some,
-  attrs ← expr.mk_capp `_ <$> attr.attrs.mmap (λ attr,
-    expr.mk_capp (mangle_ident attr.item.name) <$> attr.item.args.mmap to_pexpr),
+  attrs ← attrs_to_pexpr attr.attrs,
   let ids := expr.mk_capp `_ $ attr.ids.map $ λ id, expr.const (mangle_ident id) [],
   old_elab_command stx $ expr.mdata mdata $ expr.app attrs ids
 

src/frontends/lean/vm_elaborator.cpp

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Sebastian Ullrich
 
-TEMPORARY code for the old runtime
+Lean interface to the old elaborator/elaboration parts of the parser
 */
 
 #include <string>
@@ -17,35 +17,72 @@ TEMPORARY code for the old runtime
 #include "library/vm/vm_nat.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/parser.h"
+#include "frontends/lean/decl_cmds.h"
 
 namespace lean {
+decl_attributes to_decl_attributes(environment const & env, expr const & e, bool local) {
+    decl_attributes attributes(!local);
+    buffer<expr> args;
+    get_app_args(e, args);
+    for (auto const & e : args)
+        attributes.set_attribute(env, const_name(e));
+    return attributes;
+}
+
 environment elab_attribute_cmd(environment env, expr const & cmd) {
     auto const & data = mdata_data(cmd);
     bool local = *get_bool(data, "local");
-    decl_attributes attributes(!local);
     buffer<expr> args, eattrs, eids;
     get_app_args(mdata_expr(cmd), args);
-    get_app_args(args[0], eattrs);
+    auto attributes = to_decl_attributes(env, args[0], local);
     get_app_args(args[1], eids);
-    for (auto const & e : eattrs)
-        attributes.set_attribute(env, const_name(e));
     for (auto const & e : eids)
         env = attributes.apply(env, get_dummy_ios(), const_name(e));
     return env;
 }
 
+cmd_meta to_cmd_meta(environment const & env, expr const & e) {
+    auto const & data = mdata_data(e);
+    cmd_meta m(to_decl_attributes(env, mdata_expr(e), false));
+    m.m_modifiers.m_is_meta = get_bool(data, "meta").value_or(false);
+    m.m_modifiers.m_is_mutual = get_bool(data, "mutual").value_or(false);
+    m.m_modifiers.m_is_noncomputable = get_bool(data, "noncomputable").value_or(false);
+    m.m_modifiers.m_is_private = get_bool(data, "private").value_or(false);
+    m.m_modifiers.m_is_protected = get_bool(data, "protected").value_or(false);
+    if (auto s = get_string(data, "doc_string"))
+        m.m_doc_string = s->to_std_string();
+    return m;
+}
+
+void elab_constant_cmd(parser & p, expr const & cmd) {
+    buffer<expr> args, ls;
+    get_app_args(mdata_expr(cmd), args);
+    auto fn = get_app_args(args[1], ls);
+    buffer<name> ls_buffer;
+    for (auto const & e : ls)
+        ls_buffer.push_back(const_name(e));
+    p.set_env(elab_var(p, variable_kind::Constant, to_cmd_meta(p.env(), args[0]), get_pos_info_provider()->get_pos_info_or_some(cmd),
+                       optional<binder_info>(), const_name(fn), args[2], ls_buffer));
+}
+
 void elaborate_command(parser & p, expr const & cmd) {
     auto const & data = mdata_data(cmd);
     if (auto const & cmd_name = get_name(data, "command")) {
         if (*cmd_name == "attribute") {
             p.set_env(elab_attribute_cmd(p.env(), cmd));
             return;
+        } else if (*cmd_name == "constant") {
+            elab_constant_cmd(p, cmd);
+            return;
         }
     }
     throw elaborator_exception(cmd, "unexpected input to 'elaborate_command'");
 }
 
 
+/* TEMPORARY code for the old runtime */
+
+
 struct vm_env : public vm_external {
     environment m_env;
 
@@ -165,11 +202,11 @@ expr to_expr(vm_obj const & o) {
         case 5:
             return mk_app(to_expr(cfield(o, 0)), to_expr(cfield(o, 1)));
         case 6:
-            return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)),
-                             to_binder_info(cfield(o, 3)));
+            return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)),
+                             to_binder_info(cfield(o, 1)));
         case 7:
-            return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)),
-                         to_binder_info(cfield(o, 3)));
+            return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)),
+                         to_binder_info(cfield(o, 1)));
         case 8:
             return mk_let(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)));
         case 9: {
@@ -239,8 +276,9 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
     lean_vm_check(dynamic_cast<vm_env *>(to_external(vm_e)));
     auto env = static_cast<vm_env *>(to_external(vm_e))->m_env;
     io_state const & ios = get_dummy_ios();
+    auto filename = to_string(vm_filename);
     std::stringstream in;
-    parser p(env, ios, in, to_string(vm_filename));
+    parser p(env, ios, in, filename);
     auto s = p.mk_snapshot();
     auto ngen = to_name_generator(cfield(vm_st, 1));
     auto vm_lds = cfield(vm_st, 2);
@@ -270,8 +308,9 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
     p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
             parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info {1, 0}));
 
+    auto cmd = to_expr(vm_cmd);
     try {
-        elaborate_command(p, to_expr(vm_cmd));
+        elaborate_command(p, cmd);
         s = p.mk_snapshot();
         auto vm_st2 = mk_vm_constructor(0, {
             mk_vm_external(new vm_env(env)),
@@ -285,7 +324,10 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
         });
         return mk_vm_constructor(1, vm_st);
     } catch (exception & e) {
-        return mk_vm_constructor(0, to_obj(std::string(e.what())));
+        message_builder builder(env, ios, filename, get_pos_info_provider()->get_pos_info_or_some(cmd),
+                message_severity::ERROR);
+        builder.set_exception(e);
+        return mk_vm_constructor(0, to_obj(builder.build().get_text()));
     }
 }
 

src/runtime/optional.h

@@ -55,6 +55,10 @@ public:
     T const & value() const { lean_assert(m_some); return m_value; }
     T & value() { lean_assert(m_some); return m_value; }
 
+    T const & value_or(T const & default_value) const {
+        return m_some ? m_value : default_value;
+    }
+
     template<typename... Args>
     void emplace(Args&&... args) {
         if (m_some)