@@ -1103,6 +1103,7 @@ WhereOrTerminator ::= WhereBlock | Terminator;
11031103-}
11041104clause :: SyntaxInfo -> IdrisParser PClause
11051105clause syn
1106+ -- unnamed with or function clause (inside a with)
11061107 = appExtent (do
11071108 wargs <- P.try (do pushIndent; some (wExpr syn))
11081109 ist <- get
@@ -1123,6 +1124,7 @@ clause syn
11231124 let withs = concat ds
11241125 closeBlock
11251126 return $ \fc -> PWithR fc wargs wval pn withs))
1127+ -- <==
11261128 <|> do ty <- P.try (do pushIndent
11271129 ty <- simpleExpr syn
11281130 symbol "<=="
@@ -1139,23 +1141,14 @@ clause syn
11391141 ist <- get
11401142 put (ist { lastParse = Just n })
11411143 return $ PClause fc n capp [] r wheres
1142− <|> do (l, op, nfc) <- P.try (do
1143− pushIndent
1144− l <- argExpr syn
1145− (op, nfc) <- withExtent symbolicOperator
1146− when (op == "=" || op == "?=" ) $
1147− fail "infix clause definition with \"=\" and \"?=\" not supported "
1148− return (l, op, nfc))
1149− let n = expandNS syn (sUN op)
1150− r <- argExpr syn
1151− wargs <- many (wExpr syn)
1144+ -- lhs application "with" clause or function clause
1145+ <|> do pushIndent
1146+ (n, nfc, capp, wargs) <- lhs
1147+ modify $ \ist -> ist { lastParse = Just n }
11521148 (do (rs, fc) <- withExtent (rhs syn n)
11531149 let wsyn = syn { syn_namespace = [] }
11541150 (wheres, nmap) <- whereBlock n wsyn <* popIndent
11551151 <|> ([], []) <$ terminator
1156− ist <- get
1157− let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]
1158− put (ist { lastParse = Just n })
11591152 return $ PClause fc n capp wargs rs wheres) <|> (do
11601153 popIndent
11611154 ((wval, pn), fc) <- withExtent $ do
@@ -1166,41 +1159,33 @@ clause syn
11661159 openBlock
11671160 ds <- some $ fnDecl syn
11681161 closeBlock
1169− ist <- get
1170− let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]
1171− let withs = map (fillLHSD n capp wargs) $ concat ds
1172− put (ist { lastParse = Just n })
1173− return $ PWith fc n capp wargs wval pn withs)
1174− <|> do pushIndent
1175− (n_in, nfc) <- withExtent fnName; let n = expandNS syn n_in
1176− args <- many (P.try (implicitArg (syn { inPattern = True } ))
1177− <|> P.try (constraintArg (syn { inPattern = True }))
1178− <|> (fmap pexp (argExpr syn)))
1179− wargs <- many (wExpr syn)
1180− (do (r, fc) <- withExtent (rhs syn n)
1181− let capp = PApp fc (PRef nfc [nfc] n) args
1182− let wsyn = syn { syn_namespace = [] }
1183− (wheres, nmap) <- whereBlock n wsyn <* popIndent
1184− <|> ([], []) <$ terminator
1185− ist <- get
1186− put (ist { lastParse = Just n })
1187− return $ PClause fc n capp wargs r wheres) <|> (do
1188− keyword "with"
1189− ist <- get
1190− put (ist { lastParse = Just n })
1191− ((wval, pn), fc) <- withExtent $ do
1192− wval <- bracketed syn
1193− pn <- optProof
1194− return (wval, pn)
1195− openBlock
1196− ds <- some $ fnDecl syn
1197− closeBlock
1198− popIndent
1199− let capp = PApp fc (PRef nfc [nfc] n) args
12001162 let withs = map (fillLHSD n capp wargs) $ concat ds
12011163 return $ PWith fc n capp wargs wval pn withs)
12021164 <?> "function clause"
12031165 where
1166+ lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1167+ lhsInfixApp = do l <- argExpr syn
1168+ (op, nfc) <- withExtent symbolicOperator
1169+ when (op == "=" || op == "?=" ) $
1170+ fail "infix clause definition with \"=\" and \"?=\" not supported "
1171+ let n = expandNS syn (sUN op)
1172+ r <- argExpr syn
1173+ wargs <- many (wExpr syn)
1174+ return (n, nfc, [pexp l, pexp r], wargs)
1175+
1176+ lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
1177+ lhsPrefixApp = do (n, nfc) <- withExtent (expandNS syn <$> fnName)
1178+ args <- many (P.try (implicitArg (syn { inPattern = True } ))
1179+ <|> P.try (constraintArg (syn { inPattern = True }))
1180+ <|> (fmap pexp (argExpr syn)))
1181+ wargs <- many (wExpr syn)
1182+ return (n, nfc, args, wargs)
1183+
1184+ lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
1185+ lhs = do ((n, nfc, args, wargs), lhs_fc) <- withExtent (P.try lhsInfixApp <|> lhsPrefixApp)
1186+ let capp = PApp lhs_fc (PRef nfc [nfc] n) args
1187+ return (n, nfc, capp, wargs)
1188+
12041189 optProof = P.option Nothing (do keyword "proof"
12051190 n <- withExtent fnName
12061191 return (Just n))