From fa5beb4e2b9bafd724555c548ed5d83b79d3899b Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 4 May 2022 00:49:09 +0200
Subject: [PATCH] decimal numbers

---
 src/Quox/Lexer.idr        | 37 ++++++++++++++++++++++++++++++++++++-
 tests/src/Tests/Lexer.idr | 19 +++++++++++++++----
 2 files changed, 51 insertions(+), 5 deletions(-)

diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr
index fda0c70..f64617c 100644
--- a/src/Quox/Lexer.idr
+++ b/src/Quox/Lexer.idr
@@ -32,11 +32,19 @@ data Punc
 %runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
+||| zero and one are separate because they are
+||| quantity & dimension constants
+public export
+data Number = Zero | One | Other Nat
+
+%runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
+
 
 public export
 data Token
 = P Punc
 | Name String | Symbol String
+| N Number
 
 %runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
 
@@ -52,6 +60,30 @@ wild = exact "_" <+> reject nameCont
 symbol = exact "'" <+> name
 
 
+decimal : Lexer
+decimal =
+  digit <+> opt (many (digit <|> is '_') <+> digit)
+
+natToNumber : Nat -> Number
+natToNumber 0 = Zero
+natToNumber 1 = One
+natToNumber k = Other k
+
+toDigit : Char -> Nat
+toDigit c = cast $ ord c - ord '0'
+
+makeDec' : Nat -> String -> Maybe Nat
+makeDec' acc x with (asList x)
+  makeDec' acc ""                | []         = pure acc
+  makeDec' acc (strCons '_' str) | '_' :: lst = makeDec' acc str | lst
+  makeDec' acc (strCons d   str) | d   :: lst =
+    if d >= '0' && d <= '9' then
+      makeDec' (acc * 10 + toDigit d) str | lst
+    else
+      Nothing
+
+makeDec = fromMaybe 0 . makeDec' 0
+
 skip : Lexer -> Tokenizer (Maybe a)
 skip lex = match lex $ const Nothing
 
@@ -81,7 +113,10 @@ tokens = choice [
   match wild $ const $ Just $ P Wild,
 
   match name   $ Just . Name,
-  match symbol $ Just . Symbol . assert_total strTail
+  match symbol $ Just . Symbol . assert_total strTail,
+
+  -- [todo] other bases?
+  match (some $ digit <|> exact "_") $ Just . N . natToNumber . makeDec
 ]
 
 export
diff --git a/tests/src/Tests/Lexer.idr b/tests/src/Tests/Lexer.idr
index ceb67c6..4682612 100644
--- a/tests/src/Tests/Lexer.idr
+++ b/tests/src/Tests/Lexer.idr
@@ -77,12 +77,12 @@ tests = "lexer" :- [
 
   "punctuation" :- [
     acceptsWith' "({[:,::]})"
-      [P LParen, P LBrace, P LSquare,
-       P Colon, P Comma, P DblColon,
+      [P LParen,  P LBrace, P LSquare,
+       P Colon,   P Comma,  P DblColon,
        P RSquare, P RBrace, P RParen],
     acceptsWith' " ( { [ : , :: ] } ) "
-      [P LParen, P LBrace, P LSquare,
-       P Colon, P Comma, P DblColon,
+      [P LParen,  P LBrace, P LSquare,
+       P Colon,   P Comma,  P DblColon,
        P RSquare, P RBrace, P RParen],
     acceptsWith' "-> → => ⇒ ** × << ⊲ ∷"
       [P Arrow, P Arrow, P DblArrow, P DblArrow,
@@ -99,11 +99,22 @@ tests = "lexer" :- [
     acceptsWith' "abc'"     [Name "abc'"],
     acceptsWith' "a'b'c''"  [Name "a'b'c''"],
     acceptsWith' "abc123"   [Name "abc123"],
+    acceptsWith' "_1"       [Name "_1"],
     acceptsWith' "ab cd"    [Name "ab", Name "cd"],
     acceptsWith' "ab{--}cd" [Name "ab", Name "cd"],
     acceptsWith' "'a"       [Symbol "a"],
     acceptsWith' "'ab"      [Symbol "ab"],
     acceptsWith' "'_b"      [Symbol "_b"],
     rejects'     "'"
+  ],
+
+  "numbers" :- [
+    acceptsWith' "0"     [N Zero],
+    acceptsWith' "1"     [N One],
+    acceptsWith' "2"     [N $ Other 2],
+    acceptsWith' "69"    [N $ Other 69],
+    acceptsWith' "1_000" [N $ Other 1000],
+    todo "octal",
+    todo "hex"
   ]
 ]