feat(library/tactic/match_tactic): return also assignments for universe meta-variables

library/init/meta/match_tactic.lean

@@ -10,29 +10,32 @@ namespace tactic
 meta structure pattern :=
 /- Term to match. -/
 (target : expr)
+/- Set of universes that is instantiated for each successful match. -/
+(uoutput : list level)
 /- Set of terms that is instantiated for each successful match. -/
-(output : list expr)
+(moutput : list expr)
 /- Number of (temporary) universe meta-variables in this pattern. -/
 (nuvars : nat)
 /- Number of (temporary) meta-variables in this pattern. -/
 (nmvars : nat)
 
-/- (mk_pattern ls es t o) creates a new pattern with (length ls) universe meta-variables and (length es) meta-variables.
+/- (mk_pattern ls es t u o) creates a new pattern with (length ls) universe meta-variables and (length es) meta-variables.
    In the produced pattern p, we have that
    - (pattern.target p) is the term t where the universes ls and expressions es have been replaced with temporary meta-variables.
-   - (pattern.output p) is the list o where the universes ls and expressions es have been replaced with temporary meta-variables.
+   - (pattern.uoutput p) is the list u where the universes ls have been replaced with temporary meta-variables.
+   - (pattern.moutput p) is the list o where the universes ls and expressions es have been replaced with temporary meta-variables.
    - (pattern.nuvars p) = length ls
    - (pattern.nmvars p) = length es
 
    The tactic fails if o and the types of es do not contain all universes ls and expressions es. -/
-meta constant mk_pattern : list level → list expr → expr → list expr → tactic pattern
+meta constant mk_pattern : list level → list expr → expr → list level → list expr → tactic pattern
 /- (mk_pattern_core m p e) matches (pattern.target p) and e using transparency m.
    If the matching is successful, then return the instantiation of (pattern.output p).
    The tactic fails if not all (temporary) meta-variables are assigned. -/
-meta constant match_pattern_core : transparency → pattern → expr → tactic (list expr)
+meta constant match_pattern_core : transparency → pattern → expr → tactic (list level × list expr)
 
-meta def match_pattern : pattern → expr → tactic (list expr) :=
-match_pattern_core semireducible
+meta def match_pattern (p : pattern) (e : expr) : tactic (list expr) :=
+fmap prod.snd (match_pattern_core semireducible p e)
 
 open expr
 
@@ -52,7 +55,7 @@ private meta def to_pattern_core : expr → tactic (expr × list expr)
 meta def pexpr_to_pattern (p : pexpr) : tactic pattern :=
 do e ← to_expr p,
    (new_p, xs) ← to_pattern_core e,
-   mk_pattern [] xs new_p xs
+   mk_pattern [] xs new_p [] xs
 
 /- Convert pre-term into a pattern and try to match e.
    Given p of the form (λ x_1 ... x_n, t[x_1, ..., x_n]), a successful

src/library/tactic/match_tactic.cpp

