Merge pull request #35 from pmbittner/translate-from-FST

Translate FST to VariantList and disprove translation to OC

Author: ibbem

src/Framework/Variants.agda

@@ -10,7 +10,7 @@ open import Size using (Size; ↑_; ∞)
 
 open import Framework.Definitions using (𝕍; 𝔸; atoms)
 open import Framework.VariabilityLanguage
-open import Construct.Artifact as At using (_-<_>-; map-children) renaming (Syntax to Artifact; Construct to ArtifactC)
+open import Construct.Artifact as At using (map-children) renaming (Syntax to Artifact; Construct to ArtifactC)
 
 open import Data.EqIndexedSet
 
@@ -24,6 +24,8 @@ data Rose : Size → 𝕍 where
 rose-leaf : ∀ {A : 𝔸} → atoms A → Rose ∞ A
 rose-leaf {A} a = rose (At.leaf a)
 
+pattern _-<_>- a cs = rose (a At.-< cs >-)
+
 -- Variants are also variability languages
 Variant-is-VL : ∀ (V : 𝕍) → VariabilityLanguage V
 Variant-is-VL V = ⟪ V , ⊤ , (λ e c → e) ⟫
@@ -33,7 +35,7 @@ open import Data.Maybe using (nothing; just)
 open import Relation.Binary.PropositionalEquality as Peq using (_≡_; _≗_; refl)
 open Peq.≡-Reasoning
 
-children-equality : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → rose (a₁ -< cs₁ >-) ≡ rose (a₂ -< cs₂ >-) → cs₁ ≡ cs₂
+children-equality : ∀ {A : 𝔸} {a₁ a₂ : atoms A} {cs₁ cs₂ : List (Rose ∞ A)} → a₁ -< cs₁ >- ≡ a₂ -< cs₂ >- → cs₁ ≡ cs₂
 children-equality refl = refl
 
 Artifact∈ₛRose : Artifact ∈ₛ Rose ∞
@@ -49,8 +51,8 @@ RoseVL = Variant-is-VL (Rose ∞)
 
 open import Data.String using (String; _++_; intersperse)
 show-rose : ∀ {i} {A} → (atoms A → String) → Rose i A → String
-show-rose show-a (rose (a -< [] >-)) = show-a a
-show-rose show-a (rose (a -< es@(_ ∷ _) >-)) = show-a a ++ "-<" ++ (intersperse ", " (map (show-rose show-a) es)) ++ ">-"
+show-rose show-a (a -< [] >-) = show-a a
+show-rose show-a (a -< es@(_ ∷ _) >-) = show-a a ++ "-<" ++ (intersperse ", " (map (show-rose show-a) es)) ++ ">-"
 
 
 -- Variants can be encoded into other variability language.
@@ -123,24 +125,24 @@ rose-encoder Γ has c = record
       ⟦_⟧ₚ = pcong ArtifactC Γ
 
       h : ∀ (v : Rose ∞ A) (j : Config Γ) → ⟦ t v ⟧ j ≡ v
-      h (rose (a -< cs >-)) j =
+      h (rose (a At.-< cs >-)) j =
         begin
-          ⟦ cons (C∈ₛΓ has) (map-children t (a -< cs >-)) ⟧ j
-        ≡⟨ resistant has (map-children t (a -< cs >-)) j ⟩
-          (cons (C∈ₛV has) ∘ ⟦ map-children t (a -< cs >-)⟧ₚ) j
+          ⟦ cons (C∈ₛΓ has) (map-children t (a At.-< cs >-)) ⟧ j
+        ≡⟨ resistant has (map-children t (a At.-< cs >-)) j ⟩
+          (cons (C∈ₛV has) ∘ ⟦ map-children t (a At.-< cs >-)⟧ₚ) j
         ≡⟨⟩
-          cons (C∈ₛV has) (⟦ map-children t (a -< cs >-) ⟧ₚ j)
+          cons (C∈ₛV has) (⟦ map-children t (a At.-< cs >-) ⟧ₚ j)
         ≡⟨⟩
