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

feat(frontends/lean): add '[semireducible]' attribute

Browse source 
This commit also renames the elements of reducible_status.
The idea is to use in the C++ implementation the same names used in the
Lean front-end.
This commit is contained in:
Leonardo de Moura 2015-03-03 10:48:36 -08:00
parent b254c78c44
commit 11aad4449b
15 changed files with 91 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -118,7 +118,8 @@
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
"\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[wf\]"
"\[whnf\]" "\[multiple-instances\]"
"\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]"
"\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]" "\[reduce-hints\]"))
. 'font-lock-doc-face)

21
src/frontends/lean/decl_cmds.cpp
View file

@ -290,6 +290,7 @@ struct decl_attributes {
bool m_is_coercion;
bool m_is_reducible;
bool m_is_irreducible;
bool m_is_semireducible;
bool m_is_class;
bool m_is_parsing_only;
bool m_has_multiple_instances;
@ -303,6 +304,7 @@ struct decl_attributes {
m_is_coercion = false;
m_is_reducible = is_abbrev;
m_is_irreducible = false;
m_is_semireducible = false;
m_is_class = false;
m_is_parsing_only = false;
m_has_multiple_instances = false;
@ -361,15 +363,20 @@ struct decl_attributes {
throw parser_error("invalid '[coercion]' attribute, coercions cannot be defined in contexts", pos);
m_is_coercion = true;
} else if (p.curr_is_token(get_reducible_tk())) {
if (m_is_irreducible)
throw parser_error("invalid '[reducible]' attribute, '[irreducible]' was already provided", pos);
if (m_is_irreducible || m_is_semireducible)
throw parser_error("invalid '[reducible]' attribute, '[irreducible]' or '[semireducible]' was already provided", pos);
m_is_reducible = true;
p.next();
} else if (p.curr_is_token(get_irreducible_tk())) {
if (m_is_reducible)
throw parser_error("invalid '[irreducible]' attribute, '[reducible]' was already provided", pos);
if (m_is_reducible || m_is_semireducible)
throw parser_error("invalid '[irreducible]' attribute, '[reducible]' or '[semireducible]' was already provided", pos);
m_is_irreducible = true;
p.next();
} else if (p.curr_is_token(get_semireducible_tk())) {
if (m_is_reducible || m_is_irreducible)
throw parser_error("invalid '[irreducible]' attribute, '[reducible]' or '[irreducible]' was already provided", pos);
m_is_semireducible = true;
p.next();
} else if (p.curr_is_token(get_class_tk())) {
if (m_def_only)
throw parser_error("invalid '[class]' attribute, definitions cannot be marked as classes", pos);
@ -417,9 +424,11 @@ struct decl_attributes {
if (m_is_coercion)
env = add_coercion(env, d, ios, persistent);
if (m_is_reducible)
env = set_reducible(env, d, reducible_status::On, persistent);
env = set_reducible(env, d, reducible_status::Reducible, persistent);
if (m_is_irreducible)
env = set_reducible(env, d, reducible_status::Off, persistent);
env = set_reducible(env, d, reducible_status::Irreducible, persistent);
if (m_is_semireducible)
env = set_reducible(env, d, reducible_status::Semireducible, persistent);
if (m_is_class)
env = add_class(env, d, persistent);
if (m_has_multiple_instances)

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

@ -722,7 +722,7 @@ struct structure_cmd_fn {
rec_on_decl.get_type(), rec_on_decl.get_value(),
opaque);
m_env = module::add(m_env, check(m_env, new_decl));
m_env = set_reducible(m_env, n, reducible_status::On);
m_env = set_reducible(m_env, n, reducible_status::Reducible);
save_def_info(n);
add_alias(n);
}
@ -817,7 +817,7 @@ struct structure_cmd_fn {
declaration coercion_decl = mk_definition(m_env, coercion_name, lnames, coercion_type, coercion_value,
opaque);
m_env = module::add(m_env, check(m_env, coercion_decl));
m_env = set_reducible(m_env, coercion_name, reducible_status::On);
m_env = set_reducible(m_env, coercion_name, reducible_status::Reducible);
save_def_info(coercion_name);
add_alias(coercion_name);
if (!m_private_parents[i]) {

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

@ -87,10 +87,13 @@ void init_token_table(token_table & t) {
{"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
char const * commands[] =
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion", "abbreviation",
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"abbreviation",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print", "end", "namespace", "section", "prelude",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]",
"[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print",
"end", "namespace", "section", "prelude",
"import", "inductive", "record", "structure", "module", "universe", "universes", "local",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",

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

@ -100,6 +100,7 @@ static name * g_priority = nullptr;
static name * g_unfold_c = nullptr;
static name * g_coercion = nullptr;
static name * g_reducible = nullptr;
static name * g_semireducible = nullptr;
static name * g_irreducible = nullptr;
static name * g_parsing_only = nullptr;
static name * g_with = nullptr;
@ -219,6 +220,7 @@ void initialize_tokens() {
g_unfold_c = new name("[unfold-c");
g_coercion = new name("[coercion]");
g_reducible = new name("[reducible]");
g_semireducible = new name("[semireducible]");
g_irreducible = new name("[irreducible]");
g_parsing_only = new name("[parsing-only]");
g_attribute = new name("attribute");
@ -280,6 +282,7 @@ void finalize_tokens() {
delete g_unfold_c;
delete g_coercion;
delete g_reducible;
delete g_semireducible;
delete g_irreducible;
delete g_multiple_instances;
delete g_attribute;
@ -459,6 +462,7 @@ name const & get_priority_tk() { return *g_priority; }
name const & get_unfold_c_tk() { return *g_unfold_c; }
name const & get_coercion_tk() { return *g_coercion; }
name const & get_reducible_tk() { return *g_reducible; }
name const & get_semireducible_tk() { return *g_semireducible; }
name const & get_irreducible_tk() { return *g_irreducible; }
name const & get_multiple_instances_tk() { return *g_multiple_instances; }
name const & get_attribute_tk() { return *g_attribute; }

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

@ -102,6 +102,7 @@ name const & get_priority_tk();
name const & get_unfold_c_tk();
name const & get_coercion_tk();
name const & get_reducible_tk();
name const & get_semireducible_tk();
name const & get_irreducible_tk();
name const & get_multiple_instances_tk();
name const & get_attribute_tk();

4
src/library/definitional/brec_on.cpp
View file

@ -145,7 +145,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow
declaration new_d = mk_definition(env, below_name, blvls, below_type, below_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, below_name, reducible_status::On);
new_env = set_reducible(new_env, below_name, reducible_status::Reducible);
return add_protected(new_env, below_name);
}
@ -330,7 +330,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind)
declaration new_d = mk_definition(env, brec_on_name, blps, brec_on_type, brec_on_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, brec_on_name, reducible_status::On);
new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible);
return add_protected(new_env, brec_on_name);
}

2
src/library/definitional/cases_on.cpp
View file

@ -180,7 +180,7 @@ environment mk_cases_on(environment const & env, name const & n) {
declaration new_d = mk_definition(env, cases_on_name, rec_decl.get_univ_params(), cases_on_type, cases_on_value,
opaque, rec_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, cases_on_name, reducible_status::On);
new_env = set_reducible(new_env, cases_on_name, reducible_status::Reducible);
return add_protected(new_env, cases_on_name);
}
}

4
src/library/definitional/no_confusion.cpp
View file

@ -139,7 +139,7 @@ optional<environment> mk_no_confusion_type(environment const & env, name const &
declaration new_d = mk_definition(env, no_confusion_type_name, lps, no_confusion_type_type, no_confusion_type_value,
opaque, ind_decl.get_module_idx(), use_conv_opt);
environment new_env = module::add(env, check(env, new_d));
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::On);
new_env = set_reducible(new_env, no_confusion_type_name, reducible_status::Reducible);
return some(add_protected(new_env, no_confusion_type_name));
}
@ -274,7 +274,7 @@ environment mk_no_confusion(environment const & env, name const & n) {
declaration new_d = mk_definition(new_env, no_confusion_name, lps, no_confusion_ty, no_confusion_val,
opaque, no_confusion_type_decl.get_module_idx(), use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, no_confusion_name, reducible_status::On);
new_env = set_reducible(new_env, no_confusion_name, reducible_status::Reducible);
return add_protected(new_env, no_confusion_name);
}
}

2
src/library/definitional/projection.cpp
View file

@ -134,7 +134,7 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
declaration new_d = mk_definition(env, proj_name, lvl_params, proj_type, proj_val,
opaque, rec_decl.get_module_idx(), use_conv_opt);
new_env = module::add(new_env, check(new_env, new_d));
new_env = set_reducible(new_env, proj_name, reducible_status::On);
new_env = set_reducible(new_env, proj_name, reducible_status::Reducible);
new_env = add_unfold_c_hint(new_env, proj_name, nparams);
new_env = save_projection_info(new_env, proj_name, inductive::intro_rule_name(intro), nparams, i, inst_implicit);
expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c);

2
src/library/definitional/rec_on.cpp
View file

@ -57,7 +57,7 @@ environment mk_rec_on(environment const & env, name const & n) {
check(env, mk_definition(env, rec_on_name, rec_decl.get_univ_params(),
rec_on_type, rec_on_val,
opaque, rec_decl.get_module_idx(), use_conv_opt)));
new_env = set_reducible(new_env, rec_on_name, reducible_status::On);
new_env = set_reducible(new_env, rec_on_name, reducible_status::Reducible);
return add_protected(new_env, rec_on_name);
}
}

14
src/library/reducible.cpp
View file

@ -17,7 +17,7 @@ namespace lean {
struct reducible_entry {
reducible_status m_status;
name m_name;
reducible_entry():m_status(reducible_status::None) {}
reducible_entry():m_status(reducible_status::Semireducible) {}
reducible_entry(reducible_status s, name const & n):m_status(s), m_name(n) {}
};
@ -27,15 +27,15 @@ struct reducible_state {
void add(reducible_entry const & e) {
switch (e.m_status) {
case reducible_status::On:
case reducible_status::Reducible:
m_reducible_on.insert(e.m_name);
m_reducible_off.erase(e.m_name);
break;
case reducible_status::Off:
case reducible_status::Irreducible:
m_reducible_on.erase(e.m_name);
m_reducible_off.insert(e.m_name);
break;
case reducible_status::None:
case reducible_status::Semireducible:
m_reducible_on.erase(e.m_name);
m_reducible_off.erase(e.m_name);
break;
@ -221,9 +221,9 @@ static int set_reducible(lua_State * L) {
void open_reducible(lua_State * L) {
lua_newtable(L);
SET_ENUM("On", reducible_status::On);
SET_ENUM("Off", reducible_status::Off);
SET_ENUM("None", reducible_status::None);
SET_ENUM("On", reducible_status::Reducible);
SET_ENUM("Off", reducible_status::Irreducible);
SET_ENUM("None", reducible_status::Semireducible);
lua_setglobal(L, "reducible_status");
SET_GLOBAL_FUN(is_reducible_on, "is_reducible_on");
SET_GLOBAL_FUN(is_reducible_off, "is_reducible_off");

2
src/library/reducible.h
View file

@ -10,7 +10,7 @@ Author: Leonardo de Moura
#include "kernel/default_converter.h"
namespace lean {
enum class reducible_status { On, Off, None };
enum class reducible_status { Reducible, Irreducible, Semireducible };
/** \brief Mark the definition named \c n as reducible or not.
The method throws an exception if \c n is

26
tests/lean/red.lean Normal file
View file

@ -0,0 +1,26 @@
constant g : nat → nat
definition f := g
example : f = g := rfl
attribute f [irreducible]
example : f = g := rfl -- Error
example (a : nat) (H : a = g a) : f a = a :=
eq.subst H rfl -- Error
attribute f [semireducible]
example (a : nat) (H : a = g a) : f a = a :=
eq.subst H rfl -- Error
example : f = g := rfl
attribute f [reducible]
example : f = g := rfl
example (a : nat) (H : a = g a) : f a = a :=
eq.subst H rfl

20
tests/lean/red.lean.expected.out Normal file
View file

@ -0,0 +1,20 @@
red.lean:9:19: error: type mismatch at definition '14.1', has type
f = f
but is expected to have type
f = g
red.lean:12:0: error: type mismatch at application
eq.subst H rfl
term
rfl
has type
f ?M_1 = f ?M_1
but is expected to have type
f ?M_1 = a
red.lean:17:0: error: type mismatch at application
eq.subst H rfl
term
rfl
has type
f ?M_1 = f ?M_1
but is expected to have type
f ?M_1 = a