Merge pull request #81 from VariantSync/develop

Release 2.0

Author: pmbittner

.gitignore

@@ -5,6 +5,9 @@
 *.#*
 .dir-locals.el
 
+# emacs' agda mode
+src/agda2-mode*
+
 # build
 src/cc
 src/Main

README.md

@@ -27,6 +27,110 @@ This library formalizes all results in our paper:
 Additionally, our library comes with a small **demo**, and **tutorials** for getting to know the library and for formalizing your own variability languages (see "Tutorials" section below).
 When run in a terminal, our demo will show a translation roundtrip, showcasing the circle of compilers developed for identifying the map of variability languages (Section 5).
 
+## Overview: What is Static Variability and What is Vatras?
+
+Vatras is a library to study and compare meta-languages for specifying variability in source code and data.
+Some software systems are configurable _before_ they are compiled, i.e., statically.
+A common way example for implementing static variability is by conditional compilation, as for example possible with the C preprocessor.
+For instance, the following [code snippet from the Linux kernel](https://github.com/torvalds/linux/blob/e271ed52b344ac02d4581286961d0c40acc54c03/include/linux/console.h#L479-L486)
+
+```C
+#ifdef CONFIG_DEBUG_LOCK_ALLOC
+extern bool console_srcu_read_lock_is_held(void);
+#else
+static inline bool console_srcu_read_lock_is_held(void)
+{
+  return 1;
+}
+#endif
+```
+
+replaces the function `console_srcu_read_lock_is_held` with a default implementation in case a particular feature should be debugged.
+Essentially, the code snippet above does not denote a single `C` program but two `C` programs, each using one of two alternatives for the function `console_srcu_read_lock_is_held`.
+
+To model and analyze static variability, researchers have formalized various formal languages, including formalisms for conditional compilation.
+For example, the _choice calculus_ is a small language to formalize conditional compilation in terms of a singly syntactic term, referred to as a _choice_.
+A choice `F ⟨ l , r ⟩` specifies two alternatives `l` and `r` for a feature or configuration option `F`.
+Encoding the example above in choice calculus yields
+
+```
+CONFIG_DEBUG_LOCK_ALLOC ⟨ 
+  extern bool console_srcu_read_lock_is_held(void);
+,
+  static inline bool console_srcu_read_lock_is_held(void)
+  {
+    return 1;
+  }
+⟩
+```
+
+Apart from source code, static configuration processes emerge in many other areas, including our daily lives. 
+For instance, some restaurants offer your to configure your meal.
+Sticking to the choice calculus, we may for example specify a configurable sandwich that _always_ has bread 🍞 and cheese, _maybe_ has salad 🥗 (expressed as a choice between Salad 🥗 and an empty value `ε`), _either_ has a meat 🍖 or falafel 🧆 patty, and has _any_ combination of mayonnaise 🥚 and ketchup 🍅 as follows:
+
+```
+🍞-< 
+  Salad⟨ 🥗, ε ⟩,
+  🧀,
+  Patty⟨ 🍖, 🧆 ⟩,
+  Sauce⟨ ε, 🥚, 🍅, 🍅🥚 ⟩
+  >-
+```
+where the Y-brackets of the outer expression `🍞-< ... >-` denote that the ingredients go _within_ the bread (i.e., we build a tree where the ingredients are sub-expressions of bread).
+
+The goal of Vatras is to formalize and _compare_ languages for static variabilty.
+To this end, we formalize the syntax and semantics of the choice calculus, some of its dialects, and many more formal languages for static variability.
+For instance, writing out the above sandwich expression in our Agda formalization of the choice calculus, closely resembles the original expressions (most boilerplate comes from explicit list syntax):
+
+``` agda
+sandwich : CCC Feature ∞ Artifact
+sandwich =
+  "🍞" -<
+       "Salad" ⟨ leaf "🥗" ∷ leaf "ε" ∷ [] ⟩
+    ∷  leaf "🧀"
+    ∷  "Patty" ⟨ leaf "🍖" ∷ leaf "🧆" ∷ [] ⟩
+    ∷  "Sauce" ⟨ leaf "ε"  ∷ leaf "🥚" ∷ leaf "🍅" ∷ leaf "🍅🥚" ∷ [] ⟩
+    ∷ []
+  >-
+  where
+    leaf : String → CCC Feature ∞ Artifact
+    leaf a = a -< [] >-
+```
+
+We may configure our sandwich in terms of the semantics `⟦_⟧` for choice calculus.
+The semantics is a function takes a configuration as input to produce a variant.
+For our sandwich example, a configuration decides for each configuration option `Salad`, `Patty`, and `Sauce` which alternative to pick.
+A variant is a sandwich without any conditional elements left (i.e., a term without choices).
+From a configuration, we can derive the respective sandwich variant, and we can use Agda to prove that the semantics derive the variant we expect:
+
+``` agda
+config : Feature → ℕ
+config "Salad" = 0
+config "Patty" = 1
+config "Sauce" = 2
+config _ = 0
+
+config-makes-falafel-ketchup-sandwich :
+  ⟦ sandwich ⟧ config ≡
+    "🍞" -<
+         leaf "🥗"
+      ∷  leaf "🧀"
+      ∷  leaf "🧆"
+      ∷  leaf "🍅"
+      ∷ []
+    >-
+config-makes-falafel-ketchup-sandwich = refl
+```
+
+Vatras enables semantic comparisons of variability languages based on a meta-theory centered around the three fundamental yet unexplored properties of completeness, soundness, and expressiveness.
+Completeness serves as a lower bound (i.e., a language can express at least a given semantic domain),
+soundness serves as an upper bound (i.e., a language can express at most a given semantic domain),
+and expressiveness serves as a relative comparison (i.e., a language can express at least the semantic domain of another language).
+Proofs of these properties come as _encodings_ for completeness (i.e., a function that creates a variational expression from a set of variants), _enumerations_ for soundness (i.e., a function that enumerates all variants denoted by a variational expression), and _compilers_ between languages for expressiveness.
+Vatras includes a range of proofs of these properties for existing languages as explained in our respective paper.
+As a showcase, Vatras will show a roundtrip translation of the configurable sandwich specification above when you run it.
+Details on the features implemented in Vatras, including tutorials for integrating new languages, can be found in the **Reusability Guide** below.
+
 ## Kick-the-Tires
 
 This section gives you a short "Getting Started" guide.
@@ -502,7 +606,8 @@ Executing `git submodule update --init` in the root of the repository should fix
 ## Where does the library name 'Vatras' come from?
 
 The name Vatras is (of course) an acronym, which stands for _VAriability language TRAnslationS_.
-Besides, Vatras is a water mage in the classic german RPG [Gothic II](https://almanach.worldofgothic.de/index.php/Vatras), who is praying to the god Adanos, who brings "some kind of equality" very loosely speaking.
+Besides, Vatras is a water mage in the classic german RPG [Gothic II](https://almanach.worldofgothic.de/index.php/Vatras), who stems from the city of Varant, which almost sounds like _Variant_.
+Vatras is praying to the god Adanos, who brings some kind of equality or balance loosely speaking.
 
 [agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.4.3-blue.svg
 [agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.6.4.3

default.nix

@@ -9,7 +9,7 @@
     },
 }:
 pkgs.agdaPackages.mkDerivation {
-  version = "1.0";
+  version = "2.0";
   pname = "Vatras";
   src = with pkgs.lib.fileset;
     toSource {

src/Vatras/Framework/Composition/FeatureAlgebra.lagda.md

@@ -180,7 +180,7 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w
   ~-trans : Transitive _~_
   ~-trans (i≤j , j≤i) (j≤k , k≤j) = ≤-trans i≤j j≤k , ≤-trans k≤j j≤i
 
-  -- From the above we can conclude that introduction equivalence is an equivalence relation (not mentioned in the paper).
+  -- From the above we can conclude that introduction equivalence is an equivalence relation (not explicitly mentioned in the paper).
   ~-IsEquivalence : IsEquivalence _~_
   ~-IsEquivalence = record
     { refl  = ~-refl
@@ -207,10 +207,10 @@ record FeatureAlgebra {c} (I : Set c) (sum : Op₂ I) (𝟘 : I) : Set (suc c) w
 
   {-
   Lemma 8:
-  Introduction sum is commutative with respec to introduction equivalence.
+  Introduction sum is commutative with respect to introduction equivalence.
   This means that on both sides, we have introductions that both "contain" the same introduction
   but maybe in a different order (so the results are not propositionally equal).
-  Note that in general, introduction sum is not commutative with respect to proposition equality
+  Note that in general, introduction sum is not commutative with respect to propositional equality
   (i.e., the syntax of the actual introduction type).
   -}
   quasi-commutativity : ∀ i₂ i₁ → i₂ ⊕ i₁ ~ i₁ ⊕ i₂

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

@@ -16,7 +16,8 @@ open import Vatras.Framework.VariabilityLanguage using (VariabilityLanguage)
 open import Vatras.Framework.Properties.Completeness V
 open import Vatras.Framework.Properties.Soundness V
 open import Vatras.Framework.Relation.Expressiveness V
-open import Vatras.Data.EqIndexedSet
+-- All properties here follow from transitivity and symmetry of ≅.
+open import Vatras.Data.EqIndexedSet using (≅-trans; ≅-sym)
 ```
 
 ```agda

src/Vatras/Lang/2CC.lagda.md

@@ -3,23 +3,19 @@
 ## Module
 
 ```agda
-open import Vatras.Framework.Definitions
-module Vatras.Lang.2CC where
+open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms; 𝔼; ℂ)
+module Vatras.Lang.2CC (Dimension : 𝔽) where
 ```
 
 ## Imports
 
 ```agda
-open import Data.Bool using (Bool; true; false; if_then_else_)
-open import Data.List
-  using (List; []; _∷_; lookup)
-  renaming (map to mapl)
-open import Data.Product using (_,_)
-open import Function using (id)
+open import Data.Bool using (Bool; if_then_else_)
+open import Data.List as List using (List)
 open import Size using (Size; ↑_; ∞)
 
 open import Vatras.Framework.Variants as V using (Rose)
-open import Vatras.Framework.VariabilityLanguage
+open import Vatras.Framework.VariabilityLanguage using (𝔼-Semantics; VariabilityLanguage; ⟪_,_,_⟫)
 ```
 
 ## Syntax
@@ -31,9 +27,9 @@ or a binary choice `D ⟨ l , r ⟩` between two sub-expressions `l` and `r`, wh
 to identify the choice upon configuration.
 Dimensions `D` can be of any given type `Dimension : 𝔽`.
 ```agda
-data 2CC (Dimension : 𝔽) : Size → 𝔼 where
-   _-<_>- : ∀ {i A} → atoms A → List (2CC Dimension i A) → 2CC Dimension (↑ i) A
-   _⟨_,_⟩ : ∀ {i A} → Dimension → 2CC Dimension i A → 2CC Dimension i A → 2CC Dimension (↑ i) A
+data 2CC : Size → 𝔼 where
+   _-<_>- : ∀ {i A} → atoms A → List (2CC i A) → 2CC (↑ i) A
+   _⟨_,_⟩ : ∀ {i A} → Dimension → 2CC i A → 2CC i A → 2CC (↑ i) A
 ```
 
 ## Semantics
@@ -47,175 +43,16 @@ We define `true` to mean choosing the left alternative and `false` to choose the
 Defining it the other way around is also possible but we have to pick one definition and stay consistent.
 We choose this order to follow the known _if c then a else b_ pattern where the evaluation of a condition _c_ to true means choosing the then-branch, which is the left one.
 ```agda
-Configuration : (Dimension : 𝔽) → ℂ
-Configuration Dimension = Dimension → Bool
+Configuration : ℂ
+Configuration = Dimension → Bool
 
-⟦_⟧ : ∀ {i : Size} {Dimension : 𝔽} → 𝔼-Semantics (Rose ∞) (Configuration Dimension) (2CC Dimension i)
-⟦ a -< cs >-  ⟧ c = a V.-< mapl (λ e → ⟦ e ⟧ c) cs >-
+⟦_⟧ : ∀ {i : Size} → 𝔼-Semantics (Rose ∞) Configuration (2CC i)
+⟦ a -< cs >-  ⟧ c = a V.-< List.map (λ e → ⟦ e ⟧ c) cs >-
 ⟦ D ⟨ l , r ⟩ ⟧ c =
   if c D
   then ⟦ l ⟧ c
   else ⟦ r ⟧ c
 
-2CCL : ∀ {i : Size} (Dimension : 𝔽) → VariabilityLanguage (Rose ∞)
-2CCL {i} Dimension = ⟪ 2CC Dimension i , Configuration Dimension , ⟦_⟧ ⟫
-```
-
-In the following, we prove some interesting properties about binary choice calculus,
-known from the respective papers.
-
-```agda
-module _ {Dimension : 𝔽} where
-```
-
-## Properties
-
-Some transformation rules:
-```agda
-  open Data.List using ([_])
-  open import Data.List.Properties using (map-∘; map-cong)
-  open import Data.Nat using (ℕ)
-  open import Data.Vec as Vec using (Vec; toList; zipWith)
-  import Data.Vec.Properties as Vec
-  import Vatras.Util.Vec as Vec
-
-  open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_)
-
-  module Properties where
-    open import Vatras.Framework.Relation.Expression (Rose ∞)
-
-    module _ {A : 𝔸} where
-      {-|
-      Given a choice between two artifacts with the same atom 'a',
-      we can factor out this atom 'a' outside of the choice because no matter
-      how we configure the choice, the resulting expression will always have 'a'
-      at the top.
-      -}
-      choice-factoring : ∀ {i} {D : Dimension} {a : atoms A} {n : ℕ}
-        → (xs ys : Vec (2CC Dimension i A) n)
-          ------------------------------------------------
-        → 2CCL Dimension ⊢
-              D ⟨ a -< toList xs >- , a -< toList ys >- ⟩
-            ≣₁ a -< toList (zipWith (D ⟨_,_⟩) xs ys) >-
-      choice-factoring {i} {D} {a} {n} xs ys c =
-          ⟦ D ⟨ a -< toList xs >- , a -< toList ys >- ⟩ ⟧ c
-        ≡⟨⟩
-          (if c D then ⟦ a -< toList xs >- ⟧ c else ⟦ a -< toList ys >- ⟧ c)
-        ≡⟨ lemma (c D) ⟩
-          a V.-< toList (zipWith (λ x y → if c D then ⟦ x ⟧ c else ⟦ y ⟧ c) xs ys) >-
-        ≡⟨⟩
-          a V.-< toList (zipWith (λ x y → ⟦ D ⟨ x , y ⟩ ⟧ c) xs ys) >-
-        ≡⟨ Eq.cong (a V.-<_>-) (Eq.cong toList (Vec.map-zipWith (λ e → ⟦ e ⟧ c) (D ⟨_,_⟩) xs ys)) ⟨
-          a V.-< toList (Vec.map (λ e → ⟦ e ⟧ c) (zipWith (D ⟨_,_⟩) xs ys)) >-
-        ≡⟨ Eq.cong (a V.-<_>-) (Vec.toList-map (λ e → ⟦ e ⟧ c) (zipWith (D ⟨_,_⟩) xs ys)) ⟩
-          a V.-< mapl (λ e → ⟦ e ⟧ c) (toList (zipWith (D ⟨_,_⟩) xs ys)) >-
-        ≡⟨⟩
-          ⟦ a -< toList (zipWith (D ⟨_,_⟩) xs ys) >- ⟧ c
-        ∎
-        where
-          open Eq.≡-Reasoning
-          lemma : (b : Bool) →
-              (if b then ⟦ a -< toList xs >- ⟧ c else ⟦ a -< toList ys >- ⟧ c)
-            ≡ a V.-< toList (zipWith (λ x y → if b then ⟦ x ⟧ c else ⟦ y ⟧ c) xs ys) >-
-          lemma false =
-              (if false then ⟦ a -< toList xs >- ⟧ c else ⟦ a -< toList ys >- ⟧ c)
-            ≡⟨⟩
-              ⟦ a -< toList ys >- ⟧ c
-            ≡⟨⟩
-              a V.-< mapl (λ e → ⟦ e ⟧ c) (toList ys) >-
-            ≡⟨ Eq.cong (a V.-<_>-) (Vec.toList-map (λ e → ⟦ e ⟧ c) ys) ⟨
-              a V.-< toList (Vec.map (λ y → ⟦ y ⟧ c) ys) >-
-            ≡⟨ Eq.cong (a V.-<_>-) (Eq.cong toList (Vec.zipWith₂ (λ y → ⟦ y ⟧ c) xs ys)) ⟨
-              a V.-< toList (zipWith (λ x y → ⟦ y ⟧ c) xs ys) >-
-            ≡⟨⟩
-              a V.-< toList (zipWith (λ x y → if false then ⟦ x ⟧ c else ⟦ y ⟧ c) xs ys) >-
-            ∎
-          lemma true =
-              (if true then ⟦ a -< toList xs >- ⟧ c else ⟦ a -< toList ys >- ⟧ c)
-            ≡⟨⟩
-              ⟦ a -< toList xs >- ⟧ c
-            ≡⟨⟩
-              a V.-< mapl (λ e → ⟦ e ⟧ c) (toList xs) >-
-            ≡⟨ Eq.cong (a V.-<_>-) (Vec.toList-map (λ e → ⟦ e ⟧ c) xs) ⟨
-              a V.-< toList (Vec.map (λ x → ⟦ x ⟧ c) xs) >-
-            ≡⟨ Eq.cong (a V.-<_>-) (Eq.cong toList (Vec.zipWith₁ (λ x → ⟦ x ⟧ c) xs ys)) ⟨
-              a V.-< toList (zipWith (λ x y → ⟦ x ⟧ c) xs ys) >-
-            ≡⟨⟩
-              a V.-< toList (zipWith (λ x y → if true then ⟦ x ⟧ c else ⟦ y ⟧ c) xs ys) >-
-            ∎
-
-      {-|
-      A choice between two equal alternatives is no choice.
-      No matter how we configure the choice, the result stays the same.
-      -}
-      choice-idempotency : ∀ {D} {e : 2CC Dimension ∞ A}
-          ---------------------------------
-        → 2CCL Dimension ⊢ D ⟨ e , e ⟩ ≣₁ e
-      choice-idempotency {D} {e} c with c D
-      ... | false = refl
-      ... | true  = refl
-
-      {-|
-      If the left alternative of a choice is semantically equivalent
-      to another expression l′, we can replace the left alternative with l′.
-      -}
-      choice-l-congruence : ∀ {i : Size} {D : Dimension} {l l′ r : 2CC Dimension i A}
-        → 2CCL Dimension ⊢ l ≣₁ l′
-          ---------------------------------------
-        → 2CCL Dimension ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l′ , r ⟩
-      choice-l-congruence {D = D} l≣l′ c with c D
-      ... | false = refl
-      ... | true  = l≣l′ c
-
-      {-|
-      If the right alternative of a choice is semantically equivalent
-      to another expression r′, we can replace the right alternative with r′.
-      -}
-      choice-r-congruence : ∀ {i : Size} {D : Dimension} {l r r′ : 2CC Dimension i A}
-        → 2CCL Dimension ⊢ r ≣₁ r′
-          ---------------------------------------
-        → 2CCL Dimension ⊢ D ⟨ l , r ⟩ ≣₁ D ⟨ l , r′ ⟩
-      choice-r-congruence {D = D} r≣r′ c with c D
-      ... | false = r≣r′ c
-      ... | true  = refl
-```
-
-## Utility
-
-```agda
-  open Data.List using (concatMap) renaming (_++_ to _++l_)
-
-  {-|
-  Recursively, collect all dimensions used in a binary CC expression
-  -}
-  dims : ∀ {i : Size} {A : 𝔸} → 2CC Dimension i A → List Dimension
-  dims (_ -< es >-)  = concatMap dims es
-  dims (D ⟨ l , r ⟩) = D ∷ (dims l ++l dims r)
-```
-
-## Show
-
-```agda
-  open import Data.String as String using (String; _++_; intersperse)
-  module Pretty (show-D : Dimension → String) where
-    open import Vatras.Show.Lines
-
-    show : ∀ {i} → 2CC Dimension i (String , String._≟_) → String
-    show (a -< [] >-) = a
-    show (a -< es@(_ ∷ _) >-) = a ++ "-<" ++ (intersperse ", " (mapl show es)) ++ ">-"
-    show (D ⟨ l , r ⟩) = show-D D ++ "⟨" ++ (show l) ++ ", " ++ (show r) ++ "⟩"
-
-    pretty : ∀ {i : Size} → 2CC Dimension i (String , String._≟_) → Lines
-    pretty (a -< [] >-) = > a
-    pretty (a -< es@(_ ∷ _) >-) = do
-      > a ++ "-<"
-      indent 2 do
-        intersperseCommas (mapl pretty es)
-      > ">-"
-    pretty (D ⟨ l , r ⟩) = do
-      > show-D D ++ "⟨"
-      indent 2 do
-        appendToLastLine "," (pretty l)
-        pretty r
-      > "⟩"
+2CCL : ∀ {i : Size} → VariabilityLanguage (Rose ∞)
+2CCL {i} = ⟪ 2CC i , Configuration , ⟦_⟧ ⟫
 ```