let case be the head of an application too

also succ though that won't be well typed

lib/Quox/Parser/Parser.idr

@@ -286,8 +286,66 @@ export
 universe1 : Grammar True Universe
 universe1 = universeTok <|> res "★" *> option 0 super
 
-||| argument/atomic term: single-token terms, or those with delimiters e.g.
-||| `[t]`
+
+public export
+PCaseArm : Type
+PCaseArm = (PCasePat, PTerm)
+
+export
+caseArm : FileName -> Grammar True PCaseArm
+caseArm fname =
+  [|(,) (casePat fname) (needRes "⇒" *> assert_total term fname)|]
+
+export
+checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody
+checkCaseArms loc [] = pure $ CaseEnum [] loc
+checkCaseArms loc ((PPair x y _, rhs) :: rest) =
+  if null rest then pure $ CasePair (x, y) rhs loc
+  else fatalError "unexpected pattern after pair"
+checkCaseArms loc ((PTag tag _, rhs1) :: rest) = do
+  let rest = for rest $ \case
+        (PTag tag _, rhs) => Just (tag, rhs)
+        _                 => Nothing
+  maybe (fatalError "expected all patterns to be tags")
+        (\rest => pure $ CaseEnum ((tag, rhs1) :: rest) loc) rest
+checkCaseArms loc ((PZero _, rhs1) :: rest) = do
+  let [(PSucc p q ih _, rhs2)] = rest
+    | _ => fatalError "expected succ pattern after zero"
+  pure $ CaseNat rhs1 (p, q, ih, rhs2) loc
+checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
+  let [(PZero _, rhs2)] = rest
+    | _ => fatalError "expected zero pattern after succ"
+  pure $ CaseNat rhs2 (p, q, ih, rhs1) loc
+checkCaseArms loc ((PBox x _, rhs) :: rest) =
+  if null rest then pure $ CaseBox x rhs loc
+  else fatalError "unexpected pattern after box"
+
+export
+caseBody : FileName -> Grammar True PCaseBody
+caseBody fname = do
+  body <- bounds $ delimSep "{" "}" ";" $ caseArm fname
+  let loc = makeLoc fname body.bounds
+  checkCaseArms loc body.val
+
+export
+caseReturn : FileName -> Grammar True (PatVar, PTerm)
+caseReturn fname = do
+  x   <- patVar fname <* resC "⇒" <|> unused fname
+  ret <- assert_total term fname
+  pure (x, ret)
+
+export
+caseTerm : FileName -> Grammar True PTerm
+caseTerm fname = withLoc fname $ do
+  qty <- caseIntro fname;                     commit
+  head <- mustWork $ assert_total term fname; needRes "return"
+  ret  <- mustWork $ caseReturn fname;        needRes "of"
+  body <- mustWork $ caseBody fname
+  pure $ Case qty head ret body
+
+
+||| argument/atomic term: single-token terms, or those with delimiters
+||| e.g. `[t]`. includes `case` because the end delimiter is the `}`.
 export
 termArg : FileName -> Grammar True PTerm
 termArg fname = withLoc fname $
@@ -302,6 +360,7 @@ termArg fname = withLoc fname $
   <|> STRING <$ res "String"
   <|> [|Str strLit|]
   <|> [|V qname displacement|]
+  <|> const <$> caseTerm fname
   <|> const <$> tupleTerm fname
 
 export
@@ -381,11 +440,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 +471,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`.
@@ -521,65 +584,12 @@ where
   makePi q doms cod loc =
     foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
 
-public export
-PCaseArm : Type
-PCaseArm = (PCasePat, PTerm)
+
 
 export
-caseArm : FileName -> Grammar True PCaseArm
-caseArm fname =
-  [|(,) (casePat fname) (needRes "⇒" *> assert_total term fname)|]
-
-export
-checkCaseArms : Loc -> List PCaseArm -> Grammar False PCaseBody
-checkCaseArms loc [] = pure $ CaseEnum [] loc
-checkCaseArms loc ((PPair x y _, rhs) :: rest) =
-  if null rest then pure $ CasePair (x, y) rhs loc
-  else fatalError "unexpected pattern after pair"
-checkCaseArms loc ((PTag tag _, rhs1) :: rest) = do
-  let rest = for rest $ \case
-        (PTag tag _, rhs) => Just (tag, rhs)
-        _                 => Nothing
-  maybe (fatalError "expected all patterns to be tags")
-        (\rest => pure $ CaseEnum ((tag, rhs1) :: rest) loc) rest
-checkCaseArms loc ((PZero _, rhs1) :: rest) = do
-  let [(PSucc p q ih _, rhs2)] = rest
-    | _ => fatalError "expected succ pattern after zero"
-  pure $ CaseNat rhs1 (p, q, ih, rhs2) loc
-checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
-  let [(PZero _, rhs2)] = rest
-    | _ => fatalError "expected zero pattern after succ"
-  pure $ CaseNat rhs2 (p, q, ih, rhs1) loc
-checkCaseArms loc ((PBox x _, rhs) :: rest) =
-  if null rest then pure $ CaseBox x rhs loc
-  else fatalError "unexpected pattern after box"
-
-export
-caseBody : FileName -> Grammar True PCaseBody
-caseBody fname = do
-  body <- bounds $ delimSep "{" "}" ";" $ caseArm fname
-  let loc = makeLoc fname body.bounds
-  checkCaseArms loc body.val
-
-export
-caseReturn : FileName -> Grammar True (PatVar, PTerm)
-caseReturn fname = do
-  x   <- patVar fname <* resC "⇒" <|> unused fname
-  ret <- assert_total term fname
-  pure (x, ret)
-
-export
-caseTerm : FileName -> Grammar True PTerm
-caseTerm fname = withLoc fname $ do
-  qty <- caseIntro fname;                     commit
-  head <- mustWork $ assert_total term fname; needRes "return"
-  ret  <- mustWork $ caseReturn fname;        needRes "of"
-  body <- mustWork $ caseBody fname
-  pure $ Case qty head ret body
 
 -- term : FileName -> Grammar True PTerm
 term fname = lamTerm fname
-         <|> caseTerm fname
          <|> piTerm fname
          <|> sigmaTerm fname
 

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" :- [
@@ -392,7 +400,15 @@ tests = "parser" :- [
       `(Case (PQ Any _) (V "n" {}) (Unused _, NAT _)
         (CaseNat (Nat 0 _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
     parseFails term "caseω n return A of { zero ⇒ a }",
-    parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
+    parseFails term "caseω n return ℕ of { succ ⇒ 5 }",
+    parseMatch term
+      "case1 f s return x ⇒ A x of { (l, r) ⇒ r l } x"
+      `(App
+        (Case (PQ One _) (App (V "f" {}) (V "s" {}) _)
+          (PV "x" _, App (V "A" {}) (V "x" {}) _)
+          (CasePair (PV "l" _, PV "r" _)
+                    (App (V "r" {}) (V "l" {}) _) _) _)
+        (V "x" {}) _)
   ],
 
   "definitions" :-