From 273b12e8f016fe1a716164d514af0b2683711fd2 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Thu, 3 Jul 2025 12:01:43 -0500
Subject: Add S-Expression parser and circuit typechecker

---
 Data/Circuit/Typecheck.agda | 78 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 Data/Circuit/Typecheck.agda

(limited to 'Data/Circuit/Typecheck.agda')

diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda
new file mode 100644
index 0000000..bb7e23c
--- /dev/null
+++ b/Data/Circuit/Typecheck.agda
@@ -0,0 +1,78 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Typecheck where
+
+open import Data.SExp using (SExp)
+open import Data.Hypergraph.Base using (HypergraphLabel; module Edge; module HypergraphList)
+open import Data.Circuit.Gate using (GateLabel; Gate)
+open Edge GateLabel using (Edge)
+open HypergraphList GateLabel using (Hypergraph)
+
+open import Data.List using (List; length) renaming (map to mapL)
+open import Data.List.Effectful using () renaming (module TraversableA to ListTraversable)
+open import Data.Maybe using (Maybe) renaming (map to mapM)
+open import Data.Nat using (ℕ; _<?_; _≟_)
+open import Data.String using (String)
+open import Data.Product using (_×_; _,_; Σ)
+open import Data.Vec using (Vec; []; _∷_; fromList) renaming (map to mapV)
+open import Data.Vec.Effectful using () renaming (module TraversableA to VecTraversable)
+open import Data.Maybe.Effectful using (applicative)
+open import Data.Fin using (Fin; #_; fromℕ<)
+open import Level using (0ℓ)
+
+import Relation.Binary.PropositionalEquality as ≡
+
+open List
+open SExp
+open Gate
+open Maybe
+
+gate : {n a : ℕ} (g : Gate a) → Vec (Fin n) a → Edge n
+gate g p = record { label = g; ports = p }
+
+typeCheckGateLabel : SExp → Maybe (Σ ℕ Gate)
+typeCheckGateLabel (Atom "one")  = just (1 , ONE)
+typeCheckGateLabel (Atom "zero") = just (1 , ZERO)
+typeCheckGateLabel (Atom "not")  = just (2 , NOT)
+typeCheckGateLabel (Atom "id")   = just (2 , ID)
+typeCheckGateLabel (Atom "and")  = just (3 , AND)
+typeCheckGateLabel (Atom "or")   = just (3 , OR)
+typeCheckGateLabel (Atom "xor")  = just (3 , XOR)
+typeCheckGateLabel (Atom "nand") = just (3 , NAND)
+typeCheckGateLabel (Atom "nor")  = just (3 , NOR)
+typeCheckGateLabel (Atom "xnor") = just (3 , XNOR)
+typeCheckGateLabel _ = nothing
+
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open Dec
+open VecTraversable {0ℓ} applicative using () renaming (sequenceA to vecSequenceA)
+open ListTraversable {0ℓ} applicative using () renaming (sequenceA to listSequenceA)
+
+typeCheckPort : (v : ℕ) → SExp → Maybe (Fin v)
+typeCheckPort v (Nat n) with n <? v
+... | yes n<v = just (fromℕ< n<v)
+... | no _ = nothing
+typeCheckPort _ _ = nothing
+
+typeCheckPorts : (v n : ℕ) → List SExp → Maybe (Vec (Fin v) n)
+typeCheckPorts v n xs with length xs ≟ n
+... | yes ≡.refl = vecSequenceA (mapV (typeCheckPort v) (fromList xs))
+... | no _ = nothing
+
+typeCheckGate : (v : ℕ) → SExp → Maybe (Edge v)
+typeCheckGate v (SExps (labelString ∷ ports)) with typeCheckGateLabel labelString
+... | just (n , label) = mapM (gate label) (typeCheckPorts v n ports)
+... | nothing = nothing
+typeCheckGate v _ = nothing
+
+typeCheckHeader : SExp → Maybe ℕ
+typeCheckHeader (SExps (Atom "hypergraph" ∷ Nat n ∷ [])) = just n
+typeCheckHeader _ = nothing
+
+typeCheckHypergraph : SExp → Maybe (Σ ℕ Hypergraph)
+typeCheckHypergraph (SExps (x ∷ xs)) with typeCheckHeader x
+... | nothing = nothing
+... | just n with listSequenceA (mapL (typeCheckGate n) xs)
+...   | just e = just (n , record { edges = e })
+...   | nothing = nothing
+typeCheckHypergraph _ = nothing
-- 
cgit v1.2.3