b2f6cc3 · Idris-dev · git.iko.soy

lib/builtins.idr+9

compare with master

unifiedsplit

@@ -26,6 +26,9 @@ namespace builtins {

26id : a -> a;

27id x = x;

28

29+const : a -> b -> a;

30+const x _ = x;

31+

29fst : (s, t) -> s;

32fst : (s, t) -> s;

30fst (x, y) = x;

33fst (x, y) = x;

31

34

@@ -37,6 +40,9 @@ infixl 9 .;

37(.) : (b -> c) -> (a -> b) -> a -> c;

40(.) : (b -> c) -> (a -> b) -> a -> c;

38(.) f g x = f (g x);

41(.) f g x = f (g x);

39

42

43+flip : (a -> b -> c) -> b -> a -> c;

44+flip f x y = f y x;

45+

40infixr 1 $;

46infixr 1 $;

41

47

42($) : (a -> b) -> a -> b;

48($) : (a -> b) -> a -> b;

@@ -126,6 +132,9 @@ class Eq a => Ord a where {

126

132

127 max : a -> a -> a;

133 max : a -> a -> a;

128 max x y = if (x > y) then x else y;

134 max x y = if (x > y) then x else y;

135+

136+ min : a -> a -> a;

137+ min x y = if (x < y) then x else y;

129}

138}

130

139

131

140

lib/prelude.idr+15

@@ -93,6 +93,21 @@ instance MonadPlus Maybe where {

93 mplus Nothing Nothing = Nothing;

94}

95

96+---- Functors

97+

98+class Functor (f : Set -> Set) where {

99+ fmap : (a -> b) -> f a -> f b;

100+}

101+

102+instance Functor Maybe where {

103+ fmap f (Just x) = Just (f x);

104+ fmap f Nothing = Nothing;

105+}

106+

107+instance Functor List where {

108+ fmap = map;

109+}

110+

96---- some mathematical operations

111---- some mathematical operations

97

112

98%include "math.h"

113%include "math.h"

lib/prelude/list.idr+19

@@ -38,3 +38,22 @@ filter pred (x :: xs) with (pred x, filter pred xs) {

38 filter pred (x :: xs) | (False, fxs) = fxs;

39}

40

41+merge : Ord a => List a -> List a -> List a;

42+merge xs [] = xs;

43+merge [] ys = ys;

44+merge (x :: xs) (y :: ys) = if (x < y) then (x :: merge xs (y :: ys))

45+ else (y :: merge (x :: xs) ys);

46+

47+sort : Ord a => List a -> List a;

48+sort [] = [];

49+sort [x] = [x];

50+sort xs = let s = split xs in

51+ merge (sort (fst s)) (sort (snd s)) where {

52+ splitrec : List a -> List a -> (List a -> List a) -> (List a, List a);

53+ splitrec (_ :: _ :: xs) (y :: ys) zs = splitrec xs ys (zs . ((::) y));

54+ splitrec _ ys zs = (zs [], ys);

55+

56+ split : List a -> (List a, List a);

57+ split xs = splitrec xs xs id;

58+}

59+

lib/prelude/vect.idr+4−2

@@ -10,8 +10,6 @@ instance Eq (Fin n) where {

10 fO == fO = True;

11 (fS k) == (fS k') = k == k';

12 _ == _ = False;

13−

14− x /= y = not (x == y);

15}

13}

16

14

17infixr 7 :: ;

15infixr 7 :: ;

@@ -35,3 +33,7 @@ filter p (x :: xs) with (filter p xs) {

35 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

33 = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' );

36}

34}

37

35

36+map : (a -> b) -> Vect a n -> Vect b n;

37+map f [] = [];

38+map f (x :: xs) = f x :: map f xs;

39+