diff --git a/Citadelle/ROOT b/Citadelle/ROOT
index 77c05b38a606eb86f017fb6111bdc3a514cb2948..6b501da39fb4e9bee674a82cad4138f62bd2a60c 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 6b5d9ed8281232dfff48a78007d4f0e903a0e949..34501b280a980d725ac33f1173a87eb1e590b242 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 581656eaa09f4a79162b3fb8b8398dc1e941e9e6..517a42932e775c2fda4f76c6ad2b331ebde30913 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 6bb69dc2f933e44942e5eea8f8ea80f5a00bbb7e..b959e60dd6fa26efff0109ee453f9147afc2a02e 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