added command 'compile_generated_files';
authorwenzelm
Thu, 04 Apr 2019 14:30:58 +0200
changeset 70233 7a4dc1e60dc8
parent 70232 5b66e6672ccf
child 70234 a670d20c600d
added command 'compile_generated_files'; tuned signature;
src/Pure/Pure.thy
src/Pure/Thy/export.ML
src/Pure/Tools/generated_files.ML
--- a/src/Pure/Pure.thy	Thu Apr 04 14:29:49 2019 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 04 14:30:58 2019 +0200
@@ -23,6 +23,7 @@
   and "external_file" "bibtex_file" :: thy_load
   and "generate_file" :: thy_decl
   and "export_generated_files" :: diag
+  and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix"
   and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
   and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
   and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
@@ -126,6 +127,7 @@
       (Parse.path_binding -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
         >> Generated_Files.generate_file_cmd);
 
+
   val files_in =
     (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) --
       Scan.option (\<^keyword>\<open>in\<close> |-- Parse.!!! Parse.theory_name);
@@ -137,6 +139,28 @@
         Toplevel.keep (fn st =>
           Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args)))
 
+
+  val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false;
+
+  val executable =
+    \<^keyword>\<open>(\<close> |-- Parse.!!! (exe --| \<^keyword>\<open>)\<close>) >> SOME || Scan.succeed NONE;
+
+  val export_files = Scan.repeat1 Parse.path_binding -- executable;
+
+  val _ =
+    Outer_Syntax.command \<^command_keyword>\<open>compile_generated_files\<close>
+      "compile generated files and export results"
+      (Parse.and_list files_in --
+        Scan.optional (\<^keyword>\<open>external_files\<close> |--
+          Parse.!!! (Scan.repeat1 (Parse.position Parse.path))) [] --
+        Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
+        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("compiled", Position.none) --
+        (Parse.where_ |-- Parse.!!! Parse.ML_source)
+        >> (fn ((((args, external), export), export_prefix), source) =>
+          Toplevel.keep (fn st =>
+            Generated_Files.compile_generated_files_cmd
+              (Toplevel.context_of st) args external export export_prefix source)));
+
 in end\<close>
 
 
--- a/src/Pure/Thy/export.ML	Thu Apr 04 14:29:49 2019 +0200
+++ b/src/Pure/Thy/export.ML	Thu Apr 04 14:30:58 2019 +0200
@@ -6,6 +6,7 @@
 
 signature EXPORT =
 sig
+  val report_export: theory -> Path.binding -> unit
   type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool}
   val export_params: params -> string list -> unit
   val export: theory -> Path.binding -> string list -> unit
@@ -21,25 +22,24 @@
 
 (* export *)
 
+fun report_export thy binding =
+  let
+    val theory_name = Context.theory_long_name thy;
+    val (path, pos) = Path.dest_binding binding;
+    val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
+  in Context_Position.report_generic (Context.Theory thy) pos markup end;
+
 type params = {theory: theory, binding: Path.binding, executable: bool, compress: bool};
 
 fun export_params ({theory = thy, binding, executable, compress}: params) blob =
-  let
-    val theory_name = Context.theory_long_name thy;
-    val name = Path.implode_binding binding;
-    val (path, pos) = Path.dest_binding binding;
-    val _ =
-      Context_Position.report_generic (Context.Theory thy) pos
-        (Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path)));
-  in
-    (Output.try_protocol_message o Markup.export)
-     {id = Position.get_id (Position.thread_data ()),
-      serial = serial (),
-      theory_name = theory_name,
-      name = name,
-      executable = executable,
-      compress = compress} blob
-  end;
+ (report_export thy binding;
+  (Output.try_protocol_message o Markup.export)
+   {id = Position.get_id (Position.thread_data ()),
+    serial = serial (),
+    theory_name = Context.theory_long_name thy,
+    name = Path.implode_binding binding,
+    executable = executable,
+    compress = compress} blob);
 
 fun export thy binding blob =
   export_params {theory = thy, binding = binding, executable = false, compress = true} blob;
--- a/src/Pure/Tools/generated_files.ML	Thu Apr 04 14:29:49 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Apr 04 14:30:58 2019 +0200
@@ -9,10 +9,12 @@
   val add_files: Path.binding * string -> theory -> theory
   type file = {path: Path.T, pos: Position.T, content: string}
   val file_binding: file -> Path.binding
