michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/hop_match): do not match iff with =

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-28 00:21:05 -08:00
parent db45d02078
commit 6da1b447f0
3 changed files with 52 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/library/hop_match.cpp
View file

@ -272,46 +272,36 @@ class hop_match_fn {
return match_constant(p, t);
}
if (is_equality(p) && is_equality(t) && (!is_eq(p) || !is_eq(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 = get_equality_args(p);
expr_pair p2 = get_equality_args(t);
return match(p1.first, p2.first, ctx, ctx_size) && match(p1.second, p2.second, ctx, ctx_size);
} else {
if (p.kind() != t.kind())
return false;
switch (p.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
case expr_kind::Value: case expr_kind::MetaVar:
return false;
case expr_kind::App: {
unsigned i1 = num_args(p);
unsigned i2 = num_args(t);
while (i1 > 0 && i2 > 0) {
--i1;
--i2;
if (i1 == 0 && i2 > 0) {
return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
} else if (i2 == 0 && i1 > 0) {
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;
}
if (p.kind() != t.kind())
return false;
switch (p.kind()) {
case expr_kind::Var: case expr_kind::Constant: case expr_kind::Type:
case expr_kind::Value: case expr_kind::MetaVar:
return false;
case expr_kind::App: {
unsigned i1 = num_args(p);
unsigned i2 = num_args(t);
while (i1 > 0 && i2 > 0) {
--i1;
--i2;
if (i1 == 0 && i2 > 0) {
return match(arg(p, i1), mk_app(i2+1, begin_args(t)), ctx, ctx_size);
} else if (i2 == 0 && i1 > 0) {
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;
}
return true;
}
case expr_kind::Lambda: case expr_kind::Pi:
return
match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
case expr_kind::Let:
// TODO(Leo)
return false;
}
return true;
}
case expr_kind::Lambda: case expr_kind::Pi:
return
match(abst_domain(p), abst_domain(t), ctx, ctx_size) &&
match(abst_body(p), abst_body(t), extend(ctx, abst_name(t), abst_domain(t)), ctx_size+1);
case expr_kind::Let:
// TODO(Leo)
return false;
}
lean_unreachable();
}

16
tests/lean/nnf.lean Normal file
View file

@ -0,0 +1,16 @@
rewrite_set NNF
add_rewrite not_not_eq not_true not_false not_neq not_and not_or not_iff not_implies not_forall
not_exists forall_and_distribute exists_and_distributer exists_and_distributel : NNF
variable p : Nat → Nat → Bool
variable f : Nat → Nat
variable g : Nat → Nat → Nat
(*
local t1 = parse_lean('¬ ∀ x, (∃ y, p x y ∨ p (f x) (f y)) ∨ f 0 = 1')
local t2, pr = simplify(t1, "NNF")
print(t1)
print("====>")
print(t2)
get_environment():type_check(pr)
*)

8
tests/lean/nnf.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Assumed: p
Assumed: f
Assumed: g
¬ (∀ x : ℕ, (∃ y : ℕ, p x y ∨ p (f x) (f y)) ∨ f 0 = 1)
====>
(∃ x : ℕ, (∀ x::1 : ℕ, ¬ p x x::1) ∧ (∀ x::1 : ℕ, ¬ p (f x) (f x::1))) ∧ ¬ f 0 = 1