some actual calc stuff

.gitignore

@@ -2,4 +2,4 @@ MAlonzo/
 out/
 *.agdai
 
-calc
+Calc

Calc.agda

@@ -1 +1,18 @@
+{-# 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")))

Makefile

@@ -0,0 +1,10 @@
+.PHONY: clean
+
+default: calc
+
+clean:
+	rm -rfv MAlonzo/
+	rm -v calc
+
+calc:
+	agda -c Calc.agda

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

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)