Artifact Overview for OOPSLA

Dockerfile

@@ -37,4 +37,4 @@ COPY --from=builder /home/user/result /demo
 # Unicode characters.
 ENV LC_ALL=C.UTF-8
 
-CMD ["/demo/bin/EPVL"]
+CMD ["/demo/bin/Vatras"]

EPVL.agda-lib

@@ -1,4 +1,4 @@
-name: EPVL
+name: Vatras
 depend: standard-library-2.0
 include: src
 flags: --sized-types

default.nix

@@ -10,7 +10,7 @@
 }:
 pkgs.agdaPackages.mkDerivation {
   version = "1.0";
-  pname = "EPVL";
+  pname = "Vatras";
   src = with pkgs.lib.fileset;
     toSource {
       root = ./.;
@@ -19,6 +19,7 @@ pkgs.agdaPackages.mkDerivation {
 
   buildInputs = [
     pkgs.agdaPackages.standard-library
+    pkgs.makeWrapper
   ];
 
   buildPhase = ''
@@ -29,6 +30,8 @@ pkgs.agdaPackages.mkDerivation {
 
   postInstall = ''
     install -D src/Main "$out/bin/$pname"
+    wrapProgram "$out/bin/$pname" \
+      --set LC_ALL C.UTF-8
   '';
 
   meta = {description = "On the Expressive Power of Languages for Static Variability";};

nix/github-workflow-dependencies.nix

@@ -8,8 +8,8 @@
       inherit system;
     },
 }: let
-  EPVL = import ../default.nix {};
+  Vatras = import ../default.nix {};
 in
   pkgs.mkShell {
-    inputsFrom = [EPVL];
+    inputsFrom = [Vatras];
   }

src/Data/IndexedSet.lagda.md

@@ -15,6 +15,8 @@ open import Relation.Binary.Indexed.Heterogeneous using (
   Symmetric;
   Transitive;
   IsIndexedEquivalence)
+open import Relation.Binary.Indexed.Homogeneous using (
+  IsIndexedPartialOrder)
 module Data.IndexedSet
   {c ℓ : Level}
   (S : Setoid c ℓ)
@@ -131,6 +133,22 @@ irrelevant-index (x , Ai≈x) {i} {j} = Eq.trans (Ai≈x i) (Eq.sym (Ai≈x j))
   ; trans = ≅-trans
   }
 
+-- TODO: There is no heterogeneous version in the standard library. Hence, we
+-- only use the homogeneous one here.
+⊆-IsIndexedPartialOrder : IsIndexedPartialOrder (IndexedSet {iℓ}) _≅_ _⊆_
+⊆-IsIndexedPartialOrder = record
+  { isPreorderᵢ = record
+    { isEquivalenceᵢ = record
+      { reflᵢ = ≅-refl
+      ; symᵢ = ≅-sym
+      ; transᵢ = ≅-trans
+      }
+    ; reflexiveᵢ = proj₁
+    ; transᵢ = ⊆-trans
+    }
+  ; antisymᵢ = ⊆-antisym
+  }
+
 ≐-refl : ∀ {I} → RB.Reflexive (_≐_ {iℓ} {I})
 ≐-refl i = refl
 

src/Framework/Definitions.agda

@@ -12,22 +12,28 @@ open import Relation.Nullary.Negation using (¬_)
 
 {-
 Some Atomic Data.
-We have no assumptions on that data so its just a type.
+Any type can be used as atomic data in variants as long as
+we can decide equality.
+Our framework as well as most variability language actually
+do not require decidable equality but a few variability languages
+require it (e.g., feature structure trees).
+We decided to include the assumption that equality is decidable into
+the core definitions because it is quite reasonable.
+Any actual data we can think of to plug in here (e.g., strings, tokens or
+nodes of an abstract syntax tree) can be checked for equality.
 -}
--- 𝔸 : ∀ {ℓ} → Set (suc ℓ)
--- 𝔸 {ℓ} = Set ℓ
 𝔸 : Set₁
 𝔸 = Σ Set DecidableEquality
 
+-- retrieve the set of atoms from an atom type 𝔸
 atoms : 𝔸 → Set
 atoms = proj₁
 
 {-
 Variant Language.
 A variant should represent atomic data in some way so its parameterized in atomic data.
+In our paper, this type is fixed to rose trees (see Framework.Variants.agda).
 -}
--- 𝕍 : ∀ {ℓ} → Set (suc ℓ)
--- 𝕍 {ℓ} = 𝔸 {ℓ} → Set ℓ
 𝕍 : Set₂
 𝕍 = 𝔸 → Set₁
 
@@ -38,14 +44,12 @@ We have no assumptions on this kind of language (yet).
 In the future, it might be interesting to dig deeper into 𝔽 and to explore its impact on a
 language's expressiveness more deeply.
 -}
