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

feat(frontends/lean): add '[forward]' annotation

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-25 17:44:58 -08:00
parent 2becc0367d
commit d395a54165
7 changed files with 25 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/emacs/lean-syntax.el
View file

@ -56,7 +56,7 @@
"reducible" "irreducible" "semireducible" "quasireducible" "wf"
"whnf" "multiple_instances" "none" "decls" "declarations"
"coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr" "backward"
"no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints"
"forward" "no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints"
"reduce_hints" "unfold_hints" "aliases" "eqv"
"localrefinfo" "recursor"))
"lean modifiers")

20
src/frontends/lean/decl_attributes.cpp
View file

@ -44,6 +44,7 @@ decl_attributes::decl_attributes(bool is_abbrev, bool persistent):
m_simp = false;
m_congr = false;
m_backward = false;
m_forward = false;
m_no_pattern = false;
}
@ -91,8 +92,8 @@ void decl_attributes::parse(parser & p) {
p.next();
} else if (auto it = parse_priority(p)) {
m_priority = *it;
if (!m_is_instance && !m_simp && !m_congr && !m_backward) {
throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]', '[congr], or [backward]'", pos);
if (!m_is_instance && !m_simp && !m_congr && !m_backward && !m_forward) {
throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]', '[simp]', '[congr]', '[backward]' or '[forward]'", pos);
}
} else if (p.curr_is_token(get_parsing_only_tk())) {
if (!m_is_abbrev)
@ -140,6 +141,9 @@ void decl_attributes::parse(parser & p) {
} else if (p.curr_is_token(get_backward_attr_tk())) {
p.next();
m_backward = true;
} else if (p.curr_is_token(get_forward_attr_tk())) {
p.next();
m_forward = true;
} else if (p.curr_is_token(get_no_pattern_attr_tk())) {
p.next();
m_no_pattern = true;
@ -229,6 +233,12 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
else
env = add_backward_rule(env, d, LEAN_BACKWARD_DEFAULT_PRIORITY, m_persistent);
}
if (m_forward) {
if (m_priority)
env = add_hi_lemma(env, d, *m_priority, m_persistent);
else
env = add_hi_lemma(env, d, LEAN_HI_LEMMA_DEFAULT_PRIORITY, m_persistent);
}
if (m_no_pattern) {
env = add_no_pattern(env, d, m_persistent);
}
@ -242,7 +252,8 @@ void decl_attributes::write(serializer & s) const {
<< m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
<< m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_full_hint
<< m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
<< m_simp << m_congr << m_recursor_major_pos << m_priority << m_backward << m_no_pattern;
<< m_simp << m_congr << m_recursor_major_pos << m_priority << m_backward
<< m_forward << m_no_pattern;
write_list(s, m_unfold_hint);
}
@ -251,7 +262,8 @@ void decl_attributes::read(deserializer & d) {
>> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
>> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_full_hint
>> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
>> m_simp >> m_congr >> m_recursor_major_pos >> m_priority >> m_backward >> m_no_pattern;
>> m_simp >> m_congr >> m_recursor_major_pos >> m_priority >> m_backward
>> m_forward >> m_no_pattern;
m_unfold_hint = read_list<unsigned>(d);
}
}

1
src/frontends/lean/decl_attributes.h
View file

@ -32,6 +32,7 @@ class decl_attributes {
bool m_simp;
bool m_congr;
bool m_backward;
bool m_forward;
bool m_no_pattern;
optional<unsigned> m_recursor_major_pos;
optional<unsigned> m_priority;

2
src/frontends/lean/token_table.cpp
View file

@ -112,7 +112,7 @@ void init_token_table(token_table & t) {
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[simp]", "[congr]", "[parsing_only]", "[multiple_instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold_full]", "[unfold_hints]", "[backward]",
"[no_pattern]", "[constructor]", "[unfold", "print",
"[forward]", "[no_pattern]", "[constructor]", "[unfold", "print",
"end", "namespace", "section", "prelude", "help",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",

4
src/frontends/lean/tokens.cpp
View file

@ -122,6 +122,7 @@ static name const * g_simp_attr_tk = nullptr;
static name const * g_congr_attr_tk = nullptr;
static name const * g_backward_attr_tk = nullptr;
static name const * g_no_pattern_attr_tk = nullptr;
static name const * g_forward_attr_tk = nullptr;
static name const * g_recursor_tk = nullptr;
static name const * g_attribute_tk = nullptr;
static name const * g_with_tk = nullptr;
@ -278,6 +279,7 @@ void initialize_tokens() {
g_congr_attr_tk = new name{"[congr]"};
g_backward_attr_tk = new name{"[backward]"};
g_no_pattern_attr_tk = new name{"[no_pattern]"};
g_forward_attr_tk = new name{"[forward]"};
g_recursor_tk = new name{"[recursor"};
g_attribute_tk = new name{"attribute"};
g_with_tk = new name{"with"};
@ -435,6 +437,7 @@ void finalize_tokens() {
delete g_congr_attr_tk;
delete g_backward_attr_tk;
delete g_no_pattern_attr_tk;
delete g_forward_attr_tk;
delete g_recursor_tk;
delete g_attribute_tk;
delete g_with_tk;
@ -591,6 +594,7 @@ name const & get_simp_attr_tk() { return *g_simp_attr_tk; }
name const & get_congr_attr_tk() { return *g_congr_attr_tk; }
name const & get_backward_attr_tk() { return *g_backward_attr_tk; }
name const & get_no_pattern_attr_tk() { return *g_no_pattern_attr_tk; }
name const & get_forward_attr_tk() { return *g_forward_attr_tk; }
name const & get_recursor_tk() { return *g_recursor_tk; }
name const & get_attribute_tk() { return *g_attribute_tk; }
name const & get_with_tk() { return *g_with_tk; }

1
src/frontends/lean/tokens.h
View file

@ -124,6 +124,7 @@ name const & get_simp_attr_tk();
name const & get_congr_attr_tk();
name const & get_backward_attr_tk();
name const & get_no_pattern_attr_tk();
name const & get_forward_attr_tk();
name const & get_recursor_tk();
name const & get_attribute_tk();
name const & get_with_tk();

1
src/frontends/lean/tokens.txt
View file

@ -117,6 +117,7 @@ simp_attr [simp]
congr_attr [congr]
backward_attr [backward]
no_pattern_attr [no_pattern]
forward_attr [forward]
recursor [recursor
attribute attribute
with with