feat(library/tactic): add occurrences object

library/init/meta/occurrences.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic init.to_string init.meta.format
+import init.meta.contradiction_tactic init.meta.constructor_tactic
+import init.meta.relation_tactics init.meta.injection_tactic
+
+/-  We can specify the scope of application of some tactics using
+   the following type.
+
+   - all : all occurrences of a given term are considered.
+
+   - pos [1, 3] : only the first and third occurrences of a given
+     term are consiered.
+
+   - neg [2] : all but the second occurrence of a given term
+     are considered. -/
+inductive occurrences :=
+| all
+| pos : list nat → occurrences
+| neg : list nat → occurrences
+
+open occurrences
+
+definition occurrences_is_inhabited [instance] : inhabited occurrences :=
+inhabited.mk all
+
+definition occurrences_to_string : occurrences → string
+| all     := "*"
+| (pos l) := to_string l
+| (neg l) := "-" ++ to_string l
+
+definition occurrences_has_to_string [instance] : has_to_string occurrences :=
+has_to_string.mk occurrences_to_string
+
+meta_definition occurrences_to_format : occurrences → format
+| all     := to_fmt "*"
+| (pos l) := to_fmt l
+| (neg l) := to_fmt "-" ++ to_fmt l
+
+meta_definition occurrences_has_to_format [instance] : has_to_format occurrences :=
+has_to_format.mk occurrences_to_format
+
+open decidable tactic
+
+definition occurrences_has_decidable_eq [instance] : ∀ a b : occurrences, decidable (a = b)
+| all      all      := tt rfl
+| all      (pos l)  := by left >> intron 1 >> contradiction
+| all      (neg l)  := by left >> intron 1 >> contradiction
+| (pos l)  all      := by left >> intron 1 >> contradiction
+| (pos l₁) (pos l₂) := if H : l₁ = l₂
+                       then by right >> get_local "H" >>= subst >> reflexivity
+                       else by left >> intro "_" >>= injection >> contradiction
+| (pos l₁) (neg l₂) := by left >> intron 1 >> contradiction
+| (neg l₁)  all     := by left >> intron 1 >> contradiction
+| (neg l₁) (pos l₂) := by left >> intron 1 >> contradiction
+| (neg l₁) (neg l₂) := if H : l₁ = l₂
+                       then by right >> get_local "H" >>= subst >> reflexivity
+                       else by left >> intro "_" >>= injection >> contradiction

src/library/tactic/CMakeLists.txt

@@ -1,5 +1,5 @@
-add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp
-  revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
+add_library(tactic OBJECT occurrences.cpp tactic_state.cpp
+  intro_tactic.cpp revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp
   app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp
   change_tactic.cpp assert_tactic.cpp apply_tactic.cpp
   fun_info_tactics.cpp congr_lemma_tactics.cpp match_tactic.cpp

src/library/tactic/occurrences.cpp

@@ -0,0 +1,47 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/vm/vm_list.h"
+#include "library/vm/vm_nat.h"
+#include "library/tactic/occurrences.h"
+
+namespace lean {
+bool occurrences::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();
+}
+
+static list<unsigned> to_list_unsigned(vm_obj const & occs) {
+    return to_list<unsigned>(occs, [](vm_obj const & o) { return force_to_unsigned(o, 0); });
+}
+
+/*
+inductive occurrences :=
+| all
+| pos : list nat → occurrences
+| neg : list nat → occurrences  */
+occurrences to_occurrences(vm_obj const & o) {
+    switch (cidx(o)) {
+    case 0: return occurrences();
+    case 1: return occurrences(occurrences::Pos, to_list_unsigned(cfield(o, 0)));
+    case 2: return occurrences(occurrences::Neg, to_list_unsigned(cfield(o, 0)));
+    default: lean_unreachable();
+    }
+}
+
+vm_obj occurrences::to_obj() const {
+    switch (m_kind) {
+    case All: return mk_vm_simple(0);
+    case Pos: return mk_vm_constructor(1, ::lean::to_obj(m_occs));
+    case Neg: return mk_vm_constructor(2, ::lean::to_obj(m_occs));
+    }
+    lean_unreachable();
+}
+}

src/library/tactic/occurrences.h

@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2016 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/vm/vm.h"
+
+namespace lean {
+class occurrences {
+public:
+    enum kind { All, Pos, Neg };
+private:
+    kind           m_kind;
+    list<unsigned> m_occs;
+public:
+    occurrences():m_kind(All) {}
+    occurrences(kind k, list<unsigned> const & occs):m_kind(k), m_occs(occs) {}
+    bool is_all() const { return m_kind == All; }
+    bool is_except() const { return m_kind == Neg; }
+    /** \brief Return true iff this occurrences object contains the given occurrences index. */
+    bool contains(unsigned occ_idx) const;
+
+    bool operator==(occurrences const & o) const { return m_kind == o.m_kind && m_occs == o.m_occs; }
+    bool operator!=(occurrences const & o) const { return !operator==(o); }
+
+    vm_obj to_obj() const;
+};
+
+occurrences to_occurrences(vm_obj const &);
+inline vm_obj to_obj(occurrences const & occs) { return occs.to_obj(); }
+}