# HG changeset patch # User wenzelm # Date 1553804695 -3600 # Node ID 435fb018e8eeca6c0f1519422fb97568a1e61623 # Parent 7aaebfcf313439f141e8e25a3d67b7c98a649d88 "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples; diff -r 7aaebfcf3134 -r 435fb018e8ee NEWS --- a/NEWS Thu Mar 28 21:22:44 2019 +0100 +++ b/NEWS Thu Mar 28 21:24:55 2019 +0100 @@ -132,12 +132,21 @@ Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result] to lift specifications to the global theory level. -* Code generation: command 'export_code' without file keyword exports -code as regular theory export, which can be materialized using the -command-line tools "isabelle export" or "isabelle build -e" (with -'export_files' in the session ROOT), or browsed in Isabelle/jEdit via -the "isabelle-export:" file-system. To get generated code dumped into -output, use "file \\". Minor INCOMPATIBILITY. +* Command 'export_code' produces output as logical files within the +theory context, as well as session exports that can be materialized +using the command-line tools "isabelle export" or "isabelle build -e" +(with 'export_files' in the session ROOT), or browsed in Isabelle/jEdit +via the "isabelle-export:" file-system. A 'file_prefix' argument allows +to specify an explicit prefix, the default is "export" with a +consecutive number within each theory. The overall prefix "code" is +always prepended. + +* Command 'export_code': the 'file' argument is now legacy and will be +removed soon: writing to the physical file-system is not well-defined in +a reactive/parallel application like Isabelle. The empty 'file' has been +discontinued already: it has been superseded by the file-browser in +Isabelle/jEdit with "isabelle-export:" as file-system. Minor +INCOMPATIBILITY. * Code generation for OCaml: proper strings are used for literals. Minor INCOMPATIBILITY. diff -r 7aaebfcf3134 -r 435fb018e8ee src/Doc/Codegen/Introduction.thy --- a/src/Doc/Codegen/Introduction.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Doc/Codegen/Introduction.thy Thu Mar 28 21:24:55 2019 +0100 @@ -69,7 +69,7 @@ text \\noindent Then we can generate code e.g.~for \SML\ as follows:\ export_code %quote empty dequeue enqueue in SML - module_name Example file \$ISABELLE_TMP/example.ML\ + module_name Example file_prefix example text \\noindent resulting in the following code:\ @@ -78,19 +78,29 @@ \ text \ - \noindent The @{command_def export_code} command takes a - space-separated list of constants for which code shall be generated; - anything else needed for those is added implicitly. Then follows a - target language identifier and a freely chosen module name. A file - name denotes the destination to store the generated code. Note that - the semantics of the destination depends on the target language: for - \SML\, \OCaml\ and \Scala\ it denotes a \emph{file}, - for \Haskell\ it denotes a \emph{directory} where a file named as the - module name (with extension \.hs\) is written: + \noindent The @{command_def export_code} command takes a space-separated + list of constants for which code shall be generated; anything else needed + for those is added implicitly. Then follows a target language identifier + and a freely chosen \<^theory_text>\module_name\. A \<^theory_text>\file_prefix\ introduces + sub-directory structure for the output of logical files (within the + theory context), as well as session exports; the default is \<^verbatim>\export\ + with a consecutive number within the current theory. The prefix \<^verbatim>\code\ + is always prepended to the code output directory. For \SML\, \OCaml\ and + \Scala\ the result is a single file, for \Haskell\ each module gets its + own file with the module name and extension \<^verbatim>\.hs\. Here is an example:\<^footnote>\ + The exports may be explored within the Isabelle/jEdit Prover IDE using + the file-browser on the \<^verbatim>\isabelle-export:\ virtual file-system.\ + + %FIXME old/new "name" + %name denotes the destination to store the generated + %code. Note that the semantics of the destination depends on the target + %language: for \SML\, \OCaml\ and \Scala\ it denotes a \emph{file}, for + %\Haskell\ it denotes a \emph{directory} where a file named as the module + %name (with extension \.hs\) is written: \ export_code %quote empty dequeue enqueue in Haskell - module_name Example file \$ISABELLE_TMP/examples/\ + module_name Example file_prefix examples text \ \noindent This is the corresponding code: diff -r 7aaebfcf3134 -r 435fb018e8ee src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Mar 28 21:24:55 2019 +0100 @@ -2284,8 +2284,8 @@ @@{command (HOL) export_code} @'open'? \ (const_expr+) (export_target*) ; export_target: - @'in' target (@'module_name' @{syntax string})? \ - (@'file' @{syntax string})? ('(' args ')')? + @'in' target (@'module_name' @{syntax name})? \ + (@'file_prefix' @{syntax embedded})? ('(' args ')')? ; target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval' ; @@ -2390,13 +2390,12 @@ generated. Alternatively, a module name may be specified after the @{keyword "module_name"} keyword; then \<^emph>\all\ code is placed in this module. - By default, generated code is treated as theory export which can be - explicitly retrieved using @{tool_ref export}. For diagnostic purposes - generated code can also be written to the file system using @{keyword "file"}; - for \<^emph>\SML\, \<^emph>\OCaml\ and \<^emph>\Scala\ the file specification refers to a single - file; for \<^emph>\Haskell\, it refers to a whole directory, where code is - generated in multiple files reflecting the module hierarchy. - Passing an empty file specification denotes standard output. + Generated code is output as logical files within the theory context, as well + as session exports that can be retrieved using @{tool_ref export} (or @{tool + build} with option \<^verbatim>\-e\ and suitable \isakeyword{export\_files} + specifications in the session \<^verbatim>\ROOT\ entry). All files have a directory + prefix \<^verbatim>\code\ plus an extra file prefix that may be given via + \<^theory_text>\file_prefix\ --- the default is a numbered prefix \<^verbatim>\export\\N\. Serializers take an optional list of arguments in parentheses. diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/Code_Numeral.thy Thu Mar 28 21:24:55 2019 +0100 @@ -766,7 +766,7 @@ code_identifier code_module Code_Numeral \ (SML) Arith and (OCaml) Arith and (Haskell) Arith -export_code divmod_integer in Haskell +export_code divmod_integer in Haskell file_prefix divmod subsection \Type of target language naturals\ diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Quotient_Examples/Lift_DList.thy --- a/src/HOL/Quotient_Examples/Lift_DList.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Thu Mar 28 21:24:55 2019 +0100 @@ -50,5 +50,6 @@ text \We can export code:\ export_code empty insert remove map filter null member length fold foldr concat in SML + file_prefix dlist end diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Thu Mar 28 21:24:55 2019 +0100 @@ -113,7 +113,8 @@ text \We can export code:\ -export_code fnil fcons fappend fmap ffilter fset fmember in SML +export_code fnil fcons fappend fmap ffilter fset fmember in SML file_prefix fset + subsection \Using transfer with type \fset\\ diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Quotient_Examples/Lift_Set.thy --- a/src/HOL/Quotient_Examples/Lift_Set.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/Quotient_Examples/Lift_Set.thy Thu Mar 28 21:24:55 2019 +0100 @@ -28,6 +28,6 @@ term "Lift_Set.insert" thm Lift_Set.insert_def -export_code empty insert in SML +export_code empty insert in SML file_prefix set end diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/ex/Code_Lazy_Demo.thy --- a/src/HOL/ex/Code_Lazy_Demo.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/HOL/ex/Code_Lazy_Demo.thy Thu Mar 28 21:24:55 2019 +0100 @@ -62,7 +62,7 @@ | "lfilter P (x ### xs) = (if P x then x ### lfilter P xs else lfilter P xs)" -export_code lfilter in SML +export_code lfilter in SML file_prefix lfilter value [code] "lfilter odd llist" diff -r 7aaebfcf3134 -r 435fb018e8ee src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Pure/Pure.thy Thu Mar 28 21:24:55 2019 +0100 @@ -140,7 +140,7 @@ val paths = Generated_Files.export_files thy other_thys; in if not (null paths) then - (writeln (Export.message thy ""); + (writeln (Export.message thy Path.current); writeln (cat_lines (paths |> map (fn (path, pos) => Markup.markup (Markup.entityN, Position.def_properties_of pos) (quote (Path.implode path)))))) diff -r 7aaebfcf3134 -r 435fb018e8ee src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Pure/Thy/export.ML Thu Mar 28 21:24:55 2019 +0100 @@ -10,8 +10,8 @@ val export_params: params -> string list -> unit val export: theory -> Path.T -> string list -> unit val export_executable: theory -> Path.T -> string list -> unit - val markup: theory -> string -> Markup.T - val message: theory -> string -> string + val markup: theory -> Path.T -> Markup.T + val message: theory -> Path.T -> string end; structure Export: EXPORT = @@ -47,11 +47,13 @@ (* information message *) -fun markup thy s = - let val name = (Markup.nameN, Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s)) +fun markup thy path = + let + val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path; + val name = (Markup.nameN, Path.implode thy_path); in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end; -fun message thy s = - "See " ^ Markup.markup (markup thy s) "theory exports"; +fun message thy path = + "See " ^ Markup.markup (markup thy path) "theory exports"; end; diff -r 7aaebfcf3134 -r 435fb018e8ee src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Tools/Code/code_target.ML Thu Mar 28 21:24:55 2019 +0100 @@ -11,7 +11,7 @@ datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; - val export_code_for: Path.T option option -> string -> string -> int option -> Token.T list + val export_code_for: ({physical: bool} * Path.T) option -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list @@ -21,10 +21,10 @@ -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory val export_code: bool -> string list - -> (((string * string) * Path.T option option) * Token.T list) list + -> (((string * string) * ({physical: bool} * Path.T) option) * Token.T list) list -> local_theory -> local_theory val export_code_cmd: bool -> string list - -> (((string * string) * (string * Position.T) option) * Token.T list) list + -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list -> local_theory -> local_theory val produce_code: Proof.context -> bool -> string list -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list @@ -33,6 +33,7 @@ val check_code: bool -> string list -> ((string * bool) * Token.T list) list -> local_theory -> local_theory + val codeN: string val generatedN: string val compilation_text: Proof.context -> string -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm @@ -148,7 +149,7 @@ end; -(** serializers **) +(** theory data **) datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; @@ -166,65 +167,6 @@ -> Code_Symbol.T list -> pretty_modules * (Code_Symbol.T -> string option); -val generatedN = "Generated_Code"; - -local - -fun flat_modules format pretty_modules = - (case pretty_modules of - Singleton (_, p) => format p - | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules)); - -fun export_to_file root format pretty_modules = - (case pretty_modules of - Singleton (_, p) => File.write root (format p) - | Hierarchy code_modules => - (Isabelle_System.mkdirs root; - List.app (fn (names, p) => - File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); - -fun export_to_exports format pretty_modules = - let - fun export name content thy = (Export.export thy name [content]; thy); - in - (case pretty_modules of - Singleton (ext, p) => export (Path.basic (generatedN ^ "." ^ ext)) (format p) - | Hierarchy modules => fold (fn (names, p) => export (Path.make names) (format p)) modules) - end; - -in - -fun export_result some_file format (pretty_code, _) thy = - (case some_file of - NONE => - let - val thy' = export_to_exports format pretty_code thy; - val _ = writeln (Export.message thy' ""); - in thy' end - | SOME NONE => (writeln (flat_modules format pretty_code); thy) - | SOME (SOME relative_root) => - let - val root = File.full_path (Resources.master_directory thy) relative_root; - val _ = File.check_dir (Path.dir root); - val _ = export_to_file root format pretty_code; - in thy end); - -fun produce_result syms width pretty_modules = - let val format = Code_Printer.format [] width in - (case pretty_modules of - (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms) - | (Hierarchy code_modules, deresolve) => - ((map o apsnd) format code_modules, map deresolve syms)) - end; - -fun present_result selects width (pretty_code, _) = - flat_modules (Code_Printer.format selects width) pretty_code; - -end; - - -(** theory data **) - type language = {serializer: serializer, literals: literals, check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string}, evaluation_args: Token.T list}; @@ -237,26 +179,33 @@ structure Targets = Theory_Data ( - type T = (target * Code_Printer.data) Symtab.table; - val empty = Symtab.empty; - val extend = I; - fun merge (targets1, targets2) : T = - Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => - if #serial target1 = #serial target2 then - ({serial = #serial target1, language = #language target1, - ancestry = merge_ancestry (#ancestry target1, #ancestry target2)}, - Code_Printer.merge_data (data1, data2)) - else error ("Incompatible targets: " ^ quote target_name) - ) (targets1, targets2) + type T = (target * Code_Printer.data) Symtab.table * int; + val empty = (Symtab.empty, 0); + fun extend (targets, _) = (targets, 0); + fun merge ((targets1, _), (targets2, _)) : T = + let val targets' = + Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) => + if #serial target1 = #serial target2 then + ({serial = #serial target1, language = #language target1, + ancestry = merge_ancestry (#ancestry target1, #ancestry target2)}, + Code_Printer.merge_data (data1, data2)) + else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2) + in (targets', 0) end; ); -fun exists_target thy = Symtab.defined (Targets.get thy); -fun lookup_target_data thy = Symtab.lookup (Targets.get thy); +val exists_target = Symtab.defined o #1 o Targets.get; +val lookup_target_data = Symtab.lookup o #1 o Targets.get; fun assert_target thy target_name = if exists_target thy target_name then target_name else error ("Unknown code target language: " ^ quote target_name); +fun next_export thy = + let + val thy' = (Targets.map o apsnd) (fn i => i + 1) thy; + val i = #2 (Targets.get thy'); + in ("export" ^ string_of_int i, thy') end; + fun fold1 f xs = fold f (tl xs) (hd xs); fun join_ancestry thy target_name = @@ -278,7 +227,7 @@ else (); in thy - |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data)) + |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data)) end; fun add_language (target_name, language) = @@ -309,7 +258,7 @@ val _ = assert_target thy target_name; in thy - |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f + |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f end; fun map_reserved target_name = map_data target_name o @{apply 3(1)}; @@ -317,6 +266,71 @@ fun map_printings target_name = map_data target_name o @{apply 3(3)}; +(** serializers **) + +val codeN = "code"; +val generatedN = "Generated_Code"; + +local + +fun export_logical file_prefix format pretty_modules = + let + val prefix = Path.append (Path.basic codeN) file_prefix; + fun export name content thy = + let + val path = Path.append prefix name; + val thy' = thy |> Generated_Files.add_files ((path, Position.none), content); + val _ = Export.export thy' path [content]; + in thy' end; + in + (case pretty_modules of + Singleton (ext, p) => export (Path.basic (generatedN ^ "." ^ ext)) (format p) + | Hierarchy modules => fold (fn (names, p) => export (Path.make names) (format p)) modules) + #> tap (fn thy => writeln (Export.message thy prefix)) + end; + +fun export_physical root format pretty_modules = + (case pretty_modules of + Singleton (_, p) => File.write root (format p) + | Hierarchy code_modules => + (Isabelle_System.mkdirs root; + List.app (fn (names, p) => + File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); + +in + +fun export_result some_file format (pretty_code, _) thy = + (case some_file of + NONE => + let val (file_prefix, thy') = next_export thy; + in export_logical (Path.basic file_prefix) format pretty_code thy' end + | SOME ({physical = false}, file_prefix) => + export_logical file_prefix format pretty_code thy + | SOME ({physical = true}, file) => + let + val root = File.full_path (Resources.master_directory thy) file; + val _ = File.check_dir (Path.dir root); + val _ = export_physical root format pretty_code; + in thy end); + +fun produce_result syms width pretty_modules = + let val format = Code_Printer.format [] width in + (case pretty_modules of + (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms) + | (Hierarchy code_modules, deresolve) => + ((map o apsnd) format code_modules, map deresolve syms)) + end; + +fun present_result selects width (pretty_modules, _) = + let val format = Code_Printer.format selects width in + (case pretty_modules of + Singleton (_, p) => format p + | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules)) + end; + +end; + + (** serializer usage **) (* technical aside: pretty printing width *) @@ -434,7 +448,7 @@ val destination = make_destination p; val lthy' = lthy |> Local_Theory.background_theory - (export_result (SOME (SOME destination)) format + (export_result (SOME ({physical = true}, destination)) format (invoke_serializer lthy target_name generatedN args program all_public syms)); val cmd = make_command generatedN; val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1"; @@ -488,14 +502,23 @@ (* code generation *) -fun prep_destination (s, pos) = - if s = "" then NONE +fun prep_destination (location, (s, pos)) = + if location = {physical = false} then + (location, Path.explode s handle ERROR msg => error (msg ^ Position.here pos)) else let + val _ = + if s = "" + then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument") + else (); + val _ = + legacy_feature + (Markup.markup Markup.keyword1 "export_code" ^ " with " ^ + Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos); val _ = Position.report pos Markup.language_path; val path = Path.explode s; val _ = Position.report pos (Markup.path (Path.smart_implode path)); - in SOME path end; + in (location, path) end; fun export_code all_public cs seris lthy = let @@ -671,7 +694,9 @@ fun code_expr_inP (all_public, raw_cs) = Scan.repeat (\<^keyword>\in\ |-- Parse.!!! (Parse.name -- Scan.optional (\<^keyword>\module_name\ |-- Parse.name) "" - -- Scan.option (\<^keyword>\file\ |-- Parse.position Parse.path) + -- Scan.option + ((\<^keyword>\file_prefix\ >> K {physical = false} || \<^keyword>\file\ >> K {physical = true}) + -- Parse.!!! (Parse.position Parse.path)) -- code_expr_argsP)) >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); diff -r 7aaebfcf3134 -r 435fb018e8ee src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Thu Mar 28 21:22:44 2019 +0100 +++ b/src/Tools/Code_Generator.thy Thu Mar 28 21:24:55 2019 +0100 @@ -11,7 +11,7 @@ "export_code" "code_identifier" "code_printing" "code_reserved" "code_monad" "code_reflect" :: thy_decl and "checking" and - "datatypes" "functions" "module_name" "file" + "datatypes" "functions" "module_name" "file" "file_prefix" "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module" :: quasi_command begin