EqIndexedSet

src/Construct/Artifact.agda

@@ -7,7 +7,6 @@ open import Level using (_⊔_)
 open import Function using (id; flip; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage
 open import Framework.Construct
@@ -23,9 +22,9 @@ Syntax E A = Artifact A (E A)
 Construct : PlainConstruct
 Construct = Plain-⟪ Syntax , (λ Γ e c → map-children (flip (Semantics Γ) c) e) ⟫
 
+open import Data.EqIndexedSet as ISet
 map-children-preserves : ∀ {V : 𝕍} {Γ₁ Γ₂ : VariabilityLanguage V} {A}
-  → let open IVSet V A using (_≅_; _≅[_][_]_) in
-  ∀ (mkArtifact : Syntax ∈ₛ V)
+  → (mkArtifact : Syntax ∈ₛ V)
   → (t : LanguageCompiler Γ₁ Γ₂)
   → (a : Syntax (Expression Γ₁) A)
   → PlainConstruct-Semantics Construct mkArtifact Γ₁ a
@@ -37,9 +36,10 @@ map-children-preserves {V} {Γ₁} {Γ₂} {A} mkArtifact t (a -< cs >-) =
     ≅[]⟨ t-⊆ , t-⊇ ⟩
       (λ c → cons mkArtifact (a -< map (λ e → ⟦ e ⟧₂ c) (map (compile t) cs) >-))
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where
+      -- module I = IVSet V A
+          -- open I using (_≅[_][_]_; _⊆[_]_)
+          open ISet.≅[]-Reasoning
           open Eq.≡-Reasoning
 
           ⟦_⟧₁ = Semantics Γ₁

src/Construct/Choices.agda

@@ -9,6 +9,8 @@ open import Function using (_∘_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 
+open import Data.EqIndexedSet as ISet
+
 open import Util.AuxProofs using (if-cong)
 
 module Choice-Fix where
@@ -160,7 +162,6 @@ module Choiceₙ where
   show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-list⁺ show-a es))) <+> "⟩"
 
 -- Show how choices can be used as constructors in variability languages.
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage as VL hiding (Config; Semantics)
 open import Framework.Relation.Function using (to-is-Embedding)
@@ -184,8 +185,8 @@ module VLChoice₂ where
   Construct : ∀ (V : 𝕍) (F : 𝔽) → VariabilityConstruct V
   Construct V F = Variational-⟪ Syntax F , Config F , Semantics V F ⟫
 
