From 3e6b4577e2a412cd8505ff4ba5ef38283f483774 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jul 2016 09:49:49 -0400 Subject: [PATCH] feat(library/tactic): add occurrences object --- library/init/meta/occurrences.lean | 62 ++++++++++++++++++++++++++++++ src/library/tactic/CMakeLists.txt | 4 +- src/library/tactic/occurrences.cpp | 47 ++++++++++++++++++++++ src/library/tactic/occurrences.h | 33 ++++++++++++++++ 4 files changed, 144 insertions(+), 2 deletions(-) create mode 100644 library/init/meta/occurrences.lean create mode 100644 src/library/tactic/occurrences.cpp create mode 100644 src/library/tactic/occurrences.h diff --git a/library/init/meta/occurrences.lean b/library/init/meta/occurrences.lean new file mode 100644 index 0000000000..6ef489b50f --- /dev/null +++ b/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 diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 03c4c0e8a9..3eec1782e6 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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 diff --git a/src/library/tactic/occurrences.cpp b/src/library/tactic/occurrences.cpp new file mode 100644 index 0000000000..dc700531c2 --- /dev/null +++ b/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 to_list_unsigned(vm_obj const & occs) { + return to_list(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(); +} +} diff --git a/src/library/tactic/occurrences.h b/src/library/tactic/occurrences.h new file mode 100644 index 0000000000..de12cffb61 --- /dev/null +++ b/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 m_occs; +public: + occurrences():m_kind(All) {} + occurrences(kind k, list 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(); } +}