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

git.iko.soy/Idris-dev

Another parser fix for with

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

4 files changed+27−8

compare with master

unifiedsplit

lib/prelude/list.idr+11 lib/prelude/strings.idr+6−3 src/Idris/AbsSyntax.hs+1−1 src/Idris/Parser.hs+9−4

lib/prelude/list.idr+11

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

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

5959}

6060

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

3636span p s with strM s {

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

3838 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);

39+ | True with span p xs {

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

4141 }

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

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

4343 }

4444}

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,

4949 idris_hdrs :: [String],

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

5151 errLine :: Maybe Int,

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

52+ lastParse :: Maybe Name,

5353 ibc_write :: [IBCWrite]

5454 }

5555

src/Idris/Parser.hs+9−4

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

753753 return ([], [])]

754754 let capp = PApp fc (PRef fc n)

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

756+ ist <- getState

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

756758 return $ PClause n capp wargs rhs wheres)

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

758760 ist <- getState

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

760− Just t -> return t

761− Nothing -> fail "Invalid clause"

761+ n <- case lastParse ist of

762+ Just t -> return t

763+ Nothing -> fail "Invalid clause"

762764 rhs <- pRHS syn n

763765 let ctxt = tt_ctxt ist

764766 let wsyn = syn { syn_namespace = [] }

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

781783 ds <- many1 $ pFunDecl syn

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

783785 lchar '}'

786+ ist <- getState

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

784788 return $ PWith n capp wargs wval withs)

785789

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

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

805809 return ([], [])]

806810 ist <- getState

807811 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 })

809813 return $ PClause n capp wargs rhs wheres

810814

811815 <|> do l <- pArgExpr syn

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

822826 ist <- getState

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

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

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

825830 return $ PWith n capp wargs wval withs

826831 where

827832 fillLHS n capp owargs (PClauseR wargs v ws)