diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/Hypergraph.agda | 2 | ||||
| -rw-r--r-- | Data/Hypergraph/Edge.agda | 72 | ||||
| -rw-r--r-- | Data/Opaque/List.agda | 61 |
3 files changed, 104 insertions, 31 deletions
diff --git a/Data/Hypergraph.agda b/Data/Hypergraph.agda index 770c500..7d22129 100644 --- a/Data/Hypergraph.agda +++ b/Data/Hypergraph.agda @@ -12,6 +12,8 @@ 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 HypergraphLabel HL using (Label) public + open import Data.List using (List; map) open import Data.Nat using (ℕ) open import Data.String using (String; unlines) diff --git a/Data/Hypergraph/Edge.agda b/Data/Hypergraph/Edge.agda index 5c22a04..447f008 100644 --- a/Data/Hypergraph/Edge.agda +++ b/Data/Hypergraph/Edge.agda @@ -5,23 +5,24 @@ open import Data.Hypergraph.Label using (HypergraphLabel) 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 -import Relation.Binary.PropositionalEquality as ≡ +import Data.Vec.Functional as Vec +import Data.Vec.Functional.Relation.Binary.Equality.Setoid as PW +import Data.Fin.Properties as FinProp -open import Data.Fin using (Fin) +open import Data.Fin as Fin using (Fin) open import Data.Fin.Show using () renaming (show to showFin) open import Data.Nat using (ℕ) 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) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; module ≡-Reasoning) +open import Function using (_⟶ₛ_; Func; _∘_) module HL = HypergraphLabel HL -open HL using (Label; cast; cast-is-id) -open Vec using (Vec) +open HL using (Label) +open Vec using (Vector) open Func record Edge (v : ℕ) : Set ℓ where @@ -29,7 +30,7 @@ record Edge (v : ℕ) : Set ℓ where field {arity} : ℕ label : Label arity - ports : Vec (Fin v) arity + ports : Fin arity → Fin v map : {n m : ℕ} → (Fin n → Fin m) → Edge n → Edge m map f edge = record @@ -39,11 +40,10 @@ map f edge = record where open Edge edge -open ≡ using (_≡_) -open VecCast using (_≈[_]_) - module _ {v : ℕ} where + open PW (≡.setoid (Fin v)) using (_≋_) + -- an equivalence relation on edges with v nodes record _≈_ (E E′ : Edge v) : Set ℓ where constructor mk≈ @@ -51,34 +51,49 @@ module _ {v : ℕ} where module E′ = Edge E′ field ≡arity : E.arity ≡ E′.arity - ≡label : cast ≡arity E.label ≡ E′.label - ≡ports : E.ports ≈[ ≡arity ] E′.ports + ≡label : HL.cast ≡arity E.label ≡ E′.label + ≡ports : E.ports ≋ E′.ports ∘ Fin.cast ≡arity ≈-refl : {x : Edge v} → x ≈ x - ≈-refl = record + ≈-refl {x} = record { ≡arity = ≡.refl ; ≡label = HL.≈-reflexive ≡.refl - ; ≡ports = VecCast.≈-reflexive ≡.refl + ; ≡ports = ≡.cong (Edge.ports x) ∘ ≡.sym ∘ FinProp.cast-is-id _ } ≈-sym : {x y : Edge v} → x ≈ y → y ≈ x ≈-sym x≈y = record { ≡arity = ≡.sym ≡arity ; ≡label = HL.≈-sym ≡label - ; ≡ports = VecCast.≈-sym ≡ports + ; ≡ports = ≡.sym ∘ ≡ports-sym } where open _≈_ x≈y - - ≈-trans : {i j k : Edge v} → i ≈ j → j ≈ k → i ≈ k - ≈-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 + open ≡-Reasoning + ≡ports-sym : (i : Fin E′.arity) → E.ports (Fin.cast _ i) ≡ E′.ports i + ≡ports-sym i = begin + E.ports (Fin.cast _ i) ≡⟨ ≡ports (Fin.cast _ i) ⟩ + E′.ports (Fin.cast ≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong E′.ports (FinProp.cast-involutive ≡arity _ i) ⟩ + E′.ports i ∎ + + ≈-trans : {x y z : Edge v} → x ≈ y → y ≈ z → x ≈ z + ≈-trans {x} {y} {z} x≈y y≈z = record + { ≡arity = ≡.trans x≈y.≡arity y≈z.≡arity + ; ≡label = HL.≈-trans x≈y.≡label y≈z.≡label + ; ≡ports = ≡-ports } where - module i≈j = _≈_ i≈j - module j≈k = _≈_ j≈k + module x≈y = _≈_ x≈y + module y≈z = _≈_ y≈z + open ≡-Reasoning + ≡-ports : (i : Fin x≈y.E.arity) → x≈y.E.ports i ≡ y≈z.E′.ports (Fin.cast _ i) + ≡-ports i = begin + x≈y.E.ports i ≡⟨ x≈y.≡ports i ⟩ + y≈z.E.ports (Fin.cast _ i) ≡⟨ y≈z.≡ports (Fin.cast _ i) ⟩ + y≈z.E′.ports (Fin.cast y≈z.≡arity (Fin.cast _ i)) + ≡⟨ ≡.cong y≈z.E′.ports (FinProp.cast-trans _ y≈z.≡arity i) ⟩ + y≈z.E′.ports (Fin.cast _ i) ∎ ≈-IsEquivalence : IsEquivalence _≈_ ≈-IsEquivalence = record @@ -88,16 +103,11 @@ module _ {v : ℕ} where } show : Edge v → String - show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin p - - ≈⇒≡ : {x y : Edge v} → x ≈ y → x ≡ y - ≈⇒≡ {mkEdge l p} (mk≈ ≡.refl ≡.refl ≡.refl) - rewrite cast-is-id ≡.refl l - rewrite VecCast.cast-is-id ≡.refl p = ≡.refl + show (mkEdge {a} l p) = HL.showLabel a l <+> showVec showFin (Vec.toVec p) 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) +mapₛ f .cong (mk≈ ≡a ≡l ≡p) = mk≈ ≡a ≡l (≡.cong f ∘ ≡p) diff --git a/Data/Opaque/List.agda b/Data/Opaque/List.agda new file mode 100644 index 0000000..a8e536f --- /dev/null +++ b/Data/Opaque/List.agda @@ -0,0 +1,61 @@ +{-# OPTIONS --without-K --safe #-} + +module Data.Opaque.List where + +import Data.List as L +import Function.Construct.Constant as Const + +open import Level using (Level; _⊔_) +open import Data.List.Relation.Binary.Pointwise as PW using (++⁺; map⁺) +open import Data.Product using (uncurry′) +open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_) +open import Data.Unit.Polymorphic using (⊤) +open import Function using (_⟶ₛ_; Func) +open import Relation.Binary using (Setoid) + +open Func + +private + + variable + a c ℓ : Level + A B : Set a + Aₛ Bₛ : Setoid c ℓ + + ⊤ₛ : Setoid c ℓ + ⊤ₛ = record { Carrier = ⊤ ; _≈_ = λ _ _ → ⊤ } + +opaque + + List : Set a → Set a + List = L.List + + [] : List A + [] = L.[] + + _∷_ : A → List A → List A + _∷_ = L._∷_ + + map : (A → B) → List A → List B + map = L.map + + _++_ : List A → List A → List A + _++_ = L._++_ + + Listₛ : Setoid c ℓ → Setoid c (c ⊔ ℓ) + Listₛ = PW.setoid + + []ₛ : ⊤ₛ {c} {c ⊔ ℓ} ⟶ₛ Listₛ {c} {ℓ} Aₛ + []ₛ = Const.function ⊤ₛ (Listₛ _) [] + + ∷ₛ : Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ∷ₛ .to = uncurry′ _∷_ + ∷ₛ .cong = uncurry′ PW._∷_ + + mapₛ : (Aₛ ⟶ₛ Bₛ) → Listₛ Aₛ ⟶ₛ Listₛ Bₛ + mapₛ f .to = map (to f) + mapₛ f .cong xs≈ys = map⁺ (to f) (to f) (PW.map (cong f) xs≈ys) + + ++ₛ : Listₛ Aₛ ×ₛ Listₛ Aₛ ⟶ₛ Listₛ Aₛ + ++ₛ .to = uncurry′ _++_ + ++ₛ .cong = uncurry′ ++⁺ |