# HG changeset patch # User haftmann # Date 1547122028 0 # Node ID e02bdf853a4c861a0f30e1d2d0d0758d983eac12 # Parent ef02c5e051e57fa454028b2dda38a9e1327f4258 optional code export as theory export diff -r ef02c5e051e5 -r e02bdf853a4c NEWS --- 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, diff -r ef02c5e051e5 -r e02bdf853a4c src/Doc/Isar_Ref/HOL_Specific.thy --- 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>\all\ code is placed in this module. - For \<^emph>\SML\, \<^emph>\OCaml\ and \<^emph>\Scala\ 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>\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. 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. diff -r ef02c5e051e5 -r e02bdf853a4c src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy --- 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. \a b. a \ A \ b \ B \ 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 diff -r ef02c5e051e5 -r e02bdf853a4c src/Tools/Code/code_target.ML --- 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>\in\ |-- Parse.!!! (Parse.name -- Scan.optional (\<^keyword>\module_name\ |-- Parse.name) "" - -- Scan.optional (\<^keyword>\file\ |-- Parse.position Parse.path) ("", Position.none) + -- Scan.option (\<^keyword>\file\ |-- Parse.position Parse.path) -- code_expr_argsP)) >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);