@@ -42,362 +42,3 @@ public %assert_total -- reduces at compile time, use with extreme care!
4242really_believe_me : a -> b
4343really_believe_me x = prim__believe_me _ _ x
4444
45−-- ---------------------------------------------------------------- [ Builtins ]
46−namespace Builtins {
47−
48−Not : Type -> Type
49−Not a = a -> _|_
50−
51−-- | Identity function.
52−id : a -> a
53−id x = x
54−
55−-- | Manually assign a type to an expression.
56−the : (a : Type) -> a -> a
57−the _ = id
58−
59−-- | Constant function.
60−const : a -> b -> a
61−const x _ = x
62−
63−-- | Return the first element of a pair.
64−fst : (s, t) -> s
65−fst (x, y) = x
66−
67−-- | Return the second element of a pair.
68−snd : (a, b) -> b
69−snd (x, y) = y
70−
71−infixl 9 .
72−
73−-- | Function composition
74−(.) : (b -> c) -> (a -> b) -> a -> c
75−(.) f g x = f (g x)
76−
77−-- | Takes in the first two arguments in reverse order.
78−flip : (a -> b -> c) -> b -> a -> c
79−flip f x y = f y x
80−
81−infixr 1 $
82−
83−-- | Function application.
84−($) : (a -> b) -> a -> b
85−f $ a = f a
86−
87−cong : {f : t -> u} -> (a = b) -> f a = f b
88−cong refl = refl
89−
90−data Dec : Type -> Type where
91− Yes : {A : Type} -> A -> Dec A
92− No : {A : Type} -> (A -> _|_) -> Dec A
93−
94−-- | Boolean Data Type
95−data Bool = False | True
96−
97−-- | Boolean elimination
98−boolElim : Bool -> |(t : a) -> |(f : a) -> a
99−boolElim True t e = t
100−boolElim False t e = e
101−
102−-- | Defines a predicate on Bool which guarantees that the value is true.
103−data so : Bool -> Type where oh : so True
104−
105−-- Syntaxtic sugar for boolean elimination.
106−syntax if [test] then [t] else [e] = boolElim test t e
107−syntax [test] "?" [t] ":" [e] = if test then t else e
108−
109−-- Boolean Operator Precedence
110−infixl 4 &&, ||
111−
112−-- | Boolean OR
113−(||) : Bool -> Bool -> Bool
114−(||) False x = x
115−(||) True _ = True
116−
117−-- | Boolean AND
118−(&&) : Bool -> Bool -> Bool
119−(&&) True x = x
120−(&&) False _ = False
121−
122−-- | Boolean NOT
123−not : Bool -> Bool
124−not True = False
125−not False = True
126−
127−-- Numerical Operator Precedence
128−infixl 5 ==, /=
129−infixl 6 <, <=, >, >=
130−infixl 7 <<, >>
131−infixl 8 +,-,++
132−infixl 9 *,/
133−
134−-- ------------------------------------------------------- [ Numeric Operators ]
135−intToBool : Int -> Bool
136−intToBool 0 = False
137−intToBool x = True
138−
139−boolOp : (a -> a -> Int) -> a -> a -> Bool
140−boolOp op x y = intToBool (op x y)
141−
142−-- | The Eq class defines inequality and equality.
143−class Eq a where
144− (==) : a -> a -> Bool
145− (/=) : a -> a -> Bool
146−
147− x /= y = not (x == y)
148− x == y = not (x /= y)
149−
150−instance Eq Int where
151− (==) = boolOp prim__eqInt
152−
153−instance Eq Integer where
154− (==) = boolOp prim__eqBigInt
155−
156−instance Eq Float where
157− (==) = boolOp prim__eqFloat
158−
159−instance Eq Char where
160− (==) = boolOp prim__eqChar
161−
162−instance Eq String where
163− (==) = boolOp prim__eqString
164−
165−instance Eq Bool where
166− True == True = True
167− True == False = False
168− False == True = False
169− False == False = True
170−
171−instance (Eq a, Eq b) => Eq (a, b) where
172− (==) (a, c) (b, d) = (a == b) && (c == d)
173−
174−
175−data Ordering = LT | EQ | GT
176−
177−instance Eq Ordering where
178− LT == LT = True
179− EQ == EQ = True
180− GT == GT = True
181− _ == _ = False
182−
183−-- | The Ord class defines comparison operations on ordered data types.
184−class Eq a => Ord a where
185− compare : a -> a -> Ordering
186−
187− (<) : a -> a -> Bool
188− (<) x y with (compare x y)
189− (<) x y | LT = True
190− (<) x y | _ = False
191−
192− (>) : a -> a -> Bool
193− (>) x y with (compare x y)
194− (>) x y | GT = True
195− (>) x y | _ = False
196−
197− (<=) : a -> a -> Bool
198− (<=) x y = x < y || x == y
199−
200− (>=) : a -> a -> Bool
201− (>=) x y = x > y || x == y
202−
203− max : a -> a -> a
204− max x y = if (x > y) then x else y
205−
206− min : a -> a -> a
207− min x y = if (x < y) then x else y
208−
209−
210−instance Ord Int where
211− compare x y = if (x == y) then EQ else
212− if (boolOp prim__sltInt x y) then LT else
213− GT
214−
215−
216−instance Ord Integer where
217− compare x y = if (x == y) then EQ else
218− if (boolOp prim__sltBigInt x y) then LT else
219− GT
220−
221−
222−instance Ord Float where
223− compare x y = if (x == y) then EQ else
224− if (boolOp prim__sltFloat x y) then LT else
225− GT
226−
227−
228−instance Ord Char where
229− compare x y = if (x == y) then EQ else
230− if (boolOp prim__sltChar x y) then LT else
231− GT
232−
233−
234−instance Ord String where
235− compare x y = if (x == y) then EQ else
236− if (boolOp prim__ltString x y) then LT else
237− GT
238−
239−
240−instance (Ord a, Ord b) => Ord (a, b) where
241− compare (xl, xr) (yl, yr) =
242− if xl /= yl
243− then compare xl yl
244− else compare xr yr
245−
246−-- | The Num class defines basic numerical arithmetic.
247−class Num a where
248− (+) : a -> a -> a
249− (-) : a -> a -> a
250− (*) : a -> a -> a
251− -- | Absolute value
252− abs : a -> a
253− -- | Conversion from Integer.
254− fromInteger : Integer -> a
255−
256−instance Num Integer where
257− (+) = prim__addBigInt
258− (-) = prim__subBigInt
259− (*) = prim__mulBigInt
260−
261− abs x = if x < 0 then -x else x
262− fromInteger = id
263−
264−instance Num Int where
265− (+) = prim__addInt
266− (-) = prim__subInt
267− (*) = prim__mulInt
268−
269− fromInteger = prim__truncBigInt_Int
270− abs x = if x < (prim__truncBigInt_Int 0) then -x else x
271−
272−
273−instance Num Float where
274− (+) = prim__addFloat
275− (-) = prim__subFloat
276− (*) = prim__mulFloat
277−
278− abs x = if x < (prim__toFloatBigInt 0) then -x else x
279− fromInteger = prim__toFloatBigInt
280−
281−instance Num Bits8 where
282− (+) = prim__addB8
283− (-) = prim__subB8
284− (*) = prim__mulB8
285− abs = id
286− fromInteger = prim__truncBigInt_B8
287−
288−instance Num Bits16 where
289− (+) = prim__addB16
290− (-) = prim__subB16
291− (*) = prim__mulB16
292− abs = id
293− fromInteger = prim__truncBigInt_B16
294−
295−instance Num Bits32 where
296− (+) = prim__addB32
297− (-) = prim__subB32
298− (*) = prim__mulB32
299− abs = id
300− fromInteger = prim__truncBigInt_B32
301−
302−instance Num Bits64 where
303− (+) = prim__addB64
304− (-) = prim__subB64
305− (*) = prim__mulB64
306− abs = id
307− fromInteger = prim__truncBigInt_B64
308−
309−instance Eq Bits8 where
310− x == y = intToBool (prim__eqB8 x y)
311−
312−instance Eq Bits16 where
313− x == y = intToBool (prim__eqB16 x y)
314−
315−instance Eq Bits32 where
316− x == y = intToBool (prim__eqB32 x y)
317−
318−instance Eq Bits64 where
319− x == y = intToBool (prim__eqB64 x y)
320−
321−instance Ord Bits8 where
322− (<) = boolOp prim__ltB8
323− (>) = boolOp prim__gtB8
324− (<=) = boolOp prim__lteB8
325− (>=) = boolOp prim__gteB8
326− compare l r = if l < r then LT
327− else if l > r then GT
328− else EQ
329−
330−instance Ord Bits16 where
331− (<) = boolOp prim__ltB16
332− (>) = boolOp prim__gtB16
333− (<=) = boolOp prim__lteB16
334− (>=) = boolOp prim__gteB16
335− compare l r = if l < r then LT
336− else if l > r then GT
337− else EQ
338−
339−instance Ord Bits32 where
340− (<) = boolOp prim__ltB32
341− (>) = boolOp prim__gtB32
342− (<=) = boolOp prim__lteB32
343− (>=) = boolOp prim__gteB32
344− compare l r = if l < r then LT
345− else if l > r then GT
346− else EQ
347−
348−instance Ord Bits64 where
349− (<) = boolOp prim__ltB64
350− (>) = boolOp prim__gtB64
351− (<=) = boolOp prim__lteB64
352− (>=) = boolOp prim__gteB64
353− compare l r = if l < r then LT
354− else if l > r then GT
355− else EQ
356−
357−-- | Integer division.
358−partial
359−div : Integer -> Integer -> Integer
360−div = prim__sdivBigInt
361−
362−-- | Integer modulus.
363−partial
364−mod : Integer -> Integer -> Integer
365−mod = prim__sremBigInt
366−
367−-- | Fractional division of two Floats.
368−(/) : Float -> Float -> Float
369−(/) = prim__divFloat
370−
371−-- -------------------------------------------------------- [ String Operators ]
372−-- | Appends two strings together.
373−(++) : String -> String -> String
374−(++) = prim__concat
375−
376−-- | Returns the first character in the specified string.
377−partial
378−strHead : String -> Char
379−strHead = prim__strHead
380−
381−-- | Returns the characters specified after the head of the string.
382−partial
383−strTail : String -> String
384−strTail = prim__strTail
385−
386−-- | Adds a character to the from of the specified string.
387−strCons : Char -> String -> String
388−strCons = prim__strCons
389−
390−-- | Returns the nth character (starting from 0) of the specified string.
391−partial
392−strIndex : String -> Int -> Char
393−strIndex = prim__strIndex
394−
395−-- | Reverses the elements within a String.
396−reverse : String -> String
397−reverse = prim__strRev
398−
399−null : Ptr
400−null = prim__null
401−
402−}
403−