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
, erase
, eraseIdx
, zipWith
,
enumFrom
, and intercalate
.
set #
Tail recursive version of List.set
.
Equations
- l.setTR n a = List.setTR.go l a l n #[]
Instances For
Auxiliary for setTR
: setTR.go l a xs n acc = acc.toList ++ set xs a
,
unless n ≥ l.length
in which case it returns l
Equations
- List.setTR.go l a [] x✝ x = l
- List.setTR.go l a (head :: xs) 0 x = x.toListAppend (a :: xs)
- List.setTR.go l a (x_3 :: xs) n.succ x = List.setTR.go l a xs n (x.push x_3)
Instances For
filterMap #
Tail recursive version of filterMap
.
Equations
- List.filterMapTR f l = List.filterMapTR.go f l #[]
Instances For
Auxiliary for filterMap
: filterMap.go f l = acc.toList ++ filterMap f l
Equations
- List.filterMapTR.go f [] x = x.toList
- List.filterMapTR.go f (a :: as) x = match f a with | none => List.filterMapTR.go f as x | some b => List.filterMapTR.go f as (x.push b)
Instances For
foldr #
Tail recursive version of List.foldr
.
Equations
- List.foldrTR f init l = Array.foldr f init l.toArray
Instances For
flatMap #
Tail recursive version of List.flatMap
.
Equations
- as.flatMapTR f = List.flatMapTR.go f as #[]
Instances For
Auxiliary for flatMap
: flatMap.go f as = acc.toList ++ bind f as
Equations
- List.flatMapTR.go f [] x = x.toList
- List.flatMapTR.go f (a :: as) x = List.flatMapTR.go f as (x ++ f a)
Instances For
flatten #
Sublists #
take #
Tail recursive version of List.take
.
Equations
- List.takeTR n l = List.takeTR.go l l n #[]
Instances For
Auxiliary for take
: take.go l xs n acc = acc.toList ++ take n xs
,
unless n ≥ xs.length
in which case it returns l
.
Equations
- List.takeTR.go l [] x✝ x = l
- List.takeTR.go l (head :: xs) 0 x = x.toList
- List.takeTR.go l (x_3 :: xs) n.succ x = List.takeTR.go l xs n (x.push x_3)
Instances For
takeWhile #
Tail recursive version of List.takeWhile
.
Equations
- List.takeWhileTR p l = List.takeWhileTR.go p l l #[]
Instances For
Auxiliary for takeWhile
: takeWhile.go p l xs acc = acc.toList ++ takeWhile p xs
,
unless no element satisfying p
is found in xs
in which case it returns l
.
Equations
- List.takeWhileTR.go p l [] x = l
- List.takeWhileTR.go p l (a :: as) x = bif p a then List.takeWhileTR.go p l as (x.push a) else x.toList
Instances For
dropLast #
Manipulating elements #
replace #
Tail recursive version of List.replace
.
Equations
- l.replaceTR b c = List.replaceTR.go l b c l #[]
Instances For
Auxiliary for replace
: replace.go l b c xs acc = acc.toList ++ replace xs b c
,
unless b
is not found in xs
in which case it returns l
.
Equations
- List.replaceTR.go l b c [] x = l
- List.replaceTR.go l b c (a :: as) x = bif b == a then x.toListAppend (c :: as) else List.replaceTR.go l b c as (x.push a)
Instances For
modify #
Tail-recursive version of modify
.
Equations
- List.modifyTR f n l = List.modifyTR.go f l n #[]
Instances For
Auxiliary for modifyTR
: modifyTR.go f l n acc = acc.toList ++ modify f n l
.
Equations
- List.modifyTR.go f [] x✝ x = x.toList
- List.modifyTR.go f (head :: xs) 0 x = x.toListAppend (f head :: xs)
- List.modifyTR.go f (x_3 :: xs) n.succ x = List.modifyTR.go f xs n (x.push x_3)
Instances For
erase #
Tail recursive version of List.erase
.
Equations
- l.eraseTR a = List.eraseTR.go l a l #[]
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
- List.eraseTR.go l a [] x = l
- List.eraseTR.go l a (a_1 :: as) x = bif a_1 == a then x.toListAppend as else List.eraseTR.go l a as (x.push a_1)
Instances For
Tail-recursive version of eraseP
.
Equations
- List.erasePTR p l = List.erasePTR.go p l l #[]
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
- List.erasePTR.go p l [] x = l
- List.erasePTR.go p l (a :: as) x = bif p a then x.toListAppend as else List.erasePTR.go p l as (x.push a)
Instances For
eraseIdx #
Tail recursive version of List.eraseIdx
.
Equations
- l.eraseIdxTR n = List.eraseIdxTR.go l l n #[]
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
- List.eraseIdxTR.go l [] x✝ x = l
- List.eraseIdxTR.go l (head :: xs) 0 x = x.toListAppend xs
- List.eraseIdxTR.go l (x_3 :: xs) n.succ x = List.eraseIdxTR.go l xs n (x.push x_3)
Instances For
Zippers #
zipWith #
Tail recursive version of List.zipWith
.
Equations
- List.zipWithTR f as bs = List.zipWithTR.go f as bs #[]
Instances For
Auxiliary for zipWith
: zipWith.go f as bs acc = acc.toList ++ zipWith f as bs
Equations
- List.zipWithTR.go f (a :: as) (b :: bs) x = List.zipWithTR.go f as bs (x.push (f a b))
- List.zipWithTR.go f x✝¹ x✝ x = x.toList
Instances For
Ranges and enumeration #
enumFrom #
Tail recursive version of List.enumFrom
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Other list operations #
intercalate #
Tail recursive version of List.intercalate
.
Equations
- sep.intercalateTR [] = []
- sep.intercalateTR [x_1] = x_1
- sep.intercalateTR (x_1 :: xs) = List.intercalateTR.go sep.toArray x_1 xs #[]
Instances For
Auxiliary for intercalateTR
:
intercalateTR.go sep x xs acc = acc.toList ++ intercalate sep.toList (x::xs)
Equations
- List.intercalateTR.go sep x✝ [] x = x.toListAppend x✝
- List.intercalateTR.go sep x✝ (y :: xs) x = List.intercalateTR.go sep y xs (x ++ x✝ ++ sep)