diff options
Diffstat (limited to 'Data/Circuit')
| -rw-r--r-- | Data/Circuit/Convert.agda | 181 | ||||
| -rw-r--r-- | Data/Circuit/Gate.agda | 137 | ||||
| -rw-r--r-- | Data/Circuit/Merge.agda | 427 | ||||
| -rw-r--r-- | Data/Circuit/Typecheck.agda | 78 | ||||
| -rw-r--r-- | Data/Circuit/Value.agda | 180 |
5 files changed, 1003 insertions, 0 deletions
diff --git a/Data/Circuit/Convert.agda b/Data/Circuit/Convert.agda new file mode 100644 index 0000000..d5abd35 --- /dev/null +++ b/Data/Circuit/Convert.agda @@ -0,0 +1,181 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Convert where + +open import Level using (0ℓ) + +import Data.Vec as Vec +import Data.Vec.Relation.Binary.Equality.Cast as VecCast +import Data.List.Relation.Binary.Permutation.Propositional as L +import Data.Vec.Functional.Relation.Binary.Permutation as V +import DecorationFunctor.Hypergraph.Labeled {0ℓ} {0ℓ} as LabeledHypergraph + +open import Data.Nat.Base using (ℕ) +open import Data.Circuit.Gate using (Gate; Gates; cast-gate; cast-gate-is-id; subst-is-cast-gate) +open import Data.Circuit {0ℓ} {0ℓ} using (Circuit; Circuitₛ; _≈_; mkCircuit; module Edge; mk≈) +open import Data.Fin.Base using (Fin) +open import Data.Product.Base using (_,_) +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.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) +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 (_≡_; _≗_) + +open LabeledHypergraph using (Hypergraph-same) renaming (Hypergraph to Hypergraph′; Hypergraph-setoid to Hypergraph-Setoid′) + +to : {v : ℕ} → Circuit v → Hypergraph′ v +to C = record + { h = length edges + ; a = arity ∘ fromList edges + ; j = fromVec ∘ ports ∘ fromList edges + ; l = label ∘ fromList edges + } + where + open Edge.Edge using (arity; ports; label) + open Circuit C + +from : {v : ℕ} → Hypergraph′ v → Circuit v +from {v} H = record + { edges = toList asEdge + } + where + open Hypergraph′ H + asEdge : Fin h → Edge.Edge v + asEdge e = record { label = l e ; ports = toVec (j e) } + +to-cong : {v : ℕ} {H H′ : Circuit v} → 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.Edge using (arity; ports; label) + open _≈_ ≈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.Label using (HypergraphLabel) + open HypergraphLabel Gates 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′ + → from H ≈ from H′ + from-cong {H} {H′} ≈H = mk≈ (toList-↭ (flip ↔h , H∘ρ≗H′)) + 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.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) + + 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) + → Vec.cast m≡n (toVec (f ∘ fincast m≡n)) ≡ toVec f + cast-toVec m≡n f rewrite m≡n = begin + Vec.cast _ (toVec (f ∘ (fincast _))) ≡⟨ VecCast.cast-is-id ≡.refl (toVec (f ∘ fincast ≡.refl)) ⟩ + toVec (f ∘ fincast _) ≡⟨ tabulate-∘ f (fincast ≡.refl) ⟩ + Vec.map f (toVec (fincast _)) ≡⟨ ≡.cong (Vec.map f) (tabulate-cong (fincast-is-id ≡.refl)) ⟩ + Vec.map f (toVec id) ≡⟨ tabulate-∘ f id ⟨ + toVec f ∎ + + ≗p′ : (e : Fin H′.h) → Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡ toVec (H′.j e) + ≗p′ e = begin + Vec.cast (≗a′ e) (toVec (H.j (f e))) ≡⟨ ≡.cong (Vec.cast (≗a′ e)) (tabulate-cong (≗j′ e)) ⟩ + Vec.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 + } + +equiv : (v : ℕ) → Equivalence (Circuitₛ 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..f4b55de --- /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 + +Gates : HypergraphLabel +Gates = 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/Merge.agda b/Data/Circuit/Merge.agda new file mode 100644 index 0000000..9cf180a --- /dev/null +++ b/Data/Circuit/Merge.agda @@ -0,0 +1,427 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Merge where + +open import Data.Nat.Base using (ℕ) +open import Data.Fin.Base using (Fin; pinch; punchIn; punchOut; splitAt) +open import Data.Fin.Properties using (punchInᵢ≢i; punchIn-punchOut) +open import Data.Bool.Properties using (if-eta) +open import Data.Bool using (Bool; if_then_else_) +open import Data.Circuit.Value using (Value; join; join-comm; join-assoc) +open import Data.Sum.Properties using ([,]-cong; [,-]-cong; [-,]-cong; [,]-∘; [,]-map) +open import Data.Subset.Functional + using + ( Subset + ; ⁅_⁆ ; ⊥ ; ⁅⁆∘ρ + ; foldl ; foldl-cong₁ ; foldl-cong₂ + ; foldl-[] ; foldl-suc + ; foldl-⊥ ; foldl-⁅⁆ + ; foldl-fusion + ) +open import Data.Vector as V using (Vector; head; tail; removeAt) +open import Data.Vec.Functional using (_++_) +open import Data.Fin.Permutation + using + ( Permutation + ; Permutation′ + ; _⟨$⟩ˡ_ ; _⟨$⟩ʳ_ + ; inverseˡ ; inverseʳ + ; id + ; flip + ; insert ; remove + ; punchIn-permute + ) +open import Data.Product using (Σ-syntax; _,_) +open import Data.Fin.Preimage using (preimage; preimage-cong₁; preimage-cong₂) +open import Function.Base using (∣_⟩-_; _∘_; case_of_; _$_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≢_; _≗_; module ≡-Reasoning) + +open Value using (U) +open ℕ +open Fin +open Bool + +open ≡-Reasoning + +_when_ : Value → Bool → Value +x when b = if b then x else U + +opaque + merge-with : {A : ℕ} → Value → Vector Value A → Subset A → Value + merge-with e v = foldl (∣ join ⟩- v) e + + merge-with-cong : {A : ℕ} {v₁ v₂ : Vector Value A} (e : Value) → v₁ ≗ v₂ → merge-with e v₁ ≗ merge-with e v₂ + merge-with-cong e v₁≗v₂ = foldl-cong₁ (λ x → ≡.cong (join x) ∘ v₁≗v₂) e + + merge-with-cong₂ : {A : ℕ} (e : Value) (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge-with e v S₁ ≡ merge-with e v S₂ + merge-with-cong₂ e v = foldl-cong₂ (∣ join ⟩- v) e + + merge-with-⊥ : {A : ℕ} (e : Value) (v : Vector Value A) → merge-with e v ⊥ ≡ e + merge-with-⊥ e v = foldl-⊥ (∣ join ⟩- v) e + + merge-with-[] : (e : Value) (v : Vector Value 0) (S : Subset 0) → merge-with e v S ≡ e + merge-with-[] e v = foldl-[] (∣ join ⟩- v) e + + merge-with-suc + : {A : ℕ} (e : Value) (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge-with e v S + ≡ merge-with (if head S then join e (head v) else e) (tail v) (tail S) + merge-with-suc e v = foldl-suc (∣ join ⟩- v) e + + merge-with-join + : {A : ℕ} + (x y : Value) + (v : Vector Value A) + → merge-with (join x y) v ≗ join x ∘ merge-with y v + merge-with-join {A} x y v S = ≡.sym (foldl-fusion (join x) fuse y S) + where + fuse : (acc : Value) (k : Fin A) → join x (join acc (v k)) ≡ join (join x acc) (v k) + fuse acc k = ≡.sym (join-assoc x acc (v k)) + + merge-with-⁅⁆ : {A : ℕ} (e : Value) (v : Vector Value A) (x : Fin A) → merge-with e v ⁅ x ⁆ ≡ join e (v x) + merge-with-⁅⁆ e v = foldl-⁅⁆ (∣ join ⟩- v) e + +merge-with-U : {A : ℕ} (e : Value) (S : Subset A) → merge-with e (λ _ → U) S ≡ e +merge-with-U {zero} e S = merge-with-[] e (λ _ → U) S +merge-with-U {suc A} e S = begin + merge-with e (λ _ → U) S ≡⟨ merge-with-suc e (λ _ → U) S ⟩ + merge-with + (if head S then join e U else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with (if head S then h else e) _ _) (join-comm e U) ⟩ + merge-with + (if head S then e else e) + (tail (λ _ → U)) (tail S) ≡⟨ ≡.cong (λ h → merge-with h (λ _ → U) (tail S)) (if-eta (head S)) ⟩ + merge-with e (tail (λ _ → U)) (tail S) ≡⟨⟩ + merge-with e (λ _ → U) (tail S) ≡⟨ merge-with-U e (tail S) ⟩ + e ∎ + +merge : {A : ℕ} → Vector Value A → Subset A → Value +merge v = merge-with U v + +merge-cong₁ : {A : ℕ} {v₁ v₂ : Vector Value A} → v₁ ≗ v₂ → merge v₁ ≗ merge v₂ +merge-cong₁ = merge-with-cong U + +merge-cong₂ : {A : ℕ} (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge v S₁ ≡ merge v S₂ +merge-cong₂ = merge-with-cong₂ U + +merge-⊥ : {A : ℕ} (v : Vector Value A) → merge v ⊥ ≡ U +merge-⊥ = merge-with-⊥ U + +merge-[] : (v : Vector Value 0) (S : Subset 0) → merge v S ≡ U +merge-[] = merge-with-[] U + +merge-[]₂ : {v₁ v₂ : Vector Value 0} {S₁ S₂ : Subset 0} → merge v₁ S₁ ≡ merge v₂ S₂ +merge-[]₂ {v₁} {v₂} {S₁} {S₂} = ≡.trans (merge-[] v₁ S₁) (≡.sym (merge-[] v₂ S₂)) + +merge-⁅⁆ : {A : ℕ} (v : Vector Value A) (x : Fin A) → merge v ⁅ x ⁆ ≡ v x +merge-⁅⁆ = merge-with-⁅⁆ U + +join-merge : {A : ℕ} (e : Value) (v : Vector Value A) (S : Subset A) → join e (merge v S) ≡ merge-with e v S +join-merge e v S = ≡.sym (≡.trans (≡.cong (λ h → merge-with h v S) (join-comm U e)) (merge-with-join e U v S)) + +merge-suc + : {A : ℕ} (v : Vector Value (suc A)) (S : Subset (suc A)) + → merge v S + ≡ merge-with (head v when head S) (tail v) (tail S) +merge-suc = merge-with-suc U + +insert-f0-0 + : {A B : ℕ} + (f : Fin (suc A) → Fin (suc B)) + → Σ[ ρ ∈ Permutation′ (suc B) ] (ρ ⟨$⟩ʳ (f zero) ≡ zero) +insert-f0-0 f = insert (f zero) zero id , help + where + open import Data.Fin using (_≟_) + open import Relation.Nullary.Decidable using (yes; no) + help : insert (f zero) zero id ⟨$⟩ʳ f zero ≡ zero + help with f zero ≟ f zero + ... | yes _ = ≡.refl + ... | no f0≢f0 with () ← f0≢f0 ≡.refl + +merge-removeAt + : {A : ℕ} + (k : Fin (suc A)) + (v : Vector Value (suc A)) + (S : Subset (suc A)) + → merge v S ≡ join (v k when S k) (merge (removeAt v k) (removeAt S k)) +merge-removeAt {A} zero v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with (head v when head S) (tail v) (tail S) ≡⟨ join-merge (head v when head S) (tail v) (tail S) ⟨ + join (head v when head S) (merge-with U (tail v) (tail S)) ∎ +merge-removeAt {suc A} (suc k) v S = begin + merge-with U v S ≡⟨ merge-suc v S ⟩ + merge-with v0? (tail v) (tail S) ≡⟨ join-merge _ (tail v) (tail S) ⟨ + join v0? (merge (tail v) (tail S)) ≡⟨ ≡.cong (join v0?) (merge-removeAt k (tail v) (tail S)) ⟩ + join v0? (join vk? (merge (tail v-) (tail S-))) ≡⟨ join-assoc (head v when head S) _ _ ⟨ + join (join v0? vk?) (merge (tail v-) (tail S-)) ≡⟨ ≡.cong (λ h → join h (merge (tail v-) (tail S-))) (join-comm (head v- when head S-) _) ⟩ + join (join vk? v0?) (merge (tail v-) (tail S-)) ≡⟨ join-assoc (tail v k when tail S k) _ _ ⟩ + join vk? (join v0? (merge (tail v-) (tail S-))) ≡⟨ ≡.cong (join vk?) (join-merge _ (tail v-) (tail S-)) ⟩ + join vk? (merge-with v0? (tail v-) (tail S-)) ≡⟨ ≡.cong (join vk?) (merge-suc v- S-) ⟨ + join vk? (merge v- S-) ∎ + where + v0? vk? : Value + v0? = head v when head S + vk? = tail v k when tail S k + v- : Vector Value (suc A) + v- = removeAt v (suc k) + S- : Subset (suc A) + S- = removeAt S (suc k) + +import Function.Structures as FunctionStructures +open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ {B} _≡_ using (IsInverse) +open IsInverse using () renaming (inverseˡ to invˡ; inverseʳ to invʳ) + +merge-preimage-ρ + : {A B : ℕ} + → (ρ : Permutation A B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S +merge-preimage-ρ {zero} {zero} ρ v S = merge-[]₂ +merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero +merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero +merge-preimage-ρ {suc A} {suc B} ρ v S = begin + merge v (preimage ρʳ S) ≡⟨ merge-removeAt (head ρˡ) v (preimage ρʳ S) ⟩ + join + (head (v ∘ ρˡ) when S (ρʳ (ρˡ zero))) + (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (λ h → join h (merge v- [preimageρʳS]-)) ≡vρˡ0? ⟩ + join vρˡ0? (merge v- [preimageρʳS]-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₂ v- preimage-) ⟩ + join vρˡ0? (merge v- (preimage ρʳ- S-)) ≡⟨ ≡.cong (join vρˡ0?) (merge-preimage-ρ ρ- v- S-) ⟩ + join vρˡ0? (merge (v- ∘ ρˡ-) S-) ≡⟨ ≡.cong (join vρˡ0?) (merge-cong₁ v∘ρˡ- S-) ⟩ + join vρˡ0? (merge (tail (v ∘ ρˡ)) S-) ≡⟨ join-merge vρˡ0? (tail (v ∘ ρˡ)) S- ⟩ + merge-with vρˡ0? (tail (v ∘ ρˡ)) S- ≡⟨ merge-suc (v ∘ ρˡ) S ⟨ + merge (v ∘ ρˡ) S ∎ + where + ρˡ : Fin (suc B) → Fin (suc A) + ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρ- : Permutation A B + ρ- = remove (head ρˡ) ρ + ρˡ- : Fin B → Fin A + ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B + ρʳ- = ρ- ⟨$⟩ʳ_ + v- : Vector Value A + v- = removeAt v (head ρˡ) + [preimageρʳS]- : Subset A + [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ) + S- : Subset B + S- = tail S + vρˡ0? : Value + vρˡ0? = head (v ∘ ρˡ) when head S + ≡vρˡ0? : head (v ∘ ρˡ) when S (ρʳ (head ρˡ)) ≡ head (v ∘ ρˡ) when head S + ≡vρˡ0? = ≡.cong ((head (v ∘ ρˡ) when_) ∘ S) (inverseʳ ρ) + v∘ρˡ- : v- ∘ ρˡ- ≗ tail (v ∘ ρˡ) + v∘ρˡ- x = begin + v- (ρˡ- x) ≡⟨⟩ + v (punchIn (head ρˡ) (punchOut {A} {head ρˡ} _)) ≡⟨ ≡.cong v (punchIn-punchOut _) ⟩ + v (ρˡ (punchIn (ρʳ (ρˡ zero)) x)) ≡⟨ ≡.cong (λ h → v (ρˡ (punchIn h x))) (inverseʳ ρ) ⟩ + v (ρˡ (punchIn zero x)) ≡⟨⟩ + v (ρˡ (suc x)) ≡⟨⟩ + tail (v ∘ ρˡ) x ∎ + preimage- : [preimageρʳS]- ≗ preimage ρʳ- S- + preimage- x = begin + [preimageρʳS]- x ≡⟨⟩ + removeAt (preimage ρʳ S) (head ρˡ) x ≡⟨⟩ + S (ρʳ (punchIn (head ρˡ) x)) ≡⟨ ≡.cong S (punchIn-permute ρ (head ρˡ) x) ⟩ + S (punchIn (ρʳ (head ρˡ)) (ρʳ- x)) ≡⟨⟩ + S (punchIn (ρʳ (ρˡ zero)) (ρʳ- x)) ≡⟨ ≡.cong (λ h → S (punchIn h (ρʳ- x))) (inverseʳ ρ) ⟩ + S (punchIn zero (ρʳ- x)) ≡⟨⟩ + S (suc (ρʳ- x)) ≡⟨⟩ + preimage ρʳ- S- x ∎ + +push-with : {A B : ℕ} → (e : Value) → Vector Value A → (Fin A → Fin B) → Vector Value B +push-with e v f = merge-with e v ∘ preimage f ∘ ⁅_⁆ + +push : {A B : ℕ} → Vector Value A → (Fin A → Fin B) → Vector Value B +push = push-with U + +mutual + merge-preimage + : {A B : ℕ} + (f : Fin A → Fin B) + → (v : Vector Value A) + (S : Subset B) + → merge v (preimage f S) ≡ merge (push v f) S + merge-preimage {zero} {zero} f v S = merge-[]₂ + merge-preimage {zero} {suc B} f v S = begin + merge v (preimage f S) ≡⟨ merge-[] v (preimage f S) ⟩ + U ≡⟨ merge-with-U U S ⟨ + merge (λ _ → U) S ≡⟨ merge-cong₁ (λ x → ≡.sym (merge-[] v (⁅ x ⁆ ∘ f))) S ⟩ + merge (push v f) S ∎ + merge-preimage {suc A} {zero} f v S with () ← f zero + merge-preimage {suc A} {suc B} f v S with insert-f0-0 f + ... | ρ , ρf0≡0 = begin + merge v (preimage f S) ≡⟨ merge-cong₂ v (preimage-cong₁ (λ x → inverseˡ ρ {f x}) S) ⟨ + merge v (preimage (ρˡ ∘ ρʳ ∘ f) S) ≡⟨⟩ + merge v (preimage (ρʳ ∘ f) (preimage ρˡ S)) ≡⟨ merge-preimage-f0≡0 (ρʳ ∘ f) ρf0≡0 v (preimage ρˡ S) ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) (preimage ρˡ S) ≡⟨ merge-preimage-ρ (flip ρ) (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ ⁅_⁆ ∘ ρʳ) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₂ (ρʳ ∘ f) ∘ ⁅⁆∘ρ ρ) S ⟩ + merge (merge v ∘ preimage (ρʳ ∘ f) ∘ preimage ρˡ ∘ ⁅_⁆) S ≡⟨⟩ + merge (merge v ∘ preimage (ρˡ ∘ ρʳ ∘ f) ∘ ⁅_⁆) S ≡⟨ merge-cong₁ (merge-cong₂ v ∘ preimage-cong₁ (λ y → inverseˡ ρ {f y}) ∘ ⁅_⁆) S ⟩ + merge (merge v ∘ preimage f ∘ ⁅_⁆) S ∎ + where + ρʳ ρˡ : Fin (ℕ.suc B) → Fin (ℕ.suc B) + ρʳ = ρ ⟨$⟩ʳ_ + ρˡ = ρ ⟨$⟩ˡ_ + + merge-preimage-f0≡0 + : {A B : ℕ} + (f : Fin (ℕ.suc A) → Fin (ℕ.suc B)) + → f Fin.zero ≡ Fin.zero + → (v : Vector Value (ℕ.suc A)) + (S : Subset (ℕ.suc B)) + → merge v (preimage f S) ≡ merge (merge v ∘ preimage f ∘ ⁅_⁆) S + merge-preimage-f0≡0 {A} {B} f f0≡0 v S + using S0 , S- ← head S , tail S + using v0 , v- ← head v , tail v + using _ , f- ← head f , tail f + = begin + merge v f⁻¹[S] ≡⟨ merge-suc v f⁻¹[S] ⟩ + merge-with v0? v- f⁻¹[S]- ≡⟨ join-merge v0? v- f⁻¹[S]- ⟨ + join v0? (merge v- f⁻¹[S]-) ≡⟨ ≡.cong (join v0?) (merge-preimage f- v- S) ⟩ + join v0? (merge f[v-] S) ≡⟨ join-merge v0? f[v-] S ⟩ + merge-with v0? f[v-] S ≡⟨ merge-with-suc v0? f[v-] S ⟩ + merge-with v0?+[f[v-]0?] f[v-]- S- ≡⟨ ≡.cong (λ h → merge-with h f[v-]- S-) ≡f[v]0 ⟩ + merge-with f[v]0? f[v-]- S- ≡⟨ merge-with-cong f[v]0? ≡f[v]- S- ⟩ + merge-with f[v]0? f[v]- S- ≡⟨ merge-suc f[v] S ⟨ + merge f[v] S ∎ + where + f⁻¹[S] : Subset (suc A) + f⁻¹[S] = preimage f S + f⁻¹[S]- : Subset A + f⁻¹[S]- = tail f⁻¹[S] + f⁻¹[S]0 : Bool + f⁻¹[S]0 = head f⁻¹[S] + f[v] : Vector Value (suc B) + f[v] = push v f + f[v]- : Vector Value B + f[v]- = tail f[v] + f[v]0 : Value + f[v]0 = head f[v] + f[v-] : Vector Value (suc B) + f[v-] = push v- f- + f[v-]- : Vector Value B + f[v-]- = tail f[v-] + f[v-]0 : Value + f[v-]0 = head f[v-] + f⁻¹⁅0⁆ : Subset (suc A) + f⁻¹⁅0⁆ = preimage f ⁅ zero ⁆ + f⁻¹⁅0⁆- : Subset A + f⁻¹⁅0⁆- = tail f⁻¹⁅0⁆ + v0? v0?+[f[v-]0?] f[v]0? : Value + v0? = v0 when f⁻¹[S]0 + v0?+[f[v-]0?] = (if S0 then join v0? f[v-]0 else v0?) + f[v]0? = f[v]0 when S0 + ≡f[v]0 : v0?+[f[v-]0?] ≡ f[v]0? + ≡f[v]0 rewrite f0≡0 with S0 + ... | true = begin + join v0 (merge v- f⁻¹⁅0⁆-) ≡⟨ join-merge v0 v- (tail (preimage f ⁅ zero ⁆)) ⟩ + merge-with v0 v- f⁻¹⁅0⁆- ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ zero ⁆ h) v- f⁻¹⁅0⁆-) f0≡0 ⟨ + merge-with v0?′ v- f⁻¹⁅0⁆- ≡⟨ merge-suc v (preimage f ⁅ zero ⁆) ⟨ + merge v f⁻¹⁅0⁆ ∎ + where + v0?′ : Value + v0?′ = v0 when head f⁻¹⁅0⁆ + ... | false = ≡.refl + ≡f[v]- : f[v-]- ≗ f[v]- + ≡f[v]- x = begin + push v- f- (suc x) ≡⟨ ≡.cong (λ h → merge-with (v0 when ⁅ suc x ⁆ h) v- (preimage f- ⁅ suc x ⁆)) f0≡0 ⟨ + push-with v0?′ v- f- (suc x) ≡⟨ merge-suc v (preimage f ⁅ suc x ⁆) ⟨ + push v f (suc x) ∎ + where + v0?′ : Value + v0?′ = v0 when head (preimage f ⁅ suc x ⁆) + +merge-++ + : {n m : ℕ} + (xs : Vector Value n) + (ys : Vector Value m) + (S₁ : Subset n) + (S₂ : Subset m) + → merge (xs ++ ys) (S₁ ++ S₂) + ≡ join (merge xs S₁) (merge ys S₂) +merge-++ {zero} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-cong₂ (xs ++ ys) (λ _ → ≡.refl) ⟩ + merge (xs ++ ys) S₂ ≡⟨ merge-cong₁ (λ _ → ≡.refl) S₂ ⟩ + merge ys S₂ ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-[] xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ +merge-++ {suc n} {m} xs ys S₁ S₂ = begin + merge (xs ++ ys) (S₁ ++ S₂) ≡⟨ merge-suc (xs ++ ys) (S₁ ++ S₂) ⟩ + merge-with (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ≡⟨ join-merge (head xs when head S₁) (tail (xs ++ ys)) (tail (S₁ ++ S₂)) ⟨ + join (head xs when head S₁) (merge (tail (xs ++ ys)) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₁ ([,]-map ∘ splitAt n) (tail (S₁ ++ S₂))) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail (S₁ ++ S₂))) + ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-cong₂ (tail xs ++ ys) ([,]-map ∘ splitAt n)) ⟩ + join (head xs when head S₁) (merge (tail xs ++ ys) (tail S₁ ++ S₂)) ≡⟨ ≡.cong (join (head xs when head S₁)) (merge-++ (tail xs) ys (tail S₁) S₂) ⟩ + join (head xs when head S₁) (join (merge (tail xs) (tail S₁)) (merge ys S₂)) ≡⟨ join-assoc (head xs when head S₁) (merge (tail xs) (tail S₁)) _ ⟨ + join (join (head xs when head S₁) (merge (tail xs) (tail S₁))) (merge ys S₂) + ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (join-merge (head xs when head S₁) (tail xs) (tail S₁)) ⟩ + join (merge-with (head xs when head S₁) (tail xs) (tail S₁)) (merge ys S₂) ≡⟨ ≡.cong (λ h → join h (merge ys S₂)) (merge-suc xs S₁) ⟨ + join (merge xs S₁) (merge ys S₂) ∎ + +open import Function using (Equivalence) +open Equivalence +open import Data.Nat using (_+_) +open import Data.Fin using (_↑ˡ_; _↑ʳ_; _≟_) +open import Data.Fin.Properties using (↑ˡ-injective; ↑ʳ-injective; splitAt⁻¹-↑ˡ; splitAt-↑ˡ; splitAt⁻¹-↑ʳ; splitAt-↑ʳ) +open import Relation.Nullary.Decidable using (does; does-⇔; dec-false) + +open Fin +⁅⁆-≟ : {n : ℕ} (x y : Fin n) → ⁅ x ⁆ y ≡ does (x ≟ y) +⁅⁆-≟ zero zero = ≡.refl +⁅⁆-≟ zero (suc y) = ≡.refl +⁅⁆-≟ (suc x) zero = ≡.refl +⁅⁆-≟ (suc x) (suc y) = ⁅⁆-≟ x y + +open import Data.Sum using ([_,_]′; inj₁; inj₂) +⁅⁆-++ + : {n′ m′ : ℕ} + (i : Fin (n′ + m′)) + → [ (λ x → ⁅ x ⁆ ++ ⊥) , (λ x → ⊥ ++ ⁅ x ⁆) ]′ (splitAt n′ i) ≗ ⁅ i ⁆ +⁅⁆-++ {n′} {m′} i x with splitAt n′ i in eq₁ +... | inj₁ i′ with splitAt n′ x in eq₂ +... | inj₁ x′ = begin + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ⟩ + does (i′ ↑ˡ m′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (x′ ↑ˡ m′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (i′ ↑ˡ m′ ≡ x′ ↑ˡ m′)) + ⇔ .to = ≡.cong (_↑ˡ m′) + ⇔ .from = ↑ˡ-injective m′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl +... | inj₂ x′ = begin + false ≡⟨ dec-false (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ↑ˡ≢↑ʳ ⟨ + does (i′ ↑ˡ m′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (i′ ↑ˡ m′) (n′ ↑ʳ x′) ⟨ + ⁅ i′ ↑ˡ m′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ˡ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ˡ≢↑ʳ : i′ ↑ˡ m′ ≢ n′ ↑ʳ x′ + ↑ˡ≢↑ʳ ≡ = case ≡.trans (≡.sym (splitAt-↑ˡ n′ i′ m′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ʳ n′ m′ x′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ with splitAt n′ x in eq₂ +⁅⁆-++ {n′} {m′} i x | inj₂ i′ | inj₁ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong ([ ⊥ , ⁅ i′ ⁆ ]′) eq₂ ⟩ + false ≡⟨ dec-false (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ↑ʳ≢↑ˡ ⟨ + does (n′ ↑ʳ i′ ≟ x′ ↑ˡ m′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (x′ ↑ˡ m′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (x′ ↑ˡ m′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ˡ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ↑ʳ≢↑ˡ : n′ ↑ʳ i′ ≢ x′ ↑ˡ m′ + ↑ʳ≢↑ˡ ≡ = case ≡.trans (≡.sym (splitAt-↑ʳ n′ m′ i′)) (≡.trans (≡.cong (splitAt n′) ≡) (splitAt-↑ˡ n′ x′ m′)) of λ { () } +⁅⁆-++ {n′} i x | inj₂ i′ | inj₂ x′ = begin + [ ⊥ , ⁅ i′ ⁆ ]′ (splitAt n′ x) ≡⟨ ≡.cong [ ⊥ , ⁅ i′ ⁆ ]′ eq₂ ⟩ + ⁅ i′ ⁆ x′ ≡⟨ ⁅⁆-≟ i′ x′ ⟩ + does (i′ ≟ x′) ≡⟨ does-⇔ ⇔ (i′ ≟ x′) (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ⟩ + does (n′ ↑ʳ i′ ≟ n′ ↑ʳ x′) ≡⟨ ⁅⁆-≟ (n′ ↑ʳ i′) (n′ ↑ʳ x′) ⟨ + ⁅ n′ ↑ʳ i′ ⁆ (n′ ↑ʳ x′) ≡⟨ ≡.cong₂ ⁅_⁆ (splitAt⁻¹-↑ʳ eq₁) (splitAt⁻¹-↑ʳ eq₂) ⟩ + ⁅ i ⁆ x ∎ + where + ⇔ : Equivalence (≡.setoid (i′ ≡ x′)) (≡.setoid (n′ ↑ʳ i′ ≡ n′ ↑ʳ x′)) + ⇔ .to = ≡.cong (n′ ↑ʳ_) + ⇔ .from = ↑ʳ-injective n′ i′ x′ + ⇔ .to-cong ≡.refl = ≡.refl + ⇔ .from-cong ≡.refl = ≡.refl 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 diff --git a/Data/Circuit/Value.agda b/Data/Circuit/Value.agda new file mode 100644 index 0000000..b135c35 --- /dev/null +++ b/Data/Circuit/Value.agda @@ -0,0 +1,180 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Circuit.Value where + +import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as LatticeProp + +open import Algebra.Bundles using (CommutativeMonoid) +open import Algebra.Structures using (IsCommutativeMonoid; IsMonoid; IsSemigroup; IsMagma) +open import Data.Product.Base using (_×_; _,_) +open import Data.String.Base using (String) +open import Level using (0ℓ) +open import Relation.Binary.Lattice.Bundles using (BoundedJoinSemilattice) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open CommutativeMonoid +open IsCommutativeMonoid +open IsMagma +open IsMonoid +open IsSemigroup + +data Value : Set where + U T F X : Value + +data ≤-Value : Value → Value → Set where + v≤v : {v : Value} → ≤-Value v v + U≤T : ≤-Value U T + U≤F : ≤-Value U F + U≤X : ≤-Value U X + T≤X : ≤-Value T X + F≤X : ≤-Value F X + +≤-reflexive : {x y : Value} → x ≡ y → ≤-Value x y +≤-reflexive ≡.refl = v≤v + +≤-transitive : {i j k : Value} → ≤-Value i j → ≤-Value j k → ≤-Value i k +≤-transitive v≤v y = y +≤-transitive x v≤v = x +≤-transitive U≤T T≤X = U≤X +≤-transitive U≤F F≤X = U≤X + +≤-antisymmetric : {i j : Value} → ≤-Value i j → ≤-Value j i → i ≡ j +≤-antisymmetric v≤v _ = ≡.refl + +showValue : Value → String +showValue U = "U" +showValue T = "T" +showValue F = "F" +showValue X = "X" + +join : Value → Value → Value +join U y = y +join x U = x +join T T = T +join T F = X +join F T = X +join F F = F +join X _ = X +join _ X = X + +≤-supremum + : (x y : Value) + → ≤-Value x (join x y) + × ≤-Value y (join x y) + × ((z : Value) → ≤-Value x z → ≤-Value y z → ≤-Value (join x y) z) +≤-supremum U U = v≤v , v≤v , λ _ U≤z _ → U≤z +≤-supremum U T = U≤T , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U F = U≤F , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum U X = U≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum T U = v≤v , U≤T , λ { z x≤z y≤z → x≤z } +≤-supremum T T = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum T F = T≤X , F≤X , λ { X x≤z y≤z → v≤v } +≤-supremum T X = T≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum F U = v≤v , U≤F , λ { z x≤z y≤z → x≤z } +≤-supremum F T = F≤X , T≤X , λ { X x≤z y≤z → v≤v } +≤-supremum F F = v≤v , v≤v , λ { z x≤z y≤z → x≤z } +≤-supremum F X = F≤X , v≤v , λ { z x≤z y≤z → y≤z } +≤-supremum X U = v≤v , U≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X T = v≤v , T≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X F = v≤v , F≤X , λ { z x≤z y≤z → x≤z } +≤-supremum X X = v≤v , v≤v , λ { z x≤z y≤z → x≤z } + +join-comm : (x y : Value) → join x y ≡ join y x +join-comm U U = ≡.refl +join-comm U T = ≡.refl +join-comm U F = ≡.refl +join-comm U X = ≡.refl +join-comm T U = ≡.refl +join-comm T T = ≡.refl +join-comm T F = ≡.refl +join-comm T X = ≡.refl +join-comm F U = ≡.refl +join-comm F T = ≡.refl +join-comm F F = ≡.refl +join-comm F X = ≡.refl +join-comm X U = ≡.refl +join-comm X T = ≡.refl +join-comm X F = ≡.refl +join-comm X X = ≡.refl + +join-assoc : (x y z : Value) → join (join x y) z ≡ join x (join y z) +join-assoc U y z = ≡.refl +join-assoc T U z = ≡.refl +join-assoc T T U = ≡.refl +join-assoc T T T = ≡.refl +join-assoc T T F = ≡.refl +join-assoc T T X = ≡.refl +join-assoc T F U = ≡.refl +join-assoc T F T = ≡.refl +join-assoc T F F = ≡.refl +join-assoc T F X = ≡.refl +join-assoc T X U = ≡.refl +join-assoc T X T = ≡.refl +join-assoc T X F = ≡.refl +join-assoc T X X = ≡.refl +join-assoc F U z = ≡.refl +join-assoc F T U = ≡.refl +join-assoc F T T = ≡.refl +join-assoc F T F = ≡.refl +join-assoc F T X = ≡.refl +join-assoc F F U = ≡.refl +join-assoc F F T = ≡.refl +join-assoc F F F = ≡.refl +join-assoc F F X = ≡.refl +join-assoc F X U = ≡.refl +join-assoc F X T = ≡.refl +join-assoc F X F = ≡.refl +join-assoc F X X = ≡.refl +join-assoc X U z = ≡.refl +join-assoc X T U = ≡.refl +join-assoc X T T = ≡.refl +join-assoc X T F = ≡.refl +join-assoc X T X = ≡.refl +join-assoc X F U = ≡.refl +join-assoc X F T = ≡.refl +join-assoc X F F = ≡.refl +join-assoc X F X = ≡.refl +join-assoc X X U = ≡.refl +join-assoc X X T = ≡.refl +join-assoc X X F = ≡.refl +join-assoc X X X = ≡.refl + +Lattice : BoundedJoinSemilattice 0ℓ 0ℓ 0ℓ +Lattice = record + { Carrier = Value + ; _≈_ = _≡_ + ; _≤_ = ≤-Value + ; _∨_ = join + ; ⊥ = U + ; isBoundedJoinSemilattice = record + { isJoinSemilattice = record + { isPartialOrder = record + { isPreorder = record + { isEquivalence = ≡.isEquivalence + ; reflexive = ≤-reflexive + ; trans = ≤-transitive + } + ; antisym = ≤-antisymmetric + } + ; supremum = ≤-supremum + } + ; minimum = λ where + U → v≤v + T → U≤T + F → U≤F + X → U≤X + } + } + +module Lattice = BoundedJoinSemilattice Lattice + +Monoid : CommutativeMonoid 0ℓ 0ℓ +Monoid .Carrier = Lattice.Carrier +Monoid ._≈_ = Lattice._≈_ +Monoid ._∙_ = Lattice._∨_ +Monoid .ε = Lattice.⊥ +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .isEquivalence = ≡.isEquivalence +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .isMagma .∙-cong = ≡.cong₂ join +Monoid .isCommutativeMonoid .isMonoid .isSemigroup .assoc = join-assoc +Monoid .isCommutativeMonoid .isMonoid .identity = LatticeProp.identity Lattice +Monoid .isCommutativeMonoid .comm = join-comm |