Theory Rail
theory Rail
imports "../toy_example/embedding/Generator_dynamic_sequential" "../Antiquote_Setup"
begin
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,
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:
\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.
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
(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.
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.,
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
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›
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}
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