feat(library/tactic): add auxiliary object "location"

This object will used to specify the scope of application of tactics

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<char>(o.m_kind);
+    write_list<unsigned>(s, o.m_occs);
+    return s;
+}
+
+deserializer & operator>>(deserializer & d, occurrence & o) {
+    o.m_kind = static_cast<occurrence::kind>(d.read_char());
+    o.m_occs = read_list<unsigned>(d);
+    return d;
+}
+
+location location::mk_hypotheses(buffer<name> const & hs) {
+    buffer<pair<name, occurrence>> 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<name> const & hs) {
+    buffer<pair<name, occurrence>> 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<name> const & hs, buffer<occurrence> const & hs_occs) {
+    lean_assert(hs.size() == hs_occs.size());
+    buffer<pair<name, occurrence>> 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<name> const & hs, buffer<occurrence> const & hs_occs) {
+    lean_assert(hs.size() == hs_occs.size());
+    buffer<pair<name, occurrence>> 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<occurrence> location::includes_goal() const {
+    switch (m_kind) {
+    case Everywhere: case GoalOnly: case GoalHypotheses:
+        return optional<occurrence>(m_goal);
+    case AllHypotheses: case Hypotheses:
+        return optional<occurrence>();
+    }
+    lean_unreachable();
+}
+
+optional<occurrence> location::includes_hypothesis(name const & h) const {
+    switch (m_kind) {
+    case Everywhere: case AllHypotheses:
+        return optional<occurrence>(occurrence());
+    case GoalOnly:
+        return optional<occurrence>();
+    case Hypotheses: case GoalHypotheses:
+        for (auto const & p : m_hyps) {
+            if (p.first == h)
+                return optional<occurrence>(p.second);
+        }
+        return optional<occurrence>();
+    }
+    lean_unreachable();
+}
+
+void location::get_explicit_hypotheses_names(buffer<name> & r) const {
+    for (auto const & p : m_hyps)
+        r.push_back(p.first);
+}
+
+serializer & operator<<(serializer & s, location const & loc) {
+    s << static_cast<char>(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<location::kind>(d.read_char());
+    d >> loc.m_goal;
+    unsigned num = d.read_unsigned();
+    buffer<pair<name, occurrence>> 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;
+}
+}

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<unsigned> m_occs;
+    occurrence(kind k, list<unsigned> const & occs):m_kind(k), m_occs(occs) {}
+public:
+    occurrence():m_kind(All) {}
+    static occurrence mk_occurrences(buffer<unsigned> const & occs) { return occurrence(Pos, to_list(occs)); }
+    static occurrence mk_occurrences(list<unsigned> const & occs) { return occurrence(Pos, occs); }
+    static occurrence mk_except_occurrences(buffer<unsigned> const & occs) { return occurrence(Neg, to_list(occs)); }
+    static occurrence mk_except_occurrences(list<unsigned> 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<pair<name, occurrence>> m_hyps;
+    location(kind k, occurrence const & g = occurrence(),
+             list<pair<name, occurrence>> const & hs = list<pair<name, occurrence>>()):
+        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<name> const & hs);
+    static location mk_goal_hypotheses(buffer<name> const & hs);
+    static location mk_goal_at(occurrence const & o) { return location(GoalOnly, o); }
+    static location mk_hypotheses_at(buffer<name> const & hs, buffer<occurrence> const & occs);
+    static location mk_at(occurrence const & g_occs, buffer<name> const & hs, buffer<occurrence> const & hs_occs);
+
+    optional<occurrence> includes_goal() const;
+    optional<occurrence> includes_hypothesis(name const & h) const;
+    void get_explicit_hypotheses_names(buffer<name> & r) const;
+
+    friend serializer & operator<<(serializer & s, location const & loc);
+    friend deserializer & operator>>(deserializer & d, location & loc);
+};
+}