dd03041 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

More library functions, and a fix for building auxiliary with functions

dd03041Edwin Brady15 years ago

lib/prelude/list.idr+15

compare with master

unifiedsplit

@@ -1,5 +1,6 @@

1module prelude.list;

3+import prelude.maybe;

3import builtins;

4import builtins;

5infixr 7 :: ;

6infixr 7 :: ;

@@ -31,6 +32,13 @@ map : (a -> b) -> List a -> List b;

31map f [] = [];

32map f [] = [];

32map f (x :: xs) = f x :: map f xs;

33map f (x :: xs) = f x :: map f xs;

35+mapMaybe : (a -> Maybe b) -> List a -> List b;

36+mapMaybe f [] = [];

37+mapMaybe f (x :: xs) with f x {

38+ | Nothing = mapMaybe f xs;

39+ | Just v = v :: mapMaybe f xs;

40+}

41+

34filter : (y -> Bool) -> List y -> List y;

42filter : (y -> Bool) -> List y -> List y;

35filter pred [] = [];

43filter pred [] = [];

36filter pred (x :: xs) with (pred x, filter pred xs) {

44filter pred (x :: xs) with (pred x, filter pred xs) {

@@ -72,3 +80,10 @@ span p (x :: xs) with p x {

73break : (a -> Bool) -> List a -> (List a, List a);

81break : (a -> Bool) -> List a -> (List a, List a);

74break p = span (not . p);

82break p = span (not . p);

83+

84+split : (a -> Bool) -> List a -> List (List a);

85+split p [] = [];

86+split p xs with break p xs {

87+ | (chunk, []) = [chunk];

88+ | (chunk, (c :: rest)) = chunk :: split p rest;

89+}

lib/prelude/strings.idr+4−1

@@ -1,6 +1,7 @@

1module prelude.strings;

3import builtins;

4+import prelude.list;

5-- Some more complex string operations

6-- Some more complex string operations

@@ -33,7 +34,7 @@ pack [] = "";

33pack (x :: xs) = strCons x (pack xs);

34pack (x :: xs) = strCons x (pack xs);

35span : (Char -> Bool) -> String -> (String, String);

36span : (Char -> Bool) -> String -> (String, String);

36−span p s with strM s {

37+span p xs with strM xs {

37 span p "" | StrNil = ("", "");

38 span p "" | StrNil = ("", "");

38 span p (strCons x xs) | (StrCons _ _) with p x {

39 span p (strCons x xs) | (StrCons _ _) with p x {

39 | True with span p xs {

40 | True with span p xs {

@@ -46,3 +47,5 @@ span p s with strM s {

46break : (Char -> Bool) -> String -> (String, String);

47break : (Char -> Bool) -> String -> (String, String);

47break p = span (not . p);

48break p = span (not . p);

50+split : (Char -> Bool) -> String -> List String;

51+split p xs = map pack (split p (unpack xs));

src/Idris/ElabDecls.hs+6−3

@@ -290,7 +290,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

290 case matchClause toplhs tm of

291 Nothing -> fail "with clause does not match top level"

292 Just mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

293− lhs <- updateLHS n wname mvars ns tm w

293+ lhs <- updateLHS n wname mvars ns (fullApp tm) w

294 return $ PClause wname lhs ws rhs wheres

295 mkAux wname toplhs ns (PWith n tm_in (w:ws) wval withs)

296 = do i <- get

@@ -300,13 +300,16 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

300 withs' <- mapM (mkAuxC wname toplhs ns) withs

301 case matchClause toplhs tm of

302 Nothing -> fail "with clause does not match top level"

303− Just mvars -> do lhs <- updateLHS n wname mvars ns tm w

303+ Just mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

304 return $ PWith wname lhs ws wval withs'

305

306 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

307 = return $ substMatches mvars $

308 PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w])

309− updateLHS n wname mvars ns tm w = fail $ "Not implemented " ++ show tm

309+ updateLHS n wname mvars ns tm w = fail $ "Not implemented match " ++ show tm

310+

311+ fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

312+ fullApp x = x

310

313

311data MArgTy = IA | EA | CA deriving Show

314data MArgTy = IA | EA | CA deriving Show

312

315