git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1073 from david-christiansen/docs
3d50580Edwin Brady
libs/base/Data/BoundedList.idr+4
compare with master
unifiedsplit
@@ -3,10 +3,12 @@ module Data.BoundedList
3%access public
3%access public
4%default total
4%default total
5
5
6+||| A list with an upper bound on its length.
6data BoundedList : Type -> Nat -> Type where
7data BoundedList : Type -> Nat -> Type where
7 Nil : BoundedList a n
8 Nil : BoundedList a n
8 (::) : a -> BoundedList a n -> BoundedList a (S n)
9 (::) : a -> BoundedList a n -> BoundedList a (S n)
9
10
11+||| Compute the length of a list.
10length : BoundedList a n -> Fin (S n)
12length : BoundedList a n -> Fin (S n)
11length [] = fZ
13length [] = fZ
12length (x :: xs) = fS (length xs)
14length (x :: xs) = fS (length xs)
@@ -24,6 +26,7 @@ index (fS f) (_ :: xs) = index f xs
24-- Adjusting bounds
26-- Adjusting bounds
25--------------------------------------------------------------------------------
27--------------------------------------------------------------------------------
26
28
29+||| Loosen the bounds on a list's length.
27weaken : BoundedList a n -> BoundedList a (n + m)
30weaken : BoundedList a n -> BoundedList a (n + m)
28weaken [] = []
31weaken [] = []
29weaken (x :: xs) = x :: weaken xs
32weaken (x :: xs) = x :: weaken xs
@@ -77,6 +80,7 @@ map f (x :: xs) = f x :: map f xs
77-- Misc
80-- Misc
78--------------------------------------------------------------------------------
81--------------------------------------------------------------------------------
79
82
83+||| Extend a bounded list to the maximum size by padding on the left.
80pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
84pad : (xs : BoundedList a n) -> (padding : a) -> BoundedList a n
81pad {n=Z} [] _ = []
85pad {n=Z} [] _ = []
82pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
86pad {n=S n'} [] padding = padding :: (pad {n=n'} [] padding)
libs/base/Data/HVect.idr+6−2
@@ -6,7 +6,8 @@ import Data.Vect
6%default total
6%default total
7
7
8using (k : Nat, ts : Vect k Type)
8using (k : Nat, ts : Vect k Type)
9− ||| Heterogeneous vectors where the type index gives, element-wise, the types of the contents
9+ ||| Heterogeneous vectors where the type index gives, element-wise,
10+ ||| the types of the contents.
10 data HVect : Vect k Type -> Type where
11 data HVect : Vect k Type -> Type where
11 Nil : HVect []
12 Nil : HVect []
12 (::) : t -> HVect ts -> HVect (t::ts)
13 (::) : t -> HVect ts -> HVect (t::ts)
@@ -30,6 +31,7 @@ using (k : Nat, ts : Vect k Type)
30 updateAt fZ f (x::xs) = f x :: xs
31 updateAt fZ f (x::xs) = f x :: xs
31 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32 updateAt (fS j) f (x::xs) = x :: updateAt j f xs
32
33
34+ ||| Append two `HVect`s.
33 (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
35 (++) : {us : Vect l Type} -> HVect ts -> HVect us -> HVect (ts ++ us)
34 (++) [] ys = ys
36 (++) [] ys = ys
35 (++) (x::xs) ys = x :: (xs ++ ys)
37 (++) (x::xs) ys = x :: (xs ++ ys)
@@ -52,16 +54,18 @@ using (k : Nat, ts : Vect k Type)
52 instance (Shows k ts) => Show (HVect ts) where
54 instance (Shows k ts) => Show (HVect ts) where
53 show xs = show (shows xs)
55 show xs = show (shows xs)
54
56
55− ||| Extract an arbitrary element of the correct type
57+ ||| Extract an arbitrary element of the correct type.
56 ||| @ t the goal type
58 ||| @ t the goal type
57 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
59 get : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> HVect ts -> t
58 get {p = Here} (x::xs) = x
60 get {p = Here} (x::xs) = x
59 get {p = There p'} (x::xs) = get {p = p'} xs
61 get {p = There p'} (x::xs) = get {p = p'} xs
60
62
63+ ||| Replace an element with the correct type.
61 put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
64 put : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> t -> HVect ts -> HVect ts
62 put {p = Here} y (x::xs) = y :: xs
65 put {p = Here} y (x::xs) = y :: xs
63 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
66 put {p = There p'} y (x::xs) = x :: put {p = p'} y xs
64
67
68+ ||| Replace an element with the correct type.
65 update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
69 update : {default tactics { applyTactic findElem 100; solve; } p : Elem t ts} -> (t -> u) -> HVect ts -> HVect (replaceByElem ts p u)
66 update {p = Here} f (x::xs) = f x :: xs
70 update {p = Here} f (x::xs) = f x :: xs
67 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
71 update {p = There p'} f (x::xs) = x :: update {p = p'} f xs
libs/effects/Effect/StdIO.idr+17
@@ -3,12 +3,22 @@ module Effect.StdIO
3import Effects
3import Effects
4import Control.IOExcept
4import Control.IOExcept
5
5
6+-------------------------------------------------------------
7+-- IO effects internals
8+-------------------------------------------------------------
9+
10+||| The internal representation of StdIO effects
6data StdIO : Effect where
11data StdIO : Effect where
7 PutStr : String -> { () } StdIO ()
12 PutStr : String -> { () } StdIO ()
8 GetStr : { () } StdIO String
13 GetStr : { () } StdIO String
9 PutCh : Char -> { () } StdIO ()
14 PutCh : Char -> { () } StdIO ()
10 GetCh : { () } StdIO Char
15 GetCh : { () } StdIO Char
11
16
17+
18+-------------------------------------------------------------
19+-- IO effects handlers
20+-------------------------------------------------------------
21+
12instance Handler StdIO IO where
22instance Handler StdIO IO where
13 handle () (PutStr s) k = do putStr s; k () ()
23 handle () (PutStr s) k = do putStr s; k () ()
14 handle () GetStr k = do x <- getLine; k x ()
24 handle () GetStr k = do x <- getLine; k x ()
@@ -21,23 +31,30 @@ instance Handler StdIO (IOExcept a) where
21 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
31 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()
22 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
32 handle () GetCh k = do x <- ioe_lift $ getChar; k x ()
23
33
34+-------------------------------------------------------------
24--- The Effect and associated functions
35--- The Effect and associated functions
36+-------------------------------------------------------------
25
37
26STDIO : EFFECT
38STDIO : EFFECT
27STDIO = MkEff () StdIO
39STDIO = MkEff () StdIO
28
40
41+||| Write a string to standard output.
29putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
42putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()
30putStr s = PutStr s
43putStr s = PutStr s
31
44
45+||| Write a character to standard output.
32putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
46putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()
33putChar c = PutCh c
47putChar c = PutCh c
34
48
49+||| Write a string to standard output, terminating with a newline.
35putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
50putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()
36putStrLn s = putStr (s ++ "\n")
51putStrLn s = putStr (s ++ "\n")
37
52
53+||| Read a string from standard input.
38getStr : Handler StdIO e => { [STDIO] } Eff e String
54getStr : Handler StdIO e => { [STDIO] } Eff e String
39getStr = GetStr
55getStr = GetStr
40
56
57+||| Read a character from standard input.
41getChar : Handler StdIO e => { [STDIO] } Eff e Char
58getChar : Handler StdIO e => { [STDIO] } Eff e Char
42getChar = GetCh
59getChar = GetCh
43
60
libs/prelude/Builtins.idr+19
@@ -17,6 +17,7 @@ getWitness (a ** v) = a
17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
17getProof : {P : a -> Type} -> (s : Exists a P) -> P (getWitness s)
18getProof (a ** v) = v
18getProof (a ** v) = v
19
19
20+||| The eliminator for the empty type.
20FalseElim : _|_ -> a
21FalseElim : _|_ -> a
21
22
22||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
23||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
@@ -43,17 +44,35 @@ lazy x = x -- compiled specially
43force : a -> a
44force : a -> a
44force x = x -- compiled specially
45force x = x -- compiled specially
45
46
47+||| There are two types of laziness: that arising from lazy functions, and that
48+||| arising from codata. They differ in their totality condition.
46data LazyType = LazyCodata | LazyEval
49data LazyType = LazyCodata | LazyEval
47
50
51+||| The underlying implementation of Lazy and Inf.
48data Lazy' : LazyType -> Type -> Type where
52data Lazy' : LazyType -> Type -> Type where
53+ ||| A delayed computation.
54+ |||
55+ |||Delay is inserted automatically by the elaborator where necessary.
56+ |||
57+ ||| Note that compiled code gives `Delay` special semantics.
58+ ||| @ t whether this is laziness from codata or normal lazy evaluation
59+ ||| @ a the type of the eventual value
60+ ||| @ val a computation that will produce a value
49 Delay : {t, a : _} -> (val : a) -> Lazy' t a
61 Delay : {t, a : _} -> (val : a) -> Lazy' t a
50
62
63+||| Compute a value from a delayed computation.
64+|||
65+||| Inserted by the elaborator where necessary.
51Force : {t, a : _} -> Lazy' t a -> a
66Force : {t, a : _} -> Lazy' t a -> a
52Force (Delay x) = x
67Force (Delay x) = x
53
68
69+||| Lazily evaluated values. This has special evaluation semantics.
54Lazy : Type -> Type
70Lazy : Type -> Type
55Lazy t = Lazy' LazyEval t
71Lazy t = Lazy' LazyEval t
56
72
73+||| Recursive parameters to codata. Inserted automatically by the elaborator
74+||| on a "codata" definition but is necessary by hand if mixing inductive and
75+||| coinductive parameters.
57Inf : Type -> Type
76Inf : Type -> Type
58Inf t = Lazy' LazyCodata t
77Inf t = Lazy' LazyCodata t
59
78
libs/prelude/Prelude/Fin.idr+12−1
@@ -6,7 +6,10 @@ import Prelude.Uninhabited
6
6
7%default total
7%default total
8
8
9−||| Numbers strictly less than some bound. The name comes from "finite sets"
9+||| Numbers strictly less than some bound. The name comes from "finite sets".
10+|||
11+||| It's probably not a good idea to use `Fin` for arithmetic, and they will be
12+||| exceedingly inefficient at run time.
10||| @ n the upper bound
13||| @ n the upper bound
11data Fin : (n : Nat) -> Type where
14data Fin : (n : Nat) -> Type where
12 fZ : Fin (S k)
15 fZ : Fin (S k)
@@ -24,16 +27,19 @@ instance Eq (Fin n) where
24 (==) (fS k) (fS k') = k == k'
27 (==) (fS k) (fS k') = k == k'
25 (==) _ _ = False
28 (==) _ _ = False
26
29
30+||| There are no elements of `Fin Z`
27FinZAbsurd : Fin Z -> _|_
31FinZAbsurd : Fin Z -> _|_
28FinZAbsurd fZ impossible
32FinZAbsurd fZ impossible
29
33
30FinZElim : Fin Z -> a
34FinZElim : Fin Z -> a
31FinZElim x = FalseElim (FinZAbsurd x)
35FinZElim x = FalseElim (FinZAbsurd x)
32
36
37+||| Convert a Fin to a Nat
33finToNat : Fin n -> Nat
38finToNat : Fin n -> Nat
34finToNat fZ = Z
39finToNat fZ = Z
35finToNat (fS k) = S (finToNat k)
40finToNat (fS k) = S (finToNat k)
36
41
42+||| `finToNat` is injective
37finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
43finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn
38finToNatInjective fZ fZ refl = refl
44finToNatInjective fZ fZ refl = refl
39finToNatInjective (fS m) fZ refl impossible
45finToNatInjective (fS m) fZ refl impossible
@@ -44,6 +50,7 @@ finToNatInjective (fS m) (fS n) prf =
44instance Cast (Fin n) Nat where
50instance Cast (Fin n) Nat where
45 cast x = finToNat x
51 cast x = finToNat x
46
52
53+||| Convert a Fin to an Integer
47finToInteger : Fin n -> Integer
54finToInteger : Fin n -> Integer
48finToInteger fZ = 0
55finToInteger fZ = 0
49finToInteger (fS k) = 1 + finToInteger k
56finToInteger (fS k) = 1 + finToInteger k
@@ -123,9 +130,13 @@ natToFin _ _ = Nothing
123integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
130integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
124integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
131integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing
125
132
133+||| Proof that some `Maybe` is actually `Just`
126data IsJust : Maybe a -> Type where
134data IsJust : Maybe a -> Type where
127 ItIsJust : IsJust {a} (Just x)
135 ItIsJust : IsJust {a} (Just x)
128
136
137+||| Allow overloading of Integer literals for Fin.
138+||| @ x the Integer that the user typed
139+||| @ prf an automatically-constructed proof that `x` is in bounds
129fromInteger : (x : Integer) ->
140fromInteger : (x : Integer) ->
130 {default ItIsJust
141 {default ItIsJust
131 prf : (IsJust (integerToFin x n))} ->
142 prf : (IsJust (integerToFin x n))} ->
libs/prelude/Prelude/List.idr+132−26
@@ -15,9 +15,12 @@ import Prelude.Nat
15infix 5 \\
15infix 5 \\
16infixr 7 ::,++
16infixr 7 ::,++
17
17
18+||| Linked lists
18−%elim data List a
19+%elim data List a =
20+ ||| The empty list
19− = Nil
21+ Nil |
22+ ||| Cons cell
20− | (::) a (List a)
23+ (::) a (List a)
21
24
22-- Name hints for interactive editing
25-- Name hints for interactive editing
23%name List xs, ys, zs, ws
26%name List xs, ys, zs, ws
@@ -26,10 +29,12 @@ infixr 7 ::,++
26-- Syntactic tests
29-- Syntactic tests
27--------------------------------------------------------------------------------
30--------------------------------------------------------------------------------
28
31
32+||| Returns `True` iff the argument is empty
29isNil : List a -> Bool
33isNil : List a -> Bool
30isNil [] = True
34isNil [] = True
31isNil (x::xs) = False
35isNil (x::xs) = False
32
36
37+||| Returns `True` iff the argument is not empty
33isCons : List a -> Bool
38isCons : List a -> Bool
34isCons [] = False
39isCons [] = False
35isCons (x::xs) = True
40isCons (x::xs) = True
@@ -38,6 +43,9 @@ isCons (x::xs) = True
38-- Length
43-- Length
39--------------------------------------------------------------------------------
44--------------------------------------------------------------------------------
40
45
46+||| Compute the length of a list.
47+|||
48+||| Runs in linear time
41length : List a -> Nat
49length : List a -> Nat
42length [] = 0
50length [] = 0
43length (x::xs) = 1 + length xs
51length (x::xs) = 1 + length xs
@@ -46,49 +54,74 @@ length (x::xs) = 1 + length xs
46-- Indexing into lists
54-- Indexing into lists
47--------------------------------------------------------------------------------
55--------------------------------------------------------------------------------
48
56
57+||| Find a particular element of a list.
58+|||
59+||| @ ok a proof that the index is within bounds
49−index : (n : Nat) -> (l : List a) -> (lt n (length l) = True) -> a
60+index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a
50index Z (x::xs) p = x
61index Z (x::xs) p = x
51index (S n) (x::xs) p = index n xs ?indexTailProof
62index (S n) (x::xs) p = index n xs ?indexTailProof
52index _ [] refl impossible
63index _ [] refl impossible
53
64
65+||| Attempt to find a particular element of a list.
66+|||
67+||| If the provided index is out of bounds, return Nothing.
54index' : (n : Nat) -> (l : List a) -> Maybe a
68index' : (n : Nat) -> (l : List a) -> Maybe a
55index' Z (x::xs) = Just x
69index' Z (x::xs) = Just x
56index' (S n) (x::xs) = index' n xs
70index' (S n) (x::xs) = index' n xs
57index' _ [] = Nothing
71index' _ [] = Nothing
58
72
73+||| Get the first element of a non-empty list
74+||| @ ok proof that the list is non-empty
59−head : (l : List a) -> (isCons l = True) -> a
75+head : (l : List a) -> (ok : isCons l = True) -> a
60head [] refl impossible
76head [] refl impossible
61head (x::xs) p = x
77head (x::xs) p = x
62
78
79+||| Attempt to get the first element of a list. If the list is empty, return
80+||| `Nothing`.
63head' : (l : List a) -> Maybe a
81head' : (l : List a) -> Maybe a
64head' [] = Nothing
82head' [] = Nothing
65head' (x::xs) = Just x
83head' (x::xs) = Just x
66
84
85+||| Get the tail of a non-empty list.
86+||| @ ok proof that the list is non-empty
67−tail : (l : List a) -> (isCons l = True) -> List a
87+tail : (l : List a) -> (ok : isCons l = True) -> List a
68tail [] refl impossible
88tail [] refl impossible
69tail (x::xs) p = xs
89tail (x::xs) p = xs
70
90
91+||| Attempt to get the tail of a list.
92+|||
93+||| If the list is empty, return `Nothing`.
71tail' : (l : List a) -> Maybe (List a)
94tail' : (l : List a) -> Maybe (List a)
72tail' [] = Nothing
95tail' [] = Nothing
73tail' (x::xs) = Just xs
96tail' (x::xs) = Just xs
74
97
98+||| Retrieve the last element of a non-empty list.
99+||| @ ok proof that the list is non-empty
75−last : (l : List a) -> (isCons l = True) -> a
100+last : (l : List a) -> (ok : isCons l = True) -> a
76last [] refl impossible
101last [] refl impossible
77last [x] p = x
102last [x] p = x
78last (x::y::ys) p = last (y::ys) refl
103last (x::y::ys) p = last (y::ys) refl
79
104
105+||| Attempt to retrieve the last element of a non-empty list.
106+|||
107+||| If the list is empty, return `Nothing`.
80last' : (l : List a) -> Maybe a
108last' : (l : List a) -> Maybe a
81last' [] = Nothing
109last' [] = Nothing
82−last' (x::xs) =
110+last' (x::xs) =
83 case xs of
111 case xs of
84 [] => Just x
112 [] => Just x
85 y :: ys => last' xs
113 y :: ys => last' xs
86
114
115+||| Return all but the last element of a non-empty list.
116+||| @ ok proof that the list is non-empty
87−init : (l : List a) -> (isCons l = True) -> List a
117+init : (l : List a) -> (ok : isCons l = True) -> List a
88init [] refl impossible
118init [] refl impossible
89init [x] p = []
119init [x] p = []
90init (x::y::ys) p = x :: init (y::ys) refl
120init (x::y::ys) p = x :: init (y::ys) refl
91
121
122+||| Attempt to Return all but the last element of a list.
123+|||
124+||| If the list is empty, return `Nothing`.
92init' : (l : List a) -> Maybe (List a)
125init' : (l : List a) -> Maybe (List a)
93init' [] = Nothing
126init' [] = Nothing
94init' (x::xs) =
127init' (x::xs) =
@@ -104,21 +137,39 @@ init' (x::xs) =
104-- Sublists
137-- Sublists
105--------------------------------------------------------------------------------
138--------------------------------------------------------------------------------
106
139
140+||| Take the first `n` elements of `xs`
141+|||
142+||| If there are not enough elements, return the whole list.
143+||| @ n how many elements to take
144+||| @ xs the list to take them from
107−take : Nat -> List a -> List a
145+take : (n : Nat) -> (xs : List a) -> List a
108take Z xs = []
146take Z xs = []
109take (S n) [] = []
147take (S n) [] = []
110take (S n) (x::xs) = x :: take n xs
148take (S n) (x::xs) = x :: take n xs
111
149
150+||| Drop the first `n` elements of `xs`
151+|||
152+||| If there are not enough elements, return the empty list.
153+||| @ n how many elements to drop
154+||| @ xs the list to drop them from
112−drop : Nat -> List a -> List a
155+drop : (n : Nat) -> (xs : List a) -> List a
113drop Z xs = xs
156drop Z xs = xs
114drop (S n) [] = []
157drop (S n) [] = []
115drop (S n) (x::xs) = drop n xs
158drop (S n) (x::xs) = drop n xs
116
159
160+||| Take the longest prefix of a list such that all elements satsify some
161+||| Boolean predicate.
162+|||
163+||| @ p the predicate
117−takeWhile : (a -> Bool) -> List a -> List a
164+takeWhile : (p : a -> Bool) -> List a -> List a
118takeWhile p [] = []
165takeWhile p [] = []
119takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
166takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []
120
167
168+||| Remove the longest prefix of a list such that all removed elements satsify some
169+||| Boolean predicate.
170+|||
171+||| @ p the predicate
121−dropWhile : (a -> Bool) -> List a -> List a
172+dropWhile : (p : a -> Bool) -> List a -> List a
122dropWhile p [] = []
173dropWhile p [] = []
123dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
174dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
124
175
@@ -126,7 +177,12 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
126-- Misc.
177-- Misc.
127--------------------------------------------------------------------------------
178--------------------------------------------------------------------------------
128
179
180+||| Simply-typed recursion operator for lists.
181+|||
182+||| @ nil what to return at the end of the list
183+||| @ cons what to do at each step of recursion
184+||| @ xs the list to recurse over
129−list : a -> (a -> List a -> a) -> List a -> a
185+list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
130list nil cons [] = nil
186list nil cons [] = nil
131list nil cons (x::xs) = cons x xs
187list nil cons (x::xs) = cons x xs
132
188
@@ -134,16 +190,23 @@ list nil cons (x::xs) = cons x xs
134-- Building (bigger) lists
190-- Building (bigger) lists
135--------------------------------------------------------------------------------
191--------------------------------------------------------------------------------
136
192
193+||| Append two lists
137(++) : List a -> List a -> List a
194(++) : List a -> List a -> List a
138−(++) [] right = right
195+(++) [] right = right
139(++) (x::xs) right = x :: (xs ++ right)
196(++) (x::xs) right = x :: (xs ++ right)
140
197
198+||| Create an infinite sequence of some item.
199+|||
200+||| Consider using a `Stream` instead.
141partial
201partial
142repeat : a -> List a
202repeat : a -> List a
143repeat x = x :: lazy (repeat x)
203repeat x = x :: lazy (repeat x)
144
204
205+||| Construct a list with `n` copies of `x`
206+||| @ n how many copies
207+||| @ x the element to replicate
145−replicate : Nat -> a -> List a
208+replicate : (n : Nat) -> (x : a) -> List a
146−replicate Z x = []
209+replicate Z x = []
147replicate (S n) x = x :: replicate n x
210replicate (S n) x = x :: replicate n x
148
211
149--------------------------------------------------------------------------------
212--------------------------------------------------------------------------------
@@ -188,15 +251,27 @@ instance Functor List where
188-- Zips and unzips
251-- Zips and unzips
189--------------------------------------------------------------------------------
252--------------------------------------------------------------------------------
190
253
254+||| Combine two lists of the same length elementwise using some function.
255+||| @ f the function to combine elements with
256+||| @ l the first list
257+||| @ r the second list
258+||| @ ok a proof that the lengths of the inputs are equal
191zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
259zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
192− (length l = length r) -> List c
260+ (ok : length l = length r) -> List c
193zipWith f [] (y::ys) refl impossible
261zipWith f [] (y::ys) refl impossible
194zipWith f (x::xs) [] refl impossible
262zipWith f (x::xs) [] refl impossible
195zipWith f [] [] p = []
263zipWith f [] [] p = []
196zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
264zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys ?zipWithTailProof)
197
265
266+||| Combine three lists of the same length elementwise using some function.
267+||| @ f the function to combine elements with
268+||| @ x the first list
269+||| @ y the second list
270+||| @ z the third list
271+||| @ ok a proof that the lengths of the first two inputs are equal
272+||| @ ok' a proof that the lengths of the second and third inputs are equal
198zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
273zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
199− (z : List c) -> (length x = length y) -> (length y = length z) -> List d
274+ (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
200zipWith3 f _ [] (z::zs) p refl impossible
275zipWith3 f _ [] (z::zs) p refl impossible
201zipWith3 f _ (y::ys) [] p refl impossible
276zipWith3 f _ (y::ys) [] p refl impossible
202zipWith3 f [] (y::ys) _ refl q impossible
277zipWith3 f [] (y::ys) _ refl q impossible
@@ -205,18 +280,22 @@ zipWith3 f [] [] [] p q = []
205zipWith3 f (x::xs) (y::ys) (z::zs) p q =
280zipWith3 f (x::xs) (y::ys) (z::zs) p q =
206 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
281 f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')
207
282
283+||| Combine two lists elementwise into pairs
208zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
284zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
209zip = zipWith (\x => \y => (x, y))
285zip = zipWith (\x => \y => (x, y))
210
286
287+||| Combine three lists elementwise into tuples
211zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
288zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
212 (length y = length z) -> List (a, b, c)
289 (length y = length z) -> List (a, b, c)
213zip3 = zipWith3 (\x => \y => \z => (x, y, z))
290zip3 = zipWith3 (\x => \y => \z => (x, y, z))
214
291
292+||| Split a list of pairs into two lists
215unzip : List (a, b) -> (List a, List b)
293unzip : List (a, b) -> (List a, List b)
216unzip [] = ([], [])
294unzip [] = ([], [])
217unzip ((l, r)::xs) with (unzip xs)
295unzip ((l, r)::xs) with (unzip xs)
218 | (lefts, rights) = (l::lefts, r::rights)
296 | (lefts, rights) = (l::lefts, r::rights)
219
297
298+||| Split a list of triples into three lists
220unzip3 : List (a, b, c) -> (List a, List b, List c)
299unzip3 : List (a, b, c) -> (List a, List b, List c)
221unzip3 [] = ([], [], [])
300unzip3 [] = ([], [], [])
222unzip3 ((l, c, r)::xs) with (unzip3 xs)
301unzip3 ((l, c, r)::xs) with (unzip3 xs)
@@ -226,6 +305,8 @@ unzip3 ((l, c, r)::xs) with (unzip3 xs)
226-- Maps
305-- Maps
227--------------------------------------------------------------------------------
306--------------------------------------------------------------------------------
228
307
308+||| Apply a partial function to the elements of a list, keeping the ones at which
309+||| it is defined.
229mapMaybe : (a -> Maybe b) -> List a -> List b
310mapMaybe : (a -> Maybe b) -> List a -> List b
230mapMaybe f [] = []
311mapMaybe f [] = []
231mapMaybe f (x::xs) =
312mapMaybe f (x::xs) =
@@ -237,6 +318,7 @@ mapMaybe f (x::xs) =
237-- Folds
318-- Folds
238--------------------------------------------------------------------------------
319--------------------------------------------------------------------------------
239
320
321+||| A tail recursive right fold on Lists.
240total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
322total foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> List t -> acc
241foldrImpl f e go [] = go e
323foldrImpl f e go [] = go e
242foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
324foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs
@@ -248,6 +330,7 @@ instance Foldable List where
248-- Special folds
330-- Special folds
249--------------------------------------------------------------------------------
331--------------------------------------------------------------------------------
250
332
333+||| Convert any Foldable structure to a list.
251toList : Foldable t => t a -> List a
334toList : Foldable t => t a -> List a
252toList = foldr (::) []
335toList = foldr (::) []
253
336
@@ -255,6 +338,7 @@ toList = foldr (::) []
255-- Transformations
338-- Transformations
256--------------------------------------------------------------------------------
339--------------------------------------------------------------------------------
257
340
341+||| Return the elements of a list in reverse order.
258reverse : List a -> List a
342reverse : List a -> List a
259reverse = reverse' []
343reverse = reverse' []
260 where
344 where
@@ -262,6 +346,7 @@ reverse = reverse' []
262 reverse' acc [] = acc
346 reverse' acc [] = acc
263 reverse' acc (x::xs) = reverse' (x::acc) xs
347 reverse' acc (x::xs) = reverse' (x::acc) xs
264
348
349+||| Insert some separator between the elements of a list.
265intersperse : a -> List a -> List a
350intersperse : a -> List a -> List a
266intersperse sep [] = []
351intersperse sep [] = []
267intersperse sep (x::xs) = x :: intersperse' sep xs
352intersperse sep (x::xs) = x :: intersperse' sep xs
@@ -275,13 +360,13 @@ intercalate sep l = concat $ intersperse sep l
275
360
276||| Transposes rows and columns of a list of lists.
361||| Transposes rows and columns of a list of lists.
277|||
362|||
278−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
363+||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]
279|||
364|||
280||| This also works for non square scenarios, thus
365||| This also works for non square scenarios, thus
281||| involution does not always hold:
366||| involution does not always hold:
282|||
367|||
283−||| > transpose [[], [1, 2]] = [[1], [2]]
368+||| > transpose [[], [1, 2]] = [[1], [2]]
284−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
369+||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]
285|||
370|||
286||| TODO: Solution which satisfies the totality checker?
371||| TODO: Solution which satisfies the totality checker?
287%assert_total
372%assert_total
@@ -294,6 +379,7 @@ transpose ((x::xs) :: xss) = (x :: (mapMaybe head' xss)) :: (transpose (xs :: (m
294-- Membership tests
379-- Membership tests
295--------------------------------------------------------------------------------
380--------------------------------------------------------------------------------
296
381
382+||| Check if something is a member of a list using a custom comparison.
297elemBy : (a -> a -> Bool) -> a -> List a -> Bool
383elemBy : (a -> a -> Bool) -> a -> List a -> Bool
298elemBy p e [] = False
384elemBy p e [] = False
299elemBy p e (x::xs) =
385elemBy p e (x::xs) =
@@ -302,9 +388,11 @@ elemBy p e (x::xs) =
302 else
388 else
303 elemBy p e xs
389 elemBy p e xs
304
390
391+||| Check if something is a member of a list using the default Boolean equality.
305elem : Eq a => a -> List a -> Bool
392elem : Eq a => a -> List a -> Bool
306elem = elemBy (==)
393elem = elemBy (==)
307
394
395+||| Find associated information in a list using a custom comparison.
308lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
396lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
309lookupBy p e [] = Nothing
397lookupBy p e [] = Nothing
310lookupBy p e (x::xs) =
398lookupBy p e (x::xs) =
@@ -314,9 +402,12 @@ lookupBy p e (x::xs) =
314 else
402 else
315 lookupBy p e xs
403 lookupBy p e xs
316
404
405+||| Find associated information in a list using Boolean equality.
317lookup : Eq a => a -> List (a, b) -> Maybe b
406lookup : Eq a => a -> List (a, b) -> Maybe b
318lookup = lookupBy (==)
407lookup = lookupBy (==)
319
408
409+||| Check if any elements of the first list are found in the second, using
410+||| a custom comparison.
320hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
411hasAnyBy : (a -> a -> Bool) -> List a -> List a -> Bool
321hasAnyBy p elems [] = False
412hasAnyBy p elems [] = False
322hasAnyBy p elems (x::xs) =
413hasAnyBy p elems (x::xs) =
@@ -325,6 +416,8 @@ hasAnyBy p elems (x::xs) =
325 else
416 else
326 hasAnyBy p elems xs
417 hasAnyBy p elems xs
327
418
419+||| Check if any elements of the first list are found in the second, using
420+||| Boolean equality.
328hasAny : Eq a => List a -> List a -> Bool
421hasAny : Eq a => List a -> List a -> Bool
329hasAny = hasAnyBy (==)
422hasAny = hasAnyBy (==)
330
423
@@ -332,6 +425,7 @@ hasAny = hasAnyBy (==)
332-- Searching with a predicate
425-- Searching with a predicate
333--------------------------------------------------------------------------------
426--------------------------------------------------------------------------------
334
427
428+||| Find the first element of a list that satisfies a predicate, or `Nothing` if none do.
335find : (a -> Bool) -> List a -> Maybe a
429find : (a -> Bool) -> List a -> Maybe a
336find p [] = Nothing
430find p [] = Nothing
337find p (x::xs) =
431find p (x::xs) =
@@ -340,6 +434,8 @@ find p (x::xs) =
340 else
434 else
341 find p xs
435 find p xs
342
436
437+||| Find the index of the first element of a list that satisfies a predicate, or
438+||| `Nothing` if none do.
343findIndex : (a -> Bool) -> List a -> Maybe Nat
439findIndex : (a -> Bool) -> List a -> Maybe Nat
344findIndex = findIndex' Z
440findIndex = findIndex' Z
345 where
441 where
@@ -351,6 +447,7 @@ findIndex = findIndex' Z
351 else
447 else
352 findIndex' (S cnt) p xs
448 findIndex' (S cnt) p xs
353
449
450+||| Find the indices of all elements that satisfy some predicate.
354findIndices : (a -> Bool) -> List a -> List Nat
451findIndices : (a -> Bool) -> List a -> List Nat
355findIndices = findIndices' Z
452findIndices = findIndices' Z
356 where
453 where
@@ -420,6 +517,8 @@ union = unionBy (==)
420-- Splitting and breaking lists
517-- Splitting and breaking lists
421--------------------------------------------------------------------------------
518--------------------------------------------------------------------------------
422
519
520+||| Given a list and a predicate, returns a pair consisting of the longest
521+||| prefix of the list that satisfies a predicate and the rest of the list.
423span : (a -> Bool) -> List a -> (List a, List a)
522span : (a -> Bool) -> List a -> (List a, List a)
424span p [] = ([], [])
523span p [] = ([], [])
425span p (x::xs) =
524span p (x::xs) =
@@ -528,6 +627,7 @@ sort xs = let (x, y) = split xs in
528-- Conversions
627-- Conversions
529--------------------------------------------------------------------------------
628--------------------------------------------------------------------------------
530
629
630+||| Either return the head of a list, or `Nothing` if it is empty.
531listToMaybe : List a -> Maybe a
631listToMaybe : List a -> Maybe a
532listToMaybe [] = Nothing
632listToMaybe [] = Nothing
533listToMaybe (x::xs) = Just x
633listToMaybe (x::xs) = Just x
@@ -547,7 +647,7 @@ catMaybes (x::xs) =
547-- Properties
647-- Properties
548--------------------------------------------------------------------------------
648--------------------------------------------------------------------------------
549
649
550−-- append
650+||| The empty list is a right identity for append.
551appendNilRightNeutral : (l : List a) ->
651appendNilRightNeutral : (l : List a) ->
552 l ++ [] = l
652 l ++ [] = l
553appendNilRightNeutral [] = refl
653appendNilRightNeutral [] = refl
@@ -555,6 +655,7 @@ appendNilRightNeutral (x::xs) =
555 let inductiveHypothesis = appendNilRightNeutral xs in
655 let inductiveHypothesis = appendNilRightNeutral xs in
556 ?appendNilRightNeutralStepCase
656 ?appendNilRightNeutralStepCase
557
657
658+||| Appending lists is associative.
558appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
659appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->
559 l ++ (c ++ r) = (l ++ c) ++ r
660 l ++ (c ++ r) = (l ++ c) ++ r
560appendAssociative [] c r = refl
661appendAssociative [] c r = refl
@@ -562,7 +663,8 @@ appendAssociative (x::xs) c r =
562 let inductiveHypothesis = appendAssociative xs c r in
663 let inductiveHypothesis = appendAssociative xs c r in
563 ?appendAssociativeStepCase
664 ?appendAssociativeStepCase
564
665
565−-- length
666+||| The length of two lists that are appended is the sum of the lengths
667+||| of the input lists.
566lengthAppend : (left : List a) -> (right : List a) ->
668lengthAppend : (left : List a) -> (right : List a) ->
567 length (left ++ right) = length left + length right
669 length (left ++ right) = length left + length right
568lengthAppend [] right = refl
670lengthAppend [] right = refl
@@ -570,7 +672,7 @@ lengthAppend (x::xs) right =
570 let inductiveHypothesis = lengthAppend xs right in
672 let inductiveHypothesis = lengthAppend xs right in
571 ?lengthAppendStepCase
673 ?lengthAppendStepCase
572
674
573−-- map
675+||| Mapping a function over a list doesn't change its length.
574mapPreservesLength : (f : a -> b) -> (l : List a) ->
676mapPreservesLength : (f : a -> b) -> (l : List a) ->
575 length (map f l) = length l
677 length (map f l) = length l
576mapPreservesLength f [] = refl
678mapPreservesLength f [] = refl
@@ -578,6 +680,8 @@ mapPreservesLength f (x::xs) =
578 let inductiveHypothesis = mapPreservesLength f xs in
680 let inductiveHypothesis = mapPreservesLength f xs in
579 ?mapPreservesLengthStepCase
681 ?mapPreservesLengthStepCase
580
682
683+||| Mapping a function over two lists and appending them is equivalent
684+||| to appending them and then mapping the function.
581mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
685mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->
582 map f (l ++ r) = map f l ++ map f r
686 map f (l ++ r) = map f l ++ map f r
583mapDistributesOverAppend f [] r = refl
687mapDistributesOverAppend f [] r = refl
@@ -585,6 +689,7 @@ mapDistributesOverAppend f (x::xs) r =
585 let inductiveHypothesis = mapDistributesOverAppend f xs r in
689 let inductiveHypothesis = mapDistributesOverAppend f xs r in
586 ?mapDistributesOverAppendStepCase
690 ?mapDistributesOverAppendStepCase
587
691
692+||| Mapping two functions is the same as mapping their composition.
588mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
693mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->
589 map f (map g l) = map (f . g) l
694 map f (map g l) = map (f . g) l
590mapFusion f g [] = refl
695mapFusion f g [] = refl
@@ -592,7 +697,7 @@ mapFusion f g (x::xs) =
592 let inductiveHypothesis = mapFusion f g xs in
697 let inductiveHypothesis = mapFusion f g xs in
593 ?mapFusionStepCase
698 ?mapFusionStepCase
594
699
595−-- hasAny
700+||| No list contains an element of the empty list by any predicate.
596hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
701hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->
597 hasAnyBy p [] l = False
702 hasAnyBy p [] l = False
598hasAnyByNilFalse p [] = refl
703hasAnyByNilFalse p [] = refl
@@ -600,6 +705,7 @@ hasAnyByNilFalse p (x::xs) =
600 let inductiveHypothesis = hasAnyByNilFalse p xs in
705 let inductiveHypothesis = hasAnyByNilFalse p xs in
601 ?hasAnyByNilFalseStepCase
706 ?hasAnyByNilFalseStepCase
602
707
708+||| No list contains an element of the empty list.
603hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
709hasAnyNilFalse : Eq a => (l : List a) -> hasAny [] l = False
604hasAnyNilFalse l = ?hasAnyNilFalseBody
710hasAnyNilFalse l = ?hasAnyNilFalseBody
605
711