Add S-Expression parser and circuit typechecker

1 files changed, 75 insertions, 0 deletions

diff --git a/Data/SExp.agda b/Data/SExp.agda
new file mode 100644
index 0000000..adf4325
--- /dev/null
+++ b/Data/SExp.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.SExp where
+
+open import Data.List using (List)
+open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Show using () renaming (show to showNat)
+open import Data.String.Base as String using (String; parens; intersperse; _<+>_)
+
+open List
+
+module ListBased where
+
+  data SExp : Set where
+    Atom : String → SExp
+    Nat : ℕ → SExp
+    SExps : List SExp → SExp
+
+  mutual
+    showSExp : SExp → String
+    showSExp (Atom s)   = s
+    showSExp (Nat n)    = showNat n
+    showSExp (SExps xs) = parens (intersperse " " (showList xs))
+
+    -- expanded out map for termination checker
+    showList : List SExp → List String
+    showList []       = []
+    showList (x ∷ xs) = showSExp x ∷ showList xs
+
+module PairBased where
+
+  data SExp : Set where
+    Atom : String → SExp
+    Nat : ℕ → SExp
+    Nil : SExp
+    Pair : SExp → SExp → SExp
+
+  mutual
+    showSExp : SExp → String
+    showSExp (Atom s)   = s
+    showSExp (Nat n)    = showNat n
+    showSExp Nil        = "()"
+    showSExp (Pair l r) = parens (showPair l r)
+
+    showPair : SExp → SExp → String
+    showPair x (Atom s)   = showSExp x <+> "." <+> s
+    showPair x (Nat n)    = showSExp x <+> "." <+> showNat n
+    showPair x Nil        = showSExp x
+    showPair x (Pair l r) = showSExp x <+> showPair l r
+
+open ListBased public
+open PairBased
+
+mutual
+  sexpL→sexpP : ListBased.SExp → PairBased.SExp
+  sexpL→sexpP (Atom s)  = Atom s
+  sexpL→sexpP (Nat n)   = Nat n
+  sexpL→sexpP (SExps xs) = [sexpL]→sexpP xs
+
+  [sexpL]→sexpP : List (ListBased.SExp) → PairBased.SExp
+  [sexpL]→sexpP []       = Nil
+  [sexpL]→sexpP (x ∷ xs) = Pair (sexpL→sexpP x) ([sexpL]→sexpP xs)
+
+mutual
+  sexpP→sexpL : PairBased.SExp → ListBased.SExp
+  sexpP→sexpL (Atom s)   = Atom s
+  sexpP→sexpL (Nat n)    = Nat n
+  sexpP→sexpL Nil        = SExps []
+  sexpP→sexpL (Pair x y) = SExps (sexpP→sexpL x ∷ sexpP→[sexpL] y)
+
+  sexpP→[sexpL] : PairBased.SExp → List (ListBased.SExp)
+  sexpP→[sexpL] (Atom _)   = []
+  sexpP→[sexpL] (Nat _)    = []
+  sexpP→[sexpL] Nil        = []
+  sexpP→[sexpL] (Pair x y) = sexpP→sexpL x ∷ sexpP→[sexpL] y