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

feat(frontends/lean): add multiple_instances command

Browse source 
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
This commit is contained in:
Leonardo de Moura 2014-12-21 17:18:38 -08:00
parent 5efadb09cc
commit d2958044fd
12 changed files with 126 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/algebra/category/basic.hlean
View file

@ -12,6 +12,8 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops
structure category [class] (ob : Type) extends (precategory ob) :=
(iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
multiple_instances [persistent] category
namespace category
variables {ob : Type} {C : category ob} {a b : ob}
include C

2
hott/algebra/precategory/basic.hlean
View file

@ -14,6 +14,8 @@ structure precategory [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
multiple_instances [persistent] precategory
namespace precategory
variables {ob : Type} [C : precategory ob]
variables {a b c d : ob}

2
hott/algebra/precategory/morphism.hlean
View file

@ -16,6 +16,8 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
multiple_instances [persistent] is_iso
definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H
definition section_of (f : a ⟶ b) [H : is_retraction f] : hom b a :=

2
library/algebra/category/basic.lean
View file

@ -15,6 +15,8 @@ structure category [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
multiple_instances [persistent] category
namespace category
variables {ob : Type} [C : category ob]
variables {a b c d : ob}

2
library/algebra/category/morphism.lean
View file

@ -16,6 +16,8 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
multiple_instances [persistent] is_iso
definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H
definition section_of (f : a ⟶ b) [H : is_retraction f] : hom b a :=

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

@ -15,7 +15,7 @@
"alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
"calc_trans" "calc_subst" "calc_refl" "calc_symm"
"infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
"using" "namespace" "instance" "class" "section" "fields" "find_decl"
"using" "namespace" "instance" "class" "multiple_instances" "section" "fields" "find_decl"
"set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
"lean keywords")

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

@ -69,8 +69,24 @@ environment add_class_cmd(parser & p) {
return env;
}
environment multiple_instances_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 'multiple_instances' command, constant expected");
env = mark_multiple_instances(env, c, persistent);
}
if (!found)
throw parser_error("invalid 'multiple_instances' command, at least one identifier expected", p.pos());
return env;
}
void register_class_cmds(cmd_table & r) {
add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
add_cmd(r, cmd_info("class", "add a new class", add_class_cmd));
add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
add_cmd(r, cmd_info("class", "add a new class", add_class_cmd));
add_cmd(r, cmd_info("multiple_instances", "mark that Lean must explore multiple instances of the given class", multiple_instances_cmd));
}
}

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

