--- a/NEWS Thu Jan 10 12:07:05 2019 +0000
+++ b/NEWS Thu Jan 10 12:07:08 2019 +0000
@@ -70,6 +70,11 @@
*** HOL ***
+* Code generation: command 'export_code' without file keyword exports
+code as regular theory export, which can be materialized using tool
+'isabelle export'; to get generated code dumped into output, use
+'file ""'. Minor INCOMPATIBILITY.
+
* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 10 12:07:05 2019 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 10 12:07:08 2019 +0000
@@ -2386,10 +2386,13 @@
generated. Alternatively, a module name may be specified after the @{keyword
"module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
- For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
+ 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>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is
- generated in multiple files reflecting the module hierarchy. Omitting the
- file specification denotes standard output.
+ generated in multiple files reflecting the module hierarchy.
+ Passing an empty file specification denotes standard output.
Serializers take an optional list of arguments in parentheses.
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:05 2019 +0000
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:08 2019 +0000
@@ -133,8 +133,6 @@
where
"products A B = {c. \<exists>a b. a \<in> A \<and> b \<in> B \<and> c = a * b}"
-export_code products in Haskell
-
-export_code union common_subsets products in Haskell
+export_code union common_subsets products checking SML
end
--- a/src/Tools/Code/code_target.ML Thu Jan 10 12:07:05 2019 +0000
+++ b/src/Tools/Code/code_target.ML Thu Jan 10 12:07:08 2019 +0000
@@ -11,7 +11,7 @@
datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
- val export_code_for: Proof.context -> Path.T option -> string -> string -> int option -> Token.T list
+ val export_code_for: Proof.context -> Path.T option option -> string -> string -> int option -> Token.T list
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
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,7 +21,7 @@
-> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
val export_code: Proof.context -> bool -> string list
- -> (((string * string) * Path.T option) * Token.T list) list -> unit
+ -> (((string * string) * Path.T option option) * Token.T list) list -> unit
val produce_code: Proof.context -> bool -> string list
-> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
val present_code: Proof.context -> string list -> Code_Symbol.T list
@@ -162,6 +162,8 @@
-> Code_Symbol.T list
-> pretty_modules * (Code_Symbol.T -> string option);
+val generatedN = "Generated_Code";
+
fun flat_modules selects width (Singleton (_, p)) =
Code_Printer.format selects width p
| flat_modules selects width (Hierarchy code_modules) =
@@ -174,14 +176,25 @@
map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules;
());
-fun export_result ctxt some_root width (pretty_code, _) =
- case some_root of
- NONE => (writeln (flat_modules [] width pretty_code); ())
- | SOME relative_root =>
+fun export_to_exports thy width (Singleton (extension, p)) =
+ Export.export_raw thy (generatedN ^ "." ^ extension) [Code_Printer.format [] width p]
+ | export_to_exports thy width (Hierarchy code_modules) = (
+ map (fn (names, p) => Export.export_raw thy (Path.implode (Path.make names))
+ [Code_Printer.format [] width p]) code_modules;
+ ());
+
+fun export_result ctxt some_file width (pretty_code, _) =
+ (case some_file of
+ NONE =>
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in export_to_exports thy width pretty_code end
+ | SOME NONE => writeln (flat_modules [] width pretty_code)
+ | SOME (SOME relative_root) =>
let
val root = File.full_path (Resources.master_directory (Proof_Context.theory_of ctxt)) relative_root;
val _ = File.check_dir (Path.dir root);
- in export_to_file root width pretty_code end;
+ in export_to_file root width pretty_code end);
fun produce_result syms width (Singleton (_, p), deresolve) =
([([], Code_Printer.format [] width p)], map deresolve syms)
@@ -376,10 +389,8 @@
in
-val generatedN = "Generated_Code";
-
-fun export_code_for ctxt some_root target_name module_name some_width args =
- export_result ctxt some_root (the_width ctxt some_width)
+fun export_code_for ctxt some_file target_name module_name some_width args =
+ export_result ctxt some_file (the_width ctxt some_width)
ooo invoke_serializer ctxt target_name module_name args;
fun produce_code_for ctxt target_name module_name some_width args =
@@ -404,7 +415,7 @@
fun ext_check p =
let
val destination = make_destination p;
- val _ = export_result ctxt (SOME destination) 80
+ val _ = export_result ctxt (SOME (SOME destination)) 80
(invoke_serializer ctxt target_name generatedN args program all_public syms)
val cmd = make_command generatedN;
in
@@ -469,14 +480,14 @@
fun export_code ctxt all_public cs seris =
let
val program = Code_Thingol.consts_program ctxt cs;
- val _ = map (fn (((target_name, module_name), some_root), args) =>
- export_code_for ctxt some_root target_name module_name NONE args program all_public (map Constant cs)) seris;
+ val _ = map (fn (((target_name, module_name), some_file), args) =>
+ export_code_for ctxt some_file target_name module_name NONE args program all_public (map Constant cs)) seris;
in () end;
fun export_code_cmd all_public raw_cs seris ctxt =
export_code ctxt all_public
(Code_Thingol.read_const_exprs ctxt raw_cs)
- ((map o apfst o apsnd) prep_destination seris);
+ ((map o apfst o apsnd o Option.map) prep_destination seris);
fun produce_code ctxt all_public cs target_name some_width some_module_name args =
let
@@ -681,7 +692,7 @@
fun code_expr_inP all_public raw_cs =
Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
-- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
- -- Scan.optional (\<^keyword>\<open>file\<close> |-- Parse.position Parse.path) ("", Position.none)
+ -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.position Parse.path)
-- code_expr_argsP))
>> (fn seri_args => export_code_cmd all_public raw_cs seri_args);