Merge pull request #88 from VariantSync/develop

Release: Variation Trees

Author: pmbittner

.projectile

@@ -0,0 +1,6 @@
+;; This file stores project information for the Projectile package in Emacs.
+;; If you do not use emacs, you can ignore this file.
+
+;; ignore some files from indexing:
+-.agdai
+-src/MAlonzo

README.md

@@ -27,7 +27,7 @@ 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?
+## 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.

default.nix

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

src/Vatras/Data/Prop.agda

@@ -0,0 +1,33 @@
+module Vatras.Data.Prop where
+
+open import Data.Bool as Bool using (Bool)
+
+data Prop (F : Set) : Set where
+  true  : Prop F
+  false : Prop F
+  var   : F → Prop F
+  ¬_    : Prop F → Prop F
+  _∧_   : Prop F → Prop F → Prop F
+
+infix 23 ¬_
+infix 22 _∧_
+
+_∨_ : ∀ {F} → Prop F → Prop F → Prop F
+a ∨ b = ¬ (¬ a ∧ ¬ b)
+
+_⇒_ : ∀ {F} → Prop F → Prop F → Prop F
+a ⇒ b = ¬ a ∨ b
+
+_⇔_ : ∀ {F} → Prop F → Prop F → Prop F
+a ⇔ b = (a ⇒ b) ∧ (b ⇒ a)
+
+Assignment : Set → Set
+Assignment F = F → Bool
+
+eval : ∀ {F} → Prop F → Assignment F → Bool
+eval true    _ = Bool.true
+eval false   _ = Bool.false
+eval (var p) c = c p
+eval (¬ p)   c = Bool.not (eval p c)
+eval (p ∧ q) c = (eval p c) Bool.∧ (eval q c)
+

src/Vatras/Data/Prop/Properties.agda

