diff --git a/thys/Isabelle_Meta_Model/Antiquote_Setup.thy b/thys/Isabelle_Meta_Model/Antiquote_Setup.thy new file mode 100644 --- /dev/null +++ b/thys/Isabelle_Meta_Model/Antiquote_Setup.thy @@ -0,0 +1,9 @@ +(*<*) +theory Antiquote_Setup +imports Main +begin + +ML_file \~~/src/Doc/antiquote_setup.ML\ + +end +(*>*) diff --git a/thys/Isabelle_Meta_Model/ROOT b/thys/Isabelle_Meta_Model/ROOT --- a/thys/Isabelle_Meta_Model/ROOT +++ b/thys/Isabelle_Meta_Model/ROOT @@ -1,43 +1,44 @@ chapter AFP - + session Isabelle_Meta_Model (AFP) = "HOL-Library" + description "Isabelle_Meta_Model containing a Toy Example" options [timeout = 600] directories "document" "isabelle_home/src/HOL" "isabelle_home/src/HOL/ex" "isabelle_home/src/Pure/Isar" "isabelle_home/src/Tools/Code" "meta_isabelle" "toy_example" "toy_example/document_generated" "toy_example/embedding" "toy_example/embedding/core" "toy_example/embedding/meta_toy" "toy_example/generator" theories [document = false] + Antiquote_Setup "isabelle_home/src/HOL/Isabelle_Main0" "isabelle_home/src/HOL/Isabelle_Main1" "isabelle_home/src/HOL/Isabelle_Main2" theories "meta_isabelle/Parser_Pure" "meta_isabelle/Meta_Isabelle" "meta_isabelle/Printer_Isabelle" theories [document = false] "toy_example/embedding/Printer" theories "toy_example/embedding/Generator_static" "toy_example/embedding/Generator_dynamic_sequential" "toy_example/generator/Design_deep" "toy_example/generator/Design_shallow" "document/Rail" theories (* This part ensures that generated theories are accepted: in general, if X..._generated_generated.thy is wellformed then we also have X..._generated.thy wellformed *) "toy_example/document_generated/Design_generated" "toy_example/document_generated/Design_generated_generated" document_files "root.bib" "root.tex" diff --git a/thys/Isabelle_Meta_Model/document/Rail.thy b/thys/Isabelle_Meta_Model/document/Rail.thy --- a/thys/Isabelle_Meta_Model/document/Rail.thy +++ b/thys/Isabelle_Meta_Model/document/Rail.thy @@ -1,383 +1,382 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) (*<*) theory Rail -imports "../toy_example/embedding/Generator_dynamic_sequential" +imports "../toy_example/embedding/Generator_dynamic_sequential" "../Antiquote_Setup" begin -ML_file \~~/src/Doc/antiquote_setup.ML\ (*>*) section\Main Setup of Meta Commands\ text \ \begin{matharray}{rcl} @{command_def generation_syntax} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command generation_syntax} ( '[' (@{syntax syntax} * ',') ']' | @{syntax syntax} | @'deep' @'flush_all') ; @{syntax_def syntax}: @'deep' @{syntax semantics} @{syntax deep_embedding} | @'shallow' @{syntax semantics} @{syntax long_or_dirty} | @'syntax_print' number? ; @{syntax_def semantics}: ('(' @'generation_semantics' \ ('[' (@'design' | @'analysis') (',' @'oid_start' nat)? ']') ')')? ; @{syntax_def deep_embedding}: (@'skip_export')? \ ('(' @'THEORY' name ')' \ '(' @'IMPORTS' '[' (name * ',') ']' name ')')? \ (@'SECTION')? \ @{syntax long_or_dirty} \ ('[' (@{syntax export_code} + ',') ']') \ ('(' @'output_directory' name ')')? ; @{syntax_def export_code}: @'in' ( 'Haskell' | (( 'OCaml' | 'Scala' | 'SML') @'module_name' name)) ( '(' args ')' ) ? ; @{syntax_def long_or_dirty}: (@'SORRY' | @'no_dirty')? ; \} \ text\ @{command generation_syntax} sets the behavior of all incoming meta-commands. -By default, without firstly writing @{command generation_syntax}, -meta-commands will only print in output what they have parsed, +By default, without firstly writing @{command generation_syntax}, +meta-commands will only print in output what they have parsed, this is similar as giving to @{command generation_syntax} a non-empty list having only @{keyword "syntax_print"} as elements (on the other hand, nothing is printed when an empty list is received). Additionally @{keyword "syntax_print"} can be followed by an integer indicating the printing depth in output, similar as declaring @{attribute "ML_print_depth"} with an integer, but the global option @{keyword "syntax_print"} is restricted to meta-commands. Besides the printing of syntaxes, several options are provided to further analyze the semantics of languages being embedded, and tell if their evaluation should occur immediately using the @{keyword "shallow"} mode, or to only display what would have been evaluated using the @{keyword "deep"} mode (i.e., to only show the generated Isabelle content in the output window). Since several occurrences of @{keyword "deep"}, @{keyword "shallow"} or @{keyword "syntax_print"} can appear in the parameterizing list, for each meta-command the overall evaluation respects the order of events given in the list (from head to tail). At the time of writing, it is only possible to evaluate this list sequentially: the execution stops as soon as one first error is raised, thus ignoring remaining events. @{command generation_syntax} @{keyword "deep"} @{keyword "flush_all"} performs as side effect the writing of all the generated Isabelle contents to the hard disk (all at the calling time), by iterating the saving for each @{keyword "deep"} mode in the list. In particular, this is only effective if there is at least one @{keyword "deep"} mode earlier declared. As a side note, target languages for the @{keyword "deep"} mode currently supported are: Haskell, OCaml, Scala and SML. So in principle, all these targets generate the same Isabelle content and exit correctly. However, depending on the intended use, exporting with some targets may be more appropriate -than other targets: +than other targets: \begin{itemize} -\item For efficiency reasons, the meta-compiler has implemented a particular optimization -for accelerating the process of evaluating incoming meta-commands. -By default in Haskell and OCaml, the meta-compiler (at HOL side) is exported only once, -during the @{command generation_syntax} step. +\item For efficiency reasons, the meta-compiler has implemented a particular optimization +for accelerating the process of evaluating incoming meta-commands. +By default in Haskell and OCaml, the meta-compiler (at HOL side) is exported only once, +during the @{command generation_syntax} step. Then all incoming meta-commands are considered as arguments sent to the exported meta-compiler. As a compositionality aspect, these arguments are compiled then linked together with the (already compiled) meta-compiler, but -this implies the use of one call of -\unsafeCoerce\ in Haskell and one \Obj.magic\ statement in OCaml +this implies the use of one call of +\unsafeCoerce\ in Haskell and one \Obj.magic\ statement in OCaml (otherwise another solution would be to extract the meta-compiler as a functor). Similar optimizations are not yet implemented for Scala and are only half-implemented for the SML target (which basically performs a step of marshalling to string in Isabelle/ML). -\item For safety reasons, it simply suffices to extract all the meta-compiler together with the respective -arguments in front of each incoming meta-commands everytime, then the overall needs to be newly -compiled everytime. -This is the current implemented behavior for Scala. +\item For safety reasons, it simply suffices to extract all the meta-compiler together with the respective +arguments in front of each incoming meta-commands everytime, then the overall needs to be newly +compiled everytime. +This is the current implemented behavior for Scala. For Haskell, OCaml and SML, it was also the default behavior in a prototyping version of the compiler, as a consequence one can restore that functionality for future versions. \end{itemize} Concerning the semantics of generated contents, if lemmas and proofs are generated, @{keyword "SORRY"} allows to explicitly skip the evaluation of all proofs, -irrespective of the presence of @{command sorry} or not in generated proofs. -In any cases, the semantics of @{command sorry} has not been overloaded, e.g., +irrespective of the presence of @{command sorry} or not in generated proofs. +In any cases, the semantics of @{command sorry} has not been overloaded, e.g., red background may appear as usual. Finally @{keyword "generation_semantics"} is a container for specifying various options for varying the semantics of languages being embedded. -For example, @{keyword "design"} and @{keyword "analysis"} are two options for specifying how +For example, @{keyword "design"} and @{keyword "analysis"} are two options for specifying how the modelling of objects will be represented in the Toy Language. Similarly, this would be a typical place for options like \eager\ or \lazy\ for choosing how the evaluation should happen... \ section\All Meta Commands of the Toy Language\ text \ \begin{matharray}{rcl} @{command_def Class} & : & \theory \ theory\ \\ @{command_def Abstract_class} & : & \theory \ theory\ \\ \end{matharray} @{rail \ ( @@{command Class} | @@{command Abstract_class}) ( binding '=' @{syntax type_base} | @{syntax type_object} @{syntax class}) ; @{syntax_def class}: @'Attributes'? ((binding ':' @{syntax toy_type}) * (';'?)) \ @{syntax context} ; @{syntax_def context}: (( ((() | @'Operations' | '::') binding @{syntax toy_type} \ ('=' term | term)? (((@'Pre' | @'Post') @{syntax use_prop} | @{syntax invariant}) * ()) ) | @{syntax invariant}) * ()) ; @{syntax_def invariant}: @'Constraints'? @'Existential'? @'Inv' @{syntax use_prop} ; \} \ text \ \begin{matharray}{rcl} @{command_def Aggregation} & : & \theory \ theory\ \\ @{command_def Association} & : & \theory \ theory\ \\ @{command_def Composition} & : & \theory \ theory\ \end{matharray} @{rail \ ( @@{command Aggregation} | @@{command Association} | @@{command Composition}) binding? @{syntax association} ; @{syntax_def association}: @'Between'? (@{syntax association_end} (@{syntax association_end}+))? ; @{syntax_def association_end}: @{syntax type_object} @{syntax category} ';'? ; \} \ text \ \begin{matharray}{rcl} @{command_def Associationclass} & : & \theory \ theory\ \\ @{command_def Abstract_associationclass} & : & \theory \ theory\ \end{matharray} @{rail \ ( @@{command Associationclass} | @@{command Abstract_associationclass}) @{syntax type_object} \ @{syntax association} @{syntax class} (() | 'aggregation' | 'composition') ; \} \ text \ \begin{matharray}{rcl} @{command_def Context} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command Context} ('[' @'shallow' ']')? @{syntax type_object} @{syntax context} ; \} \ text \ \begin{matharray}{rcl} @{command_def Instance} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command Instance} ((binding ('::' @{syntax type_object})? '=' \ (@{syntax term_object} | @{syntax object_cast})) * ('and'?)) ; @{syntax_def term_object}: ('[' ((('(' binding ',' binding ')' '|=')? \ binding '=' @{syntax toy_term}) * ',') ']') ; @{syntax_def object_cast}: '(' @{syntax term_object} '::' @{syntax type_object} ')' \ (('\' 'toyAsType' '(' @{syntax type_object} ')') * ()) ; \} \ text \ \begin{matharray}{rcl} @{command_def State} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command State} ('[' @'shallow' ']')? binding ('=' @{syntax state})? ; @{syntax_def state}: '[' ((binding | @{syntax object_cast}) * ',') ']' ; \} \ text \ \begin{matharray}{rcl} @{command_def PrePost} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command PrePost} ('[' @'shallow' ']')? (binding '=')? \ @{syntax pre_post} @{syntax pre_post}? ; @{syntax_def pre_post}: binding | @{syntax state} ; \} \ text \ \begin{matharray}{rcl} @{command_def End} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command End} ('[' 'forced' ']' | '!')? \} \ text \ \begin{matharray}{rcl} @{command_def BaseType} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command BaseType} '[' (@{syntax term_base} * ',') ']' ; \} \ section\Extensions of Isabelle Commands\ (* WARNING syntax errors during the extraction to LaTeX for the symbol "acute": fun\, definition\ or code_reflect\ *) text \ \begin{matharray}{rcl} @{command_def "code_reflect'"} & : & \theory \ theory\ \end{matharray} @{rail \ @@{command "code_reflect'"} @'open'? string \ ( @'datatypes' ( string '=' ( '_' | ( string + '|' ) + @'and' ) ) ) ? \ ( @'functions' ( string + ) ) ? ( @'file' string ) ? ; \} \ text\ @{command code_reflect'} has the same semantics as @{command code_reflect} except that it additionally contains the option @{keyword "open"} inspired from the command @{command export_code} (with the same semantics). \ text \ \begin{matharray}{rcl} @{command_def lazy_code_printing} & : & \theory \ theory\ \\ @{command_def apply_code_printing} & : & \theory \ theory\ \\ @{command_def apply_code_printing_reflect} & : & \local_theory \ local_theory\ \end{matharray} @{rail \ @@{command lazy_code_printing} ( ( printing_const | printing_typeconstructor | printing_class | printing_class_relation | printing_class_instance | printing_module ) + '|' ) ; @@{command apply_code_printing} '(' ')' ; @@{command apply_code_printing_reflect} text ; \} \ text\ -@{command lazy_code_printing} has the same semantics as @{command code_printing} +@{command lazy_code_printing} has the same semantics as @{command code_printing} or @{command ML}, except that no side effects occur until we give more details about its intended future semantics: this will be precised by calling @{command apply_code_printing} or @{command apply_code_printing_reflect}. \ text\ @{command apply_code_printing} repeatedly calls @{command code_printing} to all previously registered elements with @{command lazy_code_printing} (the order is preserved). \ text\ @{command apply_code_printing_reflect} repeatedly calls @{command ML} to all previously registered elements with @{command lazy_code_printing} (the order is preserved). As a consequence, code for other targets (Haskell, OCaml, Scala) are ignored. Moreover before the execution of the overall, it is possible to give an additional piece of SML code as argument to priorly execute. \ (*<*) end (*>*) diff --git a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_static.thy b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_static.thy --- a/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_static.thy +++ b/thys/Isabelle_Meta_Model/toy_example/embedding/Generator_static.thy @@ -1,107 +1,105 @@ (****************************************************************************** * Citadelle * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) text\We present two solutions for obtaining an Isabelle file.\ section\Static Meta Embedding with Exportation\ theory Generator_static -imports Printer +imports Printer "../../Antiquote_Setup" begin (*<*) -ML_file \~~/src/Doc/antiquote_setup.ML\ - declare[[cartouche_type' = "abr_string"]] (*>*) text \In the ``static'' solution: the user manually generates the Isabelle file after writing by hand a Toy input to translate. The input is not written with the syntax of the Toy Language, but with raw Isabelle constructors.\ subsection\Giving an Input to Translate\ definition "Design = (let n = \n1 n2. ToyTyObj (ToyTyCore_pre n1) (case n2 of None \ [] | Some n2 \ [[ToyTyCore_pre n2]]) ; mk = \n l. toy_class_raw.make n l [] False in [ mk (n \Galaxy\ None) [(\sound\, ToyTy_raw \unit\), (\moving\, ToyTy_raw \bool\)] , mk (n \Planet\ (Some \Galaxy\)) [(\weight\, ToyTy_raw \nat\)] , mk (n \Person\ (Some \Planet\)) [(\salary\, ToyTy_raw \int\)] ])" -text \Since we are in a Isabelle session, at this time, it becomes possible to inspect with -the command @{command value} the result of the translations applied with @{term Design}. -A suitable environment should nevertheless be provided, +text \Since we are in a Isabelle session, at this time, it becomes possible to inspect with +the command @{command value} the result of the translations applied with @{term Design}. +A suitable environment should nevertheless be provided, one can typically experiment this by copying-pasting the following environment initialized in the above \main\:\ definition "main = (let n = \n1. ToyTyObj (ToyTyCore_pre n1) [] ; ToyMult = \m r. toy_multiplicity.make [m] r [Set] in write_file (compiler_env_config.extend (compiler_env_config_empty True None (oidInit (Oid 0)) Gen_only_design (None, False) \ D_output_disable_thy := False , D_output_header_thy := Some (\Design_generated\ ,[\../Toy_Library\] ,\../embedding/Generator_dynamic_sequential\) \) ( L.map (META_class_raw Floor1) Design @@@@ [ META_association (toy_association.make ToyAssTy_association (ToyAssRel [ (n \Person\, ToyMult (Mult_star, None) None) , (n \Person\, ToyMult (Mult_nat 0, Some (Mult_nat 1)) (Some \boss\))])) , META_flush_all ToyFlushAll] , None)))" subsection\Statically Executing the Exportation\ text\ @{verbatim "apply_code_printing ()"} \\ @{verbatim "export_code main"} \\ @{verbatim " (* in Haskell *)"} \\ @{verbatim " (* in OCaml module_name M *)"} \\ @{verbatim " (* in Scala module_name M *)"} \\ @{verbatim " (* in SML module_name M *)"} \ text\After the exportation and executing the exported, we obtain an Isabelle \verb|.thy| file containing the generated code associated to the above input.\ end diff --git a/thys/Isabelle_Meta_Model/toy_example/generator/Design_deep.thy b/thys/Isabelle_Meta_Model/toy_example/generator/Design_deep.thy --- a/thys/Isabelle_Meta_Model/toy_example/generator/Design_deep.thy +++ b/thys/Isabelle_Meta_Model/toy_example/generator/Design_deep.thy @@ -1,375 +1,375 @@ (****************************************************************************** * HOL-TOY * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Example: A Class Model Converted into a Theory File\ subsection\Introduction\ theory Design_deep imports "../embedding/Generator_dynamic_sequential" + "../../Antiquote_Setup" begin -ML_file \~~/src/Doc/antiquote_setup.ML\ text\ In this example, we configure our package to generate a \verb|.thy| file, without executing the associated generated code contained in this \verb|.thy| file (c.f. @{file \Design_shallow.thy\} for a direct evaluation). This mode is particularly relevant for debugging purposes: -while by default no evaluation occurs, +while by default no evaluation occurs, the generated files (and their proofs!) can be executed on a step by step basis, depending on how we interact with the output window (by selectively clicking on what is generated). After clicking on the generated content, the newly inserted content could depend on some theories which are not loaded by this current one. -In this case, it is necessary to manually add all the needed dependencies above after the +In this case, it is necessary to manually add all the needed dependencies above after the keyword @{keyword "imports"}. One should compare this current theory with @{file \Design_shallow.thy\} to see the differences of imported theories, and which ones to manually import (whenever an error happens). \ generation_syntax [ (*deep (generation_semantics [ design (*, oid_start 10*) ]) (THEORY Design_generated) (IMPORTS ["../Toy_Library", "../Toy_Library_Static"] "../embedding/Generator_dynamic_sequential") SECTION (*SORRY*) (*no_dirty*) [ (* in Haskell *) (* in OCaml module_name M *) (* in Scala module_name M *) in SML module_name M ] (output_directory "../document_generated") (*, syntax_print*)*) ] text\ \begin{verbatim} generation_syntax [ deep (generation_semantics [ design ]) (THEORY Design_generated) (IMPORTS ["../Toy_Library", "../Toy_Library_Static"] "../embedding/Generator_dynamic_sequential") SECTION (*SORRY*) (*no_dirty*) [ (* in Haskell *) (* in OCaml module_name M *) (* in Scala module_name M *) in SML module_name M ] (output_directory "../document_generated") (*, syntax_print*) ] \end{verbatim} While in theory it is possible to set the @{keyword "deep"} mode -for generating in all target languages, i.e. by writing +for generating in all target languages, i.e. by writing \[ in Haskell, in OCaml module_name M, in Scala module_name M, in SML module_name M ]\, usually using only one target is enough, since the task of all target is to generate the same Isabelle content. However in case one language takes too much time to setup, we recommend to try the generation with another target language, because all optimizations are currently not (yet) seemingly implemented for all target languages, or differently activated.\ subsection\Designing Class Models (I): Basics\ text\ -The following example shows the definitions of a set of classes, +The following example shows the definitions of a set of classes, called the ``universe'' of classes. Instead of providing a single command for building all the complete universe of classes -directly in one block, +directly in one block, we are constructing classes one by one. So globally the universe describing all classes is partial, it will only be fully constructed when all classes will be finished to be defined. This allows to define classes without having to follow a particular order of definitions. Here \Atom\ is defined before the one of \Molecule\ (\Molecule\ will come after): \ Class Atom < Molecule Attributes size : Integer End text\The ``blue'' color of @{command End} indicates that -@{command End} is not a ``green'' keyword. +@{command End} is not a ``green'' keyword. @{command End} and @{command Class} are in fact similar, they belong to the group of meta-commands (all meta-commands are defined in @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}). -At run-time and in @{keyword "deep"} mode, the semantics of all meta-commands are +At run-time and in @{keyword "deep"} mode, the semantics of all meta-commands are approximately similar: all meta-commands displays some quantity of Isabelle code in the output window (as long as meta-commands are syntactically correctly formed). However each meta-command is unique because what is displayed in the output window depends on the sequence of all meta-commands already encountered before (and also depends on arguments given to the meta-commands).\ text\ -One particularity of @{command End} is to behave as the identity function when +One particularity of @{command End} is to behave as the identity function when @{command End} is called without arguments. As example, here we are calling lots of @{command End} without arguments, and no Isabelle code is generated.\ - End End End + End End End text\ We remark that, like any meta-commands, @{command End} could have been written anywhere in this theory, for example before @{command Class} or even before @{command generation_syntax}... Something does not have to be specially opened before using an @{command End}. \ Class Molecule < Person text\As example, here no @{command End} is written.\ text\ -The semantics of @{command End} is further precised here. +The semantics of @{command End} is further precised here. We earlier mentioned that the universe of classes is partially constructed, but one can still examine what is partially constructed, and one possibility is to use @{command End} for doing so. -@{command End} can be seen as a lazy meta-command: +@{command End} can be seen as a lazy meta-command: \begin{itemize} \item without parameters, no code is generated, \item with some parameters (e.g., the symbol \verb|!|), it forces the generation of the computation -of the universe, by considering all already encountered classes. +of the universe, by considering all already encountered classes. Then a partial representation of the universe can be interactively inspected. \end{itemize} \ Class Galaxy Attributes wormhole : UnlimitedNatural is_sound : Void End! -text\At this position, in the output window, +text\At this position, in the output window, we can observe for the first time some generated Isabelle code, corresponding to the partial universe of classes being constructed. Note: By default, \Atom\ and \Molecule\ are not (yet) present in the shown universe because \Person\ has not been defined in a separate line (unlike \Galaxy\ above).\ Class Person < Galaxy Attributes salary : Integer boss : Person is_meta_thinking: Boolean text\ There is not only @{command End} which forces the computation of the universe, for example -@{command Instance} declares a set of objects belonging to the classes earlier defined, +@{command Instance} declares a set of objects belonging to the classes earlier defined, but the entire universe is needed as knowledge, so there is no choice than forcing the generation of the universe. \ Instance X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 :: Person = [ salary = 1300 , boss = X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 ] and X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 :: Person = [ salary = 1800 ] text\ Here we will call @{command Instance} again to show that the universe will not be computed again since it was already computed in the previous @{command Instance}. \ Instance X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 :: Person = [ salary = 1 ] text\However at any time, the universe can (or will) automatically be recomputed, whenever we are adding meanwhile another class: @{verbatim "(* Class Big_Bang < Atom (* This will force the creation of a new universe. *) *)"} -As remark, not only the universe is recomputed, but -the recomputation takes also into account all meta-commands already encountered. -So in the new setting, \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1\, \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2\ and \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3\ +As remark, not only the universe is recomputed, but +the recomputation takes also into account all meta-commands already encountered. +So in the new setting, \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1\, \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2\ and \X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3\ will be resurrected... after the \Big_Bang\. \ subsection\Designing Class Models (II): Jumping to Another Semantic Floor\ text\ Until now, meta-commands was used to generate lines of code, and these lines belong to the Isabelle language. One particularity of meta-commands is to generate pieces of code containing not only Isabelle code -but also arbitrary meta-commands. -In @{keyword "deep"} mode, this is particularly not a danger +but also arbitrary meta-commands. +In @{keyword "deep"} mode, this is particularly not a danger for meta-commands to generate themselves (whereas for @{keyword "shallow"} the recursion might not terminate). In this case, such meta-commands must automatically generate the appropriate call to -@{command generation_syntax} beforehand. +@{command generation_syntax} beforehand. However this is not enough, the compiling environment (comprising the history of meta-commands) are changing throughout the interactive evaluations, so the environment must also be taken into account and propagated when meta-commands are generating themselves. For example, the environment is needed for consultation whenever resurrecting objects, recomputing the universe or accessing the hierarchy of classes being defined. As a consequence, in the next example a line @{command setup} is added after @{command generation_syntax} for bootstrapping the state of the compiling environment. \ State \\<^sub>1 = [ ([ salary = 1000 , boss = self 1 ] :: Person) , ([ salary = 1200 ] :: Person) (* *) , ([ salary = 2600 , boss = self 3 ] :: Person) , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 , ([ salary = 2300 , boss = self 2 ] :: Person) (* *) (* *) , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 ] State \\<^sub>1' = [ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 ] text \ In certain circumstances, the command @{command setup} must be added again between some particular interleaving of two meta-commands and this may not depend on the presence of @{command generation_syntax} (which is defined only once when generating the first meta-command). For more details, one can refer to the source code of @{term "ignore_meta_header"} and @{term "bootstrap_floor"}.\ PrePost \\<^sub>1 \\<^sub>1' text\ The generation of meta-commands allows to perform various extensions on the Toy language being embedded, without altering the semantics of a particular command. @{command PrePost} usually only takes ``bound variables'' as parameters (not arbitrary \\\-terms), however the semantics of @{command PrePost} was extended to mimic the support of some particular terms not restricted to variables. This extension was implemented by executing some steps of ``\\\-reductions rewriting rules'' operating on the meta-level of commands. -First, it is at least needed to extend the syntax of expressions accepted by @{command PrePost}, +First, it is at least needed to extend the syntax of expressions accepted by @{command PrePost}, we then modify the parsing so that a larger subset of \\\-terms can be given as parameters. Starting from this expression: \\ @{verbatim "(* PrePost \\<^sub>1 [ ([ salary = 1000 , boss = self 1 ] :: Person) ] *)"} -the rewriting begins with a first call to the next semantic floor, we obtain -the following meta-commands (where @{command PrePost} \[shallow]\ is an expression +the rewriting begins with a first call to the next semantic floor, we obtain +the following meta-commands (where @{command PrePost} \[shallow]\ is an expression in normal form): \\ @{verbatim \(* State WFF_10_post = [ ([ "salary" = 1000, "boss" = self 1 ] :: Person) ]\} \\ @{verbatim " PrePost[shallow] \\<^sub>1 WFF_10_post *)"} (\WFF_10_post\ is an automatically generated name). The rewriting of the above @{command State} is performed in its turn. -Finally the overall ultimately terminates when reaching @{command Instance} being already +Finally the overall ultimately terminates when reaching @{command Instance} being already in normal form: \\ @{verbatim \(* Instance WFF_10_post_object0 :: Person = [ "salary" = 1000, "boss" = [ ] ]\} \\ @{verbatim " State[shallow] WFF_10_post = [ WFF_10_post_object0 ]"} \\ @{verbatim " PrePost[shallow] \\<^sub>1 WFF_10_post *)"} \ subsection\Designing Class Models (III): Interaction with (Pure) Term\ text\ Meta-commands are obviously not restricted to manipulate expressions in the Outer Syntax level. It is possible to build meta-commands so that Inner Syntax expressions are directly parsed. However the dependencies of this theory have been minimized so that experimentations -and debugging can easily occur in @{keyword "deep"} mode -(this file only depends on @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}). +and debugging can easily occur in @{keyword "deep"} mode +(this file only depends on @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}). Since the Inner Syntax expressions would perhaps manipulate expressions coming from other theories -than @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}, -it can be desirable to consider the Inner Syntax container as a string and leave the parsing +than @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}, +it can be desirable to consider the Inner Syntax container as a string and leave the parsing for subsequent semantic floors. This is what is implemented here: \ text\ \verb|Context Person :: content ()| \\ \verb| Post "><"| \ text\ Here the expression @{verbatim "><"} is not well-typed in Isabelle, but an error is not raised because the above expression is not (yet) parsed as an Inner Syntax element\footnote{ -In any case an error will not be raised, because the above code +In any case an error will not be raised, because the above code is written in verbatim in the real @{verbatim ".thy"} file, however one can copy-paste this code out of the verbatim scope to see that no errors are really raised. For presentation purposes, it was embedded in verbatim because we will later discuss about meta-commands generating Isabelle code, and then what is generated by this meta-command is of course not well-typed!}. However, this is not the same for the resulting generated meta-command: \\ \verb|Context [shallow] Person :: content ()| \\ \verb| Post : "(\ result self. (><))"| \\ and an error is immediately raised because the parsing of Inner Syntax expressions is activated in this case. \ text\For example, one can put the mouse, with the CTRL gesture, over the variable @{term "a"}, @{term "b"} or @{term "c"} to be convinced that they are free variables compared with above:\ -Context[shallow] Person :: content () +Context[shallow] Person :: content () Post : "a + b = c" subsection\Designing Class Models (IV): Saving the Generated to File\ text\ -The experimentations usually finish by saving all the universe +The experimentations usually finish by saving all the universe and generated Isabelle theory to the hard disk: \\ @{verbatim "(* generation_syntax deep flush_all *)"} \ subsection\Designing Class Models (V): Inspection of Generated Files\ text\ -According to options given to the (first) command @{command generation_syntax} above, +According to options given to the (first) command @{command generation_syntax} above, we retrieve the first generated file in the mentioned directory: @{file \../document_generated/Design_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 \../document_generated/Design_generated_generated.thy\}. -As remark, in this last file, the dependency to @{theory Isabelle_Meta_Model.Generator_dynamic_sequential} was +As remark, in this last file, the dependency to @{theory Isabelle_Meta_Model.Generator_dynamic_sequential} was automatically removed because the meta-compiler has detected the absence of meta-commands in the generated content. -Note: While the first generated file is intended to be always well-typed, -it can happen that subsequent generations will lead to a not well-typed file. +Note: While the first generated file is intended to be always well-typed, +it can happen that subsequent generations will lead to a not well-typed file. This is because the meta-compiler only saves the history of meta-commands. -In case some ``native'' Isabelle declarations +In case some ``native'' Isabelle declarations are generated among meta-commands, then these Isabelle declarations are not saved by the meta-compiler, so these declarations will not be again generated. -Anyway, we see potential solutions for solving this and +Anyway, we see potential solutions for solving this and they would perhaps be implemented in a future version of the meta-compiler... \ end diff --git a/thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy b/thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy --- a/thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy +++ b/thys/Isabelle_Meta_Model/toy_example/generator/Design_shallow.thy @@ -1,136 +1,136 @@ (****************************************************************************** * HOL-TOY * * Copyright (c) 2011-2018 Université Paris-Saclay, Univ. Paris-Sud, France * 2013-2017 IRT SystemX, France * 2011-2015 Achim D. Brucker, Germany * 2016-2018 The University of Sheffield, UK * 2016-2017 Nanyang Technological University, Singapore * 2017-2018 Virginia Tech, USA * * All rights reserved. * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are * met: * * * Redistributions of source code must retain the above copyright * notice, this list of conditions and the following disclaimer. * * * Redistributions in binary form must reproduce the above * copyright notice, this list of conditions and the following * disclaimer in the documentation and/or other materials provided * with the distribution. * * * Neither the name of the copyright holders nor the names of its * contributors may be used to endorse or promote products derived * from this software without specific prior written permission. * * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) section\Example: A Class Model Interactively Executed\ subsection\Introduction\ theory Design_shallow imports "../Toy_Library" "../Toy_Library_Static" "../embedding/Generator_dynamic_sequential" + "../../Antiquote_Setup" begin -ML_file \~~/src/Doc/antiquote_setup.ML\ text\ In this example, we configure our package to execute tactic SML code (corresponding to some generated \verb|.thy| file, @{file \Design_deep.thy\} details how to obtain such generated \verb|.thy| file). Since SML code are already compiled (or reflected) and bound with the native Isabelle API in @{theory Isabelle_Meta_Model.Generator_dynamic_sequential}, nothing is generated in this theory. -The system only parses arguments given to meta-commands and immediately calls the corresponding +The system only parses arguments given to meta-commands and immediately calls the corresponding compiled functions. The execution time is comparatively similar as if tactics were written by hand, except that the generated SML code potentially inherits all optimizations performed by the raw code generation of Isabelle (if any). \ generation_syntax [ shallow (generation_semantics [ design ]) (*SORRY*) (*no_dirty*) (*, syntax_print*) ] text\ The configuration in @{keyword "shallow"} mode is straightforward: in this mode @{command generation_syntax} basically terminates in $O(1)$. \ subsection\Designing Class Models (I): Basics\ Class Atom < Molecule Attributes size : Integer End - End End End + End End End Class Molecule < Person Class Galaxy Attributes wormhole : UnlimitedNatural is_sound : Void End! Class Person < Galaxy Attributes salary : Integer boss : Person is_meta_thinking: Boolean Instance X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 :: Person = [ salary = 1300 , boss = X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 ] and X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 :: Person = [ salary = 1800 ] Instance X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 :: Person = [ salary = 1 ] (* Class Big_Bang < Atom (* This will force the creation of a new universe. *) *) subsection\Designing Class Models (II): Jumping to Another Semantic Floor\ State \\<^sub>1 = [ ([ salary = 1000 , boss = self 1 ] :: Person) , ([ salary = 1200 ] :: Person) (* *) , ([ salary = 2600 , boss = self 3 ] :: Person) , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 , ([ salary = 2300 , boss = self 2 ] :: Person) (* *) (* *) , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 ] State \\<^sub>1' = [ X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n1 , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n2 , X\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n3 ] PrePost \\<^sub>1 \\<^sub>1' (* PrePost \\<^sub>1 [ ([ salary = 1000 , boss = self 1 ] :: Person) ] *) subsection\Designing Class Models (III): Interaction with (Pure) Term\ text\ Here in @{keyword "shallow"} mode, the following expression is directly rejected: \\ \verb|Context Person :: content ()| \\ \verb| Post "><"| \ -Context[shallow] Person :: content () +Context[shallow] Person :: content () Post : "a + b = c" end