-  map-compile-preserves : ∀ {F V A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+  map-compile-preserves : ∀ {F V A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible (Construct V F) Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (chc : Syntax F (Expression Γ₁) A)
@@ -210,9 +211,7 @@ module VLChoice₂ where
     ≅[]⟨⟩
       Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc)
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where open ISet.≅[]-Reasoning
 
           ⟦_⟧₁ = VL.Semantics Γ₁
           ⟦_⟧₂ = VL.Semantics Γ₂
@@ -271,8 +270,8 @@ module VLChoiceₙ where
   -- This proof is oblivious of at least
   --   - the implementation of map, we only need the preservation theorem
   --   - the Standard-Semantics, we only need the preservation theorem of t, and that the config-compiler is stable.
-  map-compile-preserves : ∀ {F V A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+  map-compile-preserves : ∀ {F V A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible (Construct V F) Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (chc : Syntax F (Expression Γ₁) A)
@@ -297,9 +296,7 @@ module VLChoiceₙ where
     ≅[]⟨⟩
       Semantics V F Γ₂ (extract ∘ fnoc t) (map (compile t) chc)
     ≅[]-∎
-    where module I = IVSet V A
-          open I using (_≅[_][_]_; _⊆[_]_)
-          open I.≅[]-Reasoning
+    where open ISet.≅[]-Reasoning
 
           ⟦_⟧₁ = VL.Semantics Γ₁
           ⟦_⟧₂ = VL.Semantics Γ₂

src/Data/EqIndexedSet.agda

@@ -0,0 +1,4 @@
+module Data.EqIndexedSet {A : Set} where
+
+import Relation.Binary.PropositionalEquality as Eq
+open import Data.IndexedSet (Eq.setoid A) as ISet public

src/Framework/Compiler.agda

@@ -1,6 +1,5 @@
 module Framework.Compiler where
 
-open import Framework.Variant
 open import Framework.Definitions
 open import Framework.VariabilityLanguage
 open import Framework.Construct
@@ -10,6 +9,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≗_)
 open import Data.Product using (_×_)
 open import Function using (id; _∘_)
 
+open import Data.EqIndexedSet using (_≅_; _≅[_][_]_; ≅[]-trans)
+
 {-|
 A translated configuration is extensionally equal.
 Fixme: Give me a proper name not this ugly one.
@@ -24,8 +25,8 @@ record LanguageCompiler {V} (Γ₁ Γ₂ : VariabilityLanguage V) : Set₁ where
   field
     compile         : ∀ {A} → L₁ A → L₂ A
     config-compiler : Config Γ₁ ⇔ Config Γ₂
-    preserves : ∀ {A} → let open IVSet V A using (_≅[_][_]_) in
-                ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂
+    preserves : ∀ {A} (e : L₁ A)
+      → ⟦ e ⟧₁ ≅[ to config-compiler ][ from config-compiler ] ⟦ compile e ⟧₂
                 -- TODO: It might nice to have syntax
                 --   ≅[ config-compiler ]
                 -- to abbreviate
@@ -46,8 +47,7 @@ record ConstructCompiler {V} (VC₁ VC₂ : VariabilityConstruct V) (Γ : Variab
 
     stable : to-is-Embedding config-compiler
     preserves : ∀ {A} (c : C₁ (Expression Γ) A)
-      → let open IVSet V A using (_≅_) in
-        Kem₁ Γ extract c ≅ Kem₂ Γ (to config-compiler ∘ extract) (compile c)
+      → Kem₁ Γ extract c ≅ Kem₂ Γ (to config-compiler ∘ extract) (compile c)
 
 {-|
 Compiles languages below constructs.
@@ -64,8 +64,8 @@ record ConstructFunctor {V} (VC : VariabilityConstruct V) : Set₁ where
     -- Note: There also should be an extract₂ but it must be
     -- equivalent to extract₁ ∘ fnoc t.
     -- extract₂ : Config Γ₂ → construct-config
-    preserves : ∀ {A} → let open IVSet V A using (_≅[_][_]_) in
-      ∀ (Γ₁ Γ₂ : VariabilityLanguage V)
+    preserves : ∀ {A}
+      → (Γ₁ Γ₂ : VariabilityLanguage V)
       → (extract : Compatible VC Γ₁)
       → (t : LanguageCompiler Γ₁ Γ₂)
       → (c : VSyntax VC (Expression Γ₁) A)
@@ -128,8 +128,6 @@ _⊕ˡ_ {V} {Γ₁} {Γ₂} {Γ₃} L₁→L₂ L₂→L₃ = record
         fnoc' = fnoc L₁→L₂ ∘ fnoc L₂→L₃
 
         module _ {A : 𝔸} where
-          open IVSet V A using (_≅[_][_]_; ≅[]-trans)
-
           -- this pattern is very similar of ⊆[]-trans
           p : ∀ (e : L₁ A) → ⟦ e ⟧₁ ≅[ conf' ][ fnoc' ] ⟦ compile L₂→L₃ (compile L₁→L₂ e) ⟧₃
           p e = ≅[]-trans (preserves L₁→L₂ e) (preserves L₂→L₃ (compile L₁→L₂ e))

src/Framework/Proof/Transitive.lagda.md

@@ -9,7 +9,7 @@ open import Framework.VariabilityLanguage using (VariabilityLanguage)
 open import Framework.Properties.Completeness V
 open import Framework.Properties.Soundness V
 open import Framework.Relation.Expressiveness V
-open import Framework.Variant V
+open import Data.EqIndexedSet
 ```
 
 ## Conclusions
@@ -34,8 +34,6 @@ completeness-by-expressiveness : ∀ {L₁ L₂ : VariabilityLanguage V}
 completeness-by-expressiveness encode-in-L₂ L₂-to-L₁ {A} vs with encode-in-L₂ vs
 ... | e₂ , m≅e₂ with L₂-to-L₁ e₂
 ...   | e₁ , e₂≅e₁ = e₁ , ≅-trans m≅e₂ e₂≅e₁
-  where
-    open IVSet A using (≅-sym; ≅-trans)
 ```
 
 If a language `L₁` is sound and at least as expressive as another language `L₂`, then also `L₂` is sound.
@@ -50,8 +48,6 @@ soundness-by-expressiveness : ∀ {L₁ L₂ : VariabilityLanguage V}
 soundness-by-expressiveness L₁-sound L₂-to-L₁ {A} e₂ with L₂-to-L₁ e₂
 ... | e₁ , e₂≅e₁ with L₁-sound e₁
 ...   | n , m , m≅e₁ = n , m , ≅-trans m≅e₁ (≅-sym e₂≅e₁)
-  where
-    open IVSet A using (≅-trans; ≅-sym)
 ```
 
 Conversely, we can conclude that any complete language is at least as expressive as any other variability language.
@@ -70,8 +66,6 @@ expressiveness-by-completeness-and-soundness : ∀ {Lᶜ Lˢ : VariabilityLangua
 expressiveness-by-completeness-and-soundness comp sound {A} eˢ with sound eˢ
 ... | p , m , m≅⟦eˢ⟧ with comp m
 ...   | eᶜ , m≅⟦eᶜ⟧ = eᶜ , ≅-trans (≅-sym m≅⟦eˢ⟧) m≅⟦eᶜ⟧
-  where
-    open IVSet A using (≅-sym; ≅-trans)
 ```
 
 If a language `L₊` is complete and another language `L₋` is incomplete then `L₋` less expressive than `L₊`.

src/Framework/Properties/Completeness.lagda.md

@@ -13,7 +13,8 @@ module Framework.Properties.Completeness (V : 𝕍) where
 open import Data.Product using (Σ-syntax)
 open import Relation.Nullary.Negation using (¬_)
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
+open import Framework.VariantMap V
+open import Data.EqIndexedSet
 ```
 
 ## Definitions
@@ -28,8 +29,7 @@ via Fin (suc n) here for convenience.
 -}
 Complete : VariabilityLanguage V → Set₁
 Complete ⟪ E , _ , ⟦_⟧ ⟫ =
-  ∀ {A} → let open IVSet A using (_≅_) in
-  ∀ {n} (m : VMap A n)
+  ∀ {A} {n} (m : VMap A n)
     ----------------------
   → Σ[ e ∈ E A ] m ≅ ⟦ e ⟧
 ```

src/Framework/Properties/Finity.agda

@@ -11,7 +11,7 @@ open import Framework.VariabilityLanguage
 open import Framework.Relation.Index V using (_∋_⊢_≣ⁱ_; ≣ⁱ-IsEquivalence; ≣ⁱ-congruent; ≣ⁱ-setoid)
 open import Framework.Properties.Soundness V
 open import Framework.Relation.Expression V
-open import Framework.Variant V
+open import Data.EqIndexedSet
 open import Util.Enumerable
 
 HasEnumerableNonEmptySemantics : VariabilityLanguage V → Set₁
@@ -35,4 +35,3 @@ soundness-from-enumerability {L} L-has-finite-semantics {A} e =
       where ⟦_⟧ = Semantics L
             fin = L-has-finite-semantics e
             enumerate-configuration = enumerate fin
-            open IVSet A using (IndexedSet; _≅_; ≅-trans; ≅-sym; re-index)

src/Framework/Properties/Soundness.lagda.md

@@ -13,16 +13,16 @@ module Framework.Properties.Soundness (V : 𝕍) where
 open import Data.Product using (∃-syntax; Σ-syntax)
 open import Relation.Nullary.Negation  using (¬_)
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
+open import Framework.VariantMap V
+open import Data.EqIndexedSet
 ```
 
 ## Definitions
 
 ```agda
 Sound : VariabilityLanguage V → Set₁
 Sound ⟪ E , _ , ⟦_⟧ ⟫ =
-  ∀ {A} → let open IVSet A using (_≅_) in
-  ∀ (e : E A)
+  ∀ {A} (e : E A)
     --------------------------------
   → ∃[ n ] Σ[ m ∈ VMap A n ] m ≅ ⟦ e ⟧
 

src/Framework/Relation/Expression.lagda.md

@@ -9,9 +9,8 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Function using (_∘_; Injective)
 
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
 
-open IVSet A using
+open import Data.EqIndexedSet using
   ( _⊆_; _≅_; _≐_
   ; ≐→≅
   ; ⊆-refl; ⊆-antisym; ⊆-trans

src/Framework/Relation/Expressiveness.lagda.md

@@ -9,7 +9,6 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
 open import Function using (_∘_; Injective)
 
 open import Framework.VariabilityLanguage
-open import Framework.Variant V
 open import Framework.Relation.Expression V
 open import Framework.Relation.Function using (_⇒ₚ_)
 ```

src/Framework/Variant.agda → src/Framework/VariantMap.agda

@@ -1,5 +1,5 @@
 open import Framework.Definitions using (𝕍; 𝔸)
-module Framework.Variant (V : 𝕍) (A : 𝔸) where
+module Framework.VariantMap (V : 𝕍) (A : 𝔸) where
 
 open import Data.Fin using (Fin)
 open import Data.List using (List)
@@ -9,23 +9,15 @@ open import Level using (0ℓ)
 open import Relation.Binary using (Setoid)
 import Relation.Binary.PropositionalEquality as Eq
 
-VariantSetoid : Setoid 0ℓ 0ℓ
-VariantSetoid = Eq.setoid (V A)
-
-import Data.IndexedSet
-module IVSet = Data.IndexedSet VariantSetoid
-
-VMapWithIndex : Set → Set
-VMapWithIndex I = IndexedSet I
-  where open IVSet using (IndexedSet)
+open import Data.EqIndexedSet {V A}
 
 {-|
 Variant maps constitute the semantic domain of variability languages.
 While we defined variant maps to be indexed sets with an arbitrary finite and non-empty index set, we directly reflect these properties
 via Fin (suc n) here for convenience.
 -}
 VMap : ℕ → Set
-VMap n = VMapWithIndex (Fin (suc n))
+VMap n = IndexedSet (Fin (suc n))
 
 -- Utility functions for manipulating variant maps.
 remove-first : ∀ {n} → VMap (suc n) → VMap n

src/Framework/Variants.agda

@@ -13,6 +13,8 @@ open import Framework.Definitions using (𝕍; 𝔸)
 open import Framework.VariabilityLanguage
 open import Construct.Artifact as At using (_-<_>-; map-children; map-children-preserves) renaming (Syntax to Artifact; Construct to ArtifactC)
 
+open import Data.EqIndexedSet
+
 data GrulerVariant : 𝕍 where
   asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
@@ -62,8 +64,7 @@ VariantEncoder V Γ = LanguageCompiler (Variant-is-VL V) Γ
 
 
 module _ (V : 𝕍) (A : 𝔸) {Γ : VariabilityLanguage V} (encoder : VariantEncoder V Γ) where
-  open import Framework.Variant V A
-  open import Data.IndexedSet VariantSetoid
+  open import Data.EqIndexedSet
 
   private
     ⟦_⟧ = Semantics Γ
@@ -119,9 +120,6 @@ rose-encoder Γ has c = record
         → Artifact (Rose ∞) A
       ⟦_⟧ₚ = pcong ArtifactC Γ
 
-      open import Framework.Variant (Rose ∞) A using (VariantSetoid)
-      open import Data.IndexedSet VariantSetoid
-
       h : ∀ (v : Rose ∞ A) (j : Config Γ) → ⟦ t v ⟧ j ≡ v
       h (rose (a -< cs >-)) j =
         begin

src/Lang/CCC.lagda.md

@@ -19,14 +19,15 @@ module Lang.CCC (Dimension : 𝔽) where
 ## Imports
 ```agda
 -- -- Imports from Standard Library
+open import Data.EqIndexedSet
 open import Data.List
   using (List; []; _∷_; foldl; map)
 open import Data.List.NonEmpty
   using (List⁺; _∷_; toList)
   renaming (map to map⁺)
 open import Data.Product
   using (_,_; proj₁; proj₂; ∃-syntax; Σ-syntax)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
 
 open import Function using (id)
 open import Size using (Size; ↑_; ∞)
@@ -87,7 +88,6 @@ module Sem (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where
 Some transformation rules
 ```agda
 module Properties (V : 𝕍) (mkArtifact : Artifact ∈ₛ V) where
-  open import Framework.Variant V
   open import Framework.Relation.Expression V
   open Sem V mkArtifact
 
@@ -187,8 +187,8 @@ Maybe its smarter to do this for ADDs and then to conclude by transitivity of tr
   --     map (flip ⟦_⟧-i c) (map describe-variant (e ∷ es))
   --   ∎)
 
-  sizeof : ∀ {i A} → CCC i A → Size
-  sizeof {i} _ = i
+  -- sizeof : ∀ {i A} → CCC i A → Size
+  -- sizeof {i} _ = i
 ```