Rename VariantMap to VariantGenerator in the documentation

During the actual rename in 2549a48, I
missed the documentation which is fixed by this commit. Now, there
should be no occurrences of variant map anymore.

Fixes #77

Author: ibbem

README.md

@@ -308,7 +308,7 @@ The following table shows where each of the definitions, theorems, and proofs fr
 | Definition 4.6  | Finite Indexed Set                |                                                                    |                                                                                                      | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately.                                                          |
 | Definition 4.8  | Non-empty Indexed Set             | `empty`                                                            | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md)                                         | The library definition is a predicate that ensures an indexed set to be non-empty.                                                                                 |
 | Definition 4.9  | Variant Generator                 | `VariantGenerator`                                                 | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda)                                       | This is the finite and non-empty indexed set definition mentioned above.                                                                                           |
-| Definition 4.10 | Semantic Domain                   | `VariantGenerator`                                                 | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda)                                       | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements.                                                             |
+| Definition 4.10 | Semantic Domain                   | `VariantGenerator`                                                 | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda)                           | In contrast to a variant generator, the semantic domain is the type of variant generators instead of its elements.                                                 |
 | Definition 4.11 | configuration language 𝐶          | `ℂ`                                                                | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda)                                     |                                                                                                                                                                    |
 | Definition 4.12 | variability language 𝐿            | `𝔼`                                                                | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda)                                     |                                                                                                                                                                    |
 | Definition 4.13 | ⟦.⟧                               | `𝔼-Semantics`                                                      | [src/Vatras/Framework/VariabilityLanguage.agda](src/Vatras/Framework/VariabilityLanguage.agda)                     |                                                                                                                                                                    |

src/Vatras/Framework/Proof/ForFree.lagda.md

@@ -26,11 +26,11 @@ The intuition is that `M` can express everything `L` can express which in turn i
 Thus also `M` is complete.
 
 **Proof Sketch:**
-Let V be an arbitrary variant map.
+Let V be an arbitrary variant generator.
 Since L is complete, there exists an expression l ∈ L that describes V.
 By assumption, M is as expressive as L.
 Thus, there exists an expression m ∈ M that also describes V.
-Since V was picked arbitrarily, M can encode any variant map.
+Since V was picked arbitrarily, M can encode any variant generator.
 Thus, M is complete.
 
 Dual theorem to: soundness-by-expressiveness.
@@ -78,7 +78,7 @@ soundness-by-expressiveness L-sound M-to-L m with M-to-L m
 {-|
 A language L is unsound if it is at least as expressive as another unsound language M.
 The intuition is that there are expressions in M that describe something else
-than a variant map.
+than a variant generator.
 Since L is at least as expressive as M, L can also express these other things.
 Hence, L cannot be sound as well.
 
@@ -96,8 +96,8 @@ We can conclude that any complete language is at least as expressive as any othe
 
 **Proof sketch:**
 Given an arbitrary expression eˢ of our target language Lˢ, we have to show that there exists an expression e₊ in our complete language Lᶜ that is variant-equivalent to eˢ.
-By soundness of Lˢ we can compute the variant map of eˢ.
-By completeness of Lᶜ, we can encode any variant map as an expression eᶜ ∈ Lᶜ.
+By soundness of Lˢ we can compute the variant generator of eˢ.
+By completeness of Lᶜ, we can encode any variant generator as an expression eᶜ ∈ Lᶜ.
 -}
 expressiveness-by-completeness-and-soundness : ∀ {Lᶜ Lˢ : VariabilityLanguage V}
   → Complete Lᶜ

src/Vatras/Framework/Properties/Completeness.lagda.md

@@ -20,7 +20,7 @@ open import Vatras.Data.EqIndexedSet
 ## Definitions
 
 A language is complete if for any element in its semantic domain, there exists an expression that denotes that element.