@@ -17,18 +17,19 @@ Author: Leonardo de Moura
 namespace lean {
 /*
 structure pattern :=
-(target : expr) (output : list expr) (nuvars : nat) (nmvars : nat)
+(target : expr) (uoutput : list level) (output : list expr) (nuvars : nat) (nmvars : nat)
 */
-vm_obj mk_pattern(expr const & target, list<expr> const & os, unsigned nuvars, unsigned nmvars) {
-    return mk_vm_constructor(0, to_obj(target), to_obj(os), mk_vm_nat(nuvars), mk_vm_nat(nmvars));
+vm_obj mk_pattern(expr const & target, list<level> const & uos, list<expr> const & os, unsigned nuvars, unsigned nmvars) {
+    return mk_vm_constructor(0, to_obj(target), to_obj(uos), to_obj(os), mk_vm_nat(nuvars), mk_vm_nat(nmvars));
 }
 
-void get_pattern_fields(vm_obj const & p, expr & target, list<expr> & os, unsigned & nuvars, unsigned & nmvars) {
-    lean_assert(csize(p) == 4);
+void get_pattern_fields(vm_obj const & p, expr & target, list<level> & uos, list<expr> & os, unsigned & nuvars, unsigned & nmvars) {
+    lean_assert(csize(p) == 5);
     target = to_expr(cfield(p, 0));
-    os     = to_list_expr(cfield(p, 1));
-    nuvars = force_to_unsigned(cfield(p, 2), 0);
-    nmvars = force_to_unsigned(cfield(p, 3), 0);
+    uos    = to_list_level(cfield(p, 1));
+    os     = to_list_expr(cfield(p, 2));
+    nuvars = force_to_unsigned(cfield(p, 3), 0);
+    nmvars = force_to_unsigned(cfield(p, 4), 0);
 }
 
 struct mk_pattern_fn {
@@ -110,14 +111,15 @@ struct mk_pattern_fn {
         }
     }
 
-    vm_obj mk(list<level> const & ls, list<expr> const & es, expr const & t, list<expr> const & os) {
+  vm_obj mk(list<level> const & ls, list<expr> const & es, expr const & t, list<level> const & ous, list<expr> const & os) {
         mk_level_uvars(ls);
         mk_expr_mvars(es);
         expr target = convert(t);
         check_levels(ls);
         check_exprs(es);
         list<expr> output = map(os, [&](expr const & e) { return convert(e); });
-        return mk_pattern(target, output, length(ls), length(es));
+        list<level> uoutput = map(ous, [&](level const & e) { return convert(e); });
+        return mk_pattern(target, uoutput, output, length(ls), length(es));
     }
 };
 
@@ -127,9 +129,9 @@ struct mk_pattern_fn {
 /*
 meta_constant mk_pattern : list level → list expr → expr → list expr → tactic pattern
 */
-vm_obj tactic_mk_pattern(vm_obj const & ls, vm_obj const & es, vm_obj const & t, vm_obj const & os, vm_obj const & s) {
+vm_obj tactic_mk_pattern(vm_obj const & ls, vm_obj const & es, vm_obj const & t, vm_obj const & ous, vm_obj const & os, vm_obj const & s) {
     TRY;
-    vm_obj pattern = mk_pattern_fn(tactic::to_state(s)).mk(to_list_level(ls), to_list_expr(es), to_expr(t), to_list_expr(os));
+    vm_obj pattern = mk_pattern_fn(tactic::to_state(s)).mk(to_list_level(ls), to_list_expr(es), to_expr(t), to_list_level(ous), to_list_expr(os));
     return tactic::mk_success(pattern, tactic::to_state(s));
     CATCH;
 }
@@ -139,8 +141,8 @@ meta_constant match_pattern_core : transparency → pattern → expr → tactic
 */
 vm_obj tactic_match_pattern_core(vm_obj const & m, vm_obj const & p, vm_obj const & e, vm_obj const & s) {
     TRY;
-    expr t; list<expr> os; unsigned nuvars, nmvars;
-    get_pattern_fields(p, t, os, nuvars, nmvars);
+    expr t; list<level> uos; list<expr> os; unsigned nuvars, nmvars;
+    get_pattern_fields(p, t, uos, os, nuvars, nmvars);
     type_context ctx = mk_type_context_for(s, m);
     type_context::tmp_mode_scope scope(ctx, nuvars, nmvars);
     if (ctx.is_def_eq(t, to_expr(e))) {
@@ -156,7 +158,11 @@ vm_obj tactic_match_pattern_core(vm_obj const & m, vm_obj const & p, vm_obj cons
         for (expr const & o : os) {
             inst_os.push_back(ctx.instantiate_mvars(o));
         }
-        return tactic::mk_success(to_obj(to_list(inst_os)), tactic::to_state(s));
+        buffer<level> inst_uos;
+        for (level const & uo : uos) {
+            inst_uos.push_back(ctx.instantiate_mvars(uo));
+        }
+        return tactic::mk_success(mk_vm_pair(to_obj(to_list(inst_uos)), to_obj(to_list(inst_os))), tactic::to_state(s));
     } else {
         return tactic::mk_exception("match_pattern failed", tactic::to_state(s));
     }

src/library/vm/vm.cpp

@@ -102,6 +102,11 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm
     return mk_vm_constructor(cidx, 4, args);
 }
 
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const & o1, vm_obj const & o2, vm_obj const & o3, vm_obj const & o4, vm_obj const & o5) {
+    vm_obj args[5] = {o1, o2, o3, o4, o5};
+    return mk_vm_constructor(cidx, 5, args);
+}
+
 vm_obj mk_vm_closure(unsigned fn_idx, unsigned sz, vm_obj const * data) {
     return mk_vm_composite(vm_obj_kind::Closure, fn_idx, sz, data);
 }

src/library/vm/vm.h

@@ -225,6 +225,7 @@ vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &);
 vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
+vm_obj mk_vm_constructor(unsigned cidx, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &);
 /* TODO(Leo, Jared): delete native closures that take environment as argument */
 vm_obj mk_native_closure(environment const & env, name const & n, unsigned sz, vm_obj const * args);
 vm_obj mk_native_closure(environment const & env, name const & n, std::initializer_list<vm_obj const> args);

tests/lean/run/do_match_else.lean

@@ -11,8 +11,8 @@ by do
   H ← get_local `H >>= infer_type,
   (lhs, rhs) ← match_eq H,
   nat_add : expr ← mk_const `nat.add,
-  p : pattern    ← mk_pattern [] [a, b] (app2 nat_add a b) [app2 nat_add b a, a, b],
-  trace (pattern.output p),
+  p : pattern    ← mk_pattern [] [a, b] (app2 nat_add a b) [] [app2 nat_add b a, a, b],
+  trace (pattern.moutput p),
   [v₁, v₂, v₃] ← match_pattern p lhs | failed,
   trace v₁, trace v₂, trace v₃,
   constructor

tests/lean/run/match_pattern1.lean

@@ -6,8 +6,8 @@ example (a b c x y : nat) (H : nat.add (nat.add x y) y = 0) : true :=
 by do
   a ← get_local `a, b ← get_local `b, c ← get_local `c,
   nat_add : expr ← mk_const `nat.add,
-  p : pattern    ← mk_pattern [] [a, b] (app_of_list nat_add [a, b]) [app_of_list nat_add [b, a], a, b],
-  trace (pattern.output p),
+  p : pattern    ← mk_pattern [] [a, b] (app_of_list nat_add [a, b]) [] [app_of_list nat_add [b, a], a, b],
+  trace (pattern.moutput p),
   H ← get_local `H >>= infer_type,
   lhs_rhs ← match_eq H,
   out     ← match_pattern p (prod.fst lhs_rhs),

tests/lean/run/match_pattern2.lean

@@ -18,7 +18,7 @@ do env ← get_env,
    ls  : list level   ← return $ map level.param (declaration.univ_params d),
    (some type)        ← return $ declaration.instantiate_type_univ_params d ls | failed,
    (es, lhs, rhs)     ← pattern_telescope type [],
-   p   : pattern      ← mk_pattern ls es lhs [rhs, app_of_list (expr.const n ls) es],
+   p   : pattern      ← mk_pattern ls es lhs [] [rhs, app_of_list (expr.const n ls) es],
    return p
 
 open nat