--- 𝔽 : ∀ {ℓ} → Set (suc ℓ)
--- 𝔽 {ℓ} = Set ℓ
 𝔽 : Set₁
 𝔽 = Set
 
 {-
 Feature Selection Language.
-This is the semantic of an annotation language 𝔽. An instance of 𝕊 describes the
+This is the semantics of an annotation language 𝔽. An instance of 𝕊 describes the
 set of configurations for a feature language 𝔽.  Usually, each feature selection
 language `S : 𝕊` has a some function `ConfigEvaluater F S Sel` which resolves an
 expression of the annotation language `F : 𝔽` to a selection `Sel` interpreted
@@ -56,6 +60,7 @@ selections language.
 𝕊 : Set₁
 𝕊 = Set
 
+-- Set of configuration languages
 𝕂 : Set₁
 𝕂 = Set
 
@@ -66,8 +71,6 @@ occur within an expression.
 Such sub-terms describe variants of atomic data (i.e., some structure on atomic elements),
 and hence expressions are parameterized in the type of this atomic data.
 -}
--- 𝔼 : ∀ {ℓ} → Set (suc ℓ)
--- 𝔼 {ℓ} = 𝔸 {ℓ} → Set ℓ
 𝔼 : Set₂
 𝔼 = 𝔸 → Set₁
 
@@ -81,7 +84,5 @@ they must know the atomic data type.
 Moreover, constructs often denote variational expressions and hence require a language
 for variability annotations 𝔽.
 -}
--- ℂ : ∀ {ℓ} → Set (suc ℓ)
--- ℂ {ℓ} = 𝔼 {ℓ} → 𝔸 {ℓ} → Set ℓ
 ℂ : Set₂
 ℂ = 𝔼 → 𝔸 → Set₁

src/Framework/Relation/Expressiveness.lagda.md

@@ -6,7 +6,7 @@ open import Data.EqIndexedSet using (≅[]→≅)
 open import Data.Empty using (⊥)
 open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂)
 open import Relation.Nullary.Negation using (¬_; contraposition)
-open import Relation.Binary using (IsEquivalence; Reflexive; Symmetric; Transitive; Antisymmetric)
+open import Relation.Binary using (IsEquivalence; IsPartialOrder; Reflexive; Symmetric; Transitive; Antisymmetric)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 open import Function using (_∘_; Injective)
 
@@ -70,6 +70,24 @@ _is-equally-expressive-as_ = _≋_
 ≋-trans (L₁≽L₂ , L₂≽L₁) (L₂≽L₃ , L₃≽L₂)
   =   ≽-trans L₁≽L₂ L₂≽L₃
     , ≽-trans L₃≽L₂ L₂≽L₁
