3 files changed, 416 insertions, 0 deletions
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda
new file mode 100644
index 0000000..ce6de69
--- /dev/null
+++ b/Data/Circuit/Convert.agda
@@ -0,0 +1,201 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Convert where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Circuit.Gate using (Gate; GateLabel; cast-gate; cast-gate-is-id; subst-is-cast-gate)
+open import Data.Fin.Base using (Fin)
+open import Data.Hypergraph.Edge GateLabel using (Edge)
+open import Data.Hypergraph.Base GateLabel using (Hypergraph; sortHypergraph; mkHypergraph)
+open import Data.Hypergraph.Setoid GateLabel using (Hypergraph-Setoid; ≈-Hypergraph)
+open import Data.Permutation using (fromList-↭; toList-↭)
+open import Data.List using (length)
+open import Data.Vec.Functional using (toVec; fromVec; toList; fromList)
+open import Function.Bundles using (Equivalence; _↔_)
+open import Function.Base using (_∘_; id)
+open import Data.List.Relation.Binary.Permutation.Homogeneous using (Permutation)
+open import Data.Product.Base using (proj₁; proj₂; _×_)
+open import Data.Fin.Permutation using (flip; _⟨$⟩ˡ_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
+
+import Function.Reasoning as →-Reasoning
+import Data.List.Relation.Binary.Permutation.Propositional as L
+import Data.Vec.Functional.Relation.Binary.Permutation as V
+import DecorationFunctor.Hypergraph.Labeled as LabeledHypergraph
+
+open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′)
+
+to : {v : ℕ} → Hypergraph v → Hypergraph′ v
+to H = record
+    { h = length edges
+    ; a = arity ∘ fromList edges
+    ; j = fromVec ∘ ports ∘ fromList edges
+    ; l = label ∘ fromList edges
+    }
+  where
+    open Edge using (arity; ports; label)
+    open Hypergraph H
+
+from : {v : ℕ} → Hypergraph′ v → Hypergraph v
+from {v} H = record
+    { edges = toList asEdge
+    }
+  where
+    open Hypergraph′ H
+    asEdge : Fin h → Edge v
+    asEdge e = record { label = l e ; ports = toVec (j e) }
+
+to-cong : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → Hypergraph-same (to H) (to H′)
+to-cong {v} {H} {H′} ≈H = record
+    { ↔h = flip ρ
+    ; ≗a = ≗a
+    ; ≗j = ≗j
+    ; ≗l = ≗l
+    }
+  where
+    open Edge using (arity; ports; label)
+    open ≈-Hypergraph ≈H
+    open import Data.Fin.Permutation using (_⟨$⟩ʳ_; _⟨$⟩ˡ_; Permutation′; inverseʳ)
+    open import Data.Fin.Base using (cast)
+    open import Data.Fin.Properties using (cast-is-id)
+    ρ : Fin (length H′.edges) ↔ Fin (length H.edges)
+    ρ = proj₁ (fromList-↭ ↭edges)
+
+    open ≡.≡-Reasoning
+    edges≗ρ∘edges′ : (i : Fin (length H.edges)) → fromList H.edges i ≡ fromList H′.edges (ρ ⟨$⟩ˡ i)
+    edges≗ρ∘edges′ i = begin
+        fromList H.edges i                    ≡⟨ ≡.cong (fromList H.edges) (inverseʳ ρ) ⟨
+        fromList H.edges (ρ ⟨$⟩ʳ (ρ ⟨$⟩ˡ i))  ≡⟨ proj₂ (fromList-↭ ↭edges) (ρ ⟨$⟩ˡ i) ⟩
+        fromList H′.edges (ρ ⟨$⟩ˡ i)          ∎
+
+    ≗a : (e : Fin (Hypergraph′.h (to H)))
+        → Hypergraph′.a (to H) e
+        ≡ arity (fromList H′.edges (ρ ⟨$⟩ˡ e))
+    ≗a = ≡.cong arity ∘ edges≗ρ∘edges′
+
+    ≗j : (e : Fin (Hypergraph′.h (to H)))
+          (i : Fin (Hypergraph′.a (to H) e))
+        → fromVec (ports (fromList H.edges e)) i
+        ≡ fromVec (ports (fromList H′.edges (ρ ⟨$⟩ˡ e))) (cast (≗a e) i)
+    ≗j e i
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-is-id ≡.refl i = ≡.refl
+
+    ≗l : (e : Fin (Hypergraph′.h (to H)))
+        → label (fromList H.edges e)
+        ≡ cast-gate (≡.sym (≗a e)) (label (fromList H′.edges (ρ ⟨$⟩ˡ e)))
+    ≗l e
+      rewrite edges≗ρ∘edges′ e
+      rewrite cast-gate-is-id ≡.refl (label (fromList H′.edges (ρ ⟨$⟩ˡ e))) =
+          ≡.refl
+
+module _ {v : ℕ} where
+  open import Data.Hypergraph.Edge GateLabel using (decTotalOrder; ≈-Edge; ≈-Edge-IsEquivalence; ≈-Edge⇒≡)
+  open import Data.List.Sort (decTotalOrder {v}) using (sort; sort-↭)
+  open import Data.Permutation.Sort (decTotalOrder {v}) using (sorted-≋)
+  open import Data.List.Relation.Binary.Pointwise using (Pointwise; Pointwise-≡⇒≡; map)
+  open import Data.Product.Base using (_,_)
+  open import Data.Hypergraph.Label using (HypergraphLabel)
+  open HypergraphLabel GateLabel using (isCastable)
+  open import Data.Castable using (IsCastable)
+  open IsCastable isCastable using (≈-reflexive; ≈-sym; ≈-trans)
+  from-cong
+      : {H H′ : Hypergraph′ v}
+      → Hypergraph-same H H′
+      → ≈-Hypergraph (from H) (from H′)
+  from-cong {H} {H′} ≈H = record
+      { ≡sorted = ≡sorted
+      }
+    where
+      module H = Hypergraph′ H
+      module H′ = Hypergraph′ H′
+      open Hypergraph′
+      open Hypergraph-same ≈H using (↔h; ≗a; ≗l; ≗j; inverseˡ) renaming (from to f; to to t)
+      asEdge : (H : Hypergraph′ v) → Fin (h H) → Edge v
+      asEdge H e = record { label = l H e ; ports = toVec (j H e) }
+
+      to-from : (e : Fin H′.h) → t (f e) ≡ e
+      to-from e = inverseˡ ≡.refl
+
+      a∘to-from : (e : Fin H′.h) → H′.a (t (f e)) ≡ H′.a e
+      a∘to-from = ≡.cong H′.a ∘ to-from
+
+      ≗a′ : (e : Fin H′.h) → H.a (f e) ≡ H′.a e
+      ≗a′ e = ≡.trans (≗a (f e)) (a∘to-from e)
+
+      l≗ : (e : Fin H.h) → cast-gate (≗a e) (H.l e) ≡ H′.l (t e)
+      l≗ e = ≈-sym (≡.sym (≗l e))
+
+      l∘to-from : (e : Fin H′.h) → cast-gate (a∘to-from e) (H′.l (t (f e))) ≡ H′.l e
+      l∘to-from e rewrite to-from e = ≈-reflexive ≡.refl
+
+      ≗l′ : (e : Fin H′.h) → cast-gate (≗a′ e) (H.l (f e)) ≡ H′.l e
+      ≗l′ e = ≈-trans {H.a _} (l≗ (f e)) (l∘to-from e)
+
+      import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+      open import Data.Vec using (cast) renaming (map to vecmap)
+      open import Data.Vec.Properties using (tabulate-cong; tabulate-∘; map-cast)
+
+      open import Data.Fin.Base using () renaming (cast to fincast)
+      open import Data.Fin.Properties using () renaming (cast-trans to fincast-trans; cast-is-id to fincast-is-id)
+
+      j∘to-from
+          : (e : Fin H′.h) (i : Fin (H′.a (t (f e))))
+          → H′.j (t (f e)) i
+          ≡ H′.j e (fincast (a∘to-from e) i)
+      j∘to-from e i rewrite to-from e = ≡.cong (H′.j e) (≡.sym (fincast-is-id ≡.refl i))
+
+      open ≡.≡-Reasoning
+
+      ≗j′ : (e : Fin H′.h) (i : Fin (H.a (f e))) → H.j (f e) i ≡ H′.j e (fincast (≗a′ e) i)
+      ≗j′ e i = begin
+          H.j (f e) i                                   ≡⟨ ≗j (f e) i ⟩
+          H′.j (t (f e)) (fincast _ i)                  ≡⟨ j∘to-from e (fincast _ i) ⟩
+          H′.j e (fincast (a∘to-from e) (fincast _ i))  ≡⟨ ≡.cong (H′.j e) (fincast-trans (≗a (f e)) _ i) ⟩
+          H′.j e (fincast (≗a′ e) i)                    ∎
+
+      cast-toVec
+          : {n m : ℕ}
+            {A : Set}
+            (m≡n : m ≡ n)
+            (f : Fin n → A)
+          → cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f
+      cast-toVec m≡n f rewrite m≡n = begin
+          cast _ (toVec (f ∘ (fincast _)))  ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩
+          toVec (f ∘ fincast _)             ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩
+          vecmap f (toVec (fincast _))      ≡⟨ ≡.cong (vecmap f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩
+          vecmap f (toVec id)               ≡⟨ tabulate-∘ f id ⟨
+          toVec f                           ∎
+
+      ≗p′ : (e : Fin H′.h) → cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e)
+      ≗p′ e = begin
+          cast (≗a′ e) (toVec (H.j (f e)))    ≡⟨ ≡.cong (cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩
+          cast _ (toVec (H′.j e ∘ fincast _)) ≡⟨ cast-toVec (≗a′ e) (H′.j e) ⟩
+          toVec (H′.j e)                      ∎
+
+      H∘ρ≗H′ : (e : Fin H′.h) → asEdge H (↔h ⟨$⟩ˡ e) ≡ asEdge H′ e
+      H∘ρ≗H′ e = ≈-Edge⇒≡ record
+          { ≡arity = ≗a′ e
+          ; ≡label = ≗l′ e
+          ; ≡ports = ≗p′ e
+          }
+
+      open Hypergraph using (edges)
+      open →-Reasoning
+      ≡sorted : sortHypergraph (from H) ≡ sortHypergraph (from H′)
+      ≡sorted =
+             flip ↔h , H∘ρ≗H′             ∶ asEdge H V.↭ asEdge H′
+          |> toList-↭                     ∶ toList (asEdge H) L.↭ toList (asEdge H′)
+          |> L.↭⇒↭ₛ′ ≈-Edge-IsEquivalence ∶ Permutation ≈-Edge (edges (from H)) (edges (from H′))
+          |> sorted-≋                     ∶ Pointwise ≈-Edge (sort (edges (from H))) (sort (edges (from H′)))
+          |> map ≈-Edge⇒≡                 ∶ Pointwise _≡_ (sort (edges (from H))) (sort (edges (from H′)))
+          |> Pointwise-≡⇒≡                ∶ sort (edges (from H)) ≡ sort (edges (from H′))
+          |> ≡.cong mkHypergraph          ∶ sortHypergraph (from H) ≡ sortHypergraph (from H′)
+
+equiv : (v : ℕ) → Equivalence (Hypergraph-Setoid v) (Hypergraph-Setoid′ v)
+equiv v = record
+    { to = to
+    ; from = from
+    ; to-cong = to-cong
+    ; from-cong = from-cong
+    }
diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda
new file mode 100644
index 0000000..8ce7e0a
--- /dev/null
+++ b/Data/Circuit/Gate.agda
@@ -0,0 +1,137 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Circuit.Gate where
+
+open import Level using (0ℓ)
+open import Data.Castable using (Castable)
+open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Data.String using (String)
+open import Data.Nat.Base using (ℕ; _≤_)
+open import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; isEquivalence; cong)
+import Relation.Binary.PropositionalEquality as ≡
+
+import Data.Nat as Nat
+import Data.Fin as Fin
+
+data Gate : ℕ → Set where
+    ZERO  : Gate 1
+    ONE   : Gate 1
+    ID    : Gate 2
+    NOT   : Gate 2
+    AND   : Gate 3
+    OR    : Gate 3
+    XOR   : Gate 3
+    NAND  : Gate 3
+    NOR   : Gate 3
+    XNOR  : Gate 3
+
+cast-gate : {e e′ : ℕ} → .(e ≡ e′) → Gate e → Gate e′
+cast-gate {1} {1} eq g = g
+cast-gate {2} {2} eq g = g
+cast-gate {3} {3} eq g = g
+
+cast-gate-trans
+    : {m n o : ℕ}
+    → .(eq₁ : m ≡ n)
+      .(eq₂ : n ≡ o)
+      (g : Gate m)
+    → cast-gate eq₂ (cast-gate eq₁ g) ≡ cast-gate (trans eq₁ eq₂) g
+cast-gate-trans {1} {1} {1} eq₁ eq₂ g = refl
+cast-gate-trans {2} {2} {2} eq₁ eq₂ g = refl
+cast-gate-trans {3} {3} {3} eq₁ eq₂ g = refl
+
+cast-gate-is-id : {m : ℕ} .(eq : m ≡ m) (g : Gate m) → cast-gate eq g ≡ g
+cast-gate-is-id {1} eq g = refl
+cast-gate-is-id {2} eq g = refl
+cast-gate-is-id {3} eq g = refl
+
+subst-is-cast-gate : {m n : ℕ} (eq : m ≡ n) (g : Gate m) → subst Gate eq g ≡ cast-gate eq g
+subst-is-cast-gate refl g = sym (cast-gate-is-id refl g)
+
+GateCastable : Castable
+GateCastable = record
+    { B = Gate
+    ; isCastable = record
+        { cast = cast-gate
+        ; cast-trans = cast-gate-trans
+        ; cast-is-id = cast-gate-is-id
+        ; subst-is-cast = subst-is-cast-gate
+        }
+    }
+
+showGate : (n : ℕ) → Gate n → String
+showGate _ ZERO = "ZERO"
+showGate _ ONE  = "ONE"
+showGate _ ID   = "ID"
+showGate _ NOT  = "NOT"
+showGate _ AND  = "AND"
+showGate _ OR   = "OR"
+showGate _ XOR  = "XOR"
+showGate _ NAND = "NAND"
+showGate _ NOR  = "NOR"
+showGate _ XNOR = "XNOR"
+
+toℕ : (n : ℕ) → Gate n → ℕ
+toℕ 1 ZERO = 0
+toℕ 1 ONE = 1
+toℕ 2 ID = 0
+toℕ 2 NOT = 1
+toℕ 3 AND = 0
+toℕ 3 OR = 1
+toℕ 3 XOR = 2
+toℕ 3 NAND = 3
+toℕ 3 NOR = 4
+toℕ 3 XNOR = 5
+
+toℕ-injective : {n : ℕ} {x y : Gate n} → toℕ n x ≡ toℕ n y → x ≡ y
+toℕ-injective {1} {ZERO} {ZERO} refl = refl
+toℕ-injective {1} {ONE} {ONE} refl = refl
+toℕ-injective {2} {ID} {ID} refl = refl
+toℕ-injective {2} {NOT} {NOT} refl = refl
+toℕ-injective {3} {AND} {AND} refl = refl
+toℕ-injective {3} {OR} {OR} refl = refl
+toℕ-injective {3} {XOR} {XOR} refl = refl
+toℕ-injective {3} {NAND} {NAND} refl = refl
+toℕ-injective {3} {NOR} {NOR} refl = refl
+toℕ-injective {3} {XNOR} {XNOR} refl = refl
+
+open import Relation.Binary using (Rel; Decidable; DecidableEquality)
+import Relation.Nullary.Decidable as Dec
+
+_[_≤_] : (n : ℕ) → Rel (Gate n) 0ℓ
+_[_≤_] n x y = toℕ n x ≤ toℕ n y
+
+_≟_ : {n : ℕ} → DecidableEquality (Gate n)
+_≟_ {n} x y = Dec.map′ toℕ-injective (cong (toℕ n)) (toℕ n x Nat.≟ toℕ n y)
+
+_≤?_ : {n : ℕ} → Decidable (n [_≤_])
+_≤?_ {n} x y = toℕ n x Nat.≤? toℕ n y
+
+GateLabel : HypergraphLabel
+GateLabel = record
+    { Label = Gate
+    ; showLabel = showGate
+    ; isCastable = record
+        { cast = cast-gate
+        ; cast-trans = cast-gate-trans
+        ; cast-is-id = cast-gate-is-id
+        ; subst-is-cast = subst-is-cast-gate
+        }
+    ; _[_≤_] = λ n x y → toℕ n x ≤ toℕ n y
+    ; isDecTotalOrder = λ n → record
+        { isTotalOrder = record
+          { isPartialOrder = record
+              { isPreorder = record
+                  { isEquivalence = isEquivalence
+                  ; reflexive = λ { refl → ≤-refl }
+                  ; trans = ≤-trans
+                  }
+              ; antisym = λ i≤j j≤i → toℕ-injective (≤-antisym i≤j j≤i)
+              }
+          ; total = λ { x y → ≤-total (toℕ n x) (toℕ n y) }
+          }
+        ; _≟_ = _≟_
+        ; _≤?_ = _≤?_
+        }
+    }
diff --git a/Data/Circuit/Typecheck.agda b/Data/Circuit/Typecheck.agda
new file mode 100644
index 0000000..e34ea44
--- /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.Circuit.Gate using (GateLabel; Gate)
+open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Data.Hypergraph.Edge GateLabel using (Edge)
+open import Data.Hypergraph.Base 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