From 03b06a694499a9bad4a0bb17ad6e968e8bf3cd83 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