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