+
+≋-IsEquivalence : IsEquivalence _≋_
+≋-IsEquivalence = record
+  { refl = ≋-refl
+  ; sym = ≋-sym
+  ; trans = ≋-trans
+  }
+
+≽-IsPartialOrder : IsPartialOrder _≋_ _≽_
+≽-IsPartialOrder = record
+  { isPreorder = record
+    { isEquivalence = ≋-IsEquivalence
+    ; reflexive = proj₁
+    ; trans = ≽-trans
+    }
+  ; antisym = ≽-antisym
+  }
+
 ```
 
 ## Concluding expressiveness from translations
@@ -89,6 +107,43 @@ expressiveness-from-compiler : ∀ {L₁ L₂ : VariabilityLanguage V}
   → L₂ ≽ L₁
 expressiveness-from-compiler compiler = expressiveness-by-translation (LanguageCompiler.compile compiler) (λ e → ≅[]→≅ (LanguageCompiler.preserves compiler e))
 
+{-
+Since Agda is based on constructive logic,
+any proof of existence explicitly constructs the element
+in questions. Hence, from a proof of expressiveness,
+we can always use the constructed elements (expressions and configurations)
+to be the result of a compiler.
+-}
+compiler-from-expressiveness : ∀ {L₁ L₂ : VariabilityLanguage V}
+  → L₂ ≽ L₁
+  → LanguageCompiler L₁ L₂
+compiler-from-expressiveness {L₁} {L₂} exp = record
+  { compile         = proj₁ ∘ exp
+  ; config-compiler = λ e → record { to = conf e ; from = fnoc e }
+  ; preserves       = λ e → ⊆-conf e , ⊆-fnoc e
+  }
+  where
+    ⟦_⟧₁ = Semantics L₁
+    ⟦_⟧₂ = Semantics L₂
+    open import Data.EqIndexedSet
+
+    conf : ∀ {A} → Expression L₁ A → Config L₁ → Config L₂
+    conf e c₁ = proj₁ (proj₁ (proj₂ (exp e)) c₁)
+
+    fnoc : ∀ {A} → Expression L₁ A → Config L₂ → Config L₁
+    fnoc e c₂ = proj₁ (proj₂ (proj₂ (exp e)) c₂)
+
+    eq : ∀ {A} → (e : Expression L₁ A) → ⟦ e ⟧₁ ≅ ⟦ proj₁ (exp e) ⟧₂
+    eq e = proj₂ (exp e)
+
+    ⊆-conf : ∀ {A} → (e : Expression L₁ A) → ⟦ e ⟧₁ ⊆[ conf e ] ⟦ proj₁ (exp e) ⟧₂
+    ⊆-conf e with eq e
+    ... | ⊆ , _ = proj₂ ∘ ⊆
+
+    ⊆-fnoc : ∀ {A} → (e : Expression L₁ A) → ⟦ proj₁ (exp e) ⟧₂ ⊆[ fnoc e ] ⟦ e ⟧₁
+    ⊆-fnoc e with eq e
+    ... | _ , ⊇ = proj₂ ∘ ⊇
+
 compiler-cannot-exist : ∀ {L₁ L₂ : VariabilityLanguage V}
   → L₂ ⋡ L₁
   → LanguageCompiler L₁ L₂

src/Main.agda

@@ -35,12 +35,11 @@ Each experiment is run on each example from a list of examples (i.e., experiment
 -}
 experimentsToRun : List (ExperimentSetup (suc 0ℓ))
 experimentsToRun =
-  -- DEPRECATED: Run some example translations from n-ary to binary choice calculus
-  -- DEPRECATED: (CCC  ∞ String , exp-to-binary-and-back , cccex-all) ∷
   -- Run some example translations of option calculus to binary choice calculus
   setup exp-oc-to-bcc optex-all ∷
-
+  -- Run some example configurations of feature structure trees.
   setup toy-calculator-experiment ex-all ∷
+  -- Run the roundtrip demo.
   setup round-trip RoundTrip.examples ∷
   []
 
@@ -52,7 +51,7 @@ main_lines = do
   linebreak
   > "It's dangerous to go alone! Take this unicode to see whether your terminal supports it:"
   > "  ₙ ₁ ₂ 𝕃 ℂ 𝔸 ⟦ ⟧ ⟨ ⟩ ❲❳"
-  > "... but now on to the experiments."
+  > "... but now on to the demo."
   linebreak
   linebreak
   overwrite-alignment-with

src/Test/Experiment.agda

@@ -25,6 +25,9 @@ Experiment A = Named (Example A → Lines)
 ExperimentSetup : ∀ ℓ → Set (suc ℓ)
 ExperimentSetup ℓ = Σ[ A ∈ Set ℓ ] (Experiment A × List (Example A))
 
+-- This functions creates an ExperimentSetup from an experiment and its list of inputs.
+-- (This basically constitutes a smart constructor avoiding the need to explicitly state
+-- the type of the underlying input data.)
 setup : ∀ {ℓ} {A : Set ℓ} → Experiment A → List (Example A) → ExperimentSetup ℓ
 setup {ℓ} {A} program inputs = A , program , inputs
 

src/Translation/Lang/OC-to-2CC.lagda.md

@@ -462,6 +462,6 @@ OC→2CC = record
   ; preserves = compile-preserves
   }
 
-2CC≽OC : 2CCL F ≽ (WFOCL F)
+2CC≽OC : 2CCL F ≽ WFOCL F
 2CC≽OC = expressiveness-from-compiler OC→2CC
 ```

src/Translation/LanguageMap.lagda.md

@@ -24,12 +24,13 @@ Variant = Rose ∞
 open import Framework.Annotation.IndexedDimension
 open import Framework.Compiler
 open import Framework.Definitions using (𝕍; 𝔽)
-open import Framework.Relation.Expressiveness Variant using (_≽_; ≽-trans; _⋡_; _≋_; compiler-cannot-exist)
+open import Framework.Relation.Expressiveness Variant using (_≽_; ≽-trans; _≻_; _⋡_; _≋_; compiler-cannot-exist)
 open import Framework.Proof.Transitive Variant using (less-expressive-from-completeness; completeness-by-expressiveness; soundness-by-expressiveness)
 open import Framework.Properties.Completeness Variant using (Complete)
 open import Framework.Properties.Soundness Variant using (Sound)
 open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs)
 open import Util.AuxProofs using (decidableEquality-×)