-For variability languages, this means that given a variant map `m` there must exist an expression `e` that describes all variants in `m`.
+For variability languages, this means that given a variant generator `m` there must exist an expression `e` that describes all variants in `m`.
 In particular, for every variant `v` in `m`, there exists a configuration `c` that configures `e` to `v`.
 ```agda
 Complete : VariabilityLanguage V → Set₁

src/Vatras/Framework/Properties/Soundness.lagda.md

@@ -20,7 +20,7 @@ open import Vatras.Data.EqIndexedSet
 ## Definitions
 
 A language is sound if every expression denotes an element in the semantic domain.
-For variability languages, this means that for any expression `e` there must exist a variant map `m` that is semantically equivalent.
+For variability languages, this means that for any expression `e` there must exist a variant generator `m` that is semantically equivalent.
 ```agda
 Sound : VariabilityLanguage V → Set₁
 Sound ⟪ E , _ , ⟦_⟧ ⟫ =

src/Vatras/Framework/Relation/Expression.lagda.md

@@ -78,7 +78,7 @@ L₁ , L₂ ⊢ e₁ ≤ e₂ = ⟦ e₁ ⟧₁ ⊆ ⟦ e₂ ⟧₂
 infix 5 _,_⊢_≤_
 
 {-|
-Two expressions denote equivalent variant maps.
+Two expressions denote equivalent variant generators.
 -}
 _,_⊢_≣_ :
   ∀ (L₁ L₂ : VariabilityLanguage V)

src/Vatras/Framework/Relation/Expressiveness.lagda.md

@@ -23,7 +23,7 @@ as well as a range of related relations `_≻_`, `_⋡_`, and proves relevant pr
 We also show that compilers for variability languages can be used as proofs
 of expressiveness and vice versa (because Agda uses constructive logic).
 
-We say that a language `L₁` is as expressive as another language `L₂` if for any expression `e₂` in `L₂`, there exists an expression `e₁` in `L₁` that describes the same variant map.
+We say that a language `L₁` is as expressive as another language `L₂` if for any expression `e₂` in `L₂`, there exists an expression `e₁` in `L₁` that describes the same variant generator.
 ```agda
 {-|
 Our central expressiveness relation.
@@ -138,7 +138,7 @@ We now prove that:
 ```agda
 {-|
 A translation of expressions preserves semantics if
-the translated expression denotes the same variant map as the initial expression.
+the translated expression denotes the same variant generator as the initial expression.
 -}
 SemanticsPreserving : ∀ (L M : VariabilityLanguage V) → Expression L ⇒ₚ Expression M → Set₁
 SemanticsPreserving L M t = ∀ {A} (e : Expression L A) → L , M ⊢ e ≣ t e

src/Vatras/Framework/VariantGenerator.agda

