# HG changeset patch # User haftmann # Date 1371309563 -7200 # Node ID 08dbf9ff21402d97951c686c7c80b9033ad9d8f2 # Parent afa72aaed518f6872ff6824fa7d115bbfb64aa01 documentation on code_printing and code_identifier diff -r afa72aaed518 -r 08dbf9ff2140 src/Doc/Codegen/Adaptation.thy --- 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 \ nat \ nat \ bool" where "in_interval (k, l) n \ k \ n \ n \ l" (*<*) -code_type %invisible bool - (SML) -code_const %invisible True and False and "op \" and Not - (SML and and and) +code_printing %invisible + type_constructor bool \ (SML) +| constant True \ (SML) +| constant False \ (SML) +| constant HOL.conj \ (SML) +| constant Not \ (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 \" - (SML "true" and "false" and "_ andalso _") +code_printing %quotett + type_constructor bool \ (SML) "bool" +| constant True \ (SML) "true" +| constant False \ (SML) "false" +| constant HOL.conj \ (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 \" - (SML infixl 1 "andalso") +code_printing %quotett + constant HOL.conj \ (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 \ (SML) +| constant Pair \ (SML) (*>*) -code_type %quotett prod - (SML infix 2 "*") -code_const %quotett Pair - (SML "!((_),/ (_))") +code_printing %quotett + type_constructor prod \ (SML) infix 2 "*" +| constant Pair \ (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 \ (Haskell) "Eq" +| constant HOL.equal \ (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 \ (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" \ (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" \ (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. *} diff -r afa72aaed518 -r 08dbf9ff2140 src/Doc/Codegen/Further.thy --- 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 \ (SML) ABC +| code_module B \ (SML) ABC +| code_module C \ (SML) ABC text {* \noindent we explicitly map all those modules on \emph{ABC}, diff -r afa72aaed518 -r 08dbf9ff2140 src/Doc/IsarRef/HOL_Specific.thy --- 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 \"} \\ @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \"} \\ @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ + @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_printing"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_const"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_type"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_class"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_instance"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_reserved"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_identifier"} & : & @{text "theory \ theory"} \\ + @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_monad"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_include"} & : & @{text "theory \ theory"} \\ - @{command_def (HOL) "code_modulename"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_reflect"} & : & @{text "theory \ theory"} \\ @{command_def (HOL) "code_pred"} & : & @{text "theory \ 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 ( '<' | '\' ) 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 ( '\' | '=>' ) \\ + ( '(' target ')' syntax ? + @'and' ) + ; + + printing_typeconstructor: symbol_typeconstructor ( '\' | '=>' ) \\ + ( '(' target ')' syntax ? + @'and' ) + ; + + printing_class: symbol_class ( '\' | '=>' ) \\ + ( '(' target ')' @{syntax string} ? + @'and' ) + ; + + printing_class_relation: symbol_class_relation ( '\' | '=>' ) \\ + ( '(' target ')' @{syntax string} ? + @'and' ) + ; + + printing_class_instance: symbol_class_instance ( '\' | '=>' ) \\ + ( '(' target ')' '-' ? + @'and' ) + ; + + printing_module: symbol_module ( '\' | '=>' ) \\ + ( '(' 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 ) ( '\' | '=>' ) \\ + ( '(' 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