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

refactor(frontends/lean): replace '[opaque]' modifier with 'opaque

Browse source 
definition', '[opaque]' is not a hint, but a kind of definition
This commit is contained in:
Leonardo de Moura 2014-09-19 13:44:44 -07:00
parent 08ccd58eb6
commit 97b1998def
8 changed files with 47 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/int/basic.lean
View file

@ -184,11 +184,11 @@ representative_map_idempotent_equiv proj_rel @proj_congr a
-- ## Definition of ℤ and basic theorems and definitions -- ## Definition of ℤ and basic theorems and definitions
definition int [opaque] [protected] := image proj opaque definition int [protected] := image proj
notation `ℤ` := int notation `ℤ` := int
definition psub [opaque] : ℕ × ℕ → ℤ := fun_image proj opaque definition psub : ℕ × ℕ → ℤ := fun_image proj
definition rep [opaque] : ℤ → ℕ × ℕ := subtype.elt_of opaque definition rep : ℤ → ℕ × ℕ := subtype.elt_of
theorem quotient : is_quotient rel psub rep := theorem quotient : is_quotient rel psub rep :=
representative_map_to_quotient_equiv rel_equiv proj_rel @proj_congr representative_map_to_quotient_equiv rel_equiv proj_rel @proj_congr

2
library/logic/axioms/hilbert.lean
View file

@ -38,7 +38,7 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w)
-- the Hilbert epsilon function -- the Hilbert epsilon function
-- ---------------------------- -- ----------------------------
definition epsilon [opaque] {A : Type} {H : nonempty A} (P : A → Prop) : A := opaque definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A :=
let u : {x : A, (∃y, P y) → P x} := let u : {x : A, (∃y, P y) → P x} :=
strong_indefinite_description P H in strong_indefinite_description P H in
elt_of u elt_of u

2
library/tools/fake_simplifier.lean
View file

@ -4,6 +4,6 @@ open tactic
namespace fake_simplifier namespace fake_simplifier
-- until we have the simplifier... -- until we have the simplifier...
definition simp [opaque] : tactic := apply @sorry opaque definition simp : tactic := apply @sorry
end fake_simplifier end fake_simplifier

2
library/tools/helper_tactics.lean
View file

@ -12,6 +12,6 @@ import .tactic
open tactic open tactic
namespace helper_tactics namespace helper_tactics
definition apply_refl [opaque] := apply @eq.refl definition apply_refl := apply @eq.refl
tactic_hint apply_refl tactic_hint apply_refl
end helper_tactics end helper_tactics

44
library/tools/tactic.lean
View file

@ -18,28 +18,28 @@ namespace tactic
-- uses them when converting Lean expressions into actual tactic objects. -- uses them when converting Lean expressions into actual tactic objects.
-- The bultin 'by' construct triggers the process of converting a -- The bultin 'by' construct triggers the process of converting a
-- a term of type 'tactic' into a tactic that sythesizes a term -- a term of type 'tactic' into a tactic that sythesizes a term
definition and_then [opaque] (t1 t2 : tactic) : tactic := builtin opaque definition and_then (t1 t2 : tactic) : tactic := builtin
definition or_else [opaque] (t1 t2 : tactic) : tactic := builtin opaque definition or_else (t1 t2 : tactic) : tactic := builtin
definition append [opaque] (t1 t2 : tactic) : tactic := builtin opaque definition append (t1 t2 : tactic) : tactic := builtin
definition interleave [opaque] (t1 t2 : tactic) : tactic := builtin opaque definition interleave (t1 t2 : tactic) : tactic := builtin
definition par [opaque] (t1 t2 : tactic) : tactic := builtin opaque definition par (t1 t2 : tactic) : tactic := builtin
definition fixpoint [opaque] (f : tactic → tactic) : tactic := builtin opaque definition fixpoint (f : tactic → tactic) : tactic := builtin
definition repeat [opaque] (t : tactic) : tactic := builtin opaque definition repeat (t : tactic) : tactic := builtin
definition at_most [opaque] (t : tactic) (k : num) : tactic := builtin opaque definition at_most (t : tactic) (k : num) : tactic := builtin
definition discard [opaque] (t : tactic) (k : num) : tactic := builtin opaque definition discard (t : tactic) (k : num) : tactic := builtin
definition focus_at [opaque] (t : tactic) (i : num) : tactic := builtin opaque definition focus_at (t : tactic) (i : num) : tactic := builtin
definition try_for [opaque] (t : tactic) (ms : num) : tactic := builtin opaque definition try_for (t : tactic) (ms : num) : tactic := builtin
definition now [opaque] : tactic := builtin opaque definition now : tactic := builtin
definition assumption [opaque] : tactic := builtin opaque definition assumption : tactic := builtin
definition eassumption [opaque] : tactic := builtin opaque definition eassumption : tactic := builtin
definition state [opaque] : tactic := builtin opaque definition state : tactic := builtin
definition fail [opaque] : tactic := builtin opaque definition fail : tactic := builtin
definition id [opaque] : tactic := builtin opaque definition id : tactic := builtin
definition beta [opaque] : tactic := builtin opaque definition beta : tactic := builtin
definition apply [opaque] {B : Type} (b : B) : tactic := builtin opaque definition apply {B : Type} (b : B) : tactic := builtin
definition unfold [opaque] {B : Type} (b : B) : tactic := builtin opaque definition unfold {B : Type} (b : B) : tactic := builtin
definition exact [opaque] {B : Type} (b : B) : tactic := builtin opaque definition exact {B : Type} (b : B) : tactic := builtin
definition trace [opaque] (s : string) : tactic := builtin opaque definition trace (s : string) : tactic := builtin
precedence `;`:200 precedence `;`:200
infixl ; := and_then infixl ; := and_then
notation `!` t:max := repeat t notation `!` t:max := repeat t

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

