documentation on code_printing and code_identifier
authorhaftmann
Sat Jun 15 17:19:23 2013 +0200 (2013-06-15)
changeset 5237808dbf9ff2140
parent 52377 afa72aaed518
child 52379 7f864f2219a9
documentation on code_printing and code_identifier
src/Doc/Codegen/Adaptation.thy
src/Doc/Codegen/Further.thy
src/Doc/IsarRef/HOL_Specific.thy
     1.1 --- a/src/Doc/Codegen/Adaptation.thy	Sat Jun 15 17:19:23 2013 +0200
     1.2 +++ b/src/Doc/Codegen/Adaptation.thy	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -177,10 +177,12 @@
     1.4  primrec %quote in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.5    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
     1.6  (*<*)
     1.7 -code_type %invisible bool
     1.8 -  (SML)
     1.9 -code_const %invisible True and False and "op \<and>" and Not
    1.10 -  (SML and and and)
    1.11 +code_printing %invisible
    1.12 +  type_constructor bool \<rightharpoonup> (SML)
    1.13 +| constant True \<rightharpoonup> (SML)
    1.14 +| constant False \<rightharpoonup> (SML)
    1.15 +| constant HOL.conj \<rightharpoonup> (SML)
    1.16 +| constant Not \<rightharpoonup> (SML)
    1.17  (*>*)
    1.18  text %quotetypewriter {*
    1.19    @{code_stmts in_interval (SML)}
    1.20 @@ -197,20 +199,21 @@
    1.21    "bool"}, we may use \qn{custom serialisations}:
    1.22  *}
    1.23  
    1.24 -code_type %quotett bool
    1.25 -  (SML "bool")
    1.26 -code_const %quotett True and False and "op \<and>"
    1.27 -  (SML "true" and "false" and "_ andalso _")
    1.28 +code_printing %quotett
    1.29 +  type_constructor bool \<rightharpoonup> (SML) "bool"
    1.30 +| constant True \<rightharpoonup> (SML) "true"
    1.31 +| constant False \<rightharpoonup> (SML) "false"
    1.32 +| constant HOL.conj \<rightharpoonup> (SML) "_ andalso _"
    1.33  
    1.34  text {*
    1.35 -  \noindent The @{command_def code_type} command takes a type constructor
    1.36 -  as arguments together with a list of custom serialisations.  Each
    1.37 +  \noindent The @{command_def code_printing} command takes a series
    1.38 +  of symbols (contants, type constructor, \ldots)
    1.39 +  together with target-specific custom serialisations.  Each
    1.40    custom serialisation starts with a target language identifier
    1.41    followed by an expression, which during code serialisation is
    1.42 -  inserted whenever the type constructor would occur.  For constants,
    1.43 -  @{command_def code_const} implements the corresponding mechanism.  Each
    1.44 +  inserted whenever the type constructor would occur.  Each
    1.45    ``@{verbatim "_"}'' in a serialisation expression is treated as a
    1.46 -  placeholder for the type constructor's (the constant's) arguments.
    1.47 +  placeholder for the constant's or the type constructor's arguments.
    1.48  *}
    1.49  
    1.50  text %quotetypewriter {*
    1.51 @@ -225,8 +228,8 @@
    1.52    precedences which may be used here:
    1.53  *}
    1.54  
    1.55 -code_const %quotett "op \<and>"
    1.56 -  (SML infixl 1 "andalso")
    1.57 +code_printing %quotett
    1.58 +  constant HOL.conj \<rightharpoonup> (SML) infixl 1 "andalso"
    1.59  
    1.60  text %quotetypewriter {*
    1.61    @{code_stmts in_interval (SML)}
    1.62 @@ -249,15 +252,13 @@
    1.63    infix ``@{verbatim "*"}'' type constructor and parentheses:
    1.64  *}
    1.65  (*<*)
    1.66 -code_type %invisible prod
    1.67 -  (SML)
    1.68 -code_const %invisible Pair
    1.69 -  (SML)
    1.70 +code_printing %invisible
    1.71 +  type_constructor prod \<rightharpoonup> (SML)
    1.72 +| constant Pair \<rightharpoonup> (SML)
    1.73  (*>*)
    1.74 -code_type %quotett prod
    1.75 -  (SML infix 2 "*")
    1.76 -code_const %quotett Pair
    1.77 -  (SML "!((_),/ (_))")
    1.78 +code_printing %quotett
    1.79 +  type_constructor prod \<rightharpoonup> (SML) infix 2 "*"
    1.80 +| constant Pair \<rightharpoonup> (SML) "!((_),/ (_))"
    1.81  
    1.82  text {*
    1.83    \noindent The initial bang ``@{verbatim "!"}'' tells the serialiser
    1.84 @@ -286,15 +287,13 @@
    1.85  text {*
    1.86    For convenience, the default @{text HOL} setup for @{text Haskell}
    1.87    maps the @{class equal} class to its counterpart in @{text Haskell},
    1.88 -  giving custom serialisations for the class @{class equal} (by command
    1.89 -  @{command_def code_class}) and its operation @{const [source] HOL.equal}
    1.90 +  giving custom serialisations for the class @{class equal}
    1.91 +  and its operation @{const [source] HOL.equal}.
    1.92  *}
    1.93  
    1.94 -code_class %quotett equal
    1.95 -  (Haskell "Eq")
    1.96 -
    1.97 -code_const %quotett "HOL.equal"
    1.98 -  (Haskell infixl 4 "==")
    1.99 +code_printing %quotett
   1.100 +  type_class equal \<rightharpoonup> (Haskell) "Eq"
   1.101 +| constant HOL.equal \<rightharpoonup> (Haskell) infixl 4 "=="
   1.102  
   1.103  text {*
   1.104    \noindent A problem now occurs whenever a type which is an instance
   1.105 @@ -314,36 +313,36 @@
   1.106  
   1.107  end %quote (*<*)
   1.108  
   1.109 -(*>*) code_type %quotett bar
   1.110 -  (Haskell "Integer")
   1.111 +(*>*) code_printing %quotett
   1.112 +  type_constructor bar \<rightharpoonup> (Haskell) "Integer"
   1.113  
   1.114  text {*
   1.115    \noindent The code generator would produce an additional instance,
   1.116    which of course is rejected by the @{text Haskell} compiler.  To
   1.117 -  suppress this additional instance, use @{command_def "code_instance"}:
   1.118 +  suppress this additional instance:
   1.119  *}
   1.120  
   1.121 -code_instance %quotett bar :: equal
   1.122 -  (Haskell -)
   1.123 +code_printing %quotett
   1.124 +  class_instance bar :: "HOL.equal" \<rightharpoonup> (Haskell) -
   1.125  
   1.126  
   1.127  subsection {* Enhancing the target language context \label{sec:include} *}
   1.128  
   1.129  text {*
   1.130    In rare cases it is necessary to \emph{enrich} the context of a
   1.131 -  target language; this is accomplished using the @{command_def
   1.132 -  "code_include"} command:
   1.133 +  target language; this can also be accomplished using the @{command
   1.134 +  "code_printing"} command:
   1.135  *}
   1.136  
   1.137 -code_include %quotett Haskell "Errno"
   1.138 -{*errno i = error ("Error number: " ++ show i)*}
   1.139 +code_printing %quotett
   1.140 +  code_module "Errno" \<rightharpoonup> (Haskell) {*errno i = error ("Error number: " ++ show i)*}
   1.141  
   1.142  code_reserved %quotett Haskell Errno
   1.143  
   1.144  text {*
   1.145 -  \noindent Such named @{text include}s are then prepended to every
   1.146 +  \noindent Such named modules are then prepended to every
   1.147    generated code.  Inspect such code in order to find out how
   1.148 -  @{command "code_include"} behaves with respect to a particular
   1.149 +  this behaves with respect to a particular
   1.150    target language.
   1.151  *}
   1.152  
     2.1 --- a/src/Doc/Codegen/Further.thy	Sat Jun 15 17:19:23 2013 +0200
     2.2 +++ b/src/Doc/Codegen/Further.thy	Sat Jun 15 17:19:23 2013 +0200
     2.3 @@ -124,10 +124,10 @@
     2.4    and \emph{C}.  Then, by stating
     2.5  *}
     2.6  
     2.7 -code_modulename %quote SML
     2.8 -  A ABC
     2.9 -  B ABC
    2.10 -  C ABC
    2.11 +code_identifier %quote
    2.12 +  code_module A \<rightharpoonup> (SML) ABC
    2.13 +| code_module B \<rightharpoonup> (SML) ABC
    2.14 +| code_module C \<rightharpoonup> (SML) ABC
    2.15  
    2.16  text {*
    2.17    \noindent we explicitly map all those modules on \emph{ABC},
     3.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Sat Jun 15 17:19:23 2013 +0200
     3.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Sat Jun 15 17:19:23 2013 +0200
     3.3 @@ -2207,14 +2207,16 @@
     3.4      @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.5      @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.6      @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     3.7 +    @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
     3.8 +    @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
     3.9      @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
    3.10      @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
    3.11      @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
    3.12      @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
    3.13 -    @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
    3.14 +    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
    3.15 +    @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
    3.16 +    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
    3.17      @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
    3.18 -    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
    3.19 -    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
    3.20      @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
    3.21      @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
    3.22    \end{matharray}
    3.23 @@ -2237,7 +2239,7 @@
    3.24      class: @{syntax nameref}
    3.25      ;
    3.26  
    3.27 -    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
    3.28 +    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
    3.29      ;
    3.30  
    3.31      @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
    3.32 @@ -2264,6 +2266,59 @@
    3.33      @@{command (HOL) code_deps} ( constexpr + ) ?
    3.34      ;
    3.35  
    3.36 +    @@{command (HOL) code_reserved} target ( @{syntax string} + )
    3.37 +    ;
    3.38 +
    3.39 +    symbol_const: ( @'constant' const )
    3.40 +    ;
    3.41 +
    3.42 +    symbol_typeconstructor: ( @'type_constructor' typeconstructor )
    3.43 +    ;
    3.44 +
    3.45 +    symbol_class: ( @'type_class' class )
    3.46 +    ;
    3.47 +
    3.48 +    symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
    3.49 +    ;
    3.50 +
    3.51 +    symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
    3.52 +    ;
    3.53 +
    3.54 +    symbol_module: ( @'code_module' name )
    3.55 +    ;
    3.56 +
    3.57 +    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
    3.58 +    ;
    3.59 +
    3.60 +    printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \\
    3.61 +      ( '(' target ')' syntax ? + @'and' )
    3.62 +    ;
    3.63 +
    3.64 +    printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \\
    3.65 +      ( '(' target ')' syntax ? + @'and' )
    3.66 +    ;
    3.67 +
    3.68 +    printing_class: symbol_class ( '\<rightharpoonup>' | '=>' )  \\
    3.69 +      ( '(' target ')' @{syntax string} ? + @'and' )
    3.70 +    ;
    3.71 +
    3.72 +    printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' )  \\
    3.73 +      ( '(' target ')' @{syntax string} ? + @'and' )
    3.74 +    ;
    3.75 +
    3.76 +    printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' )  \\
    3.77 +      ( '(' target ')' '-' ? + @'and' )
    3.78 +    ;
    3.79 +
    3.80 +    printing_module: symbol_module ( '\<rightharpoonup>' | '=>' )  \\
    3.81 +      ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
    3.82 +    ;
    3.83 +
    3.84 +    @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
    3.85 +      | printing_class | printing_class_relation | printing_class_instance
    3.86 +      | printing_module ) + '|' )
    3.87 +    ;
    3.88 +
    3.89      @@{command (HOL) code_const} (const + @'and') \\
    3.90        ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
    3.91      ;
    3.92 @@ -2280,18 +2335,21 @@
    3.93        ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
    3.94      ;
    3.95  
    3.96 -    @@{command (HOL) code_reserved} target ( @{syntax string} + )
    3.97 +    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
    3.98 +    ;
    3.99 +
   3.100 +    @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
   3.101 +      | symbol_class | symbol_class_relation | symbol_class_instance
   3.102 +      | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \\
   3.103 +      ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
   3.104 +    ;
   3.105 +
   3.106 +    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
   3.107      ;
   3.108  
   3.109      @@{command (HOL) code_monad} const const target
   3.110      ;
   3.111  
   3.112 -    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
   3.113 -    ;
   3.114 -
   3.115 -    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
   3.116 -    ;
   3.117 -
   3.118      @@{command (HOL) code_reflect} @{syntax string} \\
   3.119        ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
   3.120        ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
   3.121 @@ -2300,9 +2358,6 @@
   3.122      @@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const
   3.123      ;
   3.124  
   3.125 -    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
   3.126 -    ;
   3.127 -
   3.128      modedecl: (modes | ((const ':' modes) \\
   3.129           (@'and' ((const ':' modes @'and') +))?))
   3.130      ;
   3.131 @@ -2384,37 +2439,27 @@
   3.132    theorems representing the corresponding program containing all given
   3.133    constants after preprocessing.
   3.134  
   3.135 -  \item @{command (HOL) "code_const"} associates a list of constants
   3.136 -  with target-specific serializations; omitting a serialization
   3.137 -  deletes an existing serialization.
   3.138 -
   3.139 -  \item @{command (HOL) "code_type"} associates a list of type
   3.140 -  constructors with target-specific serializations; omitting a
   3.141 -  serialization deletes an existing serialization.
   3.142 -
   3.143 -  \item @{command (HOL) "code_class"} associates a list of classes
   3.144 -  with target-specific class names; omitting a serialization deletes
   3.145 -  an existing serialization.  This applies only to \emph{Haskell}.
   3.146 -
   3.147 -  \item @{command (HOL) "code_instance"} declares a list of type
   3.148 -  constructor / class instance relations as ``already present'' for a
   3.149 -  given target.  Omitting a ``@{text "-"}'' deletes an existing
   3.150 -  ``already present'' declaration.  This applies only to
   3.151 -  \emph{Haskell}.
   3.152 -
   3.153    \item @{command (HOL) "code_reserved"} declares a list of names as
   3.154    reserved for a given target, preventing it to be shadowed by any
   3.155    generated code.
   3.156  
   3.157 +  \item @{command (HOL) "code_printing"} associates a series of symbols
   3.158 +  (constants, type constructors, classes, class relations, instances,
   3.159 +  module names) with target-specific serializations; omitting a serialization
   3.160 +  deletes an existing serialization.  Legacy variants of this are
   3.161 +  @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
   3.162 +  @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
   3.163 +  @{command (HOL) "code_include"}.
   3.164 +
   3.165    \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
   3.166    to generate monadic code for Haskell.
   3.167  
   3.168 -  \item @{command (HOL) "code_include"} adds arbitrary named content
   3.169 -  (``include'') to generated code.  A ``@{text "-"}'' as last argument
   3.170 -  will remove an already added ``include''.
   3.171 -
   3.172 -  \item @{command (HOL) "code_modulename"} declares aliasings from one
   3.173 -  module name onto another.
   3.174 +  \item @{command (HOL) "code_identifier"} associates a a series of symbols
   3.175 +  (constants, type constructors, classes, class relations, instances,
   3.176 +  module names) with target-specific hints how these symbols shall be named.
   3.177 +  \emph{Warning:} These hints are still subject to name disambiguation.
   3.178 +  @{command (HOL) "code_modulename"} is a legacy variant for
   3.179 +  @{command (HOL) "code_identifier"} on module names.
   3.180  
   3.181    \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
   3.182    argument compiles code into the system runtime environment and