0 | module Prelude.Basics
  1 |
  2 | import Builtin
  3 |
  4 | import Prelude.Ops
  5 |
  6 | %default total
  7 |
  8 |
  9 | ||| `Not x` is an alias for `x -> Void`, indicating that any term of type `x`
 10 | ||| leads to a contradiction. It can be used in conjunction with `void` or
 11 | ||| `absurd`.
 12 | public export
 13 | Not : Type -> Type
 14 | Not x = x -> Void
 15 |
 16 | -----------------------
 17 | -- UTILITY FUNCTIONS --
 18 | -----------------------
 19 |
 20 | ||| Manually assign a type to an expression.
 21 | ||| @ a the type to assign
 22 | ||| @ x the element to get the type
 23 | public export %inline
 24 | the : (0 a : Type) -> (1 x : a) -> a
 25 | the _ x = x
 26 |
 27 | ||| Identity function.
 28 | public export %inline
 29 | id : (x : a) -> a
 30 | id x = x
 31 |
 32 | ||| Function that duplicates its input
 33 | public export
 34 | dup : a -> (a, a)
 35 | dup x = (x, x)
 36 |
 37 | ||| Constant function.  Ignores its second argument.
 38 | public export %inline
 39 | const : a -> b -> a
 40 | const x = \value => x
 41 |
 42 | ||| Function composition.
 43 | public export %inline %tcinline
 44 | (.) : (b -> c) -> (a -> b) -> a -> c
 45 | (.) f g = \x => f (g x)
 46 |
 47 | ||| Composition of a two-argument function with a single-argument one.
 48 | ||| `(.:)` is like `(.)` but the second argument and the result are two-argument functions.
 49 | ||| This operator is also known as "blackbird operator".
 50 | public export %inline %tcinline
 51 | (.:) : (c -> d) -> (a -> b -> c) -> a -> b -> d
 52 | (.:) = (.) . (.)
 53 |
 54 | ||| `on b u x y` runs the binary function b on the results of applying
 55 | ||| unary function u to two arguments x and y. From the opposite perspective,
 56 | ||| it transforms two inputs and combines the outputs.
 57 | |||
 58 | ||| ```idris example
 59 | ||| ((+) `on` f) x y = f x + f y
 60 | ||| ```
 61 | |||
 62 | ||| Typical usage:
 63 | |||
 64 | ||| ```idris example
 65 | ||| sortBy (compare `on` fst).
 66 | ||| ```
 67 | public export %tcinline
 68 | on : (b -> b -> c) -> (a -> b) -> a -> a -> c
 69 | on f g = \x, y => g x `f` g y
 70 |
 71 | export infixl 0 `on`
 72 |
 73 | ||| Takes in the first two arguments in reverse order.
 74 | ||| @ f the function to flip
 75 | public export %tcinline
 76 | flip : (f : a -> b -> c) -> b -> a -> c
 77 | flip f = \x, y => f y x
 78 |
 79 | ||| Function application.
 80 | public export %tcinline
 81 | apply : (a -> b) -> a -> b
 82 | apply f = \a => f a
 83 |
 84 | ||| Convert a function on pairs to a curried function that takes arguments separately.
 85 | ||| The curried form allows partial application.
 86 | ||| @ f the function to curry
 87 | |||
 88 | ||| ```idris example
 89 | ||| (curry swap) 1 0 = swap (1, 0)
 90 | ||| ```
 91 | public export
 92 | curry : (f : (a, b) -> c) -> a -> b -> c
 93 | curry f a b = f (a, b)
 94 |
 95 | ||| Convert a curried function that takes arguments separately to a function on pairs.
 96 | ||| @ f the function to uncurry
 97 | |||
 98 | ||| ```idris example
 99 | ||| (uncurry min) (1, 0) = min 1 0
100 | ||| ```
101 | public export
102 | uncurry : (f : a -> b -> c) -> (a, b) -> c
103 | uncurry f (a, b) = f a b
104 |
105 | ||| ($) is compiled specially to shortcut any tricky unification issues, but if
106 | ||| it did have a type this is what it would be, and it might be useful to
107 | ||| use directly sometimes (e.g. in higher order functions)
108 | public export
109 | ($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
110 | ($) f a = f a
111 |
112 | ||| Pipeline style function application, useful for chaining
113 | ||| functions into a series of transformations, reading top
114 | ||| to bottom.
115 | |||
116 | ||| ```idris example
117 | ||| [[1], [2], [3]] |> join |> map (* 2)
118 | ||| ```
119 | public export
120 | (|>) : a -> (a -> b) -> b
121 | a |> f = f a
122 |
123 | ||| Backwards pipeline style function application, similar to $.
124 | |||
125 | ||| ```idris example
126 | ||| unpack <| "hello" ++ "world"
127 | ||| ```
128 | public export
129 | (<|) : (a -> b) -> a -> b
130 | f <| a = f a
131 |
132 | -------------------
133 | -- PROOF HELPERS --
134 | -------------------
135 |
136 | ||| Equality is a congruence.
137 | public export
138 | cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b
139 | cong f Refl = Refl
140 |
141 | ||| Two-holed congruence.
142 | export
143 | -- These are natural in equational reasoning.
144 | cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d
145 | cong2 f Refl Refl = Refl
146 |
147 | ||| Dependent version of `cong`.
148 | public export
149 | depCong : {0 p : a -> Type} ->
150 |           (0 f : (x : a) -> p x) ->
151 |           {0 x1, x2 : a} ->
152 |           (prf : x1 = x2) ->
153 |           f x1 = f x2
154 | depCong f Refl = Refl
155 |
156 | ||| Dependent version of `cong2`.
157 | public export
158 | depCong2 : {0 p : a -> Type} ->
159 |            {0 q : (x : a) -> (y : p x) -> Type} ->
160 |            (0 f : (x : a) -> (y : p x) -> q x y) ->
161 |            {0 x1, x2 : a} -> (prfX : x1 = x2) ->
162 |            {0 y1 : p x1} -> {y2 : p x2} ->
163 |            (prfY : y1 = y2) -> f x1 y1 = f x2 y2
164 | depCong2 f Refl Refl = Refl
165 |
166 | ||| Irrelevant equalities can always be made relevant
167 | export
168 | irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b
169 | irrelevantEq Refl = Refl
170 |
171 | --------------
172 | -- BOOLEANS --
173 | --------------
174 |
175 | ||| Boolean Data Type.
176 | public export
177 | data Bool = False | True
178 |
179 | ||| Boolean NOT.
180 | %inline
181 | public export
182 | not : (b : Bool) -> Bool
183 | not True = False
184 | not False = True
185 |
186 | ||| Boolean AND only evaluates the second argument if the first is `True`.
187 | %inline
188 | public export
189 | (&&) : (b : Bool) -> Lazy Bool -> Bool
190 | (&&) True x = x
191 | (&&) False x = False
192 |
193 | ||| Boolean OR only evaluates the second argument if the first is `False`.
194 | %inline
195 | public export
196 | (||) : (b : Bool) -> Lazy Bool -> Bool
197 | (||) True x = True
198 | (||) False x = x
199 |
200 | ||| Non-dependent if-then-else
201 | %inline
202 | public export
203 | ifThenElse : (b : Bool) -> Lazy a -> Lazy a -> a
204 | ifThenElse True l r = l
205 | ifThenElse False l r = r
206 |
207 | %inline
208 | public export
209 | intToBool : Int -> Bool
210 | intToBool 0 = False
211 | intToBool x = True
212 |
213 | --------------
214 | -- LISTS    --
215 | --------------
216 |
217 | ||| Generic lists.
218 | public export
219 | data List a =
220 |   ||| Empty list
221 |   Nil
222 |
223 |   | ||| A non-empty list, consisting of a head element and the rest of the list.
224 |   (::) a (List a)
225 |
226 | %name List xs, ys, zs
227 |
228 | ||| Snoc lists.
229 | public export
230 | data SnocList a =
231 |   ||| Empty snoc-list
232 |   Lin
233 |
234 |   | ||| A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
235 |   (:<) (SnocList a) a
236 |
237 | %name SnocList sx, sy, sz
238 |