feat(tactic/type_context_old): Expose type_context_old as a monad. (#69)

The idea is to investigate exposing some of the constructs which Lean
uses to make type_context_old to enable the user to create
more powerful tactics.

Some examples can be seen in the `tests/lean/tco.lean`:
There is a reimplementation of `intro` and `match_pattern` using the new monad.

library/init/meta/attribute.lean

@@ -28,7 +28,7 @@ tactic.exact `(⟨λ _, pure (), []⟩ : user_attribute_cache_cfg unit)
 meta def user_attribute.dflt_parser : tactic unit :=
 tactic.exact `(pure () : lean.parser unit)
 
-/-- 
+/--
 A __user attribute__ is an attribute defined by the user (ie, not built in to Lean).
 ### Type parameters
 - `cache_ty` is the type of a cached VM object that is computed from all of the declarations in the environment tagged with this attribute.
@@ -45,8 +45,8 @@ A `user_attribute` consists of the following pieces of data:
     non-removable.
 - `before_unset` Optional handler that will be called before the attribute is removed from a declaration.
 - `cache_cfg` describes how to construct the user attribute's cache. See docstring for `user_attribute_cache_cfg`
-- `reflect_param` demands that `param_ty` can be reflected. 
-    This means we have a function from `param_ty` to an expr. 
+- `reflect_param` demands that `param_ty` can be reflected.
+    This means we have a function from `param_ty` to an expr.
     See the docstring for `has_reflect`.
 - `parser` Parser that will be invoked after parsing the attribute's name. The parse result will be reflected
 and stored and can be retrieved with `user_attribute.get_param`.

library/init/meta/default.lean

@@ -16,3 +16,4 @@ import init.meta.interactive init.meta.converter init.meta.vm
 import init.meta.comp_value_tactics init.meta.smt
 import init.meta.async_tactic init.meta.ref
 import init.meta.hole_command init.meta.congr_tactic
+import init.meta.local_context init.meta.type_context

library/init/meta/expr.lean

@@ -179,6 +179,8 @@ meta def expr.abstract : expr → expr → expr
 /-- Expressions depend on `level`s, and these may depend on universe parameters which have names.
 `instantiate_univ_params e [(n₁,l₁), ...]` will traverse `e` and replace any universe parameters with name `nᵢ` with the corresponding level `lᵢ`.  -/
 meta constant expr.instantiate_univ_params : expr → list (name × level) → expr
+/-- `instantiate_nth_var n a b` takes the `n`th de-Bruijn variable in `a` and replaces each occurrence with `b`. -/
+meta constant expr.instantiate_nth_var : nat → expr → expr → expr
 /-- `instantiate_var a b` takes the 0th de-Bruijn variable in `a` and replaces each occurrence with `b`. -/
 meta constant expr.instantiate_var         : expr → expr → expr
 /-- ``instantiate_vars `(#0 #1 #2) [x,y,z] = `(%%x %%y %%z)`` -/
@@ -187,6 +189,8 @@ meta constant expr.instantiate_vars        : expr → list expr → expr
 /-- Perform beta-reduction if the left expression is a lambda. Ie: ``expr.subst | `(λ x, %%Y) Z := Y[x/Z] | X Z := X``-/
 protected meta constant expr.subst : expr elab → expr elab → expr elab
 
+/-- `get_free_var_range e` returns one plus the maximum de-Bruijn value in `e`. Eg `get_free_var_range `(#1 #0)` yields `2` -/
+meta constant expr.get_free_var_range : expr → nat
 /-- `has_var e` returns true iff e has free variables. -/
 meta constant expr.has_var       : expr → bool
 /-- `has_var_idx e n` returns true iff `e` has a free variable with de-Bruijn index `n`. -/
@@ -226,6 +230,11 @@ meta constant expr.occurs        : expr → expr → bool
 /-- Returns true if any of the names in the given `name_set` are present in the given `expr`. -/
 meta constant expr.has_local_in : expr → name_set → bool
 
+/-- `mk_delayed_abstraction m ls` creates a delayed abstraction on the metavariable `m` with the unique names of the local constants `ls`.
+    If `m` is not a metavariable then this is equivalent to `abstract_locals`.
+ -/
+meta constant expr.mk_delayed_abstraction : expr → list name → expr
+
 /-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
     It can only be obtained via type class inference, which will use the representation
     of `a` in the calling context. Local constants in the representation are replaced

library/init/meta/local_context.lean

@@ -0,0 +1,25 @@
+prelude
+import init.meta.name init.meta.expr
+meta structure local_decl :=
+(unique_name : name)
+(pp_name : name)
+(type : expr)
+(value : option expr)
+(bi : binder_info)
+(idx : nat)
+
+/-- A local context is a list of local constant declarations.
+    Each metavariable in a metavariable context holds a local_context
+    to declare which locals the metavariable is allowed to depend on. -/
+meta constant local_context : Type
+namespace local_context
+/-- Add a new local constant to the lc. The new local has an unused unique_name. Fails when the type depends on local constants that are not present in the context.-/
+meta constant mk_local (pretty_name : name) (type : expr) (bi : binder_info) : local_context → option (expr × local_context)
+meta constant get_local_decl : name → local_context → option local_decl
+meta constant get_local : name → local_context → option expr
+meta constant is_subset : local_context → local_context → bool
+meta constant fold {α : Type} (f : α → expr → α): α → local_context → α
+meta def to_list : local_context → list expr := list.reverse ∘ fold (λ acc e, e :: acc) []
+meta def to_format : local_context → format := to_fmt ∘ to_list
+meta instance lc_has_to_format : has_to_format local_context := ⟨to_format⟩
+end local_context

library/init/meta/type_context.lean

@@ -0,0 +1,113 @@
+prelude
+import init.category init.meta.local_context init.meta.tactic init.meta.fun_info
+namespace tactic.unsafe
+/-- A monad that exposes the functionality of the C++ class `type_context`.
+    The idea is that the methods in `tco` are more powerful but _unsafe_ in the
+    sense that you can create terms that do not typecheck or that are infinitely descending.
+    Under the hood, `tco` is implemented as a reader monad, with a mutable `type_context` object.
+     -/
+meta constant type_context : Type → Type
+namespace type_context
+variables {α β : Type}
+protected meta constant bind : type_context α → (α → type_context β) → type_context β
+protected meta constant pure : α → type_context α
+protected meta constant fail : format → type_context α
+protected meta def failure : type_context α := type_context.fail ""
+meta instance : monad type_context := {bind := @type_context.bind, pure := @type_context.pure}
+meta instance : monad_fail type_context := {fail := λ α, type_context.fail ∘ to_fmt}
+meta constant get_env : type_context environment
+meta constant whnf : expr → type_context expr
+meta constant is_def_eq (e₁ e₂ : expr) (approx := ff) : type_context bool
+meta constant unify (e₁ e₂ : expr) (approx := ff) : type_context bool
+/-- Infer the type of the given expr. Inferring the type does not mean that it typechecks.
+    Will fail if type can't be inferred. -/
+meta constant infer : expr → type_context expr
+/-- A stuck expression `e` is an expression that _would_ reduce,
+except that a metavariable is present that prevents the reduction.
+Returns the metavariable which is causing the stuckage.
+For example, `@has_add.add nat ?m a b` can't project because `?m` is not given. -/
+meta constant is_stuck : expr → type_context (option expr)
+/-- Add a local to the tc local context. -/
+meta constant push_local (pp_name : name) (type : expr) (bi := binder_info.default) : type_context expr
+meta constant pop_local : type_context unit
+/-- Get the local context of the type_context. -/
+meta constant get_local_context : type_context local_context
+/-- Create and declare a new metavariable. If the local context is not given then it will use the current local context. -/
+meta constant mk_mvar (pp_name : name) (type : expr) (context : option local_context := none) : type_context expr
+/-- Iterate over all mvars in the mvar context. -/
+meta constant fold_mvars {α : Type} (f : α → expr → type_context α) : α → type_context α
+meta def list_mvars : type_context (list expr) := fold_mvars (λ l x, pure $ x :: l) []
+/-- Set the mvar to the following assignments.
+    Works for temporary metas too.
+    [WARNING] `assign` does not perform certain checks:
+     - No typecheck is done before assignment.
+     - If the metavariable is already assigned this will clobber the assignment.
+     - It will not stop you from assigning an metavariable to itself or creating cycles of metavariable assignments.
+       These will manifest as 'deep recursion' exceptions when `instantiate_mvars` is used.
+     - It is not checked whether the assignment uses local constants outside the declaration's context.
+    You can avoid the unsafety by using `unify` instead.
+-/
+meta constant assign (mvar : expr) (assignment : expr) : type_context unit
+meta constant level.assign (mvar : level) (assignment : level) : type_context unit
+/-- Returns true if the given expression is a declared local constant or a declared metavariable. -/
+meta constant is_declared (e : expr) : type_context bool
+meta constant is_assigned (mvar : expr) : type_context bool
+meta constant get_context (mvar : expr) : type_context local_context
+/-- Get the expression that is assigned to the given mvar expression. Fails if given a -/
+meta constant get_assignment (mvar : expr) : type_context expr
+
+meta constant instantiate_mvars : expr → type_context expr
+meta constant level.instantiate_mvars : level → type_context level
+
+meta constant is_tmp_mvar (mvar : expr) : type_context bool
+meta constant is_regular_mvar (mvar : expr) : type_context bool
+
+/-- Run the given `type_context` monad in a temporary mvar scope.
+Doing this twice will push the old tmp_mvar assignments to a stack.
+So it is safe to do this whether or not you are already in tmp mode. -/
+meta constant tmp_mode (n_uvars n_mvars : nat) : type_context α → type_context α
+
+/-- Returns true when in temp mode. -/
+meta constant in_tmp_mode : type_context bool
+meta constant tmp_is_assigned : nat → type_context bool
+meta constant tmp_get_assignment : nat → type_context expr
+
+meta constant level.tmp_is_assigned : nat → type_context bool
+meta constant level.tmp_get_assignment : nat → type_context level
+
+/-- Replace each metavariable in the given expression with a temporary metavariable. -/
+meta constant to_tmp_mvars : expr → type_context (expr × list level × list expr)
+meta constant mk_tmp_mvar (index : nat) (type : expr): expr
+meta constant level.mk_tmp_mvar (index : nat) : level
+
+/-- Run the provided type_context within a backtracking scope.
+    This means that any changes to the metavariable context will not be committed if the
+    inner monad fails.
+    [warning]: the local context modified by `push_local` and `pop_local`
+    is not affected by `try`. Any unpopped locals will be present after the `try` even if the inner `type_context` failed.
+-/
+meta constant try {α : Type} : type_context α → type_context (option α)
+
+meta def orelse {α : Type} : type_context α → type_context α → type_context α
+| x y := try x >>= λ x, option.rec y pure x
+
+meta instance type_context_alternative : alternative type_context := {
+    failure := λ α, type_context.fail "failed",
+    orelse := λ α x y, type_context.orelse x y
+}
+
+meta constant run (inner : type_context α) (tr := tactic.transparency.semireducible) : tactic α
+
+meta def trace {α} [has_to_format α] : α → type_context unit | a :=
+   pure $ _root_.trace_fmt (to_fmt a) (λ u, ())
+
+meta def print_mvars : type_context unit := do
+    mvs ← list_mvars,
+    mvs ← pure $ mvs.map (λ x, match x with (expr.mvar _ pp _) := to_fmt pp | _ := "" end),
+    trace mvs
+
+/-- Same as tactic.get_fun_info -/
+meta constant get_fun_info (f : expr) (nargs : option nat := none) : type_context fun_info
+
+end type_context
+end tactic.unsafe

src/library/idx_metavar.cpp

@@ -156,7 +156,7 @@ struct to_idx_metavars_fn : public replace_visitor {
         return replace_visitor::visit(e);
     }
 };
