b2f6cc3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A bit more prelude

commitb2f6cc38777e83a3ff422d27f6cb0c750d9050f5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 1 Dec 2011, 01:18 (15 years ago) parentf2e3a76

4 files changed+47−2

compare with master

unifiedsplit

lib/builtins.idr+9 lib/prelude.idr+15 lib/prelude/list.idr+19 lib/prelude/vect.idr+4−2

lib/builtins.idr+9

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

2626id : a -> a;

2727id x = x;

2828

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

30+const x _ = x;

31+

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

3033fst (x, y) = x;

3134

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

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

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

3942

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

44+flip f x y = f y x;

45+

4046infixr 1 $;

4147

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

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

126132

127133 max : a -> a -> a;

128134 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;

129138}

130139

131140

lib/prelude.idr+15

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

9393 mplus Nothing Nothing = Nothing;

9494}

9595

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+

96111---- some mathematical operations

97112

98113%include "math.h"

lib/prelude/list.idr+19

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

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

3939}

4040

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 {

1010 fO == fO = True;

1111 (fS k) == (fS k') = k == k';

1212 _ == _ = False;

13−

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

1513}

1614

1715infixr 7 :: ;

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

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

3634}

3735

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

37+map f [] = [];

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

39+