From 51fb5875ea80001290e5b5f0e203dce08506fdda Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sat, 9 May 2020 17:15:27 +0000
Subject: [PATCH] move sessions to a separate directory
git-svn-id: https://projects.brucker.ch/hol-testgen/svn/HOL-TestGen/trunk/hol-testgen@14189 3260e6d1-4efc-4170-b0a7-36055960796d
---
Citadelle/ROOT | 58 +++++++++----------
.../Analysis_deep.thy | 0
.../Analysis_shallow.thy | 0
.../{ => Design_generation}/Design_deep.thy | 0
.../Design_shallow.thy | 0
.../archive/{ => compiler}/Monads.thy | 0
.../{ => uml_ocl}/Flight_Model_compact.thy | 0
.../{ => uml_ocl}/Isabelle_Finite_Set.thy | 0
.../{ => uml_ocl}/OCL_core_experiments.thy | 0
.../OCL_lib_Gogolla_challenge.thy | 0
.../OCL_lib_Gogolla_challenge_integer.thy | 0
.../OCL_lib_Gogolla_challenge_naive.thy | 0
.../archive/{ => uml_ocl}/Simple_Model.thy | 0
.../archive/{ => uml_ocl}/Toy_deep.thy | 4 +-
.../archive/{ => uml_ocl}/Toy_shallow.thy | 0
.../examples/{ => uml_ocl}/AbstractList.thy | 0
.../examples/{ => uml_ocl}/Bank_Model.thy | 0
.../{ => uml_ocl}/Bank_Test_Model.thy | 0
.../{ => uml_ocl}/Clocks_Lib_Model.thy | 0
.../examples/{ => uml_ocl}/Flight_Model.thy | 0
.../examples/{ => uml_ocl}/LinkedList.thy | 0
.../examples/{ => uml_ocl}/ListRefinement.thy | 0
.../UML_UnlimitedNatural.thy | 0
Citadelle/src/compiler/core/Core_init.thy | 2 +-
.../{compiler => compiler_misc}/Aux_proof.thy | 0
.../Aux_tactic.thy | 0
.../{compiler => compiler_misc}/Aux_text.thy | 0
.../src/{compiler => compiler_misc}/Rail.thy | 0
Citadelle/src/uml_ocl/UML_OCL.thy | 4 +-
29 files changed, 32 insertions(+), 36 deletions(-)
rename Citadelle/examples/Employee_Model/{ => Analysis_generation}/Analysis_deep.thy (100%)
rename Citadelle/examples/Employee_Model/{ => Analysis_generation}/Analysis_shallow.thy (100%)
rename Citadelle/examples/Employee_Model/{ => Design_generation}/Design_deep.thy (100%)
rename Citadelle/examples/Employee_Model/{ => Design_generation}/Design_shallow.thy (100%)
rename Citadelle/examples/archive/{ => compiler}/Monads.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/Flight_Model_compact.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/Isabelle_Finite_Set.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/OCL_core_experiments.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/OCL_lib_Gogolla_challenge.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/OCL_lib_Gogolla_challenge_integer.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/OCL_lib_Gogolla_challenge_naive.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/Simple_Model.thy (100%)
rename Citadelle/examples/archive/{ => uml_ocl}/Toy_deep.thy (99%)
rename Citadelle/examples/archive/{ => uml_ocl}/Toy_shallow.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/AbstractList.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/Bank_Model.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/Bank_Test_Model.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/Clocks_Lib_Model.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/Flight_Model.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/LinkedList.thy (100%)
rename Citadelle/examples/{ => uml_ocl}/ListRefinement.thy (100%)
rename Citadelle/src/{basic_types => basic_types_extra}/UML_UnlimitedNatural.thy (100%)
rename Citadelle/src/{compiler => compiler_misc}/Aux_proof.thy (100%)
rename Citadelle/src/{compiler => compiler_misc}/Aux_tactic.thy (100%)
rename Citadelle/src/{compiler => compiler_misc}/Aux_text.thy (100%)
rename Citadelle/src/{compiler => compiler_misc}/Rail.thy (100%)
diff --git a/Citadelle/ROOT b/Citadelle/ROOT
index 77c05b38a60..6b501da39fb 100644
--- a/Citadelle/ROOT
+++ b/Citadelle/ROOT
@@ -122,44 +122,40 @@ session "Citadelle_C_model-dirty" in "src/compiler_citadelle_c/ml" = "Citadelle_
(******************************************************)
-session "Max-dirty" in src = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
+session "Max-dirty" = "HOL-Library" (* Note: replacing with FOCL will fail! *) +
options [quick_and_dirty]
sessions
OCL
FOCL
- Isabelle_Meta_Model
theories
- "../src/basic_types/UML_UnlimitedNatural"
-
- "../examples/empirical_evaluation/Class_model"
+ "src/basic_types_extra/UML_UnlimitedNatural"
- "../src/compiler/Generator_static"
- "../src/compiler/meta/Printer_init"
+ "examples/empirical_evaluation/Class_model"
- "../doc/Employee_AnalysisModel_UMLPart_generated"
- "../doc/Employee_DesignModel_UMLPart_generated"
+ "doc/Employee_AnalysisModel_UMLPart_generated"
+ "doc/Employee_DesignModel_UMLPart_generated"
- "../examples/Bank_Model"
- "../examples/Bank_Test_Model"
- "../examples/Clocks_Lib_Model"
- (*"../examples/Employee_Model/Analysis_deep"*)
- "../examples/Employee_Model/Analysis_shallow"
- (*"../examples/Employee_Model/Design_deep"*)
- "../examples/Employee_Model/Design_shallow"
- "../examples/Flight_Model"
- "../examples/AbstractList"
- "../examples/LinkedList"
- (*"../examples/ListRefinement"*)
- "../examples/archive/Flight_Model_compact"
- "../examples/archive/Simple_Model"
- "../examples/archive/Toy_deep"
- "../examples/archive/Toy_shallow"
+ "examples/uml_ocl/Bank_Model"
+ "examples/uml_ocl/Bank_Test_Model"
+ "examples/uml_ocl/Clocks_Lib_Model"
+ (*"examples/Employee_Model/Analysis_generation/Analysis_deep"*)
+ "examples/Employee_Model/Analysis_generation/Analysis_shallow"
+ (*"examples/Employee_Model/Design_generation/Design_deep"*)
+ "examples/Employee_Model/Design_generation/Design_shallow"
+ "examples/uml_ocl/Flight_Model"
+ "examples/uml_ocl/AbstractList"
+ "examples/uml_ocl/LinkedList"
+ (*"examples/uml_ocl/ListRefinement"*)
+ "examples/archive/uml_ocl/Flight_Model_compact"
+ "examples/archive/uml_ocl/Simple_Model"
+ "examples/archive/uml_ocl/Toy_deep"
+ "examples/archive/uml_ocl/Toy_shallow"
- "../src/compiler/Aux_proof"
- "../src/compiler/Aux_tactic"
- "../src/compiler/Aux_text"
- "../src/compiler/Rail"
+ "src/compiler_misc/Aux_proof"
+ "src/compiler_misc/Aux_tactic"
+ "src/compiler_misc/Aux_text"
+ "src/compiler_misc/Rail"
- "../examples/archive/OCL_core_experiments"
- "../examples/archive/OCL_lib_Gogolla_challenge_naive"
- "../examples/archive/OCL_lib_Gogolla_challenge_integer"
+ "examples/archive/uml_ocl/OCL_core_experiments"
+ "examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive"
+ "examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_integer"
diff --git a/Citadelle/examples/Employee_Model/Analysis_deep.thy b/Citadelle/examples/Employee_Model/Analysis_generation/Analysis_deep.thy
similarity index 100%
rename from Citadelle/examples/Employee_Model/Analysis_deep.thy
rename to Citadelle/examples/Employee_Model/Analysis_generation/Analysis_deep.thy
diff --git a/Citadelle/examples/Employee_Model/Analysis_shallow.thy b/Citadelle/examples/Employee_Model/Analysis_generation/Analysis_shallow.thy
similarity index 100%
rename from Citadelle/examples/Employee_Model/Analysis_shallow.thy
rename to Citadelle/examples/Employee_Model/Analysis_generation/Analysis_shallow.thy
diff --git a/Citadelle/examples/Employee_Model/Design_deep.thy b/Citadelle/examples/Employee_Model/Design_generation/Design_deep.thy
similarity index 100%
rename from Citadelle/examples/Employee_Model/Design_deep.thy
rename to Citadelle/examples/Employee_Model/Design_generation/Design_deep.thy
diff --git a/Citadelle/examples/Employee_Model/Design_shallow.thy b/Citadelle/examples/Employee_Model/Design_generation/Design_shallow.thy
similarity index 100%
rename from Citadelle/examples/Employee_Model/Design_shallow.thy
rename to Citadelle/examples/Employee_Model/Design_generation/Design_shallow.thy
diff --git a/Citadelle/examples/archive/Monads.thy b/Citadelle/examples/archive/compiler/Monads.thy
similarity index 100%
rename from Citadelle/examples/archive/Monads.thy
rename to Citadelle/examples/archive/compiler/Monads.thy
diff --git a/Citadelle/examples/archive/Flight_Model_compact.thy b/Citadelle/examples/archive/uml_ocl/Flight_Model_compact.thy
similarity index 100%
rename from Citadelle/examples/archive/Flight_Model_compact.thy
rename to Citadelle/examples/archive/uml_ocl/Flight_Model_compact.thy
diff --git a/Citadelle/examples/archive/Isabelle_Finite_Set.thy b/Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy
similarity index 100%
rename from Citadelle/examples/archive/Isabelle_Finite_Set.thy
rename to Citadelle/examples/archive/uml_ocl/Isabelle_Finite_Set.thy
diff --git a/Citadelle/examples/archive/OCL_core_experiments.thy b/Citadelle/examples/archive/uml_ocl/OCL_core_experiments.thy
similarity index 100%
rename from Citadelle/examples/archive/OCL_core_experiments.thy
rename to Citadelle/examples/archive/uml_ocl/OCL_core_experiments.thy
diff --git a/Citadelle/examples/archive/OCL_lib_Gogolla_challenge.thy b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy
similarity index 100%
rename from Citadelle/examples/archive/OCL_lib_Gogolla_challenge.thy
rename to Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge.thy
diff --git a/Citadelle/examples/archive/OCL_lib_Gogolla_challenge_integer.thy b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_integer.thy
similarity index 100%
rename from Citadelle/examples/archive/OCL_lib_Gogolla_challenge_integer.thy
rename to Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_integer.thy
diff --git a/Citadelle/examples/archive/OCL_lib_Gogolla_challenge_naive.thy b/Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy
similarity index 100%
rename from Citadelle/examples/archive/OCL_lib_Gogolla_challenge_naive.thy
rename to Citadelle/examples/archive/uml_ocl/OCL_lib_Gogolla_challenge_naive.thy
diff --git a/Citadelle/examples/archive/Simple_Model.thy b/Citadelle/examples/archive/uml_ocl/Simple_Model.thy
similarity index 100%
rename from Citadelle/examples/archive/Simple_Model.thy
rename to Citadelle/examples/archive/uml_ocl/Simple_Model.thy
diff --git a/Citadelle/examples/archive/Toy_deep.thy b/Citadelle/examples/archive/uml_ocl/Toy_deep.thy
similarity index 99%
rename from Citadelle/examples/archive/Toy_deep.thy
rename to Citadelle/examples/archive/uml_ocl/Toy_deep.thy
index 6b5d9ed8281..34501b280a9 100644
--- a/Citadelle/examples/archive/Toy_deep.thy
+++ b/Citadelle/examples/archive/uml_ocl/Toy_deep.thy
@@ -379,11 +379,11 @@ subsection\<open>Designing Class Models (V): Inspection of Generated Files\<clos
text\<open>
According to options given to the (first) command @{command generation_syntax} above,
we retrieve the first generated file in the mentioned directory:
-@{file "../../doc/Employee_DesignModel_UMLPart_generated.thy"}.
+@{file "../../../doc/Employee_DesignModel_UMLPart_generated.thy"}.
Because this file still contains meta-commands, we are here executing again
a new generating step inside this file, the new result becomes saved in
-@{file "../../doc/Employee_DesignModel_UMLPart_generated_generated.thy"}.
+@{file "../../../doc/Employee_DesignModel_UMLPart_generated_generated.thy"}.
As remark, in this last file, the dependency to @{theory FOCL.Generator_dynamic_sequential} was
automatically removed because the meta-compiler has detected the absence of meta-commands
in the generated content.
diff --git a/Citadelle/examples/archive/Toy_shallow.thy b/Citadelle/examples/archive/uml_ocl/Toy_shallow.thy
similarity index 100%
rename from Citadelle/examples/archive/Toy_shallow.thy
rename to Citadelle/examples/archive/uml_ocl/Toy_shallow.thy
diff --git a/Citadelle/examples/AbstractList.thy b/Citadelle/examples/uml_ocl/AbstractList.thy
similarity index 100%
rename from Citadelle/examples/AbstractList.thy
rename to Citadelle/examples/uml_ocl/AbstractList.thy
diff --git a/Citadelle/examples/Bank_Model.thy b/Citadelle/examples/uml_ocl/Bank_Model.thy
similarity index 100%
rename from Citadelle/examples/Bank_Model.thy
rename to Citadelle/examples/uml_ocl/Bank_Model.thy
diff --git a/Citadelle/examples/Bank_Test_Model.thy b/Citadelle/examples/uml_ocl/Bank_Test_Model.thy
similarity index 100%
rename from Citadelle/examples/Bank_Test_Model.thy
rename to Citadelle/examples/uml_ocl/Bank_Test_Model.thy
diff --git a/Citadelle/examples/Clocks_Lib_Model.thy b/Citadelle/examples/uml_ocl/Clocks_Lib_Model.thy
similarity index 100%
rename from Citadelle/examples/Clocks_Lib_Model.thy
rename to Citadelle/examples/uml_ocl/Clocks_Lib_Model.thy
diff --git a/Citadelle/examples/Flight_Model.thy b/Citadelle/examples/uml_ocl/Flight_Model.thy
similarity index 100%
rename from Citadelle/examples/Flight_Model.thy
rename to Citadelle/examples/uml_ocl/Flight_Model.thy
diff --git a/Citadelle/examples/LinkedList.thy b/Citadelle/examples/uml_ocl/LinkedList.thy
similarity index 100%
rename from Citadelle/examples/LinkedList.thy
rename to Citadelle/examples/uml_ocl/LinkedList.thy
diff --git a/Citadelle/examples/ListRefinement.thy b/Citadelle/examples/uml_ocl/ListRefinement.thy
similarity index 100%
rename from Citadelle/examples/ListRefinement.thy
rename to Citadelle/examples/uml_ocl/ListRefinement.thy
diff --git a/Citadelle/src/basic_types/UML_UnlimitedNatural.thy b/Citadelle/src/basic_types_extra/UML_UnlimitedNatural.thy
similarity index 100%
rename from Citadelle/src/basic_types/UML_UnlimitedNatural.thy
rename to Citadelle/src/basic_types_extra/UML_UnlimitedNatural.thy
diff --git a/Citadelle/src/compiler/core/Core_init.thy b/Citadelle/src/compiler/core/Core_init.thy
index 581656eaa09..517a42932e7 100644
--- a/Citadelle/src/compiler/core/Core_init.thy
+++ b/Citadelle/src/compiler/core/Core_init.thy
@@ -507,7 +507,7 @@ definition "print_access_dot_consts_ty attr_ty =
print_infra_type_synonym_class_set_name name)
| OclTy_object (OclTyObj (OclTyCore_pre s) _) \<Rightarrow> Raw (wrap_oclty s)
| OclTy_base_unlimitednatural \<Rightarrow> str_hol_of_ty_all Typ_apply ty_base attr_ty
- \<comment> \<open>REMARK Dependencies to \<^file>\<open>../../basic_types/UML_UnlimitedNatural.thy\<close> can be detected and added
+ \<comment> \<open>REMARK Dependencies to \<^file>\<open>../../basic_types_extra/UML_UnlimitedNatural.thy\<close> can be detected and added
so that this pattern clause would be merged with the default case\<close>
| OclTy_collection _ _ \<Rightarrow> Raw (fst (print_infra_type_synonym_class_rec_aux attr_ty))
| OclTy_pair _ _ \<Rightarrow> Raw (fst (print_infra_type_synonym_class_rec_aux attr_ty))
diff --git a/Citadelle/src/compiler/Aux_proof.thy b/Citadelle/src/compiler_misc/Aux_proof.thy
similarity index 100%
rename from Citadelle/src/compiler/Aux_proof.thy
rename to Citadelle/src/compiler_misc/Aux_proof.thy
diff --git a/Citadelle/src/compiler/Aux_tactic.thy b/Citadelle/src/compiler_misc/Aux_tactic.thy
similarity index 100%
rename from Citadelle/src/compiler/Aux_tactic.thy
rename to Citadelle/src/compiler_misc/Aux_tactic.thy
diff --git a/Citadelle/src/compiler/Aux_text.thy b/Citadelle/src/compiler_misc/Aux_text.thy
similarity index 100%
rename from Citadelle/src/compiler/Aux_text.thy
rename to Citadelle/src/compiler_misc/Aux_text.thy
diff --git a/Citadelle/src/compiler/Rail.thy b/Citadelle/src/compiler_misc/Rail.thy
similarity index 100%
rename from Citadelle/src/compiler/Rail.thy
rename to Citadelle/src/compiler_misc/Rail.thy
diff --git a/Citadelle/src/uml_ocl/UML_OCL.thy b/Citadelle/src/uml_ocl/UML_OCL.thy
index 6bb69dc2f93..b959e60dd6f 100644
--- a/Citadelle/src/uml_ocl/UML_OCL.thy
+++ b/Citadelle/src/uml_ocl/UML_OCL.thy
@@ -45,8 +45,8 @@
theory UML_OCL
imports OCL.UML_Main
- "../../examples/archive/Monads" (* NOTE: perform lazily the extraction of generation_syntax
- so that dependencies can alternate among theories *)
+ "../../examples/archive/compiler/Monads" (* NOTE: perform lazily the extraction of generation_syntax
+ so that dependencies can alternate among theories *)
"../compiler/Static"
"../compiler/Generator_dynamic_sequential"
begin
--
GitLab