split variants file into defs and default langs

VariantSync · Nov 20, 2023 · 0acf064 · 0acf064
1 parent 3b58684
commit 0acf064
Show file tree

Hide file tree

Showing 8 changed files with 39 additions and 32 deletions.
diff --git a/src/Framework/V2/Compiler.agda b/src/Framework/V2/Compiler.agda
@@ -1,6 +1,6 @@
 module Framework.V2.Compiler where
 
-open import Framework.V2.Variants
+open import Framework.V2.Variant
 open import Framework.V2.Definitions
 open import Relation.Binary.PropositionalEquality as Eq using (_≗_)
 open import Data.Product using (_×_)

diff --git a/src/Framework/V2/Constructs/Artifact.agda b/src/Framework/V2/Constructs/Artifact.agda
@@ -7,7 +7,7 @@ open import Level using (_⊔_)
 open import Function using (id; _$_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-open import Framework.V2.Variants
+open import Framework.V2.Variant
 open import Framework.V2.Definitions hiding (Semantics)
 open import Framework.V2.Compiler as Comp using (LanguageCompiler; ConfigTranslation; ConstructFunctor; Stable)
 open LanguageCompiler

diff --git a/src/Framework/V2/Constructs/Choices.agda b/src/Framework/V2/Constructs/Choices.agda
@@ -159,7 +159,7 @@ module Choiceₙ where
   show show-q show-a (D ⟨ es ⟩) = show-q D <+> "⟨" <+> (intersperse " , " (toList (map-list⁺ show-a es))) <+> "⟩"
 
 -- Show how choices can be used as constructors in variability languages.
-open import Framework.V2.Variants
+open import Framework.V2.Variant
 open import Framework.V2.Definitions as Defs hiding (Semantics)
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Function using (id)

diff --git a/src/Framework/V2/Translation/Construct/2Choice-to-NChoice-VL.agda b/src/Framework/V2/Translation/Construct/2Choice-to-NChoice-VL.agda
@@ -12,7 +12,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≗_; refl)
 
 import Data.IndexedSet
 
-open import Framework.V2.Variants
+open import Framework.V2.Variant
 open import Framework.V2.Compiler using (LanguageCompiler; Stable)
 
 import Framework.V2.Translation.Construct.2Choice-to-NChoice as 2→N

diff --git a/src/Framework/V2/Translation/Lang/2ADT-to-NADT.agda b/src/Framework/V2/Translation/Lang/2ADT-to-NADT.agda
@@ -15,7 +15,8 @@ import Data.IndexedSet
 import Framework.V2.Constructs.Choices
 open Framework.V2.Constructs.Choices.Choiceₙ renaming (map to mapₙ)
 
-open import Framework.V2.Variants using (VariantSetoid; GrulerVariant)
+open import Framework.V2.Variant using (VariantSetoid)
+open import Framework.V2.Variants using (GrulerVariant)
 open import Framework.V2.Lang.2ADT
 open import Framework.V2.Lang.NADT
 

diff --git a/src/Framework/V2/V1Compat.agda b/src/Framework/V2/V1Compat.agda
@@ -7,7 +7,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; ref
 import Data.IndexedSet
 
 open import Framework.V2.Definitions
-open import Framework.V2.Variants
+open import Framework.V2.Variant
 
 private
   variable

diff --git a/src/Framework/V2/Variant.agda b/src/Framework/V2/Variant.agda
@@ -0,0 +1,32 @@
+open import Framework.V2.Definitions using (𝕍; 𝔸)
+module Framework.V2.Variant (V : 𝕍) (A : 𝔸) where
+
+open import Data.Fin using (Fin)
+open import Data.List using (List)
+open import Data.Nat using (ℕ; suc)
+
+open import Level using (0ℓ)
+open import Relation.Binary using (Setoid)
+import Relation.Binary.PropositionalEquality as Eq
+
+import Data.IndexedSet
+
+VariantSetoid : Setoid 0ℓ 0ℓ
+VariantSetoid = Eq.setoid (V A)
+
+module IVSet = Data.IndexedSet VariantSetoid
+
+IndexedVMap : Set → Set
+IndexedVMap I = IndexedSet I
+  where open IVSet using (IndexedSet)
+
+{-|
+Variant maps constitute the semantic domain of variability languages.
+While we defined variant maps to be indexed sets with an arbitrary finite and non-empty index set, we directly reflect these properties
+via Fin (suc n) here for convenience.
+-}
+VMap : ℕ → Set
+VMap n = IndexedVMap (Fin (suc n))
+
+forget-first : ∀ {n} → VMap (suc n) → VMap n
+forget-first set i = set (Data.Fin.suc i)
diff --git a/src/Framework/V2/Variants.agda b/src/Framework/V2/Variants.agda
@@ -1,38 +1,12 @@
 module Framework.V2.Variants where
 
-open import Data.Fin using (Fin)
-open import Data.List using (List)
-open import Data.Nat using (ℕ; suc)
-
-open import Level using (0ℓ)
-open import Relation.Binary using (Setoid)
-import Relation.Binary.PropositionalEquality as Eq
-
 open import Framework.V2.Definitions using (𝕍; 𝔸)
 open import Framework.V2.Constructs.Plain.Artifact using (Artifact)
 
-import Data.IndexedSet
-
 data GrulerVariant : 𝕍 where
   asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A
   _∥_   : ∀ {A : 𝔸} (l : GrulerVariant A) → (r : GrulerVariant A) → GrulerVariant A
 
 data Rose : 𝕍 where
   artifact : ∀ {A : 𝔸} → Artifact A (Rose A) → Rose A
 
-VariantSetoid : 𝕍 → 𝔸 → Setoid 0ℓ 0ℓ
-VariantSetoid V A = Eq.setoid (V A)
-
-module IVSet (V : 𝕍) (A : 𝔸) = Data.IndexedSet (VariantSetoid V A)
-
-IndexedVMap : 𝕍 → 𝔸 → Set → Set
-IndexedVMap V A I = IndexedSet I
-  where open IVSet V A using (IndexedSet)
-
-{-|
-Variant maps constitute the semantic domain of variability languages.
-While we defined variant maps to be indexed sets with an arbitrary finite and non-empty index set, we directly reflect these properties
-via Fin (suc n) here for convenience.
--}
-VMap : 𝕍 → 𝔸 → ℕ → Set
-VMap V A n = IndexedVMap V A (Fin (suc n))