diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda index 1f9b5b69..ba2a8e02 100644 --- a/src/Framework/Variants.agda +++ b/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 = diff --git a/src/Lang/All/Generic.agda b/src/Lang/All/Generic.agda index c7beb0ec..8fb70478 100644 --- a/src/Lang/All/Generic.agda +++ b/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 diff --git a/src/Lang/FST.agda b/src/Lang/FST.agda index 8002b46a..9a8cbbe3 100644 --- a/src/Lang/FST.agda +++ b/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 diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md index 29313f8c..582bc7f0 100644 --- a/src/Lang/OC.lagda.md +++ b/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) diff --git a/src/Lang/OC/Alternative.agda b/src/Lang/OC/Alternative.agda new file mode 100644 index 00000000..6314129d --- /dev/null +++ b/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₂) diff --git a/src/Lang/OC/Properties.agda b/src/Lang/OC/Properties.agda new file mode 100644 index 00000000..349a57ea --- /dev/null +++ b/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 diff --git a/src/Lang/OC/Subtree.lagda.md b/src/Lang/OC/Subtree.lagda.md new file mode 100644 index 00000000..8c6d6421 --- /dev/null +++ b/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₂) +``` diff --git a/src/Translation/Lang/FST-to-OC.agda b/src/Translation/Lang/FST-to-OC.agda deleted file mode 100644 index 7e77e072..00000000 --- a/src/Translation/Lang/FST-to-OC.agda +++ /dev/null @@ -1,118 +0,0 @@ -open import Framework.Definitions -module Translation.Lang.FST-to-OC (F : 𝔽) where - -open import Size using (Size; ↑_; _⊔ˢ_; ∞) - -open import Data.Nat using (_≟_) -open import Data.List using (List; []; _∷_; map) -open import Data.Product using (_,_) -open import Relation.Nullary.Decidable using (yes; no; _because_; False) -open import Relation.Binary using (Decidable; DecidableEquality; Rel) -open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) - -open import Framework.Variants using (Rose; rose; Artifact∈ₛRose; rose-leaf) - -V = Rose ∞ -mkArtifact = Artifact∈ₛRose -Option = F - -open import Framework.Relation.Expressiveness V - -open import Framework.VariabilityLanguage -open import Construct.Artifact as At using () -import Lang.FST as FST -open FST F using (FST; FSTL) - -data FeatureName : Set where - X : FeatureName - Y : FeatureName - -open import Data.Bool using (true; false; if_then_else_) -open import Data.Nat using (zero; suc; ℕ) -open import Data.Fin using (Fin; zero; suc) -open import Data.List.Relation.Unary.All using (All; []; _∷_) -open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) -open import Framework.VariantMap V (ℕ , _≟_) - -import Lang.All -open Lang.All.OC using (OC; _❲_❳; WFOC; Root; opt; Configuration; ⟦_⟧; WFOCL) - -AtomSet : 𝔸 -AtomSet = ℕ , _≟_ - -open FST FeatureName using (_．_) -open FST.Impose FeatureName AtomSet using (SPL; _◀_; _::_; _⊚_) renaming (⟦_⟧ to FST⟦_⟧) - -open import Data.EqIndexedSet -open import Data.Empty using (⊥-elim) - -open import Data.Product using (_,_; ∃-syntax) -open import Util.Existence using (¬Σ-syntax) - -counterexample : VMap 3 -counterexample zero = rose-leaf 0 -counterexample (suc zero) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ [] >-) ∷ [] >-) -counterexample (suc (suc zero)) = rose (0 At.-< rose (1 At.-< rose-leaf 3 ∷ [] >-) ∷ [] >-) -counterexample (suc (suc (suc zero))) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ rose-leaf 3 ∷ [] >-) ∷ [] >-) - -open import Relation.Nullary.Negation using (¬_) - - -illegal : ∀ {i : Size} → ∄[ e ∈ WFOC FeatureName i AtomSet ] (⟦ e ⟧ ≅ counterexample) --- root must be zero because it is always zero in counterexample -illegal (Root (suc i) cs , _ , ⊇) with ⊇ zero -... | () --- there must be a child because there are variants in counterexample with children below the root (e.g., suc zero) -illegal (Root zero [] , _ , ⊇) with ⊇ (suc zero) -- illegal' (cs , eq) -... | () --- there must be an option at the front because there are variants with zero children (e.g., zero) -illegal (Root zero (a OC.-< cs >- ∷ _) , _ , ⊇) with ⊇ zero -... | () --- there can not be any other children -illegal (Root zero (O ❲ e ❳ ∷ a OC.-< as >- ∷ xs) , ⊆ , ⊇) = {!!} -illegal (Root zero (O ❲ e ❳ ∷ P OC.❲ e' ❳ ∷ xs) , ⊆ , ⊇) = {!!} --- e can be a chain of options but somewhen, there must be an artifact -illegal (Root zero (O ❲ e ❳ ∷ []) , ⊆ , ⊇) = {!!} ---illegal' (e , (O , xs , (⊆ , ⊇))) - -cef : SPL -cef = 0 ◀ ( - (X :: (1 ． 2 ． []) ⊚ ([] ∷ [] , ([] ∷ [] , ([] , []) ∷ []) ∷ [])) ∷ - (Y :: (1 ． 3 ． []) ⊚ ([] ∷ [] , ([] ∷ [] , ([] , []) ∷ []) ∷ [])) ∷ - []) - -cef-describes-counterexample : FST⟦ cef ⟧ ≅ counterexample -cef-describes-counterexample = ⊆[]→⊆ cef-⊆[] , ⊆[]→⊆ {f = fnoc} cef-⊇[] - where - conf : FST.Conf FeatureName → Fin 4 - conf c with c X | c Y - ... | false | false = zero - ... | false | true = suc (suc zero) - ... | true | false = suc zero - ... | true | true = suc (suc (suc zero)) - - cef-⊆[] : FST⟦ cef ⟧ ⊆[ conf ] counterexample - cef-⊆[] c with c X | c Y - ... | false | false = refl - ... | false | true = refl - ... | true | false = refl - ... | true | true = {!!} - - fnoc : Fin 4 → FST.Conf FeatureName - fnoc zero X = false - fnoc zero Y = false - fnoc (suc zero) X = true - fnoc (suc zero) Y = false - fnoc (suc (suc zero)) X = false - fnoc (suc (suc zero)) Y = true - fnoc (suc (suc (suc zero))) X = true - fnoc (suc (suc (suc zero))) Y = true - - cef-⊇[] : counterexample ⊆[ fnoc ] FST⟦ cef ⟧ - cef-⊇[] zero = refl - cef-⊇[] (suc zero) = refl - cef-⊇[] (suc (suc zero)) = refl - cef-⊇[] (suc (suc (suc zero))) = {!!} - -ouch : WFOCL FeatureName ⋡ FSTL -ouch sure = {!!} diff --git a/src/Translation/Lang/FST-to-OC.lagda.md b/src/Translation/Lang/FST-to-OC.lagda.md new file mode 100644 index 00000000..0624c10b --- /dev/null +++ b/src/Translation/Lang/FST-to-OC.lagda.md @@ -0,0 +1,328 @@ +# Option calculus is not as expressive as feature structure trees + +```agda +open import Framework.Definitions using (𝔽; 𝔸; atoms) +open import Relation.Binary using (DecidableEquality) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl) + +``` + +## Assumptions and Imports + +To be as general as possible, we do not fix `F` but only require that it +contains at least two distinct features `f₁` and `f₂`. To implement +configurations, equality in `F` nees to be decidable, so `==ꟳ` is also required. +```agda +module Translation.Lang.FST-to-OC {F : 𝔽} (f₁ f₂ : F) (f₁≢f₂ : f₁ ≢ f₂) (_==ꟳ_ : DecidableEquality F) where + +open import Size using (∞) +open import Data.Bool as Bool using (true; false) +import Data.Bool.Properties as Bool +open import Data.Empty using (⊥; ⊥-elim) +open import Data.List as List using (List; []; _∷_; length; catMaybes) +open import Data.List.Properties as List +open import Data.List.Relation.Binary.Sublist.Heterogeneous using ([]; _∷_; _∷ʳ_) +open import Data.List.Relation.Unary.All using ([]; _∷_) +open import Data.List.Relation.Unary.AllPairs using ([]; _∷_) +open import Data.Maybe using (nothing; just) +open import Data.Nat using (_≟_; ℕ; _+_; _≤_; z≤n; s≤s) +import Data.Nat.Properties as ℕ +open import Data.Product using (_,_; ∃-syntax) +open import Data.Sum as Sum using (_⊎_; inj₁; inj₂) +open import Function using (flip) +open import Relation.Nullary using (yes; no) + +open Eq.≡-Reasoning + +open import Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality) +import Construct.Plain.Artifact +open import Lang.All +open OC using (WFOCL; Root; _❲_❳; all-oc) +open import Lang.OC.Properties using (⟦e⟧ₒtrue≡just) +open import Lang.OC.Subtree using (Subtree; subtrees; both; neither; Implies; subtreeₒ; subtreeₒ-recurse) +open import Lang.FST using (FSTL-Sem) +open FST using (FSTL) +open FST.Impose + +V = Rose ∞ +open import Framework.Relation.Expressiveness V using (_⋡_) + +A : 𝔸 +A = ℕ , _≟_ +``` + +## Counter-Example + +To prove that option calculus is not at least as expressive as feature structure trees, +we construct a counter-example product line of feature structure trees that cannot be +translated to option calculus. + +The following counter-example embodies a form of an alternative, which +describes the following variants + + f₁ = true, f₂ = false: 0 -< 0 -< 0 -< [] >- ∷ [] >- ∷ [] >- + f₁ = false, f₂ = true: 0 -< 0 -< 1 -< [] >- ∷ [] >- ∷ [] >- + f₁ = false, f₂ = false: 0 -< >- ∷ [] >- + f₁ = true, f₂ = true: 0 -< 0 -< 0 -< [] >- ∷ 1 -< [] >- ∷ [] >- ∷ [] >- + +but not + + 0 -< 0 -< [] >- ∷ [] >- + +Hence, at least one inner child is required for a valid variant of +this counter-example SPL (or no children in which case there is only the root). +As FSTs require a fixed root artifact, the outermost artifact is always set to 0. +```agda +counter-example : SPL F A +counter-example = 0 ◀ ( + (f₁ :: ((0 -< 0 -< [] >- ∷ [] >- ∷ []) ⊚ ([] ∷ [] , (([] ∷ []) , (([] , []) ∷ [])) ∷ []))) + ∷ (f₂ :: ((0 -< 1 -< [] >- ∷ [] >- ∷ []) ⊚ ([] ∷ [] , (([] ∷ []) , (([] , []) ∷ [])) ∷ []))) + ∷ []) +``` + +## Proof that option calculus cannot encode the counter-example + +The idea of the following proof is to show that any OC expression, which describes +these variants, necessarily includes some other variant. We identified two cases: + +- In the `shared-artifact` case, the OC expression also includes the following + extra variant: + + 0 -< 0 -< [] >- ∷ [] >- + + which as stated above, is not described by the counter-example FST. + For example, the following OC expression has this problem: + + 0 -< 0 -< f₁ ❲ 0 -< [] >- ❳ ∷ f₂ ❲ 1 -< [] >- ❳ ∷ [] >- ∷ [] >- + +- In the `more-artifacts` case, the OC expression also includes an extra variant + like the following: + + 0 -< 0 -< 0 -< [] >- ∷ [] >- ∷ 0 -< 1 -< [] >- ∷ [] >- ∷ [] >- + For example: + + 0 -< f₁ ❲ 0 -< 0 -< [] >- ∷ [] >- ❳ ∷ f₂ ❲ 0 -< 1 -< [] >- ∷ [] >- ❳ ∷ [] >- + + Note that, in contrast to the `shared-artifact` case, this variant is not + uniquely determined. In fact, the order of the two features isn't fixed and + the configuration chosen by the proof could introduce more artifacts because + there can be options which are not selected by the configurations `c₁` and + `c₂` below. + +There are four relevant configurations for `counter-example` because it uses +exactly two features: `c₁`, `c₂`, `all-oc true` and `all-oc false`. +```agda +c₁ : FST.Configuration F +c₁ f with f ==ꟳ f₁ +c₁ f | yes f≡f₁ = true +c₁ f | no f≢f₁ = false + +c₂ : FST.Configuration F +c₂ f with f ==ꟳ f₂ +c₂ f | yes f≡f₂ = true +c₂ f | no f≢f₂ = false +``` + +In the following proofs, we will need the exact variants which can be configured +from `counter-example`. Agda can't compute with `==ꟳ` so we need the following +two lemmas to sort out invalid definitions of `==ꟳ`. Then Agda can actually +compute the semantics of `counter-example`. +```agda +compute-counter-example-c₁ : {v : Rose ∞ A} → FSTL-Sem F counter-example c₁ ≡ v → 0 -< 0 -< 0 -< [] >- ∷ [] >- ∷ [] >- ≡ v +compute-counter-example-c₁ p with f₁ ==ꟳ f₁ | f₂ ==ꟳ f₁ | c₁ f₁ in c₁-f₁ | c₁ f₂ in c₁-f₂ +compute-counter-example-c₁ p | yes f₁≡f₁ | yes f₂≡f₁ | _ | _ = ⊥-elim (f₁≢f₂ (Eq.sym f₂≡f₁)) +compute-counter-example-c₁ p | yes f₁≡f₁ | no f₂≢f₁ | true | false = p +compute-counter-example-c₁ p | no f₁≢f₁ | _ | _ | _ = ⊥-elim (f₁≢f₁ refl) + +compute-counter-example-c₂ : {v : Rose ∞ A} → FSTL-Sem F counter-example c₂ ≡ v → 0 -< 0 -< 1 -< [] >- ∷ [] >- ∷ [] >- ≡ v +compute-counter-example-c₂ p with f₁ ==ꟳ f₂ | f₂ ==ꟳ f₂ | c₂ f₁ in c₂-f₁ | c₂ f₂ in c₂-f₂ +compute-counter-example-c₂ p | yes f₁≡f₂ | _ | _ | _ = ⊥-elim (f₁≢f₂ f₁≡f₂) +compute-counter-example-c₂ p | no f₁≢f₂ | yes f₂≡f₂ | false | true = p +compute-counter-example-c₂ p | no f₁≢f₂ | no f₂≢f₂ | _ | _ = ⊥-elim (f₂≢f₂ refl) +``` + +For proving the `shared-artifact` case, we need to compute a configuration which +deselects the options guarding the inner artifacts (`0 -< [] >-` and `1 -< [] >-`) +but selects the options leading to the shared artifact surrounding these two +options. +```agda +_∧_ : {F : 𝔽} → OC.Configuration F → OC.Configuration F → OC.Configuration F +_∧_ c₁ c₂ f = c₁ f Bool.∧ c₂ f + +implies-∧₁ : {F : 𝔽} {c₁ c₂ : OC.Configuration F} → Implies (c₁ ∧ c₂) c₁ +implies-∧₁ {c₁ = c₁} f p with c₁ f +implies-∧₁ f p | true = refl + +implies-∧₂ : {F : 𝔽} {c₁ c₂ : OC.Configuration F} → Implies (c₁ ∧ c₂) c₂ +implies-∧₂ {c₁ = c₁} {c₂ = c₂} f p with c₁ f | c₂ f +implies-∧₂ f p | true | true = refl +``` + +### `shared-artifact` case + +We observe that any option calculus expression that describes +the variants `0 -< 0 >-` and `0 -< 1 >-` must also describe the +variant `0 -< >-`. + +In this case, the relevant options are contained in the same, shared, option +`e`. The goal is to prove that we can deselect all inner options and obtain this +shared artifact without any inner artifacts. + +As configuration, we chose the intersection of the two given configurations. +This ensures that all options up to the shared artifact are included because +they must be included in both variants. Simultaneously, this excludes the +artifacts themselves because each configuration excludes one of them. +```agda +shared-artifact : ∀ {F' : 𝔽} + → (e : OC.OC F' ∞ A) + → (c₁ c₂ : OC.Configuration F') + → just (0 -< rose-leaf 0 ∷ [] >-) ≡ OC.⟦ e ⟧ₒ c₁ + → just (0 -< rose-leaf 1 ∷ [] >-) ≡ OC.⟦ e ⟧ₒ c₂ + → just (0 -< [] >-) ≡ OC.⟦ e ⟧ₒ (c₁ ∧ c₂) +shared-artifact (0 OC.-< cs >-) c₁ c₂ p₁ p₂ + with OC.⟦ cs ⟧ₒ-recurse c₁ + | OC.⟦ cs ⟧ₒ-recurse c₂ + | OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) + | subtreeₒ-recurse cs (c₁ ∧ c₂) c₁ implies-∧₁ + | subtreeₒ-recurse cs (c₁ ∧ c₂) c₂ (implies-∧₂ {c₁ = c₁}) +shared-artifact (0 OC.-< cs >-) c₁ c₂ refl refl | _ | _ | [] | _ | _ = refl +shared-artifact (0 OC.-< cs >-) c₁ c₂ refl refl | _ | _ | _ ∷ _ | subtrees _ ∷ _ | () ∷ _ +shared-artifact (f OC.❲ e ❳) c₁ c₂ p₁ p₂ with c₁ f | c₂ f +shared-artifact (f OC.❲ e ❳) c₁ c₂ p₁ p₂ | true | true = shared-artifact e c₁ c₂ p₁ p₂ +``` + +### `more-artifacts` case + +In case we found a node corresponding to either `0 -< 0 -< [] >- ∷ [] >-` +or `0 -< 1 -< [] >- ∷ [] >-`, we choose the all true configuration and +prove that there is at least one more artifact in the resulting variant. + +As discussed at the definition of `counter-example`, the order of the artifact +nodes is not uniquely determined. Hence, there are two distinct cases in +`induction`, which we abstract over using the `v` argument. Moreover, we only +prove that there is one more artifact in the variant. In addition, there can be +additional options, only present in the all true configuration, which is why we +only prove that there is at least one more +artifact. +```agda +more-artifacts : ∀ {F' : 𝔽} + → (cs : List (OC.OC F' ∞ A)) + → (cₙ : OC.Configuration F') + → (v : Rose ∞ A) + → 0 -< v ∷ [] >- ∷ [] ≡ OC.⟦ cs ⟧ₒ-recurse cₙ + → 1 ≤ length (OC.⟦ cs ⟧ₒ-recurse (all-oc true)) +more-artifacts (a OC.-< cs' >- ∷ cs) cₙ v p = s≤s z≤n +more-artifacts (e@(f OC.❲ e' ❳) ∷ cs) cₙ v p with OC.⟦ e ⟧ₒ (all-oc true) | ⟦e⟧ₒtrue≡just e +more-artifacts (e@(f OC.❲ e' ❳) ∷ cs) cₙ v p | .(just _) | _ , refl = s≤s z≤n +``` + +### Putting the pieces together + +This is the main induction over the top most children of the OC expression. It +proves that there is at least one variant, configurable from an expression with +children `cs`, which is not included in our `counter-example`. For this result, +it requires two configurations which evaluate to the two alternative variants. +For simplicity, though not actually required for the final result, it also takes +a configuration showing that the semantics of the expression includes a variant +without children. This eliminates a bunch of proof cases (e.g., having an +unconditional artifact). + +The idea is to find a child which exists in at least one of the variants +configured by `c₁` or `c₂`. Hence, we do a case analysis on whether a given +option exists when evaluated with the configurations `c₁` and `c₂` (we can +rule out artifacts because `OC.⟦ cs ⟧ₒ-recurse c₃` evaluates to `[]` so there +are no unconditional artifacts in `cs`). Note that evaluating the configuration +for this option alone is not enough to guarantee that there is an artifact +because options can be nested arbitrarily deep without artifacts in between. +Hence, we almost always use a `with` clause to match on the final result of the +semantics (`OC.⟦_⟧ₒ`) + +If an option evaluates to an artifact in exactly one of the configurations, we +know there must be a second option in `cs` evaluating to an artifact in the +other configuration. In this case, called `more-artifacts`, we count the top +level child artifacts when the OC expression is evaluated using the all true +configuration. + +If an option evaluates to an artifact for both `c₁` and `c₂` it must also +evaluate to an artifact for the intersection (`_∧_`) of these configurations. +The resulting variant can't include the child artifacts of the `c₁` and `c₂` +variants forcing it to have exactly one shape. In this case, called +`shared-artifact`, we return the exact variant to which the expression evaluates +under the intersection of `c₁` and `c₂`. +```agda +induction : ∀ {F' : 𝔽} + → (cs : List (OC.OC F' ∞ A)) + → (c₁ c₂ c₃ : OC.Configuration F') + → 0 -< rose-leaf 0 ∷ [] >- ∷ [] ≡ OC.⟦ cs ⟧ₒ-recurse c₁ + → 0 -< rose-leaf 1 ∷ [] >- ∷ [] ≡ OC.⟦ cs ⟧ₒ-recurse c₂ + → [] ≡ OC.⟦ cs ⟧ₒ-recurse c₃ + → 2 ≤ length (OC.⟦ cs ⟧ₒ-recurse (all-oc true)) + ⊎ 0 -< [] >- ∷ [] ≡ OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) +induction (_ OC.-< _ >- ∷ cs) c₁ c₂ c₃ p₁ p₂ () +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ with OC.⟦ e ⟧ₒ c₁ in ⟦e⟧c₁ | OC.⟦ e ⟧ₒ c₂ in ⟦e⟧c₂ | OC.⟦ e ⟧ₒ c₃ +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing with induction cs c₁ c₂ c₃ p₁ p₂ p₃ +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing | inj₁ p with OC.⟦ e ⟧ₒ (all-oc true) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing | inj₁ p | just _ = inj₁ (ℕ.≤-trans p (ℕ.n≤1+n _)) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing | inj₁ p | nothing = inj₁ p +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing | inj₂ p with OC.⟦ e ⟧ₒ (c₁ ∧ c₂) | OC.⟦ e ⟧ₒ c₁ | subtreeₒ e (c₁ ∧ c₂) c₁ implies-∧₁ +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | nothing | nothing | inj₂ p | nothing | nothing | neither = inj₂ p +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | just _ | nothing with OC.⟦ e ⟧ₒ c₂ | ⟦e⟧c₂ | OC.⟦ e ⟧ₒ (all-oc true) | subtreeₒ e c₂ (all-oc true) (λ f p → refl) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | nothing | just _ | nothing | just _ | _ | .(just _) | both _ = inj₁ (s≤s (more-artifacts cs c₁ (rose-leaf 0) p₁)) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | nothing | nothing with OC.⟦ e ⟧ₒ c₁ | ⟦e⟧c₁ | OC.⟦ e ⟧ₒ (all-oc true) | subtreeₒ e c₁ (all-oc true) (λ f p → refl) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | nothing | nothing | just _ | _ | .(just _) | both _ = inj₁ (s≤s (more-artifacts cs c₂ (rose-leaf 1) p₂)) +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | just _ | nothing with List.∷-injectiveʳ p₁ +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | just _ | nothing | _ with OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) in ⟦cs⟧c₁∧c₂ | OC.⟦ cs ⟧ₒ-recurse c₁ | subtreeₒ-recurse cs (c₁ ∧ c₂) c₁ implies-∧₁ +induction (e@(_ OC.❲ _ ❳) ∷ cs) c₁ c₂ c₃ p₁ p₂ p₃ | just _ | just _ | nothing | _ | .[] | .[] | [] = inj₂ ( + 0 -< [] >- ∷ [] + ≡⟨ Eq.cong₂ _∷_ refl ⟦cs⟧c₁∧c₂ ⟨ + 0 -< [] >- ∷ OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) + ≡⟨⟩ + catMaybes (just (0 -< [] >-) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) + ≡⟨ Eq.cong catMaybes (Eq.cong₂ _∷_ (shared-artifact e c₁ c₂ + (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₁)) (Eq.sym ⟦e⟧c₁)) + (Eq.trans (Eq.cong just (List.∷-injectiveˡ p₂)) (Eq.sym ⟦e⟧c₂))) + refl) ⟩ + catMaybes (OC.⟦ e ⟧ₒ (c₁ ∧ c₂) ∷ List.map (flip OC.⟦_⟧ₒ (c₁ ∧ c₂)) cs) + ≡⟨⟩ + OC.⟦ e ∷ cs ⟧ₒ-recurse (c₁ ∧ c₂) + ∎) +``` + +The results of the `induction` show that OC has no equivalent to the FST +expression. The proof evaluates the FST expression on all relevant +configurations which results in contradictions in every case. +```agda +impossible : ∀ {F' : 𝔽} + → (cs : List (OC.OC F' ∞ A)) + → (c₁ c₂ : OC.Configuration F') + → ((c : OC.Configuration F') → ∃[ c' ] OC.⟦ Root 0 cs ⟧ c ≡ FSTL-Sem F counter-example c') + → 2 ≤ length (OC.⟦ cs ⟧ₒ-recurse (all-oc true)) + ⊎ 0 -< [] >- ∷ [] ≡ OC.⟦ cs ⟧ₒ-recurse (c₁ ∧ c₂) + → ⊥ +impossible cs c₁ c₂ alternative⊆e (inj₁ p) with alternative⊆e (all-oc true) +impossible cs c₁ c₂ alternative⊆e (inj₁ p) | c' , e' with OC.⟦ cs ⟧ₒ-recurse (all-oc true) | c' f₁ | c' f₂ +impossible cs c₁ c₂ alternative⊆e (inj₁ (s≤s ())) | c' , e' | _ ∷ [] | _ | _ +impossible cs c₁ c₂ alternative⊆e (inj₁ p) | c' , () | _ ∷ _ ∷ _ | false | false +impossible cs c₁ c₂ alternative⊆e (inj₁ p) | c' , () | _ ∷ _ ∷ _ | false | true +impossible cs c₁ c₂ alternative⊆e (inj₁ p) | c' , () | _ ∷ _ ∷ _ | true | false +impossible cs c₁ c₂ alternative⊆e (inj₁ p) | c' , () | _ ∷ _ ∷ _ | true | true +impossible cs c₁ c₂ alternative⊆e (inj₂ p) with alternative⊆e (c₁ ∧ c₂) +impossible cs c₁ c₂ alternative⊆e (inj₂ p) | c' , e' with c' f₁ | c' f₂ | Eq.trans (Eq.cong (0 -<_>-) p) e' +impossible cs c₁ c₂ alternative⊆e (inj₂ p) | c' , e' | false | false | () +impossible cs c₁ c₂ alternative⊆e (inj₂ p) | c' , e' | false | true | () +impossible cs c₁ c₂ alternative⊆e (inj₂ p) | c' , e' | true | false | () +impossible cs c₁ c₂ alternative⊆e (inj₂ p) | c' , e' | true | true | () +``` + +With a little plumbing we can now conclude that there are Feature Structure +Trees (FST) with no Option Calculus (OC) equivalent. +```agda +WFOCL⋡FSTL : ∀ {F' : 𝔽} → WFOCL F' ⋡ FSTL F +WFOCL⋡FSTL WFOCL≽FSTL with WFOCL≽FSTL counter-example +WFOCL⋡FSTL WFOCL≽FSTL | Root a cs , e⊆alternative , alternative⊆e with e⊆alternative c₁ | e⊆alternative c₂ | e⊆alternative (λ _ → false) +WFOCL⋡FSTL {F'} WFOCL≽FSTL | Root 0 cs , e⊆alternative , alternative⊆e | (c₁ , p₁) | (c₂ , p₂) | (c₃ , p₃) = + impossible cs c₁ c₂ alternative⊆e + (induction cs c₁ c₂ c₃ (children-equality (compute-counter-example-c₁ p₁)) + (children-equality (compute-counter-example-c₂ p₂)) + (children-equality p₃)) +``` diff --git a/src/Translation/Lang/FST-to-VariantList.agda b/src/Translation/Lang/FST-to-VariantList.agda new file mode 100644 index 00000000..c3cb2790 --- /dev/null +++ b/src/Translation/Lang/FST-to-VariantList.agda @@ -0,0 +1,338 @@ +open import Framework.Definitions using (𝔽; 𝔸; atoms) +open import Relation.Binary using (DecidableEquality) + +module Translation.Lang.FST-to-VariantList (F : 𝔽) (_==ꟳ_ : DecidableEquality F) where + +open import Data.Bool using (Bool; true; false) +open import Data.Empty using (⊥-elim) +open import Data.List as List using (List; []; _∷_; map) +open import Data.List.Membership.Propositional using (_∈_; mapWith∈) +open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _⁺++⁺_) +import Data.List.NonEmpty.Properties as List⁺ +import Data.List.Properties as List +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.Any using (here; there) +open import Data.Nat using (ℕ; _<_; s≤s; z≤n; _+_) +import Data.Nat.Properties as ℕ +open import Data.Product using (_,_) +open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≢_; _≗_) +open import Relation.Nullary.Decidable using (yes; no) +open import Size using (∞) + +import Data.EqIndexedSet as IndexedSet +open import Framework.Compiler using (LanguageCompiler) +import Framework.Relation.Expressiveness +open import Framework.Relation.Function using (from; to) +open import Framework.Variants using (Rose; _-<_>-) +open import Util.List using (find-or-last; map-find-or-last; find-or-last-prepend-+; find-or-last-append) + +open Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) +open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) + +open import Lang.All +open FST using (FSTL) +open FST.Impose using (SPL; Feature) +module Impose {F} {A} = FST.Impose F A +open Impose using (_◀_; _::_; name; select; forget-uniqueness; ⊛-all) +open VariantList using (VariantList; VariantListL) + +config-with : Bool → F → FST.Configuration F → FST.Configuration F +config-with value f c f' with f ==ꟳ f' +config-with value f c f' | yes _ = value +config-with value f c f' | no _ = c f' + +{-| +Given a list of feature names, +generates all possible configurations. +If there are no features, a single configuration deselecting all features +will be returned as a base case. +Beware that the size of the returned list is 2^(length l) where +l is the input list of features. +-} +configs : List F → List⁺ (FST.Configuration F) +configs [] = (λ _ → false) ∷ [] +configs (f ∷ fs) = List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs) + +{-| +Translates a feature-based product line into a variant list +by enumerating all possible configurations and then deriving +all possible variants. +A crucial observation is that each index in the list is associated to +exactly one unique configuration _and_ its respective, not neccessarily unique, variant. +(conf and fnoc below rely on exactly this correspondence.) +-} +translate : ∀ {A : 𝔸} → SPL F A → VariantList A +translate {A} (a ◀ fs) = List⁺.map (λ c → FST.⟦ a ◀ fs ⟧ c) (configs (map name fs)) + +conf' : FST.Configuration F → List F → ℕ +conf' c [] = 0 +conf' c (f ∷ fs) with c f +conf' c (f ∷ fs) | true = List⁺.length (configs fs) + conf' c fs +conf' c (f ∷ fs) | false = conf' c fs + +{-| +Translates an FST configuration to a VariantList configuration +matching a feature-based SPL that was translated via the 'translate' function above. +The translation works by computing the index of the respective variant in the +resulting list, which is possible because the order of variants in the list solely +depends on the order in which configurations were generated by 'translate'. +-} +conf : ∀ {A : 𝔸} → (e : SPL F A) → FST.Configuration F → VariantList.Configuration +conf {A} (_ ◀ fs) c = conf' c (map name fs) + +{-| +Translates a VariantList configuration back to a FST configuration +matching a feature-based SPL that was translated via the 'translate' function above. +The translation works by a lookup: +An index pointing to an FST variant in the list corresponds to exactly one unique +configuration which was enumerated by the 'configs' function. +So we can just enumerate all configurations again, and then pick the configuration at +the respective index. +-} +fnoc : ∀ {A : 𝔸} → (e : SPL F A) → VariantList.Configuration → FST.Configuration F +fnoc {A} (_ ◀ fs) n = find-or-last n (configs (map name fs)) + +{-| +An index computed by conf' is always in bounds +-} +conf'- refl (Eq.cong forget-uniqueness (Eq.cong ⊛-all (go fs ps))) + where + go : (fs : List (Feature F A)) + → All (λ f → c₁ f ≡ c₂ f) (map name fs) + → select c₁ fs ≡ select c₂ fs + go [] p = refl + go ((f :: i) ∷ fs) (px ∷ p) with c₁ f | c₂ f + go ((f :: i) ∷ fs) (px ∷ p) | false | false = go fs p + go ((f :: i) ∷ fs) (px ∷ p) | true | true = Eq.cong₂ _∷_ refl (go fs p) + +preserves-⊆ : ∀ {A : 𝔸} → (e : SPL F A) → VariantList.⟦ translate e ⟧ ⊆[ fnoc e ] FST.⟦ e ⟧ +preserves-⊆ e@(a ◀ fs) c = + VariantList.⟦ translate e ⟧ c + ≡⟨⟩ + find-or-last c (translate e) + ≡⟨⟩ + find-or-last c (List⁺.map (λ c → FST.⟦ e ⟧ c) (configs (map name fs))) + ≡⟨ map-find-or-last (λ c → FST.⟦ e ⟧ c) c (configs (map name fs)) ⟨ + FST.⟦ e ⟧ (find-or-last c (configs (map name fs))) + ≡⟨⟩ + FST.⟦ e ⟧ (fnoc e c) + ∎ + where + open Eq.≡-Reasoning + +preserves-⊇ : ∀ {A : 𝔸} → (e : SPL F A) → FST.⟦ e ⟧ ⊆[ conf e ] VariantList.⟦ translate e ⟧ +preserves-⊇ e@(a ◀ fs) c = + FST.⟦ e ⟧ c + ≡⟨ ⟦⟧-cong a fs c (find-or-last (conf e c) (configs (map name fs))) (AllWith∈ (map name fs) (λ f f∈fs → Eq.sym (conf'-lemma c f (map name fs) f∈fs))) ⟩ + FST.⟦ e ⟧ (find-or-last (conf e c) (configs (map name fs))) + ≡⟨ map-find-or-last (λ c → FST.⟦ e ⟧ c) (conf e c) (configs (map name fs)) ⟩ + find-or-last (conf e c) (List⁺.map (λ c → FST.⟦ e ⟧ c) (configs (map name fs))) + ≡⟨⟩ + find-or-last (conf e c) (translate e) + ≡⟨⟩ + VariantList.⟦ translate e ⟧ (conf e c) + ∎ + where + open Eq.≡-Reasoning + +preserves : ∀ {A : 𝔸} → (e : SPL F A) → VariantList.⟦ translate e ⟧ ≅[ fnoc e ][ conf e ] FST.⟦ e ⟧ +preserves e = preserves-⊆ e , preserves-⊇ e + +FST→VariantList : LanguageCompiler (FSTL F) VariantListL +FST→VariantList .LanguageCompiler.compile = translate +FST→VariantList .LanguageCompiler.config-compiler expr .to = conf expr +FST→VariantList .LanguageCompiler.config-compiler expr .from = fnoc expr +FST→VariantList .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr) + +VariantList≽FST : VariantListL ≽ FSTL F +VariantList≽FST = expressiveness-from-compiler FST→VariantList diff --git a/src/Translation/LanguageMap.lagda.md b/src/Translation/LanguageMap.lagda.md index 8d43e8a1..86cea961 100644 --- a/src/Translation/LanguageMap.lagda.md +++ b/src/Translation/LanguageMap.lagda.md @@ -15,7 +15,7 @@ open import Data.Product using (_×_; _,_; proj₁; proj₂) open import Function using (_∘_; id) open import Size using (∞) open import Relation.Binary using (DecidableEquality) -open import Relation.Binary.PropositionalEquality as Eq using (_≗_) +open import Relation.Binary.PropositionalEquality as Eq using (_≢_; _≗_) open import Relation.Nullary.Negation using (¬_) open import Framework.Variants using (Rose; Artifact∈ₛRose; Variant-is-VL) @@ -36,7 +36,7 @@ open import Util.AuxProofs using (decidableEquality-×) open import Construct.Artifact as At using () renaming (Syntax to Artifact) open import Lang.All -open VariantList using (VariantListL; VariantList-is-Complete; VariantList-is-Sound) +open VariantList using (VariantListL) open CCC using (CCCL) open NCC using (NCCL) open 2CC using (2CCL) @@ -67,6 +67,8 @@ import Translation.Lang.ADT-to-NADT Variant mkArtifact as ADT-to-NADT import Translation.Lang.NADT-to-CCC Variant mkArtifact as NADT-to-CCC import Translation.Lang.OC-to-2CC as OC-to-2CC import Translation.Lang.OC-to-FST as OC-to-FST +import Translation.Lang.FST-to-OC as FST-to-OC +import Translation.Lang.FST-to-VariantList as FST-to-VariantList ``` @@ -116,6 +118,13 @@ module _ {F : 𝔽} where open OC-to-2CC F using (OC→2CC) public ``` +## Feature Structure Trees vs Variant Lists + +```agda +module _ {F : 𝔽} (_==_ : DecidableEquality F) where + open FST-to-VariantList F _==_ using (FST→VariantList) public +``` + ## Expressiveness @@ -186,6 +195,9 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) VariantList≽ADT : (_==_ : DecidableEquality F) → VariantListL ≽ ADTL Variant F VariantList≽ADT _==_ = ADT-to-VariantList.VariantList≽ADT F Variant _==_ + VariantList≽FST : (_==_ : DecidableEquality F) → VariantListL ≽ FSTL F + VariantList≽FST _==_ = FST-to-VariantList.VariantList≽FST F _==_ + CCC≽VariantList : F → CCCL F ≽ VariantListL CCC≽VariantList D = VariantList-to-CCC.Translate.CCC≽VariantList F D Variant mkArtifact CCC-Rose-encoder @@ -198,6 +210,9 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) 2CC≽OC : 2CCL F ≽ WFOCL F 2CC≽OC = OC-to-2CC.2CC≽OC F + 2CC≽FST : F → (_==_ : DecidableEquality F) → 2CCL F ≽ FSTL F + 2CC≽FST D _==_ = ≽-trans 2CC≽CCC (≽-trans (CCC≽VariantList D) (VariantList≽FST _==_)) + CCC≋NCC : ∀ (n : ℕ≥ 2) → CCCL F ≋ NCCL n F CCC≋NCC n = CCC≽NCC n , NCC≽CCC n @@ -231,6 +246,8 @@ module Expressiveness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f⁻¹∘f≗id : f⁻¹ ∘ f ≗ id) (D : F) where open Expressiveness f f⁻¹ f⁻¹∘f≗id + open VariantList using (VariantList-is-Complete) public + CCC-is-complete : Complete (CCCL F) CCC-is-complete = completeness-by-expressiveness VariantList-is-Complete (CCC≽VariantList D) @@ -271,7 +288,23 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (f OC-cannot-be-compiled-to-FST = compiler-cannot-exist FST-is-less-expressive-than-OC ``` +For the proof of `WFOCL⋡FSTL`, we need to construct at least three distinct +configurations. Hence, we need at least two distint features and a method for +comparing these features to decided which values these features are assigned. ```agda + module _ {F' : 𝔽} (f₁ f₂ : F') (f₁≢f₂ : f₁ ≢ f₂) (_==ꟳ_ : DecidableEquality F') where + open FST-to-OC f₁ f₂ f₁≢f₂ _==ꟳ_ using (WFOCL⋡FSTL) + + OC-is-less-expressive-than-FST : WFOCL F ⋡ FSTL F' + OC-is-less-expressive-than-FST = WFOCL⋡FSTL {F} + + FST-cannot-be-compiled-to-OC : ¬ LanguageCompiler (FSTL F') (WFOCL F) + FST-cannot-be-compiled-to-OC = compiler-cannot-exist OC-is-less-expressive-than-FST +``` + +```agda +open VariantList using (VariantList-is-Sound) public + ADT-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (ADTL Variant F) ADT-is-sound {F} _==_ = soundness-by-expressiveness VariantList-is-Sound (ADT-to-VariantList.VariantList≽ADT F Variant _==_) @@ -289,4 +322,7 @@ NADT-is-sound _==_ = soundness-by-expressiveness (CCC-is-sound _==_) (NADT-to-CC OC-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (WFOCL F) OC-is-sound {F} _==_ = soundness-by-expressiveness (2CC-is-sound _==_) (OC-to-2CC.2CC≽OC F) + +FST-is-sound : ∀ {F : 𝔽} (_==_ : DecidableEquality F) → Sound (FSTL F) +FST-is-sound {F} _==_ = soundness-by-expressiveness VariantList-is-Sound (FST-to-VariantList.VariantList≽FST F _==_) ```