src/Doc/IsarRef/HOL_Specific.thy
changeset 52378 08dbf9ff2140
parent 50879 fc394c83e490
child 52435 6646bb548c6b
     1.1 --- a/src/Doc/IsarRef/HOL_Specific.thy	Sat Jun 15 17:19:23 2013 +0200
     1.2 +++ b/src/Doc/IsarRef/HOL_Specific.thy	Sat Jun 15 17:19:23 2013 +0200
     1.3 @@ -2207,14 +2207,16 @@
     1.4      @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.5      @{command_def (HOL) "code_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.6      @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.7 +    @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8 +    @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
     1.9      @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
    1.10      @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
    1.11      @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
    1.12      @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
    1.13 -    @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
    1.14 +    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
    1.15 +    @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
    1.16 +    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
    1.17      @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
    1.18 -    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
    1.19 -    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
    1.20      @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
    1.21      @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
    1.22    \end{matharray}
    1.23 @@ -2237,7 +2239,7 @@
    1.24      class: @{syntax nameref}
    1.25      ;
    1.26  
    1.27 -    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala'
    1.28 +    target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
    1.29      ;
    1.30  
    1.31      @@{attribute (HOL) code} ( 'del' | 'abstype' | 'abstract' )?
    1.32 @@ -2264,6 +2266,59 @@
    1.33      @@{command (HOL) code_deps} ( constexpr + ) ?
    1.34      ;
    1.35  
    1.36 +    @@{command (HOL) code_reserved} target ( @{syntax string} + )
    1.37 +    ;
    1.38 +
    1.39 +    symbol_const: ( @'constant' const )
    1.40 +    ;
    1.41 +
    1.42 +    symbol_typeconstructor: ( @'type_constructor' typeconstructor )
    1.43 +    ;
    1.44 +
    1.45 +    symbol_class: ( @'type_class' class )
    1.46 +    ;
    1.47 +
    1.48 +    symbol_class_relation: ( @'class_relation' class ( '<' | '\<subseteq>' ) class )
    1.49 +    ;
    1.50 +
    1.51 +    symbol_class_instance: ( @'class_instance' typeconstructor @'::' class )
    1.52 +    ;
    1.53 +
    1.54 +    symbol_module: ( @'code_module' name )
    1.55 +    ;
    1.56 +
    1.57 +    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
    1.58 +    ;
    1.59 +
    1.60 +    printing_const: symbol_const ( '\<rightharpoonup>' | '=>' ) \\
    1.61 +      ( '(' target ')' syntax ? + @'and' )
    1.62 +    ;
    1.63 +
    1.64 +    printing_typeconstructor: symbol_typeconstructor ( '\<rightharpoonup>' | '=>' ) \\
    1.65 +      ( '(' target ')' syntax ? + @'and' )
    1.66 +    ;
    1.67 +
    1.68 +    printing_class: symbol_class ( '\<rightharpoonup>' | '=>' )  \\
    1.69 +      ( '(' target ')' @{syntax string} ? + @'and' )
    1.70 +    ;
    1.71 +
    1.72 +    printing_class_relation: symbol_class_relation ( '\<rightharpoonup>' | '=>' )  \\
    1.73 +      ( '(' target ')' @{syntax string} ? + @'and' )
    1.74 +    ;
    1.75 +
    1.76 +    printing_class_instance: symbol_class_instance ( '\<rightharpoonup>' | '=>' )  \\
    1.77 +      ( '(' target ')' '-' ? + @'and' )
    1.78 +    ;
    1.79 +
    1.80 +    printing_module: symbol_module ( '\<rightharpoonup>' | '=>' )  \\
    1.81 +      ( '(' target ')' ( @{syntax string} ( @'attach' ( const + ) ) ? ) ? + @'and' )
    1.82 +    ;
    1.83 +
    1.84 +    @@{command (HOL) code_printing} ( ( printing_const | printing_typeconstructor
    1.85 +      | printing_class | printing_class_relation | printing_class_instance
    1.86 +      | printing_module ) + '|' )
    1.87 +    ;
    1.88 +
    1.89      @@{command (HOL) code_const} (const + @'and') \\
    1.90        ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
    1.91      ;
    1.92 @@ -2280,18 +2335,21 @@
    1.93        ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
    1.94      ;
    1.95  
    1.96 -    @@{command (HOL) code_reserved} target ( @{syntax string} + )
    1.97 +    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
    1.98 +    ;
    1.99 +
   1.100 +    @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
   1.101 +      | symbol_class | symbol_class_relation | symbol_class_instance
   1.102 +      | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \\
   1.103 +      ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
   1.104 +    ;
   1.105 +
   1.106 +    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
   1.107      ;
   1.108  
   1.109      @@{command (HOL) code_monad} const const target
   1.110      ;
   1.111  
   1.112 -    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
   1.113 -    ;
   1.114 -
   1.115 -    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
   1.116 -    ;
   1.117 -
   1.118      @@{command (HOL) code_reflect} @{syntax string} \\
   1.119        ( @'datatypes' ( @{syntax string} '=' ( '_' | ( @{syntax string} + '|' ) + @'and' ) ) ) ? \\
   1.120        ( @'functions' ( @{syntax string} + ) ) ? ( @'file' @{syntax string} ) ?
   1.121 @@ -2300,9 +2358,6 @@
   1.122      @@{command (HOL) code_pred} \\( '(' @'modes' ':' modedecl ')')? \\ const
   1.123      ;
   1.124  
   1.125 -    syntax: @{syntax string} | ( @'infix' | @'infixl' | @'infixr' ) @{syntax nat} @{syntax string}
   1.126 -    ;
   1.127 -
   1.128      modedecl: (modes | ((const ':' modes) \\
   1.129           (@'and' ((const ':' modes @'and') +))?))
   1.130      ;
   1.131 @@ -2384,37 +2439,27 @@
   1.132    theorems representing the corresponding program containing all given
   1.133    constants after preprocessing.
   1.134  
   1.135 -  \item @{command (HOL) "code_const"} associates a list of constants
   1.136 -  with target-specific serializations; omitting a serialization
   1.137 -  deletes an existing serialization.
   1.138 -
   1.139 -  \item @{command (HOL) "code_type"} associates a list of type
   1.140 -  constructors with target-specific serializations; omitting a
   1.141 -  serialization deletes an existing serialization.
   1.142 -
   1.143 -  \item @{command (HOL) "code_class"} associates a list of classes
   1.144 -  with target-specific class names; omitting a serialization deletes
   1.145 -  an existing serialization.  This applies only to \emph{Haskell}.
   1.146 -
   1.147 -  \item @{command (HOL) "code_instance"} declares a list of type
   1.148 -  constructor / class instance relations as ``already present'' for a
   1.149 -  given target.  Omitting a ``@{text "-"}'' deletes an existing
   1.150 -  ``already present'' declaration.  This applies only to
   1.151 -  \emph{Haskell}.
   1.152 -
   1.153    \item @{command (HOL) "code_reserved"} declares a list of names as
   1.154    reserved for a given target, preventing it to be shadowed by any
   1.155    generated code.
   1.156  
   1.157 +  \item @{command (HOL) "code_printing"} associates a series of symbols
   1.158 +  (constants, type constructors, classes, class relations, instances,
   1.159 +  module names) with target-specific serializations; omitting a serialization
   1.160 +  deletes an existing serialization.  Legacy variants of this are
   1.161 +  @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
   1.162 +  @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
   1.163 +  @{command (HOL) "code_include"}.
   1.164 +
   1.165    \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
   1.166    to generate monadic code for Haskell.
   1.167  
   1.168 -  \item @{command (HOL) "code_include"} adds arbitrary named content
   1.169 -  (``include'') to generated code.  A ``@{text "-"}'' as last argument
   1.170 -  will remove an already added ``include''.
   1.171 -
   1.172 -  \item @{command (HOL) "code_modulename"} declares aliasings from one
   1.173 -  module name onto another.
   1.174 +  \item @{command (HOL) "code_identifier"} associates a a series of symbols
   1.175 +  (constants, type constructors, classes, class relations, instances,
   1.176 +  module names) with target-specific hints how these symbols shall be named.
   1.177 +  \emph{Warning:} These hints are still subject to name disambiguation.
   1.178 +  @{command (HOL) "code_modulename"} is a legacy variant for
   1.179 +  @{command (HOL) "code_identifier"} on module names.
   1.180  
   1.181    \item @{command (HOL) "code_reflect"} without a ``@{text "file"}''
   1.182    argument compiles code into the system runtime environment and