From 0b3868b08c86cc7df01e2c066c1c3ec96630fb30 Mon Sep 17 00:00:00 2001
From: Benjamin Moosherr <benjamin.moosherr@uni-ulm.de>
Date: Mon, 20 May 2024 20:43:30 +0200
Subject: [PATCH] Translate FST to VariantList

---
 src/Lang/All/Generic.agda                    |  13 +-
 src/Translation/Lang/FST-to-OC.agda          |   4 +-
 src/Translation/Lang/FST-to-VariantList.agda | 241 +++++++++++++++++++
 src/Translation/LanguageMap.lagda.md         |  14 ++
 4 files changed, 268 insertions(+), 4 deletions(-)
 create mode 100644 src/Translation/Lang/FST-to-VariantList.agda

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/Translation/Lang/FST-to-OC.agda b/src/Translation/Lang/FST-to-OC.agda
index 3e97dede..7d978dc5 100644
--- a/src/Translation/Lang/FST-to-OC.agda
+++ b/src/Translation/Lang/FST-to-OC.agda
@@ -75,12 +75,12 @@ counter-example = zero ◀ (
 
 -- There are four relevant configurations for `counter-example` because it uses
 -- exactly two features: `c₁`, `c₂`, `all-oc true` and `all-oc false`.
-c₁ : FST.Conf F
+c₁ : FST.Configuration F
 c₁ f with f ==ꟳ f₁
 c₁ f | yes f≡f₁ = true
 c₁ f | no f≢f₁ = false
 
-c₂ : FST.Conf F
+c₂ : FST.Configuration F
 c₂ f with f ==ꟳ f₂
 c₂ f | yes f≡f₂ = true
 c₂ f | no f≢f₂ = false
diff --git a/src/Translation/Lang/FST-to-VariantList.agda b/src/Translation/Lang/FST-to-VariantList.agda
new file mode 100644
index 00000000..640f2187
--- /dev/null
+++ b/src/Translation/Lang/FST-to-VariantList.agda
@@ -0,0 +1,241 @@
+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'
+
+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)
+
+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
+
+conf : ∀ {A : 𝔸} → (e : SPL F A) → FST.Configuration F → VariantList.Configuration
+conf {A} (_ ◀ fs) c = conf' c (map name fs)
+
+fnoc : ∀ {A : 𝔸} → (e : SPL F A) → VariantList.Configuration → FST.Configuration F
+fnoc {A} (_ ◀ fs) n f = find-or-last n (configs (map name fs)) f
+
+conf'<configs : ∀ (c : FST.Configuration F) (fs : List F)
+  → conf' c fs < List⁺.length (configs fs)
+conf'<configs c [] = s≤s z≤n
+conf'<configs c (f ∷ fs) with c f
+conf'<configs c (f ∷ fs) | true =
+  begin-strict
+    List⁺.length (configs fs) + conf' c fs
+  <⟨ ℕ.+-monoʳ-< (List⁺.length (configs fs)) (conf'<configs c fs) ⟩
+    List⁺.length (configs fs) + List⁺.length (configs fs)
+  ≡⟨ Eq.cong₂ _+_ (List⁺.length-map (config-with false f) (configs fs)) (List⁺.length-map (config-with true f) (configs fs)) ⟨
+    List⁺.length (List⁺.map (config-with false f) (configs fs)) + List⁺.length (List⁺.map (config-with true f) (configs fs))
+  ≡⟨ List.length-++ (List⁺.toList (List⁺.map (config-with false f) (configs fs))) ⟨
+    List⁺.length (List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs))
+  ≡⟨⟩
+    List⁺.length (configs (f ∷ fs))
+  ∎
+  where
+  open ℕ.≤-Reasoning
+conf'<configs c (f ∷ fs) | false =
+  begin-strict
+    conf' c fs
+  <⟨ conf'<configs c fs ⟩
+    List⁺.length (configs fs)
+  ≡⟨ List⁺.length-map (config-with false f) (configs fs) ⟨
+    List⁺.length (List⁺.map (config-with false f) (configs fs))
+  ≤⟨ ℕ.m≤m+n (List⁺.length (List⁺.map (config-with false f) (configs fs))) (List⁺.length (List⁺.map (config-with true f) (configs fs))) ⟩
+    List⁺.length (List⁺.map (config-with false f) (configs fs)) + List⁺.length (List⁺.map (config-with true f) (configs fs))
+  ≡⟨ List.length-++ (List⁺.toList (List⁺.map (config-with false f) (configs fs))) ⟨
+    List⁺.length (List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs))
+  ≡⟨⟩
+    List⁺.length (configs (f ∷ fs))
+  ∎
+  where
+  open ℕ.≤-Reasoning
+
+config-with-≡ : (b : Bool) → (f : F) → (c : FST.Configuration F) → config-with b f c f ≡ b
+config-with-≡ b f c with f ==ꟳ f
+config-with-≡ b f c | no f≢f = ⊥-elim (f≢f refl)
+config-with-≡ b f c | yes _ = refl
+
+config-with-≢ : (b : Bool) → (f f' : F) → f ≢ f' → (c : FST.Configuration F) → config-with b f' c f ≡ c f
+config-with-≢ b f f' f≢f' c with f' ==ꟳ f
+config-with-≢ b f f' f≢f' c | no _ = refl
+config-with-≢ b f f' f≢f' c | yes f'≡f = ⊥-elim (f≢f' (Eq.sym f'≡f))
+
+find-or-last-config-with : ∀ (c : FST.Configuration F) (b : Bool) (f f' : F) (fs : List F) (v : FST.Configuration F → Bool)
+  → ((c : FST.Configuration F) → config-with b f' c f ≡ v c)
+  → find-or-last (conf' c fs) (List⁺.map (config-with b f') (configs fs)) f ≡ v (find-or-last (conf' c fs) (configs fs))
+find-or-last-config-with c b f f' fs v p =
+    find-or-last (conf' c fs) (List⁺.map (config-with b f') (configs fs)) f
+  ≡⟨ map-find-or-last (λ c → c f) (conf' c fs) (List⁺.map (config-with b f') (configs fs)) ⟩
+    find-or-last (conf' c fs) (List⁺.map (λ c → c f) (List⁺.map (config-with b f') (configs fs)))
+  ≡⟨ Eq.cong₂ find-or-last refl (List⁺.map-∘ (configs fs)) ⟨
+    find-or-last (conf' c fs) (List⁺.map (λ c → config-with b f' c f) (configs fs))
+  ≡⟨ Eq.cong₂ find-or-last refl (List⁺.map-cong p (configs fs)) ⟩
+    find-or-last (conf' c fs) (List⁺.map v (configs fs))
+  ≡⟨ map-find-or-last v (conf' c fs) (configs fs) ⟨
+    v (find-or-last (conf' c fs) (configs fs))
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+conf'-lemma : (c : FST.Configuration F) → (f : F) → (fs : List F) → f ∈ fs → find-or-last (conf' c fs) (configs fs) f ≡ c f
+conf'-lemma c f (f' ∷ fs) f∈fs with f ==ꟳ f'
+conf'-lemma c f (.f ∷ fs) f∈fs | yes refl with c f
+conf'-lemma c f (.f ∷ fs) f∈fs | yes refl | true =
+    find-or-last (List⁺.length (configs fs) + conf' c fs) (configs (f ∷ fs)) f
+  ≡⟨⟩
+    find-or-last (List⁺.length (configs fs) + conf' c fs) (List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs)) f
+  ≡⟨ Eq.cong-app (Eq.cong₂ find-or-last {u = List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs)} (Eq.cong₂ _+_ (List⁺.length-map (config-with false f) (configs fs)) refl) refl) f ⟨
+    find-or-last (List⁺.length (List⁺.map (config-with false f) (configs fs)) + conf' c fs) (List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs)) f
+  ≡⟨ Eq.cong-app (find-or-last-prepend-+ (conf' c fs) (List⁺.map (config-with false f) (configs fs)) (List⁺.map (config-with true f) (configs fs))) f ⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with true f) (configs fs)) f
+  ≡⟨ find-or-last-config-with c true f f fs (λ c → true) (λ c → config-with-≡ true f c) ⟩
+    true
+  ∎
+  where
+  open Eq.≡-Reasoning
+conf'-lemma c f (.f ∷ fs) f∈fs | yes refl | false =
+    find-or-last (conf' c fs) (configs (f ∷ fs)) f
+  ≡⟨⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with false f) (configs fs) ⁺++⁺ List⁺.map (config-with true f) (configs fs)) f
+  ≡⟨ Eq.cong-app (find-or-last-append (List⁺.map (config-with false f) (configs fs)) (List⁺.map (config-with true f) (configs fs)) (ℕ.≤-trans (conf'<configs c fs) (ℕ.≤-reflexive (Eq.sym (List⁺.length-map (config-with false f) (configs fs)))))) f ⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with false f) (configs fs)) f
+  ≡⟨ find-or-last-config-with c false f f fs (λ c → false) (λ c → config-with-≡ false f c) ⟩
+    false
+  ∎
+  where
+  open Eq.≡-Reasoning
+conf'-lemma c f (f' ∷ fs) (here f≡f') | no f≢f' = ⊥-elim (f≢f' f≡f')
+conf'-lemma c f (f' ∷ fs) (there f∈fs) | no f≢f' with c f'
+conf'-lemma c f (f' ∷ fs) (there f∈fs) | no f≢f' | true =
+    find-or-last (List⁺.length (configs fs) + conf' c fs) (configs (f' ∷ fs)) f
+  ≡⟨⟩
+    find-or-last (List⁺.length (configs fs) + conf' c fs) (List⁺.map (config-with false f') (configs fs) ⁺++⁺ List⁺.map (config-with true f') (configs fs)) f
+  ≡⟨ Eq.cong-app (Eq.cong₂ find-or-last {u = List⁺.map (config-with false f') (configs fs) ⁺++⁺ List⁺.map (config-with true f') (configs fs)} (Eq.cong₂ _+_ (List⁺.length-map (config-with false f') (configs fs)) refl) refl) f ⟨
+    find-or-last (List⁺.length (List⁺.map (config-with false f') (configs fs)) + conf' c fs) (List⁺.map (config-with false f') (configs fs) ⁺++⁺ List⁺.map (config-with true f') (configs fs)) f
+  ≡⟨ Eq.cong-app (find-or-last-prepend-+ (conf' c fs) (List⁺.map (config-with false f') (configs fs)) (List⁺.map (config-with true f') (configs fs))) f ⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with true f') (configs fs)) f
+  ≡⟨ find-or-last-config-with c true f f' fs (λ c → c f) (λ c → config-with-≢ true f f' f≢f' c) ⟩
+    find-or-last (conf' c fs) (configs fs) f
+  ≡⟨ conf'-lemma c f fs f∈fs ⟩
+    c f
+  ∎
+  where
+  open Eq.≡-Reasoning
+conf'-lemma c f (f' ∷ fs) (there f∈fs) | no f≢f' | false =
+    find-or-last (conf' c fs) (configs (f' ∷ fs)) f
+  ≡⟨⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with false f') (configs fs) ⁺++⁺ List⁺.map (config-with true f') (configs fs)) f
+  ≡⟨ Eq.cong-app (find-or-last-append (List⁺.map (config-with false f') (configs fs)) (List⁺.map (config-with true f') (configs fs)) ((ℕ.≤-trans (conf'<configs c fs) (ℕ.≤-reflexive (Eq.sym (List⁺.length-map (config-with false f') (configs fs))))))) f ⟩
+    find-or-last (conf' c fs) (List⁺.map (config-with false f') (configs fs)) f
+  ≡⟨ find-or-last-config-with c false f f' fs (λ c → c f) (λ c → config-with-≢ false f f' f≢f' c) ⟩
+    find-or-last (conf' c fs) (configs fs) f
+  ≡⟨ conf'-lemma c f fs f∈fs ⟩
+    c f
+  ∎
+  where
+  open Eq.≡-Reasoning
+
+AllWith∈ : ∀ {A : Set} {P : A → Set} (as : List A) → ((a : A) → a ∈ as → P a) → All P as
+AllWith∈ [] f = []
+AllWith∈ (a ∷ as) f = f a (here refl) ∷ AllWith∈ as (λ a a∈as → f a (there a∈as))
+
+⟦⟧-cong : ∀ {A : 𝔸} (a : atoms A) (fs : List (Feature F A)) (c : FST.Configuration F)
+  → (g : FST.Configuration F → FST.Configuration F)
+  → All (λ f → g c f ≡ c f) (map name fs)
+  → FST.⟦ a ◀ fs ⟧ (g c) ≡ FST.⟦ a ◀ fs ⟧ c
+⟦⟧-cong {A} a fs c g ps = Eq.cong₂ _-<_>- refl (Eq.cong forget-uniqueness (Eq.cong ⊛-all (go fs ps)))
+  where
+  go : (fs : List (Feature F A))
+    → All (λ f → g c f ≡ c f) (map name fs)
+    → select (g c) fs ≡ select c fs
+  go [] p = refl
+  go ((f :: i) ∷ fs) (px ∷ p) with (g 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 (λ c → find-or-last (conf e c) (configs (map name fs))) (AllWith∈ (map name fs) (λ f f∈fs → 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 475f5564..7bb5432a 100644
--- a/src/Translation/LanguageMap.lagda.md
+++ b/src/Translation/LanguageMap.lagda.md
@@ -68,6 +68,7 @@ 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
 ```
 
 
@@ -117,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
 
@@ -187,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
 
@@ -303,4 +314,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 _==_)
 ```