to fix: moves

VariantSync · Dec 6, 2023 · ca51c0f · ca51c0f
1 parent caa61e8
commit ca51c0f
Show file tree

Hide file tree

Showing 22 changed files with 41 additions and 58 deletions.
diff --git a/src/Framework/V2/Constructs/Artifact.agda → src/Construct/Artifact.agda b/src/Framework/V2/Constructs/Artifact.agda → src/Construct/Artifact.agda
@@ -1,4 +1,4 @@
-module Framework.V2.Constructs.Artifact where
+module Construct.Artifact where
 
 open import Data.List using (List; map)
 open import Data.List.Properties using (map-cong; map-∘)
@@ -15,7 +15,7 @@ open import Framework.Compiler using (LanguageCompiler)
 open LanguageCompiler
 import Data.IndexedSet
 
-open import Framework.V2.Constructs.Plain.Artifact public
+open import Construct.Plain.Artifact public
 
 Syntax : ℂ
 Syntax E A = Artifact A (E A)

diff --git a/src/Framework/V2/Constructs/Choices.agda → src/Construct/Choices.agda b/src/Framework/V2/Constructs/Choices.agda → src/Construct/Choices.agda
@@ -1,5 +1,5 @@
 {-# OPTIONS --allow-unsolved-metas #-}
-module Framework.V2.Constructs.Choices where
+module Construct.Choices where
 
 open import Data.Bool using (Bool; if_then_else_)
 open import Data.String using (String; _<+>_; intersperse)

diff --git a/...mework/V2/Constructs/GrulerArtifacts.agda → src/Construct/GrulerArtifacts.agda b/...mework/V2/Constructs/GrulerArtifacts.agda → src/Construct/GrulerArtifacts.agda
@@ -1,12 +1,14 @@
-module Framework.V2.Constructs.GrulerArtifacts where
+{-# OPTIONS --sized-types #-}
+
+module Construct.GrulerArtifacts where
 
 open import Data.Maybe using (just; nothing)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-open import Framework.V2.Definitions
-open import Framework.V2.Variants
-open import Framework.V2.Construct
-open import Framework.V2.VariabilityLanguage
+open import Framework.Definitions
+open import Framework.Variants
+open import Framework.VariabilityLanguage
+open import Framework.Construct
 
 -- this is just a value
 data Leaf {ℓ} (A : Set ℓ) : Set ℓ where

diff --git a/...Framework/V2/Constructs/NestedChoice.agda → src/Construct/NestedChoice.agda b/...Framework/V2/Constructs/NestedChoice.agda → src/Construct/NestedChoice.agda
@@ -2,12 +2,12 @@
 
 open import Framework.Definitions
 
-module Framework.V2.Constructs.NestedChoice (F : 𝔽) where
+module Construct.NestedChoice (F : 𝔽) where
 
 open import Data.String using (String)
 open import Size using (Size; ↑_)
 
-import Framework.V2.Constructs.Choices as Chc
+import Construct.Choices as Chc
 open Chc.Choice₂ renaming (Syntax to 2Choice; Standard-Semantics to ⟦_⟧₂; Config to Config₂; show to show-2choice)
 
 data NestedChoice : Size → 𝔼 where

diff --git a/src/Framework/V2/Constructs/Option.agda → src/Construct/Option.agda b/src/Framework/V2/Constructs/Option.agda → src/Construct/Option.agda
diff --git a/...amework/V2/Constructs/Plain/Artifact.agda → src/Construct/Plain/Artifact.agda b/...amework/V2/Constructs/Plain/Artifact.agda → src/Construct/Plain/Artifact.agda
@@ -1,4 +1,4 @@
-module Framework.V2.Constructs.Plain.Artifact where
+module Construct.Plain.Artifact where
 
 open import Data.List using (List; []; map)
 open import Data.List.Properties using () renaming (≡-dec to ≡-dec-l)

diff --git a/src/Framework/V2/Language.agda b/src/Framework/V2/Language.agda
diff --git a/src/Framework/Variants.agda b/src/Framework/Variants.agda
@@ -10,8 +10,8 @@ open import Function using (id; _∘_; flip)
 open import Size using (Size; ↑_; ∞)
 
 open import Framework.Definitions using (𝕍; 𝔸)
-open import Framework.V2.Constructs.Artifact as At using (_-<_>-; map-children; map-children-preserves) renaming (Syntax to Artifact; Construct to ArtifactC)
 open import Framework.VariabilityLanguage
+open import Construct.Artifact as At using (_-<_>-; map-children; map-children-preserves) renaming (Syntax to Artifact; Construct to ArtifactC)
 
 data GrulerVariant : 𝕍 where
   asset : ∀ {A : 𝔸} (a : A) → GrulerVariant A

diff --git a/src/Framework/V2/Lang/2ADT.agda → src/Lang/2ADT.agda b/src/Framework/V2/Lang/2ADT.agda → src/Lang/2ADT.agda
@@ -1,18 +1,18 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.V2.Definitions
+open import Framework.Definitions
 -- TODO: Generalize level of F
-module Framework.V2.Lang.2ADT (F : 𝔽) where
+module Lang.2ADT (F : 𝔽) where
 
 open import Data.Bool using (Bool)
 open import Function using (id)
 open import Size using (Size; ↑_)
 
-open import Framework.V2.VariabilityLanguage
-open import Framework.V2.Constructs.GrulerArtifacts
-open import Framework.V2.Constructs.Choices
-open import Framework.V2.Constructs.NestedChoice F public
-open import Framework.V2.Variants using (GrulerVariant)
+open import Framework.VariabilityLanguage
+open import Framework.Variants using (GrulerVariant)
+open import Construct.GrulerArtifacts
+open import Construct.Choices
+open import Construct.NestedChoice F public
 
 private
   Choice₂ = VLChoice₂.Syntax

diff --git a/src/Lang/BCC.lagda.md b/src/Lang/BCC.lagda.md
@@ -27,8 +27,8 @@ open import Size using (Size; ↑_; ∞)
 open import Framework.Variants
 open import Framework.VariabilityLanguage
 open import Framework.Construct
-open import Framework.V2.Constructs.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
-import Framework.V2.Constructs.Choices as Chc
+open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
+import Construct.Choices as Chc
 open Chc.VLChoice₂ using () renaming (Syntax to Choice₂; Semantics to chc-sem)
 open Chc.Choice₂ using () renaming (Config to Config₂)
 ```

diff --git a/src/Lang/CCC.lagda.md b/src/Lang/CCC.lagda.md
@@ -58,8 +58,8 @@ open import Size using (Size; ↑_; ∞)
 open import Framework.Variants
 open import Framework.VariabilityLanguage
 open import Framework.Construct
-open import Framework.V2.Constructs.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
-import Framework.V2.Constructs.Choices as Chc
+open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
+import Construct.Choices as Chc
 open Chc.VLChoiceₙ using () renaming (Syntax to Choiceₙ; Semantics to chc-sem)
 open Chc.Choiceₙ using () renaming (Config to Configₙ)
 ```

diff --git a/src/Framework/V2/Lang/Gruler.agda → src/Lang/Gruler.agda b/src/Framework/V2/Lang/Gruler.agda → src/Lang/Gruler.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.V2.Definitions
-module Framework.V2.Lang.Gruler (F : 𝔽) where
+open import Framework.Definitions
+module Lang.Gruler (F : 𝔽) where
 
 open import Data.Bool using (Bool)
 open import Data.Maybe using (Maybe; just; nothing)
@@ -10,13 +10,13 @@ open import Size using (Size; ↑_; ∞)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
 
-open import Framework.V2.VariabilityLanguage
-open import Framework.V2.Construct
-open import Framework.V2.Constructs.Choices
-open import Framework.V2.Constructs.GrulerArtifacts
-open import Framework.V2.Variants using (GrulerVariant)
+open import Framework.VariabilityLanguage
+open import Framework.Variants using (GrulerVariant)
+open import Framework.Construct
+open import Construct.Choices
+open import Construct.GrulerArtifacts
 
-open Framework.V2.Constructs.Choices.Choice₂ using (_⟨_,_⟩) renaming (Config to Config₂)
+open Construct.Choices.Choice₂ using (_⟨_,_⟩) renaming (Config to Config₂)
 
 private
   PC = VLParallelComposition.Syntax

diff --git a/src/Framework/V2/Lang/NADT.agda → src/Lang/NADT.agda b/src/Framework/V2/Lang/NADT.agda → src/Lang/NADT.agda
@@ -1,17 +1,17 @@
 {-# OPTIONS --sized-types #-}
 
-open import Framework.V2.Definitions
+open import Framework.Definitions
 -- TODO: Generalize level of F
-module Framework.V2.Lang.NADT (F : 𝔽) where
+module Lang.NADT (F : 𝔽) where
 
 open import Data.Nat using (ℕ)
 open import Function using (id)
 open import Size using (Size; ↑_)
 
-open import Framework.V2.VariabilityLanguage
-open import Framework.V2.Constructs.GrulerArtifacts
-open import Framework.V2.Constructs.Choices
-open import Framework.V2.Variants using (GrulerVariant)
+open import Framework.VariabilityLanguage
+open import Framework.Variants using (GrulerVariant)
+open import Construct.GrulerArtifacts
+open import Construct.Choices
 
 private
   Choiceₙ = VLChoiceₙ.Syntax

diff --git a/src/Lang/OC.lagda.md b/src/Lang/OC.lagda.md
@@ -26,8 +26,8 @@ open import Function using (_∘_)
 open import Framework.Variants
 open import Framework.VariabilityLanguage
 open import Framework.Construct
-open import Framework.V2.Constructs.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
-import Framework.V2.Constructs.Choices as Chc
+open import Construct.Artifact as At using () renaming (Syntax to Artifact; Construct to Artifact-Construct)
+import Construct.Choices as Chc
 open Chc.VLChoice₂ using () renaming (Syntax to Choice₂; Semantics to chc-sem)
 open Chc.Choice₂ using () renaming (Config to Config₂)
 ```

diff --git a/...tion/Construct/2Choice-to-NChoice-VL.agda → ...tion/Construct/2Choice-to-NChoice-VL.agda b/...tion/Construct/2Choice-to-NChoice-VL.agda → ...tion/Construct/2Choice-to-NChoice-VL.agda
diff --git a/...slation/Construct/2Choice-to-NChoice.agda → ...slation/Construct/2Choice-to-NChoice.agda b/...slation/Construct/2Choice-to-NChoice.agda → ...slation/Construct/2Choice-to-NChoice.agda
diff --git a/...slation/Construct/NChoice-to-2Choice.agda → ...slation/Construct/NChoice-to-2Choice.agda b/...slation/Construct/NChoice-to-2Choice.agda → ...slation/Construct/NChoice-to-2Choice.agda
diff --git a/...on/Construct/NestedChoice-to-2Choice.agda → ...on/Construct/NestedChoice-to-2Choice.agda b/...on/Construct/NestedChoice-to-2Choice.agda → ...on/Construct/NestedChoice-to-2Choice.agda
diff --git a/...iments/NChoice-to-2Choice-Experiment.agda → ...iments/NChoice-to-2Choice-Experiment.agda b/...iments/NChoice-to-2Choice-Experiment.agda → ...iments/NChoice-to-2Choice-Experiment.agda
diff --git a/...ork/V2/Translation/Lang/2ADT-to-NADT.agda → src/Translation/Lang/2ADT-to-NADT.agda b/...ork/V2/Translation/Lang/2ADT-to-NADT.agda → src/Translation/Lang/2ADT-to-NADT.agda
diff --git a/src/Translation/OC-to-BCC.lagda.md → src/Translation/Lang/OC-to-BCC.lagda.md b/src/Translation/OC-to-BCC.lagda.md → src/Translation/Lang/OC-to-BCC.lagda.md
diff --git a/src/Translation/VariantList-to-CCC.lagda.md → ...nslation/Lang/VariantList-to-CCC.lagda.md b/src/Translation/VariantList-to-CCC.lagda.md → ...nslation/Lang/VariantList-to-CCC.lagda.md