keep all statements, put numbers the right way around

Calc.agda

@@ -12,11 +12,9 @@ open import Agda.Builtin.String
 open import Data.Nat.Show
 open import IO
 
-open import Expr
 open import Parse
 open import Util
 
 main : Main
 -- main = run (getLine >>= λ c → putStrLn (showResult show (evalBin (takeBin (primStringToList c)))))
-main = run (getLine >>= λ c → putStrLn (showList (showResult show) (map evalBin (takeLine (primStringToList c)))))
+main = run (getLine >>= λ c → putStrLn (showList (showResult show) (map evalBin (takeLine (primStringToList c)))))
--- "123+415\n1+2\n")))))

Expr.agda

@@ -1,14 +0,0 @@
-module Expr 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
-
-data Token : Set where
-  Digit : Nat → Token
-  Delim : Char → Token
-  Oper : Char → Token
-  Skip : Char → Token
-  Term : Token

Makefile

@@ -4,7 +4,9 @@ default: calc
 
 clean:
 	rm -rfv MAlonzo/
-	rm -v calc
+	rm -v Calc
 
 calc:
-	agda -c Calc.agda
+	agda -c Calc.agda
+
+Calc: calc

Map.agda

@@ -1,3 +1,7 @@
+module Map where
+
+-- not really used yet
+
 record Map (K V : Set) : Set where
   constructor mapOf
   field

Parse.agda

@@ -6,11 +6,17 @@ open import Agda.Builtin.Maybe
 open import Agda.Builtin.Nat
 open import Agda.Builtin.String
 
-import Data.List using (_++_)
+open import Data.List using (_++_; reverse)
 
-open import Expr
 open import Util
 
+data Token : Set where
+  Digit : Nat → Token
+  Delim : Char → Token
+  Oper : Char → Token
+  Skip : Char → Token
+  Term : Token
+
 record Result (A : Set) : Set where
   constructor emit
   field
@@ -66,7 +72,7 @@ parseNat a (x ∷ xs) with parseChar x
 takeNat : List Char → Result Nat
 takeNat s with takeCons digits s
 ...            | emit nothing rem₁ = emit nothing rem₁
-...            | emit (just xs) rem₁ with parseNat nothing xs
+...            | emit (just xs) rem₁ with parseNat nothing (reverse xs)
 ...                                     | emit nothing rem₂ = emit nothing rem₁
 ...                                     | emit (just n) rem₂ = emit (just n) rem₁
 

State.agda

@@ -1,3 +1,7 @@
+module State where
+
+-- not really used yet
+
 record State (V : Set) : Set where
   constructor state
   field

Util.agda

@@ -17,73 +17,81 @@ default n (just m) = m
 ident : {V : Set} → V → V
 ident x = x
 
+-- transform each element of a list
 map : {A B : Set} → (A → B) → List A → List B
 map f [] = []
 map f (x ∷ []) = (f x) ∷ []
 map f (x ∷ xs) = (f x) ∷ (map f xs)
 
+-- combine two lists
 zip : {V : Set} → List V → List V → List V
 zip [] [] = []
-zip [] (x ∷ []) = x ∷ []
+zip xs [] = xs
-zip [] (x ∷ xs) = x ∷ (zip [] xs)
+zip [] ys = ys
-zip (x ∷ []) [] = x ∷ []
-zip (x ∷ []) (y ∷ []) = x ∷ y ∷ []
-zip (x ∷ xs) [] = x ∷ (zip xs [])
 zip (x ∷ xs) (y ∷ ys) = x ∷ y ∷ (zip xs ys)
 
+-- get the length of a list
 len : {A : Set} → List A → Nat
 len [] = 0
 len (x ∷ xs) = suc (len xs)
 
+-- keep items that pass the predicate
 filter : {A : Set} → (A → Bool) → List A → List A
 filter f [] = []
 filter f (x ∷ xs) with f x
 ...                   | true = x ∷ filter f xs
 ...                   | false = filter f xs
 
+-- remove nothings from a list of maybes
 filterNothing : {A : Set} → List (Maybe A) → List A
 filterNothing [] = []
 filterNothing (nothing ∷ xs) = filterNothing xs
 filterNothing (just x ∷ xs) = x ∷ filterNothing xs
 
+-- take the item at the given index
 takeIndex : {A : Set} → A → List A → Nat → A
 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
 
+-- find the index of a number
 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
 
+-- find the index of a character
 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
+-- generic find if I was smarter
-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
-
 -- findAny : { A : Set } → Nat → A → List A → Nat
 -- findAny n t [] = n
 -- findAny n t (x ∷ xs) with (t ≡ x)
 -- ...                     | refl = n
 -- ...                     | _ = findAny (suc n) t xs
 
+-- append all of the items in a list
+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))
+
+-- maybe to definitely a string
+showMaybe : {V : Set} → (V → String) → Maybe V → String
+showMaybe f nothing = "nothing"
+showMaybe f (just v) = f v
+
 split : List Char → List Char → List (List Char)
 split = go [] []
   where
     go : List Char → List (List Char) → List Char → List Char → List (List Char)
-    go acc acl delims [] = acl
+    go acc acl delims [] = acc ∷ acl
     go acc acl delims (x ∷ xs) with findCharIndex 0 x delims
     ...                           | nothing = go (x ∷ acc) acl delims xs
     ...                           | _ = go [] (acc ∷ acl) delims xs