aboutsummaryrefslogtreecommitdiff
path: root/Data
diff options
context:
space:
mode:
Diffstat (limited to 'Data')
-rw-r--r--Data/Circuit.agda16
-rw-r--r--Data/Hypergraph.agda30
-rw-r--r--Data/Hypergraph/Edge.agda15
-rw-r--r--Data/Hypergraph/Label.agda14
-rw-r--r--Data/System.agda13
5 files changed, 48 insertions, 40 deletions
diff --git a/Data/Circuit.agda b/Data/Circuit.agda
index 46c4e18..77d6b72 100644
--- a/Data/Circuit.agda
+++ b/Data/Circuit.agda
@@ -2,20 +2,22 @@
open import Level using (Level)
-module Data.Circuit {c ℓ : Level} where
+module Data.Circuit {ℓ : Level} where
open import Data.Circuit.Gate using (Gates)
import Data.List as List
-import Data.Hypergraph {c} {ℓ} Gates as Hypergraph
+import Data.Hypergraph {ℓ} Gates as Hypergraph
open import Data.Fin using (Fin)
open import Data.Nat using (ℕ)
-open import Function using (Func; _⟶ₛ_)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (map⁺)
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties using (map⁺)
+open import Function using (Func; _⟶ₛ_; _∘_)
+open import Relation.Binary using (Setoid)
open Func
-open Hypergraph using (List∘Edgeₛ)
+
+open Hypergraph using (Multiset∘Edgeₛ)
open Hypergraph
using (_≈_ ; mk≈ ; module Edge)
renaming
@@ -33,6 +35,8 @@ map f (mkCircuit edges) = mkCircuit (List.map (Edge.map f) edges)
discrete : (n : ℕ) → Circuit n
discrete n = mkCircuit []
+open Edge using (Edgeₛ)
+
mapₛ : {n m : ℕ} → (Fin n → Fin m) → Circuitₛ n ⟶ₛ Circuitₛ m
mapₛ f .to = map f
-mapₛ f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edge.map f) x≈y)
+mapₛ {n} {m} f .cong (mk≈ x≈y) = mk≈ (map⁺ (Edgeₛ n) (Edgeₛ m) (cong (Edge.mapₛ f)) x≈y)
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda
index ff92d0e..770c500 100644
--- a/Data/Hypergraph.agda
+++ b/Data/Hypergraph.agda
@@ -1,18 +1,18 @@
{-# OPTIONS --without-K --safe #-}
-open import Level using (Level; 0ℓ)
open import Data.Hypergraph.Label using (HypergraphLabel)
+open import Level using (Level; 0ℓ)
-module Data.Hypergraph {c ℓ : Level} (HL : HypergraphLabel) where
+module Data.Hypergraph {ℓ : Level} (HL : HypergraphLabel) where
import Data.List.Relation.Binary.Pointwise as PW
import Function.Reasoning as →-Reasoning
import Relation.Binary.PropositionalEquality as ≡
-import Data.Hypergraph.Edge HL as Hyperedge
+import Data.Hypergraph.Edge {ℓ} HL as Hyperedge
import Data.List.Relation.Binary.Permutation.Propositional as List-↭
+import Data.List.Relation.Binary.Permutation.Setoid as ↭
open import Data.List using (List; map)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭-refl; ↭-sym; ↭-trans)
open import Data.Nat using (ℕ)
open import Data.String using (String; unlines)
open import Function using (_∘_; _⟶ₛ_; Func)
@@ -22,13 +22,15 @@ module Edge = Hyperedge
open Edge using (Edge; Edgeₛ)
-- A hypergraph is a list of edges
-record Hypergraph (v : ℕ) : Set c where
+record Hypergraph (v : ℕ) : Set ℓ where
constructor mkHypergraph
field
edges : List (Edge v)
module _ {v : ℕ} where
+ open ↭ (Edgeₛ v) using (_↭_; ↭-refl; ↭-sym; ↭-trans)
+
show : Hypergraph v → String
show (mkHypergraph e) = unlines (map Edge.show e)
@@ -55,7 +57,7 @@ module _ {v : ℕ} where
≈-trans (mk≈ ≡n₁) (mk≈ ≡n₂) = mk≈ (↭-trans ≡n₁ ≡n₂)
-- The setoid of labeled hypergraphs with v nodes
-Hypergraphₛ : ℕ → Setoid c ℓ
+Hypergraphₛ : ℕ → Setoid ℓ ℓ
Hypergraphₛ v = record
{ Carrier = Hypergraph v
; _≈_ = _≈_
@@ -68,15 +70,11 @@ Hypergraphₛ v = record
open Func
-List∘Edgeₛ : (n : ℕ) → Setoid 0ℓ 0ℓ
-List∘Edgeₛ = PW.setoid ∘ Edgeₛ
+open ↭ using (↭-setoid)
+
+Multiset∘Edgeₛ : (n : ℕ) → Setoid ℓ ℓ
+Multiset∘Edgeₛ = ↭-setoid ∘ Edgeₛ
-mkHypergraphₛ : {n : ℕ} → List∘Edgeₛ n ⟶ₛ Hypergraphₛ n
+mkHypergraphₛ : {n : ℕ} → Multiset∘Edgeₛ n ⟶ₛ Hypergraphₛ n
mkHypergraphₛ .to = mkHypergraph
-mkHypergraphₛ {n} .cong ≋-edges = ≋-edges
- |> PW.map Edge.≈⇒≡
- |> PW.Pointwise-≡⇒≡
- |> ≡.cong mkHypergraph
- |> Setoid.reflexive (Hypergraphₛ n)
- where
- open →-Reasoning
+mkHypergraphₛ {n} .cong = mk≈
diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda
index 1e24559..5c22a04 100644
--- a/Data/Hypergraph/Edge.agda
+++ b/Data/Hypergraph/Edge.agda
@@ -2,7 +2,8 @@
open import Data.Hypergraph.Label using (HypergraphLabel)
-module Data.Hypergraph.Edge (HL : HypergraphLabel) where
+open import Level using (Level; 0ℓ)
+module Data.Hypergraph.Edge {ℓ : Level} (HL : HypergraphLabel) where
import Data.Vec as Vec
import Data.Vec.Relation.Binary.Equality.Cast as VecCast
@@ -15,13 +16,15 @@ open import Data.String using (String; _<+>_)
open import Data.Vec.Show using () renaming (show to showVec)
open import Level using (0ℓ)
open import Relation.Binary using (Setoid; IsEquivalence)
+open import Function using (_⟶ₛ_; Func)
module HL = HypergraphLabel HL
open HL using (Label; cast; cast-is-id)
open Vec using (Vec)
+open Func
-record Edge (v : ℕ) : Set where
+record Edge (v : ℕ) : Set ℓ where
constructor mkEdge
field
{arity} : ℕ
@@ -42,7 +45,7 @@ open VecCast using (_≈[_]_)
module _ {v : ℕ} where
-- an equivalence relation on edges with v nodes
- record _≈_ (E E′ : Edge v) : Set where
+ record _≈_ (E E′ : Edge v) : Set ℓ where
constructor mk≈
module E = Edge E
module E′ = Edge E′
@@ -92,5 +95,9 @@ module _ {v : ℕ} where
rewrite cast-is-id ≡.refl l
rewrite VecCast.cast-is-id ≡.refl p = ≡.refl
-Edgeₛ : (v : ℕ) → Setoid 0ℓ 0ℓ
+Edgeₛ : (v : ℕ) → Setoid ℓ ℓ
Edgeₛ v = record { isEquivalence = ≈-IsEquivalence {v} }
+
+mapₛ : {n m : ℕ} → (Fin n → Fin m) → Edgeₛ n ⟶ₛ Edgeₛ m
+mapₛ f .to = map f
+mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (VecCast.≈-cong′ (Vec.map f) ≡p)
diff --git a/Data/Hypergraph/Label.agda b/Data/Hypergraph/Label.agda
index c23d33a..ca95002 100644
--- a/Data/Hypergraph/Label.agda
+++ b/Data/Hypergraph/Label.agda
@@ -4,22 +4,22 @@ 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 Level using (Level; 0ℓ)
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
+record HypergraphLabel : Set₁ where
field
- Label : ℕ → Set ℓ
+ Label : ℕ → Set
showLabel : (n : ℕ) → Label n → String
isCastable : IsCastable Label
- _[_≤_] : (n : ℕ) → Rel (Label n) ℓ
+ _[_≤_] : (n : ℕ) → Rel (Label n) 0ℓ
isDecTotalOrder : (n : ℕ) → IsDecTotalOrder _≡_ (n [_≤_])
- decTotalOrder : (n : ℕ) → DecTotalOrder ℓ ℓ ℓ
+ decTotalOrder : (n : ℕ) → DecTotalOrder 0ℓ 0ℓ 0ℓ
decTotalOrder n = record
{ Carrier = Label n
; _≈_ = _≡_
@@ -27,10 +27,10 @@ record HypergraphLabel {ℓ : Level} : Set (suc ℓ) where
; isDecTotalOrder = isDecTotalOrder n
}
- _[_<_] : (n : ℕ) → Rel (Label n) ℓ
+ _[_<_] : (n : ℕ) → Rel (Label n) 0ℓ
_[_<_] n = _<_ (decTotalOrder n)
- strictTotalOrder : (n : ℕ) → StrictTotalOrder ℓ ℓ ℓ
+ strictTotalOrder : (n : ℕ) → StrictTotalOrder 0ℓ 0ℓ 0ℓ
strictTotalOrder n = <-strictTotalOrder (decTotalOrder n)
open IsCastable isCastable public
diff --git a/Data/System.agda b/Data/System.agda
index 0361369..cecdfcd 100644
--- a/Data/System.agda
+++ b/Data/System.agda
@@ -1,7 +1,6 @@
{-# OPTIONS --without-K --safe #-}
-open import Level using (Level)
-
+open import Level using (Level; 0ℓ; suc)
module Data.System {ℓ : Level} where
import Function.Construct.Identity as Id
@@ -11,7 +10,7 @@ open import Data.Circuit.Value using (Value)
open import Data.Nat.Base using (ℕ)
open import Data.Setoid using (_⇒ₛ_; ∣_∣)
open import Data.System.Values Value using (Values; _≋_; module ≋)
-open import Level using (Level; _⊔_; 0ℓ; suc)
+open import Level using (Level; 0ℓ; suc)
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
open import Relation.Binary using (Reflexive; Transitive; Preorder; _⇒_; Setoid)
open import Function.Base using (_∘_)
@@ -20,10 +19,10 @@ open import Function.Construct.Setoid using (_∙_)
open Func
-record System (n : ℕ) : Set (suc ℓ) where
+record System (n : ℕ) : Set₁ where
field
- S : Setoid ℓ ℓ
+ S : Setoid 0ℓ 0ℓ
fₛ : ∣ Values n ⇒ₛ S ⇒ₛ S ∣
fₒ : ∣ S ⇒ₛ Values n ∣
@@ -66,7 +65,7 @@ module _ {n : ℕ} where
≗-fₛ (≤-trans {x} {y} {z} a b) i s = System.trans z (cong (⇒S b) (≗-fₛ a i s)) (≗-fₛ b i (⇒S a ⟨$⟩ s))
≗-fₒ (≤-trans a b) s = ≋.trans (≗-fₒ a s) (≗-fₒ b (⇒S a ⟨$⟩ s))
- System-Preorder : Preorder (suc ℓ) (suc ℓ) ℓ
+ System-Preorder : Preorder (suc 0ℓ) (suc 0ℓ) ℓ
System-Preorder = record
{ Carrier = System n
; _≈_ = _≡_
@@ -82,5 +81,5 @@ module _ (n : ℕ) where
open PreorderProperties (System-Preorder {n}) using (InducedEquivalence)
- Systemₛ : Setoid (suc ℓ) ℓ
+ Systemₛ : Setoid (suc 0ℓ) ℓ
Systemₛ = InducedEquivalence
generated by cgit v1.2.3 (git 2.39.1) at 2025-11-29 08:03:01 +0000