# HG changeset patch # User wenzelm # Date 1553720310 -3600 # Node ID 76554a0cafe329c82d8145d79b01d3473669b5a1 # Parent c61f6bc9cf5c9c1475544f16a7e3efcbcbaa09f6 export_code/check_code formally updates the theory -- this opens further possibilities concerning Generated_Files; tuned; diff -r c61f6bc9cf5c -r 76554a0cafe3 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Mar 27 20:07:53 2019 +0100 +++ b/src/Tools/Code/code_target.ML Wed Mar 27 21:58:30 2019 +0100 @@ -11,23 +11,22 @@ datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.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 export_code_for: Path.T option option -> string -> string -> int option -> Token.T list + -> Code_Thingol.program -> bool -> Code_Symbol.T list -> theory -> 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 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 - val check_code_for: Proof.context -> string -> bool -> Token.T list - -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit + val check_code_for: string -> bool -> Token.T list + -> Code_Thingol.program -> bool -> Code_Symbol.T list -> theory -> theory - val export_code: Proof.context -> bool -> string list - -> (((string * string) * Path.T option option) * Token.T list) list -> unit + val export_code: bool -> string list + -> (((string * string) * Path.T option option) * Token.T list) list -> theory -> theory 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 -> string -> string -> int option -> Token.T list -> string - val check_code: Proof.context -> bool -> string list - -> ((string * bool) * Token.T list) list -> unit + val check_code: bool -> string list -> ((string * bool) * Token.T list) list -> theory -> theory val generatedN: string val compilation_text: Proof.context -> string -> Code_Thingol.program @@ -164,41 +163,51 @@ val generatedN = "Generated_Code"; -fun flat_modules selects width (Singleton (_, p)) = - Code_Printer.format selects width p - | flat_modules selects width (Hierarchy code_modules) = - space_implode "\n\n" (map (Code_Printer.format selects width o snd) code_modules); +local -fun export_to_file root width (Singleton (_, p)) = - File.write root (Code_Printer.format [] width p) - | export_to_file root width (Hierarchy code_modules) = ( - Isabelle_System.mkdirs root; - map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules; - ()); +fun flat_modules 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; -fun export_information thy name content = - (Export.export thy name [content]; writeln (Export.message thy "")); +fun export_to_file root width pretty_modules = + let val format = Code_Printer.format [] width in + (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)) + end; -fun export_to_exports thy width (Singleton (extension, p)) = - export_information thy (Path.basic (generatedN ^ "." ^ extension)) - (Code_Printer.format [] width p) - | export_to_exports thy width (Hierarchy code_modules) = ( - map (fn (names, p) => export_information thy (Path.make names) - (Code_Printer.format [] width p)) code_modules; - ()); +fun export_to_exports width pretty_modules = + let + val format = Code_Printer.format [] width; + 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; -fun export_result ctxt some_file width (pretty_code, _) = +in + +fun export_result some_file width (pretty_code, _) thy = (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) + val thy' = export_to_exports width pretty_code thy; + val _ = writeln (Export.message thy' ""); + in thy' end + | SOME NONE => (writeln (flat_modules [] width pretty_code); thy) | SOME (SOME relative_root) => let - val root = File.full_path (Resources.master_directory (Proof_Context.theory_of ctxt)) relative_root; + val root = File.full_path (Resources.master_directory thy) relative_root; val _ = File.check_dir (Path.dir root); - in export_to_file root width pretty_code end); + val _ = export_to_file root width pretty_code; + in thy end); fun produce_result syms width (Singleton (_, p), deresolve) = ([([], Code_Printer.format [] width p)], map deresolve syms) @@ -208,6 +217,8 @@ fun present_result selects width (pretty_code, _) = flat_modules selects width pretty_code; +end; + (** theory data **) @@ -390,9 +401,12 @@ in -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 export_code_for some_file target_name module_name some_width args program all_public cs thy = + let + val thy_ctxt = Proof_Context.init_global thy; + val width = the_width thy_ctxt some_width; + val res = invoke_serializer thy_ctxt target_name module_name args program all_public cs; + in export_result some_file width res thy end; fun produce_code_for ctxt target_name module_name some_width args = let @@ -409,27 +423,28 @@ present_result selects (the_width ctxt some_width) (serializer program false syms) end; -fun check_code_for ctxt target_name strict args program all_public syms = +fun check_code_for target_name strict args program all_public syms thy = let - val { env_var, make_destination, make_command } = - (#check o the_language ctxt) target_name; + val thy_ctxt = Proof_Context.init_global thy; + val { env_var, make_destination, make_command } = #check (the_language thy_ctxt target_name); fun ext_check p = let val destination = make_destination p; - val _ = export_result ctxt (SOME (SOME destination)) 80 - (invoke_serializer ctxt target_name generatedN args program all_public syms) + val thy' = + export_result (SOME (SOME destination)) 80 + (invoke_serializer thy_ctxt target_name generatedN args program all_public syms) thy; val cmd = make_command generatedN; val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1"; in if Isabelle_System.bash context_cmd <> 0 then error ("Code check failed for " ^ target_name ^ ": " ^ cmd) - else () + else thy' end; in - if not (env_var = "") andalso getenv env_var = "" - then if strict + if not (env_var = "") andalso getenv env_var = "" then + if strict then error (env_var ^ " not set; cannot check code for " ^ target_name) - else warning (env_var ^ " not set; skipped checking code for " ^ target_name) + else (warning (env_var ^ " not set; skipped checking code for " ^ target_name); thy) else Isabelle_System.with_tmp_dir "Code_Test" ext_check end; @@ -479,17 +494,21 @@ val _ = Position.report pos (Markup.path (Path.smart_implode path)); in SOME path end; -fun export_code ctxt all_public cs seris = +fun export_code all_public cs seris thy = let - val program = Code_Thingol.consts_program ctxt cs; - 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; + val thy_ctxt = Proof_Context.init_global thy; + val program = Code_Thingol.consts_program thy_ctxt cs; + in + (seris, thy) |-> fold (fn (((target_name, module_name), some_file), args) => + export_code_for some_file target_name module_name NONE args + program all_public (map Constant cs)) + 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 o Option.map) prep_destination seris); +fun export_code_cmd all_public raw_cs seris thy = + let + val thy_ctxt = Proof_Context.init_global thy; + val cs = Code_Thingol.read_const_exprs thy_ctxt raw_cs; + in export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris) thy end; fun produce_code ctxt all_public cs target_name some_width some_module_name args = let @@ -501,16 +520,18 @@ val program = Code_Thingol.consts_program ctxt cs; in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end; -fun check_code ctxt all_public cs seris = +fun check_code all_public cs seris thy = let - val program = Code_Thingol.consts_program ctxt cs; - val _ = map (fn ((target_name, strict), args) => - check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris; - in () end; + val thy_ctxt = Proof_Context.init_global thy; + val program = Code_Thingol.consts_program thy_ctxt cs; + in + (seris, thy) |-> fold (fn ((target_name, strict), args) => + check_code_for target_name strict args program all_public (map Constant cs)) + end; -fun check_code_cmd all_public raw_cs seris ctxt = - check_code ctxt all_public - (Code_Thingol.read_const_exprs ctxt raw_cs) seris; +fun check_code_cmd all_public raw_cs seris thy = + let val thy_ctxt = Proof_Context.init_global thy + in check_code all_public (Code_Thingol.read_const_exprs thy_ctxt raw_cs) seris thy end; (** serializer configuration **) @@ -683,8 +704,7 @@ val _ = Outer_Syntax.command \<^command_keyword>\export_code\ "generate executable code for constants" (Scan.optional (\<^keyword>\open\ >> K true) false -- Scan.repeat1 Parse.term - :|-- (fn args => (code_expr_checkingP args || code_expr_inP args)) - >> (fn f => Toplevel.keep (f o Toplevel.context_of))); + :|-- (fn args => (code_expr_checkingP args || code_expr_inP args)) >> Toplevel.theory); end;