@@ -1141,24 +1141,14 @@ clause syn
11411141 ist <- get
11421142 put (ist { lastParse = Just n })
11431143 return $ PClause fc n capp [] r wheres
1144− -- infix with or function clause
1144+ -- lhs application "with" clause or function clause
11451145 <|> do pushIndent
1146− ((n, nfc, args, wargs), lhs_fc) <- P.try $ withExtent (do
1147− l <- argExpr syn
1148− (op, nfc) <- withExtent symbolicOperator
1149− when (op == "=" || op == "?=" ) $
1150− fail "infix clause definition with \"=\" and \"?=\" not supported "
1151− let n = expandNS syn (sUN op)
1152− r <- argExpr syn
1153− wargs <- many (wExpr syn)
1154− return (n, nfc, [pexp l, pexp r], wargs))
1155− let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1146+ (n, nfc, capp, wargs) <- lhs
11561147 (do (rs, fc) <- withExtent (rhs syn n)
11571148 let wsyn = syn { syn_namespace = [] }
11581149 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11591150 <|> ([], []) <$ terminator
1160− ist <- get
1161− put (ist { lastParse = Just n })
1151+ modify $ \ist -> ist { lastParse = Just n }
11621152 return $ PClause fc n capp wargs rs wheres) <|> (do
11631153 popIndent
11641154 ((wval, pn), fc) <- withExtent $ do
@@ -1169,41 +1159,33 @@ clause syn
11691159 openBlock
11701160 ds <- some $ fnDecl syn
11711161 closeBlock
1172− ist <- get
1173− let withs = map (fillLHSD n capp wargs) $ concat ds
1174− put (ist { lastParse = Just n })
1175− return $ PWith fc n capp wargs wval pn withs)
1176− -- prefix with or function clause
1177− <|> do pushIndent
1178− ((n, nfc, args, wargs), lhs_fc) <- withExtent $ do
1179− (n, nfc) <- withExtent (expandNS syn <$> fnName)
1180− args <- many (P.try (implicitArg (syn { inPattern = True } ))
1181− <|> P.try (constraintArg (syn { inPattern = True }))
1182− <|> (fmap pexp (argExpr syn)))
1183− wargs <- many (wExpr syn)
1184− return (n, nfc, args, wargs)
1185− let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1186− (do (r, fc) <- withExtent (rhs syn n)
1187− let wsyn = syn { syn_namespace = [] }
1188− (wheres, nmap) <- whereBlock n wsyn <* popIndent
1189− <|> ([], []) <$ terminator
1190− modify $ \ist -> ist { lastParse = Just n }
1191− return $ PClause fc n capp wargs r wheres) <|> (do
1192− keyword "with"
1193− ist <- get
1194− put (ist { lastParse = Just n })
1195− ((wval, pn), fc) <- withExtent $ do
1196− wval <- bracketed syn
1197− pn <- optProof
1198− return (wval, pn)
1199− openBlock
1200− ds <- some $ fnDecl syn
1201− closeBlock
1202− popIndent
1162+ modify $ \ist -> ist { lastParse = Just n }
12031163 let withs = map (fillLHSD n capp wargs) $ concat ds
12041164 return $ PWith fc n capp wargs wval pn withs)
12051165 <?> "function clause"
12061166 where
1167+ lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
1168+ lhs = do ((n, nfc, args, wargs), lhs_fc) <- P.try $ withExtent (do
1169+ l <- argExpr syn
1170+ (op, nfc) <- withExtent symbolicOperator
1171+ when (op == "=" || op == "?=" ) $
1172+ fail "infix clause definition with \"=\" and \"?=\" not supported "
1173+ let n = expandNS syn (sUN op)
1174+ r <- argExpr syn
1175+ wargs <- many (wExpr syn)
1176+ return (n, nfc, [pexp l, pexp r], wargs))
1177+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1178+ return (n, nfc, capp, wargs)
1179+ <|> do ((n, nfc, args, wargs), lhs_fc) <- withExtent $ do
1180+ (n, nfc) <- withExtent (expandNS syn <$> fnName)
1181+ args <- many (P.try (implicitArg (syn { inPattern = True } ))
1182+ <|> P.try (constraintArg (syn { inPattern = True }))
1183+ <|> (fmap pexp (argExpr syn)))
1184+ wargs <- many (wExpr syn)
1185+ return (n, nfc, args, wargs)
1186+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1187+ return (n, nfc, capp, wargs)
1188+
12071189 optProof = P.option Nothing (do keyword "proof"
12081190 n <- withExtent fnName
12091191 return (Just n))