@@ -0,0 +1,141 @@
+module Vatras.Data.Prop.Properties {F : Set} where
+
+import Data.Bool as Bool
+open import Data.Bool.Properties using (∧-comm; ∧-zeroˡ; ∧-zeroʳ)
+open import Data.Empty using (⊥)
+open import Data.Product as Product using (Σ; _×_; ∃-syntax; _,_)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+
+open import Relation.Nullary.Negation renaming (¬_ to negate)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong; sym; trans)
+open Eq.≡-Reasoning
+
+open import Vatras.Data.Prop
+open import Vatras.Util.AuxProofs using (true≢false)
+
+all-true : Assignment F
+all-true _ = Bool.true
+
+all-false : Assignment F
+all-false _ = Bool.false
+
+NonContradiction :
+  ∀ {b} {p : Prop F} (a : Assignment F)
+  → eval    p  a ≡ b
+  → eval (¬ p) a ≡ Bool.not b
+NonContradiction _ eq = cong Bool.not eq
+
+NonContradiction' :
+  ∀ (p : Prop F) (a : Assignment F)
+  → eval p a ≡ Bool.true
+  → eval p a ≡ Bool.false
+  → ⊥
+NonContradiction' _ _ = true≢false
+
+Satisfying : Prop F → Assignment F → Set
+Satisfying p a = eval p a ≡ Bool.true
+
+Unsatisfying : Prop F → Assignment F → Set
+Unsatisfying p a = eval p a ≡ Bool.false
+
+Satisfiable : Prop F → Set
+Satisfiable p = Σ (Assignment F) (Satisfying p)
+
+Falsifiable : Prop F → Set
+Falsifiable p = Σ (Assignment F) (Unsatisfying p)
+
+Tautology : Prop F → Set
+Tautology p = ∀ a → Satisfying p a
+
+Contradiction : Prop F → Set
+Contradiction p = ∀ a → Unsatisfying p a
+
+Const : Prop F → Set
+Const p = Tautology p ⊎ Contradiction p
+
+Const' : Prop F → Set
+Const' p = ∃[ b ] (∀ a → eval p a ≡ b)
+
+Const→Const' : ∀ {p} → Const p → Const' p
+Const→Const' (inj₁ taut ) = Bool.true  , taut
+Const→Const' (inj₂ contr) = Bool.false , contr
+
+Const'→Const : ∀ {p} → Const' p → Const p
+Const'→Const (Bool.true  , taut ) = inj₁ taut
+Const'→Const (Bool.false , contr) = inj₂ contr
+
+Nonconst : Prop F → Set
+Nonconst p = Satisfiable p × Falsifiable p
+
+Nonconst' : Prop F → Set
+Nonconst' p = negate (Const p)
+
+Nonconst→Nonconst' : ∀ {p} → Nonconst p → Nonconst' p
+Nonconst→Nonconst' {p} (_ , (a , a-makes-false)) (inj₁ taut ) = NonContradiction' p a (taut a) a-makes-false
+Nonconst→Nonconst' {p} ((a , a-makes-true) , _)  (inj₂ contr) = NonContradiction' p a a-makes-true (contr a)
+
+sat-∧ˡ : ∀ p q
+  → Tautology p
+  → Satisfiable q
+  → Satisfiable (p ∧ q)
+sat-∧ˡ p q taut-p (a , sat) = a , (
+  eval (p ∧ q) a            ≡⟨⟩
+  eval p a  Bool.∧ eval q a ≡⟨ cong (Bool._∧ eval q a) (taut-p a) ⟩
+  Bool.true Bool.∧ eval q a ≡⟨⟩
+  eval q a                  ≡⟨ sat ⟩
+  Bool.true                 ∎)
+
+sat-∧ʳ : ∀ p q
+  → Tautology q
+  → Satisfiable p
+  → Satisfiable (p ∧ q)
+sat-∧ʳ p q taut-q (a , sat) = a , (
+  eval (p ∧ q) a            ≡⟨⟩
+  eval p a Bool.∧ eval q a  ≡⟨ cong (eval p a Bool.∧_) (taut-q a) ⟩
+  eval p a Bool.∧ Bool.true ≡⟨ cong (Bool._∧ Bool.true) sat ⟩
+  Bool.true                 ∎)
+
+fal-∧ˡ : ∀ p q
+  → Falsifiable p
+  → Falsifiable (p ∧ q)
+fal-∧ˡ p q (a , unsat) = a , (
+  eval (p ∧ q) a             ≡⟨⟩
+  eval p a   Bool.∧ eval q a ≡⟨ cong (Bool._∧ eval q a) unsat ⟩
+  Bool.false Bool.∧ eval q a ≡⟨ ∧-zeroˡ (eval q a) ⟩
+  Bool.false                 ∎)
+
+fal-∧ʳ : ∀ p q
+  → Falsifiable q
+  → Falsifiable (p ∧ q)
+fal-∧ʳ p q (a , unsat) = a , (
+  eval (p ∧ q) a             ≡⟨⟩
+  eval p a Bool.∧ eval q a   ≡⟨ cong (eval p a Bool.∧_) unsat ⟩
+  eval p a Bool.∧ Bool.false ≡⟨ ∧-zeroʳ (eval p a) ⟩
+  Bool.false                 ∎)
+
+-- generalize?
+fal-∧-cong : ∀ p q
+  → Falsifiable (p ∧ q)
+  → Falsifiable (q ∧ p)
+fal-∧-cong p q (a , unsat) rewrite ∧-comm (eval p a) (eval q a) = a , unsat
+
+taut-∧ : ∀ p q
+  → Tautology p
+  → Tautology q
+  → Tautology (p ∧ q)
+taut-∧ p q taut-p taut-q a rewrite taut-p a | taut-q a = refl
+
+contr-∧ˡ : ∀ p q
+  → Contradiction p
+  → Contradiction (p ∧ q)
+contr-∧ˡ p q contr-p a rewrite contr-p a = refl
+
+contr-∧ʳ : ∀ p q
+  → Contradiction q
+  → Contradiction (p ∧ q)
+contr-∧ʳ p q contr-q a =
+    eval (p ∧ q) a             ≡⟨⟩
+    eval p a Bool.∧ eval q a   ≡⟨ cong (eval p a Bool.∧_) (contr-q a) ⟩
+    eval p a Bool.∧ Bool.false ≡⟨ ∧-comm (eval p a) Bool.false ⟩
+    Bool.false                 ∎
+

src/Vatras/Data/Prop/Rename.agda

@@ -0,0 +1,49 @@
+{-|
+This module renames variables in Prop expressions.
+
+The idea of this translation is to apply a renaming function `f : F₁ → F₂` to
+all elements of `F₁` in the datastructure `Prop F₁` to obtain a new datastructure
+`Prop F₂`. To prove preservation of the semantics, we also require a left inverse
+`f⁻¹ : D₂ → D₁` of `f` as a proof that `f` is injective. This precondition is
+necessary because a non-injective rename could reduce the number of variables.
+-}
+module Vatras.Data.Prop.Rename where
+
+import Data.Bool as Bool
+open import Function using (_∘_; id)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_)
+
+open import Vatras.Data.Prop
+
+rename : {F₁ F₂ : Set} → (F₁ → F₂) → Prop F₁ → Prop F₂
+rename f true = true
+rename f false = false
+rename f (var v) = var (f v)
+rename f (¬ p) = ¬ (rename f p)
+rename f (p ∧ q) = rename f p ∧ rename f q
+
+rename-spec
+  : {F₁ F₂ : Set}
+  → (f : F₁ → F₂)
+  → (p : Prop F₁)
+  → (c : Assignment F₂)
+  → eval (rename f p) c ≡ eval p (c ∘ f)
+rename-spec f true c = refl
+rename-spec f false c = refl
+rename-spec f (var v) c = refl
+rename-spec f (¬ p) c = Eq.cong Bool.not (rename-spec f p c)
+rename-spec f (p ∧ q) c = Eq.cong₂ Bool._∧_ (rename-spec f p c) (rename-spec f q c)
+
+rename-preserves
+  : {F₁ F₂ : Set}
+  → (f : F₁ → F₂)
+  → (f⁻¹ : F₂ → F₁)
+  → f⁻¹ ∘ f ≗ id
+  → (p : Prop F₁)
+  → (c : Assignment F₁)
+  → eval (rename f p) (c ∘ f⁻¹) ≡ eval p c
+rename-preserves f f⁻¹ f∘f⁻¹≗id true c = refl
+rename-preserves f f⁻¹ f∘f⁻¹≗id false c = refl
+rename-preserves f f⁻¹ f∘f⁻¹≗id (var v) c = Eq.cong c (f∘f⁻¹≗id v)
+rename-preserves f f⁻¹ f∘f⁻¹≗id (¬ p) c = Eq.cong Bool.not (rename-preserves f f⁻¹ f∘f⁻¹≗id p c)
+rename-preserves f f⁻¹ f∘f⁻¹≗id (p ∧ q) c = Eq.cong₂ Bool._∧_ (rename-preserves f f⁻¹ f∘f⁻¹≗id p c) (rename-preserves f f⁻¹ f∘f⁻¹≗id q c)

src/Vatras/Framework/Annotation/IndexedDimension.agda

@@ -6,6 +6,7 @@ IndexedDimension is used for conversions from NCC to NCC with lower arity (in pa
 module Vatras.Framework.Annotation.IndexedDimension where
 
 open import Data.Fin using (Fin)
+open import Data.Nat using (ℕ)
 open import Data.Product using (_×_)
 open import Vatras.Util.Nat.AtLeast using (ℕ≥; toℕ; pred)
 open import Vatras.Framework.Definitions using (𝔽)
@@ -16,3 +17,6 @@ D with indices i ∈ ℕ, where 2 ≤ n.
 -}
 IndexedDimension : (D : 𝔽) → (n : ℕ≥ 2) → 𝔽
 IndexedDimension D n = D × Fin (toℕ (pred n))
+
+Indexed : 𝔽 → 𝔽
+Indexed F = F × ℕ

src/Vatras/Framework/Definitions.agda

@@ -61,3 +61,16 @@ and hence expressions are parameterized in the type of this atomic data.
 -}
 𝔼 : Set₂
 𝔼 = 𝔸 → Set₁
+
+-- some default atoms
+module _ where
+  open import Data.String using (String; _≟_)
+
+  STRING : 𝔸
+  STRING = String and _≟_
+
+module _ where
+  open import Data.Nat using (ℕ; _≟_)
+
+  NAT : 𝔸
+  NAT = ℕ and _≟_

src/Vatras/Framework/Variants.agda

@@ -32,6 +32,9 @@ Rose trees are sized for termination checking.
 data Rose : Size → 𝕍 where
   _-<_>- : ∀ {i} {A : 𝔸} → atoms A → List (Rose i A) → Rose (↑ i) A
 
