Theory Design_deep
section‹Example: A Class Model Converted into a Theory File›
subsection‹Introduction›
theory
Design_deep
imports
"../embedding/Generator_dynamic_sequential"
"../../Antiquote_Setup"
begin
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,
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
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 [ ]
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
‹[ 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,
called the ``universe'' of classes.
Instead of providing a single command for building all the complete universe of classes
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} 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
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
@{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
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.
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:
\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.
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,
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,
but the entire universe is needed as knowledge, so there is no choice than forcing
the generation of the universe.
›
Instance X⇩P⇩e⇩r⇩s⇩o⇩n1 :: Person = [ salary = 1300 , boss = X⇩P⇩e⇩r⇩s⇩o⇩n2 ]
and X⇩P⇩e⇩r⇩s⇩o⇩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⇩P⇩e⇩r⇩s⇩o⇩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⇩P⇩e⇩r⇩s⇩o⇩n1›, ‹X⇩P⇩e⇩r⇩s⇩o⇩n2› and ‹X⇩P⇩e⇩r⇩s⇩o⇩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
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.
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 σ⇩1 =
[ ([ salary = 1000 , boss = self 1 ] :: Person)
, ([ salary = 1200 ] :: Person)
, ([ salary = 2600 , boss = self 3 ] :: Person)
, X⇩P⇩e⇩r⇩s⇩o⇩n1
, ([ salary = 2300 , boss = self 2 ] :: Person)
, X⇩P⇩e⇩r⇩s⇩o⇩n2 ]
State σ⇩1' =
[ X⇩P⇩e⇩r⇩s⇩o⇩n1
, X⇩P⇩e⇩r⇩s⇩o⇩n2
, X⇩P⇩e⇩r⇩s⇩o⇩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 σ⇩1 σ⇩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},
we then modify the parsing so that a larger subset of ‹λ›-terms
can be given as parameters.
Starting from this expression: \\
@{verbatim "(* PrePost σ⇩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
in normal form): \\
@{verbatim ‹(* State WFF_10_post = [ ([ "salary" = 1000, "boss" = self 1 ] :: Person) ]›} \\
@{verbatim " PrePost[shallow] σ⇩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
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] σ⇩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}).
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
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
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 ()
Post : "a + b = c"
subsection‹Designing Class Models (IV): Saving the Generated to File›
text‹
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,
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
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.
This is because the meta-compiler only saves the history of meta-commands.
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
they would perhaps be implemented in a future version of the meta-compiler...
›
end