@@ -12,8 +12,8 @@ import Relation.Binary.PropositionalEquality as Eq
 open import Vatras.Data.EqIndexedSet {A = V A}
 
 {-|
-Variant maps constitute the semantic domain of variability languages.
-As a representative set, we use Fin (suc n) to ensure that variant maps
+Variant generators constitute the semantic domain of variability languages.
+As a representative set, we use Fin (suc n) to ensure that variant generators
 are finite (Fin) and non-empty (suc n) indexed sets.
 Using (suc n) here is a shortcut to ensure that the index set has at
 least one element and hence is not empty.
@@ -22,18 +22,18 @@ VariantGenerator : ℕ → Set₁
 VariantGenerator n = IndexedSet (Fin (suc n))
 
 {-|
-This function removes the first variant from a variant map.
-Given that we use natural numbers as an index set for variant maps,
-variant maps have an implicit total order.
+This function removes the first variant from a variant generator.
+Given that we use natural numbers as an index set for variant generators,
+variant generators have an implicit total order.
 Hence, we can distinguish the first element.
 -}
 remove-first : ∀ {n} → VariantGenerator (suc n) → VariantGenerator n
 remove-first set i = set (Data.Fin.suc i)
 
 {-|
-This function removes the last variant from a variant map.
-Given that we use natural numbers as an index set for variant maps,
-variant maps have an implicit total order.
+This function removes the last variant from a variant generator.
+Given that we use natural numbers as an index set for variant generators,
+variant generators have an implicit total order.
 Hence, we can distinguish the last element.
 -}
 remove-last : ∀ {n} → VariantGenerator (suc n) → VariantGenerator n

src/Vatras/Lang/FST.lagda.md

@@ -884,7 +884,7 @@ FSTL = ⟪ Impose.SPL , Conf , FSTL-Sem ⟫
 We prove that FST SPLs are an incomplete variability language, when
 assuming rose trees as variant type.
 The proof works similarly as for option calculus.
-The idea is that feature structure trees cannot encode variant maps
+The idea is that feature structure trees cannot encode variant generators
 with exactly two disjunct variants.
 
 ```agda

src/Vatras/Lang/VariantList.lagda.md

@@ -81,7 +81,7 @@ These proofs will form the basis for proving these properties for other language
 
 ### Completeness
 
-To prove completeness, we have to show that lists of variants can express any variant map.
+To prove completeness, we have to show that lists of variants can express any variant generator.
 
 ```agda
 open import Vatras.Util.Nat.AtLeast using (cappedFin)
@@ -93,7 +93,7 @@ private
     A : 𝔸
     e : VariantList A
 
--- rules for translating a variant map to a list of variants
+-- rules for translating a variant generator to a list of variants
 infix 3 _⊢_⟶_
 data _⊢_⟶_ : ∀ (n : ℕ) → VariantGenerator A n → VariantList A → Set₁ where
   -- a singleton set is translated to a singleton list
@@ -185,8 +185,8 @@ VariantList-is-Complete vs =
 ### Soundness
 
 We can use a trick to prove soundness by reusing the above definitions for completeness.
-The trick is that `⟦ e ⟧ ∘ vl-conf` denotes a variant map because it takes a `Fin (suc n)` as input and produces a variant.
-We are then left to prove that this variant map exactly denotes the expression in e which is almost true by definition.
+The trick is that `⟦ e ⟧ ∘ vl-conf` denotes a variant generator because it takes a `Fin (suc n)` as input and produces a variant.
+We are then left to prove that this variant generator exactly denotes the expression in e which is almost true by definition.
 It just requires playing with the configuration translation functions a bit, and to prove
 that `vl-conf` is the (semantic) inverse of `vl-fnoc`.
 

src/Vatras/Tutorial/C_Proofs.lagda.md

@@ -39,7 +39,7 @@ binary choice calculus `2CC` to our own language `MyLang`,
 and we have also proven this translation correct.
 By doing this, we have shown that our own language
 can express everything binary choice calculus can express
-(with respect to variant maps as a semantic domain).
+(with respect to variant generators as a semantic domain).
 We can hence conclude that our language is at least
 as expressive as binary choice calculus from having
 constructed our compiler.
@@ -108,10 +108,10 @@ A language is complete if there is an expression for
 every element in the respective semantic domain.
 For variability languages as formalized in our framework,
 this means that there must be an expression for every
-variant map (i.e., finite, non-empty set of variants).
+variant generator (i.e., finite, non-empty set of variants).
 
 Properties such as completeness, soundness, and expressiveness
-are parametric in the type of variants in the variant map.
+are parametric in the type of variants in the variant generator.
 We will reuse `V` here which was defined in the first tutorial
 to be a rose tree just as in our paper.
 (Try looking it up using your editor, and feel free to
@@ -164,7 +164,7 @@ You can read more on this process in our paper.
 A language is sound if any of its expressions
 denotes an element in the semantic domain.
 For variability languages as formalized in our framework,
-this means that there must be an variant map for every expression.
+this means that there must be an variant generator for every expression.
 
 By inspecting the `Framework.Proof.Transitive` module closely,
 you will see that proofs for soundness are exactly dual to the proofs