@ -91,7 +91,7 @@ void init_token_table(token_table & t) {
"import", "inductive", "record", "structure", "module", "universe", "universes",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "find_decl",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl",
"include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
pair<char const *, char const *> aliases[] =

81
src/library/class.cpp
View file

@ -18,15 +18,18 @@ Author: Leonardo de Moura
#endif
namespace lean {
enum class class_entry_kind { ClassCmd, InstanceCmd, MultiCmd };
struct class_entry {
bool m_class_cmd;
name m_class;
name m_instance; // only relevant if m_class_cmd == false
unsigned m_priority; // only relevant if m_class_cmd == false
class_entry():m_class_cmd(false), m_priority(0) {}
explicit class_entry(name const & c):m_class_cmd(true), m_class(c), m_priority(0) {}
class_entry_kind m_cmd_kind;
name m_class;
name m_instance; // only relevant if m_cmd_kind == InstanceCmd
unsigned m_priority; // only relevant if m_cmd_kind == InstanceCmd
class_entry():m_cmd_kind(class_entry_kind::ClassCmd), m_priority(0) {}
explicit class_entry(name const & c):m_cmd_kind(class_entry_kind::ClassCmd), m_class(c), m_priority(0) {}
class_entry(name const & c, name const & i, unsigned p):
m_class_cmd(false), m_class(c), m_instance(i), m_priority(p) {}
m_cmd_kind(class_entry_kind::InstanceCmd), m_class(c), m_instance(i), m_priority(p) {}
class_entry(name const & c, bool):
m_cmd_kind(class_entry_kind::MultiCmd), m_class(c) {}
};
struct class_state {
@ -34,6 +37,7 @@ struct class_state {
typedef name_map<unsigned> instance_priorities;
class_instances m_instances;
instance_priorities m_priorities;
name_set m_multiple; // set of classes that allow multiple solutions/instances
unsigned get_priority(name const & i) const {
if (auto it = m_priorities.find(i))
@ -42,6 +46,10 @@ struct class_state {
return LEAN_INSTANCE_DEFAULT_PRIORITY;
}
bool try_multiple_instances(name const & c) const {
return m_multiple.contains(c);
}
list<name> insert(name const & inst, unsigned priority, list<name> const & insts) const {
if (!insts)
return to_list(inst);
@ -68,6 +76,11 @@ struct class_state {
if (p != LEAN_INSTANCE_DEFAULT_PRIORITY)
m_priorities.insert(i, p);
}
void add_multiple(name const & c) {
add_class(c);
m_multiple.insert(c);
}
};
static name * g_class_name = nullptr;
@ -77,10 +90,17 @@ struct class_config {
typedef class_state state;
typedef class_entry entry;
static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
if (e.m_class_cmd)
switch (e.m_cmd_kind) {
case class_entry_kind::ClassCmd:
s.add_class(e.m_class);
else
break;
case class_entry_kind::InstanceCmd:
s.add_instance(e.m_class, e.m_instance, e.m_priority);
break;
case class_entry_kind::MultiCmd:
s.add_multiple(e.m_class);
break;
}
}
static name const & get_class_name() {
return *g_class_name;
@ -89,25 +109,38 @@ struct class_config {
return *g_key;
}
static void write_entry(serializer & s, entry const & e) {
if (e.m_class_cmd)
s << true << e.m_class;
else
s << false << e.m_class << e.m_instance << e.m_priority;
s << static_cast<char>(e.m_cmd_kind);
switch (e.m_cmd_kind) {
case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
s << e.m_class;
break;
case class_entry_kind::InstanceCmd:
s << e.m_class << e.m_instance << e.m_priority;
break;
}
}
static entry read_entry(deserializer & d) {
entry e;
d >> e.m_class_cmd;
if (e.m_class_cmd)
entry e; char k;
d >> k;
e.m_cmd_kind = static_cast<class_entry_kind>(k);
switch (e.m_cmd_kind) {
case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
d >> e.m_class;
else
break;
case class_entry_kind::InstanceCmd:
d >> e.m_class >> e.m_instance >> e.m_priority;
break;
}
return e;
}
static optional<unsigned> get_fingerprint(entry const & e) {
if (e.m_class_cmd)
switch (e.m_cmd_kind) {
case class_entry_kind::ClassCmd: case class_entry_kind::MultiCmd:
return some(e.m_class.hash());
else
case class_entry_kind::InstanceCmd:
return some(hash(hash(e.m_class.hash(), e.m_instance.hash()), e.m_priority));
}
lean_unreachable();
}
};
@ -167,6 +200,16 @@ environment add_instance(environment const & env, name const & n, bool persisten
return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent);
}
environment mark_multiple_instances(environment const & env, name const & n, bool persistent) {
check_class(env, n);
return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), persistent);
}
bool try_multiple_instances(environment const & env, name const & n) {
class_state const & s = class_ext::get_state(env);
return s.try_multiple_instances(n);
}
bool is_class(environment const & env, name const & c) {
class_state const & s = class_ext::get_state(env);
return s.m_instances.contains(c);

5
src/library/class.h
View file

@ -21,6 +21,11 @@ list<name> get_class_instances(environment const & env, name const & c);
void get_classes(environment const & env, buffer<name> & classes);
name get_class_name(environment const & env, expr const & e);
/** \brief Mark that multiple instances of class \c n must be explored. */
environment mark_multiple_instances(environment const & env, name const & n, bool persistent);
/** \brief Return true iff multiple instances of class \c n must be explored. */
bool try_multiple_instances(environment const & env, name const & n);
/** \brief Return true iff \c type is a class or Pi that produces a class. */
optional<name> is_ext_class(type_checker & tc, expr const & type);

40
src/library/tactic/class_instance_synth.cpp
View file

@ -328,7 +328,9 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & ngen) {
if (!is_ext_class(C->tc(), meta_type)) {
environment const & env = C->env();
auto cls_name_it = is_ext_class(C->tc(), meta_type);
if (!cls_name_it) {
// do nothing, since type is not a class.
return lazy_list<constraints>(constraints());
}
@ -342,7 +344,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
new_cfg.m_discard = false;
new_cfg.m_use_exceptions = false;
auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) {
auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints {
substitution new_s = subst;
// some constraints may have been postponed (example: universe level constraints)
constraints postponed = map(cnstrs,
@ -357,6 +359,13 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
return append(cs, postponed);
};
auto no_solution_fn = [=]() {
if (is_strict)
return lazy_list<constraints>();
else
return lazy_list<constraints>(constraints());
};
unify_result_seq seq1 = unify(env, 1, &c, ngen, substitution(), new_cfg);
if (get_class_unique_class_instances(C->m_ios.get_options())) {
optional<expr> solution;
@ -380,10 +389,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
}
});
if (!solution) {
if (is_strict)
return lazy_list<constraints>();
else
return lazy_list<constraints>(constraints());
return no_solution_fn();
} else {
// some constraints may have been postponed (example: universe level constraints)
return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs));
@ -395,14 +401,22 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context>
// We only keep complete solutions (modulo universe metavariables)
return !has_expr_metavar_relaxed(result);
});
lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
return to_cnstrs_fn(p.first, p.second);
});
if (is_strict) {
return seq3;
if (try_multiple_instances(env, *cls_name_it)) {
lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
return to_cnstrs_fn(p.first, p.second);
});
if (is_strict) {
return seq3;
} else {
// make sure it does not fail by appending empty set of constraints
return append(seq3, lazy_list<constraints>(constraints()));
}
} else {
// make sure it does not fail by appending empty set of constraints
return append(seq3, lazy_list<constraints>(constraints()));
auto p = seq2.pull();
if (!p)
return no_solution_fn();
else
return lazy_list<constraints>(to_cnstrs_fn(p->first.first, p->first.second));
}
}
};

2
tests/lean/run/div2.lean
View file

@ -50,6 +50,8 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom →
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
rec_measure_aux default measure rec_val (succ (measure x)) x
multiple_instances decidable
theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
(rec_val : dom → (dom → codom) → codom)
(rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →