VariantSync · pmbittner · Apr 6, 2024 · Apr 6, 2024
diff --git a/src/Lang/2ADT.agda → src/Lang/ADT.agda b/src/Lang/2ADT.agda → src/Lang/ADT.agda
@@ -1,31 +1,31 @@
 open import Framework.Definitions
-module Lang.2ADT where
+module Lang.ADT where
 
 open import Data.Bool using (Bool; if_then_else_)
 open import Framework.VariabilityLanguage
 
-data 2ADT (V : 𝕍) (F : 𝔽) : 𝔼 where
-  leaf   : ∀ {A} → V A → 2ADT V F A
-  _⟨_,_⟩ : ∀ {A} → (D : F) → (l : 2ADT V F A) → (r : 2ADT V F A) → 2ADT V F A
+data ADT (V : 𝕍) (F : 𝔽) : 𝔼 where
+  leaf   : ∀ {A} → V A → ADT V F A
+  _⟨_,_⟩ : ∀ {A} → (D : F) → (l : ADT V F A) → (r : ADT V F A) → ADT V F A
 
 Configuration : (F : 𝔽) → Set
 Configuration F = F → Bool
 
-⟦_⟧ : {V : 𝕍} → {F : 𝔽} → 𝔼-Semantics V (Configuration F) (2ADT V F)
+⟦_⟧ : {V : 𝕍} → {F : 𝔽} → 𝔼-Semantics V (Configuration F) (ADT V F)
 ⟦ leaf v      ⟧ _ = v
 ⟦ D ⟨ l , r ⟩ ⟧ c = if c D
                     then ⟦ l ⟧ c
                     else ⟦ r ⟧ c
 
-2ADTL : (V : 𝕍) → (F : 𝔽) → VariabilityLanguage V
-2ADTL V F = ⟪ 2ADT V F , Configuration F , ⟦_⟧ ⟫
+ADTL : (V : 𝕍) → (F : 𝔽) → VariabilityLanguage V
+ADTL V F = ⟪ ADT V F , Configuration F , ⟦_⟧ ⟫
 
 
 open import Data.String as String using (String; _++_; intersperse)
 open import Data.Product using (_,_)
 open import Show.Lines
 
-pretty : {A : 𝔸} → {V : 𝕍} → {F : 𝔽} → (V A → String) → (F → String) → 2ADT V F A → Lines
+pretty : {A : 𝔸} → {V : 𝕍} → {F : 𝔽} → (V A → String) → (F → String) → ADT V F A → Lines
 pretty pretty-variant show-F (leaf v) = > pretty-variant v
 pretty pretty-variant show-F (D ⟨ l , r ⟩) = do
   > show-F D ++ "⟨"

diff --git a/src/Lang/2ADT/Path.agda → src/Lang/ADT/Path.agda b/src/Lang/2ADT/Path.agda → src/Lang/ADT/Path.agda
@@ -1,6 +1,6 @@
 open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼)
 open import Relation.Binary using (DecidableEquality; Rel)
-module Lang.2ADT.Path
+module Lang.ADT.Path
   (F : 𝔽)
   (V : 𝕍)
   (_==_ : DecidableEquality F)
@@ -26,7 +26,7 @@ open Eq.≡-Reasoning
 
 open import Framework.VariabilityLanguage
 open import Util.Suffix using (_endswith_)
-open import Lang.2ADT using (2ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
+open import Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧)
 
 -- A selection of a feature matches it to a boolean value.
 record Selection : Set where
@@ -36,7 +36,7 @@ record Selection : Set where
     value : Bool
 open Selection public
 
--- A list of selection which denotes a path from the root of a 2ADT to a leaf node.
+-- A list of selection which denotes a path from the root of a ADT to a leaf node.
 Path : Set
 Path = List Selection
 
@@ -123,17 +123,17 @@ Note: The symmetry between the rules walk-left and walk-right causes many
       However, we cannot merge the rules into a single rule
       because we have to recurse on either the left or right alternative (not both).
 -}
