Tail recursive implementations for List
definitions. #
Many of the proofs require theorems about Array
,
so these are in a separate file to minimize imports.
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
, groupBy
.
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
,
minimum?
, maximum?
, and removeAll
.
The following operations are given @[csimp]
replacements below:
length
, set
, map
, filter
, filterMap
, foldr
, append
, bind
, join
, replicate
,
take
, takeWhile
, dropLast
, replace
, erase
, eraseIdx
, zipWith
, unzip
, iota
,
enumFrom
, intersperse
, and intercalate
.
length #
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
map #
Tail-recursive version of List.map
.
Equations
- List.mapTR f as = List.mapTR.loop f as []
Instances For
Equations
- List.mapTR.loop f [] x = x.reverse
- List.mapTR.loop f (a :: as) x = List.mapTR.loop f as (f a :: x)
Instances For
filter #
Tail-recursive version of List.filter
.
Equations
- List.filterTR p as = List.filterTR.loop p as []
Instances For
Equations
- List.filterTR.loop p [] x = x.reverse
- List.filterTR.loop p (a :: as) x = match p a with | true => List.filterTR.loop p as (a :: x) | false => List.filterTR.loop p as x
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 (List.toArray l) (List.toArray l).size
Instances For
bind #
Tail recursive version of List.bind
.
Equations
- as.bindTR f = List.bindTR.go f as #[]
Instances For
Auxiliary for bind
: bind.go f as = acc.toList ++ bind f as
Equations
- List.bindTR.go f [] x = x.toList
- List.bindTR.go f (a :: as) x = List.bindTR.go f as (x ++ f a)
Instances For
join #
replicate #
Tail-recursive version of List.replicate
.
Equations
- List.replicateTR n a = List.replicateTR.loop a n []
Instances For
Equations
- List.replicateTR.loop a 0 x = x
- List.replicateTR.loop a n.succ x = List.replicateTR.loop a n (a :: x)
Instances For
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 #
Tail recursive version of dropLast
.
Equations
- l.dropLastTR = (List.toArray l).pop.toList
Instances For
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
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
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
unzip #
Ranges and enumeration #
iota #
Equations
- List.iotaTR.go 0 x = x.reverse
- List.iotaTR.go n.succ x = List.iotaTR.go n (n.succ :: x)
Instances For
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 #
intersperse #
intercalate #
Tail recursive version of List.intercalate
.
Equations
- sep.intercalateTR x = match x with | [] => [] | [x] => x | x :: xs => List.intercalateTR.go (List.toArray sep) x 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)