From 1e62285fe87448798cdaf45792ec4655ba62fd2d Mon Sep 17 00:00:00 2001 From: Benjamin Moosherr Date: Wed, 28 Aug 2024 15:07:28 +0200 Subject: [PATCH] Move all modules into a Vatras module --- .gitignore | 2 +- README.md | 174 +++++++++--------- EPVL.agda-lib => Vatras.agda-lib | 0 flake.nix | 2 +- makefile | 27 ++- scripts/find-inconsistency-sources.sh | 38 ++-- src/Lang/All.agda | 35 ---- .../Lang/Transitive/2CC-to-CCC.agda | 24 --- .../Lang/Transitive/CCC-to-2CC.agda | 25 --- src/{ => Vatras}/Data/EqIndexedSet.agda | 4 +- src/{ => Vatras}/Data/IndexedSet.lagda.md | 2 +- .../Annotation/IndexedDimension.agda | 6 +- .../Framework/Annotation/Negatable.agda | 4 +- src/{ => Vatras}/Framework/Compiler.agda | 10 +- .../Composition/FeatureAlgebra.lagda.md | 2 +- src/{ => Vatras}/Framework/Definitions.agda | 4 +- .../Framework/Proof/ForFree.lagda.md | 14 +- .../Properties/Completeness.lagda.md | 10 +- .../Framework/Properties/Finity.agda | 16 +- .../Framework/Properties/NonEmpty.agda | 6 +- .../Framework/Properties/Soundness.lagda.md | 10 +- .../Framework/Relation/Configuration.lagda.md | 8 +- .../Framework/Relation/Expression.lagda.md | 8 +- .../Relation/Expressiveness.lagda.md | 16 +- .../Framework/Relation/Function.agda | 4 +- .../Framework/VariabilityLanguage.agda | 4 +- .../Framework/VariantGenerator.agda | 6 +- src/{ => Vatras}/Framework/Variants.agda | 10 +- src/{ => Vatras}/Lang/2CC.lagda.md | 14 +- src/{ => Vatras}/Lang/ADT.agda | 8 +- src/{ => Vatras}/Lang/ADT/Path.agda | 10 +- src/Vatras/Lang/All.agda | 35 ++++ src/{ => Vatras}/Lang/CCC.lagda.md | 18 +- src/{ => Vatras}/Lang/FST.lagda.md | 20 +- src/{ => Vatras}/Lang/Gruler.agda | 8 +- src/{ => Vatras}/Lang/NADT.agda | 10 +- src/{ => Vatras}/Lang/NCC.lagda.md | 12 +- src/{ => Vatras}/Lang/OC.lagda.md | 18 +- src/{ => Vatras}/Lang/OC/Alternative.agda | 10 +- src/{ => Vatras}/Lang/OC/Properties.agda | 8 +- src/{ => Vatras}/Lang/OC/Subtree.lagda.md | 10 +- src/{ => Vatras}/Lang/VariantList.lagda.md | 24 +-- src/{ => Vatras}/Main.agda | 26 +-- src/{ => Vatras}/Show/Eval.agda | 10 +- src/{ => Vatras}/Show/Lines.agda | 4 +- src/{ => Vatras}/Show/Print.agda | 4 +- src/{ => Vatras}/Test/Example.agda | 4 +- src/{ => Vatras}/Test/Examples/CCC.agda | 8 +- src/{ => Vatras}/Test/Examples/OC.agda | 8 +- src/{ => Vatras}/Test/Examples/Variants.agda | 8 +- src/{ => Vatras}/Test/Experiment.agda | 8 +- .../Test/Experiments/CCC-to-2CC.agda | 28 +-- .../Test/Experiments/FST-Experiments.agda | 18 +- .../Test/Experiments/OC-to-2CC.agda | 30 +-- .../Test/Experiments/RoundTrip.agda | 40 ++-- .../Test/Test/VariantList-Completeness.agda | 14 +- src/{ => Vatras}/Test/UnitTest.agda | 10 +- .../Translation/Lang/2CC-to-ADT.agda | 18 +- .../Translation/Lang/2CC-to-NCC.agda | 20 +- .../Translation/Lang/2CC/Redundancy.lagda.md | 14 +- .../Translation/Lang/2CC/Rename.agda | 16 +- .../Translation/Lang/ADT-to-2CC.agda | 20 +- .../Translation/Lang/ADT-to-NADT.agda | 16 +- .../Translation/Lang/ADT-to-VariantList.agda | 32 ++-- .../Translation/Lang/ADT/DeadElim.agda | 14 +- .../Translation/Lang/ADT/Rename.agda | 14 +- .../Translation/Lang/ADT/WalkSemantics.agda | 18 +- .../Translation/Lang/CCC-to-NCC.agda | 28 +-- .../Translation/Lang/FST-to-OC.lagda.md | 16 +- .../Lang/FST-to-VariantList.lagda.md | 20 +- .../Translation/Lang/NADT-to-CCC.agda | 22 +-- .../Translation/Lang/NCC-to-2CC.agda | 22 +-- .../Translation/Lang/NCC-to-CCC.agda | 20 +- .../Translation/Lang/NCC/Grow.agda | 20 +- .../Translation/Lang/NCC/NCC-to-NCC.agda | 26 +-- .../Translation/Lang/NCC/Rename.agda | 22 +-- .../Translation/Lang/NCC/ShrinkTo2.agda | 22 +-- .../Translation/Lang/OC-to-2CC.lagda.md | 22 +-- .../Translation/Lang/OC-to-FST.agda | 10 +- .../Lang/Transitive/2CC-to-CCC.agda | 24 +++ .../Lang/Transitive/CCC-to-2CC.agda | 25 +++ .../Lang/VariantList-to-CCC.lagda.md | 18 +- .../Translation/LanguageMap.lagda.md | 74 ++++---- .../Tutorial/A_NewLanguage.lagda.md | 10 +- .../Tutorial/B_Translation.lagda.md | 16 +- src/{ => Vatras}/Tutorial/C_Proofs.lagda.md | 32 ++-- src/{ => Vatras}/Util/AuxProofs.agda | 2 +- src/{ => Vatras}/Util/Embedding.agda | 2 +- src/{ => Vatras}/Util/Enumerable.agda | 2 +- src/{ => Vatras}/Util/Existence.agda | 2 +- src/{ => Vatras}/Util/Function.agda | 2 +- src/{ => Vatras}/Util/List.agda | 4 +- src/{ => Vatras}/Util/Named.agda | 2 +- src/{ => Vatras}/Util/Nat/AtLeast.agda | 2 +- .../Util/NonEmptyTraversable.agda | 2 +- src/{ => Vatras}/Util/ShowHelpers.agda | 2 +- src/{ => Vatras}/Util/String.agda | 2 +- src/{ => Vatras}/Util/Suffix.agda | 2 +- .../Util/UnwrapIndexedEquivalence.agda | 2 +- src/{ => Vatras}/Util/Vec.agda | 6 +- 100 files changed, 780 insertions(+), 781 deletions(-) rename EPVL.agda-lib => Vatras.agda-lib (100%) delete mode 100644 src/Lang/All.agda delete mode 100644 src/Translation/Lang/Transitive/2CC-to-CCC.agda delete mode 100644 src/Translation/Lang/Transitive/CCC-to-2CC.agda rename src/{ => Vatras}/Data/EqIndexedSet.agda (68%) rename src/{ => Vatras}/Data/IndexedSet.lagda.md (99%) rename src/{ => Vatras}/Framework/Annotation/IndexedDimension.agda (74%) rename src/{ => Vatras}/Framework/Annotation/Negatable.agda (88%) rename src/{ => Vatras}/Framework/Compiler.agda (92%) rename src/{ => Vatras}/Framework/Composition/FeatureAlgebra.lagda.md (99%) rename src/{ => Vatras}/Framework/Definitions.agda (94%) rename src/{ => Vatras}/Framework/Proof/ForFree.lagda.md (94%) rename src/{ => Vatras}/Framework/Properties/Completeness.lagda.md (79%) rename src/{ => Vatras}/Framework/Properties/Finity.agda (75%) rename src/{ => Vatras}/Framework/Properties/NonEmpty.agda (78%) rename src/{ => Vatras}/Framework/Properties/Soundness.lagda.md (75%) rename src/{ => Vatras}/Framework/Relation/Configuration.lagda.md (89%) rename src/{ => Vatras}/Framework/Relation/Expression.lagda.md (95%) rename src/{ => Vatras}/Framework/Relation/Expressiveness.lagda.md (94%) rename src/{ => Vatras}/Framework/Relation/Function.agda (94%) rename src/{ => Vatras}/Framework/VariabilityLanguage.agda (89%) rename src/{ => Vatras}/Framework/VariantGenerator.agda (88%) rename src/{ => Vatras}/Framework/Variants.agda (95%) rename src/{ => Vatras}/Lang/2CC.lagda.md (96%) rename src/{ => Vatras}/Lang/ADT.agda (90%) rename src/{ => Vatras}/Lang/ADT/Path.agda (96%) create mode 100644 src/Vatras/Lang/All.agda rename src/{ => Vatras}/Lang/CCC.lagda.md (93%) rename src/{ => Vatras}/Lang/FST.lagda.md (98%) rename src/{ => Vatras}/Lang/Gruler.agda (88%) rename src/{ => Vatras}/Lang/NADT.agda (82%) rename src/{ => Vatras}/Lang/NCC.lagda.md (92%) rename src/{ => Vatras}/Lang/OC.lagda.md (95%) rename src/{ => Vatras}/Lang/OC/Alternative.agda (88%) rename src/{ => Vatras}/Lang/OC/Properties.agda (81%) rename src/{ => Vatras}/Lang/OC/Subtree.lagda.md (95%) rename src/{ => Vatras}/Lang/VariantList.lagda.md (90%) rename src/{ => Vatras}/Main.agda (69%) rename src/{ => Vatras}/Show/Eval.agda (78%) rename src/{ => Vatras}/Show/Lines.agda (99%) rename src/{ => Vatras}/Show/Print.agda (84%) rename src/{ => Vatras}/Test/Example.agda (60%) rename src/{ => Vatras}/Test/Examples/CCC.agda (92%) rename src/{ => Vatras}/Test/Examples/OC.agda (88%) rename src/{ => Vatras}/Test/Examples/Variants.agda (75%) rename src/{ => Vatras}/Test/Experiment.agda (92%) rename src/{ => Vatras}/Test/Experiments/CCC-to-2CC.agda (89%) rename src/{ => Vatras}/Test/Experiments/FST-Experiments.agda (90%) rename src/{ => Vatras}/Test/Experiments/OC-to-2CC.agda (80%) rename src/{ => Vatras}/Test/Experiments/RoundTrip.agda (80%) rename src/{ => Vatras}/Test/Test/VariantList-Completeness.agda (85%) rename src/{ => Vatras}/Test/UnitTest.agda (90%) rename src/{ => Vatras}/Translation/Lang/2CC-to-ADT.agda (90%) rename src/{ => Vatras}/Translation/Lang/2CC-to-NCC.agda (90%) rename src/{ => Vatras}/Translation/Lang/2CC/Redundancy.lagda.md (92%) rename src/{ => Vatras}/Translation/Lang/2CC/Rename.agda (92%) rename src/{ => Vatras}/Translation/Lang/ADT-to-2CC.agda (82%) rename src/{ => Vatras}/Translation/Lang/ADT-to-NADT.agda (89%) rename src/{ => Vatras}/Translation/Lang/ADT-to-VariantList.agda (86%) rename src/{ => Vatras}/Translation/Lang/ADT/DeadElim.agda (96%) rename src/{ => Vatras}/Translation/Lang/ADT/Rename.agda (91%) rename src/{ => Vatras}/Translation/Lang/ADT/WalkSemantics.agda (96%) rename src/{ => Vatras}/Translation/Lang/CCC-to-NCC.agda (96%) rename src/{ => Vatras}/Translation/Lang/FST-to-OC.lagda.md (96%) rename src/{ => Vatras}/Translation/Lang/FST-to-VariantList.lagda.md (96%) rename src/{ => Vatras}/Translation/Lang/NADT-to-CCC.agda (82%) rename src/{ => Vatras}/Translation/Lang/NCC-to-2CC.agda (89%) rename src/{ => Vatras}/Translation/Lang/NCC-to-CCC.agda (90%) rename src/{ => Vatras}/Translation/Lang/NCC/Grow.agda (94%) rename src/{ => Vatras}/Translation/Lang/NCC/NCC-to-NCC.agda (66%) rename src/{ => Vatras}/Translation/Lang/NCC/Rename.agda (91%) rename src/{ => Vatras}/Translation/Lang/NCC/ShrinkTo2.agda (97%) rename src/{ => Vatras}/Translation/Lang/OC-to-2CC.lagda.md (96%) rename src/{ => Vatras}/Translation/Lang/OC-to-FST.agda (77%) create mode 100644 src/Vatras/Translation/Lang/Transitive/2CC-to-CCC.agda create mode 100644 src/Vatras/Translation/Lang/Transitive/CCC-to-2CC.agda rename src/{ => Vatras}/Translation/Lang/VariantList-to-CCC.lagda.md (90%) rename src/{ => Vatras}/Translation/LanguageMap.lagda.md (84%) rename src/{ => Vatras}/Tutorial/A_NewLanguage.lagda.md (95%) rename src/{ => Vatras}/Tutorial/B_Translation.lagda.md (95%) rename src/{ => Vatras}/Tutorial/C_Proofs.lagda.md (90%) rename src/{ => Vatras}/Util/AuxProofs.agda (99%) rename src/{ => Vatras}/Util/Embedding.agda (87%) rename src/{ => Vatras}/Util/Enumerable.agda (97%) rename src/{ => Vatras}/Util/Existence.agda (96%) rename src/{ => Vatras}/Util/Function.agda (91%) rename src/{ => Vatras}/Util/List.agda (98%) rename src/{ => Vatras}/Util/Named.agda (94%) rename src/{ => Vatras}/Util/Nat/AtLeast.agda (98%) rename src/{ => Vatras}/Util/NonEmptyTraversable.agda (93%) rename src/{ => Vatras}/Util/ShowHelpers.agda (95%) rename src/{ => Vatras}/Util/String.agda (99%) rename src/{ => Vatras}/Util/Suffix.agda (98%) rename src/{ => Vatras}/Util/UnwrapIndexedEquivalence.agda (92%) rename src/{ => Vatras}/Util/Vec.agda (96%) diff --git a/.gitignore b/.gitignore index b0aec163..db93f9fa 100644 --- a/.gitignore +++ b/.gitignore @@ -8,7 +8,7 @@ # build src/cc src/Main -src/Everything.agda +src/Vatras/Everything.agda # default nix-build symlink name /result diff --git a/README.md b/README.md index d0f6664c..6c368e5b 100644 --- a/README.md +++ b/README.md @@ -199,31 +199,31 @@ In particular, our library provides, The library is organized as follows: -- The [src/Framework](src/Framework) directory contains the definitions of our formal framework, defined in Section 4 in our paper. - - [VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics. - - Soundness and completeness are defined in the [Properties](src/Framework/Properties) sub-directory. - - Definitions for expressiveness and configuration equivalence are in the [Relation](src/Framework/Relation) sub-directory. - - Theorems for proofs for free (Section 4.4) are within the [Proof](src/Framework/Proof) sub-directory, including several additional interesting theorems, which did not fit into the paper. -- [src/Lang](src/Lang) contains definitions of particular variability languages (Section 3). -- [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) contains an overview of our case study (Section 5) to compare existing variability languages. - - [src/Translation/Lang](src/Translation/Lang) contains the compilers and the resulting expressiveness proofs in one file per language pair and direction (e.g., `2CC-to-ADT` implements the translation from binary choice calculus to algebraic decision trees and its correctness proof). - - Further sub-directories of [src/Translation/Lang](src/Translation/Lang) facilitate intra-language compilers (i.e., compilers from a language to itself). For example, [src/Translation/Lang/ADT/DeadElim.agda](src/Translation/Lang/ADT/DeadElim.agda) implements a compiler from `ADT` to `ADT` that eliminates any dead branches, and additionally generates a proof that the returned `ADT` does not have any dead branches anymore. -- [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) implements the theory of indexed sets with various operators and equational reasoning. -- [src/Test](src/Test) contains our unit test infrastructure (or better: unit _proofs_) as well as some example expressions for some languages. -- [src/Test/Experiments/RoundTrip.agda](src/Test/Experiments/RoundTrip.agda) implements the round-trip for our demo, including our sandwich running example. This file may serve as an entry point and example on how to run the compilers implemented in the library. -- [src/Tutorial](src/Tutorial) contains tutorials for getting to know the library (explained in more detail below). -- [src/Show/Lines.agda](src/Show/Lines.agda) implements a small pretty-printer, which we use for the demo's output. +- The [src/Vatras/Framework](src/Vatras/Framework) directory contains the definitions of our formal framework, defined in Section 4 in our paper. + - [VariabilityLanguage.agda](src/Vatras/Framework/VariabilityLanguage.agda) defines variability languages and their denotational semantics. + - Soundness and completeness are defined in the [Properties](src/Vatras/Framework/Properties) sub-directory. + - Definitions for expressiveness and configuration equivalence are in the [Relation](src/Vatras/Framework/Relation) sub-directory. + - Theorems for proofs for free (Section 4.4) are within the [Proof](src/Vatras/Framework/Proof) sub-directory, including several additional interesting theorems, which did not fit into the paper. +- [src/Vatras/Lang](src/Vatras/Lang) contains definitions of particular variability languages (Section 3). +- [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) contains an overview of our case study (Section 5) to compare existing variability languages. + - [src/Vatras/Translation/Lang](src/Vatras/Translation/Lang) contains the compilers and the resulting expressiveness proofs in one file per language pair and direction (e.g., `2CC-to-ADT` implements the translation from binary choice calculus to algebraic decision trees and its correctness proof). + - Further sub-directories of [src/Vatras/Translation/Lang](src/Vatras/Translation/Lang) facilitate intra-language compilers (i.e., compilers from a language to itself). For example, [src/Vatras/Translation/Lang/ADT/DeadElim.agda](src/Vatras/Translation/Lang/ADT/DeadElim.agda) implements a compiler from `ADT` to `ADT` that eliminates any dead branches, and additionally generates a proof that the returned `ADT` does not have any dead branches anymore. +- [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) implements the theory of indexed sets with various operators and equational reasoning. +- [src/Vatras/Test](src/Vatras/Test) contains our unit test infrastructure (or better: unit _proofs_) as well as some example expressions for some languages. +- [src/Vatras/Test/Experiments/RoundTrip.agda](src/Vatras/Test/Experiments/RoundTrip.agda) implements the round-trip for our demo, including our sandwich running example. This file may serve as an entry point and example on how to run the compilers implemented in the library. +- [src/Vatras/Tutorial](src/Vatras/Tutorial) contains tutorials for getting to know the library (explained in more detail below). +- [src/Vatras/Show/Lines.agda](src/Vatras/Show/Lines.agda) implements a small pretty-printer, which we use for the demo's output. ### Tutorials -To extend or reuse the library, we offer a range of tutorials in the [Tutorials module](src/Tutorial). +To extend or reuse the library, we offer a range of tutorials in the [Tutorials module](src/Vatras/Tutorial). These tutorials are literate Agda files with holes for you to fill in. Hence, when trying the tutorials you can directly check your definitions to be type-correct with Agda in a suitable editor (e.g., Emacs or VS Code) and you can navigate the framework. The tutorials might also serve as copy-and-paste-templates for new definitions. -1. [The New Language Tutorial](src/Tutorial/A_NewLanguage.lagda.md) explains how to define a new variability language, including syntax, semantics, and configuration. -2. [The Translation Tutorial](src/Tutorial/B_Translation.lagda.md) explains how to compile/translate your language to another existing language and proving correctness. -3. [The Proofs Tutorial](src/Tutorial/C_Proofs.lagda.md) explains how to prove completeness, soundness, and expressiveness, and how you can use your compiler to do so. +1. [The New Language Tutorial](src/Vatras/Tutorial/A_NewLanguage.lagda.md) explains how to define a new variability language, including syntax, semantics, and configuration. +2. [The Translation Tutorial](src/Vatras/Tutorial/B_Translation.lagda.md) explains how to compile/translate your language to another existing language and proving correctness. +3. [The Proofs Tutorial](src/Vatras/Tutorial/C_Proofs.lagda.md) explains how to prove completeness, soundness, and expressiveness, and how you can use your compiler to do so. We recommend following the tutorials in order. @@ -236,9 +236,9 @@ We refrained from providing documentation in terms of a separate website because ### Changing the Demo Input -To adapt the demo, you can implement your own experiments and add them to the list of experiments to run at the top of the [Main](src/Main.agda) file. +To adapt the demo, you can implement your own experiments and add them to the list of experiments to run at the top of the [Main](src/Vatras/Main.agda) file. If you simply want to change the inputs of existing experiments, you can change the list of inputs for each experiment in the list of experiments as well. -In particular, you may add new inputs to the round-trip translation by adding your own example core choice calculus expression (`CCC`) to the `examples` list at the bottom of the [RoundTrip module](src/Test/Experiments/RoundTrip.agda). +In particular, you may add new inputs to the round-trip translation by adding your own example core choice calculus expression (`CCC`) to the `examples` list at the bottom of the [RoundTrip module](src/Vatras/Test/Experiments/RoundTrip.agda). You may define your own expression by adding a new definition like this, where `ex-new` is the name of your example, `"The new example"` is its title, and where `{!!}` is an Agda hole which you can fill in with an abstract syntax tree of a core choice calculus expression: ```agda ex-new : Example (CCC.CCC Feature ∞ Artifact) @@ -286,77 +286,77 @@ The following table shows where each of the definitions, theorems, and proofs fr | statement | notation in paper | name in our Agda Library | file | notes | |-----------------|-----------------------------------|--------------------------------------------------------------------|------------------------------------------------------------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------------------------| -| Section 1 | contribution: a map of languages | | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Section 2 | running example | | [src/Test/Experiments/RoundTrip.agda](src/Test/Experiments/RoundTrip.agda) | | -| Table 1 | | | [src/Lang/All.agda](src/Lang/All.agda) | This file only reexports the language definitions. Use the go-to-definition functionality of your editor for easy exploration. | -| | Core Choice Calculus | `CCC` | [src/Lang/CCC.lagda.md](src/Lang/CCC.lagda.md) | | -| | Binary Choice Calculus | `2CC` | [src/Lang/2CC.lagda.md](src/Lang/2CC.lagda.md) | | -| | Algebraic Decision Trees | `ADT` | [src/Lang/ADT.agda](src/Lang/ADT.agda) | | -| | Gruler's Language | `Gruler` | [src/Lang/Gruler.agda](src/Lang/Gruler.agda) | | -| | Option Calculus | `WFOC`, `OC` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | In contrast to the paper, WFOC duplicates the artifact constructor to enforce the existence of a top-level artifact. | -| | Feature Structure Trees | `FST` | [src/Lang/FST.agda](src/Lang/FST.lagda.md) | | -| | Clone-and-Own (List of Variants) | `VariantList` | [src/Lang/VariantList.lagda.md](src/Lang/VariantList.lagda.md) | | -| Definition 4.1 | Indexed Set | `IndexedSet` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | -| Definition 4.3 | Indexed Set Inclusion ⋿ | `_∈_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | -| | Subset ⊑ | `_⊆_`, `_⊆[_]_` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | In contrast to `_⊆_`, `_⊆[_]_` requires an explicit mapping between the indices of the two indexed sets which can be useful information. | -| | Equivalence ≅ | `_≅_`, `_≅[_][_]`_ | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | The difference between `_≅_` and `_≅[_][_]_` is the same as between `_⊆_` and `_⊆[_]_`. | -| Corollary 4.5 | ⊑ is a partial order | `⊆-IsIndexedPartialOrder`, `⊆[]-refl`, `⊆[]-antisym`, `⊆[]-trans` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | -| | ≅ is an equivalence relation | `≅-IsIndexedEquivalence`, `≅[]-refl`, `≅[]-sym`, `≅[]-trans` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | | +| Section 1 | contribution: a map of languages | | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Section 2 | running example | | [src/Vatras/Test/Experiments/RoundTrip.agda](src/Vatras/Test/Experiments/RoundTrip.agda) | | +| Table 1 | | | [src/Vatras/Lang/All.agda](src/Vatras/Lang/All.agda) | This file only reexports the language definitions. Use the go-to-definition functionality of your editor for easy exploration. | +| | Core Choice Calculus | `CCC` | [src/Vatras/Lang/CCC.lagda.md](src/Vatras/Lang/CCC.lagda.md) | | +| | Binary Choice Calculus | `2CC` | [src/Vatras/Lang/2CC.lagda.md](src/Vatras/Lang/2CC.lagda.md) | | +| | Algebraic Decision Trees | `ADT` | [src/Vatras/Lang/ADT.agda](src/Vatras/Lang/ADT.agda) | | +| | Gruler's Language | `Gruler` | [src/Vatras/Lang/Gruler.agda](src/Vatras/Lang/Gruler.agda) | | +| | Option Calculus | `WFOC`, `OC` | [src/Vatras/Lang/OC.lagda.md](src/Vatras/Lang/OC.lagda.md) | In contrast to the paper, WFOC duplicates the artifact constructor to enforce the existence of a top-level artifact. | +| | Feature Structure Trees | `FST` | [src/Vatras/Lang/FST.agda](src/Vatras/Lang/FST.lagda.md) | | +| | Clone-and-Own (List of Variants) | `VariantList` | [src/Vatras/Lang/VariantList.lagda.md](src/Vatras/Lang/VariantList.lagda.md) | | +| Definition 4.1 | Indexed Set | `IndexedSet` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | | +| Definition 4.3 | Indexed Set Inclusion ⋿ | `_∈_` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | | +| | Subset ⊑ | `_⊆_`, `_⊆[_]_` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | In contrast to `_⊆_`, `_⊆[_]_` requires an explicit mapping between the indices of the two indexed sets which can be useful information. | +| | Equivalence ≅ | `_≅_`, `_≅[_][_]`_ | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The difference between `_≅_` and `_≅[_][_]_` is the same as between `_⊆_` and `_⊆[_]_`. | +| Corollary 4.5 | ⊑ is a partial order | `⊆-IsIndexedPartialOrder`, `⊆[]-refl`, `⊆[]-antisym`, `⊆[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | | +| | ≅ is an equivalence relation | `≅-IsIndexedEquivalence`, `≅[]-refl`, `≅[]-sym`, `≅[]-trans` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | | | Definition 4.6 | Finite Indexed Set | | | We actually only need finite and non-empty indexed sets and do not define finite indexed sets separately. | -| Definition 4.8 | Non-empty Indexed Set | `empty` | [src/Data/IndexedSet.lagda.md](src/Data/IndexedSet.lagda.md) | The library definition is a predicate that ensures an indexed set to be non-empty. | -| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Framework/VariantGenerator.agda](src/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. | -| Definition 4.10 | Semantic Domain | `VariantGenerator` | [src/Framework/VariantGenerator.agda](src/Framework/VariantGenerator.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. | -| Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | | -| Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Framework/Definitions.agda](src/Framework/Definitions.agda) | | -| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | | -| | | `VariabilityLanguage` | [src/Framework/VariabilityLanguage.agda](src/Framework/VariabilityLanguage.agda) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. | -| Definition 4.15 | Complete(𝐿) | `Complete` | [src/Framework/Properties/Completeness.lagda.md](src/Framework/Properties/Completeness.lagda.md) | | -| Definition 4.16 | Sound(𝐿) | `Sound` | [src/Framework/Properties/Soundness.lagda.md](src/Framework/Properties/Soundness.lagda.md) | | -| Definition 4.17 | ⪰ | `_≽_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| | ≡ | `_≋_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| | ≻ | `_≻_` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| Corollary 4.18 | ⪰ is a partial order | `≽-IsPartialOrder` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| | ≡ is an equivalence relation | `≋-IsEquivalence` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | +| Definition 4.8 | Non-empty Indexed Set | `empty` | [src/Vatras/Data/IndexedSet.lagda.md](src/Vatras/Data/IndexedSet.lagda.md) | The library definition is a predicate that ensures an indexed set to be non-empty. | +| Definition 4.9 | Variant Generator | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | This is the finite and non-empty indexed set definition mentioned above. | +| Definition 4.10 | Semantic Domain | `VariantGenerator` | [src/Vatras/Framework/VariantGenerator.agda](src/Vatras/Framework/VariantGenerator.agda) | In contrast to a variant map, the semantic domain is the type of variant maps instead of its elements. | +| Definition 4.11 | configuration language 𝐶 | `ℂ` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | | +| Definition 4.12 | variability language 𝐿 | `𝔼` | [src/Vatras/Framework/Definitions.agda](src/Vatras/Framework/Definitions.agda) | | +| Definition 4.13 | ⟦.⟧ | `𝔼-Semantics` | [src/Vatras/Framework/VariabilityLanguage.agda](src/Vatras/Framework/VariabilityLanguage.agda) | | +| | | `VariabilityLanguage` | [src/Vatras/Framework/VariabilityLanguage.agda](src/Vatras/Framework/VariabilityLanguage.agda) | VariabilityLanguage is a bundle of 𝔼, 𝕂 and 𝔼-Semantics. | +| Definition 4.15 | Complete(𝐿) | `Complete` | [src/Vatras/Framework/Properties/Completeness.lagda.md](src/Vatras/Framework/Properties/Completeness.lagda.md) | | +| Definition 4.16 | Sound(𝐿) | `Sound` | [src/Vatras/Framework/Properties/Soundness.lagda.md](src/Vatras/Framework/Properties/Soundness.lagda.md) | | +| Definition 4.17 | ⪰ | `_≽_` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | +| | ≡ | `_≋_` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | +| | ≻ | `_≻_` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | +| Corollary 4.18 | ⪰ is a partial order | `≽-IsPartialOrder` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | +| | ≡ is an equivalence relation | `≋-IsEquivalence` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | | Definition 4.19 | 𝑀 ⇾ 𝐿 | | | We only model correct compilers. | -| Definition 4.20 | 𝑀 ⇾ 𝐿 correct | `LanguageCompiler` | [src/Framework/Compiler.agda](src/Framework/Compiler.agda) | | -| Theorem 4.21 | 𝑀 ⇾ 𝐿 ⇒ 𝐿 ⪰ 𝑀 | `expressiveness-from-compiler` | [src/Framework/Relation/Expressiveness.lagda.md](src/Framework/Relation/Expressiveness.lagda.md) | | -| Theorem 4.22 | Complete(M) ∧ L ≽ M ⇒ Complete(L) | `completeness-by-expressiveness` | [src/Framework/Proof/ForFree.lagda.md](src/Framework/Proof/ForFree.lagda.md) | | -| Theorem 4.23 | Sound(L) ∧ L ≽ M ⇒ Sound(M) | `soundness-by-expressiveness` | [src/Framework/Proof/ForFree.lagda.md](src/Framework/Proof/ForFree.lagda.md) | | -| Theorem 4.24 | Complete(L) ∧ Sound(M) ⇒ L ≽ M | `expressiveness-by-completeness-and-soundness` | [src/Framework/Proof/ForFree.lagda.md](src/Framework/Proof/ForFree.lagda.md) | | -| Figure 3 | | | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | This file mostly reexports expressiveness results and applies transitivity and the above theorems. It serves as a nice entry point to explore most of our results. | -| Theorem 5.1 | 𝑛-CC | `NCC` | [src/Lang/NCC.lagda.md](src/Lang/NCC.lagda.md) | | -| | 𝑛-CC ⪰ CCC | `NCC≽CCC` | [src/Translation/Lang/CCC-to-NCC.agda](src/Translation/Lang/CCC-to-NCC.agda) | | -| | clamp | `Exact.translate` | [src/Translation/Lang/CCC-to-NCC.agda](src/Translation/Lang/CCC-to-NCC.agda) | | -| | shrink₂ | `shrinkTo2Compiler` | [src/Translation/Lang/NCC/ShrinkTo2.agda](src/Translation/Lang/NCC/ShrinkTo2.agda) | | -| | grow | `growCompiler` | [src/Translation/Lang/NCC/Grow.agda](src/Translation/Lang/NCC/Grow.agda) | | -| Theorem 5.3 | ADT ≽ 2CC | `ADT≽2CC` | [src/Translation/Lang/2CC-to-ADT.agda](src/Translation/Lang/2CC-to-ADT.agda) | | -| Corollary 5.5 | CCC ≡ 2CC ≡ ADT ≡ 𝑛-CC | `CCC≋NCC`, `NCC≋2CC`, and `2CC≋ADT` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.6 | Complete(CaO) | `VariantList-is-Complete` | [src/Lang/VariantList.lagda.md](src/Lang/VariantList.lagda.md) | | -| Theorem 5.7 | Sound(CaO) | `VariantList-is-Sound` | [src/Lang/VariantList.lagda.md](src/Lang/VariantList.lagda.md) | | -| Theorem 5.8 | CaO ≽ ADT | `VariantList≽ADT` | [src/Translation/Lang/ADT-to-VariantList.agda](src/Translation/Lang/ADT-to-VariantList.agda) | | -| Theorem 5.10 | CCC ≽ CaO | `CCC≽VariantList` | [src/Translation/Lang/VariantList-to-CCC.lagda.md](src/Translation/Lang/VariantList-to-CCC.lagda.md) | | -| Corollary 5.11 | CCC is complete and sound | `CCC-is-complete`, `CCC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| | 2CC is complete and sound | `2CC-is-complete`, `2CC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| | ADT is complete and sound | `ADT-is-complete`, `ADT-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| | 𝑛-CC is complete and sound | `NCC-is-complete`, `NCC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.12 | 2CC ≽ OC | `2CC≽OC` | [src/Translation/Lang/OC-to-2CC.lagda.md](src/Translation/Lang/OC-to-2CC.lagda.md) | | -| Corollary 5.13 | Sound(OC) | `OC-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.14 | ¬Complete(OC) | `OC-is-incomplete` | [src/Lang/OC.lagda.md](src/Lang/OC.lagda.md) | | -| Theorem 5.15 | 2CC ≻ OC | `2CC≻WFOC` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Lang/FST.lagda.md](src/Lang/FST.lagda.md) | | -| Theorem 5.17 | OC ⋡ FST | `WFOC⋡FST` | [src/Translation/Lang/FST-to-OC.lagda.md](src/Translation/Lang/FST-to-OC.lagda.md) | | -| Theorem 5.18 | FST ⋡ OC | `FSTL⋡WFOCL` | [src/Translation/Lang/OC-to-FST.agda](src/Translation/Lang/OC-to-FST.agda) | | -| Corollary 5.19 | FST ⋡ CaO | `FST⋡VariantList` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Theorem 5.20 | CaO ≽ FST | `VariantList≽FST` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | -| Corollary 5.21 | Sound(FST) | `FST-is-sound` | [src/Translation/LanguageMap.lagda.md](src/Translation/LanguageMap.lagda.md) | | +| Definition 4.20 | 𝑀 ⇾ 𝐿 correct | `LanguageCompiler` | [src/Vatras/Framework/Compiler.agda](src/Vatras/Framework/Compiler.agda) | | +| Theorem 4.21 | 𝑀 ⇾ 𝐿 ⇒ 𝐿 ⪰ 𝑀 | `expressiveness-from-compiler` | [src/Vatras/Framework/Relation/Expressiveness.lagda.md](src/Vatras/Framework/Relation/Expressiveness.lagda.md) | | +| Theorem 4.22 | Complete(M) ∧ L ≽ M ⇒ Complete(L) | `completeness-by-expressiveness` | [src/Vatras/Framework/Proof/ForFree.lagda.md](src/Vatras/Framework/Proof/ForFree.lagda.md) | | +| Theorem 4.23 | Sound(L) ∧ L ≽ M ⇒ Sound(M) | `soundness-by-expressiveness` | [src/Vatras/Framework/Proof/ForFree.lagda.md](src/Vatras/Framework/Proof/ForFree.lagda.md) | | +| Theorem 4.24 | Complete(L) ∧ Sound(M) ⇒ L ≽ M | `expressiveness-by-completeness-and-soundness` | [src/Vatras/Framework/Proof/ForFree.lagda.md](src/Vatras/Framework/Proof/ForFree.lagda.md) | | +| Figure 3 | | | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | This file mostly reexports expressiveness results and applies transitivity and the above theorems. It serves as a nice entry point to explore most of our results. | +| Theorem 5.1 | 𝑛-CC | `NCC` | [src/Vatras/Lang/NCC.lagda.md](src/Vatras/Lang/NCC.lagda.md) | | +| | 𝑛-CC ⪰ CCC | `NCC≽CCC` | [src/Vatras/Translation/Lang/CCC-to-NCC.agda](src/Vatras/Translation/Lang/CCC-to-NCC.agda) | | +| | clamp | `Exact.translate` | [src/Vatras/Translation/Lang/CCC-to-NCC.agda](src/Vatras/Translation/Lang/CCC-to-NCC.agda) | | +| | shrink₂ | `shrinkTo2Compiler` | [src/Vatras/Translation/Lang/NCC/ShrinkTo2.agda](src/Vatras/Translation/Lang/NCC/ShrinkTo2.agda) | | +| | grow | `growCompiler` | [src/Vatras/Translation/Lang/NCC/Grow.agda](src/Vatras/Translation/Lang/NCC/Grow.agda) | | +| Theorem 5.3 | ADT ≽ 2CC | `ADT≽2CC` | [src/Vatras/Translation/Lang/2CC-to-ADT.agda](src/Vatras/Translation/Lang/2CC-to-ADT.agda) | | +| Corollary 5.5 | CCC ≡ 2CC ≡ ADT ≡ 𝑛-CC | `CCC≋NCC`, `NCC≋2CC`, and `2CC≋ADT` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Theorem 5.6 | Complete(CaO) | `VariantList-is-Complete` | [src/Vatras/Lang/VariantList.lagda.md](src/Vatras/Lang/VariantList.lagda.md) | | +| Theorem 5.7 | Sound(CaO) | `VariantList-is-Sound` | [src/Vatras/Lang/VariantList.lagda.md](src/Vatras/Lang/VariantList.lagda.md) | | +| Theorem 5.8 | CaO ≽ ADT | `VariantList≽ADT` | [src/Vatras/Translation/Lang/ADT-to-VariantList.agda](src/Vatras/Translation/Lang/ADT-to-VariantList.agda) | | +| Theorem 5.10 | CCC ≽ CaO | `CCC≽VariantList` | [src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md](src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md) | | +| Corollary 5.11 | CCC is complete and sound | `CCC-is-complete`, `CCC-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| | 2CC is complete and sound | `2CC-is-complete`, `2CC-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| | ADT is complete and sound | `ADT-is-complete`, `ADT-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| | 𝑛-CC is complete and sound | `NCC-is-complete`, `NCC-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Theorem 5.12 | 2CC ≽ OC | `2CC≽OC` | [src/Vatras/Translation/Lang/OC-to-2CC.lagda.md](src/Vatras/Translation/Lang/OC-to-2CC.lagda.md) | | +| Corollary 5.13 | Sound(OC) | `OC-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Theorem 5.14 | ¬Complete(OC) | `OC-is-incomplete` | [src/Vatras/Lang/OC.lagda.md](src/Vatras/Lang/OC.lagda.md) | | +| Theorem 5.15 | 2CC ≻ OC | `2CC≻WFOC` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Theorem 5.16 | ¬Complete(FST) | `FST-is-incomplete` | [src/Vatras/Lang/FST.lagda.md](src/Vatras/Lang/FST.lagda.md) | | +| Theorem 5.17 | OC ⋡ FST | `WFOC⋡FST` | [src/Vatras/Translation/Lang/FST-to-OC.lagda.md](src/Vatras/Translation/Lang/FST-to-OC.lagda.md) | | +| Theorem 5.18 | FST ⋡ OC | `FSTL⋡WFOCL` | [src/Vatras/Translation/Lang/OC-to-FST.agda](src/Vatras/Translation/Lang/OC-to-FST.agda) | | +| Corollary 5.19 | FST ⋡ CaO | `FST⋡VariantList` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Theorem 5.20 | CaO ≽ FST | `VariantList≽FST` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | +| Corollary 5.21 | Sound(FST) | `FST-is-sound` | [src/Vatras/Translation/LanguageMap.lagda.md](src/Vatras/Translation/LanguageMap.lagda.md) | | Some formalizations in the library differ slightly from their in-paper-representation: - A few definitions and proofs in this library generalize over the type of variants `V : 𝕍`. -In the paper, this type is fixed to rose trees (see Definition 3.1, trees where each node can have any number of children), which we also formalized in [src/Framework/Variants.agda](src/Framework/Variants.agda) as type `Rose`. +In the paper, this type is fixed to rose trees (see Definition 3.1, trees where each node can have any number of children), which we also formalized in [src/Vatras/Framework/Variants.agda](src/Vatras/Framework/Variants.agda) as type `Rose`. This generalization allows us to also formalize variability languages that -(1) have other variant types such as Gruler's language (see [src/Lang/Gruler.agda](src/Lang/Gruler.agda), Section 3.6 in the paper), or -(2) are independent of the variant type, such as [clone and own](src/Lang/VariantList.lagda.md) (Section 5.2 in the paper). +(1) have other variant types such as Gruler's language (see [src/Vatras/Lang/Gruler.agda](src/Vatras/Lang/Gruler.agda), Section 3.6 in the paper), or +(2) are independent of the variant type, such as [clone and own](src/Vatras/Lang/VariantList.lagda.md) (Section 5.2 in the paper). - Also generalizing over the annotation language `F : 𝔽` was rather easy in the paper (Section 3.3) but requires to carry around that `𝔽` explicitly in Agda in definitions and theorems a lot. #### Frameworks and Dependencies @@ -382,7 +382,7 @@ Of course, there are three exceptions to this. ##### Exception 1 -For the [tutorials](src/Tutorial) (see above), we deliberately use many holes. +For the [tutorials](src/Vatras/Tutorial) (see above), we deliberately use many holes. These holes are intended to be exercises for someone who is working through the tutorial. We also use a terminating macro here to avoid sized types to keep the tutorial simple. The place where we use the macro is proven to terminate throughout the rest @@ -405,7 +405,7 @@ For a non-crucial part of our framework, we included four postulates, which assu - converting `String`s to lists of characters and vice versa, - converting characters to natural numbers and vice versa. -These postulates can be found in [src/Util/String.agda](src/Util/String.agda). +These postulates can be found in [src/Vatras/Util/String.agda](src/Vatras/Util/String.agda). We believe these postulates to be reasonable because strings are commonly _defined_ as lists of characters, and because characters are usually encoded as natural numbers in text encodings (e.g., UTF-8). We use these axioms as an example, to prove that we can simplify annotations `String × ℕ` to just `String`, by turning a pair `s , n` into a String representation `s ++ "." ++ show n`. This simplification only exists to beautify theorems (so they do not have to mention the pair) and align them more closely to our paper but our results would remain the same without that simplification. @@ -421,7 +421,7 @@ In fact, some of these postulates are an open issue [#6119](https://github.com/a If you see an error similar to this one ``` -.../src/MAlonzo/Code/Data/IndexedSet.hs:1705:3: error: +.../src/MAlonzo/Code/Vatras/Data/IndexedSet.hs:1705:3: error: Not in scope: type constructor or class ‘MAlonzo.Code.Agda.Primitive.T_Level_14’ Perhaps you meant ‘MAlonzo.Code.Agda.Primitive.T_Level_18’ (imported from MAlonzo.Code.Agda.Primitive) diff --git a/EPVL.agda-lib b/Vatras.agda-lib similarity index 100% rename from EPVL.agda-lib rename to Vatras.agda-lib diff --git a/flake.nix b/flake.nix index 6049a410..0789519a 100644 --- a/flake.nix +++ b/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; }; diff --git a/makefile b/makefile index dd823dc1..ab294578 100644 --- a/makefile +++ b/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 diff --git a/scripts/find-inconsistency-sources.sh b/scripts/find-inconsistency-sources.sh index fcd94341..a9101cfc 100755 --- a/scripts/find-inconsistency-sources.sh +++ b/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 diff --git a/src/Lang/All.agda b/src/Lang/All.agda deleted file mode 100644 index 7e478f02..00000000 --- a/src/Lang/All.agda +++ /dev/null @@ -1,35 +0,0 @@ -{-| -This module reexports all our language definitions as new modules. -If you intend to work with more than one language in a file -we recommend using this module to easily import the languages you need. --} -module Lang.All where - -import Lang.VariantList -import Lang.CCC -import Lang.NCC -import Lang.2CC -import Lang.NADT -import Lang.ADT -import Lang.OC -import Lang.Gruler - -module VariantList = Lang.VariantList -module CCC = Lang.CCC -module NCC = Lang.NCC -module 2CC = Lang.2CC -module NADT = Lang.NADT -module ADT = Lang.ADT -module OC = Lang.OC -module Gruler = Lang.Gruler - -module FST where - open import Size using (∞) - open import Framework.Definitions using (𝔽; 𝔸) - open import Framework.Variants using (Rose) - 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/Transitive/2CC-to-CCC.agda b/src/Translation/Lang/Transitive/2CC-to-CCC.agda deleted file mode 100644 index cae0919e..00000000 --- a/src/Translation/Lang/Transitive/2CC-to-CCC.agda +++ /dev/null @@ -1,24 +0,0 @@ -module Translation.Lang.Transitive.2CC-to-CCC where - -open import Size using (Size; ∞) -open import Data.Nat using (zero) -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔽) -open import Framework.Variants using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Util.Nat.AtLeast using (sucs) - -open import Lang.All -open CCC using (CCCL) -open 2CC using (2CCL) - -import Translation.Lang.2CC-to-NCC -open Translation.Lang.2CC-to-NCC.2Ary using (2CC→NCC) -open import Translation.Lang.NCC-to-CCC using (NCC→CCC) - - -2CC→CCC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (CCCL D) -2CC→CCC = 2CC→NCC ⊕ NCC→CCC (sucs zero) - -CCC≽2CC : ∀ {D : 𝔽} → CCCL D ≽ 2CCL D -CCC≽2CC = expressiveness-from-compiler 2CC→CCC diff --git a/src/Translation/Lang/Transitive/CCC-to-2CC.agda b/src/Translation/Lang/Transitive/CCC-to-2CC.agda deleted file mode 100644 index ce3f7b42..00000000 --- a/src/Translation/Lang/Transitive/CCC-to-2CC.agda +++ /dev/null @@ -1,25 +0,0 @@ -module Translation.Lang.Transitive.CCC-to-2CC where - -open import Size using (Size; ∞) -open import Data.Nat using (ℕ; zero) -open import Data.Product using (_×_) -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔽) -open import Framework.Variants using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Util.Nat.AtLeast using (sucs) - -open import Lang.All -open CCC using (CCCL) -open 2CC using (2CCL) - -open import Translation.Lang.CCC-to-NCC using (CCC→NCC) -import Translation.Lang.NCC-to-2CC -open Translation.Lang.NCC-to-2CC.2Ary using (NCC→2CC) - - -CCC→2CC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (CCCL {i} D) (2CCL (D × ℕ)) -CCC→2CC = CCC→NCC (sucs zero) ⊕ NCC→2CC - -2CC≽CCC : ∀ {D : 𝔽} → 2CCL (D × ℕ) ≽ CCCL D -2CC≽CCC = expressiveness-from-compiler CCC→2CC diff --git a/src/Data/EqIndexedSet.agda b/src/Vatras/Data/EqIndexedSet.agda similarity index 68% rename from src/Data/EqIndexedSet.agda rename to src/Vatras/Data/EqIndexedSet.agda index 2ad79472..40acd659 100644 --- a/src/Data/EqIndexedSet.agda +++ b/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 diff --git a/src/Data/IndexedSet.lagda.md b/src/Vatras/Data/IndexedSet.lagda.md similarity index 99% rename from src/Data/IndexedSet.lagda.md rename to src/Vatras/Data/IndexedSet.lagda.md index cfaa4b2b..b520e52e 100644 --- a/src/Data/IndexedSet.lagda.md +++ b/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 diff --git a/src/Framework/Annotation/IndexedDimension.agda b/src/Vatras/Framework/Annotation/IndexedDimension.agda similarity index 74% rename from src/Framework/Annotation/IndexedDimension.agda rename to src/Vatras/Framework/Annotation/IndexedDimension.agda index 2da8576b..466f3623 100644 --- a/src/Framework/Annotation/IndexedDimension.agda +++ b/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 diff --git a/src/Framework/Annotation/Negatable.agda b/src/Vatras/Framework/Annotation/Negatable.agda similarity index 88% rename from src/Framework/Annotation/Negatable.agda rename to src/Vatras/Framework/Annotation/Negatable.agda index 05956ca3..21b27187 100644 --- a/src/Framework/Annotation/Negatable.agda +++ b/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) {-| diff --git a/src/Framework/Compiler.agda b/src/Vatras/Framework/Compiler.agda similarity index 92% rename from src/Framework/Compiler.agda rename to src/Vatras/Framework/Compiler.agda index 9128f36d..42898a06 100644 --- a/src/Framework/Compiler.agda +++ b/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 diff --git a/src/Framework/Composition/FeatureAlgebra.lagda.md b/src/Vatras/Framework/Composition/FeatureAlgebra.lagda.md similarity index 99% rename from src/Framework/Composition/FeatureAlgebra.lagda.md rename to src/Vatras/Framework/Composition/FeatureAlgebra.lagda.md index ac3cb7ec..b361fdf6 100644 --- a/src/Framework/Composition/FeatureAlgebra.lagda.md +++ b/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) diff --git a/src/Framework/Definitions.agda b/src/Vatras/Framework/Definitions.agda similarity index 94% rename from src/Framework/Definitions.agda rename to src/Vatras/Framework/Definitions.agda index 97222b77..825fd651 100644 --- a/src/Framework/Definitions.agda +++ b/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₁ diff --git a/src/Framework/Proof/ForFree.lagda.md b/src/Vatras/Framework/Proof/ForFree.lagda.md similarity index 94% rename from src/Framework/Proof/ForFree.lagda.md rename to src/Vatras/Framework/Proof/ForFree.lagda.md index 7e447be2..46ff90af 100644 --- a/src/Framework/Proof/ForFree.lagda.md +++ b/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 diff --git a/src/Framework/Properties/Completeness.lagda.md b/src/Vatras/Framework/Properties/Completeness.lagda.md similarity index 79% rename from src/Framework/Properties/Completeness.lagda.md rename to src/Vatras/Framework/Properties/Completeness.lagda.md index 673282c1..0f0534f0 100644 --- a/src/Framework/Properties/Completeness.lagda.md +++ b/src/Vatras/Framework/Properties/Completeness.lagda.md @@ -3,8 +3,8 @@ ## 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 @@ -12,9 +12,9 @@ module Framework.Properties.Completeness (V : 𝕍) where ```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 diff --git a/src/Framework/Properties/Finity.agda b/src/Vatras/Framework/Properties/Finity.agda similarity index 75% rename from src/Framework/Properties/Finity.agda rename to src/Vatras/Framework/Properties/Finity.agda index 181660f8..b107ece4 100644 --- a/src/Framework/Properties/Finity.agda +++ b/src/Vatras/Framework/Properties/Finity.agda @@ -1,10 +1,10 @@ -open import Framework.Definitions using (𝕍) +open import Vatras.Framework.Definitions using (𝕍) {-| This module contains definition to say that a variability language denotes a finite set of variants. -} -module Framework.Properties.Finity (V : 𝕍) where +module Vatras.Framework.Properties.Finity (V : 𝕍) where open import Data.Product using (_,_) open import Function using (_∘_; Surjective; Congruent) @@ -12,12 +12,12 @@ open import Function using (_∘_; Surjective; Congruent) open import Relation.Binary using (IsEquivalence) open import Relation.Binary.PropositionalEquality as Eq using (_≡_) -open import Framework.VariabilityLanguage -open import Framework.Relation.Configuration V using (_∋_⊢_≣ⁱ_; ≣ⁱ-IsEquivalence; ≣ⁱ-congruent; ≣ⁱ-setoid) -open import Framework.Properties.Soundness V -open import Framework.Relation.Expression V -open import Data.EqIndexedSet -open import Util.Enumerable +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Relation.Configuration V using (_∋_⊢_≣ⁱ_; ≣ⁱ-IsEquivalence; ≣ⁱ-congruent; ≣ⁱ-setoid) +open import Vatras.Framework.Properties.Soundness V +open import Vatras.Framework.Relation.Expression V +open import Vatras.Data.EqIndexedSet +open import Vatras.Util.Enumerable {-| A variability language satisfies this predicate diff --git a/src/Framework/Properties/NonEmpty.agda b/src/Vatras/Framework/Properties/NonEmpty.agda similarity index 78% rename from src/Framework/Properties/NonEmpty.agda rename to src/Vatras/Framework/Properties/NonEmpty.agda index 7688efb6..d843302f 100644 --- a/src/Framework/Properties/NonEmpty.agda +++ b/src/Vatras/Framework/Properties/NonEmpty.agda @@ -2,10 +2,10 @@ This module provides definitions to say that the semantics of a variability language are non-empty. -} -module Framework.Properties.NonEmpty where +module Vatras.Framework.Properties.NonEmpty where -open import Framework.VariabilityLanguage using (VariabilityLanguage; Expression; Config; Semantics) -open import Data.EqIndexedSet +open import Vatras.Framework.VariabilityLanguage using (VariabilityLanguage; Expression; Config; Semantics) +open import Vatras.Data.EqIndexedSet {-| A variability language is not empty if there exists at least one configuration for each expression. diff --git a/src/Framework/Properties/Soundness.lagda.md b/src/Vatras/Framework/Properties/Soundness.lagda.md similarity index 75% rename from src/Framework/Properties/Soundness.lagda.md rename to src/Vatras/Framework/Properties/Soundness.lagda.md index f9eafc58..8842f006 100644 --- a/src/Framework/Properties/Soundness.lagda.md +++ b/src/Vatras/Framework/Properties/Soundness.lagda.md @@ -3,8 +3,8 @@ ## Module ```agda -open import Framework.Definitions using (𝕍) -module Framework.Properties.Soundness (V : 𝕍) where +open import Vatras.Framework.Definitions using (𝕍) +module Vatras.Framework.Properties.Soundness (V : 𝕍) where ``` ## Imports @@ -12,9 +12,9 @@ module Framework.Properties.Soundness (V : 𝕍) where ```agda open import Data.Product using (∃-syntax; Σ-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 diff --git a/src/Framework/Relation/Configuration.lagda.md b/src/Vatras/Framework/Relation/Configuration.lagda.md similarity index 89% rename from src/Framework/Relation/Configuration.lagda.md rename to src/Vatras/Framework/Relation/Configuration.lagda.md index 7df489ff..ec3cf9d6 100644 --- a/src/Framework/Relation/Configuration.lagda.md +++ b/src/Vatras/Framework/Relation/Configuration.lagda.md @@ -1,15 +1,15 @@ # Definitions for Relating Configurations. ```agda -open import Framework.Definitions using (𝕍; 𝔸) -module Framework.Relation.Configuration (V : 𝕍) where +open import Vatras.Framework.Definitions using (𝕍; 𝔸) +module Vatras.Framework.Relation.Configuration (V : 𝕍) where open import Level using (0ℓ; suc) open import Relation.Binary using (Setoid; IsEquivalence) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl; sym; trans) open import Function using (_∘_; Congruent) -open import Framework.VariabilityLanguage -open import Data.EqIndexedSet +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Data.EqIndexedSet ``` This module defines semantic equivalence of configurations. diff --git a/src/Framework/Relation/Expression.lagda.md b/src/Vatras/Framework/Relation/Expression.lagda.md similarity index 95% rename from src/Framework/Relation/Expression.lagda.md rename to src/Vatras/Framework/Relation/Expression.lagda.md index f46b3e4a..475d87e8 100644 --- a/src/Framework/Relation/Expression.lagda.md +++ b/src/Vatras/Framework/Relation/Expression.lagda.md @@ -9,8 +9,8 @@ by reusing the definitions in here. The proofs and definitions in this module mostly amount to reusing indexed sets and their relations. ```agda -open import Framework.Definitions -module Framework.Relation.Expression (V : 𝕍) {A : 𝔸} where +open import Vatras.Framework.Definitions +module Vatras.Framework.Relation.Expression (V : 𝕍) {A : 𝔸} where open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂) open import Relation.Nullary.Negation using (¬_) @@ -18,9 +18,9 @@ open import Relation.Binary using (IsEquivalence; Reflexive; Symmetric; Transiti open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans) open import Function using (_∘_; Injective) -open import Framework.VariabilityLanguage +open import Vatras.Framework.VariabilityLanguage -open import Data.EqIndexedSet using +open import Vatras.Data.EqIndexedSet using ( _⊆_; _≅_; _≐_ ; ≐→≅ ; ⊆-refl; ⊆-antisym; ⊆-trans diff --git a/src/Framework/Relation/Expressiveness.lagda.md b/src/Vatras/Framework/Relation/Expressiveness.lagda.md similarity index 94% rename from src/Framework/Relation/Expressiveness.lagda.md rename to src/Vatras/Framework/Relation/Expressiveness.lagda.md index ed8f8172..860ca9e8 100644 --- a/src/Framework/Relation/Expressiveness.lagda.md +++ b/src/Vatras/Framework/Relation/Expressiveness.lagda.md @@ -1,10 +1,10 @@ # Expressiveness of Languages for Static Variability ```agda -open import Framework.Definitions -module Framework.Relation.Expressiveness (V : 𝕍) where +open import Vatras.Framework.Definitions +module Vatras.Framework.Relation.Expressiveness (V : 𝕍) where -open import Data.EqIndexedSet using (≅[]→≅) +open import Vatras.Data.EqIndexedSet using (≅[]→≅) open import Data.Empty using (⊥) open import Data.Product using (_,_; _×_; Σ-syntax; proj₁; proj₂) open import Relation.Nullary.Negation using (¬_; contraposition) @@ -12,10 +12,10 @@ open import Relation.Binary open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans) open import Function using (_∘_; Injective) -open import Framework.VariabilityLanguage -open import Framework.Relation.Expression V -open import Framework.Relation.Function using (_⇒ₚ_) -open import Framework.Compiler +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Relation.Expression V +open import Vatras.Framework.Relation.Function using (_⇒ₚ_) +open import Vatras.Framework.Compiler ``` This module contains the basic definition of (relative) expressiveness `_≽_`, @@ -186,7 +186,7 @@ compiler-from-expressiveness {L} {M} exp = record ; preserves = ≅→≅[] ∘ proj₂ ∘ exp } where - open import Data.EqIndexedSet + open import Vatras.Data.EqIndexedSet {-| When M is not at least as expressive as L, diff --git a/src/Framework/Relation/Function.agda b/src/Vatras/Framework/Relation/Function.agda similarity index 94% rename from src/Framework/Relation/Function.agda rename to src/Vatras/Framework/Relation/Function.agda index 5535993d..e678b6fc 100644 --- a/src/Framework/Relation/Function.agda +++ b/src/Vatras/Framework/Relation/Function.agda @@ -3,9 +3,9 @@ This module contains some helper types for dealing with functions on the syntax of variability languages. -} -module Framework.Relation.Function where +module Vatras.Framework.Relation.Function where -open import Framework.Definitions +open import Vatras.Framework.Definitions open import Relation.Binary.PropositionalEquality as Eq using (_≗_; _≡_) open import Function using (id; _∘_; Injective) diff --git a/src/Framework/VariabilityLanguage.agda b/src/Vatras/Framework/VariabilityLanguage.agda similarity index 89% rename from src/Framework/VariabilityLanguage.agda rename to src/Vatras/Framework/VariabilityLanguage.agda index 1a4f097e..6681ac21 100644 --- a/src/Framework/VariabilityLanguage.agda +++ b/src/Vatras/Framework/VariabilityLanguage.agda @@ -1,9 +1,9 @@ {-| This module formalizes languages for static variability. -} -module Framework.VariabilityLanguage where +module Vatras.Framework.VariabilityLanguage where -open import Framework.Definitions +open import Vatras.Framework.Definitions {-| A common semantics for variability languages is diff --git a/src/Framework/VariantGenerator.agda b/src/Vatras/Framework/VariantGenerator.agda similarity index 88% rename from src/Framework/VariantGenerator.agda rename to src/Vatras/Framework/VariantGenerator.agda index 3f537cef..f7e9f819 100644 --- a/src/Framework/VariantGenerator.agda +++ b/src/Vatras/Framework/VariantGenerator.agda @@ -1,5 +1,5 @@ -open import Framework.Definitions using (𝕍; 𝔸) -module Framework.VariantGenerator (V : 𝕍) (A : 𝔸) where +open import Vatras.Framework.Definitions using (𝕍; 𝔸) +module Vatras.Framework.VariantGenerator (V : 𝕍) (A : 𝔸) where open import Data.Fin using (Fin) open import Data.List using (List) @@ -9,7 +9,7 @@ open import Level using (0ℓ) open import Relation.Binary using (Setoid) import Relation.Binary.PropositionalEquality as Eq -open import Data.EqIndexedSet {A = V A} +open import Vatras.Data.EqIndexedSet {A = V A} {-| Variant maps constitute the semantic domain of variability languages. diff --git a/src/Framework/Variants.agda b/src/Vatras/Framework/Variants.agda similarity index 95% rename from src/Framework/Variants.agda rename to src/Vatras/Framework/Variants.agda index 0664c625..ddf7f994 100644 --- a/src/Framework/Variants.agda +++ b/src/Vatras/Framework/Variants.agda @@ -3,7 +3,7 @@ This module defines variant types for variability languages. In particular, we define Rose trees here as we use in our paper. -} -module Framework.Variants where +module Vatras.Framework.Variants where open import Data.List using (List; []; _∷_; map) open import Data.Maybe using (nothing; just) @@ -16,9 +16,9 @@ open Eq.≡-Reasoning open import Function using (id; _∘_; flip) open import Size using (Size; ↑_; ∞) -open import Framework.Definitions using (𝕍; 𝔸; atoms) -open import Framework.VariabilityLanguage -open import Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝕍; 𝔸; atoms) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Compiler using (LanguageCompiler) open LanguageCompiler {-| @@ -99,7 +99,7 @@ VariantEncoder V L = LanguageCompiler (Variant-is-VL V) L This module groups some interesting properties of variant encoders. -} module _ (V : 𝕍) (A : 𝔸) {L : VariabilityLanguage V} (encoder : VariantEncoder V L) where - open import Data.EqIndexedSet + open import Vatras.Data.EqIndexedSet private ⟦_⟧ = Semantics L diff --git a/src/Lang/2CC.lagda.md b/src/Vatras/Lang/2CC.lagda.md similarity index 96% rename from src/Lang/2CC.lagda.md rename to src/Vatras/Lang/2CC.lagda.md index fa2c175b..0714eeb4 100644 --- a/src/Lang/2CC.lagda.md +++ b/src/Vatras/Lang/2CC.lagda.md @@ -3,8 +3,8 @@ ## Module ```agda -open import Framework.Definitions -module Lang.2CC where +open import Vatras.Framework.Definitions +module Vatras.Lang.2CC where ``` ## Imports @@ -18,8 +18,8 @@ open import Data.Product using (_,_) open import Function using (id) open import Size using (Size; ↑_; ∞) -open import Framework.Variants as V using (Rose) -open import Framework.VariabilityLanguage +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.VariabilityLanguage ``` ## Syntax @@ -77,12 +77,12 @@ Some transformation rules: open import Data.Nat using (ℕ) open import Data.Vec as Vec using (Vec; toList; zipWith) import Data.Vec.Properties as Vec - import Util.Vec as Vec + import Vatras.Util.Vec as Vec open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) module Properties where - open import Framework.Relation.Expression (Rose ∞) + open import Vatras.Framework.Relation.Expression (Rose ∞) module _ {A : 𝔸} where {-| @@ -198,7 +198,7 @@ Some transformation rules: ```agda open import Data.String as String using (String; _++_; intersperse) module Pretty (show-D : Dimension → String) where - open import Show.Lines + open import Vatras.Show.Lines show : ∀ {i} → 2CC Dimension i (String , String._≟_) → String show (a -< [] >-) = a diff --git a/src/Lang/ADT.agda b/src/Vatras/Lang/ADT.agda similarity index 90% rename from src/Lang/ADT.agda rename to src/Vatras/Lang/ADT.agda index bf102455..9b5c25f1 100644 --- a/src/Lang/ADT.agda +++ b/src/Vatras/Lang/ADT.agda @@ -1,11 +1,11 @@ {-| This module defines algebraic decision trees as defined in our paper. -} -module Lang.ADT where +module Vatras.Lang.ADT where open import Data.Bool using (Bool; if_then_else_) -open import Framework.Definitions -open import Framework.VariabilityLanguage +open import Vatras.Framework.Definitions +open import Vatras.Framework.VariabilityLanguage {-| An algebraic decision tree stores variants in leaf nodes @@ -34,7 +34,7 @@ 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 +open import Vatras.Show.Lines {-| Pretty printer for ADTs. diff --git a/src/Lang/ADT/Path.agda b/src/Vatras/Lang/ADT/Path.agda similarity index 96% rename from src/Lang/ADT/Path.agda rename to src/Vatras/Lang/ADT/Path.agda index b5cec613..a7c86b20 100644 --- a/src/Lang/ADT/Path.agda +++ b/src/Vatras/Lang/ADT/Path.agda @@ -2,9 +2,9 @@ This module defines paths in ASTs from the root to a leaf. We use paths to reason on dead branches later on. -} -open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) +open import Vatras.Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) open import Relation.Binary using (DecidableEquality; Rel) -module Lang.ADT.Path +module Vatras.Lang.ADT.Path (F : 𝔽) (V : 𝕍) (_==_ : DecidableEquality F) @@ -28,9 +28,9 @@ open import Relation.Binary using (Decidable; Symmetric) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open Eq.≡-Reasoning -open import Framework.VariabilityLanguage -open import Util.Suffix using (_endswith_) -open import Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Util.Suffix using (_endswith_) +open import Vatras.Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧) -- A selection of a feature matches it to a boolean value. record Selection : Set where diff --git a/src/Vatras/Lang/All.agda b/src/Vatras/Lang/All.agda new file mode 100644 index 00000000..9838ccde --- /dev/null +++ b/src/Vatras/Lang/All.agda @@ -0,0 +1,35 @@ +{-| +This module reexports all our language definitions as new modules. +If you intend to work with more than one language in a file +we recommend using this module to easily import the languages you need. +-} +module Vatras.Lang.All where + +import Vatras.Lang.VariantList +import Vatras.Lang.CCC +import Vatras.Lang.NCC +import Vatras.Lang.2CC +import Vatras.Lang.NADT +import Vatras.Lang.ADT +import Vatras.Lang.OC +import Vatras.Lang.Gruler + +module VariantList = Vatras.Lang.VariantList +module CCC = Vatras.Lang.CCC +module NCC = Vatras.Lang.NCC +module 2CC = Vatras.Lang.2CC +module NADT = Vatras.Lang.NADT +module ADT = Vatras.Lang.ADT +module OC = Vatras.Lang.OC +module Gruler = Vatras.Lang.Gruler + +module FST where + open import Size using (∞) + open import Vatras.Framework.Definitions using (𝔽; 𝔸) + open import Vatras.Framework.Variants using (Rose) + open import Vatras.Lang.FST hiding (FST; FSTL-Sem; Conf) public + + Configuration = Vatras.Lang.FST.Conf + + ⟦_⟧ : ∀ {F : 𝔽} {A : 𝔸} → Impose.SPL F A → Configuration F → Rose ∞ A + ⟦_⟧ {F} = Vatras.Lang.FST.FSTL-Sem F diff --git a/src/Lang/CCC.lagda.md b/src/Vatras/Lang/CCC.lagda.md similarity index 93% rename from src/Lang/CCC.lagda.md rename to src/Vatras/Lang/CCC.lagda.md index b28bdaaf..9e5dc859 100644 --- a/src/Lang/CCC.lagda.md +++ b/src/Vatras/Lang/CCC.lagda.md @@ -1,8 +1,8 @@ # Core Choice Calculus ```agda -open import Framework.Definitions -module Lang.CCC where +open import Vatras.Framework.Definitions +module Vatras.Lang.CCC where ``` ## Imports @@ -16,11 +16,11 @@ open import Data.Nat using (ℕ) open import Function using (id; _∘_; _$_) open import Size using (Size; ↑_; ∞) -open import Framework.Variants as V using (Rose; VariantEncoder; Variant-is-VL) -open import Framework.VariabilityLanguage -open import Util.List using (find-or-last) +open import Vatras.Framework.Variants as V using (Rose; VariantEncoder; Variant-is-VL) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Util.List using (find-or-last) -open import Data.EqIndexedSet as ISet +open import Vatras.Data.EqIndexedSet as ISet ``` ## Syntax @@ -77,7 +77,7 @@ Some interesting properties: ```agda module Properties where - open import Framework.Relation.Expression (Rose ∞) + open import Vatras.Framework.Relation.Expression (Rose ∞) module _ {A : 𝔸} where {-| @@ -113,7 +113,7 @@ Such behavior is implemented in terms of [variant encoders](../Framework/Variant We can encode a variant in core choice calculus by using only the artifact constructor and no choices. ```agda module Encode where - open import Framework.Relation.Function using (_⇔_; to; from) + open import Vatras.Framework.Relation.Function using (_⇔_; to; from) open import Data.List.Properties using (map-∘; map-id; map-cong) open Eq.≡-Reasoning @@ -186,7 +186,7 @@ Recursively, collect all dimensions used in a CCC expression: ## Show ```agda - open import Show.Lines hiding (map) + open import Vatras.Show.Lines hiding (map) open import Data.String as String using (String; _++_) show : ∀ {i} → (Dimension → String) → CCC Dimension i (String , String._≟_) → String diff --git a/src/Lang/FST.lagda.md b/src/Vatras/Lang/FST.lagda.md similarity index 98% rename from src/Lang/FST.lagda.md rename to src/Vatras/Lang/FST.lagda.md index e56a8e63..073bd204 100644 --- a/src/Lang/FST.lagda.md +++ b/src/Vatras/Lang/FST.lagda.md @@ -2,9 +2,9 @@ This module formalizes feature structure trees. We formalize the language, its semantics, and the typing to disallow duplicate neighbors. ```agda -open import Framework.Definitions +open import Vatras.Framework.Definitions -module Lang.FST (F : 𝔽) where +module Vatras.Lang.FST (F : 𝔽) where open import Data.Bool using (Bool; true; false; if_then_else_) open import Data.List using (List; []; _∷_; _∷ʳ_; _++_; foldl; foldr; map; filterᵇ; concat; reverse) @@ -29,12 +29,12 @@ open import Relation.Binary using (Decidable; DecidableEquality; Rel) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open Eq.≡-Reasoning -open import Framework.Variants using (Rose; _-<_>-; rose-leaf; children-equality) -open import Framework.Composition.FeatureAlgebra -open import Framework.VariabilityLanguage +open import Vatras.Framework.Variants using (Rose; _-<_>-; rose-leaf; children-equality) +open import Vatras.Framework.Composition.FeatureAlgebra +open import Vatras.Framework.VariabilityLanguage -open import Util.Function using (cong-app₂) -open import Util.List using (++-tail) +open import Vatras.Util.Function using (cong-app₂) +open import Vatras.Util.List using (++-tail) ``` ## Basic Definitions @@ -851,7 +851,7 @@ We now prove that feature structure trees form a feature algebra. ```agda open import Data.String using (String; _<+>_) - open import Show.Lines hiding (map) + open import Vatras.Show.Lines hiding (map) module Show (show-F : F → String) (show-A : A → String) where mutual @@ -891,8 +891,8 @@ with exactly two disjunct variants. module IncompleteOnRose where open import Data.Fin using (zero; suc) open import Data.Nat as ℕ using (ℕ; zero; suc) - open import Framework.VariantGenerator using (VariantGenerator) - open import Framework.Properties.Completeness using (Incomplete) + open import Vatras.Framework.VariantGenerator using (VariantGenerator) + open import Vatras.Framework.Properties.Completeness using (Incomplete) variant-0 = rose-leaf {A = (ℕ , ℕ._≟_)} 0 variant-1 = rose-leaf {A = (ℕ , ℕ._≟_)} 1 diff --git a/src/Lang/Gruler.agda b/src/Vatras/Lang/Gruler.agda similarity index 88% rename from src/Lang/Gruler.agda rename to src/Vatras/Lang/Gruler.agda index 139672a4..04630e4e 100644 --- a/src/Lang/Gruler.agda +++ b/src/Vatras/Lang/Gruler.agda @@ -3,8 +3,8 @@ This module defines Gruler's language as defined in our paper. While the original formalization uses natural numbers to name choices, we allow any kind of annotation language F here without any loss of generality. -} -open import Framework.Definitions -module Lang.Gruler (F : 𝔽) where +open import Vatras.Framework.Definitions +module Vatras.Lang.Gruler (F : 𝔽) where open import Data.Bool using (Bool; if_then_else_) open import Data.Maybe using (Maybe; just; nothing) @@ -14,8 +14,8 @@ import Level open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Framework.VariabilityLanguage -open import Framework.Variants using (GrulerVariant; ε; asset; _∥_) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Variants using (GrulerVariant; ε; asset; _∥_) {-| A simplified syntax of Gruler's language from: diff --git a/src/Lang/NADT.agda b/src/Vatras/Lang/NADT.agda similarity index 82% rename from src/Lang/NADT.agda rename to src/Vatras/Lang/NADT.agda index 3f2cfff4..c0f3f4b0 100644 --- a/src/Lang/NADT.agda +++ b/src/Vatras/Lang/NADT.agda @@ -1,14 +1,14 @@ -module Lang.NADT where +module Vatras.Lang.NADT where open import Data.Nat using (ℕ) open import Data.List.NonEmpty using (List⁺) open import Function using (id) open import Size using (Size; ↑_) -open import Framework.Definitions -open import Framework.VariabilityLanguage -open import Framework.Variants using (GrulerVariant) -open import Util.List using (find-or-last) +open import Vatras.Framework.Definitions +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Variants using (GrulerVariant) +open import Vatras.Util.List using (find-or-last) {-| A generalisation of algebraic decision trees diff --git a/src/Lang/NCC.lagda.md b/src/Vatras/Lang/NCC.lagda.md similarity index 92% rename from src/Lang/NCC.lagda.md rename to src/Vatras/Lang/NCC.lagda.md index 4f428cc0..5c9d50bc 100644 --- a/src/Lang/NCC.lagda.md +++ b/src/Vatras/Lang/NCC.lagda.md @@ -11,9 +11,9 @@ In our paper, we also only inspect the languages with `n ≥ 2`. ## Module ```agda -open import Framework.Definitions -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥) -module Lang.NCC where +open import Vatras.Framework.Definitions +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥) +module Vatras.Lang.NCC where ``` ## Imports @@ -29,8 +29,8 @@ open import Data.Product using (_,_) open import Function using (id) open import Size using (Size; ↑_; ∞) -open import Framework.Variants as V using (Rose) -open import Framework.VariabilityLanguage +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.VariabilityLanguage ``` ## Syntax @@ -85,7 +85,7 @@ Recursively, collect all dimensions used in an n-CC expression: ```agda open import Data.String as String using (String; _++_; intersperse) module Pretty (show-D : Dimension → String) where - open import Show.Lines + open import Vatras.Show.Lines show : ∀ {i} → NCC n Dimension i (String , String._≟_) → String show (a -< [] >-) = a diff --git a/src/Lang/OC.lagda.md b/src/Vatras/Lang/OC.lagda.md similarity index 95% rename from src/Lang/OC.lagda.md rename to src/Vatras/Lang/OC.lagda.md index b4650b72..9fe52283 100644 --- a/src/Lang/OC.lagda.md +++ b/src/Vatras/Lang/OC.lagda.md @@ -6,8 +6,8 @@ we introduce to capture variability with exactly and only optional variability. ## Module ```agda -open import Framework.Definitions -module Lang.OC where +open import Vatras.Framework.Definitions +module Vatras.Lang.OC where ``` ## Imports @@ -19,8 +19,8 @@ open import Data.String as String using (String) open import Size using (Size; ∞; ↑_) open import Function using (_∘_) -open import Framework.Variants as V using (Rose; rose-leaf) -open import Framework.VariabilityLanguage +open import Vatras.Framework.Variants as V using (Rose; rose-leaf) +open import Vatras.Framework.VariabilityLanguage ``` ## Syntax @@ -135,7 +135,7 @@ WFOCL {i} Option = ⟪ WFOC Option i , Configuration Option , ⟦_⟧ ⟫ open import Data.Fin using (zero; suc) open import Data.Nat as ℕ using (ℕ; zero; suc) open import Data.Product using (_,_; ∃-syntax; ∄-syntax) -open import Util.Existence using (_,_) +open import Vatras.Util.Existence using (_,_) open import Data.List.Relation.Unary.All using (_∷_; []) open import Data.Empty using (⊥) open import Relation.Binary.PropositionalEquality using (_≡_) @@ -148,8 +148,8 @@ In particular, any set of variants that includes two entirely distinct variants As our counter example, we use the set `{0, 1}` as our variants: ```agda module IncompleteOnRose where - open import Framework.VariantGenerator (Rose ∞) (ℕ , ℕ._≟_) - open import Framework.Properties.Completeness (Rose ∞) using (Incomplete) + open import Vatras.Framework.VariantGenerator (Rose ∞) (ℕ , ℕ._≟_) + open import Vatras.Framework.Properties.Completeness (Rose ∞) using (Incomplete) variant-0 = rose-leaf {A = (ℕ , ℕ._≟_)} 0 variant-1 = rose-leaf {A = (ℕ , ℕ._≟_)} 1 @@ -199,7 +199,7 @@ Another way is to enrich the annotation language, for example using propositiona singleton : ∀ {i : Size} {A : 𝔸} → atoms A → OC Option i A → OC Option (↑ i) A singleton a e = a -< e ∷ [] >- - open import Util.Named + open import Vatras.Util.Named {-| Creates a constant configuration, fixed to the given boolean value. @@ -225,7 +225,7 @@ Another way is to enrich the annotation language, for example using propositiona ## Show ```agda -open import Show.Lines hiding (map) +open import Vatras.Show.Lines hiding (map) open String using (_++_; intersperse) open import Function using (_∘_) diff --git a/src/Lang/OC/Alternative.agda b/src/Vatras/Lang/OC/Alternative.agda similarity index 88% rename from src/Lang/OC/Alternative.agda rename to src/Vatras/Lang/OC/Alternative.agda index 6742d36a..1ca6ca34 100644 --- a/src/Lang/OC/Alternative.agda +++ b/src/Vatras/Lang/OC/Alternative.agda @@ -3,7 +3,7 @@ This module proves that option calculus cannot encode alternatives, at the example of natural numbers as the atom set. The proof is restricted to variants with alternatives at their root. -} -module Lang.OC.Alternative where +module Vatras.Lang.OC.Alternative where open import Data.List using (List; []; _∷_) open import Data.Sum as Sum using (_⊎_; inj₁; inj₂) @@ -14,11 +14,11 @@ open import Data.Product using (_,_; ∃-syntax) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Size using (∞) -open import Framework.Definitions using (𝔽; 𝔸; atoms) -open import Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality) -open import Lang.All +open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms) +open import Vatras.Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality) +open import Vatras.Lang.All open OC using (WFOC; Root; all-oc) -open import Lang.OC.Subtree using (Subtree; subtrees; subtreeₒ-recurse) +open import Vatras.Lang.OC.Subtree using (Subtree; subtrees; subtreeₒ-recurse) A : 𝔸 A = ℕ , _≟_ diff --git a/src/Lang/OC/Properties.agda b/src/Vatras/Lang/OC/Properties.agda similarity index 81% rename from src/Lang/OC/Properties.agda rename to src/Vatras/Lang/OC/Properties.agda index eb04a151..5abbf358 100644 --- a/src/Lang/OC/Properties.agda +++ b/src/Vatras/Lang/OC/Properties.agda @@ -2,7 +2,7 @@ This module contains proofs of some basic properties of option calculus. -} -module Lang.OC.Properties where +module Vatras.Lang.OC.Properties where open import Data.Bool using (true) open import Data.Maybe using (just) @@ -10,9 +10,9 @@ open import Data.Product using (_,_; ∃-syntax) open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Size using (∞) -open import Framework.Definitions using (𝔽; 𝔸) -import Framework.Variants as V -open import Lang.All +open import Vatras.Framework.Definitions using (𝔽; 𝔸) +import Vatras.Framework.Variants as V +open import Vatras.Lang.All open OC using (OC; _-<_>-; _❲_❳; ⟦_⟧ₒ; ⟦_⟧ₒ-recurse; all-oc) {-| diff --git a/src/Lang/OC/Subtree.lagda.md b/src/Vatras/Lang/OC/Subtree.lagda.md similarity index 95% rename from src/Lang/OC/Subtree.lagda.md rename to src/Vatras/Lang/OC/Subtree.lagda.md index e8b9a3c4..f54b323f 100644 --- a/src/Lang/OC/Subtree.lagda.md +++ b/src/Vatras/Lang/OC/Subtree.lagda.md @@ -3,7 +3,7 @@ This module introduces reasoning on subtrees of variants and in option calculus. ```agda -module Lang.OC.Subtree where +module Vatras.Lang.OC.Subtree where open import Data.Bool using (true; false) open import Data.Empty using (⊥-elim) @@ -13,10 +13,10 @@ open import Data.Maybe using (Maybe; nothing; just) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Size using (∞) -open import Framework.Definitions using (𝔽; 𝔸; atoms) -open import Framework.Variants as V hiding (_-<_>-) -open import Lang.OC -open import Util.AuxProofs using (true≢false) +open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms) +open import Vatras.Framework.Variants as V hiding (_-<_>-) +open import Vatras.Lang.OC +open import Vatras.Util.AuxProofs using (true≢false) ``` Relates two variants iff the first argument is a subtree of the second argument. diff --git a/src/Lang/VariantList.lagda.md b/src/Vatras/Lang/VariantList.lagda.md similarity index 90% rename from src/Lang/VariantList.lagda.md rename to src/Vatras/Lang/VariantList.lagda.md index 8a9ae22c..da8f7524 100644 --- a/src/Lang/VariantList.lagda.md +++ b/src/Vatras/Lang/VariantList.lagda.md @@ -7,8 +7,8 @@ Formally, expressing variability in this way amounts to declaring a list of vari ## Module ```agda -open import Framework.Definitions -module Lang.VariantList (V : 𝕍) where +open import Vatras.Framework.Definitions +module Vatras.Lang.VariantList (V : 𝕍) where ``` ## Imports @@ -23,13 +23,13 @@ open import Function using (_∘_; Surjective) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) -open import Framework.VariabilityLanguage -open import Framework.Properties.Completeness V using (Complete) -open import Framework.Properties.Soundness V using (Sound) -open import Framework.Properties.Finity V using (soundness-from-enumerability) -open import Framework.Relation.Configuration V using (_∋_⊢_≣ⁱ_) -open import Data.EqIndexedSet as ISet -open import Util.List using (find-or-last) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Properties.Completeness V using (Complete) +open import Vatras.Framework.Properties.Soundness V using (Sound) +open import Vatras.Framework.Properties.Finity V using (soundness-from-enumerability) +open import Vatras.Framework.Relation.Configuration V using (_∋_⊢_≣ⁱ_) +open import Vatras.Data.EqIndexedSet as ISet +open import Vatras.Util.List using (find-or-last) ``` ## Syntax @@ -84,10 +84,10 @@ These proofs will form the basis for proving these properties for other language To prove completeness, we have to show that lists of variants can express any variant map. ```agda -open import Util.Nat.AtLeast using (cappedFin) +open import Vatras.Util.Nat.AtLeast using (cappedFin) private - open import Framework.VariantGenerator V + open import Vatras.Framework.VariantGenerator V variable n : ℕ A : 𝔸 @@ -210,7 +210,7 @@ VariantList-is-Sound e = ```agda open import Data.String as String using (String; _++_; intersperse) open import Data.Product using (_,_) -open import Show.Lines +open import Vatras.Show.Lines pretty : {A : 𝔸} → (V A → String) → VariantList A → Lines pretty {A} pretty-variant (v ∷ vs) = do diff --git a/src/Main.agda b/src/Vatras/Main.agda similarity index 69% rename from src/Main.agda rename to src/Vatras/Main.agda index 5e150718..e5fb8df7 100644 --- a/src/Main.agda +++ b/src/Vatras/Main.agda @@ -1,6 +1,6 @@ {-# OPTIONS --guardedness --allow-unsolved-metas #-} -module Main where +module Vatras.Main where open import Level using (0ℓ; suc) @@ -9,24 +9,24 @@ open import Data.List using (List; []; _∷_; map) open import Data.Product using (∃-syntax; Σ-syntax; _×_; _,_) open import Size using (∞) -open import Show.Lines hiding (map) -open import Show.Print +open import Vatras.Show.Lines hiding (map) +open import Vatras.Show.Print -open import Test.Example using (Example) -open import Test.Experiment using (Experiment; ExperimentSetup; setup; run-setup) +open import Vatras.Test.Example using (Example) +open import Vatras.Test.Experiment using (Experiment; ExperimentSetup; setup; run-setup) -open import Lang.CCC using (CCC) -open import Lang.OC using (WFOC) +open import Vatras.Lang.CCC using (CCC) +open import Vatras.Lang.OC using (WFOC) -open import Test.Examples.CCC using (cccex-all) -open import Test.Examples.OC using (optex-all) +open import Vatras.Test.Examples.CCC using (cccex-all) +open import Vatras.Test.Examples.OC using (optex-all) -open import Test.Experiments.CCC-to-2CC -open import Test.Experiments.OC-to-2CC +open import Vatras.Test.Experiments.CCC-to-2CC +open import Vatras.Test.Experiments.OC-to-2CC -import Test.Experiments.FST-Experiments as FSTs +import Vatras.Test.Experiments.FST-Experiments as FSTs open FSTs.Java.Calculator using (toy-calculator-experiment; ex-all) -open import Test.Experiments.RoundTrip as RoundTrip using (round-trip) +open import Vatras.Test.Experiments.RoundTrip as RoundTrip using (round-trip) {-| A list of programs that we want to run. diff --git a/src/Show/Eval.agda b/src/Vatras/Show/Eval.agda similarity index 78% rename from src/Show/Eval.agda rename to src/Vatras/Show/Eval.agda index bb3236ca..bd51a219 100644 --- a/src/Show/Eval.agda +++ b/src/Vatras/Show/Eval.agda @@ -1,7 +1,7 @@ {-| Some helper functions for pretty printing. -} -module Show.Eval where +module Vatras.Show.Eval where open import Data.Bool using (Bool) open import Data.Bool.Show renaming (show to show-bool) @@ -9,11 +9,11 @@ open import Data.String using (String; _++_) open import Size using (Size) open import Function using (id) -open import Framework.Definitions -open import Framework.VariabilityLanguage +open import Vatras.Framework.Definitions +open import Vatras.Framework.VariabilityLanguage -open import Show.Lines -open import Util.Named +open import Vatras.Show.Lines +open import Vatras.Util.Named show-in-semantics : String → String show-in-semantics s = "⟦ " ++ s ++ " ⟧" diff --git a/src/Show/Lines.agda b/src/Vatras/Show/Lines.agda similarity index 99% rename from src/Show/Lines.agda rename to src/Vatras/Show/Lines.agda index 9315b16f..f6378293 100644 --- a/src/Show/Lines.agda +++ b/src/Vatras/Show/Lines.agda @@ -1,7 +1,7 @@ {-| This module introduces our pretty printing monad. -} -module Show.Lines where +module Vatras.Show.Lines where open import Data.Bool using (true; false; if_then_else_) open import Data.Nat using (ℕ; _*_; _∸_; ⌊_/2⌋; ⌈_/2⌉; _≤ᵇ_) @@ -20,7 +20,7 @@ open import Effect.Monad.Writer as Writer using (RawMonadWriter; Writer; runWrit open import Data.List.Effectful as List using () renaming (applicative to list-applicative; monad to list-monad) open import Level using (0ℓ) -open import Util.List using (max) +open import Vatras.Util.List using (max) open Data.String using (Left; Center; Right) public diff --git a/src/Show/Print.agda b/src/Vatras/Show/Print.agda similarity index 84% rename from src/Show/Print.agda rename to src/Vatras/Show/Print.agda index d1b31dca..205d95a7 100644 --- a/src/Show/Print.agda +++ b/src/Vatras/Show/Print.agda @@ -1,6 +1,6 @@ {-# OPTIONS --guardedness #-} -module Show.Print where +module Vatras.Show.Print where open import Data.Nat using (ℕ) open import Data.Unit.Polymorphic using (⊤) @@ -8,7 +8,7 @@ open import IO using (IO; putStrLn) open IO.List using (mapM′) open import Level using (0ℓ) -open import Show.Lines using (Lines; align; content; raw-lines) +open import Vatras.Show.Lines using (Lines; align; content; raw-lines) open import Data.Nat.Show using (show) open import Data.List using (length) diff --git a/src/Test/Example.agda b/src/Vatras/Test/Example.agda similarity index 60% rename from src/Test/Example.agda rename to src/Vatras/Test/Example.agda index d35151b6..ed614599 100644 --- a/src/Test/Example.agda +++ b/src/Vatras/Test/Example.agda @@ -1,7 +1,7 @@ -module Test.Example where +module Vatras.Test.Example where open import Data.String using (String) -open import Util.Named public +open import Vatras.Util.Named public Example = Named diff --git a/src/Test/Examples/CCC.agda b/src/Vatras/Test/Examples/CCC.agda similarity index 92% rename from src/Test/Examples/CCC.agda rename to src/Vatras/Test/Examples/CCC.agda index bf666141..5915d05e 100644 --- a/src/Test/Examples/CCC.agda +++ b/src/Vatras/Test/Examples/CCC.agda @@ -1,4 +1,4 @@ -module Test.Examples.CCC where +module Vatras.Test.Examples.CCC where open import Data.String as String using (String) open import Data.List using (List; _∷_; []) @@ -10,11 +10,11 @@ open import Data.Product open import Size using (Size; ∞; ↑_) -open import Framework.Definitions using (𝔸; atoms) +open import Vatras.Framework.Definitions using (𝔸; atoms) -open import Lang.All +open import Vatras.Lang.All open CCC -- use strings as dimensions -open import Test.Example +open import Vatras.Test.Example CCCExample : Set₁ CCCExample = Example (CCC String ∞ (String , String._≟_)) diff --git a/src/Test/Examples/OC.agda b/src/Vatras/Test/Examples/OC.agda similarity index 88% rename from src/Test/Examples/OC.agda rename to src/Vatras/Test/Examples/OC.agda index 33aa0ed4..94dd1b8d 100644 --- a/src/Test/Examples/OC.agda +++ b/src/Vatras/Test/Examples/OC.agda @@ -1,4 +1,4 @@ -module Test.Examples.OC where +module Vatras.Test.Examples.OC where open import Data.List using (List; []; _∷_; [_]) open import Data.String as String using (String) @@ -6,11 +6,11 @@ open import Data.Product using (_,_) open import Size using (Size; ↑_; ∞) -- open import Framework.Annotation.Name using (Option) -open import Framework.Definitions using (𝔸; 𝔽) -open import Lang.All +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Lang.All open OC -open import Test.Example +open import Vatras.Test.Example OCExample : Set₁ OCExample = Example (WFOC String ∞ (String , String._≟_)) diff --git a/src/Test/Examples/Variants.agda b/src/Vatras/Test/Examples/Variants.agda similarity index 75% rename from src/Test/Examples/Variants.agda rename to src/Vatras/Test/Examples/Variants.agda index cf224658..1a3989e0 100644 --- a/src/Test/Examples/Variants.agda +++ b/src/Vatras/Test/Examples/Variants.agda @@ -1,4 +1,4 @@ -module Test.Examples.Variants where +module Vatras.Test.Examples.Variants where open import Data.Fin using (zero; suc) open import Data.Nat as ℕ using (ℕ) @@ -6,10 +6,10 @@ open import Data.Product using (∃-syntax; _,_) open import Data.List using (List; []; _∷_) open import Data.String as String using (String) open import Size using (∞) -open import Framework.Variants using (Rose; rose-leaf) -open import Framework.VariantGenerator (Rose ∞) using (VariantGenerator) +open import Vatras.Framework.Variants using (Rose; rose-leaf) +open import Vatras.Framework.VariantGenerator (Rose ∞) using (VariantGenerator) -open import Test.Example +open import Vatras.Test.Example 𝕍-123 : Example (VariantGenerator (ℕ , ℕ._≟_) 2) 𝕍-123 = "123" ≔ set diff --git a/src/Test/Experiment.agda b/src/Vatras/Test/Experiment.agda similarity index 92% rename from src/Test/Experiment.agda rename to src/Vatras/Test/Experiment.agda index 196711af..1c487bb4 100644 --- a/src/Test/Experiment.agda +++ b/src/Vatras/Test/Experiment.agda @@ -1,4 +1,4 @@ -module Test.Experiment where +module Vatras.Test.Experiment where open import Data.List using (List; map) open import Data.Nat using (ℕ; _+_; _∸_) @@ -6,10 +6,10 @@ open import Data.Product using (Σ-syntax; _×_; _,_) open import Data.String using (String; _++_; length; replicate) open import Level using (suc) -open import Show.Lines hiding (map) +open import Vatras.Show.Lines hiding (map) -open import Test.Example -open import Util.Named +open import Vatras.Test.Example +open import Vatras.Util.Named EXPERIMENT-BOX-WIDTH : ℕ EXPERIMENT-BOX-WIDTH = 100 diff --git a/src/Test/Experiments/CCC-to-2CC.agda b/src/Vatras/Test/Experiments/CCC-to-2CC.agda similarity index 89% rename from src/Test/Experiments/CCC-to-2CC.agda rename to src/Vatras/Test/Experiments/CCC-to-2CC.agda index 83cef2c5..68f0746b 100644 --- a/src/Test/Experiments/CCC-to-2CC.agda +++ b/src/Vatras/Test/Experiments/CCC-to-2CC.agda @@ -1,4 +1,4 @@ -module Test.Experiments.CCC-to-2CC where +module Vatras.Test.Experiments.CCC-to-2CC where open import Data.Bool using (Bool) @@ -17,30 +17,30 @@ open import Function using (_∘_; id) open import Size using (∞) -open import Show.Lines +open import Vatras.Show.Lines -- open import Framework.Annotation.Name using (Dimension) --- open import Lang.CCC +-- open import Vatras.Lang.CCC -- renaming (Configuration to Configurationₙ; -- ⟦_⟧ to ⟦_⟧ₙ) --- open import Lang.2CC +-- open import Vatras.Lang.2CC -- renaming (Configuration to Configuration₂; -- ⟦_⟧ to ⟦_⟧₂) --- open import Framework.Definitions using (ℂ) +-- open import Vatras.Framework.Definitions using (ℂ) -- open import Translation.CCC-to-2CC using (CCC→2CC) -- open import Framework.Proof.Translation using (expr; conf; fnoc) --- open import Util.ShowHelpers +-- open import Vatras.Util.ShowHelpers --- open import Test.Example --- open import Test.Experiment --- open import Test.UnitTest +-- open import Vatras.Test.Example +-- open import Vatras.Test.Experiment +-- open import Vatras.Test.UnitTest --- open import Util.Named --- open import Show.Eval +-- open import Vatras.Util.Named +-- open import Vatras.Show.Eval --- open import Test.Examples.CCC +-- open import Vatras.Test.Examples.CCC -- -- Make a configuration that always selects n and also generate its name. -- all-n : ℕ → Named Configurationₙ @@ -107,12 +107,12 @@ open import Show.Lines -- show-fnoc-conf-all-n : ℕ → String -- show-fnoc-conf-all-n = λ n → show-named (λ c → show-nary-config c (Lang.CCC.dims cc)) (fnoc-named (conf-named (all-n n))) -- in do --- > show-named Lang.CCC.show ex +-- > show-named Vatras.Lang.CCC.show ex -- >∷ mapl (show-all-n) conf-vals -- lines (mapl eval-all-n conf-vals) -- linebreak --- > show-named Lang.2CC.show expr-named +-- > show-named Vatras.Lang.2CC.show expr-named -- >∷ mapl (show-conf-all-n) conf-vals -- lines (mapl eval-forth-all-n conf-vals) -- linebreak diff --git a/src/Test/Experiments/FST-Experiments.agda b/src/Vatras/Test/Experiments/FST-Experiments.agda similarity index 90% rename from src/Test/Experiments/FST-Experiments.agda rename to src/Vatras/Test/Experiments/FST-Experiments.agda index aaae9d19..6ac1efd9 100644 --- a/src/Test/Experiments/FST-Experiments.agda +++ b/src/Vatras/Test/Experiments/FST-Experiments.agda @@ -1,7 +1,7 @@ {-# OPTIONS --allow-unsolved-metas #-} -open import Framework.Definitions -module Test.Experiments.FST-Experiments where +open import Vatras.Framework.Definitions +module Vatras.Test.Experiments.FST-Experiments where open import Data.Bool using (true; false) open import Data.List using (List; _∷_; []; map; [_]) @@ -13,16 +13,16 @@ open import Relation.Nullary.Decidable using (yes; no; does; _because_; _×-dec_ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Util.Named -open import Test.Example -open import Test.Experiment -open import Show.Lines hiding (map) -open import Util.ShowHelpers +open import Vatras.Util.Named +open import Vatras.Test.Example +open import Vatras.Test.Experiment +open import Vatras.Show.Lines hiding (map) +open import Vatras.Util.ShowHelpers open import Data.String using (String; _<+>_; _++_) renaming (_≟_ to _≟ˢ_) -open import Framework.Variants using (show-rose) +open import Vatras.Framework.Variants using (show-rose) -import Lang.FST as FST +import Vatras.Lang.FST as FST open FST using (Conf) module _ (F : 𝔽) (A : 𝔸) where diff --git a/src/Test/Experiments/OC-to-2CC.agda b/src/Vatras/Test/Experiments/OC-to-2CC.agda similarity index 80% rename from src/Test/Experiments/OC-to-2CC.agda rename to src/Vatras/Test/Experiments/OC-to-2CC.agda index 305f6c66..4f7dd191 100644 --- a/src/Test/Experiments/OC-to-2CC.agda +++ b/src/Vatras/Test/Experiments/OC-to-2CC.agda @@ -1,4 +1,4 @@ -module Test.Experiments.OC-to-2CC where +module Vatras.Test.Experiments.OC-to-2CC where open import Data.Bool using (Bool; true; false) open import Data.List using (_∷_; []) @@ -13,31 +13,31 @@ open import Level using (0ℓ) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) -open import Framework.Definitions using (ℂ) -open import Framework.Variants using (Rose; show-rose) +open import Vatras.Framework.Definitions using (ℂ) +open import Vatras.Framework.Variants using (Rose; show-rose) Feature = String -open import Lang.All --- open import Lang.OC Feature as OCL renaming (Configuration to Conf-oc) --- open import Lang.2CC as 2CCL +open import Vatras.Lang.All +-- open import Vatras.Lang.OC Feature as OCL renaming (Configuration to Conf-oc) +-- open import Vatras.Lang.2CC as 2CCL open OC using (WFOC; WFOCL) open OC.Show Feature id open 2CC using (2CCL) -open import Translation.Lang.2CC.Redundancy Feature _≟_ +open import Vatras.Translation.Lang.2CC.Redundancy Feature _≟_ open 2CC.Pretty id -open import Translation.Lang.OC-to-2CC Feature using (compile; compile-configs) +open import Vatras.Translation.Lang.OC-to-2CC Feature using (compile; compile-configs) -open import Show.Lines -open import Util.Named -open import Show.Eval +open import Vatras.Show.Lines +open import Vatras.Util.Named +open import Vatras.Show.Eval -open import Test.Experiment -open import Test.Example -open import Test.Examples.OC +open import Vatras.Test.Experiment +open import Vatras.Test.Example +open import Vatras.Test.Examples.OC -open import Test.UnitTest +open import Vatras.Test.UnitTest OC→2CC-Test : UnitTest (OC.Configuration Feature) OC→2CC-Test c = ForAllExamplesIn optex-all (test-translation (WFOCL Feature) (2CCL Feature) compile compile-configs c) diff --git a/src/Test/Experiments/RoundTrip.agda b/src/Vatras/Test/Experiments/RoundTrip.agda similarity index 80% rename from src/Test/Experiments/RoundTrip.agda rename to src/Vatras/Test/Experiments/RoundTrip.agda index bab4ba05..2a78527a 100644 --- a/src/Test/Experiments/RoundTrip.agda +++ b/src/Vatras/Test/Experiments/RoundTrip.agda @@ -1,4 +1,4 @@ -module Test.Experiments.RoundTrip where +module Vatras.Test.Experiments.RoundTrip where open import Data.Bool using (Bool; true; false) import Data.Fin as Fin @@ -16,31 +16,31 @@ open import Level using (0ℓ) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (ℂ; 𝔸) -open import Framework.Variants using (Rose; show-rose) -open import Framework.VariabilityLanguage using (VariabilityLanguage; Expression) -open import Util.AuxProofs using (decidableEquality-×) -open import Util.Nat.AtLeast using (ℕ≥) -import Util.String as String +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (ℂ; 𝔸) +open import Vatras.Framework.Variants using (Rose; show-rose) +open import Vatras.Framework.VariabilityLanguage using (VariabilityLanguage; Expression) +open import Vatras.Util.AuxProofs using (decidableEquality-×) +open import Vatras.Util.Nat.AtLeast using (ℕ≥) +import Vatras.Util.String as String -open import Lang.All +open import Vatras.Lang.All open CCC using (CCC; _⟨_⟩; _-<_>-) open NCC using (NCC) -open import Translation.LanguageMap -import Translation.Lang.CCC-to-NCC -module CCC-to-NCC = Translation.Lang.CCC-to-NCC.Exact -import Translation.Lang.NCC-to-2CC -open Translation.Lang.NCC-to-2CC.2Ary using () renaming (NCC→2CC to NCC-2→2CC) +open import Vatras.Translation.LanguageMap +import Vatras.Translation.Lang.CCC-to-NCC +module CCC-to-NCC = Vatras.Translation.Lang.CCC-to-NCC.Exact +import Vatras.Translation.Lang.NCC-to-2CC +open Vatras.Translation.Lang.NCC-to-2CC.2Ary using () renaming (NCC→2CC to NCC-2→2CC) open CCC.Encode using () renaming (encoder to CCC-Rose-encoder) -open import Show.Lines -open import Util.Named -open import Show.Eval +open import Vatras.Show.Lines +open import Vatras.Util.Named +open import Vatras.Show.Eval -open import Test.Experiment -open import Test.Example -open import Test.Examples.OC +open import Vatras.Test.Experiment +open import Vatras.Test.Example +open import Vatras.Test.Examples.OC Feature = String Artifact : 𝔸 diff --git a/src/Test/Test/VariantList-Completeness.agda b/src/Vatras/Test/Test/VariantList-Completeness.agda similarity index 85% rename from src/Test/Test/VariantList-Completeness.agda rename to src/Vatras/Test/Test/VariantList-Completeness.agda index 1226682c..d8a5b574 100644 --- a/src/Test/Test/VariantList-Completeness.agda +++ b/src/Vatras/Test/Test/VariantList-Completeness.agda @@ -1,4 +1,4 @@ -module Test.Test.VariantList-Completeness where +module Vatras.Test.Test.VariantList-Completeness where open import Level using (Level; 0ℓ; Lift; lift) renaming (suc to lsuc) open import Size using (∞) @@ -8,15 +8,15 @@ open import Data.Fin using (Fin) renaming (zero to f-zero; suc to f-suc) open import Data.Product using (_,_; proj₁; proj₂) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Util.Named using (get) -open import Test.Examples.Variants -open import Test.UnitTest +open import Vatras.Util.Named using (get) +open import Vatras.Test.Examples.Variants +open import Vatras.Test.UnitTest -open import Framework.Variants using (Rose) +open import Vatras.Framework.Variants using (Rose) Variant = Rose ∞ -open import Lang.All +open import Vatras.Lang.All open VariantList Variant using (Configuration; ⟦_⟧; encode; vl-conf; vl-fnoc) -open import Framework.VariantGenerator Variant using (VariantGenerator) +open import Vatras.Framework.VariantGenerator Variant using (VariantGenerator) test-encode-conf : ∀ {A n} → Fin (suc n) → UnitTest (VariantGenerator A n) test-encode-conf i vs = ⟦ encode vs ⟧ (vl-conf i) ≡ vs i diff --git a/src/Test/UnitTest.agda b/src/Vatras/Test/UnitTest.agda similarity index 90% rename from src/Test/UnitTest.agda rename to src/Vatras/Test/UnitTest.agda index 5db15edf..1dde125c 100644 --- a/src/Test/UnitTest.agda +++ b/src/Vatras/Test/UnitTest.agda @@ -1,4 +1,4 @@ -module Test.UnitTest where +module Vatras.Test.UnitTest where open import Data.List using (List) open import Data.List.Relation.Unary.All using (All) @@ -10,11 +10,11 @@ open import Function using (_∘_) open import Level using (0ℓ; _⊔_; suc) open import Size using (Size) -open import Framework.Definitions -open import Framework.VariabilityLanguage -open import Framework.Relation.Function using (_⇒ₚ_; _⇔_; to; from) +open import Vatras.Framework.Definitions +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Relation.Function using (_⇒ₚ_; _⇔_; to; from) -open import Test.Example using (Example; _called_) +open import Vatras.Test.Example using (Example; _called_) open Data.List.Relation.Unary.All using ([]; _∷_) public open Eq using (refl) public diff --git a/src/Translation/Lang/2CC-to-ADT.agda b/src/Vatras/Translation/Lang/2CC-to-ADT.agda similarity index 90% rename from src/Translation/Lang/2CC-to-ADT.agda rename to src/Vatras/Translation/Lang/2CC-to-ADT.agda index 1ee94c1a..9906ef5f 100644 --- a/src/Translation/Lang/2CC-to-ADT.agda +++ b/src/Vatras/Translation/Lang/2CC-to-ADT.agda @@ -5,27 +5,27 @@ artifact constructors below the `2CC` choices if necessary. This translation eliminates all sharing between the variants by effectively enumerating all variants differentiated by a choice. -} -module Translation.Lang.2CC-to-ADT where +module Vatras.Translation.Lang.2CC-to-ADT where open import Size using (Size; ∞) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Bool as Bool using (if_then_else_) import Data.Bool.Properties as Bool open import Data.List as List using (List; []; _∷_; _ʳ++_) import Data.List.Properties as List -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (𝔸; 𝔽; atoms) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝔸; 𝔽; atoms) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (id) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) -open import Lang.2CC as 2CC using (2CC; 2CCL) -open import Lang.ADT as ADT using (ADT; ADTL; leaf; _⟨_,_⟩) +open import Vatras.Lang.2CC as 2CC using (2CC; 2CCL) +open import Vatras.Lang.ADT as ADT using (ADT; ADTL; leaf; _⟨_,_⟩) push-down-artifact : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → atoms A → List (ADT (Rose ∞) D A) → ADT (Rose ∞) D A push-down-artifact {A = A} a cs = go cs [] diff --git a/src/Translation/Lang/2CC-to-NCC.agda b/src/Vatras/Translation/Lang/2CC-to-NCC.agda similarity index 90% rename from src/Translation/Lang/2CC-to-NCC.agda rename to src/Vatras/Translation/Lang/2CC-to-NCC.agda index 0c7c6da3..b1612bcf 100644 --- a/src/Translation/Lang/2CC-to-NCC.agda +++ b/src/Vatras/Translation/Lang/2CC-to-NCC.agda @@ -3,12 +3,12 @@ This module shows that `2CC` is a subset of `NCC 2` by translating the `2CC` constructors into their `NCC 2` equivalent. For convenience, it also provides a composition to allow translations to arbitrary arity `NCC` expressions. -} -module Translation.Lang.2CC-to-NCC where +module Vatras.Translation.Lang.2CC-to-NCC where open import Size using (Size; ∞) open import Data.Bool using (true; false; if_then_else_) open import Data.Bool.Properties as Bool -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin using (zero; suc) open import Data.List as List using (List) import Data.List.Properties as List @@ -16,22 +16,22 @@ open import Data.Nat using (zero) open import Data.Product using () renaming (_,_ to _and_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Util.Nat.AtLeast using (ℕ≥; sucs) +open import Vatras.Util.Nat.AtLeast using (ℕ≥; sucs) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) -open import Translation.Lang.NCC.Grow using (growFrom2Compiler) +open import Vatras.Translation.Lang.NCC.Grow using (growFrom2Compiler) module 2Ary where translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} diff --git a/src/Translation/Lang/2CC/Redundancy.lagda.md b/src/Vatras/Translation/Lang/2CC/Redundancy.lagda.md similarity index 92% rename from src/Translation/Lang/2CC/Redundancy.lagda.md rename to src/Vatras/Translation/Lang/2CC/Redundancy.lagda.md index 289d9c58..f8ac92c1 100644 --- a/src/Translation/Lang/2CC/Redundancy.lagda.md +++ b/src/Vatras/Translation/Lang/2CC/Redundancy.lagda.md @@ -22,9 +22,9 @@ TODO: The compiler currently is forgetful. While it produces an expression resulting expression that it indeed has this property. -} ```agda -open import Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) open import Relation.Binary.Definitions using (DecidableEquality) -module Translation.Lang.2CC.Redundancy (Dimension : 𝔽) (_==_ : DecidableEquality Dimension) where +module Vatras.Translation.Lang.2CC.Redundancy (Dimension : 𝔽) (_==_ : DecidableEquality Dimension) where open import Function using (id) open import Size using (Size; ∞) @@ -38,13 +38,13 @@ open import Relation.Nullary using (yes; no) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≡_) open Eq.≡-Reasoning -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Variants as V using (Rose) -open import Util.AuxProofs using (true≢false) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Util.AuxProofs using (true≢false) -open import Data.EqIndexedSet using (≗→≅[]; ≅[]-sym) +open import Vatras.Data.EqIndexedSet using (≗→≅[]; ≅[]-sym) -open import Lang.2CC +open import Vatras.Lang.2CC ``` A scope remembers any dominating outer choices. diff --git a/src/Translation/Lang/2CC/Rename.agda b/src/Vatras/Translation/Lang/2CC/Rename.agda similarity index 92% rename from src/Translation/Lang/2CC/Rename.agda rename to src/Vatras/Translation/Lang/2CC/Rename.agda index bdc6cd77..9f7abd20 100644 --- a/src/Translation/Lang/2CC/Rename.agda +++ b/src/Vatras/Translation/Lang/2CC/Rename.agda @@ -8,27 +8,27 @@ all elements of `D₁` in the datastructure `2CC D₁` to obtain a new datastruc necessary because a non-injective rename would reduce the number of possible variants. -} -module Translation.Lang.2CC.Rename where +module Vatras.Translation.Lang.2CC.Rename where open import Size using (Size; ∞) open import Data.Bool using (if_then_else_) import Data.Bool.Properties as Bool -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.List as List using (List) import Data.List.Properties as List open import Data.Product using () renaming (_,_ to _and_) -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) 2CC-map-config : ∀ {D₁ D₂ : 𝔽} diff --git a/src/Translation/Lang/ADT-to-2CC.agda b/src/Vatras/Translation/Lang/ADT-to-2CC.agda similarity index 82% rename from src/Translation/Lang/ADT-to-2CC.agda rename to src/Vatras/Translation/Lang/ADT-to-2CC.agda index 0dbf3217..f23171a1 100644 --- a/src/Translation/Lang/ADT-to-2CC.agda +++ b/src/Vatras/Translation/Lang/ADT-to-2CC.agda @@ -2,29 +2,29 @@ This module shows that `ADT` is a subset of `2CC` by translating the `ADT` constructors into their, less restrictive, `2CC` equivalent. -} -module Translation.Lang.ADT-to-2CC where +module Vatras.Translation.Lang.ADT-to-2CC where open import Size using (Size; ∞) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Bool as Bool using (if_then_else_) import Data.Bool.Properties as Bool open import Data.Product using (proj₂) open import Data.List as List using (List; []; _∷_; _ʳ++_) import Data.List.Properties as List -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) -open import Framework.Variants using (VariantEncoder) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Variants using (VariantEncoder) open import Function using (id) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) open Eq.≡-Reasoning using (step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) -open import Lang.2CC as 2CC using (2CC; 2CCL) -open import Lang.ADT as ADT using (ADT; ADTL; leaf; _⟨_,_⟩) +open import Vatras.Lang.2CC as 2CC using (2CC; 2CCL) +open import Vatras.Lang.ADT as ADT using (ADT; ADTL; leaf; _⟨_,_⟩) translate : ∀ {F : 𝔽} {A : 𝔸} → VariantEncoder (Rose ∞) (2CCL F) → ADT (Rose ∞) F A → 2CC F ∞ A translate Variant→2CC (ADT.leaf v) = LanguageCompiler.compile Variant→2CC v diff --git a/src/Translation/Lang/ADT-to-NADT.agda b/src/Vatras/Translation/Lang/ADT-to-NADT.agda similarity index 89% rename from src/Translation/Lang/ADT-to-NADT.agda rename to src/Vatras/Translation/Lang/ADT-to-NADT.agda index 65a08a11..9f49a6a6 100644 --- a/src/Translation/Lang/ADT-to-NADT.agda +++ b/src/Vatras/Translation/Lang/ADT-to-NADT.agda @@ -2,9 +2,9 @@ This module shows that `ADT` is a subset of `NADT` by translating the `ADT` constructors into their, less restrictive, `NADT` equivalent. -} -open import Framework.Definitions using (𝔸; 𝕍; 𝔽) +open import Vatras.Framework.Definitions using (𝔸; 𝕍; 𝔽) -module Translation.Lang.ADT-to-NADT (V : 𝕍) where +module Vatras.Translation.Lang.ADT-to-NADT (V : 𝕍) where open import Data.Bool using (if_then_else_; true; false) import Data.Bool.Properties as Bool @@ -15,18 +15,18 @@ open import Data.Product using () renaming (_,_ to _and_) open import Level using (0ℓ) open import Size using (Size; ∞) -import Util.List as List -open import Framework.Relation.Function using (from; to) -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Relation.Expressiveness V using (expressiveness-from-compiler; _≽_) +import Vatras.Util.List as List +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Relation.Expressiveness V using (expressiveness-from-compiler; _≽_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open Eq.≡-Reasoning -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open ADT using (ADT; ADTL; _⟨_,_⟩) open NADT using (NADT; NADTL; leaf; _⟨_⟩) diff --git a/src/Translation/Lang/ADT-to-VariantList.agda b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda similarity index 86% rename from src/Translation/Lang/ADT-to-VariantList.agda rename to src/Vatras/Translation/Lang/ADT-to-VariantList.agda index 5b246428..23c4552b 100644 --- a/src/Translation/Lang/ADT-to-VariantList.agda +++ b/src/Vatras/Translation/Lang/ADT-to-VariantList.agda @@ -4,10 +4,10 @@ all possible configurations for each choice. However, this simple process might result in impossible, dead variants. Hence, dead branch elimination is applied first, resulting in the correct list of variants. -} -open import Framework.Definitions using (𝔽; 𝕍; 𝔸) +open import Vatras.Framework.Definitions using (𝔽; 𝕍; 𝔸) open import Data.Bool using (Bool; true; false; not; if_then_else_) open import Relation.Binary using (DecidableEquality; Rel) -module Translation.Lang.ADT-to-VariantList +module Vatras.Translation.Lang.ADT-to-VariantList (F : 𝔽) (V : 𝕍) (_==_ : DecidableEquality F) @@ -25,27 +25,27 @@ open import Relation.Nullary.Decidable using (yes; no) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open Eq.≡-Reasoning -open import Data.EqIndexedSet hiding (Index; _∈_) -open Data.EqIndexedSet.≅[]-Reasoning +open import Vatras.Data.EqIndexedSet hiding (Index; _∈_) +open Vatras.Data.EqIndexedSet.≅[]-Reasoning -open import Framework.VariabilityLanguage -open import Framework.Compiler -open import Framework.Relation.Expressiveness V using (_≽_; expressiveness-from-compiler) -open import Framework.Properties.Soundness V using (Sound) -open import Framework.Proof.ForFree V using (soundness-by-expressiveness) -open import Lang.ADT +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Compiler +open import Vatras.Framework.Relation.Expressiveness V using (_≽_; expressiveness-from-compiler) +open import Vatras.Framework.Properties.Soundness V using (Sound) +open import Vatras.Framework.Proof.ForFree V using (soundness-by-expressiveness) +open import Vatras.Lang.ADT using (ADT; ADTL; leaf; _⟨_,_⟩) renaming (⟦_⟧ to ⟦_⟧₂; Configuration to Conf₂) -open import Lang.VariantList V +open import Vatras.Lang.VariantList V using (VariantList; VariantListL; VariantList-is-Sound) renaming (⟦_⟧ to ⟦_⟧ₗ; Configuration to Confₗ) -open import Lang.ADT.Path F V _==_ -open import Translation.Lang.ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ; UndeadADT; UndeadADTL) -open import Translation.Lang.ADT.WalkSemantics F V _==_ as Walk using () +open import Vatras.Lang.ADT.Path F V _==_ +open import Vatras.Translation.Lang.ADT.DeadElim F V _==_ as DeadElim using (node; kill-dead; ⟦_⟧ᵤ; UndeadADT; UndeadADTL) +open import Vatras.Translation.Lang.ADT.WalkSemantics F V _==_ as Walk using () -open import Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸) -open import Util.AuxProofs using (<-cong-+ˡ) +open import Vatras.Util.List using (find-or-last; ⁺++⁺-length; ⁺++⁺-length-≤; find-or-last-append; find-or-last-prepend-+; find-or-last-prepend-∸) +open import Vatras.Util.AuxProofs using (<-cong-+ˡ) {- This translates a ADT to a VariantList. diff --git a/src/Translation/Lang/ADT/DeadElim.agda b/src/Vatras/Translation/Lang/ADT/DeadElim.agda similarity index 96% rename from src/Translation/Lang/ADT/DeadElim.agda rename to src/Vatras/Translation/Lang/ADT/DeadElim.agda index 744958bb..61aaf8cb 100644 --- a/src/Translation/Lang/ADT/DeadElim.agda +++ b/src/Vatras/Translation/Lang/ADT/DeadElim.agda @@ -10,9 +10,9 @@ expression `c` , all choices that mention `f` can be configured exactly like `kill-dead-below` transformation keeps track of the feature names and their respective configuration for the current expression. -} -open import Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) +open import Vatras.Framework.Definitions using (𝔽; 𝕍; 𝔸; 𝔼) open import Relation.Binary using (DecidableEquality; Rel) -module Translation.Lang.ADT.DeadElim +module Vatras.Translation.Lang.ADT.DeadElim (F : 𝔽) (V : 𝕍) (_==_ : DecidableEquality F) @@ -32,11 +32,11 @@ open import Relation.Nullary.Decidable using (yes; no; toWitness) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open Eq.≡-Reasoning -open import Framework.VariabilityLanguage -open import Framework.Compiler -open import Data.EqIndexedSet using (_≅[_][_]_; ≐→≅[]) -open import Lang.ADT -open import Lang.ADT.Path F V _==_ +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Compiler +open import Vatras.Data.EqIndexedSet using (_≅[_][_]_; ≐→≅[]) +open import Vatras.Lang.ADT +open import Vatras.Lang.ADT.Path F V _==_ {- A ADT is undead if it does not contain any dead branches. diff --git a/src/Translation/Lang/ADT/Rename.agda b/src/Vatras/Translation/Lang/ADT/Rename.agda similarity index 91% rename from src/Translation/Lang/ADT/Rename.agda rename to src/Vatras/Translation/Lang/ADT/Rename.agda index b53b64b7..cd60f5b4 100644 --- a/src/Translation/Lang/ADT/Rename.agda +++ b/src/Vatras/Translation/Lang/ADT/Rename.agda @@ -9,27 +9,27 @@ This precondition is necessary because a non-injective rename would reduce the number of possible variants. -} -open import Framework.Definitions using (𝔸; 𝔽; 𝕍) +open import Vatras.Framework.Definitions using (𝔸; 𝔽; 𝕍) -module Translation.Lang.ADT.Rename (V : 𝕍) where +module Vatras.Translation.Lang.ADT.Rename (V : 𝕍) where open import Size using (Size; ∞) open import Data.Bool using (if_then_else_) open import Data.Bool.Properties as Bool -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.List as List using (List) import Data.List.Properties as List open import Data.Product using () renaming (_,_ to _and_) -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Relation.Expressiveness V using (_≽_; expressiveness-from-compiler) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Relation.Expressiveness V using (_≽_; expressiveness-from-compiler) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open ADT using (ADT; ADTL; leaf; _⟨_,_⟩) ADT-map-config : ∀ {D₁ D₂ : 𝔽} diff --git a/src/Translation/Lang/ADT/WalkSemantics.agda b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda similarity index 96% rename from src/Translation/Lang/ADT/WalkSemantics.agda rename to src/Vatras/Translation/Lang/ADT/WalkSemantics.agda index e8ac0a83..a6c1038c 100644 --- a/src/Translation/Lang/ADT/WalkSemantics.agda +++ b/src/Vatras/Translation/Lang/ADT/WalkSemantics.agda @@ -5,9 +5,9 @@ This means that configurations can be modelled as functions or as paths. Interestingly, we obtain a compiler that does not change the input expression but only translates configurations. -} -open import Framework.Definitions using (𝔽; 𝕍; 𝔸) +open import Vatras.Framework.Definitions using (𝔽; 𝕍; 𝔸) open import Relation.Binary using (DecidableEquality; Rel) -module Translation.Lang.ADT.WalkSemantics +module Vatras.Translation.Lang.ADT.WalkSemantics (F : 𝔽) (V : 𝕍) (_==_ : DecidableEquality F) @@ -26,15 +26,15 @@ open import Relation.Nullary.Decidable using (yes; no; isYes; toWitness; fromWit open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open Eq.≡-Reasoning -open import Data.EqIndexedSet hiding (_∈_) -open Data.EqIndexedSet.≅-Reasoning +open import Vatras.Data.EqIndexedSet hiding (_∈_) +open Vatras.Data.EqIndexedSet.≅-Reasoning -open import Framework.VariabilityLanguage -open import Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧) -open import Lang.ADT.Path F V _==_ -open import Translation.Lang.ADT.DeadElim F V _==_ +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Lang.ADT using (ADT; leaf; _⟨_,_⟩; Configuration; ⟦_⟧) +open import Vatras.Lang.ADT.Path F V _==_ +open import Vatras.Translation.Lang.ADT.DeadElim F V _==_ -open import Util.Suffix +open import Vatras.Util.Suffix {- Converts a configuration function to a valid path within diff --git a/src/Translation/Lang/CCC-to-NCC.agda b/src/Vatras/Translation/Lang/CCC-to-NCC.agda similarity index 96% rename from src/Translation/Lang/CCC-to-NCC.agda rename to src/Vatras/Translation/Lang/CCC-to-NCC.agda index 9c0177ea..262404e9 100644 --- a/src/Translation/Lang/CCC-to-NCC.agda +++ b/src/Vatras/Translation/Lang/CCC-to-NCC.agda @@ -3,10 +3,10 @@ This module translates `CCC` expressions to `NCC` expressions by calculating the maximum number of choice alternatives, translating `CCC` into `NCC` with that arity and then translating the `NCC` expression to a fixed arity. -} -module Translation.Lang.CCC-to-NCC where +module Vatras.Translation.Lang.CCC-to-NCC where open import Size using (Size; ↑_; ∞) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin) open import Data.List as List using (List; []; _∷_) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_) @@ -15,28 +15,28 @@ open import Data.Nat.Properties as ℕ using (≤-reflexive; ≤-trans) open import Data.Product using (_×_; _,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (𝔸; 𝔽; atoms) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝔸; 𝔽; atoms) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (_∘_; id) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; _≗_) -open import Util.List using (find-or-last; map-find-or-last; find-or-last⇒lookup) -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs; _⊔_) -import Util.Vec as Vec +open import Vatras.Util.List using (find-or-last; map-find-or-last; find-or-last⇒lookup) +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs; _⊔_) +import Vatras.Util.Vec as Vec open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) open IndexedSet.≅[]-Reasoning using (step-≅[]-⟨; step-≅[]-⟩; _≅[]⟨⟩_; _≅[]-∎) -open import Lang.All +open import Vatras.Lang.All open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩) open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -open import Framework.Annotation.IndexedDimension -open import Translation.Lang.NCC.NCC-to-NCC using (NCC→NCC) -open import Translation.Lang.NCC.Rename using (NCC-rename; NCC-map-config) +open import Vatras.Framework.Annotation.IndexedDimension +open import Vatras.Translation.Lang.NCC.NCC-to-NCC using (NCC→NCC) +open import Vatras.Translation.Lang.NCC.Rename using (NCC-rename; NCC-map-config) module NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse = LanguageCompiler (NCC-rename {i} {D₁} {D₂} n f f⁻¹ is-inverse) module NCC→NCC {i} {D} n m = LanguageCompiler (NCC→NCC {i} {D} n m) diff --git a/src/Translation/Lang/FST-to-OC.lagda.md b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md similarity index 96% rename from src/Translation/Lang/FST-to-OC.lagda.md rename to src/Vatras/Translation/Lang/FST-to-OC.lagda.md index 1c45f8c8..2ba8cb2a 100644 --- a/src/Translation/Lang/FST-to-OC.lagda.md +++ b/src/Vatras/Translation/Lang/FST-to-OC.lagda.md @@ -1,7 +1,7 @@ # Option calculus is not as expressive as feature structure trees ```agda -open import Framework.Definitions using (𝔽; 𝔸) +open import Vatras.Framework.Definitions using (𝔽; 𝔸) open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl) @@ -13,7 +13,7 @@ To be as general as possible, we do not fix `F` but only require that it contains at least two distinct features `f₁` and `f₂`. To implement configurations, equality in `F` nees to be decidable, so `==ꟳ` is also required. ```agda -module Translation.Lang.FST-to-OC {F : 𝔽} (f₁ f₂ : F) (f₁≢f₂ : f₁ ≢ f₂) (_==ꟳ_ : DecidableEquality F) where +module Vatras.Translation.Lang.FST-to-OC {F : 𝔽} (f₁ f₂ : F) (f₁≢f₂ : f₁ ≢ f₂) (_==ꟳ_ : DecidableEquality F) where open import Size using (∞) open import Data.Bool as Bool using (true; false) @@ -34,17 +34,17 @@ open import Relation.Nullary using (yes; no) open Eq.≡-Reasoning -open import Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality) -open import Lang.All +open import Vatras.Framework.Variants using (Rose; rose-leaf; _-<_>-; children-equality) +open import Vatras.Lang.All open OC using (OC; WFOCL; Root; _❲_❳; all-oc) -open import Lang.OC.Properties using (⟦e⟧ₒtrue≡just) -open import Lang.OC.Subtree using (Subtree; subtrees; both; neither; Implies; subtreeₒ; subtreeₒ-recurse) -open import Lang.FST using (FSTL-Sem) +open import Vatras.Lang.OC.Properties using (⟦e⟧ₒtrue≡just) +open import Vatras.Lang.OC.Subtree using (Subtree; subtrees; both; neither; Implies; subtreeₒ; subtreeₒ-recurse) +open import Vatras.Lang.FST using (FSTL-Sem) open FST using (FSTL) open FST.Impose V = Rose ∞ -open import Framework.Relation.Expressiveness V using (_⋡_) +open import Vatras.Framework.Relation.Expressiveness V using (_⋡_) A : 𝔸 A = ℕ , _≟_ diff --git a/src/Translation/Lang/FST-to-VariantList.lagda.md b/src/Vatras/Translation/Lang/FST-to-VariantList.lagda.md similarity index 96% rename from src/Translation/Lang/FST-to-VariantList.lagda.md rename to src/Vatras/Translation/Lang/FST-to-VariantList.lagda.md index 9d97c381..40abd18d 100644 --- a/src/Translation/Lang/FST-to-VariantList.lagda.md +++ b/src/Vatras/Translation/Lang/FST-to-VariantList.lagda.md @@ -3,10 +3,10 @@ sublists of the features contained in the `FST` expression and configuring it accordingly. ```agda -open import Framework.Definitions using (𝔽; 𝔸; atoms) +open import Vatras.Framework.Definitions using (𝔽; 𝔸; atoms) open import Relation.Binary using (DecidableEquality) -module Translation.Lang.FST-to-VariantList (F : 𝔽) (_==ꟳ_ : DecidableEquality F) where +module Vatras.Translation.Lang.FST-to-VariantList (F : 𝔽) (_==ꟳ_ : DecidableEquality F) where open import Data.Bool using (Bool; true; false) open import Data.Empty using (⊥-elim) @@ -24,17 +24,17 @@ 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) +import Vatras.Data.EqIndexedSet as IndexedSet +open import Vatras.Framework.Compiler using (LanguageCompiler) +import Vatras.Framework.Relation.Expressiveness +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Variants using (Rose; _-<_>-) +open import Vatras.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 Vatras.Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open FST using (FSTL) open FST.Impose using (SPL; Feature) module Impose {F} {A} = FST.Impose F A diff --git a/src/Translation/Lang/NADT-to-CCC.agda b/src/Vatras/Translation/Lang/NADT-to-CCC.agda similarity index 82% rename from src/Translation/Lang/NADT-to-CCC.agda rename to src/Vatras/Translation/Lang/NADT-to-CCC.agda index fce22283..9113ddfc 100644 --- a/src/Translation/Lang/NADT-to-CCC.agda +++ b/src/Vatras/Translation/Lang/NADT-to-CCC.agda @@ -2,27 +2,27 @@ This module shows that `NADT` is a subset of `CCC` by translating the `NADT` constructors into their, less restrictive, `CCC` equivalent. -} -module Translation.Lang.NADT-to-CCC where +module Vatras.Translation.Lang.NADT-to-CCC where open import Size using (Size; ∞) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet import Data.List.NonEmpty as List⁺ open import Data.Product using (proj₂) -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions -open import Framework.Variants using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) -open import Framework.Variants using (VariantEncoder) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Variants using (VariantEncoder) open import Function using (id) open import Relation.Binary.PropositionalEquality as Eq using (refl; _≗_) -import Util.List as List +import Vatras.Util.List as List open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; ≅[]-sym; ≗→≅[]) -open import Lang.NADT as NADT using (NADT; NADTL; leaf; _⟨_⟩) -open import Lang.CCC as CCC using (CCC; CCCL; _-<_>-) +open import Vatras.Lang.NADT as NADT using (NADT; NADTL; leaf; _⟨_⟩) +open import Vatras.Lang.CCC as CCC using (CCC; CCCL; _-<_>-) translate : ∀ {i : Size} {F : 𝔽} {A : 𝔸} → VariantEncoder (Rose ∞) (CCCL F) → NADT (Rose ∞) F i A → CCC F ∞ A diff --git a/src/Translation/Lang/NCC-to-2CC.agda b/src/Vatras/Translation/Lang/NCC-to-2CC.agda similarity index 89% rename from src/Translation/Lang/NCC-to-2CC.agda rename to src/Vatras/Translation/Lang/NCC-to-2CC.agda index 85fee53f..dc44a5f6 100644 --- a/src/Translation/Lang/NCC-to-2CC.agda +++ b/src/Vatras/Translation/Lang/NCC-to-2CC.agda @@ -3,11 +3,11 @@ This module translates expressions from `NCC` to `2CC` by first translating any `NCC` expression to `NCC 2` and then replacing all `NCC 2` constructors to their equivalent `2CC` constructors. -} -module Translation.Lang.NCC-to-2CC where +module Vatras.Translation.Lang.NCC-to-2CC where open import Size using (Size; ∞) open import Data.Bool using (true; false; if_then_else_) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) open import Data.List as List using (List) import Data.List.Properties as List @@ -15,23 +15,23 @@ open import Data.Nat using (zero; suc) open import Data.Product using (_×_) renaming (_,_ to _and_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -open import Framework.Annotation.IndexedDimension -open import Translation.Lang.NCC.NCC-to-NCC using (NCC→NCC) +open import Vatras.Framework.Annotation.IndexedDimension +open import Vatras.Translation.Lang.NCC.NCC-to-NCC using (NCC→NCC) module 2Ary where translate : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → NCC (sucs zero) D i A → 2CC D ∞ A diff --git a/src/Translation/Lang/NCC-to-CCC.agda b/src/Vatras/Translation/Lang/NCC-to-CCC.agda similarity index 90% rename from src/Translation/Lang/NCC-to-CCC.agda rename to src/Vatras/Translation/Lang/NCC-to-CCC.agda index e8fafeb8..f7b403b0 100644 --- a/src/Translation/Lang/NCC-to-CCC.agda +++ b/src/Vatras/Translation/Lang/NCC-to-CCC.agda @@ -3,10 +3,10 @@ This module shows that `NCC`, regardless of arity, is a subset of `CCC` by translating the `NCC` constructors into their, less restrictive, `CCC` equivalent. -} -module Translation.Lang.NCC-to-CCC where +module Vatras.Translation.Lang.NCC-to-CCC where open import Size using (Size; ∞) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin) open import Data.List as List using (List; []; _∷_) import Data.List.NonEmpty as List⁺ @@ -14,19 +14,19 @@ import Data.List.Properties as List open import Data.Product using (_,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Relation.Binary.PropositionalEquality as Eq using (refl) -open import Util.List using (find-or-last; lookup⇒find-or-last) -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +open import Vatras.Util.List using (find-or-last; lookup⇒find-or-last) +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open CCC using (CCC; CCCL; _-<_>-; _⟨_⟩) open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) diff --git a/src/Translation/Lang/NCC/Grow.agda b/src/Vatras/Translation/Lang/NCC/Grow.agda similarity index 94% rename from src/Translation/Lang/NCC/Grow.agda rename to src/Vatras/Translation/Lang/NCC/Grow.agda index d80af473..cb32e955 100644 --- a/src/Translation/Lang/NCC/Grow.agda +++ b/src/Vatras/Translation/Lang/NCC/Grow.agda @@ -3,10 +3,10 @@ This module defines a compiler from NCC to NCC where the number N of alternative choice grows. The compiler duplicates the last alternative in each choice to grow the vector of alternatives to match a desired larger size. -} -module Translation.Lang.NCC.Grow where +module Vatras.Translation.Lang.NCC.Grow where open import Data.Empty using (⊥-elim) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) import Data.Fin.Properties as Fin open import Data.List as List using (List; []; _∷_) @@ -16,22 +16,22 @@ open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans open import Data.Product using (_×_; _,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Relation.Function using (from; to) -open import Framework.Variants as V using (Rose) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Variants as V using (Rose) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_) open import Relation.Nullary.Decidable using (yes; no) open import Size using (Size; ∞) -import Util.AuxProofs as ℕ -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -import Util.Vec as Vec +import Vatras.Util.AuxProofs as ℕ +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Vatras.Util.Vec as Vec open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -- Increasing the arity is straightforward. We have to duplicate one element (we choose the last one to be consistent with the saturation semantic of `CCC`, see `find-or-last`) until the arity difference is zero. diff --git a/src/Translation/Lang/NCC/NCC-to-NCC.agda b/src/Vatras/Translation/Lang/NCC/NCC-to-NCC.agda similarity index 66% rename from src/Translation/Lang/NCC/NCC-to-NCC.agda rename to src/Vatras/Translation/Lang/NCC/NCC-to-NCC.agda index 27009eb4..9ba016fc 100644 --- a/src/Translation/Lang/NCC/NCC-to-NCC.agda +++ b/src/Vatras/Translation/Lang/NCC/NCC-to-NCC.agda @@ -6,11 +6,11 @@ This means, given an n-ary expression, it is first reduced to a 2-ary expression and then pumped to an m-ary expression. -} -module Translation.Lang.NCC.NCC-to-NCC where +module Vatras.Translation.Lang.NCC.NCC-to-NCC where open import Size using (Size; ∞) open import Data.Empty using (⊥-elim) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) import Data.Fin.Properties as Fin open import Data.List as List using (List; []; _∷_) @@ -20,23 +20,23 @@ open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans open import Data.Product using (_×_; _,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_) open import Relation.Nullary.Decidable using (yes; no) -import Util.AuxProofs as ℕ -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -import Util.Vec as Vec +import Vatras.Util.AuxProofs as ℕ +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Vatras.Util.Vec as Vec -open import Lang.All +open import Vatras.Lang.All open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -open import Translation.Lang.NCC.ShrinkTo2 using (shrinkTo2Compiler) -open import Translation.Lang.NCC.Grow using (growFrom2Compiler) +open import Vatras.Translation.Lang.NCC.ShrinkTo2 using (shrinkTo2Compiler) +open import Vatras.Translation.Lang.NCC.Grow using (growFrom2Compiler) NCC→NCC : ∀ {i : Size} {D : 𝔽} → (n m : ℕ≥ 2) → LanguageCompiler (NCCL {i} n D) (NCCL m (D × Fin (ℕ≥.toℕ (ℕ≥.pred n)))) NCC→NCC n m = shrinkTo2Compiler n ⊕ growFrom2Compiler m diff --git a/src/Translation/Lang/NCC/Rename.agda b/src/Vatras/Translation/Lang/NCC/Rename.agda similarity index 91% rename from src/Translation/Lang/NCC/Rename.agda rename to src/Vatras/Translation/Lang/NCC/Rename.agda index 9e493a48..53dc7a5d 100644 --- a/src/Translation/Lang/NCC/Rename.agda +++ b/src/Vatras/Translation/Lang/NCC/Rename.agda @@ -8,11 +8,11 @@ require a left inverse `f⁻¹ : D₂ → D₁` of `f` as a proof that `f` is in This precondition is necessary because a non-injective rename would reduce the number of possible variants. -} -module Translation.Lang.NCC.Rename where +module Vatras.Translation.Lang.NCC.Rename where open import Size using (Size; ∞) open import Data.Empty using (⊥-elim) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) import Data.Fin.Properties as Fin open import Data.List as List using (List; []; _∷_) @@ -22,22 +22,22 @@ open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans open import Data.Product using (_×_; _,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Variants as V using (Rose) -open import Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) -open import Framework.Relation.Function using (from; to) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Variants as V using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (_≽_; expressiveness-from-compiler) +open import Vatras.Framework.Relation.Function using (from; to) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_) open import Relation.Nullary.Decidable using (yes; no) -import Util.AuxProofs as ℕ -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -import Util.Vec as Vec +import Vatras.Util.AuxProofs as ℕ +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Vatras.Util.Vec as Vec open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) NCC-map-config : ∀ {D₁ D₂ : Set} diff --git a/src/Translation/Lang/NCC/ShrinkTo2.agda b/src/Vatras/Translation/Lang/NCC/ShrinkTo2.agda similarity index 97% rename from src/Translation/Lang/NCC/ShrinkTo2.agda rename to src/Vatras/Translation/Lang/NCC/ShrinkTo2.agda index 0d10e4a0..44cb3c46 100644 --- a/src/Translation/Lang/NCC/ShrinkTo2.agda +++ b/src/Vatras/Translation/Lang/NCC/ShrinkTo2.agda @@ -8,10 +8,10 @@ as. The results looks like this: ↓ D.0 ⟨ a , D.1 ⟨ b , D.2 ⟨ c , d ⟩ ⟩ ⟩ -} -module Translation.Lang.NCC.ShrinkTo2 where +module Vatras.Translation.Lang.NCC.ShrinkTo2 where open import Data.Empty using (⊥-elim) -import Data.EqIndexedSet as IndexedSet +import Vatras.Data.EqIndexedSet as IndexedSet open import Data.Fin as Fin using (Fin; zero; suc) import Data.Fin.Properties as Fin open import Data.List as List using (List; []; _∷_) @@ -21,22 +21,22 @@ open import Data.Nat.Properties as ℕ using (≤-refl; ≤-reflexive; ≤-trans open import Data.Product using (_×_; _,_) open import Data.Vec as Vec using (Vec; []; _∷_) import Data.Vec.Properties as Vec -open import Framework.Compiler using (LanguageCompiler; _⊕_) -open import Framework.Definitions using (𝔸; 𝔽) -open import Framework.Relation.Function using (from; to) -open import Framework.Variants as V using (Rose) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔸; 𝔽) +open import Vatras.Framework.Relation.Function using (from; to) +open import Vatras.Framework.Variants as V using (Rose) open import Function using (id; _∘_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≢_; refl; _≗_) open import Relation.Nullary.Decidable using (yes; no) open import Size using (Size; ∞) -import Util.AuxProofs as ℕ -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -import Util.Vec as Vec +import Vatras.Util.AuxProofs as ℕ +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Vatras.Util.Vec as Vec open Eq.≡-Reasoning using (step-≡-⟨; step-≡-⟩; step-≡-∣; _∎) open IndexedSet using (_≅[_][_]_; _⊆[_]_; ≅[]-sym) -open import Lang.All +open import Vatras.Lang.All open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -- To simplify the implementation and the proof, we constrain the translation to result in 2-ary `NCC` expressions. @@ -45,7 +45,7 @@ open NCC using (NCC; NCCL; _-<_>-; _⟨_⟩) -- Otherwise only the first, or last alternative can be selected by configuring `d`. -- The solution is to extend the dimension `d` by an index (`IndexedDimension`) which numbers the list of alternatives. -- Note that the last choice in the list of alternatives holds two alternatives, so there will be one less dimension index than there are alternatives. -open import Framework.Annotation.IndexedDimension +open import Vatras.Framework.Annotation.IndexedDimension shrinkTo2 : ∀ {i : Size} {D : 𝔽} {A : 𝔸} → (n : ℕ≥ 2) diff --git a/src/Translation/Lang/OC-to-2CC.lagda.md b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md similarity index 96% rename from src/Translation/Lang/OC-to-2CC.lagda.md rename to src/Vatras/Translation/Lang/OC-to-2CC.lagda.md index 765400a7..c3176714 100644 --- a/src/Translation/Lang/OC-to-2CC.lagda.md +++ b/src/Vatras/Translation/Lang/OC-to-2CC.lagda.md @@ -3,10 +3,10 @@ ## Module ```agda -open import Framework.Definitions -module Translation.Lang.OC-to-2CC (F : 𝔽) where +open import Vatras.Framework.Definitions +module Vatras.Translation.Lang.OC-to-2CC (F : 𝔽) where -open import Framework.Variants as V using (Rose) +open import Vatras.Framework.Variants as V using (Rose) open import Size using (Size; ↑_; _⊔ˢ_; ∞) V = Rose ∞ Option = F @@ -22,17 +22,17 @@ open import Data.Product using (∃; ∃-syntax; _,_; proj₁; proj₂) open import Data.Vec using (Vec; []; _∷_; toList; fromList) open import Function using (id; _∘_; flip) -open import Framework.VariabilityLanguage -open import Lang.All +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Lang.All open OC renaming (_-<_>- to Artifactₒ) open 2CC renaming (_-<_>- to Artifact₂; ⟦_⟧ to ⟦_⟧₂) -open import Data.EqIndexedSet +open import Vatras.Data.EqIndexedSet Artifactᵥ : ∀ {A} → atoms A → List (Rose ∞ A) → Rose ∞ A Artifactᵥ a cs = a V.-< cs >- -open import Util.AuxProofs using (id≗toList∘fromList) +open import Vatras.Util.AuxProofs using (id≗toList∘fromList) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open Eq.≡-Reasoning @@ -426,10 +426,10 @@ preserves {b = b} {e = Root a es} c (T-root z⟶b) = ## Translation Implementation ```agda -open import Framework.Compiler using (LanguageCompiler) -open import Framework.VariabilityLanguage -open import Framework.Relation.Expressiveness V -open import Framework.Relation.Function using (_⇔_) +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Relation.Expressiveness V +open import Vatras.Framework.Relation.Function using (_⇔_) compile : ∀ {i : Size} {A : 𝔸} → WFOC F i A → 2CC F ∞ A compile = proj₁ ∘ ⟶-is-total diff --git a/src/Translation/Lang/OC-to-FST.agda b/src/Vatras/Translation/Lang/OC-to-FST.agda similarity index 77% rename from src/Translation/Lang/OC-to-FST.agda rename to src/Vatras/Translation/Lang/OC-to-FST.agda index 571432a3..2dcd91ae 100644 --- a/src/Translation/Lang/OC-to-FST.agda +++ b/src/Vatras/Translation/Lang/OC-to-FST.agda @@ -3,9 +3,9 @@ This module provides an example of neighboring artifacts with equal atoms and uses the `cannotEncodeNeighbors` lemma from `FST` to show that there are expressions in `WFOC` that cannot be encoded in `FST`. -} -open import Framework.Definitions using (𝔽; 𝔸) +open import Vatras.Framework.Definitions using (𝔽; 𝔸) -module Translation.Lang.OC-to-FST (F : 𝔽) where +module Vatras.Translation.Lang.OC-to-FST (F : 𝔽) where open import Size using (∞) open import Data.Bool using (true) @@ -14,13 +14,13 @@ open import Data.Nat using (zero; _≟_; ℕ) open import Data.Product using (_,_) import Relation.Binary.PropositionalEquality as Eq -open import Framework.Variants using (Rose) -open import Lang.All +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Lang.All open OC using (WFOC; Root; _-<_>-; WFOCL) open FST using (FSTL; cannotEncodeNeighbors) V = Rose ∞ -open import Framework.Relation.Expressiveness V using (_⋡_) +open import Vatras.Framework.Relation.Expressiveness V using (_⋡_) A : 𝔸 A = ℕ , _≟_ diff --git a/src/Vatras/Translation/Lang/Transitive/2CC-to-CCC.agda b/src/Vatras/Translation/Lang/Transitive/2CC-to-CCC.agda new file mode 100644 index 00000000..077c2ce1 --- /dev/null +++ b/src/Vatras/Translation/Lang/Transitive/2CC-to-CCC.agda @@ -0,0 +1,24 @@ +module Vatras.Translation.Lang.Transitive.2CC-to-CCC where + +open import Size using (Size; ∞) +open import Data.Nat using (zero) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔽) +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Util.Nat.AtLeast using (sucs) + +open import Vatras.Lang.All +open CCC using (CCCL) +open 2CC using (2CCL) + +import Vatras.Translation.Lang.2CC-to-NCC +open Vatras.Translation.Lang.2CC-to-NCC.2Ary using (2CC→NCC) +open import Vatras.Translation.Lang.NCC-to-CCC using (NCC→CCC) + + +2CC→CCC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (2CCL {i} D) (CCCL D) +2CC→CCC = 2CC→NCC ⊕ NCC→CCC (sucs zero) + +CCC≽2CC : ∀ {D : 𝔽} → CCCL D ≽ 2CCL D +CCC≽2CC = expressiveness-from-compiler 2CC→CCC diff --git a/src/Vatras/Translation/Lang/Transitive/CCC-to-2CC.agda b/src/Vatras/Translation/Lang/Transitive/CCC-to-2CC.agda new file mode 100644 index 00000000..f9c0c422 --- /dev/null +++ b/src/Vatras/Translation/Lang/Transitive/CCC-to-2CC.agda @@ -0,0 +1,25 @@ +module Vatras.Translation.Lang.Transitive.CCC-to-2CC where + +open import Size using (Size; ∞) +open import Data.Nat using (ℕ; zero) +open import Data.Product using (_×_) +open import Vatras.Framework.Compiler using (LanguageCompiler; _⊕_) +open import Vatras.Framework.Definitions using (𝔽) +open import Vatras.Framework.Variants using (Rose) +open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (expressiveness-from-compiler; _≽_) +open import Vatras.Util.Nat.AtLeast using (sucs) + +open import Vatras.Lang.All +open CCC using (CCCL) +open 2CC using (2CCL) + +open import Vatras.Translation.Lang.CCC-to-NCC using (CCC→NCC) +import Vatras.Translation.Lang.NCC-to-2CC +open Vatras.Translation.Lang.NCC-to-2CC.2Ary using (NCC→2CC) + + +CCC→2CC : ∀ {i : Size} {D : 𝔽} → LanguageCompiler (CCCL {i} D) (2CCL (D × ℕ)) +CCC→2CC = CCC→NCC (sucs zero) ⊕ NCC→2CC + +2CC≽CCC : ∀ {D : 𝔽} → 2CCL (D × ℕ) ≽ CCCL D +2CC≽CCC = expressiveness-from-compiler CCC→2CC diff --git a/src/Translation/Lang/VariantList-to-CCC.lagda.md b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md similarity index 90% rename from src/Translation/Lang/VariantList-to-CCC.lagda.md rename to src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md index c191927e..7830ade5 100644 --- a/src/Translation/Lang/VariantList-to-CCC.lagda.md +++ b/src/Vatras/Translation/Lang/VariantList-to-CCC.lagda.md @@ -3,10 +3,10 @@ ## Module ```agda -open import Framework.Definitions -open import Data.EqIndexedSet +open import Vatras.Framework.Definitions +open import Vatras.Data.EqIndexedSet -module Translation.Lang.VariantList-to-CCC +module Vatras.Translation.Lang.VariantList-to-CCC (Dimension : 𝔽) (𝔻 : Dimension) where @@ -27,16 +27,16 @@ open import Size open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym) open Eq.≡-Reasoning -open import Framework.Compiler using (LanguageCompiler) -open import Framework.VariabilityLanguage -open import Framework.Variants using (Rose; Variant-is-VL; encode-idemp) -open import Lang.All +open import Vatras.Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Variants using (Rose; Variant-is-VL; encode-idemp) +open import Vatras.Lang.All open VariantList (Rose ∞) using (VariantList; VariantListL; VariantList-is-Complete) renaming (⟦_⟧ to ⟦_⟧ₗ; Configuration to Cₗ) open CCC renaming (Configuration to Cᶜ) -open import Util.List using (find-or-last; map-find-or-last; map⁺-id) +open import Vatras.Util.List using (find-or-last; map-find-or-last; map⁺-id) ``` ## Translation @@ -144,7 +144,7 @@ module Translate preserves-⊆ e , preserves-⊇ e } - open import Framework.Relation.Expressiveness (Rose ∞) using (_≽_) + open import Vatras.Framework.Relation.Expressiveness (Rose ∞) using (_≽_) CCC≽VariantList : CCCL Dimension ≽ VariantListL CCC≽VariantList {A} e = translate e , ≅[]→≅ (LanguageCompiler.preserves VariantList→CCC e) diff --git a/src/Translation/LanguageMap.lagda.md b/src/Vatras/Translation/LanguageMap.lagda.md similarity index 84% rename from src/Translation/LanguageMap.lagda.md rename to src/Vatras/Translation/LanguageMap.lagda.md index 83294135..1ef0365b 100644 --- a/src/Translation/LanguageMap.lagda.md +++ b/src/Vatras/Translation/LanguageMap.lagda.md @@ -6,7 +6,7 @@ In particular, this file corresponds to the map of compilers in Section 5 of our ## Module ```agda -module Translation.LanguageMap where +module Vatras.Translation.LanguageMap where ``` ## Imports @@ -21,21 +21,21 @@ open import Relation.Binary using (DecidableEquality) open import Relation.Binary.PropositionalEquality as Eq using (_≢_; _≗_) open import Relation.Nullary.Negation using (¬_) -open import Framework.Variants using (Rose; Variant-is-VL) +open import Vatras.Framework.Variants using (Rose; Variant-is-VL) Variant = Rose ∞ -open import Framework.Annotation.IndexedDimension -open import Framework.Compiler -open import Framework.Definitions using (𝕍; 𝔽) -open import Framework.Relation.Expressiveness Variant using (_≽_; ≽-trans; _≻_; _⋡_; _≋_; compiler-cannot-exist) -open import Framework.Proof.ForFree Variant using (less-expressive-from-completeness; completeness-by-expressiveness; soundness-by-expressiveness) -open import Framework.Properties.Completeness Variant using (Complete) -open import Framework.Properties.Soundness Variant using (Sound) -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -open import Util.AuxProofs using (decidableEquality-×) -open import Util.String using (diagonal-ℕ; diagonal-ℕ⁻¹; diagonal-ℕ-proof) - -open import Lang.All +open import Vatras.Framework.Annotation.IndexedDimension +open import Vatras.Framework.Compiler +open import Vatras.Framework.Definitions using (𝕍; 𝔽) +open import Vatras.Framework.Relation.Expressiveness Variant using (_≽_; ≽-trans; _≻_; _⋡_; _≋_; compiler-cannot-exist) +open import Vatras.Framework.Proof.ForFree Variant using (less-expressive-from-completeness; completeness-by-expressiveness; soundness-by-expressiveness) +open import Vatras.Framework.Properties.Completeness Variant using (Complete) +open import Vatras.Framework.Properties.Soundness Variant using (Sound) +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +open import Vatras.Util.AuxProofs using (decidableEquality-×) +open import Vatras.Util.String using (diagonal-ℕ; diagonal-ℕ⁻¹; diagonal-ℕ-proof) + +open import Vatras.Lang.All open VariantList using (VariantListL) open CCC using (CCCL) open NCC using (NCCL) @@ -46,29 +46,29 @@ open OC using (WFOCL) open FST using (FSTL) open CCC.Encode using () renaming (encoder to CCC-Rose-encoder) -open import Translation.Lang.NCC.Rename using (NCC-rename≽NCC) -open import Translation.Lang.2CC.Rename using (2CC-rename; 2CC-rename≽2CC) - -import Translation.Lang.CCC-to-NCC as CCC-to-NCC -import Translation.Lang.NCC-to-CCC as NCC-to-CCC -import Translation.Lang.NCC.Grow as Grow -import Translation.Lang.NCC.ShrinkTo2 as ShrinkTo2 -import Translation.Lang.NCC.NCC-to-NCC as NCC-to-NCC -import Translation.Lang.NCC-to-2CC as NCC-to-2CC -import Translation.Lang.2CC-to-NCC as 2CC-to-NCC -import Translation.Lang.Transitive.CCC-to-2CC as CCC-to-2CC -import Translation.Lang.Transitive.2CC-to-CCC as 2CC-to-CCC -import Translation.Lang.2CC-to-ADT as 2CC-to-ADT -import Translation.Lang.ADT-to-2CC as ADT-to-2CC -import Translation.Lang.ADT.DeadElim as DeadElim -import Translation.Lang.ADT-to-VariantList as ADT-to-VariantList -import Translation.Lang.VariantList-to-CCC as VariantList-to-CCC -import Translation.Lang.ADT-to-NADT as ADT-to-NADT -import Translation.Lang.NADT-to-CCC 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 +open import Vatras.Translation.Lang.NCC.Rename using (NCC-rename≽NCC) +open import Vatras.Translation.Lang.2CC.Rename using (2CC-rename; 2CC-rename≽2CC) + +import Vatras.Translation.Lang.CCC-to-NCC as CCC-to-NCC +import Vatras.Translation.Lang.NCC-to-CCC as NCC-to-CCC +import Vatras.Translation.Lang.NCC.Grow as Grow +import Vatras.Translation.Lang.NCC.ShrinkTo2 as ShrinkTo2 +import Vatras.Translation.Lang.NCC.NCC-to-NCC as NCC-to-NCC +import Vatras.Translation.Lang.NCC-to-2CC as NCC-to-2CC +import Vatras.Translation.Lang.2CC-to-NCC as 2CC-to-NCC +import Vatras.Translation.Lang.Transitive.CCC-to-2CC as CCC-to-2CC +import Vatras.Translation.Lang.Transitive.2CC-to-CCC as 2CC-to-CCC +import Vatras.Translation.Lang.2CC-to-ADT as 2CC-to-ADT +import Vatras.Translation.Lang.ADT-to-2CC as ADT-to-2CC +import Vatras.Translation.Lang.ADT.DeadElim as DeadElim +import Vatras.Translation.Lang.ADT-to-VariantList as ADT-to-VariantList +import Vatras.Translation.Lang.VariantList-to-CCC as VariantList-to-CCC +import Vatras.Translation.Lang.ADT-to-NADT as ADT-to-NADT +import Vatras.Translation.Lang.NADT-to-CCC as NADT-to-CCC +import Vatras.Translation.Lang.OC-to-2CC as OC-to-2CC +import Vatras.Translation.Lang.OC-to-FST as OC-to-FST +import Vatras.Translation.Lang.FST-to-OC as FST-to-OC +import Vatras.Translation.Lang.FST-to-VariantList as FST-to-VariantList ``` diff --git a/src/Tutorial/A_NewLanguage.lagda.md b/src/Vatras/Tutorial/A_NewLanguage.lagda.md similarity index 95% rename from src/Tutorial/A_NewLanguage.lagda.md rename to src/Vatras/Tutorial/A_NewLanguage.lagda.md index 5e4ee9d5..5a1c6051 100644 --- a/src/Tutorial/A_NewLanguage.lagda.md +++ b/src/Vatras/Tutorial/A_NewLanguage.lagda.md @@ -9,14 +9,14 @@ variability language within our framework. It covers defining syntax, configurations, and semantics. ```agda -module Tutorial.A_NewLanguage where +module Vatras.Tutorial.A_NewLanguage where open import Data.List using (List) open import Size using (∞) -open import Framework.Definitions -open import Framework.Variants using (Rose; _-<_>-) -open import Framework.VariabilityLanguage +open import Vatras.Framework.Definitions +open import Vatras.Framework.Variants using (Rose; _-<_>-) +open import Vatras.Framework.VariabilityLanguage ``` To define your own language, you must first define its (abstract syntax) as a data type. @@ -79,7 +79,7 @@ V = Rose ∞ ⟦_⟧ = {!!} ``` where `V` is the type of variants. -In our paper and for the language comparisons implemented here, this type is often fixed to a rose tree `Rose ∞` (see [Variants.agda](src/Framework/Variants.agda)). +In our paper and for the language comparisons implemented here, this type is often fixed to a rose tree `Rose ∞` (see [Variants.agda](../Framework/Variants.agda)). You can also change the type of variants produced (e.g., as in Gruler's language, which produces a `GrulerVariant`) or even make your semantics generic in the type of variants. In case you decided to go with the example C-preprocessor-inspired syntax above, try to find a reasonable semantics for it. (At the very bottom of this file, you can find an example solution for the semantics, which you can use to complete the remaining tutorial. We encourage you to try to find one your own semantics though. 🙂) diff --git a/src/Tutorial/B_Translation.lagda.md b/src/Vatras/Tutorial/B_Translation.lagda.md similarity index 95% rename from src/Tutorial/B_Translation.lagda.md rename to src/Vatras/Tutorial/B_Translation.lagda.md index 74d0668d..04e4963a 100644 --- a/src/Tutorial/B_Translation.lagda.md +++ b/src/Vatras/Tutorial/B_Translation.lagda.md @@ -5,31 +5,31 @@ # Translating Variability Languages ```agda -module Tutorial.B_Translation where +module Vatras.Tutorial.B_Translation where open import Data.Product using (_,_) open import Data.List using (List) open import Size using (Size) -open import Framework.Definitions -open import Framework.Relation.Function using (_⇔_) -open import Framework.VariabilityLanguage -open import Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions +open import Vatras.Framework.Relation.Function using (_⇔_) +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Compiler using (LanguageCompiler) ``` In this tutorial, we are going to translate our new language from the last tutorial to another variability language. So first, we are going to import our previous definitions. ```agda -open import Tutorial.A_NewLanguage +open import Vatras.Tutorial.A_NewLanguage ``` Let's assume, we want to later prove that our new language is at least as expressive as binary choice calculus (`2CC`). We hence want to translate binary choice calculus to our new language: ```agda -open import Lang.All +open import Vatras.Lang.All open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) renaming (⟦_⟧ to ⟦_⟧₂) ``` @@ -97,7 +97,7 @@ So our goal is to prove the following, where `⟦_⟧₂` is the semantics of `2CC`, and `⟦_⟧` is the semantics of `MyLang`. ```agda -open import Data.EqIndexedSet +open import Vatras.Data.EqIndexedSet preservation : ∀ {A : 𝔸} {i : Size} → (e : 2CC F i A) diff --git a/src/Tutorial/C_Proofs.lagda.md b/src/Vatras/Tutorial/C_Proofs.lagda.md similarity index 90% rename from src/Tutorial/C_Proofs.lagda.md rename to src/Vatras/Tutorial/C_Proofs.lagda.md index 10746adc..0bf8f38e 100644 --- a/src/Tutorial/C_Proofs.lagda.md +++ b/src/Vatras/Tutorial/C_Proofs.lagda.md @@ -5,16 +5,16 @@ # Proving Properties of a Language ```agda -module Tutorial.C_Proofs where +module Vatras.Tutorial.C_Proofs where open import Data.Product using (Σ-syntax; ∃-syntax; _,_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -open import Framework.Definitions -open import Framework.VariabilityLanguage -open import Framework.Compiler using (LanguageCompiler) +open import Vatras.Framework.Definitions +open import Vatras.Framework.VariabilityLanguage +open import Vatras.Framework.Compiler using (LanguageCompiler) -open import Data.EqIndexedSet +open import Vatras.Data.EqIndexedSet ``` In this tutorial, we are going to prove our language from the first @@ -25,10 +25,10 @@ We will also cover what it takes to prove `soundness`, as well as So first, we are going to import our previous definitions and `2CC` ```agda -open import Tutorial.A_NewLanguage -open import Tutorial.B_Translation +open import Vatras.Tutorial.A_NewLanguage +open import Vatras.Tutorial.B_Translation -open import Lang.All +open import Vatras.Lang.All open 2CC using (2CC; 2CCL; _-<_>-; _⟨_,_⟩) renaming (⟦_⟧ to ⟦_⟧₂) ``` @@ -44,7 +44,7 @@ We can hence conclude that our language is at least as expressive as binary choice calculus from having constructed our compiler. ```agda -open import Framework.Relation.Expressiveness V +open import Vatras.Framework.Relation.Expressiveness V MyLang≽2CC : MyVarLang ≽ 2CCL F -- MyLang≽2CC : MyVarLang is-at-least-as-expressive-as 2CCL F @@ -77,9 +77,9 @@ expressiveness proofs, where we fix the annotation type `F : 𝔽` to `String`. If you changed the definition of `F` in the first tutorial, some of the following might not compiler. ```agda -open import Lang.All -open import Translation.LanguageMap -open Translation.LanguageMap.Expressiveness-String +open import Vatras.Lang.All +open import Vatras.Translation.LanguageMap +open Vatras.Translation.LanguageMap.Expressiveness-String ``` By transitivity, we can conlude that our variability language is @@ -119,9 +119,9 @@ change it if you like 🙂! (Some proofs might break but you can just replace them by a whole to experiment a bit)). ```agda -open import Framework.Properties.Completeness V -open import Framework.Proof.ForFree V -open Translation.LanguageMap.Completeness-String +open import Vatras.Framework.Properties.Completeness V +open import Vatras.Framework.Proof.ForFree V +open Vatras.Translation.LanguageMap.Completeness-String ``` In our library, it is already proven that binary choice calculus `2CC` @@ -180,7 +180,7 @@ open import Data.String using (_≟_) Try to figure out now how to conclude soundness of your language. ```agda -open import Framework.Properties.Soundness V +open import Vatras.Framework.Properties.Soundness V MyLang-is-Sound : Sound MyVarLang MyLang-is-Sound = {!!} diff --git a/src/Util/AuxProofs.agda b/src/Vatras/Util/AuxProofs.agda similarity index 99% rename from src/Util/AuxProofs.agda rename to src/Vatras/Util/AuxProofs.agda index 5c879b25..2646b973 100644 --- a/src/Util/AuxProofs.agda +++ b/src/Vatras/Util/AuxProofs.agda @@ -1,4 +1,4 @@ -module Util.AuxProofs where +module Vatras.Util.AuxProofs where open import Level using (Level) open import Function using (id; _∘_) diff --git a/src/Util/Embedding.agda b/src/Vatras/Util/Embedding.agda similarity index 87% rename from src/Util/Embedding.agda rename to src/Vatras/Util/Embedding.agda index 212db22f..c5a4292c 100644 --- a/src/Util/Embedding.agda +++ b/src/Vatras/Util/Embedding.agda @@ -1,4 +1,4 @@ -module Util.Embedding where +module Vatras.Util.Embedding where open import Function using (_∘_; id) open import Relation.Binary.PropositionalEquality using (_≗_) diff --git a/src/Util/Enumerable.agda b/src/Vatras/Util/Enumerable.agda similarity index 97% rename from src/Util/Enumerable.agda rename to src/Vatras/Util/Enumerable.agda index 572af543..22813a52 100644 --- a/src/Util/Enumerable.agda +++ b/src/Vatras/Util/Enumerable.agda @@ -4,7 +4,7 @@ that a type has a finite amount of instances (or might have infinite instances but only a finite subset of _unique_ instances w.r.t. to an equivalence relation). -} -module Util.Enumerable where +module Vatras.Util.Enumerable where open import Data.Nat using (ℕ; suc) open import Data.Fin using (Fin) diff --git a/src/Util/Existence.agda b/src/Vatras/Util/Existence.agda similarity index 96% rename from src/Util/Existence.agda rename to src/Vatras/Util/Existence.agda index df886144..867b26db 100644 --- a/src/Util/Existence.agda +++ b/src/Vatras/Util/Existence.agda @@ -1,4 +1,4 @@ -module Util.Existence where +module Vatras.Util.Existence where open import Agda.Primitive using (Level; _⊔_) open import Data.Product using (Σ; ∄) diff --git a/src/Util/Function.agda b/src/Vatras/Util/Function.agda similarity index 91% rename from src/Util/Function.agda rename to src/Vatras/Util/Function.agda index f0077aea..90970cc0 100644 --- a/src/Util/Function.agda +++ b/src/Vatras/Util/Function.agda @@ -1,4 +1,4 @@ -module Util.Function where +module Vatras.Util.Function where open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) diff --git a/src/Util/List.agda b/src/Vatras/Util/List.agda similarity index 98% rename from src/Util/List.agda rename to src/Vatras/Util/List.agda index 7f8ea3f0..bcc5981e 100644 --- a/src/Util/List.agda +++ b/src/Vatras/Util/List.agda @@ -1,7 +1,7 @@ {-| Utilities for lists. -} -module Util.List where +module Vatras.Util.List where open import Data.Bool using (Bool; true; false) open import Data.Fin using (Fin) @@ -11,7 +11,7 @@ open import Data.List as List using (List; []; _∷_; lookup; foldr; _++_) open import Data.List.Properties using (map-id; length-++) open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; toList; _⁺++⁺_) renaming (map to map⁺) open import Data.Vec as Vec using (Vec; []; _∷_) -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) open import Function using (id; _∘_; flip) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; _≗_; refl) diff --git a/src/Util/Named.agda b/src/Vatras/Util/Named.agda similarity index 94% rename from src/Util/Named.agda rename to src/Vatras/Util/Named.agda index cc3f4aa2..3af7d5e1 100644 --- a/src/Util/Named.agda +++ b/src/Vatras/Util/Named.agda @@ -1,4 +1,4 @@ -module Util.Named where +module Vatras.Util.Named where open import Data.String using (String; _++_) diff --git a/src/Util/Nat/AtLeast.agda b/src/Vatras/Util/Nat/AtLeast.agda similarity index 98% rename from src/Util/Nat/AtLeast.agda rename to src/Vatras/Util/Nat/AtLeast.agda index e2c14538..953617f3 100644 --- a/src/Util/Nat/AtLeast.agda +++ b/src/Vatras/Util/Nat/AtLeast.agda @@ -1,4 +1,4 @@ -module Util.Nat.AtLeast where +module Vatras.Util.Nat.AtLeast where open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) open import Data.Nat as ℕ using (ℕ; zero; suc; _+_; s≤s) diff --git a/src/Util/NonEmptyTraversable.agda b/src/Vatras/Util/NonEmptyTraversable.agda similarity index 93% rename from src/Util/NonEmptyTraversable.agda rename to src/Vatras/Util/NonEmptyTraversable.agda index 50037cc0..b568b95a 100644 --- a/src/Util/NonEmptyTraversable.agda +++ b/src/Vatras/Util/NonEmptyTraversable.agda @@ -1,7 +1,7 @@ {-| Traversable instance on non-empty lists. -} -module Util.NonEmptyTraversable where +module Vatras.Util.NonEmptyTraversable where open import Function using (_∘_) open import Data.List.NonEmpty using (List⁺; _∷_) diff --git a/src/Util/ShowHelpers.agda b/src/Vatras/Util/ShowHelpers.agda similarity index 95% rename from src/Util/ShowHelpers.agda rename to src/Vatras/Util/ShowHelpers.agda index a5eb9354..72fe7198 100644 --- a/src/Util/ShowHelpers.agda +++ b/src/Vatras/Util/ShowHelpers.agda @@ -1,7 +1,7 @@ {-| Utility functions for pretty printing. -} -module Util.ShowHelpers where +module Vatras.Util.ShowHelpers where open import Data.Bool using (Bool; true; false) open import Data.List using (List; map) diff --git a/src/Util/String.agda b/src/Vatras/Util/String.agda similarity index 99% rename from src/Util/String.agda rename to src/Vatras/Util/String.agda index d17a2f0e..2c07945f 100644 --- a/src/Util/String.agda +++ b/src/Vatras/Util/String.agda @@ -1,4 +1,4 @@ -module Util.String where +module Vatras.Util.String where open import Data.Bool using (true; false) open import Data.Char as Char using (Char) diff --git a/src/Util/Suffix.agda b/src/Vatras/Util/Suffix.agda similarity index 98% rename from src/Util/Suffix.agda rename to src/Vatras/Util/Suffix.agda index 21707bfc..d3381ce8 100644 --- a/src/Util/Suffix.agda +++ b/src/Vatras/Util/Suffix.agda @@ -1,4 +1,4 @@ -module Util.Suffix where +module Vatras.Util.Suffix where open import Data.Empty using (⊥-elim) open import Data.List using (List; _∷_) diff --git a/src/Util/UnwrapIndexedEquivalence.agda b/src/Vatras/Util/UnwrapIndexedEquivalence.agda similarity index 92% rename from src/Util/UnwrapIndexedEquivalence.agda rename to src/Vatras/Util/UnwrapIndexedEquivalence.agda index 5f5ff552..e9717667 100644 --- a/src/Util/UnwrapIndexedEquivalence.agda +++ b/src/Vatras/Util/UnwrapIndexedEquivalence.agda @@ -5,7 +5,7 @@ open import Relation.Binary.Indexed.Heterogeneous using ( IRel; IsIndexedEquivalence) -module Util.UnwrapIndexedEquivalence where +module Vatras.Util.UnwrapIndexedEquivalence where {-| Unwraps an indexed equivalence. diff --git a/src/Util/Vec.agda b/src/Vatras/Util/Vec.agda similarity index 96% rename from src/Util/Vec.agda rename to src/Vatras/Util/Vec.agda index 0e2f54ec..d573888a 100644 --- a/src/Util/Vec.agda +++ b/src/Vatras/Util/Vec.agda @@ -1,4 +1,4 @@ -module Util.Vec where +module Vatras.Util.Vec where open import Data.Fin as Fin using (Fin; zero; suc) open import Data.List as List using (List; []; _∷_) @@ -7,8 +7,8 @@ import Data.List.Properties as List open import Data.Nat as ℕ using (ℕ; zero; suc; _≤_; s≤s; z≤n) open import Data.Vec as Vec using (Vec; []; _∷_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl) -import Util.List as List -open import Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) +import Vatras.Util.List as List +open import Vatras.Util.Nat.AtLeast as ℕ≥ using (ℕ≥; sucs) -- Duplicates the last element of a vector to increase its length. saturate : ∀ {ℓ} {A : Set ℓ} {n : ℕ≥ 1} {m : ℕ}