-          (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (map-children t (a -< cs >-))
+          (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (map-children t (a At.-< cs >-))
         ≡⟨⟩
-          (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (a -< map t cs >-)
-        -- ≡⟨ Peq.cong (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (Peq.cong (a -<_>-) {!!}) ⟩
-          -- (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (a -< cs >-)
+          (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (a At.-< map t cs >-)
+        -- ≡⟨ Peq.cong (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (Peq.cong (a At.-<_>-) {!!}) ⟩
+          -- (cons (C∈ₛV has) ∘ flip ⟦_⟧ₚ j) (a At.-< cs >-)
         ≡⟨ {!!} ⟩
         -- ≡⟨ bar _ ⟩
-          -- rose            (pcong ArtifactC Γ (a -< map t cs >-) j)
-        -- ≡⟨ Peq.cong rose {!preservation ppp (a -< map t cs >-)!} ⟩
-          rose (a -< cs >-)
+          -- rose            (pcong ArtifactC Γ (a At.-< map t cs >-) j)
+        -- ≡⟨ Peq.cong rose {!preservation ppp (a At.-< map t cs >-)!} ⟩
+          rose (a At.-< cs >-)
         ∎
         where
           module _ where
@@ -150,8 +152,8 @@ rose-encoder Γ has c = record
 
             -- unprovable
             -- Imagine our domain A is pairs (a , b)
-            -- Then cons could take an '(a , b) -< cs >-'
-            -- and encode it as a 'rose ((b , a) -< cs >-)'
+            -- Then cons could take an '(a , b) At.-< cs >-'
+            -- and encode it as a 'rose ((b , a) At.-< cs >-)'
             -- for which exists an inverse snoc that just has
             -- to swap the arguments in the pair again.
             -- So we need a stronger axiom here that syntax
@@ -163,8 +165,8 @@ rose-encoder Γ has c = record
             sno : oc ∘ rose ≗ just
             sno a rewrite Peq.sym (bar a) = id-l (C∈ₛV has) a
 
-            foo : co (a -< cs >-) ≡ rose (a -< cs >-)
-            foo = bar (a -< cs >-)
+            foo : co (a At.-< cs >-) ≡ rose (a At.-< cs >-)
+            foo = bar (a At.-< cs >-)
 
       -- lp : ∀ (e : Rose ∞ A) → ⟦ e ⟧ᵥ ⊆[ confi ] ⟦ t e ⟧
       -- lp (rose x) i =

src/Lang/All/Generic.agda

@@ -1,9 +1,13 @@
-open import Framework.Definitions using (𝕍)
+open import Framework.Definitions using (𝕍; 𝔽; 𝔸)
 open import Framework.Construct using (_∈ₛ_)
 open import Construct.Artifact using () renaming (Syntax to Artifact)
 
 module Lang.All.Generic (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
+open import Size using (∞)
+
+open import Framework.Variants using (Rose)
+
 module VariantList where
   open import Lang.VariantList Variant public
 
@@ -30,4 +34,9 @@ module OC where
   open Lang.OC.Sem Variant Artifact∈ₛVariant public
 
 module FST where
-  open import Lang.FST renaming (FSTL-Sem to ⟦_⟧) public
+  open import Lang.FST hiding (FST; FSTL-Sem; Conf) public
+
+  Configuration = Lang.FST.Conf
+
+  ⟦_⟧ : ∀ {F : 𝔽} {A : 𝔸} → Impose.SPL F A → Configuration F → Rose ∞ A
+  ⟦_⟧ {F} = Lang.FST.FSTL-Sem F

src/Lang/FST.agda

@@ -33,11 +33,11 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 open Eq.≡-Reasoning
 
 open import Framework.Annotation.Name using (Name)
-open import Framework.Variants using (Rose; rose; rose-leaf; children-equality)
+open import Framework.Variants using (Rose; _-<_>-; rose-leaf; children-equality)
 open import Framework.Composition.FeatureAlgebra
 open import Framework.VariabilityLanguage
 open import Framework.VariantMap using (VMap)
-open import Construct.Artifact as At using ()
+import Construct.Artifact as At
 open import Framework.Properties.Completeness using (Incomplete)
 
 Conf : Set
@@ -53,7 +53,6 @@ open TODO-MOVE-TO-AUX-OR-USE-STL
 FST : Size → 𝔼
 FST i = Rose i
 
-pattern _-<_>- a cs = rose (a At.-< cs >-)
 fst-leaf = rose-leaf
 
 induction : ∀ {A : 𝔸} {B : Set} → (atoms A → List B → B) → FST ∞ A → B
@@ -505,7 +504,7 @@ module IncompleteOnRose where
   FST-is-incomplete complete with complete variants-0-and-1
   FST-is-incomplete complete | e , e⊆vs , vs⊆e = does-not-describe-variants-0-and-1 e (e⊆vs zero) (e⊆vs (suc zero))
 
-cannotEncodeNeighbors : ∀ {A : 𝔸} (a b : atoms A) → ∄[ e ] (∃[ c ] FSTL-Sem e c ≡ rose (a At.-< rose-leaf b ∷ rose-leaf b ∷ [] >-))
+cannotEncodeNeighbors : ∀ {A : 𝔸} (a b : atoms A) → ∄[ e ] (∃[ c ] FSTL-Sem e c ≡ a -< rose-leaf b ∷ rose-leaf b ∷ [] >-)
 cannotEncodeNeighbors {A} a b (e , conf , ⟦e⟧c≡neighbors) =
   ¬Unique b (Eq.subst (λ l → Unique l) (children-equality ⟦e⟧c≡neighbors) (lemma (⊛-all (select conf (features e)))))
   where

src/Lang/OC.lagda.md

@@ -22,7 +22,7 @@ open import Data.String as String using (String)
 open import Size using (Size; ∞; ↑_)
 open import Function using (_∘_)
 
-open import Framework.Variants
+open import Framework.Variants hiding (_-<_>-)
 open import Framework.VariabilityLanguage
 open import Framework.Construct
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)

src/Lang/OC/Alternative.agda

@@ -0,0 +1,45 @@
+module Lang.OC.Alternative where
+
+open import Data.List using (List; []; _∷_)
+open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
+open import Data.Bool using (true; false)
+open import Data.Nat using (zero; suc; _≟_; ℕ)
+open import Data.List.Relation.Binary.Sublist.Heterogeneous using (Sublist; _∷_; _∷ʳ_)
+open import Data.Product using (_,_; ∃-syntax)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Size using (∞)
+
+open import Framework.Definitions using (𝔽; 𝔸; atoms)
+open import Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality)
+open import Lang.All
+open OC using (WFOC; Root; all-oc)
+open import Lang.OC.Subtree using (Subtree; subtrees; subtreeₒ-recurse)
+
+A : 𝔸
+A = ℕ , _≟_
+
+cannotEncodeAlternative : ∀ {F : 𝔽}
+  → (e : WFOC F ∞ A)
+  → (∃[ c ] zero -< rose-leaf      zero  ∷ [] >- ≡ OC.⟦ e ⟧ c)
+  → (∃[ c ] zero -< rose-leaf (suc zero) ∷ [] >- ≡ OC.⟦ e ⟧ c)
+  → (zero -< [] >- ≡ OC.⟦ e ⟧ (all-oc false))
+  → Subtree (zero -< rose-leaf zero ∷ rose-leaf (suc zero) ∷ [] >-) (OC.⟦ e ⟧ (all-oc true))
+  ⊎ Subtree (zero -< rose-leaf (suc zero) ∷ rose-leaf zero ∷ [] >-) (OC.⟦ e ⟧ (all-oc true))
+cannotEncodeAlternative e@(Root zero cs) p₁ p₂ p₃ = Sum.map subtrees subtrees (mergeSubtrees' (sublist p₁) (sublist p₂))
+  where
+  sublist : ∀ {a : atoms A} {v : Rose ∞ A} → (∃[ c ] a -< v ∷ [] >- ≡ OC.⟦ e ⟧ c) → Sublist Subtree (v ∷ []) (OC.⟦ cs ⟧ₒ-recurse (all-oc true))
+  sublist (c₁ , p₁) =
+    Eq.subst
+      (λ cs' → Sublist Subtree cs' (OC.⟦ cs ⟧ₒ-recurse (all-oc true)))
+      (children-equality (Eq.sym p₁))
+      (subtreeₒ-recurse cs c₁ (all-oc true) (λ f p → refl))
+
+  mergeSubtrees' : ∀ {cs : List (Rose ∞ A)}
+    → Sublist Subtree (rose-leaf zero ∷ []) cs
+    → Sublist Subtree (rose-leaf (suc zero) ∷ []) cs
+    → Sublist Subtree (rose-leaf zero ∷ rose-leaf (suc zero) ∷ []) cs
+    ⊎ Sublist Subtree (rose-leaf (suc zero) ∷ rose-leaf zero ∷ []) cs
+  mergeSubtrees' (a ∷ʳ as₁) (.a ∷ʳ as₂) = Sum.map (a ∷ʳ_) (a ∷ʳ_) (mergeSubtrees' as₁ as₂)
+  mergeSubtrees' (a₁ ∷ʳ as₁) (p₂ ∷ as₂) = inj₂ (p₂ ∷ as₁)
+  mergeSubtrees' (p₁ ∷ as₁) (a₂ ∷ʳ as₂) = inj₁ (p₁ ∷ as₂)
+  mergeSubtrees' (subtrees v ∷ as₁) (() ∷ as₂)

src/Lang/OC/Properties.agda

@@ -0,0 +1,16 @@
+module Lang.OC.Properties where
+
+open import Data.Bool using (true)
+open import Data.Maybe using (just)
+open import Data.Product using (_,_; ∃-syntax)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Size using (∞)
+
+open import Framework.Definitions using (𝔽; 𝔸)
+import Framework.Variants as V
+open import Lang.All
+open OC using (OC; _-<_>-; _❲_❳; ⟦_⟧ₒ; ⟦_⟧ₒ-recurse; all-oc)
+
+⟦e⟧ₒtrue≡just : ∀ {F : 𝔽} {A : 𝔸} (e : OC F ∞ A) → ∃[ v ] ⟦ e ⟧ₒ (all-oc true) ≡ just v
+⟦e⟧ₒtrue≡just (a -< cs >-) = a V.-< ⟦ cs ⟧ₒ-recurse (all-oc true) >- , refl
+⟦e⟧ₒtrue≡just (f ❲ e ❳) = ⟦e⟧ₒtrue≡just e

src/Lang/OC/Subtree.lagda.md

@@ -0,0 +1,84 @@
+```agda
+module Lang.OC.Subtree where
+
+open import Data.Bool using (true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List using (List; []; _∷_)
+open import Data.List.Relation.Binary.Sublist.Heterogeneous using (Sublist; []; _∷_; _∷ʳ_)
+open import Data.Maybe using (Maybe; nothing; just)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
+open import Size using (∞)
+
+open import Framework.Definitions using (𝔽; 𝔸; atoms)
+open import Framework.Variants as V hiding (_-<_>-)
+open import Lang.OC
+open Sem (Rose ∞) Artifact∈ₛRose
+open import Util.AuxProofs using (true≢false)
+```
+
+Relates two variants iff the first argument is a subtree of the second argument.
+In other words: if some artifacts (including all their children) can be removed
+from the second variant to obtain the first variant exactly.
+```agda
+data Subtree {A : 𝔸} : Rose ∞ A → Rose ∞ A → Set₁ where
+  subtrees : {a : atoms A} → {cs₁ cs₂ : List (Rose ∞ A)} → Sublist Subtree cs₁ cs₂ → Subtree (a V.-< cs₁ >-) (a V.-< cs₂ >-)
+```
+
+Relates two optional variants using `Subtree`. This is mostly useful for
+relating `⟦_⟧ₒ` whereas `Subtree` is mostly used to relate `⟦_⟧`. It has the
+same semantics as `Subtree` but allows for the removal of the root artifact,
+which is fixed in `Subtree`.
+```agda
+data MaybeSubtree {A : 𝔸} : Maybe (Rose ∞ A) → Maybe (Rose ∞ A) → Set₁ where
+  neither : MaybeSubtree nothing nothing
+  one : {c : Rose ∞ A} → MaybeSubtree nothing (just c)
+  both : {c₁ c₂ : Rose ∞ A} → Subtree c₁ c₂ → MaybeSubtree (just c₁) (just c₂)
+```
+
+```agda
+Implies : {F : 𝔽} → Configuration F → Configuration F → Set
+Implies {F} c₁ c₂ = (f : F) → c₁ f ≡ true → c₂ f ≡ true
+```
+
+If two configurations are related, their variants are also related. This result
+is enabled by the fact that OC cannot encode alternatives but only include or
+exclude subtrees. Hence, a subtree present in `c₂` can be removed, without any
+accidental additions anywhere in the variant, by configuring an option above it
+to `false` in `c₁`. However, the reverse is ruled out by the `Implies`
+assumption.
+
+The following lemmas require mutual recursion because they are properties about
+functions (`⟦_⟧ₒ` and `⟦_⟧ₒ-recurse`) which are also defined mutually recursive.
+```agda
+mutual
+  subtreeₒ : ∀ {F : 𝔽} {A : 𝔸} → (e : OC F ∞ A) → (c₁ c₂ : Configuration F) → Implies c₁ c₂ → MaybeSubtree (⟦ e ⟧ₒ c₁) (⟦ e ⟧ₒ c₂)
+  subtreeₒ (a -< cs >-) c₁ c₂ c₁-implies-c₂ = both (subtrees (subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂))
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ with c₁ f in c₁-f | c₂ f in c₂-f
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | false | false = neither
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | false | true with ⟦ c ⟧ₒ c₂
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | false | true | just _ = one
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | false | true | nothing = neither
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | true | false = ⊥-elim (true≢false refl (Eq.trans (Eq.sym (c₁-implies-c₂ f c₁-f)) c₂-f))
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | true | true with ⟦ c ⟧ₒ c₁ | ⟦ c ⟧ₒ c₂ | subtreeₒ c c₁ c₂ c₁-implies-c₂
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | true | true | .nothing | .nothing | neither = neither
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | true | true | .nothing | .(just _) | one = one
+  subtreeₒ (f ❲ c ❳) c₁ c₂ c₁-implies-c₂ | true | true | .(just _) | .(just _) | both p = both p
+```
+
+From `subtreeₒ`, we know that `map (λ c → ⟦ c ⟧ₒ c₁)` can produce `nothing`s
+instead of `just`s at some outputs of `map (λ c → ⟦ c ⟧ₒ c₂)`. All other
+elements must be the same. Hence, `catMaybes` results in a sublist.
+```agda
+  subtreeₒ-recurse : ∀ {F : 𝔽} {A : 𝔸} → (cs : List (OC F ∞ A)) → (c₁ c₂ : Configuration F) → Implies c₁ c₂ → Sublist Subtree (⟦ cs ⟧ₒ-recurse c₁) (⟦ cs ⟧ₒ-recurse c₂)
+  subtreeₒ-recurse [] c₁ c₂ c₁-implies-c₂ = []
+  subtreeₒ-recurse (c ∷ cs) c₁ c₂ c₁-implies-c₂ with ⟦ c ⟧ₒ c₁ | ⟦ c ⟧ₒ c₂ | subtreeₒ c c₁ c₂ c₁-implies-c₂
+  ... | .nothing | .nothing | neither = subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂
+  ... | .nothing | just c' | one = c' ∷ʳ subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂
+  ... | .(just _) | .(just _) | both p = p ∷ subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂
+```
+
+This theorem still holds if we guarantee that there is an artifact at the root.
+```agda
+subtree : ∀ {F : 𝔽} {A : 𝔸} → (e : WFOC F ∞ A) → (c₁ c₂ : Configuration F) → Implies c₁ c₂ → Subtree (⟦ e ⟧ c₁) (⟦ e ⟧ c₂)
+subtree {F} {A} (Root a cs) c₁ c₂ c₁-implies-c₂ = subtrees (subtreeₒ-recurse cs c₁ c₂ c₁-implies-c₂)
+```