# HG changeset patch # User wenzelm # Date 1656015413 -7200 # Node ID 2a40ca7454bcf0aa04094b2afdff4b72d5041ce1 # Parent 5ec227251b07da44640fb32d8bfcd13168b69747# Parent 39df30349778afccf07891d346cd4745ea380e56 merged diff -r 5ec227251b07 -r 2a40ca7454bc src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/HOL/Library/code_test.ML Thu Jun 23 22:16:53 2022 +0200 @@ -153,7 +153,8 @@ | SOME drv => drv) val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir fun eval result = - with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result)) + with_dir "Code_Test" + (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result)) |> parse_result compiler fun evaluator program _ vs_ty deps = Exn.interruptible_capture eval diff -r 5ec227251b07 -r 2a40ca7454bc src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Jun 23 22:16:53 2022 +0200 @@ -215,8 +215,9 @@ |> Exn.release fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) - ctxt cookie (code_modules, _) = + ctxt cookie (code_modules_bytes, _) = let + val code_modules = (map o apsnd) Bytes.content code_modules_bytes val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie fun message s = if quiet then () else writeln s fun verbose_message s = if not quiet andalso verbose then writeln s else () diff -r 5ec227251b07 -r 2a40ca7454bc src/Pure/General/bytes.ML --- a/src/Pure/General/bytes.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Pure/General/bytes.ML Thu Jun 23 22:16:53 2022 +0200 @@ -12,6 +12,7 @@ sig val chunk_size: int type T + val eq: T * T -> bool val length: T -> int val contents: T -> string list val contents_blob: T -> XML.body @@ -27,6 +28,7 @@ val last_string: T -> string option val trim_line: T -> T val append: T -> T -> T + val appends: T list -> T val string: string -> T val newline: T val buffer: Buffer.T -> T @@ -56,6 +58,10 @@ val compact = implode o rev; +fun eq (Bytes {buffer, chunks, m, n}, Bytes {buffer = buffer', chunks = chunks', m = m', n = n'}) = + m = m' andalso n = n' andalso chunks = chunks' andalso + (buffer = buffer' orelse compact buffer = compact buffer); + fun contents (Bytes {buffer, chunks, ...}) = rev (chunks |> not (null buffer) ? cons (compact buffer)); @@ -136,6 +142,8 @@ else if is_empty bytes2 then bytes1 else bytes1 |> fold add (contents bytes2); +val appends = build o fold (fn b => fn a => append a b); + val string = build o add; val newline = string "\n"; @@ -196,10 +204,12 @@ | s => read (add s bytes)) in read empty end; -fun write_stream stream = File.outputs stream o contents; +fun write_stream stream bytes = + File.outputs stream (contents bytes); -val read = File.open_input (read_stream ~1); -val write = File.open_output write_stream; +fun read path = File.open_input (fn stream => read_stream ~1 stream) path; + +fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path; (* ML pretty printing *) diff -r 5ec227251b07 -r 2a40ca7454bc src/Pure/General/file.ML --- a/src/Pure/General/file.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Pure/General/file.ML Thu Jun 23 22:16:53 2022 +0200 @@ -34,7 +34,6 @@ val read: Path.T -> string val write: Path.T -> string -> unit val append: Path.T -> string -> unit - val generate: Path.T -> string -> unit val output: BinIO.outstream -> string -> unit val outputs: BinIO.outstream -> string list -> unit val write_list: Path.T -> string list -> unit @@ -170,7 +169,6 @@ fun write path txt = write_list path [txt]; fun append path txt = append_list path [txt]; -fun generate path txt = if try read path = SOME txt then () else write path txt; fun write_buffer path buf = open_output (fn file => List.app (output file) (Buffer.contents buf)) path; diff -r 5ec227251b07 -r 2a40ca7454bc src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Pure/Thy/export.ML Thu Jun 23 22:16:53 2022 +0200 @@ -53,10 +53,10 @@ {theory = thy, binding = binding, executable = true, compress = true, strict = true} body; fun export_file thy binding file = - export thy binding [XML.Text (File.read file)]; + export thy binding (Bytes.contents_blob (Bytes.read file)); fun export_executable_file thy binding file = - export_executable thy binding [XML.Text (File.read file)]; + export_executable thy binding (Bytes.contents_blob (Bytes.read file)); (* information message *) diff -r 5ec227251b07 -r 2a40ca7454bc src/Pure/Tools/generated_files.ML --- a/src/Pure/Tools/generated_files.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Pure/Tools/generated_files.ML Thu Jun 23 22:16:53 2022 +0200 @@ -6,8 +6,8 @@ signature GENERATED_FILES = sig - val add_files: Path.binding * string -> theory -> theory - type file = {path: Path.T, pos: Position.T, content: string} + val add_files: Path.binding * Bytes.T -> theory -> theory + type file = {path: Path.T, pos: Position.T, content: Bytes.T} val file_binding: file -> Path.binding val file_markup: file -> Markup.T val print_file: file -> string @@ -52,7 +52,7 @@ (** context data **) -type file = Path.T * (Position.T * string); +type file = Path.T * (Position.T * Bytes.T); type file_type = {name: string, ext: string, make_comment: string -> string, make_string: string -> string}; @@ -75,10 +75,11 @@ fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) = let val files' = - (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) => - if path1 <> path2 then false - else if file1 = file2 then true - else err_dup_files path1 (#1 file1) (#1 file2)))); + (files1, files2) |> Symtab.join (fn _ => + Library.merge (fn ((path1, (pos1, bytes1)), (path2, (pos2, bytes2))) => + if path1 <> path2 then false + else if pos1 = pos2 andalso Bytes.eq (bytes1, bytes2) then true + else err_dup_files path1 pos1 pos2)); val types' = Name_Space.merge_tables (types1, types2); val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2); in (files', types', antiqs') end; @@ -104,7 +105,7 @@ (* get files *) -type file = {path: Path.T, pos: Position.T, content: string}; +type file = {path: Path.T, pos: Position.T, content: Bytes.T}; fun file_binding (file: file) = Path.binding (#path file, #pos file); @@ -147,11 +148,15 @@ let val path = Path.expand (dir + #path file); val _ = Isabelle_System.make_directory (Path.dir path); - val _ = File.generate path (#content file); - in () end; + val content = #content file; + val write_content = + (case try Bytes.read path of + SOME old_content => not (Bytes.eq (content, old_content)) + | NONE => true) + in if write_content then Bytes.write path content else () end; fun export_file thy (file: file) = - Export.export thy (file_binding file) [XML.Text (#content file)]; + Export.export thy (file_binding file) (Bytes.contents_blob (#content file)); (* file types *) @@ -244,7 +249,7 @@ handle ERROR msg => error (msg ^ Position.here pos); val header = #make_comment file_type " generated by Isabelle "; - val content = header ^ "\n" ^ read_source lthy file_type source; + val content = Bytes.string (header ^ "\n" ^ read_source lthy file_type source); in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end; fun generate_file_cmd (file, source) lthy = @@ -297,15 +302,15 @@ val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe); val (path, pos) = Path.dest_binding binding; val content = - (case try File.read (dir + path) of - SOME context => context + (case try Bytes.read (dir + path) of + SOME bytes => Bytes.contents_blob bytes | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos)); val _ = Export.report_export thy export_prefix; val binding' = Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding; in (if is_some executable then Export.export_executable else Export.export) - thy binding' [XML.Text content] + thy binding' content end)); val _ = if null export then () diff -r 5ec227251b07 -r 2a40ca7454bc src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Tools/Code/code_printer.ML Thu Jun 23 22:16:53 2022 +0200 @@ -26,7 +26,7 @@ val doublesemicolon: Pretty.T list -> Pretty.T val indent: int -> Pretty.T -> Pretty.T val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T - val format: Code_Symbol.T list -> int -> Pretty.T -> string + val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T type var_ctxt val make_vars: string list -> var_ctxt @@ -165,7 +165,7 @@ #> YXML.parse_body #> filter_presentation presentation_names #> Buffer.add "\n" - #> Buffer.content; + #> Bytes.buffer; (** names and variable name contexts **) diff -r 5ec227251b07 -r 2a40ca7454bc src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Tools/Code/code_runtime.ML Thu Jun 23 22:16:53 2022 +0200 @@ -92,7 +92,7 @@ fun build_compilation_text ctxt some_target program consts = Code_Target.compilation_text ctxt (the_default target some_target) program consts false - #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); + #>> (fn ml_modules => space_implode "\n\n" (map (Bytes.content o snd) ml_modules)); fun run_compilation_text cookie ctxt comp vs_t args = let @@ -439,7 +439,7 @@ val (ml_modules, target_names) = Code_Target.produce_code_for ctxt target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos); - val ml_code = space_implode "\n\n" (map snd ml_modules); + val ml_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules); val (consts', tycos') = chop (length consts) target_names; val consts_map = map2 (fn const => fn NONE => @@ -482,7 +482,7 @@ | SOME c' => c'; val tyco_names = map deresolve_tyco named_tycos; val const_names = map deresolve_const named_consts; - val generated_code = space_implode "\n\n" (map snd ml_modules); + val generated_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules); val (of_term_code, of_term_names) = print_computation_code ctxt compiled_value computation_cTs computation_Ts; val compiled_computation = generated_code ^ "\n" ^ of_term_code; @@ -720,7 +720,7 @@ "(* Generated from " ^ Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ "; DO NOT EDIT! *)"; - val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy; + val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy; val _ = Code_Target.code_export_message thy'; in thy' end; diff -r 5ec227251b07 -r 2a40ca7454bc src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Jun 22 08:15:14 2022 +0000 +++ b/src/Tools/Code/code_target.ML Thu Jun 23 22:16:53 2022 +0200 @@ -16,9 +16,9 @@ -> 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 + -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * Bytes.T) list * string option list val present_code_for: Proof.context -> string -> string -> int option -> Token.T list - -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string + -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> Bytes.T val check_code_for: string -> bool -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory @@ -29,9 +29,9 @@ -> (((string * string) * ({physical: bool} * Input.source) 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 + -> string -> string -> int option -> Token.T list -> (string list * Bytes.T) list * string option list val present_code: Proof.context -> string list -> Code_Symbol.T list - -> string -> string -> int option -> Token.T list -> string + -> string -> string -> int option -> Token.T list -> Bytes.T val check_code: bool -> string list -> ((string * bool) * Token.T list) list -> local_theory -> local_theory @@ -39,13 +39,13 @@ val generatedN: string val code_path: Path.T -> Path.T val code_export_message: theory -> unit - val export: Path.binding -> string -> theory -> theory + val export: Path.binding -> Bytes.T -> theory -> theory val compilation_text: Proof.context -> string -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm - -> (string list * string) list * string + -> (string list * Bytes.T) list * string val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm - -> ((string list * string) list * string) * (Code_Symbol.T -> string option) + -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option) type serializer type literals = Code_Printer.literals @@ -289,7 +289,7 @@ fun export binding content thy = let val thy' = thy |> Generated_Files.add_files (binding, content); - val _ = Export.export thy' binding [XML.Text content]; + val _ = Export.export thy' binding (Bytes.contents_blob content); in thy' end; local @@ -309,11 +309,11 @@ fun export_physical root format pretty_modules = (case pretty_modules of - Singleton (_, p) => File.write root (format p) + Singleton (_, p) => Bytes.write root (format p) | Hierarchy code_modules => (Isabelle_System.make_directory root; List.app (fn (names, p) => - File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); + Bytes.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules)); in @@ -343,7 +343,8 @@ 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)) + | Hierarchy code_modules => + Bytes.appends (separate (Bytes.string "\n\n") (map (format o #2) code_modules))) end; end; @@ -788,6 +789,7 @@ (fn ctxt => fn ((consts, symbols), (target_name, some_width)) => present_code ctxt consts symbols target_name "Example" some_width [] + |> Bytes.content |> trim_line |> Document_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));