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 | public export
 85 | curry : ((a, b) -> c) -> a -> b -> c
 86 | curry f a b = f (a, b)
 87 |
 88 | public export
 89 | uncurry : (a -> b -> c) -> (a, b) -> c
 90 | uncurry f (a, b) = f a b
 91 |
 92 | ||| ($) is compiled specially to shortcut any tricky unification issues, but if
 93 | ||| it did have a type this is what it would be, and it might be useful to
 94 | ||| use directly sometimes (e.g. in higher order functions)
 95 | public export
 96 | ($) : forall a, b . ((x : a) -> b x) -> (x : a) -> b x
 97 | ($) f a = f a
 98 |
 99 | ||| Pipeline style function application, useful for chaining
100 | ||| functions into a series of transformations, reading top
101 | ||| to bottom.
102 | |||
103 | ||| ```idris example
104 | ||| [[1], [2], [3]] |> join |> map (* 2)
105 | ||| ```
106 | public export
107 | (|>) : a -> (a -> b) -> b
108 | a |> f = f a
109 |
110 | ||| Backwards pipeline style function application, similar to $.
111 | |||
112 | ||| ```idris example
113 | ||| unpack <| "hello" ++ "world"
114 | ||| ```
115 | public export
116 | (<|) : (a -> b) -> a -> b
117 | f <| a = f a
118 |
119 | -------------------
120 | -- PROOF HELPERS --
121 | -------------------
122 |
123 | ||| Equality is a congruence.
124 | public export
125 | cong : (0 f : t -> u) -> (0 p : a = b) -> f a = f b
126 | cong f Refl = Refl
127 |
128 | ||| Two-holed congruence.
129 | export
130 | -- These are natural in equational reasoning.
131 | cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d
132 | cong2 f Refl Refl = Refl
133 |
134 | ||| Dependent version of `cong`.
135 | public export
136 | depCong : {0 p : a -> Type} ->
137 |           (0 f : (x : a) -> p x) ->
138 |           {0 x1, x2 : a} ->
139 |           (prf : x1 = x2) ->
140 |           f x1 = f x2
141 | depCong f Refl = Refl
142 |
143 | ||| Dependent version of `cong2`.
144 | public export
145 | depCong2 : {0 p : a -> Type} ->
146 |            {0 q : (x : a) -> (y : p x) -> Type} ->
147 |            (0 f : (x : a) -> (y : p x) -> q x y) ->
148 |            {0 x1, x2 : a} -> (prfX : x1 = x2) ->
149 |            {0 y1 : p x1} -> {y2 : p x2} ->
150 |            (prfY : y1 = y2) -> f x1 y1 = f x2 y2
151 | depCong2 f Refl Refl = Refl
152 |
153 | ||| Irrelevant equalities can always be made relevant
154 | export
155 | irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b
156 | irrelevantEq Refl = Refl
157 |
158 | --------------
159 | -- BOOLEANS --
160 | --------------
161 |
162 | ||| Boolean Data Type.
163 | public export
164 | data Bool = False | True
165 |
166 | ||| Boolean NOT.
167 | %inline
168 | public export
169 | not : (b : Bool) -> Bool
170 | not True = False
171 | not False = True
172 |
173 | ||| Boolean AND only evaluates the second argument if the first is `True`.
174 | %inline
175 | public export
176 | (&&) : (b : Bool) -> Lazy Bool -> Bool
177 | (&&) True x = x
178 | (&&) False x = False
179 |
180 | ||| Boolean OR only evaluates the second argument if the first is `False`.
181 | %inline
182 | public export
183 | (||) : (b : Bool) -> Lazy Bool -> Bool
184 | (||) True x = True
185 | (||) False x = x
186 |
187 | ||| Non-dependent if-then-else
188 | %inline
189 | public export
190 | ifThenElse : (b : Bool) -> Lazy a -> Lazy a -> a
191 | ifThenElse True l r = l
192 | ifThenElse False l r = r
193 |
194 | %inline
195 | public export
196 | intToBool : Int -> Bool
197 | intToBool 0 = False
198 | intToBool x = True
199 |
200 | --------------
201 | -- LISTS    --
202 | --------------
203 |
204 | ||| Generic lists.
205 | public export
206 | data List a =
207 |   ||| Empty list
208 |   Nil
209 |
210 |   | ||| A non-empty list, consisting of a head element and the rest of the list.
211 |   (::) a (List a)
212 |
213 | %name List xs, ys, zs
214 |
215 | ||| Snoc lists.
216 | public export
217 | data SnocList a =
218 |   ||| Empty snoc-list
219 |   Lin
220 |
221 |   | ||| A non-empty snoc-list, consisting of the rest of the snoc-list and the final element.
222 |   (:<) (SnocList a) a
223 |
224 | %name SnocList sx, sy, sz
225 |