From 8a78adc9af30eb6809c3f8c5d0801d25aa6e6b85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Feb 2015 14:51:42 -0800 Subject: [PATCH] feat(library/tactic): add auxiliary object "location" This object will used to specify the scope of application of tactics --- src/library/tactic/location.cpp | 113 ++++++++++++++++++++++++++++++++ src/library/tactic/location.h | 81 +++++++++++++++++++++++ 2 files changed, 194 insertions(+) create mode 100644 src/library/tactic/location.cpp create mode 100644 src/library/tactic/location.h diff --git a/src/library/tactic/location.cpp b/src/library/tactic/location.cpp new file mode 100644 index 000000000..66b7e078e --- /dev/null +++ b/src/library/tactic/location.cpp @@ -0,0 +1,113 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/kernel_serializer.h" +#include "library/tactic/location.h" + +namespace lean { +unsigned occurrence::contains(unsigned occ_idx) const { + switch (m_kind) { + case All: return true; + case Pos: return std::find(m_occs.begin(), m_occs.end(), occ_idx) != m_occs.end(); + case Neg: return std::find(m_occs.begin(), m_occs.end(), occ_idx) == m_occs.end(); + } + lean_unreachable(); +} + +serializer & operator<<(serializer & s, occurrence const & o) { + s << static_cast(o.m_kind); + write_list(s, o.m_occs); + return s; +} + +deserializer & operator>>(deserializer & d, occurrence & o) { + o.m_kind = static_cast(d.read_char()); + o.m_occs = read_list(d); + return d; +} + +location location::mk_hypotheses(buffer const & hs) { + buffer> tmp; + for (name const & h : hs) + tmp.push_back(mk_pair(h, occurrence())); + return location(Hypotheses, occurrence(), to_list(tmp)); +} + +location location::mk_goal_hypotheses(buffer const & hs) { + buffer> tmp; + for (name const & h : hs) + tmp.push_back(mk_pair(h, occurrence())); + return location(GoalHypotheses, occurrence(), to_list(tmp)); +} + +location location::mk_hypotheses_at(buffer const & hs, buffer const & hs_occs) { + lean_assert(hs.size() == hs_occs.size()); + buffer> tmp; + for (unsigned i = 0; i < hs.size(); i++) + tmp.push_back(mk_pair(hs[i], hs_occs[i])); + return location(Hypotheses, occurrence(), to_list(tmp)); +} + +location location::mk_at(occurrence const & g_occs, buffer const & hs, buffer const & hs_occs) { + lean_assert(hs.size() == hs_occs.size()); + buffer> tmp; + for (unsigned i = 0; i < hs.size(); i++) + tmp.push_back(mk_pair(hs[i], hs_occs[i])); + return location(GoalHypotheses, g_occs, to_list(tmp)); +} + +optional location::includes_goal() const { + switch (m_kind) { + case Everywhere: case GoalOnly: case GoalHypotheses: + return optional(m_goal); + case AllHypotheses: case Hypotheses: + return optional(); + } + lean_unreachable(); +} + +optional location::includes_hypothesis(name const & h) const { + switch (m_kind) { + case Everywhere: case AllHypotheses: + return optional(occurrence()); + case GoalOnly: + return optional(); + case Hypotheses: case GoalHypotheses: + for (auto const & p : m_hyps) { + if (p.first == h) + return optional(p.second); + } + return optional(); + } + lean_unreachable(); +} + +void location::get_explicit_hypotheses_names(buffer & r) const { + for (auto const & p : m_hyps) + r.push_back(p.first); +} + +serializer & operator<<(serializer & s, location const & loc) { + s << static_cast(loc.m_kind) << loc.m_goal << length(loc.m_hyps); + for (auto const & p : loc.m_hyps) + s << p.first << p.second; + return s; +} + +deserializer & operator>>(deserializer & d, location & loc) { + loc.m_kind = static_cast(d.read_char()); + d >> loc.m_goal; + unsigned num = d.read_unsigned(); + buffer> tmp; + for (unsigned i = 0; i < num; i++) { + name h; occurrence o; + d >> h >> o; + tmp.emplace_back(h, o); + } + loc.m_hyps = to_list(tmp); + return d; +} +} diff --git a/src/library/tactic/location.h b/src/library/tactic/location.h new file mode 100644 index 000000000..3c5868e58 --- /dev/null +++ b/src/library/tactic/location.h @@ -0,0 +1,81 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/kernel_serializer.h" + +namespace lean { +/* + We can specify the scope of application of some clauses using + "locations". Locations specify goal and/or hypotheses and + "occurrences" inside a given location. The occurrences are + just numeric values and the specify which occurrences of a + term instance are considered by the tactic. + + Examples: + + - rewrite H1 in H at (1, 3) + + says the scope of (rewrite H1) is the hypothesis H, and + only the first and third occurrences of the H1 left-hand-side + will be considered. + + - rewrite H1 in H at -1 + + says the scope of (rewrite H1) is the hypothesis H and all + but the first occurrence of the H1 left-hand-side + will be considered. +*/ + +class occurrence { + enum kind { All, Pos, Neg }; + kind m_kind; + list m_occs; + occurrence(kind k, list const & occs):m_kind(k), m_occs(occs) {} +public: + occurrence():m_kind(All) {} + static occurrence mk_occurrences(buffer const & occs) { return occurrence(Pos, to_list(occs)); } + static occurrence mk_occurrences(list const & occs) { return occurrence(Pos, occs); } + static occurrence mk_except_occurrences(buffer const & occs) { return occurrence(Neg, to_list(occs)); } + static occurrence mk_except_occurrences(list const & occs) { return occurrence(Neg, occs); } + bool is_all() const { return m_kind == All; } + bool is_except() const { return m_kind == Neg; } + /** \brief Return true iff this occurrence object contains the given occurrence index. */ + unsigned contains(unsigned occ_idx) const; + friend serializer & operator<<(serializer & s, occurrence const & o); + friend deserializer & operator>>(deserializer & d, occurrence & o); +}; + +class location { +public: + enum kind { Everywhere, GoalOnly, AllHypotheses, Hypotheses, GoalHypotheses }; +private: + kind m_kind; + occurrence m_goal; + list> m_hyps; + location(kind k, occurrence const & g = occurrence(), + list> const & hs = list>()): + m_kind(k), m_goal(g), m_hyps(hs) {} +public: + location():m_kind(GoalOnly) {} + + static location mk_goal_only() { return location(); } + static location mk_everywhere() { return location(Everywhere); } + static location mk_all_hypotheses() { return location(AllHypotheses); } + static location mk_hypotheses(buffer const & hs); + static location mk_goal_hypotheses(buffer const & hs); + static location mk_goal_at(occurrence const & o) { return location(GoalOnly, o); } + static location mk_hypotheses_at(buffer const & hs, buffer const & occs); + static location mk_at(occurrence const & g_occs, buffer const & hs, buffer const & hs_occs); + + optional includes_goal() const; + optional includes_hypothesis(name const & h) const; + void get_explicit_hypotheses_names(buffer & r) const; + + friend serializer & operator<<(serializer & s, location const & loc); + friend deserializer & operator>>(deserializer & d, location & loc); +}; +}