@ -8,7 +8,7 @@
(require 'rx) (require 'rx)
(defconst lean-keywords (defconst lean-keywords
'("import" "reducible" "tactic_hint" "definition" "renaming" '("import" "reducible" "tactic_hint" "opaque" "definition" "renaming"
"inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
"hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
"context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment" "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
@ -70,7 +70,7 @@
;; place holder ;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers ;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[opaque\]" "\[visible\]" "\[protected\]" "\[private\]" (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]" "\[private\]"
"\[instance\]" "\[class\]" "\[coercion\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face) "\[instance\]" "\[class\]" "\[coercion\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
;; tactics ;; tactics
(,(rx symbol-start (,(rx symbol-start

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

@ -26,11 +26,11 @@ static name g_llevel_curly(".{");
static name g_rcurly("}"); static name g_rcurly("}");
static name g_colon(":"); static name g_colon(":");
static name g_assign(":="); static name g_assign(":=");
static name g_definition("definition");
static name g_private("[private]"); static name g_private("[private]");
static name g_protected("[protected]"); static name g_protected("[protected]");
static name g_instance("[instance]"); static name g_instance("[instance]");
static name g_coercion("[coercion]"); static name g_coercion("[coercion]");
static name g_opaque("[opaque]");
static name g_reducible("[reducible]"); static name g_reducible("[reducible]");
environment universe_cmd(parser & p) { environment universe_cmd(parser & p) {
@ -164,14 +164,12 @@ environment axiom_cmd(parser & p) {
struct decl_modifiers { struct decl_modifiers {
bool m_is_private; bool m_is_private;
bool m_is_protected; bool m_is_protected;
bool m_is_opaque;
bool m_is_instance; bool m_is_instance;
bool m_is_coercion; bool m_is_coercion;
bool m_is_reducible; bool m_is_reducible;
decl_modifiers() { decl_modifiers() {
m_is_private = false; m_is_private = false;
m_is_protected = false; m_is_protected = false;
m_is_opaque = true;
m_is_instance = false; m_is_instance = false;
m_is_coercion = false; m_is_coercion = false;
m_is_reducible = false; m_is_reducible = false;
@ -185,9 +183,6 @@ struct decl_modifiers {
} else if (p.curr_is_token(g_protected)) { } else if (p.curr_is_token(g_protected)) {
m_is_protected = true; m_is_protected = true;
p.next(); p.next();
} else if (p.curr_is_token(g_opaque)) {
m_is_opaque = true;
p.next();
} else if (p.curr_is_token(g_instance)) { } else if (p.curr_is_token(g_instance)) {
m_is_instance = true; m_is_instance = true;
p.next(); p.next();
@ -214,13 +209,14 @@ static void erase_local_binder_info(buffer<expr> & ps) {
p = update_local(p, binder_info()); p = update_local(p, binder_info());
} }
environment definition_cmd_core(parser & p, bool is_theorem) { environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
auto n_pos = p.pos(); auto n_pos = p.pos();
unsigned start_line = n_pos.first; unsigned start_line = n_pos.first;
name n = p.check_id_next("invalid declaration, identifier expected"); name n = p.check_id_next("invalid declaration, identifier expected");
decl_modifiers modifiers; decl_modifiers modifiers;
name real_n; // real name for this declaration name real_n; // real name for this declaration
modifiers.m_is_opaque = is_theorem; if (is_theorem)
is_opaque = true;
buffer<name> ls_buffer; buffer<name> ls_buffer;
expr type, value; expr type, value;
level_param_names ls; level_param_names ls;
@ -231,8 +227,6 @@ environment definition_cmd_core(parser & p, bool is_theorem) {
// Parse modifiers // Parse modifiers
modifiers.parse(p); modifiers.parse(p);
if (is_theorem && !modifiers.m_is_opaque)
throw exception("invalid theorem declaration, theorems cannot be transparent");
if (p.curr_is_token(g_assign)) { if (p.curr_is_token(g_assign)) {
auto pos = p.pos(); auto pos = p.pos();
@ -321,7 +315,7 @@ environment definition_cmd_core(parser & p, bool is_theorem) {
if (is_theorem) if (is_theorem)
cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value)); cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
else else
cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, modifiers.m_is_opaque)); cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, is_opaque));
if (!modifiers.m_is_private) if (!modifiers.m_is_private)
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type); p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type);
env = module::add(env, *cd); env = module::add(env, *cd);
@ -343,15 +337,15 @@ environment definition_cmd_core(parser & p, bool is_theorem) {
p.add_delayed_theorem(env, real_n, ls, type_as_is, value); p.add_delayed_theorem(env, real_n, ls, type_as_is, value);
env = module::add(env, check(env, mk_axiom(real_n, ls, type))); env = module::add(env, check(env, mk_axiom(real_n, ls, type)));
} else { } else {
std::tie(type, value, new_ls) = p.elaborate_definition(n, type_as_is, value, modifiers.m_is_opaque); std::tie(type, value, new_ls) = p.elaborate_definition(n, type_as_is, value, is_opaque);
new_ls = append(ls, new_ls); new_ls = append(ls, new_ls);
env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value))); env = module::add(env, check(env, mk_theorem(real_n, new_ls, type, value)));
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
} }
} else { } else {
std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, modifiers.m_is_opaque); std::tie(type, value, new_ls) = p.elaborate_definition(n, type, value, is_opaque);
new_ls = append(ls, new_ls); new_ls = append(ls, new_ls);
env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, modifiers.m_is_opaque))); env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, is_opaque)));
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value); p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
} }
if (!modifiers.m_is_private) if (!modifiers.m_is_private)
@ -371,10 +365,14 @@ environment definition_cmd_core(parser & p, bool is_theorem) {
return env; return env;
} }
environment definition_cmd(parser & p) { environment definition_cmd(parser & p) {
return definition_cmd_core(p, false); return definition_cmd_core(p, false, false);
}
environment opaque_definition_cmd(parser & p) {
p.check_token_next(g_definition, "invalid 'opaque' definition, 'definition' expected");
return definition_cmd_core(p, false, true);
} }
environment theorem_cmd(parser & p) { environment theorem_cmd(parser & p) {
return definition_cmd_core(p, true); return definition_cmd_core(p, true, true);
} }
static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("["); static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("[");
@ -419,6 +417,7 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd)); add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd));
add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd)); add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd));
add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); add_cmd(r, cmd_info("definition", "add new definition", definition_cmd));
add_cmd(r, cmd_info("opaque", "add new opaque definition", opaque_definition_cmd));
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd)); add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd)); add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd));
} }

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

@ -77,9 +77,9 @@ token_table init_token_table() {
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", char const * commands[] = {"theorem", "axiom", "variable", "opaque", "definition", "coercion",
"variables", "[persistent]", "[private]", "[protected]", "[visible]", "[instance]", "variables", "[persistent]", "[private]", "[protected]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[opaque]", "[reducible]", "reducible", "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible",
"evaluate", "check", "print", "end", "namespace", "section", "import", "evaluate", "check", "print", "end", "namespace", "section", "import",
"inductive", "record", "renaming", "extends", "structure", "module", "universe", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
"precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",