From 30f4b2f2ddc771a8763f70a4a7bdc337e2e2b1ca Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 5 Jul 2017 12:35:44 +0200 Subject: [PATCH] refactor(library): `list.taken/dropn` ~> `list.take/drop` --- library/data/bitvec.lean | 4 ++-- library/data/buffer.lean | 12 +++++----- library/data/buffer/parser.lean | 4 ++-- library/data/vector.lean | 12 +++++----- library/init/data/array/slice.lean | 8 +++---- library/init/data/list/basic.lean | 8 +++---- library/init/data/list/instances.lean | 8 +++---- library/init/data/list/lemmas.lean | 22 +++++++++---------- library/init/data/string/basic.lean | 4 ++-- library/init/meta/coinductive_predicates.lean | 2 +- library/init/native/default.lean | 2 +- tests/lean/run/mk_byte.lean | 4 ++-- 12 files changed, 45 insertions(+), 45 deletions(-) diff --git a/library/data/bitvec.lean b/library/data/bitvec.lean index 8f1d37243e..0b19b54b88 100644 --- a/library/data/bitvec.lean +++ b/library/data/bitvec.lean @@ -36,7 +36,7 @@ section shift def shl (x : bitvec n) (i : ℕ) : bitvec n := bitvec.cong (by simp) $ - dropn i x ++ₜ repeat ff (min n i) + drop i x ++ₜ repeat ff (min n i) def fill_shr (x : bitvec n) (i : ℕ) (fill : bool) : bitvec n := bitvec.cong @@ -47,7 +47,7 @@ section shift { have h₁ := le_of_not_ge h, rw [min_eq_left h₁, sub_eq_zero_of_le h₁, min_zero_left, add_zero] } end $ - repeat fill (min n i) ++ₜ taken (n-i) x + repeat fill (min n i) ++ₜ take (n-i) x -- unsigned shift right def ushr (x : bitvec n) (i : ℕ) : bitvec n := diff --git a/library/data/buffer.lean b/library/data/buffer.lean index b709174e23..c822ebc5ef 100644 --- a/library/data/buffer.lean +++ b/library/data/buffer.lean @@ -90,14 +90,14 @@ def foldl : buffer α → β → (α → β → β) → β def rev_iterate : Π (b : buffer α), β → (fin b.size → α → β → β) → β | ⟨_, a⟩ b f := a.rev_iterate b f -def taken (b : buffer α) (n : nat) : buffer α := -if h : n ≤ b.size then ⟨n, b.to_array.taken n h⟩ else b +def take (b : buffer α) (n : nat) : buffer α := +if h : n ≤ b.size then ⟨n, b.to_array.take n h⟩ else b -def taken_right (b : buffer α) (n : nat) : buffer α := -if h : n ≤ b.size then ⟨n, b.to_array.taken_right n h⟩ else b +def take_right (b : buffer α) (n : nat) : buffer α := +if h : n ≤ b.size then ⟨n, b.to_array.take_right n h⟩ else b -def dropn (b : buffer α) (n : nat) : buffer α := -if h : n ≤ b.size then ⟨_, b.to_array.dropn n h⟩ else b +def drop (b : buffer α) (n : nat) : buffer α := +if h : n ≤ b.size then ⟨_, b.to_array.drop n h⟩ else b def reverse (b : buffer α) : buffer α := ⟨b.size, b.to_array.reverse⟩ diff --git a/library/data/buffer/parser.lean b/library/data/buffer/parser.lean index f7baa40777..411d586fef 100644 --- a/library/data/buffer/parser.lean +++ b/library/data/buffer/parser.lean @@ -185,8 +185,8 @@ private def make_monospaced : char → char | c := c def mk_error_msg (input : char_buffer) (pos : ℕ) (expected : dlist string) : char_buffer := -let left_ctx := (input.taken pos).taken_right 10, - right_ctx := (input.dropn pos).taken 10 in +let left_ctx := (input.take pos).take_right 10, + right_ctx := (input.drop pos).take 10 in left_ctx.map make_monospaced ++ right_ctx.map make_monospaced ++ "\n".to_char_buffer ++ left_ctx.map (λ _, ' ') ++ "^\n".to_char_buffer ++ "\n".to_char_buffer ++ diff --git a/library/data/vector.lean b/library/data/vector.lean index df502d36ef..b835dd5bc6 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -76,11 +76,11 @@ def map₂ (f : α → β → φ) : vector α n → vector β n → vector φ n def repeat (a : α) (n : ℕ) : vector α n := ⟨ list.repeat a n, list.length_repeat a n ⟩ -def dropn (i : ℕ) : vector α n → vector α (n - i) -| ⟨l, p⟩ := ⟨ list.dropn i l, by simp * ⟩ +def drop (i : ℕ) : vector α n → vector α (n - i) +| ⟨l, p⟩ := ⟨ list.drop i l, by simp * ⟩ -def taken (i : ℕ) : vector α n → vector α (min i n) -| ⟨l, p⟩ := ⟨ list.taken i l, by simp * ⟩ +def take (i : ℕ) : vector α n → vector α (min i n) +| ⟨l, p⟩ := ⟨ list.take i l, by simp * ⟩ def remove_nth (i : fin n) : vector α n → vector α (n - 1) | ⟨l, p⟩ := ⟨ list.remove_nth l i.1, by rw[l.length_remove_nth i.1]; rw p; exact i.2 ⟩ @@ -126,10 +126,10 @@ begin cases v, reflexivity end @[simp] lemma to_list_append {n m : nat} (v : vector α n) (w : vector α m) : to_list (append v w) = to_list v ++ to_list w := begin cases v, cases w, reflexivity end -@[simp] lemma to_list_dropn {n m : ℕ} (v : vector α m) : to_list (dropn n v) = list.dropn n (to_list v) := +@[simp] lemma to_list_drop {n m : ℕ} (v : vector α m) : to_list (drop n v) = list.drop n (to_list v) := begin cases v, reflexivity end -@[simp] lemma to_list_taken {n m : ℕ} (v : vector α m) : to_list (taken n v) = list.taken n (to_list v) := +@[simp] lemma to_list_take {n m : ℕ} (v : vector α m) : to_list (take n v) = list.take n (to_list v) := begin cases v, reflexivity end end vector diff --git a/library/init/data/array/slice.lean b/library/init/data/array/slice.lean index a22e18c625..05e73806df 100644 --- a/library/init/data/array/slice.lean +++ b/library/init/data/array/slice.lean @@ -16,18 +16,18 @@ def slice (a : array α n) (k l : nat) (h₁ : k ≤ l) (h₂ : l ≤ n) : array ... = l : nat.sub_add_cancel h₁ ... ≤ n : h₂⟩ ⟩ -def taken (a : array α n) (m : nat) (h : m ≤ n) : array α m := +def take (a : array α n) (m : nat) (h : m ≤ n) : array α m := cast (by simp) $ a.slice 0 m (nat.zero_le _) h -def dropn (a : array α n) (m : nat) (h : m ≤ n) : array α (n-m) := +def drop (a : array α n) (m : nat) (h : m ≤ n) : array α (n-m) := a.slice m n h (le_refl _) private lemma sub_sub_cancel (m n : ℕ) (h : m ≤ n) : n - (n - m) = m := calc n - (n - m) = (n - m) + m - (n - m) : by rw nat.sub_add_cancel; assumption ... = m : nat.add_sub_cancel_left _ _ -def taken_right (a : array α n) (m : nat) (h : m ≤ n) : array α m := -cast (by simp [*, sub_sub_cancel]) $ a.dropn (n - m) (nat.sub_le _ _) +def take_right (a : array α n) (m : nat) (h : m ≤ n) : array α m := +cast (by simp [*, sub_sub_cancel]) $ a.drop (n - m) (nat.sub_le _ _) def reverse (a : array α n) : array α n := ⟨ λ ⟨ i, hi ⟩, a.read ⟨ n - (i + 1), diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 341c4a0d54..adcf87b980 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -182,15 +182,15 @@ def index_of [decidable_eq α] (a : α) : list α → nat := find_index (eq a) def indexes_of [decidable_eq α] (a : α) : list α → list nat := find_indexes (eq a) -def dropn : ℕ → list α → list α +def drop : ℕ → list α → list α | 0 a := a | (succ n) [] := [] -| (succ n) (x::r) := dropn n r +| (succ n) (x::r) := drop n r -def taken : ℕ → list α → list α +def take : ℕ → list α → list α | 0 a := [] | (succ n) [] := [] -| (succ n) (x :: r) := x :: taken n r +| (succ n) (x :: r) := x :: take n r def split_at : ℕ → list α → list α × list α | 0 a := ([], a) diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index 91153bae85..fe47146b5f 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.lean @@ -113,13 +113,13 @@ instance decidable_suffix [decidable_eq α] : ∀ (l₁ l₂ : list α), decidab append_ne_nil_of_ne_nil_right _ _ $ λh, list.no_confusion h | l₁ l₂ := let len1 := length l₁, len2 := length l₂ in if hl : len1 ≤ len2 then - if he : dropn (len2 - len1) l₂ = l₁ then is_true $ - ⟨taken (len2 - len1) l₂, by rw [-he, taken_append_dropn]⟩ + if he : drop (len2 - len1) l₂ = l₁ then is_true $ + ⟨take (len2 - len1) l₂, by rw [-he, take_append_drop]⟩ else is_false $ - suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → dropn (length l₂ - length l₁) l₂ = l₁, + suffices length l₁ ≤ length l₂ → l₁ <:+ l₂ → drop (length l₂ - length l₁) l₂ = l₁, from λsuf, he (this hl suf), λ hl ⟨t, te⟩, and.right $ - append_right_inj (eq.trans (taken_append_dropn (length l₂ - length l₁) l₂) te.symm) $ + append_right_inj (eq.trans (take_append_drop (length l₂ - length l₁) l₂) te.symm) $ by simp; exact nat.sub_sub_self hl else is_false $ λ⟨t, te⟩, hl $ show length l₁ ≤ length l₂, by rw [-te, length_append]; apply nat.le_add_left diff --git a/library/init/data/list/lemmas.lean b/library/init/data/list/lemmas.lean index b1dd824a7b..c8ce3f5eb4 100644 --- a/library/init/data/list/lemmas.lean +++ b/library/init/data/list/lemmas.lean @@ -57,19 +57,19 @@ by {induction l, contradiction, simp} @[simp] lemma length_tail (l : list α) : length (tail l) = length l - 1 := by cases l; refl -/- repeat taken dropn -/ +/- repeat take drop -/ -attribute [simp] repeat taken dropn +attribute [simp] repeat take drop -@[simp] lemma split_at_eq_taken_dropn : ∀ (n : ℕ) (l : list α), split_at n l = (taken n l, dropn n l) +@[simp] lemma split_at_eq_take_drop : ∀ (n : ℕ) (l : list α), split_at n l = (take n l, drop n l) | 0 a := rfl | (succ n) [] := rfl -| (succ n) (x :: xs) := by simp [split_at, split_at_eq_taken_dropn n xs] +| (succ n) (x :: xs) := by simp [split_at, split_at_eq_take_drop n xs] -@[simp] lemma taken_append_dropn : ∀ (n : ℕ) (l : list α), taken n l ++ dropn n l = l +@[simp] lemma take_append_drop : ∀ (n : ℕ) (l : list α), take n l ++ drop n l = l | 0 a := rfl | (succ n) [] := rfl -| (succ n) (x :: xs) := by simp [taken_append_dropn n xs] +| (succ n) (x :: xs) := by simp [take_append_drop n xs] /- length -/ @@ -94,18 +94,18 @@ lemma ne_nil_of_length_eq_succ {l : list α} : ∀ {n : nat}, length l = succ n by induction l; intros; contradiction -- TODO(Leo): cleanup proof after arith dec proc -@[simp] lemma length_taken : ∀ (i : ℕ) (l : list α), length (taken i l) = min i (length l) +@[simp] lemma length_take : ∀ (i : ℕ) (l : list α), length (take i l) = min i (length l) | 0 l := by simp | (succ n) [] := by simp | (succ n) (a::l) := begin simp [*, nat.min_succ_succ, add_one_eq_succ] end -- TODO(Leo): cleanup proof after arith dec proc -@[simp] lemma length_dropn : ∀ (i : ℕ) (l : list α), length (dropn i l) = length l - i +@[simp] lemma length_drop : ∀ (i : ℕ) (l : list α), length (drop i l) = length l - i | 0 l := rfl | (succ i) [] := eq.symm (nat.zero_sub_eq_zero (succ i)) | (succ i) (x::l) := calc - length (dropn (succ i) (x::l)) - = length l - i : length_dropn i l + length (drop (succ i) (x::l)) + = length l - i : length_drop i l ... = succ (length l) - succ i : nat.sub_eq_succ_sub_succ (length l) i lemma length_remove_nth : ∀ (l : list α) (i : ℕ), i < length l → length (remove_nth l i) = length l - 1 @@ -627,7 +627,7 @@ by simp [scanr] /- filter, partition, take_while, drop_while, span -/ -attribute [simp] repeat taken dropn +attribute [simp] repeat take drop @[simp] lemma partition_eq_filter_filter (p : α → Prop) [decidable_pred p] : ∀ (l : list α), partition p l = (filter p l, filter (not ∘ p) l) | [] := rfl diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index cc481db1b9..ca7a140cfe 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -48,7 +48,7 @@ def pop_back : string → string | ⟨s⟩ := ⟨s.tail⟩ def popn_back : string → nat → string -| ⟨s⟩ n := ⟨s.dropn n⟩ +| ⟨s⟩ n := ⟨s.drop n⟩ def intercalate (s : string) (ss : list string) : string := (list.intercalate s.to_list (ss.map to_list)).as_string @@ -64,7 +64,7 @@ def back : string → char | ⟨c::cs⟩ := c def backn : string → nat → string -| ⟨s⟩ n := ⟨s.taken n⟩ +| ⟨s⟩ n := ⟨s.take n⟩ def join (l : list string) : string := l.foldl (λ r s, r ++ s) "" diff --git a/library/init/meta/coinductive_predicates.lean b/library/init/meta/coinductive_predicates.lean index ca40c6a583..9f76abf45a 100644 --- a/library/init/meta/coinductive_predicates.lean +++ b/library/init/meta/coinductive_predicates.lean @@ -106,7 +106,7 @@ private meta def elim_gen_sum_aux : nat → expr → list expr → tactic (list meta def elim_gen_sum (n : nat) (e : expr) : tactic (list expr) := do (hs, h') ← elim_gen_sum_aux n e [], gs ← get_goals, - set_goals $ (gs.taken (n+1)).reverse ++ gs.dropn (n+1), + set_goals $ (gs.take (n+1)).reverse ++ gs.drop (n+1), return $ hs.reverse ++ [h'] end tactic diff --git a/library/init/native/default.lean b/library/init/native/default.lean index 260e3c56df..731ffea460 100644 --- a/library/init/native/default.lean +++ b/library/init/native/default.lean @@ -215,7 +215,7 @@ meta def compile_call (head : name) (arity : nat) (args : list ir.expr) : ir_com then mk_call head args else if list.length args < arity then mk_under_sat_call head args - else mk_over_sat_call head (list.taken arity args) (list.dropn arity args) + else mk_over_sat_call head (list.take arity args) (list.drop arity args) meta def mk_object (arity : unsigned) (args : list ir.expr) : ir_compiler ir.expr := let args'' := list.map assert_name args diff --git a/tests/lean/run/mk_byte.lean b/tests/lean/run/mk_byte.lean index 7d8987a0ae..44540aef49 100644 --- a/tests/lean/run/mk_byte.lean +++ b/tests/lean/run/mk_byte.lean @@ -8,12 +8,12 @@ def byte_type := bitvec 8 def mk_byte (a b : bool) (l : bitvec 6) : byte_type := a :: b :: l -- Get the third component -def get_data (byte : byte_type) : bitvec 6 := vector.dropn 2 byte +def get_data (byte : byte_type) : bitvec 6 := vector.drop 2 byte lemma get_data_mk_byte {a b : bool} {l : bitvec 6} : get_data (mk_byte a b l) = l := begin apply vector.eq, unfold mk_byte, unfold get_data, - simp [to_list_dropn, to_list_cons, list.dropn] + simp [to_list_drop, to_list_cons, list.drop] end