d7df489 · Idris-dev · git.iko.soy

lib/builtins.idr+1−1

compare with master

unifiedsplit

@@ -59,7 +59,7 @@ data so : Bool -> Set where oh : so True;

59

60syntax if [test] then [t] else [e] = boolElim test t e;

61

62−infix 4 &&, ||;

62+infixl 4 &&, ||;

63

64(||) : Bool -> Bool -> Bool;

65(||) False x = x;

lib/prelude.idr+1

@@ -9,6 +9,7 @@ import prelude.maybe;

9import prelude.either;

10import prelude.vect;

11import prelude.strings;

12+import prelude.char;

12

13

13-- Show and instances

14-- Show and instances

14

15

lib/prelude/char.idrnew file+25

@@ -0,0 +1,25 @@

1+module prelude.char;

2+

3+import builtins;

4+

5+isUpper : Char -> Bool;

6+isUpper x = x >= 'A' && x <= 'Z';

7+

8+isLower : Char -> Bool;

9+isLower x = x >= 'a' && x <= 'z';

10+

11+isAlpha : Char -> Bool;

12+isAlpha x = isUpper x || isLower x;

13+

14+isDigit : Char -> Bool;

15+isDigit x = (x >= '0' && x <= '9');

16+

17+isAlphaNum : Char -> Bool;

18+isAlphaNum x = isDigit x || isAlpha x;

19+

20+isSpace : Char -> Bool;

21+isSpace x = x == ' ' || x == '\t' || x == '\r' ||

22+ x == '\n' || x == '\f' || x == '\v' ||

23+ x == '\xa0';

24+

25+

lib/prelude/strings.idr+10

@@ -32,3 +32,13 @@ pack : List Char -> String;

32pack [] = "";

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

34

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

36+span p s with strM s {

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

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

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

40+ span p (strCons x xs) | (StrCons _ _) | True | (ys, zs) = (strCons x ys, zs);

41+ }

42+ span p (strCons x xs) | (StrCons _ _) | False = ("", strCons x xs);

43+ }

44+}

src/Idris/AbsSyntax.hs+4−1

@@ -1069,7 +1069,10 @@ dumpDecl _ = "..."

1069

1070matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]

1071matchClause x y = match x y where

1072− matchArg x y = match (getTm x) (getTm y)

1072+ matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))

1073+

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

1075+ fullApp x = x

1073

1076

1074 match (PApp _ f args) (PApp _ f' args')

1077 match (PApp _ f args) (PApp _ f' args')

1075 | length args == length args'

1078 | length args == length args'

src/Idris/ElabDecls.hs+5−4

@@ -277,8 +277,8 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)

277 getImps _ = []

278

279 mkAuxC wname lhs ns (PClauses fc o n cs)

280− | n == fname = do cs' <- mapM (mkAux wname lhs ns) cs

280+ | True = do cs' <- mapM (mkAux wname lhs ns) cs

281− return $ PClauses fc o wname cs'

281+ return $ PClauses fc o wname cs'

282 | otherwise = fail $ "with clause uses wrong function name " ++ show n

283 mkAuxC wname lhs ns d = return $ d

284

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

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

293 lhs <- updateLHS n wname mvars ns tm w

294 return $ PClause wname lhs ws rhs wheres

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

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

296 = do i <- get

297 let tm = addImpl i tm_in

298 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

299 showImp True toplhs)

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

300 case matchClause toplhs tm of

301 case matchClause toplhs tm of

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

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

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

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

303− return $ PWith wname lhs ws wval wheres

304+ return $ PWith wname lhs ws wval withs'

304

305

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

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

306 = return $ substMatches mvars $

307 = return $ substMatches mvars $