decimal numbers

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