From 48dbd13eef55d42829ab38d0da8b2be1124ed8aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Sep 2014 12:42:22 -0700 Subject: [PATCH] feat(frontends/lean): allow transient classes/instances, i.e., classes/instances that are not saved in .olean files --- library/algebra/relation.lean | 40 ++++++++++------------------- library/hott/fibrant.lean | 16 +++++------- src/frontends/lean/builtin_cmds.cpp | 12 --------- src/frontends/lean/class.cpp | 18 ++++++++----- src/frontends/lean/class.h | 4 +-- src/frontends/lean/util.cpp | 12 +++++++++ src/frontends/lean/util.h | 6 +++++ tests/lean/run/fibrant.lean | 4 +++ 8 files changed, 57 insertions(+), 55 deletions(-) create mode 100644 tests/lean/run/fibrant.lean diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean index 5df8353656..10916f8cf6 100644 --- a/library/algebra/relation.lean +++ b/library/algebra/relation.lean @@ -63,42 +63,30 @@ end is_transitive inductive is_equivalence {T : Type} (R : T → T → Type) : Prop := mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R -namespace is_equivalence +theorem is_equivalence.is_reflexive [instance] + {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R := +is_equivalence.rec (λx y z, x) C - theorem is_reflexive {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R := - is_equivalence.rec (λx y z, x) C - - theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R := - is_equivalence.rec (λx y z, y) C - - theorem is_transitive {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R := - is_equivalence.rec (λx y z, z) C - -end is_equivalence - -instance is_equivalence.is_reflexive -instance is_equivalence.is_symmetric -instance is_equivalence.is_transitive +theorem is_equivalence.is_symmetric [instance] + {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R := +is_equivalence.rec (λx y z, y) C +theorem is_equivalence.is_transitive [instance] + {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R := +is_equivalence.rec (λx y z, z) C -- partial equivalence relation inductive is_PER {T : Type} (R : T → T → Type) : Prop := mk : is_symmetric R → is_transitive R → is_PER R -namespace is_PER +theorem is_PER.is_symmetric [instance] + {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R := +is_PER.rec (λx y, x) C - theorem is_symmetric {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R := - is_PER.rec (λx y, x) C - - theorem is_transitive {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R := +theorem is_PER.is_transitive [instance] + {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R := is_PER.rec (λx y, y) C -end is_PER - -instance is_PER.is_symmetric -instance is_PER.is_transitive - - -- Congruence for unary and binary functions -- ----------------------------------------- diff --git a/library/hott/fibrant.lean b/library/hott/fibrant.lean index 3f5606bf9e..6bf736316f 100644 --- a/library/hott/fibrant.lean +++ b/library/hott/fibrant.lean @@ -22,14 +22,12 @@ axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, axiom pi_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) : fibrant (Πx : A, B x) -instance unit_fibrant -instance nat_fibrant -instance bool_fibrant -instance sum_fibrant -instance prod_fibrant -instance sigma_fibrant -instance pi_fibrant - -theorem test_fibrant : fibrant (nat × (nat ⊎ nat)) := _ +instance [persistent] unit_fibrant +instance [persistent] nat_fibrant +instance [persistent] bool_fibrant +instance [persistent] sum_fibrant +instance [persistent] prod_fibrant +instance [persistent] sigma_fibrant +instance [persistent] pi_fibrant end fibrant diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 5e98c41e96..4c42450b37 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -46,8 +46,6 @@ static name g_renaming("renaming"); static name g_as("as"); static name g_colon(":"); -static name g_persistent("[persistent]"); - environment print_cmd(parser & p) { if (p.curr() == scanner::token_kind::String) { p.regular_stream() << p.get_str_val() << endl; @@ -296,16 +294,6 @@ environment open_export_cmd(parser & p, bool open) { environment open_cmd(parser & p) { return open_export_cmd(p, true); } environment export_cmd(parser & p) { return open_export_cmd(p, false); } -bool parse_persistent(parser & p, bool & persistent) { - if (p.curr_is_token_or_id(g_persistent)) { - p.next(); - persistent = true; - return true; - } else { - return false; - } -} - environment coercion_cmd(parser & p) { bool persistent = false; parse_persistent(p, persistent); diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 07952aaf40..29059c4211 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/kernel_serializer.h" #include "library/opaque_hints.h" #include "frontends/lean/parser.h" +#include "frontends/lean/util.h" #include "frontends/lean/tactic_hint.h" namespace lean { @@ -91,13 +92,13 @@ name get_class_name(environment const & env, expr const & e) { return c_name; } -environment add_class(environment const & env, name const & n) { +environment add_class(environment const & env, name const & n, bool persistent) { check_class(env, n); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(n)); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); } static name g_tmp_prefix = name::mk_internal_unique_name(); -environment add_instance(environment const & env, name const & n) { +environment add_instance(environment const & env, name const & n, bool persistent) { declaration d = env.get(n); expr type = d.get_type(); name_generator ngen(g_tmp_prefix); @@ -109,7 +110,7 @@ environment add_instance(environment const & env, name const & n) { type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); } name c = get_class_name(env, get_app_fn(type)); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n)); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n), persistent); } bool is_class(environment const & env, name const & c) { @@ -124,24 +125,29 @@ list get_class_instances(environment const & env, name const & c) { environment add_instance_cmd(parser & p) { bool found = false; + bool persistent = false; + parse_persistent(p, persistent); environment env = p.env(); while (p.curr_is_identifier()) { found = true; name c = p.check_constant_next("invalid 'class instance' declaration, constant expected"); - env = add_instance(env, c); + env = add_instance(env, c, persistent); } if (!found) throw parser_error("invalid 'class instance' declaration, at least one identifier expected", p.pos()); return env; } + environment add_class_cmd(parser & p) { bool found = false; environment env = p.env(); + bool persistent = false; + parse_persistent(p, persistent); while (p.curr_is_identifier()) { found = true; name c = p.check_constant_next("invalid 'class' declaration, constant expected"); - env = add_class(env, c); + env = add_class(env, c, persistent); } if (!found) throw parser_error("invalid 'class' declaration, at least one identifier expected", p.pos()); diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h index 9ccf9614d4..f220b6e5a3 100644 --- a/src/frontends/lean/class.h +++ b/src/frontends/lean/class.h @@ -12,9 +12,9 @@ Author: Leonardo de Moura namespace lean { /** \brief Add a new 'class' to the environment (if it is not already declared) */ -environment add_class(environment const & env, name const & n); +environment add_class(environment const & env, name const & n, bool persistent = true); /** \brief Add a new 'class instance' to the environment. */ -environment add_instance(environment const & env, name const & n); +environment add_instance(environment const & env, name const & n, bool persistent = true); /** \brief Return true iff \c c was declared with \c add_class . */ bool is_class(environment const & env, name const & c); /** \brief Return the instances of the given class. */ diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index b829aff00c..18487c1ef1 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -17,6 +17,18 @@ Author: Leonardo de Moura #include "frontends/lean/parser.h" namespace lean { +static name g_persistent("[persistent]"); + +bool parse_persistent(parser & p, bool & persistent) { + if (p.curr_is_token_or_id(g_persistent)) { + p.next(); + persistent = true; + return true; + } else { + return false; + } +} + void check_atomic(name const & n) { if (!n.is_atomic()) throw exception(sstream() << "invalid declaration name '" << n << "', identifier must be atomic"); diff --git a/src/frontends/lean/util.h b/src/frontends/lean/util.h index 2c58c8b6f2..9abbe6b9f7 100644 --- a/src/frontends/lean/util.h +++ b/src/frontends/lean/util.h @@ -12,6 +12,12 @@ Author: Leonardo de Moura namespace lean { class parser; typedef std::unique_ptr type_checker_ptr; + +/** \brief Parse optional '[persistent]' modifier. + return true if it is was found, and paremeter \c persistent to true. +*/ +bool parse_persistent(parser & p, bool & persistent); + void check_atomic(name const & n); void check_in_section_or_context(parser const & p); bool is_root_namespace(name const & n); diff --git a/tests/lean/run/fibrant.lean b/tests/lean/run/fibrant.lean new file mode 100644 index 0000000000..f503ff6d2f --- /dev/null +++ b/tests/lean/run/fibrant.lean @@ -0,0 +1,4 @@ +import hott.fibrant +open prod sum fibrant + +theorem test_fibrant : fibrant (nat × (nat ⊎ nat))