Merge pull request #10 from pmbittner/small-improvements

Small improvements

src/Framework/Annotation/Name.agda

@@ -11,11 +11,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_)
 Name : Set
 Name = String
 
-_≟_ : Decidable (_≡_)
-_≟_ = Data.String.Properties._≟_
-
-_==_ : Name → Name → Bool
-_==_ = Data.String.Properties._==_
+open Data.String.Properties using (_≟_; _==_) public
 
 -- Some common names for names.
 

src/Framework/Definitions.lagda.md

@@ -56,7 +56,7 @@ Artifactˡ L = ∀ {i : Size} {A : 𝔸} → A → List (L i A) → L (↑ i) A
 
 Variability languages denote sets of variants.
 Interestingly, variants can be modelled as a variability language in which nothing can be configured.
-Every expressions describes a singleton set of variants.
+Every expression describes a singleton set of variants.
 ```agda
 -- 𝟙-Lang
 data Variant : 𝕃 where
@@ -191,8 +191,7 @@ suc-variant-size : ∀ {i} {A} → Variant i A → Variant i A
 suc-variant-size v = v
 
 forget-variant-size : ∀ {i} {A} → Variant i A → Variant ∞ A
-forget-variant-size (Artifactᵥ a []) = Artifactᵥ a []
-forget-variant-size (Artifactᵥ a (e ∷ es)) = Artifactᵥ a (map forget-variant-size (e ∷ es))
+forget-variant-size (Artifactᵥ a es) = Artifactᵥ a (map forget-variant-size es)
 
 forget-size-cong : ∀ {i} {A B : Set} {x : Variant ∞ A} {y : Variant i A}
   → (f : ∀ {j} → Variant j A → B)
@@ -203,8 +202,7 @@ forget-size-cong _ refl = refl
 sequence-forget-size : ∀ {A} {i} {a : A}
   → (xs : List (Variant i A))
   → Artifactᵥ a (map forget-variant-size xs) ≡ forget-variant-size (Artifactᵥ a xs)
-sequence-forget-size [] = refl
-sequence-forget-size (_ ∷ _) = refl
+sequence-forget-size _ = refl
 
 {-
 Creates an Artifact from a list of expressions of a certain size.

src/Framework/Properties/Completeness.lagda.md

@@ -29,7 +29,7 @@ private module ISet A = Data.IndexedSet (VariantSetoid ∞ A)
 
 ## Definitions
 
-Completeness is given iff for any set of variants `vs` (modelled as a list for convenience in Agda), there exists an expression `e` in the language `L` that describes all variants in `v`.
+Completeness is given iff for any set of variants `vs` (modeled as a list for convenience in Agda), there exists an expression `e` in the language `L` that describes all variants in `vs`.
 In particular, for every variant `v` in `vs`, there exists a configuration `c` that configures `e` to `v`.
 ```agda
 Complete : VariabilityLanguage → Set₁

src/Framework/Relation/Expressiveness.lagda.md

@@ -26,7 +26,7 @@ L₁ ≽ L₂ =
   ∀ {A : 𝔸} (e₂ : Expression A L₂) →
       (Σ[ e₁ ∈ Expression A L₁ ]
         (e₂ ≚ e₁))
-  -- It would be nice if we could rephrase expressiveness to (semantics L₂) ⊆ (semantics L₁) but I we have to generalize our multisets somehow first to allow keys in the source set.
+  -- It would be nice if we could rephrase expressiveness to (semantics L₂) ⊆ (semantics L₁) but first we have to generalize our multisets somehow to allow keys in the source set.
 
 _⋡_ : VariabilityLanguage → VariabilityLanguage → Set₁ -- \nsucceq
 L₁ ⋡ L₂ = ¬ (L₁ ≽ L₂)

src/Framework/Relation/Syntactic.lagda.md

@@ -1,7 +1,7 @@
 ```agda
 {-# OPTIONS --sized-types #-}
 
-module Relations.Syntactic where
+module Framework.Relation.Syntactic where
 ```
 
 # Syntactic Relations of Variability Languages

src/Framework/V2/TODO.lagda.md

@@ -34,7 +34,7 @@ Prove for all of the following languages whether they are complete, sound, and h
 
 ## Issues
 
-Nest Issue No: 12
+Next Issue No: 12
 
 ### [2] Embed NestedChoice
 

src/Framework/V2/Translation/Construct/2Choice-to-NChoice-VL.agda

@@ -22,7 +22,7 @@ open import Framework.V2.Constructs.Choices as Chc
 open Chc.Choice₂ using (_⟨_,_⟩) renaming (Config to Config₂; map to map₂)
 open Chc.Choiceₙ using () renaming (map to mapₙ)
 
-module Translate {F : 𝔽} {V : 𝕍} {A : 𝔸}
+module Translate {V : 𝕍} {F : 𝔽} {A : 𝔸}
   (Γ₁ : VariabilityLanguage V F Bool)
   (Γ₂ : VariabilityLanguage V F ℕ)
   (t : LanguageCompiler Γ₁ Γ₂)

src/Framework/V2/Translation/Construct/2Choice-to-NChoice.agda

@@ -26,7 +26,9 @@ to prove preservation of the conversion from binary to n-ary choices.
 
 The requirement for translating binary to n-ary configurations is
 that there exist two natural numbers that we can associate with the boolean values true and false.
-To simplify things, we fix these two numbers to be 0 for true, and 1 for false.
+To simplify things, we fix these two numbers to be 0 for true, and 1 for false. These values are chosen such that
+`D < l ,  r       >` lines up with
+`D < l :: r :: [] >`
 -}
 record ConfContract (f : Q) (conf : Config₂ Q → Configₙ Q) : Set ℓ₁ where
   field

src/Translation/LanguageMap.lagda.md

@@ -30,9 +30,9 @@ open import Lang.BCC
 ### Properties and Relations
 
 ```agda
+open import Framework.Relation.Expressiveness
 open import Framework.Properties.Completeness
-open import Framework.Properties.Conclude.Completeness
-open import Relations.Semantic
+open import Framework.Proof.Completeness
 ```
 
 ### Translations