diff options
Diffstat (limited to 'Data/Circuit')
| -rw-r--r-- | Data/Circuit/Gate.agda | 137 | ||||
| -rw-r--r-- | Data/Circuit/Typecheck.agda | 78 |
2 files changed, 215 insertions, 0 deletions
diff --git a/Data/Circuit/Gate.agda b/Data/Circuit/Gate.agda new file mode 100644 index 0000000..915ee8b --- /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.Base using (HypergraphLabel; module Edge; module HypergraphList) +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..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 |