-data _starts-at_ : ∀ {A} → (p : Path) → (e : 2ADT V F A) → Set where
+data _starts-at_ : ∀ {A} → (p : Path) → (e : ADT V F A) → Set where
   tleaf : ∀ {A} {v : V A}
       ------------------
     → [] starts-at (leaf v)
 
-  walk-left : ∀ {A} {D : F} {l r : 2ADT V F A} {pl : Path}
+  walk-left : ∀ {A} {D : F} {l r : ADT V F A} {pl : Path}
     → pl starts-at l
       -------------------------------------
     → ((D ↣ true) ∷ pl) starts-at (D ⟨ l , r ⟩)
 
-  walk-right : ∀ {A} {D : F} {l r : 2ADT V F A} {pr : Path}
+  walk-right : ∀ {A} {D : F} {l r : ADT V F A} {pr : Path}
     → pr starts-at r
       --------------------------------------
     → ((D ↣ false) ∷ pr) starts-at (D ⟨ l , r ⟩)
@@ -142,27 +142,27 @@ data _starts-at_ : ∀ {A} → (p : Path) → (e : 2ADT V F A) → Set where
 An expression does not contain a feature name
 if all paths do not contain that feature name.
 -}
-_∉'_ : ∀{A} → F → 2ADT V F A → Set
+_∉'_ : ∀{A} → F → ADT V F A → Set
 D ∉' e = ∀ (p : Path) → p starts-at e → D ∉ p
 
 {-
 A path serves as a configuration for an expression e
 if it starts at that expression and ends at a leaf.
 -}
-record PathConfig {A} (e : 2ADT V F A) : Set where
+record PathConfig {A} (e : ADT V F A) : Set where
   constructor _is-valid_
   field
     path : Path
     valid : path starts-at e
 open PathConfig public
 
 {-
-Alternative semantics of 2ADTs by walking a path.
+Alternative semantics of ADTs by walking a path.
 This walk may be illegal by choosing different alternatives for the same choice within a path.
 For example in D ⟨ D ⟨ 1 , dead ⟩ , 2 ⟩ we can reach 'dead' via (D ↣ true ∷ D ↣ false ∷ []).
 However, walking like this is fine as long as the path is unique as we will later prove.
 -}
-walk : ∀ {A} → (e : 2ADT V F A) → PathConfig e → V A
+walk : ∀ {A} → (e : ADT V F A) → PathConfig e → V A
 walk (leaf v) ([] is-valid tleaf) = v
 walk (D ⟨ l , _ ⟩) ((.(D ↣ true ) ∷ pl) is-valid walk-left  t) = walk l (pl is-valid t)
 walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r (pr is-valid t)
@@ -171,7 +171,7 @@ walk (D ⟨ _ , r ⟩) ((.(D ↣ false) ∷ pr) is-valid walk-right t) = walk r
 An expression a is a sub-expression of b
 iff all valid paths from a lead to paths from b.
 -}