-
+/** Replace each occurrence of a metavariable in `e` with a temporary metavariable. */
 expr to_idx_metavars(metavar_context const & mctx, expr const & e, buffer<level> & new_us, buffer<expr> & new_ms) {
     if (!has_metavar(e))
         return e;

src/library/metavar_context.cpp

@@ -28,6 +28,10 @@ bool is_metavar_decl_ref(expr const & e) {
     return is_metavar(e) && mlocal_type(e) == *g_dummy_type;
 }
 
+expr metavar_decl::mk_ref() const {
+    return mk_meta_ref(m_name, m_pp_name);
+}
+
 name get_metavar_decl_ref_suffix(level const & u) {
     lean_assert(is_metavar_decl_ref(u));
     return meta_id(u).replace_prefix(*g_meta_prefix, name());
@@ -51,10 +55,14 @@ level metavar_context::mk_univ_metavar_decl() {
 expr metavar_context::mk_metavar_decl(optional<name> const & pp_n, local_context const & ctx, expr const & type) {
     // TODO(Leo): should use name_generator
     name n = mk_meta_decl_name();
-    m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type)));
+    m_decls.insert(n, metavar_decl(ctx, head_beta_reduce(type), n, pp_n));
     return mk_meta_ref(n, pp_n);
 }
 