+  val file_markup: file -> Markup.T
   val print_file: file -> string
+  val report_file: Proof.context -> Position.T -> file -> unit
   val get_files: theory -> file list
   val get_file: theory -> Path.binding -> file
-  val get_files_in: Path.binding list * theory -> file list
+  val get_files_in: Path.binding list * theory -> (file * Position.T) list
   val check_files_in: Proof.context ->
     (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
   val write_file: Path.T -> file -> unit
@@ -31,6 +33,13 @@
   val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
   val export_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list -> unit
+  val with_compile_dir: (Path.T -> unit) -> unit
+  val compile_generated_files: Proof.context -> (Path.binding list * theory) list ->
+    Path.T list -> (Path.binding list * bool option) list -> Path.binding -> Input.source -> unit
+  val compile_generated_files_cmd: Proof.context ->
+    ((string * Position.T) list * (string * Position.T) option) list ->
+    (string * Position.T) list -> ((string * Position.T) list * bool option) list ->
+    string * Position.T -> Input.source -> unit
 end;
 
 structure Generated_Files: GENERATED_FILES =
@@ -76,9 +85,12 @@
 
 fun file_binding (file: file) = Path.binding (#path file, #pos file);
 
-fun print_file (file: file) =
-  quote (Path.implode (#path file))
-  |> Markup.markup (Markup.entityN, Position.def_properties_of (#pos file));
+fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file));
+
+fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file)));
+
+fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file);
+
 
 fun get_files thy =
   Data.get thy |> #1 |> rev |> map (fn (path, (pos, content)) =>
@@ -93,8 +105,9 @@
           " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
   end;
 
-fun get_files_in ([], thy) = get_files thy
-  | get_files_in (files, thy) = map (get_file thy) files;
+fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy)
+  | get_files_in (files, thy) =
+      map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files;
 
 
 (* check and output files *)
@@ -196,6 +209,8 @@
 
 (** Isar commands **)
 
+(* generate_file *)
+
 fun generate_file (binding, source) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -212,9 +227,12 @@
 fun generate_file_cmd (file, source) lthy =
   generate_file (Path.explode_binding file, source) lthy;
 
+
+(* export_generated_files *)
+
 fun export_generated_files ctxt args =
   let val thy = Proof_Context.theory_of ctxt in
-    (case maps get_files_in args of
+    (case map #1 (maps get_files_in args) of
       [] => ()
     | files =>
        (List.app (export_file thy) files;
@@ -224,7 +242,58 @@
 
 fun export_generated_files_cmd ctxt args =
   export_generated_files ctxt (map (check_files_in ctxt) args);
- 
+
+
+(* compile_generated_files *)
+
+val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
+
+fun with_compile_dir body : unit =
+  body (Path.explode (Config.get (Context.the_local_context ()) compile_dir));
+
+fun compile_generated_files ctxt args external export export_prefix source =
+  Isabelle_System.with_tmp_dir "compile" (fn dir =>
+    let
+      val thy = Proof_Context.theory_of ctxt;
+
+      val files = maps get_files_in args;
+      val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
+      val _ = List.app (write_file dir o #1) files;
+      val _ = external |> List.app (fn file => Isabelle_System.copy_file file dir);
+      val _ =
+        ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
+          ML_Compiler.flags (Input.pos_of source)
+          (ML_Lex.read "Generated_Files.with_compile_dir (" @
+            ML_Lex.read_source source @ ML_Lex.read ")");
+      val _ =
+        export |> List.app (fn (bindings, executable) =>
+          bindings |> List.app (fn binding =>
+            let
+              val (path, pos) = Path.dest_binding binding |>> executable = SOME true ? Path.exe;
+              val content =
+                (case try File.read (Path.append dir path) of
+                  SOME context => context
+                | 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' [content]
+            end));
+      val _ =
+        if null export then ()
+        else writeln (Export.message thy (Path.path_of_binding export_prefix));
+    in () end);
+
+fun compile_generated_files_cmd ctxt args external export export_prefix source =
+  compile_generated_files ctxt
+    (map (check_files_in ctxt) args)
+    (map (Resources.check_file ctxt NONE) external)
+    ((map o apfst o map) Path.explode_binding export)
+    (Path.explode_binding export_prefix)
+    source;
+
 
 
 (** concrete file types **)