0 | module Builtin
  1 |
  2 | %default total
  3 |
  4 | -- The most primitive data types; things which are used by desugaring
  5 |
  6 | -- Totality assertions
  7 |
  8 | ||| Assert to the totality checker that the given expression will always
  9 | ||| terminate.
 10 | |||
 11 | ||| The multiplicity of its argument is 1, so `assert_total` won't affect how
 12 | ||| many times variables are used. If you're not writing a linear function,
 13 | ||| this doesn't make a difference.
 14 | |||
 15 | ||| Note: assert_total can reduce at compile time, if required for unification,
 16 | ||| which might mean that it's no longer guarded a subexpression. Therefore,
 17 | ||| it is best to use it around the smallest possible subexpression.
 18 | %inline %unsafe
 19 | public export
 20 | assert_total : (1 _ : a) -> a
 21 | assert_total x = x
 22 |
 23 | ||| Assert to the totality checker that y is always structurally smaller than x
 24 | ||| (which is typically a pattern argument, and *must* be in normal form for
 25 | ||| this to work).
 26 | |||
 27 | ||| The multiplicity of x is 0, so in a linear function, you can pass values to
 28 | ||| x even if they have already been used.
 29 | ||| The multiplicity of y is 1, so `assert_smaller` won't affect how many times
 30 | ||| its y argument is used.
 31 | ||| If you're not writing a linear function, the multiplicities don't make a
 32 | ||| difference.
 33 | |||
 34 | ||| @ x the larger value (typically a pattern argument)
 35 | ||| @ y the smaller value (typically an argument to a recursive call)
 36 | %inline %unsafe
 37 | public export
 38 | assert_smaller : (0 x : a) -> (1 y : b) -> b
 39 | assert_smaller x y = y
 40 |
 41 | -- Unit type and pairs
 42 |
 43 | ||| The canonical single-element type, also known as the trivially true
 44 | ||| proposition.
 45 | public export
 46 | data Unit =
 47 |   ||| The trivial constructor for `()`.
 48 |   MkUnit
 49 |
 50 | ||| The non-dependent pair type, also known as conjunction.
 51 | public export
 52 | data Pair : Type -> Type -> Type where
 53 |   ||| A pair of elements.
 54 |   ||| @ a the left element of the pair
 55 |   ||| @ b the right element of the pair
 56 |   MkPair : {0 a, b : Type} -> (x : a) -> (y : b) -> Pair a b
 57 |
 58 | ||| Return the first element of a pair.
 59 | public export
 60 | fst : {0 a, b : Type} -> (a, b) -> a
 61 | fst (x, y) = x
 62 |
 63 | ||| Return the second element of a pair.
 64 | public export
 65 | snd : {0 a, b : Type} -> (a, b) -> b
 66 | snd (x, y) = y
 67 |
 68 | ||| Swap the elements in a pair
 69 | public export
 70 | swap : (a, b) -> (b, a)
 71 | swap (x, y) = (y, x)
 72 |
 73 | -- This directive tells auto implicit search what to use to look inside pairs
 74 | %pair Pair fst snd
 75 |
 76 | export infixr 5 #
 77 |
 78 | ||| A pair type where each component is linear
 79 | public export
 80 | data LPair : Type -> Type -> Type where
 81 |   ||| A linear pair of elements.
 82 |   ||| If you take one copy of the linear pair apart
 83 |   ||| then you only get one copy of its left and right elements.
 84 |   ||| @ a the left element of the pair
 85 |   ||| @ b the right element of the pair
 86 |   (#) : (1 _ : a) -> (1 _ : b) -> LPair a b
 87 |
 88 | namespace DPair
 89 |   ||| Dependent pairs aid in the construction of dependent types by providing
 90 |   ||| evidence that some value resides in the type.
 91 |   |||
 92 |   ||| Formally, speaking, dependent pairs represent existential quantification -
 93 |   ||| they consist of a witness for the existential claim and a proof that the
 94 |   ||| property holds for it.
 95 |   |||
 96 |   ||| @ a the value to place in the type.
 97 |   ||| @ p the dependent type that requires the value.
 98 |   public export
 99 |   record DPair a (p : a -> Type) where
100 |     constructor MkDPair
101 |     fst : a
102 |     snd : p fst
103 |
104 |   ||| A dependent variant of LPair, pairing a result value with a resource
105 |   ||| that depends on the result value
106 |   public export
107 |   data Res : (a : Type) -> (a -> Type) -> Type where
108 |        (#) : (val : a) -> (1 r : t val) -> Res a t
109 |
110 | -- The empty type
111 |
112 | ||| The empty type, also known as the trivially false proposition.
113 | |||
114 | ||| Use `void` or `absurd` to prove anything if you have a variable of type
115 | ||| `Void` in scope.
116 | public export
117 | data Void : Type where
118 |
119 | -- Equality
120 |
121 | public export
122 | data Equal : forall a, b . a -> b -> Type where
123 |      [search a b]
124 |      Refl : {0 x : a} -> Equal x x
125 |
126 | %name Equal prf
127 |
128 | export infix 6 ===, ~=~
129 |
130 | -- An equality type for when you want to assert that each side of the
131 | -- equality has the same type, but there's not other evidence available
132 | -- to help with unification
133 | public export
134 | (===) : (x : a) -> (y : a) -> Type
135 | (===) = Equal
136 |
137 | ||| Explicit heterogeneous ("John Major") equality.  Use this when Idris
138 | ||| incorrectly chooses homogeneous equality for `(=)`.
139 | ||| @ a the type of the left side
140 | ||| @ b the type of the right side
141 | ||| @ x the left side
142 | ||| @ y the right side
143 | public export
144 | (~=~) : (x : a) -> (y : b) -> Type
145 | (~=~) = Equal
146 |
147 | ||| Perform substitution in a term according to some equality.
148 | |||
149 | ||| Like `replace`, but with an explicit predicate, and applying the rewrite in
150 | ||| the other direction, which puts it in a form usable by the `rewrite` tactic
151 | ||| and term.
152 | %inline
153 | public export
154 | rewrite__impl : {0 x, y : a} -> (0 p : _) ->
155 |                 (0 rule : x = y) -> (1 val : p y) -> p x
156 | rewrite__impl p Refl prf = prf
157 |
158 | %rewrite Equal rewrite__impl
159 |
160 | ||| Perform substitution in a term according to some equality.
161 | %inline
162 | public export
163 | replace : forall x, y, p . (0 rule : x = y) -> (1 _ : p x) -> p y
164 | replace Refl prf = prf
165 |
166 | ||| Symmetry of propositional equality.
167 | %inline
168 | public export
169 | sym : (0 rule : x ~=~ y) -> y ~=~ x
170 | sym Refl = Refl
171 |
172 | ||| Transitivity of propositional equality.
173 | %inline
174 | public export
175 | trans : forall a, b, c . (0 l : a = b) -> (0 r : b = c) -> a = c
176 | trans Refl Refl = Refl
177 |
178 | ||| Injectivity of MkDPair (first components)
179 | export
180 | mkDPairInjectiveFst : MkDPair a pa === MkDPair b qb -> a === b
181 | mkDPairInjectiveFst Refl = Refl
182 |
183 | ||| Injectivity of MkDPair (snd components)
184 | export
185 | mkDPairInjectiveSnd : MkDPair a pa === MkDPair a qa -> pa === qa
186 | mkDPairInjectiveSnd Refl = Refl
187 |
188 | ||| Subvert the type checker.  This function is abstract, so it will not reduce
189 | ||| in the type checker.  Use it with care - it can result in segfaults or
190 | ||| worse!
191 | public export %inline %unsafe
192 | believe_me : a -> b -- TODO: make linear
193 | believe_me v = prim__believe_me _ _ v
194 |
195 | ||| Assert to the usage checker that the given function uses its argument linearly.
196 | public export %unsafe
197 | assert_linear : (1 f : a -> b) -> (1 val : a) -> b
198 | assert_linear = believe_me id
199 |   where
200 |     id : (1 f : a -> b) -> a -> b
201 |     id f = f
202 |
203 | export partial %unsafe
204 | idris_crash : String -> a
205 | idris_crash = prim__crash _
206 |
207 | public export %inline
208 | delay : a -> Lazy a
209 | delay x = Delay x
210 |
211 | public export %inline
212 | force : Lazy a -> a
213 | force x = Force x
214 |
215 | %stringLit fromString
216 |
217 | ||| Interface for types that can be constructed from string literals.
218 | public export
219 | interface FromString ty where
220 |   constructor MkFromString
221 |   ||| Conversion from String.
222 |   fromString : String -> ty
223 |
224 | %allow_overloads fromString
225 |
226 | %inline
227 | public export
228 | FromString String where
229 |   fromString s = s
230 |
231 | %defaulthint
232 | %inline
233 | public export
234 | defaultString : FromString String
235 | defaultString = %search
236 |
237 | %charLit fromChar
238 |
239 | ||| Interface for types that can be constructed from char literals.
240 | public export
241 | interface FromChar ty where
242 |   constructor MkFromChar
243 |   ||| Conversion from Char.
244 |   fromChar : Char -> ty
245 |
246 | %allow_overloads fromChar
247 |
248 | %inline
249 | public export
250 | FromChar Char where
251 |   fromChar s = s
252 |
253 | %defaulthint
254 | %inline
255 | public export
256 | defaultChar : FromChar Char
257 | defaultChar = %search
258 |
259 | %doubleLit fromDouble
260 |
261 | ||| Interface for types that can be constructed from double literals.
262 | public export
263 | interface FromDouble ty where
264 |   constructor MkFromDouble
265 |   ||| Conversion from Double.
266 |   fromDouble : Double -> ty
267 |
268 | %allow_overloads fromDouble
269 |
270 | %inline
271 | public export
272 | FromDouble Double where
273 |   fromDouble s = s
274 |
275 | %defaulthint
276 | %inline
277 | public export
278 | defaultDouble : FromDouble Double
279 | defaultDouble = %search
280 |