+bool metavar_context::is_declared(expr const & e) const {
+    return is_metavar(e) && m_decls.contains(mlocal_name(e));
+}
+
 optional<metavar_decl> metavar_context::find_metavar_decl(expr const & e) const {
     lean_assert(is_metavar_decl_ref(e));
     if (auto r = m_decls.find(mlocal_name(e)))
@@ -70,6 +78,10 @@ metavar_decl const & metavar_context::get_metavar_decl(expr const & e) const {
         throw exception("unknown metavariable");
 }
 
+void metavar_context::for_each(std::function<void(metavar_decl const &)> const & fn) const {
+    m_decls.for_each([&](name, metavar_decl const & d) { fn(d); });
+}
+
 optional<local_decl> metavar_context::find_local_decl(expr const & mvar, name const & n) const {
     auto mdecl = find_metavar_decl(mvar);
     if (!mdecl) return optional<local_decl>();
@@ -149,7 +161,7 @@ void metavar_context::instantiate_mvars_at_type_of(expr const & m) {
     expr type      = d.get_type();
     expr new_type  = instantiate_mvars(type);
     if (new_type != type) {
-        m_decls.insert(mlocal_name(m), metavar_decl(d.get_context(), new_type));
+        m_decls.insert(d.m_name, metavar_decl(d.get_context(), new_type, d.m_name, d.m_pp_name));
     }
 }
 

src/library/metavar_context.h

@@ -9,14 +9,19 @@ Author: Leonardo de Moura
 
 namespace lean {
 class metavar_decl {
-    local_context m_context;
-    expr          m_type;
+    name           m_name;
+    optional<name> m_pp_name;
+    local_context  m_context;
+    expr           m_type;
     friend class metavar_context;
-    metavar_decl(local_context const & ctx, expr const & type):m_context(ctx), m_type(type) {}
+    metavar_decl(local_context const & ctx, expr const & type, name const & n, optional<name> const & pp_name): m_name(n), m_pp_name(pp_name), m_context(ctx), m_type(type) {}
 public:
     metavar_decl() {}
+    name const & get_name() { return m_name; }
+    optional<name> const & get_pp_name() { return m_pp_name; }
     expr const & get_type() const { return m_type; }
     local_context const & get_context() const { return m_context; }
+    expr mk_ref() const;
 };
 
 bool is_metavar_decl_ref(level const & l);
@@ -44,6 +49,7 @@ class metavar_context {
     }
 
     optional<metavar_decl> find_metavar_decl(expr const & mvar) const;
+    void for_each(std::function<void(metavar_decl const &)> const & fn) const;
 
     metavar_decl const & get_metavar_decl(expr const & mvar) const;
 
@@ -59,7 +65,7 @@ class metavar_context {
         \pre find_metavar_decl(mvar)
         \pre find_metavar_decl(mvar)->get_context().get_local_decl(n) */
     expr get_local(expr const & mvar, name const & n) const;
-
+    bool is_declared(expr const & mvar) const;
     bool is_assigned(level const & l) const {
         lean_assert(is_metavar_decl_ref(l));
         return m_uassignment.contains(meta_id(l));

src/library/tactic/CMakeLists.txt

@@ -9,7 +9,9 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp
   simp_result.cpp user_attribute.cpp eval.cpp
   simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp
   vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp hole_command.cpp
-  elaborator_exception.cpp algebraic_normalizer.cpp tactic_evaluator.cpp)
+  elaborator_exception.cpp algebraic_normalizer.cpp tactic_evaluator.cpp
+  vm_local_context.cpp
+  vm_type_context.cpp)
 if(EMSCRIPTEN)
 add_dependencies(tactic gmp)
 endif()

src/library/tactic/fun_info_tactics.h

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 namespace lean {
+vm_obj to_obj(fun_info const & info);
 void initialize_fun_info_tactics();
 void finalize_fun_info_tactics();
 }

src/library/tactic/init_module.cpp

@@ -38,6 +38,8 @@ Author: Leonardo de Moura
 #include "library/tactic/hole_command.h"
 #include "library/tactic/backward/init_module.h"
 #include "library/tactic/smt/init_module.h"
+#include "library/tactic/vm_local_context.h"
+#include "library/tactic/vm_type_context.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -75,6 +77,8 @@ void initialize_tactic_module() {
     initialize_algebraic_normalizer();
     initialize_hole_command();
     initialize_smt_module();
+    initialize_vm_local_context();
+    initialize_vm_type_context();
 }
 void finalize_tactic_module() {
     finalize_smt_module();
@@ -111,5 +115,7 @@ void finalize_tactic_module() {
     finalize_intro_tactic();
     finalize_tactic_state();
     finalize_kabstract();
+    finalize_vm_local_context();
+    finalize_vm_type_context();
 }
 }