From 4291afd51be5070a0a3f2b6df81e88c31a9776db Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 4 Dec 2023 18:21:27 +0100
Subject: [PATCH] allow fst/snd to take multiple arguments

also succ though that won't be well typed
---
 lib/Quox/Parser/Parser.idr | 28 ++++++++++++++++------------
 tests/Tests/Parser.idr     | 10 +++++++++-
 2 files changed, 25 insertions(+), 13 deletions(-)

diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index de94618..c8b7192 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -381,11 +381,24 @@ eqTerm : FileName -> Grammar True PTerm
 eqTerm fname = withLoc fname $
   resC "Eq" *> mustWork [|Eq (typeLine fname) (termArg fname) (termArg fname)|]
 
+private
+appArg : Loc -> PTerm -> Either PDim PTerm -> PTerm
+appArg loc f (Left  p) = DApp f p loc
+appArg loc f (Right s) = App  f s loc
+
+||| a dimension argument with an `@` prefix, or
+||| a term argument with no prefix
+export
+anyArg : FileName -> Grammar True (Either PDim PTerm)
+anyArg fname = dimArg fname <||> termArg fname
+
 export
 resAppTerm : FileName -> (word : String) -> (0 _ : IsReserved word) =>
              (PTerm -> Loc -> PTerm) -> Grammar True PTerm
-resAppTerm fname word f = withLoc fname $
-  resC word *> mustWork [|f (termArg fname)|]
+resAppTerm fname word f = withLoc fname $ do
+  head <- withLoc fname $ resC word *> mustWork [|f (termArg fname)|]
+  args <- many $ anyArg fname
+  pure $ \loc => foldl (appArg loc) head args
 
 export
 succTerm : FileName -> Grammar True PTerm
@@ -399,21 +412,12 @@ export
 sndTerm : FileName -> Grammar True PTerm
 sndTerm fname = resAppTerm fname "snd" Snd
 
-||| a dimension argument with an `@` prefix, or
-||| a term argument with no prefix
-export
-anyArg : FileName -> Grammar True (Either PDim PTerm)
-anyArg fname = dimArg fname <||> termArg fname
-
 export
 normalAppTerm : FileName -> Grammar True PTerm
 normalAppTerm fname = withLoc fname $ do
   head <- termArg fname
   args <- many $ anyArg fname
-  pure $ \loc => foldl (ap loc) head args
-where ap : Loc -> PTerm -> Either PDim PTerm -> PTerm
-      ap loc f (Left  p) = DApp f p loc
-      ap loc f (Right s) = App  f s loc
+  pure $ \loc => foldl (appArg loc) head args
 
 ||| application term `f x @y z`, or other terms that look like application
 ||| like `succ` or `coe`.
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index 4736e89..26b327a 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -138,7 +138,15 @@ tests = "parser" :- [
     parseMatch term "f @p"
       `(DApp (V "f" {}) (V "p" {}) _),
     parseMatch term "f x @p y"
-      `(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _)
+      `(App (DApp (App (V "f" {}) (V "x" {}) _) (V "p" {}) _) (V "y" {}) _),
+    parseMatch term "fst e"
+      `(Fst (V "e" {}) _),
+    parseMatch term "snd e"
+      `(Snd (V "e" {}) _),
+    parseMatch term "(fst e) x"
+      `(App (Fst (V "e" {}) _) (V "x" {}) _),
+    parseMatch term "fst e x"
+      `(App (Fst (V "e" {}) _) (V "x" {}) _)
   ],
 
   "annotations" :- [