Merge pull request #72 from pmbittner/vatras-module

Move all modules into a Vatras module

.gitignore

@@ -8,7 +8,7 @@
 # build
 src/cc
 src/Main
-src/Everything.agda
+src/Vatras/Everything.agda
 
 # default nix-build symlink name
 /result

flake.nix

@@ -3,7 +3,7 @@
     packages.x86_64-linux.default = import inputs.self {system = "x86_64-linux";};
     overlays.default = final: prev: {
       agdaPackages = prev.agdaPackages.overrideScope' (self: super: {
-        EPVL = import inputs.self {
+        Vatras = import inputs.self {
           system = "x86_64-linux";
           pkgs = final;
         };

makefile

@@ -3,19 +3,19 @@
 andrun : build run
 
 check:
-	env AGDA_DIR="./libs" agda src/Main.agda
+	env AGDA_DIR="./libs" agda src/Vatras/Main.agda
 
 check-all:
 	./scripts/check-all.sh
 
-check-everything: src/Everything.agda
-	env AGDA_DIR="./libs" agda src/Everything.agda
+check-everything: src/Vatras/Everything.agda
+	env AGDA_DIR="./libs" agda src/Vatras/Everything.agda
 
 build:
-	env AGDA_DIR="./libs" agda --compile src/Main.agda
+	env AGDA_DIR="./libs" agda --compile src/Vatras/Main.agda
 
 build-2.6.4.3:
-	env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Main.agda
+	env AGDA_DIR="./libs" agda-2.6.4.3 --compile src/Vatras/Main.agda
 
 run:
 	./src/Main
@@ -24,14 +24,13 @@ clean:
 	rm -f src/Main
 	rm -rf _build
 	rm -rf src/MAlonzo
-	rm -f src/Everything.agda
+	rm -f src/Vatras/Everything.agda
 	find . -name "*.agdai" -type f -delete
 
-# Don't cache src/Everything.agda as it will break everytime some file is deleted
-.PHONY: src/Everything.agda
-src/Everything.agda:
-	echo '{-# OPTIONS --sized-types #-}' > src/Everything.agda
-	echo '{-# OPTIONS --allow-unsolved-metas #-}' >> src/Everything.agda
-	echo '{-# OPTIONS --guardedness #-}' >> src/Everything.agda
-	echo 'module Everything where' >> src/Everything.agda
-	find src -regextype posix-extended -regex '.*/.*\.l?agda(.md)?' -not -path 'src/Everything.agda' | sed -E 's|^src/|import |; s|\.l?agda(.md)?$$||; s|/|.|g' >> src/Everything.agda
+# Don't cache src/Vatras/Everything.agda as it will break everytime some file is deleted
+.PHONY: src/Vatras/Everything.agda
+src/Vatras/Everything.agda:
+	echo '{-# OPTIONS --allow-unsolved-metas #-}' > src/Vatras/Everything.agda
+	echo '{-# OPTIONS --guardedness #-}' >> src/Vatras/Everything.agda
+	echo 'module Vatras.Everything where' >> src/Vatras/Everything.agda
+	find src -regextype posix-extended -regex '.*/.*\.l?agda(.md)?' -not -path 'src/Vatras/Everything.agda' | sed -E 's|^src/|import |; s|\.l?agda(.md)?$$||; s|/|.|g' >> src/Vatras/Everything.agda

scripts/find-inconsistency-sources.sh

@@ -15,61 +15,61 @@ awkDocumentationMap='
       ignore["holes:"]=1
 
       document(1,
-        "src/Util/String.agda:  where postulate trustMe : _",
+        "src/Vatras/Util/String.agda:  where postulate trustMe : _",
         "Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples.")
       document(2,
-        "src/Util/String.agda:  where postulate trustMe : _",
+        "src/Vatras/Util/String.agda:  where postulate trustMe : _",
         "Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples.")
       document(3,
-        "src/Util/String.agda:  where postulate trustMe : _",
+        "src/Vatras/Util/String.agda:  where postulate trustMe : _",
         "Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples.")
       document(4,
-        "src/Util/String.agda:  where postulate trustMe : _",
+        "src/Vatras/Util/String.agda:  where postulate trustMe : _",
         "Also proposed in the Agda issue tracker to make String propositions provable. Only used in examples.")
       document(1,
-        "src/Show/Lines.agda:{-# NON_TERMINATING #-}",
+        "src/Vatras/Show/Lines.agda:{-# NON_TERMINATING #-}",
         "Only used for printing and thus not proof relevant. Also, NON_TERMINATING functions do not reduce during type checking.")
       document(1,
-        "src/Tutorial/A_NewLanguage.lagda.md:We are using the `{-# TERMINATING -#}` flag here:",
+        "src/Vatras/Tutorial/A_NewLanguage.lagda.md:We are using the `{-# TERMINATING -#}` flag here:",
         "This is actually a comment.")
       document(1,
-        "src/Tutorial/A_NewLanguage.lagda.md:{-# TERMINATING #-}",
+        "src/Vatras/Tutorial/A_NewLanguage.lagda.md:{-# TERMINATING #-}",
         "Simplification of the tutorial. Not used in the anything else.")
       document(1,
-        "src/Tutorial/A_NewLanguage.lagda.md:MyConfig = {!!}",
+        "src/Vatras/Tutorial/A_NewLanguage.lagda.md:MyConfig = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/A_NewLanguage.lagda.md:⟦_⟧ = {!!}",
+        "src/Vatras/Tutorial/A_NewLanguage.lagda.md:⟦_⟧ = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:conf e c²ᶜᶜ = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:conf e c²ᶜᶜ = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:fnoc e cᵐʸ = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:fnoc e cᵐʸ = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:preservation-⊆[] e c = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:preservation-⊆[] e c = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:preservation-⊇[] e c = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:preservation-⊇[] e c = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:translate (D ⟨ l , r ⟩) = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:translate (D ⟨ l , r ⟩) = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/B_Translation.lagda.md:translate (a -< cs >-)  = {!!}",
+        "src/Vatras/Tutorial/B_Translation.lagda.md:translate (a -< cs >-)  = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/C_Proofs.lagda.md:  {!!}   -- write down the proof of correctness in this hole",
+        "src/Vatras/Tutorial/C_Proofs.lagda.md:  {!!}   -- write down the proof of correctness in this hole",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/C_Proofs.lagda.md:  {!!} , -- write down the expression in this hole",
+        "src/Vatras/Tutorial/C_Proofs.lagda.md:  {!!} , -- write down the expression in this hole",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/C_Proofs.lagda.md:2CC≽MyLang = {!!}",
+        "src/Vatras/Tutorial/C_Proofs.lagda.md:2CC≽MyLang = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
       document(1,
-        "src/Tutorial/C_Proofs.lagda.md:MyLang-is-Sound = {!!}",
+        "src/Vatras/Tutorial/C_Proofs.lagda.md:MyLang-is-Sound = {!!}",
         "Intentional hole to be filled by you! Not used in anything other than the tutorial.")
 
       exitCode=0

src/Data/EqIndexedSet.agda → src/Vatras/Data/EqIndexedSet.agda

@@ -5,8 +5,8 @@ This module re-exports indexed sets but where the underlying
 equivalence for the target set is fixed to propositional equality _≡_.
 Importing this module should be your usual way of importing indexed sets.
 -}
-module Data.EqIndexedSet {ℓ : Level} {A : Set ℓ} where
+module Vatras.Data.EqIndexedSet {ℓ : Level} {A : Set ℓ} where
 
 import Relation.Binary.PropositionalEquality as Eq
-open import Data.IndexedSet {ℓ} (Eq.setoid A) as ISet public
+open import Vatras.Data.IndexedSet {ℓ} (Eq.setoid A) as ISet public
 

src/Data/IndexedSet.lagda.md → src/Vatras/Data/IndexedSet.lagda.md

@@ -17,7 +17,7 @@ where two indices point to the same element (`A(i) ≈ A(j)` for two indices `i
 open import Level using (Level)
 open import Relation.Binary as RB using (Setoid)
 
-module Data.IndexedSet {c ℓ : Level} (S : Setoid c ℓ) where
+module Vatras.Data.IndexedSet {c ℓ : Level} (S : Setoid c ℓ) where
 ```
 
 ## Imports

src/Framework/Annotation/IndexedDimension.agda → src/Vatras/Framework/Annotation/IndexedDimension.agda

@@ -3,12 +3,12 @@ This module defines an annotation that equips another annotation with an index.
 The index is bounded (i.e., it is a Fin).
 IndexedDimension is used for conversions from NCC to NCC with lower arity (in particular 2).
 -}
-module Framework.Annotation.IndexedDimension where
+module Vatras.Framework.Annotation.IndexedDimension where
 
 open import Data.Fin using (Fin)
 open import Data.Product using (_×_)
-open import Util.Nat.AtLeast using (ℕ≥; toℕ; pred)
-open import Framework.Definitions using (𝔽)
+open import Vatras.Util.Nat.AtLeast using (ℕ≥; toℕ; pred)
+open import Vatras.Framework.Definitions using (𝔽)
 
 {-|
 An indexed dimension indexes another type of annotations

src/Framework/Annotation/Negatable.agda → src/Vatras/Framework/Annotation/Negatable.agda

@@ -1,6 +1,6 @@
-module Framework.Annotation.Negatable where
+module Vatras.Framework.Annotation.Negatable where
 
-open import Framework.Definitions using (𝔽)
+open import Vatras.Framework.Definitions using (𝔽)
 open import Data.Bool using (Bool; true; false; not)
 
 {-|

src/Framework/Compiler.agda → src/Vatras/Framework/Compiler.agda

@@ -2,17 +2,17 @@
 This module defines compilers of variability languages
 and useful operators.
 -}
-module Framework.Compiler where
+module Vatras.Framework.Compiler where
 
-open import Framework.Definitions
-open import Framework.VariabilityLanguage
-open import Framework.Relation.Function using (_⇔_; to; from; to-is-Embedding)
+open import Vatras.Framework.Definitions
+open import Vatras.Framework.VariabilityLanguage
+open import Vatras.Framework.Relation.Function using (_⇔_; to; from; to-is-Embedding)
 
 open import Relation.Binary.PropositionalEquality as Eq using (_≗_)
 open import Data.Product using (_×_)
 open import Function using (id; _∘_)
 
-open import Data.EqIndexedSet using (_≅_; _≅[_][_]_; ≅[]-trans)
+open import Vatras.Data.EqIndexedSet using (_≅_; _≅[_][_]_; ≅[]-trans)
 
 {-|
 A compiler from a variability language L to another language M translates

src/Framework/Composition/FeatureAlgebra.lagda.md → src/Vatras/Framework/Composition/FeatureAlgebra.lagda.md

@@ -11,7 +11,7 @@ that some data should be composed from a range of modules or components (before
 if our domain is programs).
 
 ```agda
-module Framework.Composition.FeatureAlgebra where
+module Vatras.Framework.Composition.FeatureAlgebra where
 
 open import Data.Product using (proj₁; proj₂; _×_; _,_)
 open import Algebra.Structures using (IsMonoid)

src/Framework/Definitions.agda → src/Vatras/Framework/Definitions.agda

@@ -1,4 +1,4 @@
-module Framework.Definitions where
+module Vatras.Framework.Definitions where
 
 open import Data.Maybe using (Maybe; just)
 open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂) renaming (_,_ to _and_)
@@ -30,7 +30,7 @@ atoms = proj₁
 {-|
 Variant Language.
 A variant should represent atomic data in some way so its parameterized in atomic data.
-In our paper, this type is fixed to rose trees (see Framework.Variants.agda).
+In our paper, this type is fixed to rose trees (see Vatras.Framework.Variants.agda).
 -}
 𝕍 : Set₂
 𝕍 = 𝔸 → Set₁

src/Framework/Proof/ForFree.lagda.md → src/Vatras/Framework/Proof/ForFree.lagda.md

@@ -8,15 +8,15 @@ also a range of further interesting proofs for free (e.g., also relating incompl
 with expressiveness), which did not fit into the paper.
 
 ```agda
-open import Framework.Definitions using (𝕍)
-module Framework.Proof.ForFree (V : 𝕍) where
+open import Vatras.Framework.Definitions using (𝕍)
+module Vatras.Framework.Proof.ForFree (V : 𝕍) where
 
 open import Data.Product using (_,_; _×_; ∄-syntax)
-open import Framework.VariabilityLanguage using (VariabilityLanguage)
-open import Framework.Properties.Completeness V
-open import Framework.Properties.Soundness V
-open import Framework.Relation.Expressiveness V
-open import Data.EqIndexedSet
+open import Vatras.Framework.VariabilityLanguage using (VariabilityLanguage)
+open import Vatras.Framework.Properties.Completeness V
+open import Vatras.Framework.Properties.Soundness V
+open import Vatras.Framework.Relation.Expressiveness V
+open import Vatras.Data.EqIndexedSet
 ```
 
 ```agda

src/Framework/Properties/Completeness.lagda.md → src/Vatras/Framework/Properties/Completeness.lagda.md

@@ -3,18 +3,18 @@
 ## Module
 
 ```agda
-open import Framework.Definitions using (𝕍)
-module Framework.Properties.Completeness (V : 𝕍) where
+open import Vatras.Framework.Definitions using (𝕍)
+module Vatras.Framework.Properties.Completeness (V : 𝕍) where
 ```
 
 ## Imports
 
 ```agda
 open import Data.Product using (Σ-syntax)
 open import Relation.Nullary.Negation using (¬_)
-open import Framework.VariabilityLanguage
-open import Framework.VariantGenerator V
-open import Data.EqIndexedSet
+open import Vatras.Framework.VariabilityLanguage
+open import Vatras.Framework.VariantGenerator V
+open import Vatras.Data.EqIndexedSet
 ```
 
 ## Definitions