--- a/src/Doc/Codegen/Adaptation.thy Sat Jun 15 17:19:23 2013 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Sat Jun 15 17:19:23 2013 +0200
@@ -177,10 +177,12 @@
primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
"in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
(*<*)
-code_type %invisible bool
- (SML)
-code_const %invisible True and False and "op \<and>" and Not
- (SML and and and)
+code_printing %invisible
+ type_constructor bool \<rightharpoonup> (SML)
+| constant True \<rightharpoonup> (SML)
+| constant False \<rightharpoonup> (SML)
+| constant HOL.conj \<rightharpoonup> (SML)
+| constant Not \<rightharpoonup> (SML)
(*>*)
text %quotetypewriter {*
@{code_stmts in_interval (SML)}
@@ -197,20 +199,21 @@
"bool"}, we may use \qn{custom serialisations}:
*}
-code_type %quotett bool
- (SML "bool")
-code_const %quotett True and False and "op \<and>"
- (SML "true" and "false" and "_ andalso _")
+code_printing %quotett
+ type_constructor bool \<rightharpoonup> (SML) "bool"
+| constant True \<rightharpoonup> (SML) "true"
+| constant False \<rightharpoonup> (SML) "false"
+| constant HOL.conj \<rightharpoonup> (SML) "_ andalso _"
text {*
- \noindent The @{command_def code_type} command takes a type constructor
- as arguments together with a list of custom serialisations. Each
+ \noindent The @{command_def code_printing} command takes a series
+ of symbols (contants, type constructor, \ldots)
+ together with target-specific custom serialisations. Each
custom serialisation starts with a target language identifier
followed by an expression, which during code serialisation is
- inserted whenever the type constructor would occur. For constants,
- @{command_def code_const} implements the corresponding mechanism. Each
+ inserted whenever the type constructor would occur. Each
``@{verbatim "_"}'' in a serialisation expression is treated as a
- placeholder for the type constructor's (the constant's) arguments.
+ placeholder for the constant's or the type constructor's arguments.
*}
text %quotetypewriter {*
@@ -225,8 +228,8 @@
precedences which may be used here:
*}
-code_const %quotett "op \<and>"
- (SML infixl 1 "andalso")
+code_printing %quotett
+ constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
text %quotetypewriter {*
@{code_stmts in_interval (SML)}
@@ -249,15 +252,13 @@
infix ``@{verbatim "*"}'' type constructor and parentheses:
*}
(*<*)
-code_type %invisible prod
- (SML)
-code_const %invisible Pair
- (SML)
+code_printing %invisible
+ type_constructor prod \<rightharpoonup> (SML)
+| constant Pair \<rightharpoonup> (SML)
(*>*)
-code_type %quotett prod
- (SML infix 2 "*")
-code_const %quotett Pair
- (SML "!((_),/ (_))")
+code_printing %quotett
+ type_constructor prod \<rightharpoonup> (SML) infix 2 "*"
+| constant Pair \<rightharpoonup> (SML) "!((_),/ (_))"
text {*
\noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
@@ -286,15 +287,13 @@
text {*
For convenience, the default @{text HOL} setup for @{text Haskell}
maps the @{class equal} class to its counterpart in @{text Haskell},
- giving custom serialisations for the class @{class equal} (by command
- @{command_def code_class}) and its operation @{const [source] HOL.equal}
+ giving custom serialisations for the class @{class equal}
+ and its operation @{const [source] HOL.equal}.
*}
-code_class %quotett equal
- (Haskell "Eq")
-
-code_const %quotett "HOL.equal"
- (Haskell infixl 4 "==")
+code_printing %quotett
+ type_class equal \<rightharpoonup> (Haskell) "Eq"
+| constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "=="
text {*
\noindent A problem now occurs whenever a type which is an instance
@@ -314,36 +313,36 @@
end %quote (*<*)
-(*>*) code_type %quotett bar
- (Haskell "Integer")
+(*>*) code_printing %quotett
+ type_constructor bar \<rightharpoonup> (Haskell) "Integer"
text {*
\noindent The code generator would produce an additional instance,
which of course is rejected by the @{text Haskell} compiler. To
- suppress this additional instance, use @{command_def "code_instance"}:
+ suppress this additional instance:
*}
-code_instance %quotett bar :: equal
- (Haskell -)
+code_printing %quotett
+ class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -
subsection {* Enhancing the target language context \label{sec:include} *}
text {*
In rare cases it is necessary to \emph{enrich} the context of a
- target language; this is accomplished using the @{command_def
- "code_include"} command:
+ target language; this can also be accomplished using the @{command
+ "code_printing"} command:
*}
-code_include %quotett Haskell "Errno"
-{*errno i = error ("Error number: " ++ show i)*}
+code_printing %quotett
+ code_module "Errno" \<rightharpoonup> (Haskell) {*errno i = error ("Error number: " ++ show i)*}
code_reserved %quotett Haskell Errno
text {*
- \noindent Such named @{text include}s are then prepended to every
+ \noindent Such named modules are then prepended to every
generated code. Inspect such code in order to find out how
- @{command "code_include"} behaves with respect to a particular
+ this behaves with respect to a particular
target language.
*}
--- a/src/Doc/Codegen/Further.thy Sat Jun 15 17:19:23 2013 +0200
+++ b/src/Doc/Codegen/Further.thy Sat Jun 15 17:19:23 2013 +0200
@@ -124,10 +124,10 @@
and \emph{C}. Then, by stating
*}
-code_modulename %quote SML
- A ABC
- B ABC
- C ABC
+code_identifier %quote
+ code_module A \<rightharpoonup> (SML) ABC
+| code_module B \<rightharpoonup> (SML) ABC
+| code_module C \<rightharpoonup> (SML) ABC
text {*
\noindent we explicitly map all those modules on \emph{ABC},
--- a/src/Doc/IsarRef/HOL_Specific.thy Sat Jun 15 17:19:23 2013 +0200
+++ b/src/Doc/IsarRef/HOL_Specific.thy Sat Jun 15 17:19:23 2013 +0200
@@ -2207,14 +2207,16 @@
@{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
+ @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
\end{matharray}
@@ -2237,7 +2239,7 @@
class: @{syntax nameref}
;
- target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
+ target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
;
@@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
@@ -2264,6 +2266,59 @@
@@{command (HOL) code_deps} ( constexpr + ) ?
;
+ @@{command (HOL) code_reserved} target ( @{syntax string} + )
+ ;
+
+ symbol_const: ( @'constant' const )
+ ;
+
+ symbol_typeconstructor: ( @'type_constructor' typeconstructor )
+ ;
+
+ symbol_class: ( @'type_class' class )
+ ;
+
+ symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
+ ;
+
+ symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
+ ;
+
+ symbol_module: ( @'code_module' name )
+ ;
+
+ syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
+ ;
+
+ printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' syntax ? + @'and' )
+ ;
+
+ printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' syntax ? + @'and' )
+ ;
+
+ printing_class: symbol_class ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' @{syntax string} ? + @'and' )
+ ;
+
+ printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' @{syntax string} ? + @'and' )
+ ;
+
+ printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' '-' ? + @'and' )
+ ;
+
+ printing_module: symbol_module ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
+ ;
+
+ @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
+ | printing_class | printing_class_relation | printing_class_instance
+ | printing_module ) + '|' )
+ ;
+
@@{command (HOL) code_const} (const + @'and') \\
( ( '(' target ( syntax ? + @'and' ) ')' ) + )
;
@@ -2280,18 +2335,21 @@
( ( '(' target ( '-' ? + @'and' ) ')' ) + )
;
- @@{command (HOL) code_reserved} target ( @{syntax string} + )
+ @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
+ ;
+
+ @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
+ | symbol_class | symbol_class_relation | symbol_class_instance
+ | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \\
+ ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
+ ;
+
+ @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
;
@@{command (HOL) code_monad} const const target
;
- @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
- ;
-
- @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
- ;
-
@@{command (HOL) code_reflect} @{syntax string} \\
( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
@@ -2300,9 +2358,6 @@
@@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const
;
- syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
- ;
-
modedecl: (modes | ((const ':' modes) \\
(@'and' ((const ':' modes @'and') +))?))
;
@@ -2384,37 +2439,27 @@
theorems representing the corresponding program containing all given
constants after preprocessing.
- \item @{command (HOL) "code_const"} associates a list of constants
- with target-specific serializations; omitting a serialization
- deletes an existing serialization.
-
- \item @{command (HOL) "code_type"} associates a list of type
- constructors with target-specific serializations; omitting a
- serialization deletes an existing serialization.
-
- \item @{command (HOL) "code_class"} associates a list of classes
- with target-specific class names; omitting a serialization deletes
- an existing serialization. This applies only to \emph{Haskell}.
-
- \item @{command (HOL) "code_instance"} declares a list of type
- constructor / class instance relations as ``already present'' for a
- given target. Omitting a ``@{text "-"}'' deletes an existing
- ``already present'' declaration. This applies only to
- \emph{Haskell}.
-
\item @{command (HOL) "code_reserved"} declares a list of names as
reserved for a given target, preventing it to be shadowed by any
generated code.
+ \item @{command (HOL) "code_printing"} associates a series of symbols
+ (constants, type constructors, classes, class relations, instances,
+ module names) with target-specific serializations; omitting a serialization
+ deletes an existing serialization. Legacy variants of this are
+ @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
+ @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
+ @{command (HOL) "code_include"}.
+
\item @{command (HOL) "code_monad"} provides an auxiliary mechanism
to generate monadic code for Haskell.
- \item @{command (HOL) "code_include"} adds arbitrary named content
- (``include'') to generated code. A ``@{text "-"}'' as last argument
- will remove an already added ``include''.
-
- \item @{command (HOL) "code_modulename"} declares aliasings from one
- module name onto another.
+ \item @{command (HOL) "code_identifier"} associates a a series of symbols
+ (constants, type constructors, classes, class relations, instances,
+ module names) with target-specific hints how these symbols shall be named.
+ \emph{Warning:} These hints are still subject to name disambiguation.
+ @{command (HOL) "code_modulename"} is a legacy variant for
+ @{command (HOL) "code_identifier"} on module names.
\item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
argument compiles code into the system runtime environment and