max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/parser): revised pattern validation

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-17 15:11:52 -07:00
parent 5ffa481634
commit 93d48ae620
6 changed files with 206 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/logic.lean
View file

@ -223,16 +223,16 @@ theorem eq_rec_heq {A : Type} {P : A → Type} {a a' : A} (H : a = a') (p : P a)
eq.drec_on H (heq.refl p)
theorem heq_of_eq_rec_left {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a = a') (h₂ : eq.rec_on e p₁ = p₂), p₁ == p₂
| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
| a ⌞a⌟ p₁ p₂ (eq.refl ⌞a⌟) h := eq.rec_on h (heq.refl p₁)
theorem heq_of_eq_rec_right {A : Type} {P : A → Type} : ∀ {a a' : A} {p₁ : P a} {p₂ : P a'} (e : a' = a) (h₂ : p₁ = eq.rec_on e p₂), p₁ == p₂
| a a p₁ p₂ (eq.refl a) h := eq.rec_on h (heq.refl p₁)
| a ⌞a⌟ p₁ p₂ (eq.refl ⌞a⌟) h := eq.rec_on h (heq.refl p₁)
theorem of_heq_true {a : Prop} (H : a == true) : a :=
of_eq_true (eq_of_heq H)
theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), eq.rec_on p₁ (eq.rec_on p₂ a : B) = eq.rec_on (eq.trans p₂ p₁) a
| A A A (eq.refl A) (eq.refl A) a := calc
| A ⌞A⌟ ⌞A⌟ (eq.refl ⌞A⌟) (eq.refl ⌞A⌟) a := calc
eq.rec_on (eq.refl A) (eq.rec_on (eq.refl A) a) = eq.rec_on (eq.refl A) a : rfl
... = eq.rec_on (eq.trans (eq.refl A) (eq.refl A)) a : eq.subst (proof_irrel (eq.refl A) (eq.trans (eq.refl A) (eq.refl A))) rfl
@ -240,7 +240,7 @@ theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁
eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
theorem eq_rec_of_heq_left : ∀ {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂), eq.rec_on (type_eq_of_heq h) a₁ = a₂
| A A a a (heq.refl a) := rfl
| A ⌞A⌟ a ⌞a⌟ (heq.refl ⌞a⌟) := rfl
theorem eq_rec_of_heq_right {A₁ A₂ : Type} {a₁ : A₁} {a₂ : A₂} (h : a₁ == a₂) : a₁ = eq.rec_on (eq.symm (type_eq_of_heq h)) a₂ :=
eq_rec_eq_eq_rec (eq_rec_of_heq_left h)
@ -252,7 +252,7 @@ attribute heq_of_eq_of_heq [trans]
attribute heq.symm [symm]
theorem cast_heq : ∀ {A B : Type} (H : A = B) (a : A), cast H a == a
| A A (eq.refl A) a := heq.refl a
| A ⌞A⌟ (eq.refl ⌞A⌟) a := heq.refl a
/- and -/

2
library/init/sigma.lean
View file

@ -29,7 +29,7 @@ namespace sigma
variable (Rb : ∀ a, B a → B a → Prop)
theorem dpair_eq : ∀ {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂), eq.rec_on H₁ b₁ = b₂ → (sigma.mk a₁ b₁) = (sigma.mk a₂ b₂)
| a₁ a₁ b₁ b₁ (eq.refl a₁) (eq.refl b₁) := rfl
| a₁ ⌞a₁⌟ b₁ ⌞b₁⌟ (eq.refl ⌞a₁⌟) (eq.refl ⌞b₁⌟) := rfl
protected theorem eq {p₁ p₂ : Σa : A, B a} :
∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=

124
src/frontends/lean/parser.cpp
View file

@ -1611,16 +1611,51 @@ expr parser::parse_led_notation(expr left) {
}
}
/**
\brief Auxiliary object for converting pattern_or_expr into a pattern.
The main points are:
1- Collect all pattern variables. Each pattern variable can only be
"declared" once. That is, the following equation is not valid
definition f : nat -> nat -> nat
| a a := a
2- We do not collect pattern variables inside inaccessible term (e.g., ⌞f a⌟)
Remark: An inaccessible term may contain a reference to a variable defined
later. Here is an example:
inductive imf {A B : Type} (f : A → B) : B → Type
| mk : ∀ (a : A), imf (f a)
definition inv {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞f a⌟ (imf.mk ⌞f⌟ a) := a
The 'a' in ⌞f a⌟ is a reference to the variable 'a' being declared at
(imf.mk ⌞f⌟ a)
3- The type in type ascriptions is implicitly marked as inaccessible.
4- An inaccessible term cannot be the function in an application.
Example: (⌞f⌟ a) is not allowed.
5- In a pattern (f a), f must be a constructor or a constant tagged with the
[pattern] attribute
6- A '_' is treated as an anonymous variable in patterns, and as placeholder
inside of inaccessible terms. */
struct to_pattern_fn {
parser & m_parser;
buffer<expr> & m_new_locals;
name_map<expr> m_vars;
environment const & env() { return m_parser.env(); }
name_map<expr> m_locals_map; // local variable name --> its interpretation
expr_map<expr> m_anonymous_vars; // for _
to_pattern_fn(parser & p, buffer<expr> & new_locals):
m_parser(p), m_new_locals(new_locals) {}
environment const & env() { return m_parser.env(); }
/* Return true iff the constant n may occur in a pattern */
bool is_pattern_constant(name const & n) {
if (inductive::is_intro_rule(env(), n))
@ -1630,13 +1665,13 @@ struct to_pattern_fn {
return false;
}
expr visit_local(expr const & e) {
if (auto r = m_vars.find(local_pp_name(e)))
return *r;
void collect_new_local(expr const & e) {
name const & n = local_pp_name(e);
bool resolve_only = true;
expr new_e = m_parser.id_to_expr(local_pp_name(e), m_parser.pos_of(e), resolve_only);
expr new_e = m_parser.id_to_expr(n, m_parser.pos_of(e), resolve_only);
if (is_constant(new_e) && is_pattern_constant(const_name(new_e))) {
return new_e;
m_locals_map.insert(n, new_e);
return;
} else if (is_choice(new_e)) {
bool all_pattern_constant = true;
bool has_pattern_constant = false;
@ -1648,7 +1683,8 @@ struct to_pattern_fn {
all_pattern_constant = false;
}
if (all_pattern_constant) {
return new_e;
m_locals_map.insert(n, new_e);
return;
} else if (has_pattern_constant) {
throw parser_error(sstream() << "invalid pattern, '" << e << "' is overloaded, "
<< "and some interpretations may occur in patterns and others not "
@ -1658,19 +1694,53 @@ struct to_pattern_fn {
// assume e is a variable shadowing overloaded constants
}
}
if (!local_pp_name(e).is_atomic()) {
if (!n.is_atomic()) {
throw parser_error("invalid pattern, variable, constructor or constant tagged as pattern expected",
m_parser.pos_of(e));
}
m_vars.insert(local_pp_name(e), e);
if (m_locals_map.contains(n)) {
throw parser_error(sstream() << "invalid pattern, '" << n << "' already appeared in this pattern",
m_parser.pos_of(e));
}
m_locals_map.insert(n, e);
m_new_locals.push_back(e);
return e;
}
void collect_new_locals(expr const & e, bool skip_main_fn) {
if (is_typed_expr(e)) {
collect_new_locals(get_typed_expr_expr(e), false);
} else if (is_prenum(e)) {
// do nothing
} else if (is_inaccessible(e)) {
// do nothing
} else if (is_placeholder(e)) {
expr r = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
m_new_locals.push_back(r);
m_anonymous_vars.insert(mk_pair(e, r));
} else if (is_app(e)) {
collect_new_locals(app_fn(e), skip_main_fn);
collect_new_locals(app_arg(e), false);
} else if (is_local(e)) {
if (skip_main_fn) {
// do nothing
} else {
collect_new_local(e);
}
} else if (is_annotation(e)) {
collect_new_locals(get_annotation_arg(e), skip_main_fn);
} else if (is_constant(e) && is_pattern_constant(const_name(e))) {
// do nothing
} else {
throw parser_error("invalid pattern, must be an application, "
"constant, variable, type ascription or inaccessible term",
m_parser.pos_of(e));
}
}
expr to_expr(expr const & e) {
return replace(e, [&](expr const & e, unsigned) {
if (is_local(e)) {
if (auto r = m_vars.find(local_pp_name(e)))
if (auto r = m_locals_map.find(local_pp_name(e)))
return some_expr(*r);
else
return some_expr(m_parser.patexpr_to_expr(e));
@ -1679,9 +1749,9 @@ struct to_pattern_fn {
});
}
expr visit(expr const & e, bool skip_main_fn) {
expr visit(expr const & e) {
if (is_typed_expr(e)) {
expr new_v = visit(get_typed_expr_expr(e), false);
expr new_v = visit(get_typed_expr_expr(e));
expr new_t = to_expr(get_typed_expr_type(e));
return copy_tag(e, mk_typed_expr(new_t, new_v));
} else if (is_prenum(e)) {
@ -1689,20 +1759,22 @@ struct to_pattern_fn {
} else if (is_inaccessible(e)) {
return to_expr(e);
} else if (is_placeholder(e)) {
expr r = mk_local(mk_fresh_name(), "_x", mk_expr_placeholder(), binder_info());
m_new_locals.push_back(r);
return r;
return m_anonymous_vars.find(e)->second;
} else if (is_app(e)) {
expr new_f = visit(app_fn(e), skip_main_fn);
expr new_a = visit(app_arg(e), false);
if (is_inaccessible(app_fn(e))) {
throw parser_error("invalid inaccessible annotation, it cannot be used around functions in applications",
m_parser.pos_of(e));
}
expr new_f = visit(app_fn(e));
expr new_a = visit(app_arg(e));
return update_app(e, new_f, new_a);
} else if (is_local(e)) {
if (skip_main_fn)
return e;
if (auto r = m_locals_map.find(local_pp_name(e)))
return *r;
else
return visit_local(e);
return e;
} else if (is_annotation(e)) {
return copy_tag(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e), skip_main_fn)));
return copy_tag(e, mk_annotation(get_annotation_kind(e), visit(get_annotation_arg(e))));
} else if (is_constant(e) && is_pattern_constant(const_name(e))) {
return e;
} else {
@ -1713,7 +1785,9 @@ struct to_pattern_fn {
}
expr operator()(expr const & e, bool skip_main_fn) {
return visit(e, skip_main_fn);
collect_new_locals(e, skip_main_fn);
expr r = visit(e);
return r;
}
};

82
tests/lean/inaccessible.lean Normal file
View file

@ -0,0 +1,82 @@
inductive imf {A B : Type} (f : A → B) : B → Type
| mk : ∀ (a : A), imf (f a)
definition inv_1 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞f a⌟ (imf.mk ⌞f⌟ a) := a
definition inv_2 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞_⌟ (imf.mk ⌞_⌟ a) := a
definition mk {A B : Type} {f : A → B} (a : A) := imf.mk f a
definition inv_3 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞f a⌟ (mk a) := a -- Error, mk is not a constructor
definition inv_4 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞f a⌟ (⌞mk⌟ a) := a -- Error, we cannot use inaccessible annotation around functions in applications
attribute [pattern] mk
definition inv_5 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| ⌞f a⌟ (mk a) := a
definition inv_6 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| (f a) (mk a) := a -- Error, 'a' is being "declared" twice in the pattern
definition inv_7 {A B : Type} (f : A → B) : ∀ (b : B), imf f b → A
| (f a) (mk b) := a -- Typing error, it would also fail when compiling the pattern
definition g_1 : nat → nat → nat
| a a := a -- Error, 'a' is being "declared" twice
definition g_2 (a : nat) : nat → nat → nat
| a b := a
example (a b c : nat) : g_2 a b c = b :=
rfl
inductive vec1 (A : Type) : nat → Type
| nil : vec1 0
| cons : ∀ n, A → vec1 n → vec1 (n+1)
section
open vec1
definition map_1 {A : Type} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
| 0 (nil ⌞A⌟) (nil ⌞A⌟) := nil A
| (n+1) (cons ⌞n⌟ h₁ v₁) (cons ⌞n⌟ h₂ v₂) := cons n (f h₁ h₂) (map_1 v₁ v₂)
definition map_2 {A : Type} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
| 0 (nil ⌞_⌟) (nil ⌞_⌟) := nil A
| (n+1) (cons ⌞_⌟ h₁ v₁) (cons ⌞_⌟ h₂ v₂) := cons n (f h₁ h₂) (map_2 v₁ v₂)
/- In map_3, we use the inaccessible terms to avoid pattern/matching on the first argument -/
definition map_3 {A : Type} (f : A → A → A) : Π {n}, vec1 A n → vec1 A n → vec1 A n
| ⌞_⌟ (nil ⌞_⌟) (nil ⌞_⌟) := nil A
| ⌞_⌟ (cons n h₁ v₁) (cons ⌞n⌟ h₂ v₂) := cons n (f h₁ h₂) (map_3 v₁ v₂)
end
inductive vec2 (A : Type) : nat → Type
| nil {} : vec2 0
| cons : ∀ {n}, A → vec2 n → vec2 (n+1)
section
open vec2
definition map_4 {A : Type} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
| 0 nil nil := nil
| (n+1) (cons h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_4 v₁ v₂)
definition map_5 {A : Type} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
| ⌞_⌟ nil nil := nil
| ⌞_⌟ (@cons ⌞A⌟ n h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_5 v₁ v₂)
/-
The following variant will be rejected by the new equation compiler.
In Lean2, the second equation is accepted because unassigned metavariables
occurring in patterns become new variables. This feature is too hackish.
-/
definition map_6 {A : Type} (f : A → A → A) : Π {n}, vec2 A n → vec2 A n → vec2 A n
| ⌞_⌟ nil nil := nil
| ⌞_⌟ (cons h₁ v₁) (cons h₂ v₂) := cons (f h₁ h₂) (map_6 v₁ v₂)
end

17
tests/lean/inaccessible.lean.expected.out Normal file
View file

@ -0,0 +1,17 @@
inaccessible.lean:13:9: error: invalid argument, it is not a constructor, variable, nor it is marked as an inaccessible pattern
mk a
in the following equation left-hand-side
inv_3 ⌞f a⌟ (mk a)
inaccessible.lean:16:10: error: invalid inaccessible annotation, it cannot be used around functions in applications
inaccessible.lean:24:12: error: invalid pattern, 'a' already appeared in this pattern
inaccessible.lean:27:9: error: type mismatch at application
inv_7 (f_1 a) (mk b)
term
mk b
has type
imf f (f b)
but is expected to have type
imf f (f_1 a)
The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
f a b
inaccessible.lean:30:4: error: invalid pattern, 'a' already appeared in this pattern

4
tests/lean/run/eq2.lean
View file

@ -1,5 +1,5 @@
definition symm {A : Type} : Π {a b : A}, a = b → b = a
| a a rfl := rfl
| a ⌞a⌟ rfl := rfl
definition trans {A : Type} : Π {a b c : A}, a = b → b = c → a = c
| a a a rfl rfl := rfl
| a ⌞a⌟ ⌞a⌟ rfl rfl := rfl