aboutsummaryrefslogtreecommitdiff
path: root/Data
diff options
context:
space:
mode:
Diffstat (limited to 'Data')
-rw-r--r--Data/Castable.agda50
-rw-r--r--Data/Circuit/Convert.agda201
-rw-r--r--Data/Circuit/Gate.agda137
-rw-r--r--Data/Circuit/Typecheck.agda78
-rw-r--r--Data/Hypergraph/Base.agda26
-rw-r--r--Data/Hypergraph/Edge.agda335
-rw-r--r--Data/Hypergraph/Label.agda36
-rw-r--r--Data/Hypergraph/Setoid.agda50
-rw-r--r--Data/Permutation.agda217
-rw-r--r--Data/Permutation/Sort.agda29
-rw-r--r--Data/SExp.agda75
-rw-r--r--Data/SExp/Parser.agda73
12 files changed, 1307 insertions, 0 deletions
diff --git a/Data/Castable.agda b/Data/Castable.agda
new file mode 100644
index 0000000..4f85b3d
--- /dev/null
+++ b/Data/Castable.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Castable where
+
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst; cong; module ≡-Reasoning)
+open import Relation.Binary using (Sym; Trans; _⇒_)
+
+record IsCastable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} (B : A → Set ℓ₂) : Set (ℓ₁ ⊔ ℓ₂) where
+
+ field
+ cast : {e e′ : A} → .(e ≡ e′) → B e → B e′
+ cast-trans
+ : {m n o : A}
+ → .(eq₁ : m ≡ n)
+ .(eq₂ : n ≡ o)
+ (x : B m)
+ → cast eq₂ (cast eq₁ x) ≡ cast (trans eq₁ eq₂) x
+ cast-is-id : {m : A} .(eq : m ≡ m) (x : B m) → cast eq x ≡ x
+ subst-is-cast : {m n : A} (eq : m ≡ n) (x : B m) → subst B eq x ≡ cast eq x
+
+ infix 3 _≈[_]_
+ _≈[_]_ : {n m : A} → B n → .(eq : n ≡ m) → B m → Set ℓ₂
+ _≈[_]_ x eq y = cast eq x ≡ y
+
+ ≈-reflexive : {n : A} → _≡_ ⇒ (λ xs ys → _≈[_]_ {n} xs refl ys)
+ ≈-reflexive {n} {x} {y} eq = trans (cast-is-id refl x) eq
+
+ ≈-sym : {m n : A} .{m≡n : m ≡ n} → Sym _≈[ m≡n ]_ _≈[ sym m≡n ]_
+ ≈-sym {m} {n} {m≡n} {x} {y} x≡y = begin
+ cast (sym m≡n) y ≡⟨ cong (cast (sym m≡n)) x≡y ⟨
+ cast (sym m≡n) (cast m≡n x) ≡⟨ cast-trans m≡n (sym m≡n) x ⟩
+ cast (trans m≡n (sym m≡n)) x ≡⟨ cast-is-id (trans m≡n (sym m≡n)) x ⟩
+ x ∎
+ where
+ open ≡-Reasoning
+
+ ≈-trans : {m n o : A} .{m≡n : m ≡ n} .{n≡o : n ≡ o} → Trans _≈[ m≡n ]_ _≈[ n≡o ]_ _≈[ trans m≡n n≡o ]_
+ ≈-trans {m} {n} {o} {m≡n} {n≡o} {x} {y} {z} x≡y y≡z = begin
+ cast (trans m≡n n≡o) x ≡⟨ cast-trans m≡n n≡o x ⟨
+ cast n≡o (cast m≡n x) ≡⟨ cong (cast n≡o) x≡y ⟩
+ cast n≡o y ≡⟨ y≡z ⟩
+ z ∎
+ where
+ open ≡-Reasoning
+
+record Castable {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} : Set (suc (ℓ₁ ⊔ ℓ₂)) where
+ field
+ B : A → Set ℓ₂
+ isCastable : IsCastable B
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
diff --git a/Data/Hypergraph/Base.agda b/Data/Hypergraph/Base.agda
new file mode 100644
index 0000000..6988cf0
--- /dev/null
+++ b/Data/Hypergraph/Base.agda
@@ -0,0 +1,26 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Base (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (Edge; decTotalOrder; showEdge)
+open import Data.List.Base using (List; map)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String; unlines)
+
+import Data.List.Sort as Sort
+
+record Hypergraph (v : ℕ) : Set where
+ constructor mkHypergraph
+ field
+ edges : List (Edge v)
+
+sortHypergraph : {v : ℕ} → Hypergraph v → Hypergraph v
+sortHypergraph {v} H = record { edges = sort edges }
+ where
+ open Hypergraph H
+ open Sort decTotalOrder using (sort)
+
+showHypergraph : {v : ℕ} → Hypergraph v → String
+showHypergraph record { edges = e} = unlines (map showEdge e)
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
new file mode 100644
index 0000000..13b9278
--- /dev/null
+++ b/Data/Hypergraph/Edge.agda
@@ -0,0 +1,335 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+
+
+open import Relation.Binary using (Rel; IsStrictTotalOrder; Tri; Trichotomous; _Respects_)
+open import Data.Castable using (IsCastable)
+open import Data.Fin using (Fin)
+open import Data.Fin.Show using () renaming (show to showFin)
+open import Data.Nat.Base using (ℕ; _<_)
+open import Data.Nat.Properties using (<-irrefl; <-trans; <-resp₂-≡; <-cmp)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.String using (String; _<+>_)
+open import Data.Vec.Relation.Binary.Pointwise.Inductive using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
+open import Data.Vec.Show using () renaming (show to showVec)
+open import Level using (0ℓ)
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Nullary using (¬_)
+
+import Data.Fin.Base as Fin
+import Data.Fin.Properties as FinProp
+import Data.Vec.Base as VecBase
+import Data.Vec.Relation.Binary.Equality.Cast as VecCast
+import Data.Vec.Relation.Binary.Lex.Strict as Lex
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Properties.DecTotalOrder as DTOP
+import Relation.Binary.Properties.StrictTotalOrder as STOP
+
+module HL = HypergraphLabel HL
+open HL using (Label; cast; cast-is-id)
+open VecBase using (Vec)
+
+record Edge (v : ℕ) : Set where
+ field
+ {arity} : ℕ
+ label : Label arity
+ ports : Vec (Fin v) arity
+
+open ≡ using (_≡_)
+open VecCast using (_≈[_]_)
+
+record ≈-Edge {n : ℕ} (E E′ : Edge n) : Set where
+ module E = Edge E
+ module E′ = Edge E′
+ field
+ ≡arity : E.arity ≡ E′.arity
+ ≡label : cast ≡arity E.label ≡ E′.label
+ ≡ports : E.ports ≈[ ≡arity ] E′.ports
+
+≈-Edge-refl : {v : ℕ} {x : Edge v} → ≈-Edge x x
+≈-Edge-refl {_} {x} = record
+ { ≡arity = ≡.refl
+ ; ≡label = HL.≈-reflexive ≡.refl
+ ; ≡ports = VecCast.≈-reflexive ≡.refl
+ }
+ where
+ open Edge x using (arity; label)
+ open DecTotalOrder (HL.decTotalOrder arity) using (module Eq)
+
+≈-Edge-sym : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ≈-Edge y x
+≈-Edge-sym {_} {x} {y} x≈y = record
+ { ≡arity = ≡.sym ≡arity
+ ; ≡label = HL.≈-sym ≡label
+ ; ≡ports = VecCast.≈-sym ≡ports
+ }
+ where
+ open ≈-Edge x≈y
+ open DecTotalOrder (HL.decTotalOrder E.arity) using (module Eq)
+
+≈-Edge-trans : {v : ℕ} {i j k : Edge v} → ≈-Edge i j → ≈-Edge j k → ≈-Edge i k
+≈-Edge-trans {_} {i} {j} {k} i≈j j≈k = record
+ { ≡arity = ≡.trans i≈j.≡arity j≈k.≡arity
+ ; ≡label = HL.≈-trans i≈j.≡label j≈k.≡label
+ ; ≡ports = VecCast.≈-trans i≈j.≡ports j≈k.≡ports
+ }
+ where
+ module i≈j = ≈-Edge i≈j
+ module j≈k = ≈-Edge j≈k
+
+open import Relation.Binary using (IsEquivalence)
+≈-Edge-IsEquivalence : {v : ℕ} → IsEquivalence (≈-Edge {v})
+≈-Edge-IsEquivalence = record
+ { refl = ≈-Edge-refl
+ ; sym = ≈-Edge-sym
+ ; trans = ≈-Edge-trans
+ }
+
+open HL using (_[_<_])
+_<<_ : {v a : ℕ} → Rel (Vec (Fin v) a) 0ℓ
+_<<_ {v} = Lex.Lex-< _≡_ (Fin._<_ {v})
+data <-Edge {v : ℕ} : Edge v → Edge v → Set where
+ <-arity
+ : {x y : Edge v}
+ → Edge.arity x < Edge.arity y
+ → <-Edge x y
+ <-label
+ : {x y : Edge v}
+ (≡a : Edge.arity x ≡ Edge.arity y)
+ → Edge.arity y [ cast ≡a (Edge.label x) < Edge.label y ]
+ → <-Edge x y
+ <-ports
+ : {x y : Edge v}
+ (≡a : Edge.arity x ≡ Edge.arity y)
+ (≡l : Edge.label x HL.≈[ ≡a ] Edge.label y)
+ → VecBase.cast ≡a (Edge.ports x) << Edge.ports y
+ → <-Edge x y
+
+<-Edge-irrefl : {v : ℕ} {x y : Edge v} → ≈-Edge x y → ¬ <-Edge x y
+<-Edge-irrefl record { ≡arity = ≡a } (<-arity n<m) = <-irrefl ≡a n<m
+<-Edge-irrefl record { ≡label = ≡l } (<-label _ (_ , x≉y)) = x≉y ≡l
+<-Edge-irrefl record { ≡ports = ≡p } (<-ports ≡.refl ≡l x<y)
+ = Lex.<-irrefl FinProp.<-irrefl (≡⇒Pointwise-≡ ≡p) x<y
+
+<-Edge-trans : {v : ℕ} {i j k : Edge v} → <-Edge i j → <-Edge j k → <-Edge i k
+<-Edge-trans (<-arity i<j) (<-arity j<k) = <-arity (<-trans i<j j<k)
+<-Edge-trans (<-arity i<j) (<-label ≡.refl j<k) = <-arity i<j
+<-Edge-trans (<-arity i<j) (<-ports ≡.refl _ j<k) = <-arity i<j
+<-Edge-trans (<-label ≡.refl i<j) (<-arity j<k) = <-arity j<k
+<-Edge-trans {_} {i} (<-label ≡.refl i<j) (<-label ≡.refl j<k)
+ = <-label ≡.refl (<-label-trans i<j (<-respˡ-≈ (HL.≈-reflexive ≡.refl) j<k))
+ where
+ open DTOP (HL.decTotalOrder (Edge.arity i)) using (<-respˡ-≈) renaming (<-trans to <-label-trans)
+<-Edge-trans {k = k} (<-label ≡.refl i<j) (<-ports ≡.refl ≡.refl _)
+ = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) i<j)
+ where
+ open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respʳ-≈)
+<-Edge-trans (<-ports ≡.refl _ _) (<-arity j<k) = <-arity j<k
+<-Edge-trans {k = k} (<-ports ≡.refl ≡.refl _) (<-label ≡.refl j<k)
+ = <-label ≡.refl (<-respˡ-≈ (≡.cong (cast _) (HL.≈-reflexive ≡.refl)) j<k)
+ where
+ open DTOP (HL.decTotalOrder (Edge.arity k)) using (<-respˡ-≈)
+<-Edge-trans {j = j} (<-ports ≡.refl ≡l₁ i<j) (<-ports ≡.refl ≡l₂ j<k)
+ rewrite (VecCast.cast-is-id ≡.refl (Edge.ports j))
+ = <-ports ≡.refl
+ (HL.≈-trans ≡l₁ ≡l₂)
+ (Lex.<-trans ≡-isPartialEquivalence FinProp.<-resp₂-≡ FinProp.<-trans i<j j<k)
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respˡ-≈ : {v : ℕ} {y : Edge v} → (λ x → <-Edge x y) Respects ≈-Edge
+<-Edge-respˡ-≈ ≈x (<-arity x₁<y) = <-arity (proj₂ <-resp₂-≡ ≡arity x₁<y)
+ where
+ open ≈-Edge ≈x using (≡arity)
+<-Edge-respˡ-≈ {_} {y} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x₁<y)
+ = <-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x₁<y)
+ where
+ module y = Edge y
+ open DTOP (HL.decTotalOrder y.arity) using (<-respˡ-≈)
+<-Edge-respˡ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x₁<y)
+ = <-ports
+ ≡.refl
+ (≡.cong (cast _) (HL.≈-reflexive ≡.refl))
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+ x₁<y)
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+<-Edge-respʳ-≈ : {v : ℕ} {x : Edge v} → <-Edge x Respects ≈-Edge
+<-Edge-respʳ-≈ record { ≡arity = ≡a } (<-arity x<y₁) = <-arity (proj₁ <-resp₂-≡ ≡a x<y₁)
+<-Edge-respʳ-≈ {_} {x} record { ≡arity = ≡.refl ; ≡label = ≡.refl } (<-label ≡.refl x<y₁)
+ = <-label ≡.refl (<-respʳ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y₁)
+ where
+ module x = Edge x
+ open DTOP (HL.decTotalOrder x.arity) using (<-respʳ-≈)
+<-Edge-respʳ-≈ record { ≡arity = ≡.refl ; ≡label = ≡.refl; ≡ports = ≡.refl} (<-ports ≡.refl ≡.refl x<y₁)
+ = <-ports
+ ≡.refl
+ (≡.cong (cast _) (≡.sym (HL.≈-reflexive ≡.refl)))
+ (Lex.<-respectsʳ
+ ≡-isPartialEquivalence
+ FinProp.<-respʳ-≡
+ (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+ x<y₁)
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+
+open Tri
+open ≈-Edge
+tri : {v : ℕ} → Trichotomous (≈-Edge {v}) (<-Edge {v})
+tri x y with <-cmp x.arity y.arity
+ where
+ module x = Edge x
+ module y = Edge y
+tri x y | tri< x<y x≢y y≮x = tri< (<-arity x<y) (λ x≡y → x≢y (≡arity x≡y)) ¬y<x
+ where
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label ≡a _) = x≢y (≡.sym ≡a)
+ ¬y<x (<-ports ≡a _ _) = x≢y (≡.sym ≡a)
+tri x y | tri≈ x≮y ≡.refl y≮x = compare-label
+ where
+ module x = Edge x
+ module y = Edge y
+ open StrictTotalOrder (HL.strictTotalOrder x.arity) using (compare)
+ import Relation.Binary.Properties.DecTotalOrder
+ open DTOP (HL.decTotalOrder x.arity) using (<-respˡ-≈)
+ compare-label : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+ compare-label with compare x.label y.label
+ ... | tri< x<y x≢y y≮x′ = tri<
+ (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) x<y))
+ (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+ ¬y<x
+ where
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+ ¬y<x (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym ≡l) (cast-is-id ≡.refl y.label))
+ ... | tri≈ x≮y′ x≡y′ y≮x′ = compare-ports
+ where
+ compare-ports : Tri (<-Edge x y) (≈-Edge x y) (<-Edge y x)
+ compare-ports with Lex.<-cmp ≡.sym FinProp.<-cmp x.ports y.ports
+ ... | tri< x<y x≢y y≮x″ =
+ tri<
+ (<-ports ≡.refl
+ (HL.≈-reflexive x≡y′)
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+ x<y))
+ (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+ ¬y<x
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+ ¬y<x (<-ports _ _ y<x) =
+ y≮x″
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+ y<x)
+ ... | tri≈ x≮y″ x≡y″ y≮x″ = tri≈
+ ¬x<y
+ (record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive x≡y′ ; ≡ports = VecCast.≈-reflexive (Pointwise-≡⇒≡ x≡y″) })
+ ¬y<x
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+ ¬x<y (<-ports _ _ x<y) =
+ x≮y″
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+ x<y)
+ ¬y<x : ¬ <-Edge y x
+ ¬y<x (<-arity y<x) = y≮x y<x
+ ¬y<x (<-label _ y<x) = y≮x′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) y<x)
+ ¬y<x (<-ports _ _ y<x) =
+ y≮x″
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+ y<x)
+
+ ... | tri> x≮y″ x≢y y<x =
+ tri>
+ ¬x<y
+ (λ x≡y → x≢y (≡⇒Pointwise-≡ (≡.trans (≡.sym (VecCast.≈-reflexive ≡.refl)) (≡ports x≡y))))
+ (<-ports
+ ≡.refl
+ (HL.≈-sym (HL.≈-reflexive x≡y′))
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (≡.sym (VecCast.≈-reflexive ≡.refl)))
+ y<x))
+ where
+ open IsEquivalence ≡.isEquivalence using () renaming (isPartialEquivalence to ≡-isPartialEquivalence)
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label _ x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+ ¬x<y (<-ports _ _ x<y) =
+ x≮y″
+ (Lex.<-respectsˡ
+ ≡-isPartialEquivalence
+ FinProp.<-respˡ-≡
+ (≡⇒Pointwise-≡ (VecCast.≈-reflexive ≡.refl))
+ x<y)
+ ... | tri> x≮y′ x≢y y<x = tri>
+ ¬x<y
+ (λ x≡y → x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) (≡label x≡y)))
+ (<-label ≡.refl (<-respˡ-≈ (≡.sym (HL.≈-reflexive ≡.refl)) y<x))
+ where
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label ≡a x<y) = x≮y′ (<-respˡ-≈ (HL.≈-reflexive ≡.refl) x<y)
+ ¬x<y (<-ports _ ≡l _) = x≢y (≡.trans (≡.sym (HL.≈-reflexive ≡.refl)) ≡l)
+tri x y | tri> x≮y x≢y y<x = tri> ¬x<y (λ x≡y → x≢y (≡arity x≡y)) (<-arity y<x)
+ where
+ ¬x<y : ¬ <-Edge x y
+ ¬x<y (<-arity x<y) = x≮y x<y
+ ¬x<y (<-label ≡a x<y) = x≢y ≡a
+ ¬x<y (<-ports ≡a _ _) = x≢y ≡a
+
+isStrictTotalOrder : {v : ℕ} → IsStrictTotalOrder (≈-Edge {v}) (<-Edge {v})
+isStrictTotalOrder = record
+ { isStrictPartialOrder = record
+ { isEquivalence = ≈-Edge-IsEquivalence
+ ; irrefl = <-Edge-irrefl
+ ; trans = <-Edge-trans
+ ; <-resp-≈ = <-Edge-respʳ-≈ , <-Edge-respˡ-≈
+ }
+ ; compare = tri
+ }
+
+strictTotalOrder : {v : ℕ} → StrictTotalOrder 0ℓ 0ℓ 0ℓ
+strictTotalOrder {v} = record
+ { Carrier = Edge v
+ ; _≈_ = ≈-Edge {v}
+ ; _<_ = <-Edge {v}
+ ; isStrictTotalOrder = isStrictTotalOrder {v}
+ }
+
+showEdge : {v : ℕ} → Edge v → String
+showEdge record { arity = a ; label = l ; ports = p} = HL.showLabel a l <+> showVec showFin p
+
+open module STOP′ {v} = STOP (strictTotalOrder {v}) using (decTotalOrder) public
+
+≈-Edge⇒≡ : {v : ℕ} {x y : Edge v} → ≈-Edge x y → x ≡ y
+≈-Edge⇒≡ {v} {record { label = l ; ports = p }} record { ≡arity = ≡.refl ; ≡label = ≡.refl ; ≡ports = ≡.refl }
+ rewrite cast-is-id ≡.refl l
+ rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
new file mode 100644
index 0000000..c23d33a
--- /dev/null
+++ b/Data/Hypergraph/Label.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --without-K --safe #-}
+module Data.Hypergraph.Label where
+
+open import Data.Castable using (IsCastable)
+open import Data.Nat.Base using (ℕ)
+open import Data.String using (String)
+open import Level using (Level; suc)
+open import Relation.Binary using (Rel; IsDecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Properties.DecTotalOrder using (<-strictTotalOrder; _<_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+
+record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
+
+ field
+ Label : ℕ → Set ℓ
+ showLabel : (n : ℕ) → Label n → String
+ isCastable : IsCastable Label
+ _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+ isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
+
+ decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+ decTotalOrder n = record
+ { Carrier = Label n
+ ; _≈_ = _≡_
+ ; _≤_ = n [_≤_]
+ ; isDecTotalOrder = isDecTotalOrder n
+ }
+
+ _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+ _[_<_] n = _<_ (decTotalOrder n)
+
+ strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+ strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
+
+ open IsCastable isCastable public
diff --git a/Data/Hypergraph/Setoid.agda b/Data/Hypergraph/Setoid.agda
new file mode 100644
index 0000000..c39977d
--- /dev/null
+++ b/Data/Hypergraph/Setoid.agda
@@ -0,0 +1,50 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Hypergraph.Label using (HypergraphLabel)
+
+module Data.Hypergraph.Setoid (HL : HypergraphLabel) where
+
+open import Data.Hypergraph.Edge HL using (decTotalOrder)
+open import Data.Hypergraph.Base HL using (Hypergraph; sortHypergraph)
+open import Data.Nat.Base using (ℕ)
+open import Level using (0ℓ)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+
+record ≈-Hypergraph {v : ℕ} (H H′ : Hypergraph v) : Set where
+ module H = Hypergraph H
+ module H′ = Hypergraph H′
+ field
+ ≡sorted : sortHypergraph H ≡ sortHypergraph H′
+ open Hypergraph using (edges)
+ ≡edges : edges (sortHypergraph H) ≡ edges (sortHypergraph H′)
+ ≡edges = ≡.cong edges ≡sorted
+ open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-reflexive; ↭-sym; ↭-trans)
+ open import Data.List.Sort decTotalOrder using (sort-↭)
+ ↭edges : H.edges ↭ H′.edges
+ ↭edges = ↭-trans (↭-sym (sort-↭ H.edges)) (↭-trans (↭-reflexive ≡edges) (sort-↭ H′.edges))
+
+≈-refl : {v : ℕ} {H : Hypergraph v} → ≈-Hypergraph H H
+≈-refl = record { ≡sorted = ≡.refl }
+
+≈-sym : {v : ℕ} {H H′ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H
+≈-sym ≈H = record { ≡sorted = ≡.sym ≡sorted }
+ where
+ open ≈-Hypergraph ≈H
+
+≈-trans : {v : ℕ} {H H′ H″ : Hypergraph v} → ≈-Hypergraph H H′ → ≈-Hypergraph H′ H″ → ≈-Hypergraph H H″
+≈-trans ≈H₁ ≈H₂ = record { ≡sorted = ≡.trans ≈H₁.≡sorted ≈H₂.≡sorted }
+ where
+ module ≈H₁ = ≈-Hypergraph ≈H₁
+ module ≈H₂ = ≈-Hypergraph ≈H₂
+
+Hypergraph-Setoid : (v : ℕ) → Setoid 0ℓ 0ℓ
+Hypergraph-Setoid v = record
+ { Carrier = Hypergraph v
+ ; _≈_ = ≈-Hypergraph
+ ; isEquivalence = record
+ { refl = ≈-refl
+ ; sym = ≈-sym
+ ; trans = ≈-trans
+ }
+ }
diff --git a/Data/Permutation.agda b/Data/Permutation.agda
new file mode 100644
index 0000000..55c8748
--- /dev/null
+++ b/Data/Permutation.agda
@@ -0,0 +1,217 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Permutation {ℓ : Level} {A : Set ℓ} where
+
+import Data.Fin as Fin
+import Data.Fin.Properties as FinProp
+import Data.Fin.Permutation as ↔-Fin
+import Data.List as List
+import Data.List.Properties as ListProp
+import Data.List.Relation.Binary.Permutation.Propositional as ↭-List
+import Data.Nat as Nat
+import Data.Vec.Functional as Vector
+import Data.Vec.Functional.Properties as VectorProp
+import Data.Vec.Functional.Relation.Binary.Permutation as ↭-Vec
+import Data.Vec.Functional.Relation.Binary.Permutation.Properties as ↭-VecProp
+
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Vec.Functional.Relation.Unary.Any using (Any)
+open import Function.Base using (_∘_)
+
+open ↭-Vec using () renaming (_↭_ to _↭′_)
+open ↭-List using (_↭_; ↭-sym; module PermutationReasoning)
+open ↔-Fin using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
+open List using (List) hiding (module List)
+open Fin using (Fin; cast) hiding (module Fin)
+open Vector using (Vector; toList; fromList)
+open Fin.Fin
+open Nat using (ℕ; zero; suc)
+open _↭_
+
+module _ where
+
+ open Fin using (#_)
+ open ↔-Fin using (lift₀; insert)
+ open ↭-VecProp using (↭-refl; ↭-trans)
+
+ -- convert a List permutation to a Vector permutation
+ fromList-↭
+ : {xs ys : List A}
+ → xs ↭ ys
+ → fromList xs ↭′ fromList ys
+ fromList-↭ refl = ↭-refl
+ fromList-↭ (prep _ xs↭ys)
+ with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = lift₀ n↔m , λ where
+ zero → ≡.refl
+ (suc i) → xs↭ys′ i
+ fromList-↭ (swap x y xs↭ys)
+ with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = insert (# 0) (# 1) (lift₀ n↔m) , λ where
+ zero → ≡.refl
+ (suc zero) → ≡.refl
+ (suc (suc i)) → xs↭ys′ i
+ fromList-↭ (trans {xs} xs↭ys ys↭zs) =
+ ↭-trans {_} {_} {_} {i = fromList xs} (fromList-↭ xs↭ys) (fromList-↭ ys↭zs)
+
+-- witness for an element in a Vector
+_∈_ : A → {n : ℕ} → Vector A n → Set ℓ
+x ∈ xs = Any (x ≡_) xs
+
+-- apply a permutation to a witness
+apply
+ : {n m : ℕ}
+ {xs : Vector A n}
+ {ys : Vector A m}
+ {x : A}
+ → (xs↭ys : xs ↭′ ys)
+ → x ∈ xs
+ → x ∈ ys
+apply {suc n} {zero} (↔n , _) (i , _) with () ← ↔n ⟨$⟩ˡ i
+apply {suc n} {suc m} {xs} {ys} {x} (↔n , ↔≗) (i , x≡xs-i) = i′ , x≡ys-i′
+ where
+ i′ : Fin (suc m)
+ i′ = ↔n ⟨$⟩ˡ i
+ open ≡.≡-Reasoning
+ x≡ys-i′ : x ≡ ys i′
+ x≡ys-i′ = begin
+ x ≡⟨ x≡xs-i ⟩
+ xs i ≡⟨ ≡.cong xs (↔-Fin.inverseʳ ↔n) ⟨
+ xs (↔n ⟨$⟩ʳ (↔n ⟨$⟩ˡ i)) ≡⟨⟩
+ xs (↔n ⟨$⟩ʳ i′) ≡⟨ ↔≗ i′ ⟩
+ ys i′ ∎
+
+-- remove an element from a Vector
+remove : {n : ℕ} {x : A} (xs : Vector A (suc n)) → x ∈ xs → Vector A n
+remove xs (i , _) = Vector.removeAt xs i
+
+-- remove an element and its image from a permutation
+↭-remove
+ : {n m : ℕ}
+ {xs : Vector A (suc n)}
+ {ys : Vector A (suc m)}
+ {x : A}
+ → (xs↭ys : xs ↭′ ys)
+ → (x∈xs : x ∈ xs)
+ → let x∈ys = apply xs↭ys x∈xs in
+ remove xs x∈xs ↭′ remove ys x∈ys
+↭-remove {n} {m} {xs} {ys} {x} xs↭ys@(ρ , ↔≗) x∈xs@(k , _) = ρ⁻ , ↔≗⁻
+ where
+ k′ : Fin (suc m)
+ k′ = ρ ⟨$⟩ˡ k
+ x∈ys : x ∈ ys
+ x∈ys = apply xs↭ys x∈xs
+ ρ⁻ : Permutation m n
+ ρ⁻ = ↔-Fin.remove k′ ρ
+ xs⁻ : Vector A n
+ xs⁻ = remove xs x∈xs
+ ys⁻ : Vector A m
+ ys⁻ = remove ys x∈ys
+ open ≡.≡-Reasoning
+ open Fin using (punchIn)
+ ↔≗⁻ : (i : Fin m) → xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡ ys⁻ i
+ ↔≗⁻ i = begin
+ xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡⟨⟩
+ remove xs x∈xs (ρ⁻ ⟨$⟩ʳ i) ≡⟨⟩
+ xs (punchIn k (ρ⁻ ⟨$⟩ʳ i)) ≡⟨ ≡.cong xs (↔-Fin.punchIn-permute′ ρ k i) ⟨
+ xs (ρ ⟨$⟩ʳ (punchIn k′ i)) ≡⟨ ↔≗ (punchIn k′ i) ⟩
+ ys (punchIn k′ i) ≡⟨⟩
+ remove ys x∈ys i ≡⟨⟩
+ ys⁻ i ∎
+
+open List.List
+open List using (length; insertAt)
+
+-- build a permutation which moves the first element of a list to an arbitrary position
+↭-insert-half
+ : {x₀ : A}
+ {xs : List A}
+ → (i : Fin (suc (length xs)))
+ → x₀ ∷ xs ↭ insertAt xs i x₀
+↭-insert-half zero = refl
+↭-insert-half {x₀} {x₁ ∷ xs} (suc i) = trans (swap x₀ x₁ refl) (prep x₁ (↭-insert-half i))
+
+-- add a mapping to a permutation, given a value and its start and end positions
+↭-insert
+ : {xs ys : List A}
+ → xs ↭ ys
+ → (i : Fin (suc (length xs)))
+ (j : Fin (suc (length ys)))
+ (x : A)
+ → insertAt xs i x ↭ insertAt ys j x
+↭-insert {xs} {ys} xs↭ys i j x = xs↭ys⁺
+ where
+ open PermutationReasoning
+ xs↭ys⁺ : insertAt xs i x ↭ insertAt ys j x
+ xs↭ys⁺ = begin
+ insertAt xs i x ↭⟨ ↭-insert-half i ⟨
+ x ∷ xs <⟨ xs↭ys ⟩
+ x ∷ ys ↭⟨ ↭-insert-half j ⟩
+ insertAt ys j x ∎
+
+open ListProp using (length-tabulate; tabulate-cong)
+insertAt-toList
+ : {n : ℕ}
+ {v : Vector A n}
+ (i : Fin (suc (length (toList v))))
+ (i′ : Fin (suc n))
+ → i ≡ cast (≡.cong suc (≡.sym (length-tabulate v))) i′
+ → (x : A)
+ → insertAt (toList v) i x
+ ≡ toList (Vector.insertAt v i′ x)
+insertAt-toList zero zero _ x = ≡.refl
+insertAt-toList {suc n} {v} (suc i) (suc i′) ≡.refl x =
+ ≡.cong (v zero ∷_) (insertAt-toList i i′ ≡.refl x)
+
+-- convert a Vector permutation to a List permutation
+toList-↭
+ : {n m : ℕ}
+ {xs : Vector A n}
+ {ys : Vector A m}
+ → xs ↭′ ys
+ → toList xs ↭ toList ys
+toList-↭ {zero} {zero} _ = refl
+toList-↭ {zero} {suc m} (ρ , _) with () ← ρ ⟨$⟩ʳ zero
+toList-↭ {suc n} {zero} (ρ , _) with () ← ρ ⟨$⟩ˡ zero
+toList-↭ {suc n} {suc m} {xs} {ys} xs↭ys′ = xs↭ys
+ where
+ -- first element and its image
+ x₀ : A
+ x₀ = xs zero
+ x₀∈xs : x₀ ∈ xs
+ x₀∈xs = zero , ≡.refl
+ x₀∈ys : x₀ ∈ ys
+ x₀∈ys = apply xs↭ys′ x₀∈xs
+ -- reduce the problem by removing those elements
+ xs⁻ : Vector A n
+ xs⁻ = remove xs x₀∈xs
+ ys⁻ : Vector A m
+ ys⁻ = remove ys x₀∈ys
+ xs↭ys⁻ : xs⁻ ↭′ ys⁻
+ xs↭ys⁻ = ↭-remove xs↭ys′ x₀∈xs
+ -- recursion on the reduced problem
+ xs↭ys⁻′ : toList xs⁻ ↭ toList ys⁻
+ xs↭ys⁻′ = toList-↭ xs↭ys⁻
+ -- indices for working with vectors
+ i : Fin (suc n)
+ i = proj₁ x₀∈xs
+ j : Fin (suc m)
+ j = proj₁ x₀∈ys
+ i′ : Fin (suc (length (toList xs⁻)))
+ i′ = cast (≡.sym (≡.cong suc (length-tabulate xs⁻))) i
+ j′ : Fin (suc (length (toList ys⁻)))
+ j′ = cast (≡.sym (≡.cong suc (length-tabulate ys⁻))) j
+ -- main construction
+ open VectorProp using (insertAt-removeAt)
+ open PermutationReasoning
+ open Vector using () renaming (insertAt to insertAt′)
+ xs↭ys : toList xs ↭ toList ys
+ xs↭ys = begin
+ toList xs ≡⟨ tabulate-cong (insertAt-removeAt xs i) ⟨
+ toList (insertAt′ xs⁻ i x₀) ≡⟨ insertAt-toList i′ i ≡.refl x₀ ⟨
+ insertAt (toList xs⁻) i′ x₀ ↭⟨ ↭-insert xs↭ys⁻′ i′ j′ x₀ ⟩
+ insertAt (toList ys⁻) j′ x₀ ≡⟨ insertAt-toList j′ j ≡.refl x₀ ⟩
+ toList (insertAt′ ys⁻ j x₀) ≡⟨ ≡.cong (toList ∘ insertAt′ ys⁻ j) (proj₂ x₀∈ys) ⟩
+ toList (insertAt′ ys⁻ j (ys j)) ≡⟨ tabulate-cong (insertAt-removeAt ys j) ⟩
+ toList ys ∎
diff --git a/Data/Permutation/Sort.agda b/Data/Permutation/Sort.agda
new file mode 100644
index 0000000..8d097f2
--- /dev/null
+++ b/Data/Permutation/Sort.agda
@@ -0,0 +1,29 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary.Bundles using (DecTotalOrder)
+
+module Data.Permutation.Sort {ℓ₁ ℓ₂ ℓ₃} (dto : DecTotalOrder ℓ₁ ℓ₂ ℓ₃) where
+
+open DecTotalOrder dto using (module Eq; totalOrder) renaming (Carrier to A)
+
+open import Data.List.Base using (List)
+open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid using (_≋_)
+open import Data.List.Relation.Binary.Permutation.Setoid Eq.setoid using (_↭_; module PermutationReasoning)
+open import Data.List.Relation.Unary.Sorted.TotalOrder.Properties using (↗↭↗⇒≋)
+open import Data.List.Sort dto using (sortingAlgorithm)
+open import Data.List.Sort.Base totalOrder using (SortingAlgorithm)
+open SortingAlgorithm sortingAlgorithm using (sort; sort-↭ₛ; sort-↗)
+
+sorted-≋
+ : {xs ys : List A}
+ → xs ↭ ys
+ → sort xs ≋ sort ys
+sorted-≋ {xs} {ys} xs↭ys = ↗↭↗⇒≋ totalOrder (sort-↗ xs) (sort-↗ ys) sort-xs↭sort-ys
+ where
+ open PermutationReasoning
+ sort-xs↭sort-ys : sort xs ↭ sort ys
+ sort-xs↭sort-ys = begin
+ sort xs ↭⟨ sort-↭ₛ xs ⟩
+ xs ↭⟨ xs↭ys ⟩
+ ys ↭⟨ sort-↭ₛ ys ⟨
+ sort ys ∎
diff --git a/Data/SExp.agda b/Data/SExp.agda
new file mode 100644
index 0000000..adf4325
--- /dev/null
+++ b/Data/SExp.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.SExp where
+
+open import Data.List using (List)
+open import Data.Nat.Base using (ℕ)
+open import Data.Nat.Show using () renaming (show to showNat)
+open import Data.String.Base as String using (String; parens; intersperse; _<+>_)
+
+open List
+
+module ListBased where
+
+ data SExp : Set where
+ Atom : String → SExp
+ Nat : ℕ → SExp
+ SExps : List SExp → SExp
+
+ mutual
+ showSExp : SExp → String
+ showSExp (Atom s) = s
+ showSExp (Nat n) = showNat n
+ showSExp (SExps xs) = parens (intersperse " " (showList xs))
+
+ -- expanded out map for termination checker
+ showList : List SExp → List String
+ showList [] = []
+ showList (x ∷ xs) = showSExp x ∷ showList xs
+
+module PairBased where
+
+ data SExp : Set where
+ Atom : String → SExp
+ Nat : ℕ → SExp
+ Nil : SExp
+ Pair : SExp → SExp → SExp
+
+ mutual
+ showSExp : SExp → String
+ showSExp (Atom s) = s
+ showSExp (Nat n) = showNat n
+ showSExp Nil = "()"
+ showSExp (Pair l r) = parens (showPair l r)
+
+ showPair : SExp → SExp → String
+ showPair x (Atom s) = showSExp x <+> "." <+> s
+ showPair x (Nat n) = showSExp x <+> "." <+> showNat n
+ showPair x Nil = showSExp x
+ showPair x (Pair l r) = showSExp x <+> showPair l r
+
+open ListBased public
+open PairBased
+
+mutual
+ sexpL→sexpP : ListBased.SExp → PairBased.SExp
+ sexpL→sexpP (Atom s) = Atom s
+ sexpL→sexpP (Nat n) = Nat n
+ sexpL→sexpP (SExps xs) = [sexpL]→sexpP xs
+
+ [sexpL]→sexpP : List (ListBased.SExp) → PairBased.SExp
+ [sexpL]→sexpP [] = Nil
+ [sexpL]→sexpP (x ∷ xs) = Pair (sexpL→sexpP x) ([sexpL]→sexpP xs)
+
+mutual
+ sexpP→sexpL : PairBased.SExp → ListBased.SExp
+ sexpP→sexpL (Atom s) = Atom s
+ sexpP→sexpL (Nat n) = Nat n
+ sexpP→sexpL Nil = SExps []
+ sexpP→sexpL (Pair x y) = SExps (sexpP→sexpL x ∷ sexpP→[sexpL] y)
+
+ sexpP→[sexpL] : PairBased.SExp → List (ListBased.SExp)
+ sexpP→[sexpL] (Atom _) = []
+ sexpP→[sexpL] (Nat _) = []
+ sexpP→[sexpL] Nil = []
+ sexpP→[sexpL] (Pair x y) = sexpP→sexpL x ∷ sexpP→[sexpL] y
diff --git a/Data/SExp/Parser.agda b/Data/SExp/Parser.agda
new file mode 100644
index 0000000..ec1b6a5
--- /dev/null
+++ b/Data/SExp/Parser.agda
@@ -0,0 +1,73 @@
+{-# OPTIONS --without-K --guardedness --safe #-}
+
+open import Text.Parser.Types.Core using (Parameters)
+
+module Data.SExp.Parser {l} {P : Parameters l} where
+
+import Data.String.Base as String
+open import Data.List as List using (List)
+
+open import Data.Char.Base using (Char)
+open import Data.List.Sized.Interface using (Sized)
+open import Data.List.NonEmpty as List⁺ using (List⁺) renaming (map to map⁺)
+open import Data.Subset using (Subset; into)
+open import Effect.Monad using (RawMonadPlus)
+open import Function.Base using (_∘_; _$_)
+open import Induction.Nat.Strong using (fix; map; □_)
+open import Relation.Binary.PropositionalEquality.Decidable using (DecidableEquality)
+open import Relation.Unary using (IUniversal; _⇒_)
+open import Level.Bounded using (theSet; [_])
+open import Text.Parser.Types P using (Parser)
+open import Text.Parser.Combinators {P = P} using (_<$>_; list⁺; _<|>_; _<$_; _<&_; _<&?_; box)
+open import Text.Parser.Combinators.Char {P = P} using (alpha; parens; withSpaces; spaces; char)
+open import Text.Parser.Combinators.Numbers {P = P} using (decimalℕ)
+
+open import Data.SExp using (SExp)
+open SExp
+
+open Parameters P using (M; Tok; Toks)
+
+module _
+ {{𝕄 : RawMonadPlus M}}
+ {{𝕊 : Sized Tok Toks}}
+ {{𝔻 : DecidableEquality (theSet Tok)}}
+ {{ℂ : Subset Char (theSet Tok)}}
+ {{ℂ⁻ : Subset (theSet Tok) Char}}
+ where
+
+ -- An atom is just a non-empty list of alphabetical characters.
+ -- We use `<$>` to turn that back into a string and apply the `Atom` constructor.
+ atom : ∀[ Parser [ SExp ] ]
+ atom = Atom ∘ String.fromList⁺ ∘ map⁺ (into ℂ⁻) <$> list⁺ alpha
+
+ -- Natural number parser
+ nat : ∀[ Parser [ SExp ] ]
+ nat = Nat <$> decimalℕ
+
+ -- Empty list parser
+ nil : ∀[ Parser [ SExp ] ]
+ nil = SExps List.[] <$ char '(' <&? box spaces <& box (char ')')
+
+ -- Parser for a list of S-Expressions
+ list : ∀[ Parser [ SExp ] ⇒ Parser [ List SExp ] ]
+ list sexp = List⁺.toList <$> list⁺ (withSpaces sexp)
+
+ -- Compound S-Expression parser
+ compound : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
+ compound rec = nil <|> SExps <$> parens (map list rec)
+
+ -- S-Expression parser
+ sexp : ∀[ □ Parser [ SExp ] ⇒ Parser [ SExp ] ]
+ sexp rec = atom <|> nat <|> compound rec
+
+ -- Build the parser as a fixpoint since SExp is an inductive type
+ sexp-top : ∀[ Parser [ SExp ] ]
+ sexp-top = fix (Parser [ SExp ]) sexp
+
+ -- Top-level parser for list of S-Expressions
+ LIST : ∀[ Parser [ SExp ] ]
+ LIST = SExps <$> list sexp-top
+
+ -- Top-level S-Expression parser
+ SEXP : ∀[ Parser [ SExp ] ]
+ SEXP = withSpaces sexp-top
generated by cgit v1.2.3 (git 2.39.1) at 2025-10-30 18:14:09 +0000