fix(library/hop_match): bugs in the higher-order matching procedure, add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
acfb11e290
commit
8217a544cc
2 changed files with 88 additions and 19 deletions
|
|
@ -104,12 +104,29 @@ class hop_match_fn {
|
|||
return some_expr(r);
|
||||
}
|
||||
|
||||
// We say \c t has a simple projection when it is of the form (f v1 ... vn)
|
||||
// where f does no contain locally bound variables, and v1 ... vn are exactly the variables in vars.
|
||||
// In this case, the proj procedure can return f instead of (fun xn .... x1, f x1 ... xn)
|
||||
bool is_simple_proj(expr const & t, unsigned ctx_size, buffer<expr> const & vars) {
|
||||
if (is_app(t) && !has_locally_bound_var(arg(t, 0), ctx_size) && num_args(t) == vars.size() + 1) {
|
||||
for (unsigned i = 0; i < vars.size(); i++)
|
||||
if (arg(t, i+1) != vars[i])
|
||||
return false;
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return <tt>(fun (x1 ... xn) t')</tt> if all locally bound variables in \c t occur in vars.
|
||||
\c n is the size of \c vars.
|
||||
None is returned if \c t contains a locally bound variable that does not occur in \c vars.
|
||||
*/
|
||||
optional<expr> proj(expr const & t, context const & ctx, unsigned ctx_size, buffer<expr> const & vars) {
|
||||
if (is_simple_proj(t, ctx_size, vars)) {
|
||||
return some_expr(lower_free_vars(arg(t, 0), ctx_size, ctx_size));
|
||||
}
|
||||
optional<expr> t_prime = proj_core(t, ctx_size, vars, vars.size());
|
||||
if (!t_prime)
|
||||
return none_expr();
|
||||
|
|
@ -137,39 +154,40 @@ class hop_match_fn {
|
|||
if (is_free_var(p, ctx_size)) {
|
||||
auto s = get_subst(p, ctx_size);
|
||||
if (s) {
|
||||
return match(lift_free_vars(*s, ctx_size), t, ctx, ctx_size);
|
||||
return lift_free_vars(*s, ctx_size) == t;
|
||||
} else if (has_locally_bound_var(t, ctx_size)) {
|
||||
return false;
|
||||
} else {
|
||||
assign(p, lower_free_vars(t, ctx_size, ctx_size), ctx_size);
|
||||
return true;
|
||||
}
|
||||
} else if (is_app(p) && is_free_var(arg(p, 0), ctx_size)) {
|
||||
} else if (is_app(p) && is_free_var(arg(p, 0), ctx_size) && args_are_distinct_locally_bound_vars(p, ctx_size, m_vars)) {
|
||||
// higher-order pattern case
|
||||
auto s = get_subst(arg(p, 0), ctx_size);
|
||||
unsigned num = num_args(p);
|
||||
if (s) {
|
||||
expr f = lift_free_vars(*s, ctx_size);
|
||||
expr new_p = apply_beta(f, num - 1, &(arg(p, 1)));
|
||||
return match(new_p, t, ctx, ctx_size);
|
||||
return new_p == t;
|
||||
} else {
|
||||
// Check if p is a higher-order pattern.
|
||||
// That is, all arguments are distinct locally bound variables
|
||||
if (args_are_distinct_locally_bound_vars(p, ctx_size, m_vars)) {
|
||||
optional<expr> new_t = proj(t, ctx, ctx_size, m_vars);
|
||||
if (new_t) {
|
||||
assign(arg(p, 0), *new_t, ctx_size);
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
optional<expr> new_t = proj(t, ctx, ctx_size, m_vars);
|
||||
if (new_t) {
|
||||
assign(arg(p, 0), *new_t, ctx_size);
|
||||
return true;
|
||||
}
|
||||
// fallback to the first-order case
|
||||
}
|
||||
}
|
||||
|
||||
if (p == t)
|
||||
if (p == t && !has_free_var_ge(p, ctx_size)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (is_eq_heq(p) && is_eq_heq(t)) {
|
||||
if (is_eq_heq(p) && is_eq_heq(t) && (is_heq(p) || is_heq(t))) {
|
||||
// Remark: if p and t are homogeneous equality, then we handle as an application (in the else branch)
|
||||
// We do that because we can get more information. For example, the pattern
|
||||
// may be (eq #1 a b).
|
||||
// This branch ignores the type.
|
||||
expr_pair p1 = eq_heq_args(p);
|
||||
expr_pair p2 = eq_heq_args(t);
|
||||
return match(p1.first, p2.first, ctx, ctx_size) && match(p1.second, p2.second, ctx, ctx_size);
|
||||
|
|
@ -187,11 +205,9 @@ class hop_match_fn {
|
|||
--i1;
|
||||
--i2;
|
||||
if (i1 == 0 && i2 > 0) {
|
||||
if (!match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size))
|
||||
return false;
|
||||
return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
|
||||
} else if (i2 == 0 && i1 > 0) {
|
||||
if (!match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size))
|
||||
return false;
|
||||
return match(mk_app(i1+1, begin_args(p)), arg(t, i2), ctx, ctx_size);
|
||||
} else {
|
||||
if (!match(arg(p, i1), arg(t, i2), ctx, ctx_size))
|
||||
return false;
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ function hoptst(rule, target, expected)
|
|||
local p = pibody(th):arg(2)
|
||||
local t = funbody(parse_lean(target))
|
||||
local r = hop_match(p, t)
|
||||
-- print(p, t)
|
||||
if (r and not expected) or (not r and expected) then
|
||||
error("test failed: " .. tostring(rule) .. " === " .. tostring(target))
|
||||
end
|
||||
|
|
@ -34,6 +35,7 @@ function hoptst(rule, target, expected)
|
|||
print("#" .. tostring(i) .. " <--- " .. tostring(r[i]))
|
||||
end
|
||||
print ""
|
||||
t = t:beta_reduce()
|
||||
if s ~= t then
|
||||
print("Mismatch")
|
||||
print(s)
|
||||
|
|
@ -47,8 +49,15 @@ parse_lean_cmds([[
|
|||
variable f : Nat -> Nat -> Nat
|
||||
variable g : Nat -> Nat
|
||||
variable p : Nat -> Bool
|
||||
variable n : Nat
|
||||
]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat), (forall x : Nat, h 0 = h x) = true]],
|
||||
[[fun (ff : Nat -> Nat), forall x : Nat, ff 0 = ff x]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat -> Nat) (a : Nat), (forall x : Nat, (h x a) = a) = true]],
|
||||
[[fun (a b c : Nat), (forall x : Nat, (f x b) = b)]])
|
||||
|
||||
hoptst([[forall (A : TypeU) (P Q : A -> Bool), (forall x : A, P x /\ Q x) = ((forall x : A, P x) /\ (forall x : A, Q x))]],
|
||||
[[forall x : Nat, p (f x 0) /\ f (f x x) 1 >= 0]])
|
||||
|
||||
|
|
@ -70,3 +79,47 @@ hoptst([[forall (F G : Nat -> Bool), (forall x : Nat, F x = (F x ∧ G x)) = (F
|
|||
hoptst([[forall (F G : Nat -> Nat), (forall x y : Nat, F x = x /\ G y = y) = (F = G)]],
|
||||
[[fun (a b c : Nat), (forall x y : Nat, f x (f (g y) c) = x /\ (f (g (g (f y c))) a) = y)]], false)
|
||||
|
||||
hoptst([[forall (a : Bool), (a /\ true) = a]],
|
||||
[[fun (p1 p2 p3 : Bool), (p1 /\ p2) /\ true]])
|
||||
|
||||
hoptst([[forall (a : Bool), (a /\ true) = a]],
|
||||
[[fun (p1 p2 p3 : Bool), (p1 /\ p2) /\ false]], false)
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat) (a : Nat), (h a) = a]],
|
||||
[[fun (a b c : Nat), f a b]])
|
||||
|
||||
hoptst([[forall (a : Nat), (g a) = a]],
|
||||
[[fun (a b c : Nat), f a b]], false)
|
||||
|
||||
hoptst([[forall (A : Type) (a : A), (a = a) = true]],
|
||||
[[fun (a b : Nat), b = b]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat), (forall x : Nat, h x = h 0) = true]],
|
||||
[[fun (ff : Nat -> Nat), forall x : Nat, ff x = ff 0]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat), (forall x : Nat, h x = h 0) = true]],
|
||||
[[fun (ff : Nat -> Nat) (a b c : Nat), forall x : Nat, ff x = ff 0]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat -> Bool), (forall x : Nat, h x x) = true]],
|
||||
[[fun (a b : Nat), forall x : Nat, f x x]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat -> Bool), (forall x : Nat, h x x) = true]], -- this is not a higher-order pattern
|
||||
[[fun (a b : Nat), forall x : Nat, f (f x) (f x)]], false)
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat -> Bool), (forall x : Nat, h n x) = true]],
|
||||
[[fun (ff : Nat -> Nat -> Bool) (a b : Nat), forall x : Nat, ff n x]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Nat -> Bool), (forall x : Nat, h n x) = true]], -- this is not a higher-order pattern
|
||||
[[fun (ff : Nat -> Nat -> Bool) (a b : Nat), forall x : Nat, ff n (g x)]], false)
|
||||
|
||||
hoptst([[forall (h : Nat -> Bool), (forall x y : Nat, h x) = true]],
|
||||
[[fun (a b : Nat), forall x y : Nat, (fun z : Nat, z + x) (fun w1 w2 : Nat, w1 + w2 + x)]])
|
||||
|
||||
hoptst([[forall (h : Nat -> Bool), (forall x y : Nat, h y) = true]],
|
||||
[[fun (a b : Nat), forall x y : Nat, (fun z : Nat, z + y) (fun w1 w2 : Nat, w1 + w2 + y)]])
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue