Merge pull request #82 from VariantSync/variation-tree

Variation Trees

Author: pmbittner

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/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

src/Vatras/Lang/ADT/Prop.agda

@@ -0,0 +1,13 @@
+open import Vatras.Framework.Definitions
+module Vatras.Lang.ADT.Prop (F : 𝔽) (V : 𝕍) where
+
+open import Data.Bool using (if_then_else_)
+open import Vatras.Data.Prop using (Prop; Assignment; eval)
+open import Vatras.Framework.VariabilityLanguage
+open import Vatras.Lang.ADT (Prop F) V
+
+⟦_⟧ₚ : 𝔼-Semantics V (Assignment F) ADT
+⟦ e ⟧ₚ c = ⟦ e ⟧ (λ D → eval D c)
+
+PropADTL : VariabilityLanguage V
+PropADTL = ⟪ ADT , Assignment F , ⟦_⟧ₚ ⟫

src/Vatras/Lang/ADT/Pushdown.agda

@@ -0,0 +1,65 @@
+open import Vatras.Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
+open import Data.List as List using (List; []; _∷_; _ʳ++_)
+
+{-|
+This module provides a function for inserting artifacts at the top of ADTs.
+This operation means that any produced variant will have the given atom at the top.
+The parameter of this module is the constructor for adding an atom on top of existing variants.
+-}
+module Vatras.Lang.ADT.Pushdown (F : 𝔽) (V : 𝕍)
+  (_-<_>- : ∀ {A} → atoms A → List (V A) → V A)
+  where
+
+open import Data.Bool using (if_then_else_)
+import Data.Bool.Properties as Bool
+import Data.List.Properties as List
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎)
+open import Size using (Size)
+
+open import Vatras.Lang.ADT F V
+
+push-down-artifact : ∀ {i : Size} {A : 𝔸} → atoms A → List (ADT A) → ADT A
+push-down-artifact {A = A} a cs = go cs []
+  module push-down-artifact-Implementation where
+  go : ∀ {i : Size} → List (ADT A) → List (V A) → ADT A
+  go [] vs = leaf (a -< List.reverse vs >-)
+  go (leaf v ∷ cs) vs = go cs (v ∷ vs)
+  go (d ⟨ c₁ , c₂ ⟩ ∷ cs) vs = d ⟨ go (c₁ ∷ cs) vs , go (c₂ ∷ cs) vs ⟩
+
+⟦push-down-artifact⟧ : ∀ {i : Size} {A : 𝔸}
+  → (a : atoms A)
+  → (cs : List (ADT A))
+  → (config : Configuration)
+  → ⟦ push-down-artifact a cs ⟧ config ≡ a -< List.map (λ e → ⟦ e ⟧ config) cs >-
+⟦push-down-artifact⟧ {A = A} a cs config = go' cs []
+  where
+  open push-down-artifact-Implementation
+
+  go' : ∀ {i : Size}
+    → (cs' : List (ADT A))
+    → (vs : List (V A))
+    → ⟦ go a cs cs' vs ⟧ config ≡ a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) cs' >-
+  go' [] vs = Eq.sym (Eq.cong₂ _-<_>- refl (Eq.trans (List.ʳ++-defn vs) (List.++-identityʳ (List.reverse vs))))
+  go' (leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ _-<_>- refl (List.++-ʳ++ List.[ v ] {ys = vs}))
+  go' ((d ⟨ c₁ , c₂ ⟩) ∷ cs') vs =
+      ⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config
+    ≡⟨⟩
+      (if config d
+        then ⟦ go a cs (c₁ ∷ cs') vs ⟧ config
+        else ⟦ go a cs (c₂ ∷ cs') vs ⟧ config)
+    ≡⟨ Eq.cong₂ (if config d then_else_) (go' (c₁ ∷ cs') vs) (go' (c₂ ∷ cs') vs) ⟩
+      (if config d
+        then a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (c₁ ∷ cs') >-
+        else a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (c₂ ∷ cs') >-)
+    ≡⟨ Bool.if-float (λ c → a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (c ∷ cs') >-) (config d) ⟨
+      a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs') >-
+    ≡⟨⟩
+      a -< vs ʳ++ ⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → ⟦ e ⟧ config) cs' >-
+    ≡⟨ Eq.cong₂ _-<_>- refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.if-float (λ e → ⟦ e ⟧ config) (config d)) refl)) ⟩
+      a -< vs ʳ++ (if config d then ⟦ c₁ ⟧ config else ⟦ c₂ ⟧ config) ∷ List.map (λ e → ⟦ e ⟧ config) cs' >-
+    ≡⟨⟩
+      a -< vs ʳ++ ⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → ⟦ e ⟧ config) cs' >-
+    ≡⟨⟩
+      a -< vs ʳ++ List.map (λ e → ⟦ e ⟧ config) (d ⟨ c₁ , c₂ ⟩ ∷ cs') >-
+    ∎