Tail recursive implementations for List
definitions. #
Many of the proofs require theorems about Array
,
so these are in a separate file to minimize imports.
If you import Init.Data.List.Basic
but do not import this file,
then at runtime you will get non-tail recursive versions of the following definitions.
Basic List
operations. #
The following operations are already tail-recursive, and do not need @[csimp]
replacements:
get
, foldl
, beq
, isEqv
, reverse
, elem
(and hence contains
), drop
, dropWhile
,
partition
, isPrefixOf
, isPrefixOf?
, find?
, findSome?
, lookup
, any
(and hence or
),
all
(and hence and
) , range
, eraseDups
, eraseReps
, span
, splitBy
.
The following operations are still missing @[csimp]
replacements:
concat
, zipWithAll
.
The following operations are not recursive to begin with
(or are defined in terms of recursive primitives):
isEmpty
, isSuffixOf
, isSuffixOf?
, rotateLeft
, rotateRight
, insert
, zip
, enum
,
min?
, max?
, and removeAll
.
The following operations were already given @[csimp]
replacements in Init/Data/List/Basic.lean
:
length
, map
, filter
, replicate
, leftPad
, unzip
, range'
, iota
, intersperse
.
The following operations are given @[csimp]
replacements below:
set
, filterMap
, foldr
, append
, bind
, join
,
take
, takeWhile
, dropLast
, replace
, modify
, insertIdx
, erase
, eraseIdx
, zipWith
,
enumFrom
, and intercalate
.
set #
Replaces the value at (zero-based) index n
in l
with a
. If the index is out of bounds, then
the list is returned unmodified.
This is a tail-recursive version of List.set
that's used at runtime.
Examples:
["water", "coffee", "soda", "juice"].set 1 "tea" = ["water", "tea", "soda", "juice"]
["water", "coffee", "soda", "juice"].set 4 "tea" = ["water", "coffee", "soda", "juice"]
Equations
Instances For
filterMap #
Applies a function that returns an Option
to each element of a list, collecting the non-none
values.
O(|l|)
. This is a tail-recursive version of List.filterMap
, used at runtime.
Example:
#eval [1, 2, 5, 2, 7, 7].filterMapTR fun x =>
if x > 2 then some (2 * x) else none
[10, 14, 14]
Equations
Instances For
foldr #
Folds a function over a list from the right, accumulating a value starting with init
. The
accumulated value is combined with the each element of the list in reverse order, using f
.
O(|l|)
. This is the tail-recursive replacement for List.foldr
in runtime code.
Examples:
[a, b, c].foldrTR f init = f a (f b (f c init))
[1, 2, 3].foldrTR (toString · ++ ·) "" = "123"
[1, 2, 3].foldrTR (s!"({·} {·})") "!" = "(1 (2 (3 !)))"
Equations
Instances For
flatMap #
Applies a function that returns a list to each element of a list, and concatenates the resulting lists.
This is the tail-recursive version of List.flatMap
that's used at runtime.
Examples:
[2, 3, 2].flatMapTR List.range = [0, 1, 0, 1, 2, 0, 1]
["red", "blue"].flatMapTR String.toList = ['r', 'e', 'd', 'b', 'l', 'u', 'e']
Equations
Instances For
flatten #
Concatenates a list of lists into a single list, preserving the order of the elements.
O(|flatten L|)
. This is a tail-recursive version of List.flatten
, used in runtime code.
Examples:
[["a"], ["b", "c"]].flattenTR = ["a", "b", "c"]
[["a"], [], ["b", "c"], ["d", "e", "f"]].flattenTR = ["a", "b", "c", "d", "e", "f"]
Equations
Instances For
Sublists #
take #
Extracts the first n
elements of xs
, or the whole list if n
is greater than xs.length
.
O(min n |xs|)
. This is a tail-recursive version of List.take
, used at runtime.
Examples:
[a, b, c, d, e].takeTR 0 = []
[a, b, c, d, e].takeTR 3 = [a, b, c]
[a, b, c, d, e].takeTR 6 = [a, b, c, d, e]
Equations
Instances For
takeWhile #
Returns the longest initial segment of xs
for which p
returns true.
O(|xs|)
. This is a tail-recursive version of List.take
, used at runtime.
Examples:
[7, 6, 4, 8].takeWhileTR (· > 5) = [7, 6]
[7, 6, 6, 5].takeWhileTR (· > 5) = [7, 6, 6]
[7, 6, 6, 8].takeWhileTR (· > 5) = [7, 6, 6, 8]
Equations
Instances For
dropLast #
Removes the last element of the list, if one exists.
This is a tail-recursive version of List.dropLast
, used at runtime.
Examples:
[].dropLastTR = []
["tea"].dropLastTR = []
["tea", "coffee", "juice"].dropLastTR = ["tea", "coffee"]
Equations
Instances For
Finding elements #
Manipulating elements #
replace #
Replaces the first element of the list l
that is equal to a
with b
. If no element is equal to
a
, then the list is returned unchanged.
O(|l|)
. This is a tail-recursive version of List.replace
that's used in runtime code.
Examples:
[1, 4, 2, 3, 3, 7].replaceTR 3 6 = [1, 4, 2, 6, 3, 7]
[1, 4, 2, 3, 3, 7].replaceTR 5 6 = [1, 4, 2, 3, 3, 7]
Equations
Instances For
modify #
Replaces the element at the given index, if it exists, with the result of applying f
to it.
This is a tail-recursive version of List.modify
.
Examples:
[1, 2, 3].modifyTR 0 (· * 10) = [10, 2, 3]
[1, 2, 3].modifyTR 2 (· * 10) = [1, 2, 30]
[1, 2, 3].modifyTR 3 (· * 10) = [1, 2, 3]
Equations
Instances For
insertIdx #
Inserts an element into a list at the specified index. If the index is greater than the length of the list, then the list is returned unmodified.
In other words, the new element is inserted into the list l
after the first i
elements of l
.
This is a tail-recursive version of List.insertIdx
, used at runtime.
Examples:
["tues", "thur", "sat"].insertIdxTR 1 "wed" = ["tues", "wed", "thur", "sat"]
["tues", "thur", "sat"].insertIdxTR 2 "wed" = ["tues", "thur", "wed", "sat"]
["tues", "thur", "sat"].insertIdxTR 3 "wed" = ["tues", "thur", "sat", "wed"]
["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]
Equations
Instances For
Auxiliary for insertIdxTR
: insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
.
Equations
Instances For
erase #
Removes the first occurrence of a
from l
. If a
does not occur in l
, the list is returned
unmodified.
O(|l|)
.
This is a tail-recursive version of List.erase
, used in runtime code.
Examples:
Equations
Instances For
Auxiliary for eraseTR
: eraseTR.go l a xs acc = acc.toList ++ erase xs a
,
unless a
is not present in which case it returns l
Equations
Instances For
Removes the first element of a list for which p
returns true
. If no element satisfies p
, then
the list is returned unchanged.
This is a tail-recursive version of eraseP
, used at runtime.
Examples:
[2, 1, 2, 1, 3, 4].erasePTR (· < 2) = [2, 2, 1, 3, 4]
[2, 1, 2, 1, 3, 4].erasePTR (· > 2) = [2, 1, 2, 1, 4]
[2, 1, 2, 1, 3, 4].erasePTR (· > 8) = [2, 1, 2, 1, 3, 4]
Equations
Instances For
Auxiliary for erasePTR
: erasePTR.go p l xs acc = acc.toList ++ eraseP p xs
,
unless xs
does not contain any elements satisfying p
, where it returns l
.
Equations
Instances For
eraseIdx #
Removes the element at the specified index. If the index is out of bounds, the list is returned unmodified.
O(i)
.
This is a tail-recursive version of List.eraseIdx
, used at runtime.
Examples:
[0, 1, 2, 3, 4].eraseIdxTR 0 = [1, 2, 3, 4]
[0, 1, 2, 3, 4].eraseIdxTR 1 = [0, 2, 3, 4]
[0, 1, 2, 3, 4].eraseIdxTR 5 = [0, 1, 2, 3, 4]
Equations
Instances For
Auxiliary for eraseIdxTR
: eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a
,
unless a
is not present in which case it returns l
Equations
Instances For
Zippers #
zipWith #
Applies a function to the corresponding elements of two lists, stopping at the end of the shorter list.
O(min |xs| |ys|)
. This is a tail-recursive version of List.zipWith
that's used at runtime.
Examples:
[1, 2].zipWithTR (· + ·) [5, 6] = [6, 8]
[1, 2, 3].zipWithTR (· + ·) [5, 6, 10] = [6, 8, 13]
[].zipWithTR (· + ·) [5, 6] = []
[x₁, x₂, x₃].zipWithTR f [y₁, y₂, y₃, y₄] = [f x₁ y₁, f x₂ y₂, f x₃ y₃]
Equations
Instances For
Ranges and enumeration #
zipIdx #
Pairs each element of a list with its index, optionally starting from an index other than 0
.
O(|l|)
. This is a tail-recursive version of List.zipIdx
that's used at runtime.
Examples:
Equations
Instances For
enumFrom #
Tail recursive version of List.enumFrom
.
Equations
Instances For
Other list operations #
intercalate #
Alternates the lists in xs
with the separator sep
.
This is a tail-recursive version of List.intercalate
used at runtime.
Examples:
List.intercalateTR sep [] = []
List.intercalateTR sep [a] = a
List.intercalateTR sep [a, b] = a ++ sep ++ b
List.intercalateTR sep [a, b, c] = a ++ sep ++ b ++ sep ++ c
Equations
Instances For
Auxiliary for intercalateTR
:
intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)