clarified 'file_prefix';
authorwenzelm
Fri Mar 29 13:42:17 2019 +0100 (5 months ago)
changeset 700119dde788b0128
parent 70010 499896e3a7b0
child 70012 36aeb535a801
clarified 'file_prefix';
NEWS
src/Doc/Codegen/Introduction.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Pure/Thy/export.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
     1.1 --- a/NEWS	Fri Mar 29 12:24:34 2019 +0100
     1.2 +++ b/NEWS	Fri Mar 29 13:42:17 2019 +0100
     1.3 @@ -133,20 +133,20 @@
     1.4  to lift specifications to the global theory level.
     1.5  
     1.6  * Command 'export_code' produces output as logical files within the
     1.7 -theory context, as well as session exports that can be materialized
     1.8 -using the command-line tools "isabelle export" or "isabelle build -e"
     1.9 -(with 'export_files' in the session ROOT), or browsed in Isabelle/jEdit
    1.10 -via the "isabelle-export:" file-system. A 'file_prefix' argument allows
    1.11 -to specify an explicit prefix, the default is "export" with a
    1.12 -consecutive number within each theory. The overall prefix "code" is
    1.13 -always prepended.
    1.14 +theory context, as well as formal session exports that can be
    1.15 +materialized via command-line tools "isabelle export" or "isabelle build
    1.16 +-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
    1.17 +provides a virtual file-system "isabelle-export:" that can be explored
    1.18 +in the regular file-browser. A 'file_prefix' argument allows to specify
    1.19 +an explicit name prefix for the target file (SML, OCaml, Scala) or
    1.20 +directory (Haskell); the default is "export" with a consecutive number
    1.21 +within each theory.
    1.22  
    1.23  * Command 'export_code': the 'file' argument is now legacy and will be
    1.24  removed soon: writing to the physical file-system is not well-defined in
    1.25 -a reactive/parallel application like Isabelle. The empty 'file' has been
    1.26 -discontinued already: it has been superseded by the file-browser in
    1.27 -Isabelle/jEdit with "isabelle-export:" as file-system. Minor
    1.28 -INCOMPATIBILITY.
    1.29 +a reactive/parallel application like Isabelle. The empty 'file' argument
    1.30 +has been discontinued already: it is superseded by the file-browser in
    1.31 +Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
    1.32  
    1.33  * Code generation for OCaml: proper strings are used for literals.
    1.34  Minor INCOMPATIBILITY.
     2.1 --- a/src/Doc/Codegen/Introduction.thy	Fri Mar 29 12:24:34 2019 +0100
     2.2 +++ b/src/Doc/Codegen/Introduction.thy	Fri Mar 29 13:42:17 2019 +0100
     2.3 @@ -68,8 +68,7 @@
     2.4  
     2.5  text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close>
     2.6  
     2.7 -export_code %quote empty dequeue enqueue in SML
     2.8 -  module_name Example file_prefix example
     2.9 +export_code %quote empty dequeue enqueue in SML module_name Example
    2.10  
    2.11  text \<open>\noindent resulting in the following code:\<close>
    2.12  
    2.13 @@ -78,29 +77,29 @@
    2.14  \<close>
    2.15  
    2.16  text \<open>
    2.17 -  \noindent The @{command_def export_code} command takes a space-separated
    2.18 -  list of constants for which code shall be generated; anything else needed
    2.19 -  for those is added implicitly. Then follows a target language identifier
    2.20 -  and a freely chosen \<^theory_text>\<open>module_name\<close>. A \<^theory_text>\<open>file_prefix\<close> introduces
    2.21 -  sub-directory structure for the output of logical files (within the
    2.22 -  theory context), as well as session exports; the default is \<^verbatim>\<open>export\<close>
    2.23 -  with a consecutive number within the current theory. The prefix \<^verbatim>\<open>code\<close>
    2.24 -  is always prepended to the code output directory. For \<open>SML\<close>, \<open>OCaml\<close> and
    2.25 -  \<open>Scala\<close> the result is a single file, for \<open>Haskell\<close> each module gets its
    2.26 -  own file with the module name and extension \<^verbatim>\<open>.hs\<close>. Here is an example:\<^footnote>\<open>
    2.27 -  The exports may be explored within the Isabelle/jEdit Prover IDE using
    2.28 -  the file-browser on the \<^verbatim>\<open>isabelle-export:\<close> virtual file-system.\<close>
    2.29 +  \noindent The @{command_def export_code} command takes multiple constants
    2.30 +  for which code shall be generated; anything else needed for those is
    2.31 +  added implicitly. Then follows a target language identifier and a freely
    2.32 +  chosen \<^theory_text>\<open>module_name\<close>.
    2.33  
    2.34 -  %FIXME old/new "name"
    2.35 -  %name denotes the destination to store the generated
    2.36 -  %code. Note that the semantics of the destination depends on the target
    2.37 -  %language: for \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close> it denotes a \emph{file}, for
    2.38 -  %\<open>Haskell\<close> it denotes a \emph{directory} where a file named as the module
    2.39 -  %name (with extension \<open>.hs\<close>) is written:
    2.40 +  Output is written to a logical file-system within the theory context,
    2.41 +  with the theory name and ``\<^verbatim>\<open>code\<close>'' as overall prefix. There is also a
    2.42 +  formal session export using the same name: the result may be explored in
    2.43 +  the Isabelle/jEdit Prover IDE using the file-browser on the URL
    2.44 +  ``\<^verbatim>\<open>isabelle-export:\<close>''.
    2.45 +
    2.46 +  The file name is determined by the target language together with an
    2.47 +  optional \<^theory_text>\<open>file_prefix\<close> (the default is ``\<^verbatim>\<open>export\<close>'' with a consecutive
    2.48 +  number within the current theory). For \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close>, the
    2.49 +  file prefix becomes a plain file with extension (e.g.\ ``\<^verbatim>\<open>.ML\<close>'' for
    2.50 +  SML). For \<open>Haskell\<close> the file prefix becomes a directory that is populated
    2.51 +  with a separate file for each module (with extension ``\<^verbatim>\<open>.hs\<close>'').
    2.52 +
    2.53 +  Consider the following example:
    2.54  \<close>
    2.55  
    2.56  export_code %quote empty dequeue enqueue in Haskell
    2.57 -  module_name Example file_prefix examples
    2.58 +  module_name Example file_prefix example
    2.59  
    2.60  text \<open>
    2.61    \noindent This is the corresponding code:
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Mar 29 12:24:34 2019 +0100
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Fri Mar 29 13:42:17 2019 +0100
     3.3 @@ -2285,7 +2285,7 @@
     3.4      ;
     3.5      export_target:
     3.6        @'in' target (@'module_name' @{syntax name})? \<newline>
     3.7 -      (@'file_prefix' @{syntax embedded})? ('(' args ')')?
     3.8 +      (@'file_prefix' @{syntax path})? ('(' args ')')?
     3.9      ;
    3.10      target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
    3.11      ;
    3.12 @@ -2297,6 +2297,8 @@
    3.13      ;
    3.14      class: @{syntax name}
    3.15      ;
    3.16 +    path: @{syntax embedded}
    3.17 +    ;
    3.18      @@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
    3.19        | 'del' | 'drop:' (const+) | 'abort:' (const+))?
    3.20      ;
    3.21 @@ -2365,7 +2367,7 @@
    3.22      ;
    3.23      @@{command (HOL) code_reflect} @{syntax string} \<newline>
    3.24        (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \<newline>
    3.25 -      (@'functions' (@{syntax string} +))? (@'file' @{syntax string})?
    3.26 +      (@'functions' (@{syntax string} +))? (@'file' @{syntax path})?
    3.27      ;
    3.28      @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
    3.29      ;
    3.30 @@ -2391,11 +2393,16 @@
    3.31    "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
    3.32  
    3.33    Generated code is output as logical files within the theory context, as well
    3.34 -  as session exports that can be retrieved using @{tool_ref export} (or @{tool
    3.35 +  as session exports that can be retrieved using @{tool_ref export}, or @{tool
    3.36    build} with option \<^verbatim>\<open>-e\<close> and suitable \isakeyword{export\_files}
    3.37 -  specifications in the session \<^verbatim>\<open>ROOT\<close> entry). All files have a directory
    3.38 -  prefix \<^verbatim>\<open>code\<close> plus an extra file prefix that may be given via
    3.39 -  \<^theory_text>\<open>file_prefix\<close> --- the default is a numbered prefix \<^verbatim>\<open>export\<close>\<open>N\<close>.
    3.40 +  specifications in the session \<^verbatim>\<open>ROOT\<close> entry. All files have a common
    3.41 +  directory prefix: the long theory name plus ``\<^verbatim>\<open>code\<close>''. The actual file
    3.42 +  name is determined by the target language together with an optional
    3.43 +  \<^theory_text>\<open>file_prefix\<close> (the default is ``\<^verbatim>\<open>export\<close>'' with a consecutive number
    3.44 +  within the current theory). For \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close>, the file prefix
    3.45 +  becomes a plain file with extension (e.g.\ ``\<^verbatim>\<open>.ML\<close>'' for SML). For
    3.46 +  \<open>Haskell\<close> the file prefix becomes a directory that is populated with a
    3.47 +  separate file for each module (with extension ``\<^verbatim>\<open>.hs\<close>'').
    3.48  
    3.49    Serializers take an optional list of arguments in parentheses.
    3.50  
     4.1 --- a/src/Pure/Thy/export.ML	Fri Mar 29 12:24:34 2019 +0100
     4.2 +++ b/src/Pure/Thy/export.ML	Fri Mar 29 13:42:17 2019 +0100
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature EXPORT =
     4.6  sig
     4.7 +  val check_name: Path.T -> string
     4.8    type params = {theory: theory, path: Path.T, executable: bool, compress: bool}
     4.9    val export_params: params -> string list -> unit
    4.10    val export: theory -> Path.T -> string list -> unit
     5.1 --- a/src/Tools/Code/code_runtime.ML	Fri Mar 29 12:24:34 2019 +0100
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Mar 29 13:42:17 2019 +0100
     5.3 @@ -780,7 +780,7 @@
     5.4      (Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
     5.5        ::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
     5.6      -- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
     5.7 -    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.name)
     5.8 +    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.embedded)
     5.9      >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
    5.10        (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
    5.11  
     6.1 --- a/src/Tools/Code/code_target.ML	Fri Mar 29 12:24:34 2019 +0100
     6.2 +++ b/src/Tools/Code/code_target.ML	Fri Mar 29 13:42:17 2019 +0100
     6.3 @@ -276,17 +276,17 @@
     6.4  fun export_logical file_prefix format pretty_modules =
     6.5    let
     6.6      val prefix = Path.append (Path.basic codeN) file_prefix;
     6.7 -    fun export name content thy =
     6.8 +    fun export path content thy =
     6.9        let
    6.10 -        val path = Path.append prefix name;
    6.11          val thy' = thy |> Generated_Files.add_files ((path, Position.none), content);
    6.12          val _ = Export.export thy' path [content];
    6.13        in thy' end;
    6.14    in
    6.15      (case pretty_modules of
    6.16 -      Singleton (ext, p) => export (Path.basic (generatedN ^ "." ^ ext)) (format p)
    6.17 -    | Hierarchy modules => fold (fn (names, p) => export (Path.make names) (format p)) modules)
    6.18 -    #> tap (fn thy => writeln (Export.message thy prefix))
    6.19 +      Singleton (ext, p) => export (Path.ext ext prefix) (format p)
    6.20 +    | Hierarchy modules =>
    6.21 +        fold (fn (names, p) => export (Path.append prefix (Path.make names)) (format p)) modules)
    6.22 +    #> tap (fn thy => writeln (Export.message thy (Path.basic codeN)))
    6.23    end;
    6.24  
    6.25  fun export_physical root format pretty_modules =
    6.26 @@ -504,7 +504,10 @@
    6.27  
    6.28  fun prep_destination (location, (s, pos)) =
    6.29    if location = {physical = false} then
    6.30 -    (location, Path.explode s handle ERROR msg => error (msg ^ Position.here pos))
    6.31 +    let
    6.32 +      val path = (Path.explode s |> tap Export.check_name)
    6.33 +        handle ERROR msg => error (msg ^ Position.here pos)
    6.34 +    in (location, path) end
    6.35    else
    6.36      let
    6.37        val _ =