parser stuff

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
 ]
 
 

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)

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]
 

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],

tests/Tests/Parser.idr

@@ -128,10 +128,17 @@ tests = "parser" :- [
       trejects = rejectsNote tgrm " (term)"
       erejects = rejectsNote egrm " (elim)"
   in [
-    eparses  "a"   (F "a"),
+    "universes" :- [
-    eparses  "x"   (BV 2),
+      tparses "★0"    (TYPE 0),
-    trejects "a",
+      tparses "★1000" (TYPE 1000)
-    tparses  "[a]" (FT "a"),
+    ],
-    tparses  "[x]" (BVT 2)
+
+    "variables" :- [
+      eparses  "a"   (F "a"),
+      eparses  "x"   (BV 2),
+      trejects "a",
+      tparses  "[a]" (FT "a"),
+      tparses  "[x]" (BVT 2)
+    ]
   ]
 ]