Prove that FST is less expressive than OC

src/Framework/Variants.agda

@@ -4,7 +4,7 @@ module Framework.Variants where
 
 open import Data.Unit using (⊤; tt)
 open import Data.Product using (_,_; proj₁; proj₂)
-open import Data.List using ([]; _∷_; map)
+open import Data.List using (List; []; _∷_; map)
 open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
@@ -33,6 +33,9 @@ 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 refl = refl
+
 Artifact∈ₛRose : Artifact ∈ₛ Rose ∞
 cons Artifact∈ₛRose x = rose x
 snoc Artifact∈ₛRose (rose x) = just x

src/Lang/FST.agda

@@ -33,7 +33,7 @@ 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)
+open import Framework.Variants using (Rose; rose; rose-leaf; children-equality)
 open import Framework.Composition.FeatureAlgebra
 open import Framework.VariabilityLanguage
 open import Framework.VariantMap using (VMap)
@@ -504,3 +504,15 @@ module IncompleteOnRose where
   FST-is-incomplete : Incomplete (Rose ∞) FSTL
   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 (e , conf , ⟦e⟧c≡neighbors) =
+  ¬Unique b (Eq.subst (λ l → Unique l) (children-equality ⟦e⟧c≡neighbors) (lemma (⊛-all (select conf (features e)))))
+  where
+  open Impose A
+
+  lemma : ∀ (e : FSF) → Unique (forget-uniqueness e)
+  lemma (_ Impose.⊚ (unique , _)) = unique
+
+  ¬Unique : ∀ (a : atoms A) → ¬ Unique (a -< [] >- ∷ a -< [] >- ∷ [])
+  ¬Unique a ((a≢a ∷ []) ∷ [] ∷ []) = a≢a refl

src/Translation/Lang/OC-to-FST.agda

@@ -0,0 +1,29 @@
+open import Framework.Definitions using (𝔽; 𝔸)
+
+module Translation.Lang.OC-to-FST (F : 𝔽) where
+
+open import Size using (∞)
+open import Data.Bool using (true)
+open import Data.List using ([]; _∷_)
+open import Data.Nat using (zero; _≟_; ℕ)
+open import Data.Product using (_,_)
+import Relation.Binary.PropositionalEquality as Eq
+
+open import Framework.Variants using (Rose)
+open import Lang.All
+open OC using (WFOC; Root; _-<_>-; WFOCL)
+open FST using (FSTL; cannotEncodeNeighbors)
+
+V = Rose ∞
+open import Framework.Relation.Expressiveness V using (_⋡_)
+
+A : 𝔸
+A = ℕ , _≟_
+
+neighbors : WFOC F ∞ A
+neighbors = Root zero (zero -< [] >- ∷ zero -< [] >- ∷ [])
+
+FSTL⋡WFOCL : FSTL F ⋡ WFOCL F
+FSTL⋡WFOCL FSTL≽WFOCL with FSTL≽WFOCL neighbors
+... | e , e⊆neighbors , neighbors⊆e with e⊆neighbors (λ a → true)
+... | conf , e≡neighbors = cannotEncodeNeighbors F zero zero (e , conf , Eq.sym e≡neighbors)

src/Translation/LanguageMap.lagda.md

@@ -66,6 +66,7 @@ import Translation.Lang.VariantList-to-CCC as VariantList-to-CCC
 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
 ```
 
 
@@ -260,6 +261,14 @@ module Completeness {F : 𝔽} (f : F × ℕ → F) (f⁻¹ : F → F × ℕ) (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
+
+  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
+
+  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
 ```
 
 ```agda