dd03041 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitdd030412e5027c9766775b2a8a82ac7d00986ede authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 23 Dec 2011, 15:02 (15 years ago) parent88f6bf1

3 files changed+25−4

compare with master

unifiedsplit

lib/prelude/list.idr+15 lib/prelude/strings.idr+4−1 src/Idris/ElabDecls.hs+6−3

lib/prelude/list.idr+15

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

11module prelude.list;

3+import prelude.maybe;

34import builtins;

56infixr 7 :: ;

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

3132map f [] = [];

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

3334

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+

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

3543filter pred [] = [];

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

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

7280

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

7482break 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 @@

11module prelude.strings;

33import builtins;

4+import prelude.list;

56-- Some more complex string operations

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

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

3435

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

36−span p s with strM s {

37+span p xs with strM xs {

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

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

3940 | True with span p xs {

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

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

4748break p = span (not . p);

4849

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)

290290 case matchClause toplhs tm of

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

292292 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

294294 return $ PClause wname lhs ws rhs wheres

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

296296 = do i <- get

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

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

301301 case matchClause toplhs tm of

302302 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

304304 return $ PWith wname lhs ws wval withs'

305305

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

307307 = return $ substMatches mvars $

308308 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

310313

311314data MArgTy = IA | EA | CA deriving Show

312315