git.iko.soy/Idris-dev
on master help sign in
Library changes: Please read details below!
90eb6a2Edwin Brady
libs/base/Control/Category.idr+1−1
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ class Category (cat : Type -> Type -> Type) where
9 (.) : cat b c -> cat a b -> cat a c
9 (.) : cat b c -> cat a b -> cat a c
10
10
11instance Category Morphism where
11instance Category Morphism where
12− id = Mor Builtins.id
12+ id = Mor id
13 (Mor f) . (Mor g) = Mor (f . g)
13 (Mor f) . (Mor g) = Mor (f . g)
14
14
15instance Monad m => Category (Kleislimorphism m) where
15instance Monad m => Category (Kleislimorphism m) where
libs/prelude/Builtins.idr−359
@@ -42,362 +42,3 @@ public %assert_total -- reduces at compile time, use with extreme care!
42really_believe_me : a -> b
42really_believe_me : a -> b
43really_believe_me x = prim__believe_me _ _ x
43really_believe_me x = prim__believe_me _ _ x
44
44
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−
libs/prelude/Prelude.idr+2
@@ -3,6 +3,8 @@ module Prelude
3import Builtins
3import Builtins
4import IO
4import IO
5
5
6+import Prelude.Bool
7+import Prelude.Classes
6import Prelude.Cast
8import Prelude.Cast
7import Prelude.Nat
9import Prelude.Nat
8import Prelude.Fin
10import Prelude.Fin
libs/prelude/Prelude/Basics.idrnew file+48
@@ -0,0 +1,48 @@
1+module Prelude.Basics
2+
3+Not : Type -> Type
4+Not a = a -> _|_
5+
6+-- | Identity function.
7+id : a -> a
8+id x = x
9+
10+-- | Manually assign a type to an expression.
11+the : (a : Type) -> a -> a
12+the _ = id
13+
14+-- | Constant function.
15+const : a -> b -> a
16+const x _ = x
17+
18+-- | Return the first element of a pair.
19+fst : (s, t) -> s
20+fst (x, y) = x
21+
22+-- | Return the second element of a pair.
23+snd : (a, b) -> b
24+snd (x, y) = y
25+
26+infixl 9 .
27+
28+-- | Function composition
29+(.) : (b -> c) -> (a -> b) -> a -> c
30+(.) f g x = f (g x)
31+
32+-- | Takes in the first two arguments in reverse order.
33+flip : (a -> b -> c) -> b -> a -> c
34+flip f x y = f y x
35+
36+infixr 1 $
37+
38+-- | Function application.
39+($) : (a -> b) -> a -> b
40+f $ a = f a
41+
42+cong : {f : t -> u} -> (a = b) -> f a = f b
43+cong refl = refl
44+
45+data Dec : Type -> Type where
46+ Yes : {A : Type} -> A -> Dec A
47+ No : {A : Type} -> (A -> _|_) -> Dec A
48+
libs/prelude/Prelude/Bool.idrnew file+35
@@ -0,0 +1,35 @@
1+module Prelude.Bool
2+
3+-- | Boolean Data Type
4+data Bool = False | True
5+
6+-- | Boolean elimination
7+boolElim : Bool -> |(t : a) -> |(f : a) -> a
8+boolElim True t e = t
9+boolElim False t e = e
10+
11+-- | Defines a predicate on Bool which guarantees that the value is true.
12+data so : Bool -> Type where oh : so True
13+
14+-- Syntaxtic sugar for boolean elimination.
15+syntax if [test] then [t] else [e] = boolElim test t e
16+syntax [test] "?" [t] ":" [e] = if test then t else e
17+
18+-- Boolean Operator Precedence
19+infixl 4 &&, ||
20+
21+-- | Boolean OR
22+(||) : Bool -> Bool -> Bool
23+(||) False x = x
24+(||) True _ = True
25+
26+-- | Boolean AND
27+(&&) : Bool -> Bool -> Bool
28+(&&) True x = x
29+(&&) False _ = False
30+
31+-- | Boolean NOT
32+not : Bool -> Bool
33+not True = False
34+not False = True
35+
libs/prelude/Prelude/Classes.idrnew file+250
@@ -0,0 +1,250 @@
1+module Prelude.Classes
2+
3+import Builtins
4+import Prelude.Basics
5+import Prelude.Bool
6+
7+-- Numerical Operator Precedence
8+infixl 5 ==, /=
9+infixl 6 <, <=, >, >=
10+infixl 7 <<, >>
11+infixl 8 +,-
12+infixl 9 *,/
13+
14+-- ------------------------------------------------------- [ Numeric Operators ]
15+intToBool : Int -> Bool
16+intToBool 0 = False
17+intToBool x = True
18+
19+boolOp : (a -> a -> Int) -> a -> a -> Bool
20+boolOp op x y = intToBool (op x y)
21+
22+-- | The Eq class defines inequality and equality.
23+class Eq a where
24+ (==) : a -> a -> Bool
25+ (/=) : a -> a -> Bool
26+
27+ x /= y = not (x == y)
28+ x == y = not (x /= y)
29+
30+instance Eq Int where
31+ (==) = boolOp prim__eqInt
32+
33+instance Eq Integer where
34+ (==) = boolOp prim__eqBigInt
35+
36+instance Eq Float where
37+ (==) = boolOp prim__eqFloat
38+
39+instance Eq Char where
40+ (==) = boolOp prim__eqChar
41+
42+instance Eq String where
43+ (==) = boolOp prim__eqString
44+
45+instance Eq Bool where
46+ True == True = True
47+ True == False = False
48+ False == True = False
49+ False == False = True
50+
51+instance (Eq a, Eq b) => Eq (a, b) where
52+ (==) (a, c) (b, d) = (a == b) && (c == d)
53+
54+
55+data Ordering = LT | EQ | GT
56+
57+instance Eq Ordering where
58+ LT == LT = True
59+ EQ == EQ = True
60+ GT == GT = True
61+ _ == _ = False
62+
63+-- | The Ord class defines comparison operations on ordered data types.
64+class Eq a => Ord a where
65+ compare : a -> a -> Ordering
66+
67+ (<) : a -> a -> Bool
68+ (<) x y with (compare x y)
69+ (<) x y | LT = True
70+ (<) x y | _ = False
71+
72+ (>) : a -> a -> Bool
73+ (>) x y with (compare x y)
74+ (>) x y | GT = True
75+ (>) x y | _ = False
76+
77+ (<=) : a -> a -> Bool
78+ (<=) x y = x < y || x == y
79+
80+ (>=) : a -> a -> Bool
81+ (>=) x y = x > y || x == y
82+
83+ max : a -> a -> a
84+ max x y = if (x > y) then x else y
85+
86+ min : a -> a -> a
87+ min x y = if (x < y) then x else y
88+
89+
90+instance Ord Int where
91+ compare x y = if (x == y) then EQ else
92+ if (boolOp prim__sltInt x y) then LT else
93+ GT
94+
95+
96+instance Ord Integer where
97+ compare x y = if (x == y) then EQ else
98+ if (boolOp prim__sltBigInt x y) then LT else
99+ GT
100+
101+
102+instance Ord Float where
103+ compare x y = if (x == y) then EQ else
104+ if (boolOp prim__sltFloat x y) then LT else
105+ GT
106+
107+
108+instance Ord Char where
109+ compare x y = if (x == y) then EQ else
110+ if (boolOp prim__sltChar x y) then LT else
111+ GT
112+
113+
114+instance Ord String where
115+ compare x y = if (x == y) then EQ else
116+ if (boolOp prim__ltString x y) then LT else
117+ GT
118+
119+
120+instance (Ord a, Ord b) => Ord (a, b) where
121+ compare (xl, xr) (yl, yr) =
122+ if xl /= yl
123+ then compare xl yl
124+ else compare xr yr
125+
126+-- | The Num class defines basic numerical arithmetic.
127+class Num a where
128+ (+) : a -> a -> a
129+ (-) : a -> a -> a
130+ (*) : a -> a -> a
131+ -- | Absolute value
132+ abs : a -> a
133+ -- | Conversion from Integer.
134+ fromInteger : Integer -> a
135+
136+instance Num Integer where
137+ (+) = prim__addBigInt
138+ (-) = prim__subBigInt
139+ (*) = prim__mulBigInt
140+
141+ abs x = if x < 0 then -x else x
142+ fromInteger = id
143+
144+instance Num Int where
145+ (+) = prim__addInt
146+ (-) = prim__subInt
147+ (*) = prim__mulInt
148+
149+ fromInteger = prim__truncBigInt_Int
150+ abs x = if x < (prim__truncBigInt_Int 0) then -x else x
151+
152+
153+instance Num Float where
154+ (+) = prim__addFloat
155+ (-) = prim__subFloat
156+ (*) = prim__mulFloat
157+
158+ abs x = if x < (prim__toFloatBigInt 0) then -x else x
159+ fromInteger = prim__toFloatBigInt
160+
161+instance Num Bits8 where
162+ (+) = prim__addB8
163+ (-) = prim__subB8
164+ (*) = prim__mulB8
165+ abs = id
166+ fromInteger = prim__truncBigInt_B8
167+
168+instance Num Bits16 where
169+ (+) = prim__addB16
170+ (-) = prim__subB16
171+ (*) = prim__mulB16
172+ abs = id
173+ fromInteger = prim__truncBigInt_B16
174+
175+instance Num Bits32 where
176+ (+) = prim__addB32
177+ (-) = prim__subB32
178+ (*) = prim__mulB32
179+ abs = id
180+ fromInteger = prim__truncBigInt_B32
181+
182+instance Num Bits64 where
183+ (+) = prim__addB64
184+ (-) = prim__subB64
185+ (*) = prim__mulB64
186+ abs = id
187+ fromInteger = prim__truncBigInt_B64
188+
189+instance Eq Bits8 where
190+ x == y = intToBool (prim__eqB8 x y)
191+
192+instance Eq Bits16 where
193+ x == y = intToBool (prim__eqB16 x y)
194+
195+instance Eq Bits32 where
196+ x == y = intToBool (prim__eqB32 x y)
197+
198+instance Eq Bits64 where
199+ x == y = intToBool (prim__eqB64 x y)
200+
201+instance Ord Bits8 where
202+ (<) = boolOp prim__ltB8
203+ (>) = boolOp prim__gtB8
204+ (<=) = boolOp prim__lteB8
205+ (>=) = boolOp prim__gteB8
206+ compare l r = if l < r then LT
207+ else if l > r then GT
208+ else EQ
209+
210+instance Ord Bits16 where
211+ (<) = boolOp prim__ltB16
212+ (>) = boolOp prim__gtB16
213+ (<=) = boolOp prim__lteB16
214+ (>=) = boolOp prim__gteB16
215+ compare l r = if l < r then LT
216+ else if l > r then GT
217+ else EQ
218+
219+instance Ord Bits32 where
220+ (<) = boolOp prim__ltB32
221+ (>) = boolOp prim__gtB32
222+ (<=) = boolOp prim__lteB32
223+ (>=) = boolOp prim__gteB32
224+ compare l r = if l < r then LT
225+ else if l > r then GT
226+ else EQ
227+
228+instance Ord Bits64 where
229+ (<) = boolOp prim__ltB64
230+ (>) = boolOp prim__gtB64
231+ (<=) = boolOp prim__lteB64
232+ (>=) = boolOp prim__gteB64
233+ compare l r = if l < r then LT
234+ else if l > r then GT
235+ else EQ
236+
237+-- | Integer division.
238+partial
239+div : Integer -> Integer -> Integer
240+div = prim__sdivBigInt
241+
242+-- | Integer modulus.
243+partial
244+mod : Integer -> Integer -> Integer
245+mod = prim__sremBigInt
246+
247+-- | Fractional division of two Floats.
248+(/) : Float -> Float -> Float
249+(/) = prim__divFloat
250+
libs/prelude/Prelude/Foldable.idr+2
@@ -1,6 +1,8 @@
1module Prelude.Foldable
1module Prelude.Foldable
2
2
3import Builtins
3import Builtins
4+import Prelude.Bool
5+import Prelude.Classes
4import Prelude.Algebra
6import Prelude.Algebra
5
7
6%access public
8%access public
libs/prelude/Prelude/List.idr+2
@@ -3,6 +3,7 @@ module Prelude.List
3import Builtins
3import Builtins
4
4
5import Prelude.Algebra
5import Prelude.Algebra
6+import Prelude.Basics
6import Prelude.Foldable
7import Prelude.Foldable
7import Prelude.Functor
8import Prelude.Functor
8import Prelude.Maybe
9import Prelude.Maybe
@@ -12,6 +13,7 @@ import Prelude.Nat
12%default total
13%default total
13
14
14infixr 7 ::
15infixr 7 ::
16+infixl 8 ++
15
17
16data List a
18data List a
17 = Nil
19 = Nil
libs/prelude/Prelude/Nat.idr+2
@@ -3,7 +3,9 @@ module Prelude.Nat
3import Builtins
3import Builtins
4
4
5import Prelude.Algebra
5import Prelude.Algebra
6+import Prelude.Bool
6import Prelude.Cast
7import Prelude.Cast
8+import Prelude.Classes
7
9
8%access public
10%access public
9%default total
11%default total
libs/prelude/Prelude/Strings.idr+30
@@ -7,6 +7,36 @@ import Prelude.Cast
7import Prelude.Either
7import Prelude.Either
8import Prelude.Foldable
8import Prelude.Foldable
9
9
10+-- | Appends two strings together.
11+(++) : String -> String -> String
12+(++) = prim__concat
13+
14+-- | Returns the first character in the specified string.
15+partial
16+strHead : String -> Char
17+strHead = prim__strHead
18+
19+-- | Returns the characters specified after the head of the string.
20+partial
21+strTail : String -> String
22+strTail = prim__strTail
23+
24+-- | Adds a character to the from of the specified string.
25+strCons : Char -> String -> String
26+strCons = prim__strCons
27+
28+-- | Returns the nth character (starting from 0) of the specified string.
29+partial
30+strIndex : String -> Int -> Char
31+strIndex = prim__strIndex
32+
33+-- | Reverses the elements within a String.
34+reverse : String -> String
35+reverse = prim__strRev
36+
37+null : Ptr
38+null = prim__null
39+
10-- Some more complex string operations
40-- Some more complex string operations
11
41
12data StrM : String -> Type where
42data StrM : String -> Type where
libs/prelude/prelude.ipkg+6−6
@@ -1,13 +1,13 @@
1package prelude
1package prelude
2
2
3−opts = "--noprelude --total"
3+opts = "--nobuiltins --total"
4modules = Builtins, Prelude, IO,
4modules = Builtins, Prelude, IO,
5
5
6− Prelude.Algebra, Prelude.Cast, Prelude.Nat, Prelude.Fin,
6+ Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
7+ Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,
7− Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,
8+ Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
8− Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,
9+ Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,
9− Prelude.Functor, Prelude.Foldable,
10− Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10+ Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11
11
12 Decidable.Equality
12 Decidable.Equality
13
13
src/Idris/AbsSyntaxTree.hs+1
@@ -262,6 +262,7 @@ data Opt = Filename String
262 | ShowLibdir
262 | ShowLibdir
263 | ShowIncs
263 | ShowIncs
264 | NoPrelude
264 | NoPrelude
265+ | NoBuiltins -- only for the really primitive stuff!
265 | NoREPL
266 | NoREPL
266 | OLogging Int
267 | OLogging Int
267 | Output String
268 | Output String
src/Idris/DataOpts.hs+2−2
@@ -221,9 +221,9 @@ instance Optimisable (TT Name) where
221 applyOpts (App (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _) x)
221 applyOpts (App (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _) x)
222 = applyOpts x
222 = applyOpts x
223 applyOpts (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _)
223 applyOpts (P _ (NS (UN "fromIntegerNat") ["Nat","Prelude"]) _)
224− = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)
224+ = return (App (P Ref (NS (UN "id") ["Basics","Prelude"]) Erased) Erased)
225 applyOpts (P _ (NS (UN "toIntegerNat") ["Nat","Prelude"]) _)
225 applyOpts (P _ (NS (UN "toIntegerNat") ["Nat","Prelude"]) _)
226− = return (App (P Ref (NS (UN "id") ["Builtins"]) Erased) Erased)
226+ = return (App (P Ref (NS (UN "id") ["Basics","Prelude"]) Erased) Erased)
227 applyOpts c@(P (DCon t arity) n _)
227 applyOpts c@(P (DCon t arity) n _)
228 = do i <- getIState
228 = do i <- getIState
229 case lookupCtxt n (idris_optimisation i) of
229 case lookupCtxt n (idris_optimisation i) of
src/Idris/ElabTerm.hs+1−1
@@ -687,7 +687,7 @@ resolveTC depth fn ist
687 chaser (NS n _) = chaser n
687 chaser (NS n _) = chaser n
688 chaser _ = False
688 chaser _ = False
689
689
690− needsDefault t num@(P _ (NS (UN "Num") ["Builtins"]) _) [P Bound a _]
690+ needsDefault t num@(P _ (NS (UN "Num") ["Classes","Prelude"]) _) [P Bound a _]
691 = do focus a
691 = do focus a
692 fill (RConstant (AType (ATInt ITBig))) -- default Integer
692 fill (RConstant (AType (ATInt ITBig))) -- default Integer
693 solve
693 solve
src/Idris/REPL.hs+4−1
@@ -940,6 +940,7 @@ parseArgs ("--ideslave":ns) = Ideslave : (parseArgs ns)
940parseArgs ("--client":ns) = [Client (showSep " " ns)]
940parseArgs ("--client":ns) = [Client (showSep " " ns)]
941parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
941parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)
942parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
942parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
943+parseArgs ("--nobuiltins":ns) = NoBuiltins : NoPrelude : (parseArgs ns)
943parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
944parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
944parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
945parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
945parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
946parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
@@ -1126,10 +1127,12 @@ idrisMain opts =
1126 (d:_) -> setIBCSubDir d
1127 (d:_) -> setIBCSubDir d
1127 setImportDirs importdirs
1128 setImportDirs importdirs
1128
1129
1129− addPkgDir "base"
1130 addPkgDir "prelude"
1130 addPkgDir "prelude"
1131+ addPkgDir "base"
1131 mapM_ addPkgDir pkgdirs
1132 mapM_ addPkgDir pkgdirs
1132 elabPrims
1133 elabPrims
1134+ when (not (NoBuiltins `elem` opts)) $ do x <- loadModule stdout "Builtins"
1135+ return ()
1133 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1136 when (not (NoPrelude `elem` opts)) $ do x <- loadModule stdout "Prelude"
1134 return ()
1137 return ()
1135 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner
1138 when (runrepl && not quiet && not idesl && not (isJust script)) $ iputStrLn banner