From fed48dd5eb5634a46975db7076d8c9b26469e6f0 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Fri, 24 Jan 2025 22:18:09 -0500
Subject: [PATCH] numbers: Nat parser

---
 src/Parser/Numbers.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/Parser/Numbers.md b/src/Parser/Numbers.md
index 195570f..008b649 100644
--- a/src/Parser/Numbers.md
+++ b/src/Parser/Numbers.md
@@ -9,6 +9,10 @@ import Data.Vect
 import Control.Eff
 ```
 
+<!-- idris
+import System
+-->
+
 ## Base Abstraction
 
 ```idris
@@ -52,6 +56,20 @@ hex = MkBase 16
 ```idris
 export
 nat : Base -> Parser Nat
+nat b = do
+  error <- replaceError "Expected digit"
+  (first ::: rest) <- atLeastOne error parseDigit
+  pure $ foldl (\acc, e => 10 * acc + e) first rest
+  where
+    parseDigit : Parser Nat
+    parseDigit = do
+      GotChar char <- parseChar (hasDigit b) id
+        | GotError e => throwParseError "\{show e} is not a digit"
+        | EndOfInput => throwParseError "End Of Input"
+      case digitValue b char of
+        Nothing =>
+          throwParseError "Failed to parse as base \{show b.base}: \{show char}"
+        Just x => pure x
 
 export
 natBase10 : Parser Nat