c3427e8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

with parsing fix

c3427e8Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+2

compare with master

unifiedsplit

@@ -319,6 +319,8 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

319

320data PClause' t = PClause Name t [t] t [PDecl' t]

321 | PWith Name t [t] t [PDecl' t]

322+ | PClauseR [t] t [PDecl' t]

323+ | PWithR [t] t [PDecl' t]

322 deriving Functor

324 deriving Functor

323

325

324data PData' t = PDatadecl { d_name :: Name,

326data PData' t = PDatadecl { d_name :: Name,

src/Idris/Parser.hs+16−14

@@ -753,9 +753,8 @@ pClause syn

753 return ([], [])]

754 let capp = PApp fc (PRef fc n)

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

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

757 return $ PClause n capp wargs rhs wheres)

756 return $ PClause n capp wargs rhs wheres)

758− <|> try (do wargs <- many (pWExpr syn)

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

759 ist <- getState

758 ist <- getState

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

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

761 Just t -> return t

760 Just t -> return t

@@ -766,7 +765,7 @@ pClause syn

766 (wheres, nmap) <- choice [pWhereblock n wsyn,

765 (wheres, nmap) <- choice [pWhereblock n wsyn,

767 do lchar ';'

766 do lchar ';'

768 return ([], [])]

767 return ([], [])]

769− return $ PClause n capp (owargs ++ wargs) rhs wheres)

768+ return $ PClauseR wargs rhs wheres)

770

769

771 <|> try (do n_in <- pfName; let n = expandNS syn n_in

770 <|> try (do n_in <- pfName; let n = expandNS syn n_in

772 cargs <- many (pConstraintArg syn)

771 cargs <- many (pConstraintArg syn)

@@ -776,28 +775,22 @@ pClause syn

776 wargs <- many (pWExpr syn)

775 wargs <- many (pWExpr syn)

777 let capp = PApp fc (PRef fc n)

776 let capp = PApp fc (PRef fc n)

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

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

779− ist <- getState

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

781 reserved "with"

778 reserved "with"

782 wval <- pExpr syn

779 wval <- pExpr syn

783 lchar '{'

780 lchar '{'

784 ds <- many1 $ pFunDecl syn

781 ds <- many1 $ pFunDecl syn

785− let withs = concat ds

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

786 lchar '}'

783 lchar '}'

787 return $ PWith n capp wargs wval withs)

784 return $ PWith n capp wargs wval withs)

788

785

789− <|> try (do wargs <- many (pWExpr syn)

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

790 reserved "with"

787 reserved "with"

791− ist <- getState

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

793− Just t -> return t

794− Nothing -> fail "Invalid clause"

795 wval <- pExpr syn

788 wval <- pExpr syn

796 lchar '{'

789 lchar '{'

797 ds <- many1 $ pFunDecl syn

790 ds <- many1 $ pFunDecl syn

798 let withs = concat ds

791 let withs = concat ds

799 lchar '}'

792 lchar '}'

800− return $ PWith n capp (owargs ++ wargs) wval withs)

793+ return $ PWithR wargs wval withs)

801

794

802 <|> do l <- pArgExpr syn

795 <|> do l <- pArgExpr syn

803 op <- operator

796 op <- operator

@@ -825,12 +818,21 @@ pClause syn

825 wval <- pExpr syn

818 wval <- pExpr syn

826 lchar '{'

819 lchar '{'

827 ds <- many1 $ pFunDecl syn

820 ds <- many1 $ pFunDecl syn

828− let withs = concat ds

829 lchar '}'

821 lchar '}'

830 ist <- getState

822 ist <- getState

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

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

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

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

833 return $ PWith n capp wargs wval withs

825 return $ PWith n capp wargs wval withs

826+ where

827+ fillLHS n capp owargs (PClauseR wargs v ws)

828+ = PClause n capp (owargs ++ wargs) v ws

829+ fillLHS n capp owargs (PWithR wargs v ws)

830+ = PWith n capp (owargs ++ wargs) v

831+ (map (fillLHSD n capp (owargs ++ wargs)) ws)

832+ fillLHS _ _ _ c = c

833+

834+ fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)

835+ fillLHSD n c a x = x

834

836

835pWExpr :: SyntaxInfo -> IParser PTerm

837pWExpr :: SyntaxInfo -> IParser PTerm

836pWExpr syn = do lchar '|'; pExpr' syn

838pWExpr syn = do lchar '|'; pExpr' syn