Construct SM nat trans from Circ to Sysmain

1 files changed, 165 insertions, 0 deletions

diff --git a/NaturalTransformation/Instance/GateSemantics.agda b/NaturalTransformation/Instance/GateSemantics.agda
new file mode 100644
index 0000000..e86e942
--- /dev/null
+++ b/NaturalTransformation/Instance/GateSemantics.agda
@@ -0,0 +1,165 @@
+{-# OPTIONS --without-K --safe #-}
+
+module NaturalTransformation.Instance.GateSemantics where
+
+open import Level using (suc; 0ℓ)
+open import Category.Instance.Setoids.SymmetricMonoidal {suc 0ℓ} {suc 0ℓ} using (Setoids-×)
+
+import Data.Fin.Properties as FinProp
+import Data.Circuit.Value as Value
+import Functor.Forgetful.Instance.CMonoid Setoids-×.symmetric as CMonoid
+import Functor.Forgetful.Instance.Monoid Setoids-×.monoidal as Monoid
+
+open import Categories.Category.Instance.Nat using (Nat)
+open import Categories.Category.Instance.Setoids using (Setoids)
+open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
+open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
+open import Category.Construction.CMonoids Setoids-×.symmetric using (CMonoids)
+open import Data.Circuit {suc 0ℓ} using () renaming (module Edge to EGate)
+open import Data.Circuit.Gate using (Gate; Gates)
+open import Data.Fin using (Fin; #_)
+open import Data.Fin.Patterns using (0F; 1F; 2F)
+open import Data.Nat using (ℕ)
+open import Data.Setoid using (∣_∣; _⇒ₛ_)
+open import Data.Setoid.Unit using (⊤ₛ)
+open import Data.System {suc 0ℓ} using (System)
+open import Data.System.Values Value.Monoid using (Values)
+open import Function using (Func; _⟶ₛ_; id; _⟨$⟩_)
+open import Function.Construct.Constant using () renaming (function to Const)
+open import Function.Construct.Identity using () renaming (function to Id)
+open import Functor.Instance.Nat.Edge {suc 0ℓ} Gates using (Edge)
+open import Functor.Instance.Nat.System using (module NatCMon)
+open import Relation.Binary using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+open Value using (Value)
+open NatCMon using (Sys)
+open System
+open Func
+
+Valueₛ : Setoid 0ℓ 0ℓ
+Valueₛ = ≡.setoid Value
+
+opaque
+
+  unfolding Values
+
+  1-cell : Value → System 1
+  1-cell x .S = ⊤ₛ
+  1-cell x .fₛ = Const (Values 1) (⊤ₛ ⇒ₛ ⊤ₛ) (Id ⊤ₛ)
+  1-cell x .fₒ = Const ⊤ₛ (Values 1) λ { 0F → x }
+
+  2-cell : (Value → Value) → System 2
+  2-cell f .S = Valueₛ
+  2-cell f .fₛ .to x = Const Valueₛ Valueₛ (f (x (# 0)))
+  2-cell f .fₛ .cong x = ≡.cong f (x (# 0))
+  2-cell f .fₒ .to x 0F = Value.U
+  2-cell f .fₒ .to x 1F = x
+  2-cell f .fₒ .cong _ 0F = ≡.refl
+  2-cell f .fₒ .cong x 1F = x
+
+  3-cell : (Value → Value → Value) → System 3
+  3-cell f .S = Valueₛ
+  3-cell f .fₛ .to i = Const Valueₛ Valueₛ (f (i (# 0)) (i (# 1)))
+  3-cell f .fₛ .cong ≡i = ≡.cong₂ f (≡i (# 0)) (≡i (# 1))
+  3-cell f .fₒ .to _ 0F = Value.U
+  3-cell f .fₒ .to _ 1F = Value.U
+  3-cell f .fₒ .to x 2F = x
+  3-cell f .fₒ .cong _ 0F = ≡.refl
+  3-cell f .fₒ .cong _ 1F = ≡.refl
+  3-cell f .fₒ .cong x 2F = x
+
+-- Belnap's four-valued logic
+module Belnap where
+
+  open Value.Value
+
+  true false : Value
+  true = T
+  false = F
+
+  not : Value → Value
+  not U = U
+  not T = F
+  not F = T
+  not X = X
+
+  and : Value → Value → Value
+  and U U = U
+  and U T = U
+  and U F = F
+  and U X = F
+  and T y = y
+  and F _ = F
+  and X U = F
+  and X T = X
+  and X F = F
+  and X X = X
+
+  or : Value → Value → Value
+  or U U = U
+  or U T = T
+  or U F = U
+  or U X = T
+  or T _ = T
+  or F y = y
+  or X U = T
+  or X T = T
+  or X F = X
+  or X X = X
+
+  xor : Value → Value → Value
+  xor x y = or (and x (not y)) (and (not x) y)
+
+  nand : Value → Value → Value
+  nand x y = not (and x y)
+
+  nor : Value → Value → Value
+  nor x y = not (or x y)
+
+  xnor : Value → Value → Value
+  xnor x y = not (xor x y)
+
+module _ where
+
+  open Belnap
+  open Gate
+
+  system-of-gate : {n : ℕ} → Gate n → System n
+  system-of-gate ZERO = 1-cell true
+  system-of-gate ONE  = 1-cell false
+  system-of-gate ID   = 2-cell id
+  system-of-gate NOT  = 2-cell not
+  system-of-gate AND  = 3-cell and
+  system-of-gate OR   = 3-cell or
+  system-of-gate XOR  = 3-cell xor
+  system-of-gate NAND = 3-cell nand
+  system-of-gate NOR  = 3-cell nor
+  system-of-gate XNOR = 3-cell xnor
+
+private
+
+  U : Functor CMonoids (Setoids (suc 0ℓ) (suc 0ℓ))
+  U = Monoid.Forget ∙ CMonoid.Forget
+
+  module U = Functor U
+  module Edge = Functor Edge
+
+open EGate hiding (Edge)
+
+system-of-edge : {n : ℕ} → ∣ Edge.₀ n ∣ → System n
+system-of-edge (mkEdge gate ports) = U.₁ (Sys.₁ ports) ⟨$⟩ system-of-gate gate
+
+system-of-edgeₛ : (n : ℕ) → Edge.₀ n ⟶ₛ U.₀ (Sys.₀ n)
+system-of-edgeₛ n .to = system-of-edge {n}
+system-of-edgeₛ n .cong {mkEdge label₁ ports₁} {mkEdge label₂ ports₂} (mk≈ ≡.refl ≡.refl ≡ports)
+    rewrite EGate.HL.cast-is-id ≡.refl label₁ = Sys.F-resp-≈ ≗ports {system-of-gate label₁}
+  where
+    ≗ports : (x : Fin _) → ports₁ x ≡ ports₂ x
+    ≗ports x = ≡.trans (≡ports x) (≡.cong ports₂ (FinProp.cast-is-id ≡.refl x))
+
+semantics : NaturalTransformation Edge (U ∙ Sys)
+semantics = ntHelper record
+    { η = system-of-edgeₛ
+    ; commute = λ _ → Sys.homomorphism
+    }