+open import Util.String using (diagonal-ℕ; diagonal-ℕ⁻¹; diagonal-ℕ-proof)
 
 open import Lang.All
 open VariantList using (VariantListL)
@@ -144,7 +145,12 @@ make the changes in the feature model explicit. For theoretical results however,
 it is easier to assume that the set of annotations `F` is infinite, which is
 equivalent to the restriction used here (except if `F` is empty).
 
-A witness of these preconditions can be faund in `Util.String`.
+This assumption is reasonable because it is satisfied by natural numbers
+(via [Cantor's first diagonal argument](https://de.wikipedia.org/wiki/Cantors_erstes_Diagonalargument)
+which was used to show that there are countably but infinite many rational numbers)
+and Strings. A witness of these preconditions for Strings can be found in `Util.String`.
+An alias module for importing expressiveness fixed to Strings and with the
+respective preconditions satisfied can be found below the `Expressivness` module.
 
 ```agda
 module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f⁻¹∘f≗id : f⁻¹ ∘ f ≗ id) where
@@ -235,6 +241,12 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ)
   VariantList≋CCC _==_ D = ≽-trans (VariantList≽ADT _==_) (≽-trans ADT≽2CC 2CC≽CCC) , CCC≽VariantList D
 ```
 
+The following module is an alias, which you can used to import
+the `Expressiveness` module above but with the set of annotations
+fixed to Strings.
+```agda
+module Expressiveness-String = Expressiveness diagonal-ℕ diagonal-ℕ⁻¹ diagonal-ℕ-proof
+```
 
 ## Completeness
 
@@ -261,27 +273,30 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f
 
   open OC.IncompleteOnRose using (OC-is-incomplete)
 
-  OC-is-less-expressive-than-2CC : WFOCL F ⋡ 2CCL F
-  OC-is-less-expressive-than-2CC = less-expressive-from-completeness 2CC-is-complete OC-is-incomplete
+  OC⋡2CC : WFOCL F ⋡ 2CCL F
+  OC⋡2CC = less-expressive-from-completeness 2CC-is-complete OC-is-incomplete
+
+  2CC≻WFOC : 2CCL F ≻ WFOCL F
+  2CC≻WFOC = 2CC≽OC , OC⋡2CC
 
   2CC-cannot-be-compiled-to-OC : ¬ (LanguageCompiler (2CCL F) (WFOCL F))
-  2CC-cannot-be-compiled-to-OC = compiler-cannot-exist OC-is-less-expressive-than-2CC
+  2CC-cannot-be-compiled-to-OC = compiler-cannot-exist OC⋡2CC
 
   open FST.IncompleteOnRose using (FST-is-incomplete)
 
-  FST-is-less-expressive-than-2CC : FSTL F ⋡ 2CCL F
-  FST-is-less-expressive-than-2CC = less-expressive-from-completeness 2CC-is-complete (FST-is-incomplete F)
+  FST⋡2CC : FSTL F ⋡ 2CCL F
+  FST⋡2CC = less-expressive-from-completeness 2CC-is-complete (FST-is-incomplete F)
 
   2CC-cannot-be-compiled-to-FST : ¬ (LanguageCompiler (2CCL F) (FSTL F))
-  2CC-cannot-be-compiled-to-FST = compiler-cannot-exist FST-is-less-expressive-than-2CC
+  2CC-cannot-be-compiled-to-FST = compiler-cannot-exist FST⋡2CC
 
   open OC-to-FST using (FSTL⋡WFOCL)
 
-  FST-is-less-expressive-than-OC : FSTL F ⋡ WFOCL F
-  FST-is-less-expressive-than-OC = FSTL⋡WFOCL F
+  FST⋡OC : FSTL F ⋡ WFOCL F
+  FST⋡OC = FSTL⋡WFOCL F
 
   OC-cannot-be-compiled-to-FST : ¬ (LanguageCompiler (WFOCL F) (FSTL F))
-  OC-cannot-be-compiled-to-FST = compiler-cannot-exist FST-is-less-expressive-than-OC
+  OC-cannot-be-compiled-to-FST = compiler-cannot-exist FST⋡OC
 ```
 
 For the proof of `WFOCL⋡FSTL`, we need to construct at least three distinct
@@ -298,6 +313,11 @@ comparing these features to decided which values these features are assigned.
     FST-cannot-be-compiled-to-OC = compiler-cannot-exist OC-is-less-expressive-than-FST
 ```
 
+As for `Expressiveness` we re-export `Completeness` fixed to String and its respective proofs.
+```agda
+module Completeness-String = Completeness diagonal-ℕ diagonal-ℕ⁻¹ diagonal-ℕ-proof
+```
+
 ```agda
 open VariantList using (VariantList-is-Sound) public