git.iko.soy/Idris-dev
on master help sign in
Moved primitive operators to builtints.idr
commit0eac224d1e3fcd9aa75131bb51f17ba67fa36e7c authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 25 Oct 2011, 20:13 (15 years ago) parent6757c47
3 files changed+87−82
compare with master
unifiedsplit
lib/builtins.idr+82 lib/list.idr+5 lib/prelude.idr−82
lib/builtins.idr+82
@@ -21,4 +21,86 @@ infixl 9 .;
2121(.) : (b -> c) -> (a -> b) -> a -> c;
2222(.) f g x = f (g x);
2323
24+data Bool = False | True;
25+
26+boolElim : (x:Bool) -> a -> a -> a;
27+boolElim True t e = t;
28+boolElim False t e = e;
29+
30+syntax if [test] then [t] else [e] = boolElim test t e;
31+
32+infixl 5 ==, /=, ==.;
33+infixl 6 <, <=, >, >=, <., <=., >., >=.;
34+infixl 7 <<, >>;
35+infixl 8 +,-,++,+.,-.;
36+infixl 9 *,/,*.,/.;
37+
38+--- Numeric operators
39+
40+intToBool : Int -> Bool;
41+intToBool 0 = False;
42+intToBool x = True;
43+
44+boolOp : (a -> a -> Int) -> a -> a -> Bool;
45+boolOp op x y = intToBool (op x y);
46+
47+(+) : Int -> Int -> Int;
48+(+) = prim__addInt;
49+
50+(-) : Int -> Int -> Int;
51+(-) = prim__subInt;
52+
53+(*) : Int -> Int -> Int;
54+(*) = prim__mulInt;
55+
56+div : Int -> Int -> Int;
57+div = prim__divInt;
58+
59+(==) : Int -> Int -> Bool;
60+(==) = boolOp prim__eqInt;
61+
62+(<) : Int -> Int -> Bool;
63+(<) = boolOp prim__ltInt;
64+
65+(<=) : Int -> Int -> Bool;
66+(<=) = boolOp prim__lteInt;
67+
68+(>) : Int -> Int -> Bool;
69+(>) = boolOp prim__gtInt;
70+
71+(>=) : Int -> Int -> Bool;
72+(>=) = boolOp prim__gteInt;
73+
74+(+.) : Float -> Float -> Float;
75+(+.) = prim__addFloat;
76+
77+(-.) : Float -> Float -> Float;
78+(-.) = prim__subFloat;
79+
80+(*.) : Float -> Float -> Float;
81+(*.) = prim__mulFloat;
82+
83+(/.) : Float -> Float -> Float;
84+(/.) = prim__divFloat;
85+
86+(==.) : Float -> Float -> Bool;
87+(==.) = boolOp prim__eqFloat;
88+
89+(<.) : Float -> Float -> Bool;
90+(<.) = boolOp prim__ltFloat;
91+
92+(<=.) : Float -> Float -> Bool;
93+(<=.) = boolOp prim__lteFloat;
94+
95+(>.) : Float -> Float -> Bool;
96+(>.) = boolOp prim__gtFloat;
97+
98+(>=.) : Float -> Float -> Bool;
99+(>=.) = boolOp prim__gteFloat;
100+
101+--- string operators
102+
103+(++) : String -> String -> String;
104+(++) = prim__concat;
105+
24106
lib/list.idr+5
@@ -1,3 +1,5 @@
1+import builtins;
2+
13data List a = Nil | Cons a (List a);
24
35rev : List a -> List a;
@@ -8,3 +10,6 @@ rev xs = revAcc Nil xs
810 revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;
911 }
1012
13+length : List a -> Int;
14+length Nil = 0;
15+length (Cons x xs) = 1 + length xs;
lib/prelude.idr−82
@@ -4,88 +4,6 @@ import list;
44import vect;
55import io;
66
7−data Bool = False | True;
8−
9−boolElim : (x:Bool) -> a -> a -> a;
10−boolElim True t e = t;
11−boolElim False t e = e;
12−
13−syntax if [test] then [t] else [e] = boolElim test t e;
14−
15−infixl 5 ==, /=, ==.;
16−infixl 6 <, <=, >, >=, <., <=., >., >=.;
17−infixl 7 <<, >>;
18−infixl 8 +,-,++,+.,-.;
19−infixl 9 *,/,*.,/.;
20−
21−--- Numeric operators
22−
23−intToBool : Int -> Bool;
24−intToBool 0 = False;
25−intToBool x = True;
26−
27−boolOp : (a -> a -> Int) -> a -> a -> Bool;
28−boolOp op x y = intToBool (op x y);
29−
30−(+) : Int -> Int -> Int;
31−(+) = prim__addInt;
32−
33−(-) : Int -> Int -> Int;
34−(-) = prim__subInt;
35−
36−(*) : Int -> Int -> Int;
37−(*) = prim__mulInt;
38−
39−div : Int -> Int -> Int;
40−div = prim__divInt;
41−
42−(==) : Int -> Int -> Bool;
43−(==) = boolOp prim__eqInt;
44−
45−(<) : Int -> Int -> Bool;
46−(<) = boolOp prim__ltInt;
47−
48−(<=) : Int -> Int -> Bool;
49−(<=) = boolOp prim__lteInt;
50−
51−(>) : Int -> Int -> Bool;
52−(>) = boolOp prim__gtInt;
53−
54−(>=) : Int -> Int -> Bool;
55−(>=) = boolOp prim__gteInt;
56−
57−(+.) : Float -> Float -> Float;
58−(+.) = prim__addFloat;
59−
60−(-.) : Float -> Float -> Float;
61−(-.) = prim__subFloat;
62−
63−(*.) : Float -> Float -> Float;
64−(*.) = prim__mulFloat;
65−
66−(/.) : Float -> Float -> Float;
67−(/.) = prim__divFloat;
68−
69−(==.) : Float -> Float -> Bool;
70−(==.) = boolOp prim__eqFloat;
71−
72−(<.) : Float -> Float -> Bool;
73−(<.) = boolOp prim__ltFloat;
74−
75−(<=.) : Float -> Float -> Bool;
76−(<=.) = boolOp prim__lteFloat;
77−
78−(>.) : Float -> Float -> Bool;
79−(>.) = boolOp prim__gtFloat;
80−
81−(>=.) : Float -> Float -> Bool;
82−(>=.) = boolOp prim__gteFloat;
83−
84−--- string operators
85−
86−(++) : String -> String -> String;
87−(++) = prim__concat;
88−
897---- some basic io
908
919putStr : String -> IO ();