From 1e94ee8299253bb51e2049531e12f29465188216 Mon Sep 17 00:00:00 2001
From: Sean Sube <seansube@gmail.com>
Date: Tue, 27 Sep 2022 23:12:48 -0500
Subject: [PATCH] basics

---
 .gitignore |  5 +++++
 Calc.agda  |  1 +
 Expr.agda  |  6 ++++++
 Map.agda   | 14 ++++++++++++++
 Parse.agda | 33 +++++++++++++++++++++++++++++++++
 State.agda | 20 ++++++++++++++++++++
 Util.agda  | 44 ++++++++++++++++++++++++++++++++++++++++++++
 7 files changed, 123 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Calc.agda
 create mode 100644 Expr.agda
 create mode 100644 Map.agda
 create mode 100644 Parse.agda
 create mode 100644 State.agda
 create mode 100644 Util.agda

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..b705ea3
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,5 @@
+MAlonzo/
+out/
+*.agdai
+
+calc
diff --git a/Calc.agda b/Calc.agda
new file mode 100644
index 0000000..f4f30ef
--- /dev/null
+++ b/Calc.agda
@@ -0,0 +1 @@
+-- this one has main
\ No newline at end of file
diff --git a/Expr.agda b/Expr.agda
new file mode 100644
index 0000000..fcd863b
--- /dev/null
+++ b/Expr.agda
@@ -0,0 +1,6 @@
+data BinExpr : Set where
+  binE : Token → Token → Token → BinExpr
+
+evalBin : BinExpr → Maybe Nat
+evalBin (binE (Oper '+') (Digit a) (Digit b)) = just (a + b)
+evalBin (binE _ _ _) = nothing
diff --git a/Map.agda b/Map.agda
new file mode 100644
index 0000000..1857404
--- /dev/null
+++ b/Map.agda
@@ -0,0 +1,14 @@
+record Map (K V : Set) : Set where
+  constructor mapOf
+  field
+    keys : List K
+    values : List V
+
+showMap : {V : Set} → (V → String) → Map String V → String
+showMap f m = "map: " +++ (showList ident (zip (Map.keys m) (map f (Map.values m))))
+
+findMap : Map Nat Nat → Nat → Nat
+findMap m k = takeIndex 0 (Map.values m) (findIndex 0 k (Map.keys m))
+
+showNatMap : Map String Nat → String
+showNatMap m = showMap show m
diff --git a/Parse.agda b/Parse.agda
new file mode 100644
index 0000000..a697173
--- /dev/null
+++ b/Parse.agda
@@ -0,0 +1,33 @@
+data Token : Set where
+  Digit : Nat → Token
+  Delim : Char → Token
+  Oper : Char → Token
+  Term : Token
+
+parseChar : Char → Token
+parseChar '0' = Digit 0
+parseChar '1' = Digit 1
+parseChar '2' = Digit 2
+parseChar '3' = Digit 3
+parseChar '4' = Digit 4
+parseChar '5' = Digit 5
+parseChar '6' = Digit 6
+parseChar '7' = Digit 7
+parseChar '8' = Digit 8
+parseChar '9' = Digit 9
+parseChar ',' = Delim ','
+parseChar '=' = Oper '='
+parseChar '+' = Oper '+'
+parseChar _   = Term
+
+parseList : Nat → List Char → List Nat
+parseList a [] = a ∷ []
+parseList a (x ∷ xs) with parseChar x
+...                     | Digit n = parseList ((a * 10) + n) xs
+...                     | Delim s = a ∷ parseList 0 xs
+...                     | Oper o = [] -- ignore for now
+...                     | Term = []
+
+parseExpr : String → List Nat
+parseExpr "" = []
+parseExpr x = parseList 0 (primStringToList x)
diff --git a/State.agda b/State.agda
new file mode 100644
index 0000000..9002c74
--- /dev/null
+++ b/State.agda
@@ -0,0 +1,20 @@
+record State (V : Set) : Set where
+  constructor state
+  field
+    globals : Map String V
+    scopes : List (Map String V)
+
+showGlobals : State Nat → String
+showGlobals s = "globals: " +++ (showMap show (State.globals s))
+
+showScopes : State Nat → String
+showScopes s = "scopes: " +++ (showList (showMap show) (State.scopes s))
+
+showState : State Nat → String
+showState s = "state: " +++ ((showGlobals s) +++ (", " +++ (showScopes s)))
+
+smap : Map String Nat
+smap = mapOf ("foo" ∷ []) (4 ∷ [])
+
+stest : State Nat
+stest = state (smap) (smap ∷ [])
diff --git a/Util.agda b/Util.agda
new file mode 100644
index 0000000..bbcd2dc
--- /dev/null
+++ b/Util.agda
@@ -0,0 +1,44 @@
+module Util where
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.List
+open import Agda.Builtin.Maybe
+open import Agda.Builtin.Nat
+
+ident : {V : Set} → V → V
+ident x = x
+
+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)
+
+zip : {V : Set} → List V → List V → List V
+zip [] [] = []
+zip [] (x ∷ []) = x ∷ []
+zip [] (x ∷ xs) = x ∷ (zip [] xs)
+zip (x ∷ []) [] = x ∷ []
+zip (x ∷ []) (y ∷ []) = x ∷ y ∷ []
+zip (x ∷ xs) [] = x ∷ (zip xs [])
+zip (x ∷ xs) (y ∷ ys) = x ∷ y ∷ (zip xs ys)
+
+len : {A : Set} → List A → Nat
+len [] = 0
+len (x ∷ xs) = suc (len xs)
+
+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
+
+filterNothing : {A : Set} → List (Maybe A) → List A
+filterNothing [] = []
+filterNothing (nothing ∷ xs) = filterNothing xs
+filterNothing (just x ∷ xs) = x ∷ filterNothing xs
+
+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