From a26eba7d7fba5947358ad02d32fd75ea8482c321 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 9 May 2022 18:31:30 +0200
Subject: [PATCH] parser stuff

---
 lib/Quox/Lexer.idr     |  4 ++--
 lib/Quox/Parser.idr    | 15 +++++++++++++++
 lib/Quox/Token.idr     |  6 +++---
 tests/Tests/Lexer.idr  |  6 +++++-
 tests/Tests/Parser.idr | 17 ++++++++++++-----
 5 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/lib/Quox/Lexer.idr b/lib/Quox/Lexer.idr
index 511c2e7..3a299dd 100644
--- a/lib/Quox/Lexer.idr
+++ b/lib/Quox/Lexer.idr
@@ -83,12 +83,12 @@ tokens = choice [
   keyword "case" Case, keyword "of" Of,
   keyword "ω"    Omega,
   keyword "Π"    Pi,   keyword "Σ"  Sigma, keyword "W" W,
-  simple  '★'  $ K TYPE,
 
   match name   $ Name,
   match symbol $ Symbol . assert_total strTail,
 
-  match decimal $ N . natToNumber . cast
+  match decimal $ N . natToNumber . cast,
+  match (is '★' <+> decimal) $ TYPE . cast . assert_total strTail
 ]
 
 
diff --git a/lib/Quox/Parser.idr b/lib/Quox/Parser.idr
index 7975688..f9f4b09 100644
--- a/lib/Quox/Parser.idr
+++ b/lib/Quox/Parser.idr
@@ -45,14 +45,23 @@ lexParseAll grm = lex' >=> parseAll grm
 
 
 
+export
 punc : Punc -> Grammar True ()
 punc p = terminal (show p) $ \case
   P p' => if p == p' then Just () else Nothing
   _    => Nothing
 
+export
+keyword : Keyword -> Grammar True ()
+keyword k = terminal (show k) $ \case
+  K k' => if k == k' then Just () else Nothing
+  _    => Nothing
+
+export
 between : Punc -> Punc -> Grammar True a -> Grammar True a
 between opener closer inner = punc opener *> inner <* punc closer
 
+export
 parens, squares, braces : Grammar True a -> Grammar True a
 parens  = between LParen  RParen
 squares = between LSquare RSquare
@@ -67,6 +76,11 @@ number = terminal "number" $ \case
   N (Other k) => Just k
   _           => Nothing
 
+export
+universe : Grammar True Nat
+universe = terminal "universe" $ \case TYPE k => Just k; _ => Nothing
+
+export
 zero, one, omega : Grammar True ()
 zero  = terminal "0" $ \case N Zero  => Just (); _ => Nothing
 one   = terminal "1" $ \case N One   => Just (); _ => Nothing
@@ -137,6 +151,7 @@ mutual
   term : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Term d n)
   term dvars tvars =
         E <$> squares (elim {dvars, tvars})
+    <|> TYPE . U <$> universe
 
   export
   elim : (dvars : Vars d) -> (tvars : Vars n) -> Grammar True (Elim d n)
diff --git a/lib/Quox/Token.idr b/lib/Quox/Token.idr
index a997693..be0bb05 100644
--- a/lib/Quox/Token.idr
+++ b/lib/Quox/Token.idr
@@ -25,7 +25,7 @@ data Punc
 public export
 data Keyword
 = Lam | Let | In | Case | Of | Omega
-| Pi | Sigma | W | TYPE
+| Pi | Sigma | W
 
 %runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
 
@@ -41,9 +41,9 @@ data Number = Zero | One | Other Nat
 public export
 data Token
 = P Punc
-| Name String | Symbol String
-| N Number
 | K Keyword
+| Name String | Symbol String
+| N Number | TYPE Nat
 
 %runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
 
diff --git a/tests/Tests/Lexer.idr b/tests/Tests/Lexer.idr
index 04ba205..c432360 100644
--- a/tests/Tests/Lexer.idr
+++ b/tests/Tests/Lexer.idr
@@ -127,10 +127,14 @@ tests = "lexer" :- [
     acceptsWith' "Π"    [K Pi],
     acceptsWith' "Σ"    [K Sigma],
     acceptsWith' "W"    [K W],
-    acceptsWith' "★"    [K TYPE],
     acceptsWith' "WAAA" [Name "WAAA"]
   ],
 
+  "universes" :- [
+    acceptsWith' "★10"    [TYPE 10],
+    rejects'     "★"
+  ],
+
   "numbers" :- [
     acceptsWith' "0"      [N Zero],
     acceptsWith' "1"      [N One],
diff --git a/tests/Tests/Parser.idr b/tests/Tests/Parser.idr
index dfd39bc..d335a7a 100644
--- a/tests/Tests/Parser.idr
+++ b/tests/Tests/Parser.idr
@@ -128,10 +128,17 @@ tests = "parser" :- [
       trejects = rejectsNote tgrm " (term)"
       erejects = rejectsNote egrm " (elim)"
   in [
-    eparses  "a"   (F "a"),
-    eparses  "x"   (BV 2),
-    trejects "a",
-    tparses  "[a]" (FT "a"),
-    tparses  "[x]" (BVT 2)
+    "universes" :- [
+      tparses "★0"    (TYPE 0),
+      tparses "★1000" (TYPE 1000)
+    ],
+
+    "variables" :- [
+      eparses  "a"   (F "a"),
+      eparses  "x"   (BV 2),
+      trejects "a",
+      tparses  "[a]" (FT "a"),
+      tparses  "[x]" (BVT 2)
+    ]
   ]
 ]