-_subexprof_ : ∀ {A} → 2ADT V F A → 2ADT V F A → Set
+_subexprof_ : ∀ {A} → ADT V F A → ADT V F A → Set
 a subexprof b = ∀ (pa : Path) → pa starts-at a → ∃[ pb ] ((pb starts-at b) × (pb endswith pa))
 
 {-

diff --git a/src/Lang/All/Generic.agda b/src/Lang/All/Generic.agda
@@ -24,8 +24,8 @@ module 2CC where
 module NADT where
   open import Lang.NADT renaming (NADTVL to NADTL) public
 
-module 2ADT where
-  open import Lang.2ADT public
+module ADT where
+  open import Lang.ADT public
 
 module OC where
   open import Lang.OC public

diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Test/Experiments/RoundTrip.agda
@@ -84,12 +84,12 @@ get     round-trip ex@(name ≔ ccc) = do
   overwrite-alignment-with Center
     (boxed (6 + width pretty-ccc) "" pretty-ccc)
 
-  ncc         ← translate ccc         "NCC"         CCC→NCC-Exact                                               (NCC.Pretty.pretty id)
-  ncc2        ← compile   ncc         "NCC"         (shrinkTo2Compiler ⌈ ccc ⌉)                                 (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  2cc         ← compile   ncc2        "2CC"         NCC-2→2CC                                                   (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  2adt        ← compile   2cc         "2ADT"        2CC→2ADT                                                    (2ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
-  variantList ← compile   2adt        "VariantList" (2ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id))
-  ccc'        ← compile   variantList "CCC"         (VariantList→CCC "default feature")                         (CCC.pretty id)
+  ncc         ← translate ccc         "NCC"         CCC→NCC-Exact                                              (NCC.Pretty.pretty id)
+  ncc2        ← compile   ncc         "NCC"         (shrinkTo2Compiler ⌈ ccc ⌉)                                (NCC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  2cc         ← compile   ncc2        "2CC"         NCC-2→2CC                                                  (2CC.Pretty.pretty (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  adt         ← compile   2cc         "ADT"         2CC→ADT                                                    (ADT.pretty (show-rose id) (String.diagonal-ℕ ∘ map₂ Fin.toℕ))
+  variantList ← compile   adt         "VariantList" (ADT→VariantList (decidableEquality-× String._≟_ Fin._≟_)) (VariantList.pretty (show-rose id))
+  ccc'        ← compile   variantList "CCC"         (VariantList→CCC "default feature")                        (CCC.pretty id)
   linebreak
 
 

diff --git a/src/Translation/Lang/2CC-to-2ADT.agda → src/Translation/Lang/2CC-to-ADT.agda b/src/Translation/Lang/2CC-to-2ADT.agda → src/Translation/Lang/2CC-to-ADT.agda
@@ -4,7 +4,7 @@ open import Framework.Construct using (_∈ₛ_; cons)
 open import Framework.Definitions using (𝔸; 𝔽; 𝕍; atoms)
 open import Construct.Artifact as At using () renaming (Syntax to Artifact; _-<_>- to artifact-constructor)
 
-module Translation.Lang.2CC-to-2ADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
+module Translation.Lang.2CC-to-ADT (Variant : 𝕍) (Artifact∈ₛVariant : Artifact ∈ₛ Variant) where
 
 import Data.EqIndexedSet as IndexedSet
 open import Data.Bool as Bool using (if_then_else_)
@@ -23,87 +23,87 @@ open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[])
 
 open import Lang.All.Generic Variant Artifact∈ₛVariant
 open 2CC using (2CC; 2CCL)
-open 2ADT using (2ADT; 2ADTL; leaf; _⟨_,_⟩)
+open ADT using (ADT; ADTL; leaf; _⟨_,_⟩)
 
 artifact : ∀ {A : 𝔸} → atoms A → List (Variant A) → Variant A
 artifact a cs = cons Artifact∈ₛVariant (artifact-constructor a cs)
 
 
-push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → atoms A → List (2ADT Variant D A) → 2ADT Variant D A
+push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → atoms A → List (ADT Variant D A) → ADT Variant D A
 push-down-artifact {A = A} a cs = go cs []
   module push-down-artifact-Implementation where
-  go : ∀ {i : Size} {D : 𝔽} → List (2ADT Variant D A) → List (Variant A) → 2ADT Variant D A
+  go : ∀ {i : Size} {D : 𝔽} → List (ADT Variant D A) → List (Variant A) → ADT Variant D A
   go [] vs = leaf (artifact 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 ⟩
 
 translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → 2CC D i A
-  → 2ADT Variant D A
+  → ADT Variant D A
 translate (a 2CC.-< cs >-) = push-down-artifact a (List.map translate cs)
 translate (d 2CC.⟨ l , r ⟩) = d ⟨ translate l , translate r ⟩
 
 ⟦push-down-artifact⟧ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → (a : atoms A)
-  → (cs : List (2ADT Variant D A))
-  → (config : 2ADT.Configuration D)
-  → 2ADT.⟦ push-down-artifact a cs ⟧ config ≡ artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) cs)
+  → (cs : List (ADT Variant D A))
+  → (config : ADT.Configuration D)
+  → ADT.⟦ push-down-artifact a cs ⟧ config ≡ artifact a (List.map (λ e → ADT.⟦ e ⟧ config) cs)
 ⟦push-down-artifact⟧ {D = D} {A = A} a cs config = go' cs []
   where
   open push-down-artifact-Implementation
 
   go' : ∀ {i : Size}
-    → (cs' : List (2ADT Variant D A))
+    → (cs' : List (ADT Variant D A))
     → (vs : List (Variant A))
-    → 2ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+    → ADT.⟦ go a cs cs' vs ⟧ config ≡ artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) cs')
   go' [] vs = Eq.sym (Eq.cong₂ artifact refl (Eq.trans (List.ʳ++-defn vs) (List.++-identityʳ (List.reverse vs))))
   go' (leaf v ∷ cs') vs = Eq.trans (go' cs' (v ∷ vs)) (Eq.cong₂ artifact refl (List.ʳ++-++ List.[ v ] {ys = vs}))
   go' ((d ⟨ c₁ , c₂ ⟩) ∷ cs') vs =
-      2ADT.⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config
+      ADT.⟦ d ⟨ go a cs (c₁ ∷ cs') vs , go a cs (c₂ ∷ cs') vs ⟩ ⟧ config
     ≡⟨⟩
       (if config d
-        then 2ADT.⟦ go a cs (c₁ ∷ cs') vs ⟧ config
-        else 2ADT.⟦ go a cs (c₂ ∷ cs') vs ⟧ config)
+        then ADT.⟦ go a cs (c₁ ∷ cs') vs ⟧ config
+        else ADT.⟦ 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 artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₁ ∷ cs'))
-        else artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c₂ ∷ cs')))
-    ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩
-      artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs'))
+        then artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₁ ∷ cs'))
+        else artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c₂ ∷ cs')))
+    ≡˘⟨ Bool.push-function-into-if (λ c → artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (c ∷ cs'))) (config d) ⟩
+      artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) ((if config d then c₁ else c₂) ∷ cs'))
     ≡⟨⟩
-      artifact a (vs ʳ++ 2ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
-    ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → 2ADT.⟦ e ⟧ config) (config d)) refl)) ⟩
-      artifact a (vs ʳ++ (if config d then 2ADT.⟦ c₁ ⟧ config else 2ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+      artifact a (vs ʳ++ ADT.⟦ if config d then c₁ else c₂ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
+    ≡⟨ Eq.cong₂ artifact refl (Eq.cong₂ _ʳ++_ {x = vs} refl (Eq.cong₂ _∷_ (Bool.push-function-into-if (λ e → ADT.⟦ e ⟧ config) (config d)) refl)) ⟩
+      artifact a (vs ʳ++ (if config d then ADT.⟦ c₁ ⟧ config else ADT.⟦ c₂ ⟧ config) ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
     ≡⟨⟩
-      artifact a (vs ʳ++ 2ADT.⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → 2ADT.⟦ e ⟧ config) cs')
+      artifact a (vs ʳ++ ADT.⟦ d ⟨ c₁ , c₂ ⟩ ⟧ config ∷ List.map (λ e → ADT.⟦ e ⟧ config) cs')
     ≡⟨⟩
-      artifact a (vs ʳ++ List.map (λ e → 2ADT.⟦ e ⟧ config) (d ⟨ c₁ , c₂ ⟩ ∷ cs'))
+      artifact a (vs ʳ++ List.map (λ e → ADT.⟦ e ⟧ config) (d ⟨ c₁ , c₂ ⟩ ∷ cs'))
     ∎
 
 preserves-≗ : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → (expr : 2CC D i A)
-  → 2ADT.⟦ translate expr ⟧ ≗ 2CC.⟦ expr ⟧
+  → ADT.⟦ translate expr ⟧ ≗ 2CC.⟦ expr ⟧
 preserves-≗ {D = D} {A = A} (a 2CC.-< cs >-) config =
-    2ADT.⟦ translate (a 2CC.-< cs >-) ⟧ config
+    ADT.⟦ translate (a 2CC.-< cs >-) ⟧ config
   ≡⟨⟩
-    2ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config
+    ADT.⟦ push-down-artifact a (List.map translate cs) ⟧ config
   ≡⟨ ⟦push-down-artifact⟧ a (List.map translate cs) config ⟩
-    artifact a (List.map (λ e → 2ADT.⟦ e ⟧ config) (List.map translate cs))
+    artifact a (List.map (λ e → ADT.⟦ e ⟧ config) (List.map translate cs))
   ≡˘⟨ Eq.cong₂ artifact refl (List.map-∘ cs) ⟩
-    artifact a (List.map (λ e → 2ADT.⟦ translate e ⟧ config) cs)
+    artifact a (List.map (λ e → ADT.⟦ translate e ⟧ config) cs)
   ≡⟨ Eq.cong₂ artifact refl (List.map-cong (λ e → preserves-≗ e config) cs) ⟩
     artifact a (List.map (λ e → 2CC.⟦ e ⟧ config) cs)
   ≡⟨⟩
     2CC.⟦ a 2CC.-< cs >- ⟧ config
   ∎
 preserves-≗ (d 2CC.⟨ l , r ⟩) config =
-    2ADT.⟦ translate (d 2CC.⟨ l , r ⟩) ⟧ config
+    ADT.⟦ translate (d 2CC.⟨ l , r ⟩) ⟧ config
   ≡⟨⟩
-    2ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config
+    ADT.⟦ d ⟨ translate l , translate r ⟩ ⟧ config
   ≡⟨⟩
-    (if config d then 2ADT.⟦ translate l ⟧ config else 2ADT.⟦ translate r ⟧ config)
-  ≡˘⟨ Bool.push-function-into-if (λ e → 2ADT.⟦ translate e ⟧ config) (config d) ⟩
-    2ADT.⟦ translate (if config d then l else r) ⟧ config
+    (if config d then ADT.⟦ translate l ⟧ config else ADT.⟦ translate r ⟧ config)
+  ≡˘⟨ Bool.push-function-into-if (λ e → ADT.⟦ translate e ⟧ config) (config d) ⟩
+    ADT.⟦ translate (if config d then l else r) ⟧ config
   ≡⟨ preserves-≗ (if config d then l else r) config ⟩
     2CC.⟦ if config d then l else r ⟧ config
   ≡⟨⟩
@@ -112,14 +112,14 @@ preserves-≗ (d 2CC.⟨ l , r ⟩) config =
 
 preserves : ∀ {i : Size} {D : 𝔽} {A : 𝔸}
   → (expr : 2CC D i A)
-  → 2ADT.⟦ translate expr ⟧ ≅[ id ][ id ] 2CC.⟦ expr ⟧
+  → ADT.⟦ translate expr ⟧ ≅[ id ][ id ] 2CC.⟦ expr ⟧
 preserves expr = ≗→≅[] (preserves-≗ expr)
 
-2CC→2ADT : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (2ADTL Variant D)
-2CC→2ADT .LanguageCompiler.compile = translate
-2CC→2ADT .LanguageCompiler.config-compiler expr .to = id
-2CC→2ADT .LanguageCompiler.config-compiler expr .from = id
-2CC→2ADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
+2CC→ADT : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (ADTL Variant D)
+2CC→ADT .LanguageCompiler.compile = translate
+2CC→ADT .LanguageCompiler.config-compiler expr .to = id
+2CC→ADT .LanguageCompiler.config-compiler expr .from = id
+2CC→ADT .LanguageCompiler.preserves expr = ≅[]-sym (preserves expr)
 
-2ADT≽2CC : ∀ {D : 𝔽} → 2ADTL Variant D ≽ 2CCL D
-2ADT≽2CC = expressiveness-from-compiler 2CC→2ADT
+ADT≽2CC : ∀ {D : 𝔽} → ADTL Variant D ≽ 2CCL D
+ADT≽2CC = expressiveness-from-compiler 2CC→ADT