From 68d8019f00dad77196a6f80c0d306e724fa7936f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 4 Dec 2023 18:48:25 +0100
Subject: [PATCH] add `let` to frontend syntax

---
 lib/Quox/Parser/FromParser.idr |  3 +++
 lib/Quox/Parser/Lexer.idr      |  3 +++
 lib/Quox/Parser/Parser.idr     | 15 +++++++++++++++
 lib/Quox/Parser/Syntax.idr     |  3 +++
 tests/Tests/Lexer.idr          |  7 +++++++
 tests/Tests/Parser.idr         | 24 ++++++++++++++++++++++++
 6 files changed, 55 insertions(+)

diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index d96645c..75c2bdf 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -264,6 +264,9 @@ mutual
         <*> fromPTermDScope ds ns [< j1] val1
         <*> pure loc
 
+    Let (qty, x, rhs) body loc =>
+      ?fromPTerm_let
+
   private
   fromPTermEnumArms : Loc -> Context' PatVar d -> Context' PatVar n ->
                       List (PTagVal, PTerm) ->
diff --git a/lib/Quox/Parser/Lexer.idr b/lib/Quox/Parser/Lexer.idr
index 7c4f26f..afd6df5 100644
--- a/lib/Quox/Parser/Lexer.idr
+++ b/lib/Quox/Parser/Lexer.idr
@@ -261,6 +261,9 @@ reserved =
    Word "caseω" `Or` Word "case#",
    Word1 "return",
    Word1 "of",
+   Word1 "let", Word1 "in",
+   Word1 "let0", Word1 "let1",
+   Word "letω" `Or` Word "let#",
    Word1 "fst", Word1 "snd",
    Word1 "_",
    Word1 "Eq",
diff --git a/lib/Quox/Parser/Parser.idr b/lib/Quox/Parser/Parser.idr
index b73044a..42e2170 100644
--- a/lib/Quox/Parser/Parser.idr
+++ b/lib/Quox/Parser/Parser.idr
@@ -585,13 +585,28 @@ where
     foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
 
 
+letIntro : FileName -> Grammar True PQty
+letIntro fname =
+      withLoc fname (PQ Zero <$ res "let0")
+  <|> withLoc fname (PQ One  <$ res "let1")
+  <|> withLoc fname (PQ Any  <$ res "letω")
+  <|> do resC "let"
+         qty fname <* needRes "." <|> defLoc fname (PQ One)
 
 export
+letTerm : FileName -> Grammar True PTerm
+letTerm fname = withLoc fname $ do
+  qty  <- letIntro fname
+  x    <- patVar fname <* mustWork (resC "=")
+  rhs  <- assert_total term fname <* mustWork (resC "in")
+  body <- assert_total term fname
+  pure $ Let (qty, x, rhs) body
 
 -- term : FileName -> Grammar True PTerm
 term fname = lamTerm fname
          <|> piTerm fname
          <|> sigmaTerm fname
+         <|> letTerm fname
 
 
 export
diff --git a/lib/Quox/Parser/Syntax.idr b/lib/Quox/Parser/Syntax.idr
index 3265fd2..4011ac5 100644
--- a/lib/Quox/Parser/Syntax.idr
+++ b/lib/Quox/Parser/Syntax.idr
@@ -100,6 +100,8 @@ namespace PTerm
       | Coe (PatVar, PTerm) PDim PDim PTerm Loc
       | Comp (PatVar, PTerm) PDim PDim PTerm PDim
              (PatVar, PTerm) (PatVar, PTerm) Loc
+
+      | Let (PQty, PatVar, PTerm) PTerm Loc
     %name PTerm s, t
 
     public export
@@ -144,6 +146,7 @@ Located PTerm where
   (Ann     _ _           loc).loc = loc
   (Coe     _ _ _ _       loc).loc = loc
   (Comp    _ _ _ _ _ _ _ loc).loc = loc
+  (Let     _ _           loc).loc = loc
 
 export
 Located PCaseBody where
diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr
index 499aab4..549de46 100644
--- a/tests/Tests/Lexer.idr
+++ b/tests/Tests/Lexer.idr
@@ -108,6 +108,13 @@ tests = "lexer" :- [
     lexes "case0" [Reserved "case0"],
     lexes "case##" [Name "case##"],
 
+    lexes "let" [Reserved "let"],
+    lexes "letω" [Reserved "letω"],
+    lexes "let#" [Reserved "letω"],
+    lexes "let1" [Reserved "let1"],
+    lexes "let0" [Reserved "let0"],
+    lexes "let##" [Name "let##"],
+
     lexes "_" [Reserved "_"],
     lexes "_a" [Name "_a"],
     lexes "a_" [Name "a_"],
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index d27ee2b..dc27730 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -411,6 +411,30 @@ tests = "parser" :- [
         (V "x" {}) _)
   ],
 
+  "let" :- [
+    parseMatch term "let x = y in z"
+      `(Let (PQ One _, PV "x" {}, V "y" {}) (V "z" {}) _),
+    parseMatch term "let0 x = y in z"
+      `(Let (PQ Zero _, PV "x" {}, V "y" {}) (V "z" {}) _),
+    parseMatch term "let1 x = y in z"
+      `(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 = y1 y2 in z1 z2"
+      `(Let (PQ One _, PV "x" {},
+             (App (V "y1" {}) (V "y2" {}) _))
+          (App (V "z1" {}) (V "z2" {}) _) _),
+    parseMatch term "let x = a in let y = b in z"
+      `(Let (PQ One _, PV "x" {}, V "a" {})
+        (Let (PQ One _, PV "y" {}, V "b" {}) (V "z" {}) _) _),
+    parseMatch term "let x = y in z ∷ Z"
+      `(Let (PQ One _, PV "x" {}, V "y" {})
+          (Ann (V "z" {}) (V "Z" {}) _) _),
+    parseMatch term "let x = y in z₁ ≡ z₂ : Z"
+      `(Let (PQ One _, PV "x" {}, V "y" {})
+          (Eq (Unused _, V "Z" {}) (V "z₁" {}) (V "z₂" {}) _) _)
+  ],
+
   "definitions" :-
   let definition = flip definition [] in [
     parseMatch definition "defω x : {a} × {b} = ('a, 'b);"