From 3db0ebdcf0a71b43e34106ccb5e1a1e91d40de11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Wed, 15 Feb 2017 23:16:06 -0500 Subject: [PATCH] feat(library/tactic/match_tactic): return also assignments for universe meta-variables --- library/init/meta/match_tactic.lean | 19 ++++++++------- src/library/tactic/match_tactic.cpp | 36 +++++++++++++++++------------ src/library/vm/vm.cpp | 5 ++++ src/library/vm/vm.h | 1 + tests/lean/run/do_match_else.lean | 4 ++-- tests/lean/run/match_pattern1.lean | 4 ++-- tests/lean/run/match_pattern2.lean | 2 +- 7 files changed, 43 insertions(+), 28 deletions(-) diff --git a/library/init/meta/match_tactic.lean b/library/init/meta/match_tactic.lean index a91d862341..3ae618dce6 100644 --- a/library/init/meta/match_tactic.lean +++ b/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 diff --git a/src/library/tactic/match_tactic.cpp b/src/library/tactic/match_tactic.cpp index 09f0ccaef4..195a91aa44 100644 --- a/src/library/tactic/match_tactic.cpp +++ b/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 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 const & uos, list 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 & os, unsigned & nuvars, unsigned & nmvars) { - lean_assert(csize(p) == 4); +void get_pattern_fields(vm_obj const & p, expr & target, list & uos, list & 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 const & ls, list const & es, expr const & t, list const & os) { + vm_obj mk(list const & ls, list const & es, expr const & t, list const & ous, list const & os) { mk_level_uvars(ls); mk_expr_mvars(es); expr target = convert(t); check_levels(ls); check_exprs(es); list output = map(os, [&](expr const & e) { return convert(e); }); - return mk_pattern(target, output, length(ls), length(es)); + list 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 os; unsigned nuvars, nmvars; - get_pattern_fields(p, t, os, nuvars, nmvars); + expr t; list uos; list 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 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)); } diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index ae9176fed3..2d7fb29181 100644 --- a/src/library/vm/vm.cpp +++ b/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); } diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 6bd96b6399..7a28d60857 100644 --- a/src/library/vm/vm.h +++ b/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 args); diff --git a/tests/lean/run/do_match_else.lean b/tests/lean/run/do_match_else.lean index 18a7101017..bf16e9dfd4 100644 --- a/tests/lean/run/do_match_else.lean +++ b/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 diff --git a/tests/lean/run/match_pattern1.lean b/tests/lean/run/match_pattern1.lean index c15a050e42..4562a85c78 100644 --- a/tests/lean/run/match_pattern1.lean +++ b/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), diff --git a/tests/lean/run/match_pattern2.lean b/tests/lean/run/match_pattern2.lean index 89081c0427..a5a53bed3b 100644 --- a/tests/lean/run/match_pattern2.lean +++ b/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