00e21ca · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Another parser fix for with

00e21caEdwin Brady15 years ago

lib/prelude/list.idr+11

compare with master

unifiedsplit

@@ -58,3 +58,14 @@ sort xs = let s = split xs in

58 else (y :: merge (x :: xs) ys);

59}

61+span : (a -> Bool) -> List a -> (List a, List a);

62+span p [] = ([], []);

63+span p (x :: xs) with p x {

64+ | True with span p xs {

65+ | (ys, zs) = (x :: ys, zs);

66+ }

67+ | False = ([], x :: xs);

68+}

69+

70+break : (a -> Bool) -> List a -> (List a, List a);

71+break p = span (not . p);

lib/prelude/strings.idr+6−3

@@ -36,9 +36,12 @@ span : (Char -> Bool) -> String -> (String, String);

36span 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 {

39+ | True with span p xs {

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

40+ | (ys, zs) = (strCons x ys, zs);

41 }

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

42+ | False = ("", strCons x xs);

43 }

44}

45+

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

47+break p = span (not . p);

src/Idris/AbsSyntax.hs+1−1

@@ -49,7 +49,7 @@ data IState = IState { tt_ctxt :: Context,

49 idris_hdrs :: [String],

50 last_proof :: Maybe (Name, [String]),

51 errLine :: Maybe Int,

52− lastParse :: Maybe (Name, PTerm, [PTerm]),

52+ lastParse :: Maybe Name,

53 ibc_write :: [IBCWrite]

54 }

src/Idris/Parser.hs+9−4

@@ -753,12 +753,14 @@ pClause syn

753 return ([], [])]

754 let capp = PApp fc (PRef fc n)

755 (iargs ++ cargs ++ map pexp args)

756+ ist <- getState

757+ setState (ist { lastParse = Just n })

756 return $ PClause n capp wargs rhs wheres)

758 return $ PClause n capp wargs rhs wheres)

757 <|> try (do wargs <- many1 (pWExpr syn)

759 <|> try (do wargs <- many1 (pWExpr syn)

758 ist <- getState

760 ist <- getState

759− (n, capp, owargs) <- case lastParse ist of

761+ n <- case lastParse ist of

760− Just t -> return t

762+ Just t -> return t

761− Nothing -> fail "Invalid clause"

763+ Nothing -> fail "Invalid clause"

762 rhs <- pRHS syn n

764 rhs <- pRHS syn n

763 let ctxt = tt_ctxt ist

765 let ctxt = tt_ctxt ist

764 let wsyn = syn { syn_namespace = [] }

766 let wsyn = syn { syn_namespace = [] }

@@ -781,6 +783,8 @@ pClause syn

781 ds <- many1 $ pFunDecl syn

783 ds <- many1 $ pFunDecl syn

782 let withs = map (fillLHSD n capp wargs) $ concat ds

784 let withs = map (fillLHSD n capp wargs) $ concat ds

783 lchar '}'

785 lchar '}'

786+ ist <- getState

787+ setState (ist { lastParse = Just n })

784 return $ PWith n capp wargs wval withs)

788 return $ PWith n capp wargs wval withs)

785

789

786 <|> try (do wargs <- many1 (pWExpr syn)

790 <|> try (do wargs <- many1 (pWExpr syn)

@@ -805,7 +809,7 @@ pClause syn

805 return ([], [])]

809 return ([], [])]

806 ist <- getState

810 ist <- getState

807 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

811 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

808− setState (ist { lastParse = Just (n, capp, wargs) })

812+ setState (ist { lastParse = Just n })

809 return $ PClause n capp wargs rhs wheres

813 return $ PClause n capp wargs rhs wheres

810

814

811 <|> do l <- pArgExpr syn

815 <|> do l <- pArgExpr syn

@@ -822,6 +826,7 @@ pClause syn

822 ist <- getState

826 ist <- getState

823 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

827 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

824 let withs = map (fillLHSD n capp wargs) $ concat ds

828 let withs = map (fillLHSD n capp wargs) $ concat ds

829+ setState (ist { lastParse = Just n })

825 return $ PWith n capp wargs wval withs

830 return $ PWith n capp wargs wval withs

826 where

831 where

827 fillLHS n capp owargs (PClauseR wargs v ws)

832 fillLHS n capp owargs (PClauseR wargs v ws)