From aa4ead592a043028dae93577e30aadb3c6c88300 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 21 Dec 2023 17:54:31 +0100
Subject: [PATCH] allow "let x : A = e in s" with type annotation

---
 lib/Quox/Parser/Parser.idr | 20 +++++++++++++-------
 tests/Tests/Parser.idr     |  2 ++
 2 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index 6419c55..b34599c 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -593,15 +593,21 @@ letIntro fname =
   <|> withLoc fname (Just . PQ Any  <$ res "letω")
   <|> Nothing <$ resC "let"
 
-export
+private
 letBinder : FileName -> Maybe PQty -> Grammar True (PQty, PatVar, PTerm)
 letBinder fname mq = do
-  qty <- the (Grammar False PQty) $ case mq of
-    Just q  => pure q
-    Nothing => qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
-  x   <- patVar fname; mustWork (resC "=")
-  rhs <- term fname
-  pure $ (qty, x, rhs)
+  qty  <- letQty fname mq
+  x    <- patVar fname
+  type <- optional $ resC ":" *> term fname
+  rhs  <- resC "=" *> term fname
+  pure (qty, x, makeLetRhs rhs type)
+where
+  letQty : FileName -> Maybe PQty -> Grammar False PQty
+  letQty fname Nothing  = qty fname <* mustWork (resC ".") <|> defLoc fname (PQ One)
+  letQty fname (Just q) = pure q
+
+  makeLetRhs : PTerm -> Maybe PTerm -> PTerm
+  makeLetRhs tm ty = maybe tm (\t => Ann tm t (extendL tm.loc t.loc)) ty
 
 export
 letTerm : FileName -> Grammar True PTerm
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index e1f780a..4c0dc0f 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -422,6 +422,8 @@ tests = "parser" :- [
       `(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "letω x = y in z"
       `(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
+    parseMatch term "letω x : X = y in z"
+      `(Let (PQ Any _, PV "x" {}, Ann (V "y" {}) (V "X" {}) _) (V "z" {}) _),
     parseMatch term "let ω.x = y in z"
       `(Let (PQ Any _, PV "x" {}, V "y" {}) (V "z" {}) _),
     parseMatch term "let x = y1 y2 in z1 z2"