d7df489 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed a 'with' bug; added char and span for Strings

commitd7df4894cac680ced600120c21a1cf1f8a60bd72 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 20 Dec 2011, 22:36 (15 years ago) parent582afe1

6 files changed+46−6

compare with master

unifiedsplit

lib/builtins.idr+1−1 lib/prelude.idr+1 lib/prelude/char.idr+25 lib/prelude/strings.idr+10 src/Idris/AbsSyntax.hs+4−1 src/Idris/ElabDecls.hs+5−4

lib/builtins.idr+1−1

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

5959

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

6161

62−infix 4 &&, ||;

62+infixl 4 &&, ||;

6363

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

6565(||) False x = x;

lib/prelude.idr+1

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

99import prelude.either;

1010import prelude.vect;

1111import prelude.strings;

12+import prelude.char;

1213

1314-- Show and instances

1415

lib/prelude/char.idrnew file+25

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

1+module prelude.char;

3+import builtins;

5+isUpper : Char -> Bool;

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

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;

3232pack [] = "";

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

3434

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 _ = "..."

10691069

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

10711071matchClause 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

10731076

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

10751078 | 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)

277277 getImps _ = []

278278

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

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

281− return $ PClauses fc o wname cs'

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

281+ return $ PClauses fc o wname cs'

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

283283 mkAuxC wname lhs ns d = return $ d

284284

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

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

293293 lhs <- updateLHS n wname mvars ns tm w

294294 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)

296296 = do i <- get

297297 let tm = addImpl i tm_in

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

299299 showImp True toplhs)

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

300301 case matchClause toplhs tm of

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

302303 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'

304305

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

306307 = return $ substMatches mvars $