From c50f49ebcb9d81032f2aaf915dbb024046d05100 Mon Sep 17 00:00:00 2001
From: Sean Sube <seansube@gmail.com>
Date: Wed, 28 Sep 2022 00:05:16 -0500
Subject: [PATCH] some actual calc stuff

---
 .gitignore |  2 +-
 Calc.agda  | 19 ++++++++++++++++++-
 Makefile   | 10 ++++++++++
 Parse.agda | 33 +++++++++++++++++++++++++++++++++
 Util.agda  | 31 +++++++++++++++++++++++++++++++
 5 files changed, 93 insertions(+), 2 deletions(-)
 create mode 100644 Makefile

diff --git a/.gitignore b/.gitignore
index b705ea3..df14629 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,4 +2,4 @@ MAlonzo/
 out/
 *.agdai
 
-calc
+Calc
diff --git a/Calc.agda b/Calc.agda
index f4f30ef..a9c594b 100644
--- a/Calc.agda
+++ b/Calc.agda
@@ -1 +1,18 @@
--- this one has main
\ No newline at end of file
+{-# OPTIONS --guardedness #-}
+
+-- this one has main
+
+module Calc where
+
+open import Agda.Builtin.Char
+open import Agda.Builtin.Nat
+open import Agda.Builtin.String
+
+open import Data.Nat.Show
+open import IO
+
+open import Parse
+open import Util
+
+main : Main
+main = run (putStrLn (showMaybe show (takeNat "123a456")))
\ No newline at end of file
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..d01f359
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,10 @@
+.PHONY: clean
+
+default: calc
+
+clean:
+	rm -rfv MAlonzo/
+	rm -v calc
+
+calc:
+	agda -c Calc.agda
\ No newline at end of file
diff --git a/Parse.agda b/Parse.agda
index a697173..be8db5c 100644
--- a/Parse.agda
+++ b/Parse.agda
@@ -1,3 +1,13 @@
+module Parse where
+
+open import Agda.Builtin.Char
+open import Agda.Builtin.List
+open import Agda.Builtin.Maybe
+open import Agda.Builtin.Nat
+open import Agda.Builtin.String
+
+open import Util
+
 data Token : Set where
   Digit : Nat → Token
   Delim : Char → Token
@@ -20,6 +30,29 @@ parseChar '=' = Oper '='
 parseChar '+' = Oper '+'
 parseChar _   = Term
 
+parseNat : Nat → List Char → Nat
+parseNat a [] = a
+parseNat a (x ∷ xs) with parseChar x
+...                     | Digit n = parseNat ((a * 10) + n) xs
+...                     | _ = a
+
+digits : List Char
+digits = primStringToList "0123456789"
+
+takeNat : String → Maybe Nat
+takeNat s with takeCons digits (primStringToList s)
+...            | [] = nothing
+...            | xs = just (parseNat 0 xs)
+
+parseList₂ : String → List Nat
+parseList₂ s with primStringToList s
+...             | [] = []
+...             | (x ∷ xs) with parseChar x
+...                           | Digit n = n ∷ []
+...                           | _ = []
+
+-- old stuff...
+
 parseList : Nat → List Char → List Nat
 parseList a [] = a ∷ []
 parseList a (x ∷ xs) with parseChar x
diff --git a/Util.agda b/Util.agda
index bbcd2dc..f6d4c59 100644
--- a/Util.agda
+++ b/Util.agda
@@ -1,9 +1,11 @@
 module Util where
 
 open import Agda.Builtin.Bool
+open import Agda.Builtin.Char
 open import Agda.Builtin.List
 open import Agda.Builtin.Maybe
 open import Agda.Builtin.Nat
+open import Agda.Builtin.String
 
 ident : {V : Set} → V → V
 ident x = x
@@ -42,3 +44,32 @@ takeIndex d [] 0 = d
 takeIndex d [] (suc x) = d
 takeIndex d (x ∷ xs) 0 = x
 takeIndex d (x ∷ xs) (suc n) = takeIndex d xs n
+
+findIndex : Nat → Nat → List Nat → Maybe Nat
+findIndex n t [] = nothing
+findIndex n t (x ∷ xs) with (t == x)
+...                       | true = just n
+...                       | false = findIndex (suc n) t xs
+
+findCharIndex : Nat → Char → List Char → Maybe Nat
+findCharIndex n t [] = nothing
+findCharIndex n t (x ∷ xs) with primCharEquality t x
+...                       | true = just n
+...                       | false = findCharIndex (suc n) t xs
+
+showList : {V : Set} → (V → String) → List V → String
+showList f [] = ""
+showList f (x ∷ []) = f x
+showList f (x ∷ xs) = primStringAppend (f x) (primStringAppend ", " (showList f xs))
+
+showMaybe : {V : Set} → (V → String) → Maybe V → String
+showMaybe f nothing = "nothing"
+showMaybe f (just v) = f v
+
+-- take consecutive occurences of a character set
+takeCons : List Char → List Char → List Char
+takeCons [] _ = []
+takeCons _ [] = []
+takeCons cs (x ∷ xs) with (findCharIndex 0 x cs)
+...                     | nothing = []
+...                     | just n = x ∷ (takeCons cs xs)