@@ -753,9 +753,8 @@ pClause syn
753753 return ([], [])]
754754 let capp = PApp fc (PRef fc n)
755755 (iargs ++ cargs ++ map pexp args)
756− setState (ist { lastParse = Just (n, capp, wargs) })
757756 return $ PClause n capp wargs rhs wheres)
758− <|> try (do wargs <- many (pWExpr syn)
757+ <|> try (do wargs <- many1 (pWExpr syn)
759758 ist <- getState
760759 (n, capp, owargs) <- case lastParse ist of
761760 Just t -> return t
@@ -766,7 +765,7 @@ pClause syn
766765 (wheres, nmap) <- choice [pWhereblock n wsyn,
767766 do lchar ';'
768767 return ([], [])]
769− return $ PClause n capp (owargs ++ wargs) rhs wheres)
768+ return $ PClauseR wargs rhs wheres)
770769
771770 <|> try (do n_in <- pfName; let n = expandNS syn n_in
772771 cargs <- many (pConstraintArg syn)
@@ -776,28 +775,22 @@ pClause syn
776775 wargs <- many (pWExpr syn)
777776 let capp = PApp fc (PRef fc n)
778777 (iargs ++ cargs ++ map pexp args)
779− ist <- getState
780− setState (ist { lastParse = Just (n, capp, wargs) })
781778 reserved "with"
782779 wval <- pExpr syn
783780 lchar '{'
784781 ds <- many1 $ pFunDecl syn
785− let withs = concat ds
782+ let withs = map (fillLHSD n capp wargs) $ concat ds
786783 lchar '}'
787784 return $ PWith n capp wargs wval withs)
788785
789− <|> try (do wargs <- many (pWExpr syn)
786+ <|> try (do wargs <- many1 (pWExpr syn)
790787 reserved "with"
791− ist <- getState
792− (n, capp, owargs) <- case lastParse ist of
793− Just t -> return t
794− Nothing -> fail "Invalid clause"
795788 wval <- pExpr syn
796789 lchar '{'
797790 ds <- many1 $ pFunDecl syn
798791 let withs = concat ds
799792 lchar '}'
800− return $ PWith n capp (owargs ++ wargs) wval withs)
793+ return $ PWithR wargs wval withs)
801794
802795 <|> do l <- pArgExpr syn
803796 op <- operator
@@ -825,12 +818,21 @@ pClause syn
825818 wval <- pExpr syn
826819 lchar '{'
827820 ds <- many1 $ pFunDecl syn
828− let withs = concat ds
829821 lchar '}'
830822 ist <- getState
831823 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
833825 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
834836
835837pWExpr :: SyntaxInfo -> IParser PTerm
836838pWExpr syn = do lchar '|'; pExpr' syn