+Forest : 𝕍
+Forest A = List (Rose ∞ A)
+
 {-|
 Variants for gruler's language also form trees but opposed to rose trees,
 nodes are binary and data is stored only in leaves.
@@ -50,6 +53,12 @@ data GrulerVariant : 𝕍 where
 rose-leaf : ∀ {A : 𝔸} → atoms A → Rose ∞ A
 rose-leaf {A} a = a -< [] >-
 
+forest-leaf : ∀ {A : 𝔸} → atoms A → Forest A
+forest-leaf a = rose-leaf a ∷ []
+
+forest-singleton : ∀ {A : 𝔸} → atoms A → Forest A → Forest A
+forest-singleton a l = a -< l >- ∷ []
+
 {-|
 Interestingly, variants are also variability languages
 (and it does not matter how variants actually look like).

src/Vatras/Lang/ADT/Merge.agda

@@ -0,0 +1,81 @@
+open import Vatras.Framework.Definitions
+module Vatras.Lang.ADT.Merge
+  (V : 𝕍)
+  (_+ᵥ_ : ∀ {A} → V A → V A → V A)
+  where
+
+open import Data.Bool using (if_then_else_; true; false)
+open import Data.Bool.Properties using (if-float)
+open import Relation.Binary.PropositionalEquality using (refl; _≡_; _≗_)
+open Relation.Binary.PropositionalEquality.≡-Reasoning
+
+open import Vatras.Util.AuxProofs using (if-cong)
+
+import Vatras.Lang.ADT
+
+module Named (F : 𝔽) where
+  open Vatras.Lang.ADT F V
+
+  {-|
+  Merges two ADTs.
+  The resulting ADT denotes all possible compositions of variants, such that configuring the resulting ADT
+  is equivalent to configuring both input ADTs and composing the resulting variants (see ⊕-spec below).
+  This operations inherits all properties of the variant composition (e.g., commutativity, associativity etc).
+  -}
+  _⊕_ : ∀ {A} → ADT A → ADT A → ADT A
+  leaf l          ⊕ leaf r          = leaf (l +ᵥ r)
+  leaf l          ⊕ (E ⟨ el , er ⟩) = E ⟨ leaf l ⊕ el , leaf l ⊕ er ⟩
+  (D ⟨ dl , dr ⟩) ⊕ r               = D ⟨ dl ⊕ r , dr ⊕ r ⟩
+
+  ⊕-spec : ∀ {A} (l r : ADT A) (c : Configuration) →
+     ⟦ l ⊕ r ⟧ c ≡ ⟦ l ⟧ c +ᵥ ⟦ r ⟧ c
+  ⊕-spec (leaf l) (leaf r) c = refl
+  ⊕-spec (leaf l) (E ⟨ el , er ⟩) c with c E
+  ... | true = ⊕-spec (leaf l) el c
+  ... | false = ⊕-spec (leaf l) er c
+  ⊕-spec (D ⟨ dl , dr ⟩) r c with c D
+  ... | true  = ⊕-spec dl r c
+  ... | false = ⊕-spec dr r c
+
+  ---- Properties ----
+  -- The merge operator inherits
+  -- properties of the variant composition operator.
+  --------------------
+
+  -- import Algebra.Definitions
+  -- module Eq (A : 𝔸) where
+  --   open Algebra.Definitions (_≡_ {A = V A}) using (Commutative) public
+
+  -- module Sem (A : 𝔸) where
+  --   open Algebra.Definitions (_⊢_≣₁_ {A} ADTL) using (Commutative) public
+
+  -- ⊕-comm : ∀ {A} → Eq.Commutative A _+ᵥ_ -> Sem.Commutative A _⊕_
+  ⊕-comm :
+    (∀ {A} (v w : V A) → v +ᵥ w ≡ w +ᵥ v) →
+    ---------------------------------------------
+    (∀ {A} (l r : ADT A) → ⟦ l ⊕ r ⟧ ≗ ⟦ r ⊕ l ⟧)
+  ⊕-comm +ᵥ-comm l r c =
+      ⟦ l ⊕ r ⟧ c
+    ≡⟨ ⊕-spec l r c ⟩
+      ⟦ l ⟧ c +ᵥ ⟦ r ⟧ c
+    ≡⟨ +ᵥ-comm (⟦ l ⟧ c) (⟦ r ⟧ c) ⟩
+      ⟦ r ⟧ c +ᵥ ⟦ l ⟧ c
+    ≡⟨ ⊕-spec r l c ⟨
+      ⟦ r ⊕ l ⟧ c
+    ∎
+
+module Prop (F : 𝔽) where
+  open import Vatras.Data.Prop
+  open Vatras.Lang.ADT (Prop F) V
+  open import Vatras.Lang.ADT.Prop F V
+  open Named (Prop F)
+
+  ⊕-specₚ : ∀ {A} (l r : ADT A) (c : Assignment F) →
+     ⟦ l ⊕ r ⟧ₚ c ≡ ⟦ l ⟧ₚ c +ᵥ ⟦ r ⟧ₚ c
+  ⊕-specₚ (leaf v) (leaf r) c = refl
+  ⊕-specₚ (leaf l) (E ⟨ el , er ⟩) c with eval E c
+  ... | true  = ⊕-specₚ (leaf l) el c
+  ... | false = ⊕-specₚ (leaf l) er c
+  ⊕-specₚ (D ⟨ dl , dr ⟩) r c with eval D c
+  ... | true = ⊕-specₚ dl r c
+  ... | false = ⊕-specₚ dr r c