From 60e320fd79dc6f036dd9687ce49d9c6cbe94e9e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Apr 2015 17:45:58 -0700 Subject: [PATCH] feat(frontends/lean): protected constants and axioms fixes #527 --- src/emacs/lean-syntax.el | 2 +- src/frontends/lean/decl_cmds.cpp | 57 +++++++++++++------ src/frontends/lean/token_table.cpp | 7 ++- src/frontends/lean/tokens.cpp | 8 +++ src/frontends/lean/tokens.h | 2 + tests/lean/protected_consts.lean | 36 ++++++++++++ tests/lean/protected_consts.lean.expected.out | 24 ++++++++ 7 files changed, 114 insertions(+), 22 deletions(-) create mode 100644 tests/lean/protected_consts.lean create mode 100644 tests/lean/protected_consts.lean.expected.out diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index bc4a64ec8..c3d6d36f0 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -12,7 +12,7 @@ "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants" "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "print" "theorem" "example" "abbreviation" - "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes" + "context" "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes" "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 3246096e3..2555d661a 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -119,7 +119,8 @@ static void check_parameter_type(parser & p, name const & n, expr const & type, static environment declare_var(parser & p, environment env, name const & n, level_param_names const & ls, expr const & type, - variable_kind k, optional const & _bi, pos_info const & pos) { + variable_kind k, optional const & _bi, pos_info const & pos, + bool is_protected) { binder_info bi; if (_bi) bi = *_bi; if (k == variable_kind::Parameter || k == variable_kind::Variable) { @@ -151,6 +152,8 @@ static environment declare_var(parser & p, environment env, } if (!ns.is_anonymous()) env = add_expr_alias(env, n, full_n); + if (is_protected) + env = add_protected(env, full_n); return env; } } @@ -179,7 +182,7 @@ static void check_variable_kind(parser & p, variable_kind k) { } } -static environment variable_cmd_core(parser & p, variable_kind k) { +static environment variable_cmd_core(parser & p, variable_kind k, bool is_protected = false) { check_variable_kind(p, k); auto pos = p.pos(); optional bi = parse_binder_info(p, k); @@ -217,7 +220,7 @@ static environment variable_cmd_core(parser & p, variable_kind k) { std::tie(type, new_ls) = p.elaborate_type(type, ctx); if (k == variable_kind::Variable || k == variable_kind::Parameter) update_local_levels(p, new_ls, k == variable_kind::Variable); - return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos); + return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, is_protected); } static environment variable_cmd(parser & p) { return variable_cmd_core(p, variable_kind::Variable); @@ -232,7 +235,7 @@ static environment parameter_cmd(parser & p) { return variable_cmd_core(p, variable_kind::Parameter); } -static environment variables_cmd_core(parser & p, variable_kind k) { +static environment variables_cmd_core(parser & p, variable_kind k, bool is_protected = false) { check_variable_kind(p, k); auto pos = p.pos(); environment env = p.env(); @@ -261,7 +264,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) { if (k == variable_kind::Variable || k == variable_kind::Parameter) update_local_levels(p, new_ls, k == variable_kind::Variable); new_ls = append(ls, new_ls); - env = declare_var(p, env, id, new_ls, new_type, k, bi, pos); + env = declare_var(p, env, id, new_ls, new_type, k, bi, pos, is_protected); } if (p.curr_is_token(get_lparen_tk()) || p.curr_is_token(get_lcurly_tk()) || p.curr_is_token(get_ldcurly_tk()) || p.curr_is_token(get_lbracket_tk())) { @@ -286,6 +289,9 @@ static environment parameters_cmd(parser & p) { static environment constants_cmd(parser & p) { return variables_cmd_core(p, variable_kind::Constant); } +static environment axioms_cmd(parser & p) { + return variables_cmd_core(p, variable_kind::Axiom); +} struct decl_attributes { bool m_def_only; // if true only definition attributes are allowed @@ -1252,25 +1258,39 @@ static environment private_definition_cmd(parser & p) { return definition_cmd_core(p, kind, is_opaque, true, false); } static environment protected_definition_cmd(parser & p) { - def_cmd_kind kind = Definition; - bool is_opaque = false; - if (p.curr_is_token_or_id(get_opaque_tk())) { - is_opaque = true; + if (p.curr_is_token_or_id(get_axiom_tk())) { p.next(); - p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected"); - } else if (p.curr_is_token_or_id(get_definition_tk())) { + return variable_cmd_core(p, variable_kind::Axiom, true); + } else if (p.curr_is_token_or_id(get_constant_tk())) { p.next(); - } else if (p.curr_is_token_or_id(get_abbreviation_tk())) { + return variable_cmd_core(p, variable_kind::Constant, true); + } else if (p.curr_is_token_or_id(get_axioms_tk())) { p.next(); - kind = Abbreviation; - } else if (p.curr_is_token_or_id(get_theorem_tk())) { + return variables_cmd_core(p, variable_kind::Axiom, true); + } else if (p.curr_is_token_or_id(get_constants_tk())) { p.next(); - kind = Theorem; - is_opaque = true; + return variables_cmd_core(p, variable_kind::Constant, true); } else { - throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos()); + def_cmd_kind kind = Definition; + bool is_opaque = false; + if (p.curr_is_token_or_id(get_opaque_tk())) { + is_opaque = true; + p.next(); + p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected"); + } else if (p.curr_is_token_or_id(get_definition_tk())) { + p.next(); + } else if (p.curr_is_token_or_id(get_abbreviation_tk())) { + p.next(); + kind = Abbreviation; + } else if (p.curr_is_token_or_id(get_theorem_tk())) { + p.next(); + kind = Theorem; + is_opaque = true; + } else { + throw parser_error("invalid 'protected' definition/theorem, 'definition' or 'theorem' expected", p.pos()); + } + return definition_cmd_core(p, kind, is_opaque, false, true); } - return definition_cmd_core(p, kind, is_opaque, false, true); } static environment include_cmd_core(parser & p, bool include) { @@ -1338,6 +1358,7 @@ void register_decl_cmds(cmd_table & r) { add_cmd(r, cmd_info("variables", "declare new variables", variables_cmd)); add_cmd(r, cmd_info("parameters", "declare new parameters", parameters_cmd)); add_cmd(r, cmd_info("constants", "declare new constants (aka top-level variables)", constants_cmd)); + add_cmd(r, cmd_info("axioms", "declare new axioms", axioms_cmd)); add_cmd(r, cmd_info("definition", "add new definition", definition_cmd)); add_cmd(r, cmd_info("example", "add new example", example_cmd)); add_cmd(r, cmd_info("opaque", "add new opaque definition", opaque_definition_cmd)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 51f4a0e9c..962c7c59f 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -88,8 +88,8 @@ void init_token_table(token_table & t) { {" aliases[] = diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 9b0a62995..8bc49f978 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -96,6 +96,8 @@ static name * g_theorem = nullptr; static name * g_abbreviation = nullptr; static name * g_axiom = nullptr; static name * g_axioms = nullptr; +static name * g_constant = nullptr; +static name * g_constants = nullptr; static name * g_variable = nullptr; static name * g_variables = nullptr; static name * g_opaque = nullptr; @@ -223,6 +225,8 @@ void initialize_tokens() { g_opaque = new name("opaque"); g_axiom = new name("axiom"); g_axioms = new name("axioms"); + g_constant = new name("constant"); + g_constants = new name("constants"); g_variable = new name("variable"); g_variables = new name("variables"); g_instance = new name("[instance]"); @@ -287,6 +291,8 @@ void finalize_tokens() { delete g_opaque; delete g_axiom; delete g_axioms; + delete g_constant; + delete g_constants; delete g_variables; delete g_variable; delete g_instance; @@ -476,6 +482,8 @@ name const & get_theorem_tk() { return *g_theorem; } name const & get_abbreviation_tk() { return *g_abbreviation; } name const & get_axiom_tk() { return *g_axiom; } name const & get_axioms_tk() { return *g_axioms; } +name const & get_constant_tk() { return *g_constant; } +name const & get_constants_tk() { return *g_constants; } name const & get_variable_tk() { return *g_variable; } name const & get_variables_tk() { return *g_variables; } name const & get_opaque_tk() { return *g_opaque; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 4a1c1ab44..266802511 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -98,6 +98,8 @@ name const & get_theorem_tk(); name const & get_abbreviation_tk(); name const & get_axiom_tk(); name const & get_axioms_tk(); +name const & get_constant_tk(); +name const & get_constants_tk(); name const & get_variable_tk(); name const & get_variables_tk(); name const & get_opaque_tk(); diff --git a/tests/lean/protected_consts.lean b/tests/lean/protected_consts.lean new file mode 100644 index 000000000..b5e15624c --- /dev/null +++ b/tests/lean/protected_consts.lean @@ -0,0 +1,36 @@ +namespace foo + protected axiom A : Prop + axiom B : Prop + protected constant a : A + constant b : B + protected axioms (A₁ A₂ : Prop) + protected constants (a₁ a₂ : A) + axioms (B₁ B₂ : Prop) + constants (b₁ b₂ : B) +end foo + +open foo +check foo.A +check A -- error +check foo.a +check a -- error +check foo.A₁ +check foo.A₂ +check A₁ -- error +check A₂ -- error +check foo.a₁ +check foo.a₂ +check a₁ -- error +check a₂ -- error +check foo.B +check B +check foo.b +check b +check foo.b₁ +check foo.b₂ +check b₁ +check b₂ +check foo.B₁ +check foo.B₂ +check B₁ +check B₂ diff --git a/tests/lean/protected_consts.lean.expected.out b/tests/lean/protected_consts.lean.expected.out new file mode 100644 index 000000000..9a9a9ad8e --- /dev/null +++ b/tests/lean/protected_consts.lean.expected.out @@ -0,0 +1,24 @@ +foo.A : Prop +protected_consts.lean:14:6: error: unknown identifier 'A' +foo.a : foo.A +protected_consts.lean:16:6: error: unknown identifier 'a' +foo.A₁ : Prop +foo.A₂ : Prop +protected_consts.lean:19:6: error: unknown identifier 'A₁' +protected_consts.lean:20:6: error: unknown identifier 'A₂' +foo.a₁ : foo.A +foo.a₂ : foo.A +protected_consts.lean:23:6: error: unknown identifier 'a₁' +protected_consts.lean:24:6: error: unknown identifier 'a₂' +B : Prop +B : Prop +b : B +b : B +b₁ : B +b₂ : B +b₁ : B +b₂ : B +B₁ : Prop +B₂ : Prop +B₁ : Prop +B₂ : Prop