@@ -190,9 +190,7 @@ extension syn (Rule ssym ptm _)
190190{- | Parses a (normal) built-in expression
191191@
192192InternalExpr ::=
193− App
194− | MatchApp
195− | UnifyLog
193+ UnifyLog
196194 | RecordType
197195 | SimpleExpr
198196 | Lambda
@@ -202,14 +200,14 @@ InternalExpr ::=
202200 | Pi
203201 | CaseExpr
204202 | DoBlock
203+ | App
204+ | MatchApp
205205 ;
206206@
207207-}
208208internalExpr :: SyntaxInfo -> IdrisParser PTerm
209209internalExpr syn =
210− try (app syn)
211− <|> try (matchApp syn)
212− <|> unifyLog syn
210+ unifyLog syn
213211 <|> try (disamb syn)
214212 <|> noImplicits syn
215213 <|> recordType syn
@@ -220,7 +218,7 @@ internalExpr syn =
220218 <|> try (pi syn)
221219 <|> doBlock syn
222220 <|> caseExpr syn
223− <|> simpleExpr syn
221+ <|> app syn
224222 <?> "expression"
225223
226224{- | Parses a case expression
@@ -483,24 +481,6 @@ hsimpleExpr syn =
483481 <|> simpleExpr syn
484482 <?> "expression"
485483
486−{- | Parses a matching application expression
487−@
488−MatchApp ::=
489− SimpleExpr '<==' FnName
490− ;
491−@
492−-}
493−matchApp :: SyntaxInfo -> IdrisParser PTerm
494−matchApp syn = do ty <- simpleExpr syn
495− symbol "<=="
496− fc <- getFC
497− f <- fnName
498− return (PLet (sMN 0 "match")
499− ty
500− (PMatchApp fc f)
501− (PRef fc (sMN 0 "match")))
502− <?> "matching application expression"
503−
504484{- | Parses a unification log expression
505485UnifyLog ::=
506486 '%' 'unifyLog' SimpleExpr
@@ -542,7 +522,11 @@ noImplicits syn = do try (lchar '%' *> reserved "noImplicits")
542522@
543523App ::=
544524 'mkForeign' Arg Arg*
545− | SimpleExpr Arg+
525+ | MatchApp
526+ | SimpleExpr Arg*
527+ ;
528+MatchApp ::=
529+ SimpleExpr '<==' FnName
546530 ;
547531@
548532-}
@@ -552,8 +536,6 @@ app syn = do f <- reserved "mkForeign"
552536 fn <- arg syn
553537 args <- many (do notEndApp; arg syn)
554538 i <- get
555− -- mkForeign f args ==>
556− -- liftPrimIO (\w => mkForeignPrim f args w)
557539 let ap = PApp fc (PRef fc (sUN "liftPrimIO"))
558540 [pexp (PLam (sMN 0 "w")
559541 Placeholder
@@ -563,13 +545,20 @@ app syn = do f <- reserved "mkForeign"
563545 return (dslify i ap)
564546
565547 <|> do f <- simpleExpr syn
548+ (do try $ symbol "<=="
549+ fc <- getFC
550+ ff <- fnName
551+ return (PLet (sMN 0 "match")
552+ f
553+ (PMatchApp fc ff)
554+ (PRef fc (sMN 0 "match")))
555+ <?> "matching application expression") <|> (do
566556 fc <- getFC
567− args <- some (do notEndApp; arg syn)
568557 i <- get
569−-- case f of
570−-- PAppBind fc ref [] ->
571−-- return (dslify i (PAppBind fc ref args))
572− return (dslify i (PApp fc f args))
558+ args <- many (do notEndApp; arg syn)
559+ case args of
560+ [] -> return f
561+ _ -> return (dslify i (PApp fc f args)))
573562 <?> "function application"
574563 where
575564 dslify :: IState -> PTerm -> PTerm