Quelle generated_files.ML Sprache: SML

(*  Title:      Pure/Tools/generated_files.ML
    Author:     Makarius

Generated source files for other languages: with antiquotations, without Isabelle symbols.
*)

signature GENERATED_FILES =
sig
  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
  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 * 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
  val export_file: theory -> file -> unit
  type file_type =
    {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
  val file_type:
    binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
    theory -> theory
  val antiquotation: binding -> 'a Token.context_parser ->
    ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
    theory -> theory
  val set_string: string -> Proof.context -> Proof.context
  val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
  val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
  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 check_external_files: Proof.context ->
    Input.source list * Input.source -> Path.T list * Path.T
  val get_external_files: Path.T -> Path.T list * Path.T -> unit
  val scala_build_generated_files: Proof.context -> (Path.binding list * theory) list ->
    (Path.T list * Path.T) list -> unit
  val scala_build_generated_files_cmd: Proof.context ->
    ((string * Position.T) list * (string * Position.T) option) list ->
    (Input.source list * Input.source) 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.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 ->
    (Input.source list * Input.source) list ->
    ((string * Position.T) list * bool option) list ->
    string * Position.T -> Input.source -> unit
  val execute: Path.T -> Input.source -> string -> string
end;

structure Generated_Files: GENERATED_FILES =
struct

(** context data **)

type file = Path.T * (Position.T * Bytes.T);

type file_type =
  {name: string, ext: string, make_comment: string -> string, make_string: string -> string};

type antiquotation = Token.src -> Proof.context -> file_type -> string;

fun err_dup_files path pos pos' =
  error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']);

structure Data = Theory_Data
(
  type T =
    file list Symtab.table *  (*files for named theory*)
    file_type Name_Space.table *  (*file types*)
    antiquotation Name_Space.table;  (*antiquotations*)
  val empty =
    (Symtab.empty,
     Name_Space.empty_table Markup.file_typeN,
     Name_Space.empty_table Markup.antiquotationN);
  fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
    let
      val files' =
        (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;
);

fun lookup_files thy =
  Symtab.lookup_list (#1 (Data.get thy)) (Context.theory_long_name thy);

fun update_files thy_files' thy =
  (Data.map o @{apply 3(1)}) (Symtab.update (Context.theory_long_name thy, thy_files')) thy;

fun add_files (binding, content) thy =
  let
    val _ = Path.proper_binding binding;
    val (path, pos) = Path.dest_binding binding;
    val thy_files = lookup_files thy;
    val thy_files' =
      (case AList.lookup (op =) thy_files path of
        SOME (pos', _) => err_dup_files path pos pos'
      | NONE => (path, (pos, content)) :: thy_files);
  in update_files thy_files' thy end;

(* get files *)

type file = {path: Path.T, pos: Position.T, content: Bytes.T};

fun file_binding (file: file) = Path.binding (#path file, #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 =
  lookup_files thy |> rev |> map (fn (path, (pos, content)) =>
    {path = path, pos = pos, content = content}: file);

fun get_file thy binding =
  let val (path, pos) = Path.dest_binding binding in
    (case find_first (fn file => #path file = path) (get_files thy) of
      SOME file => file
    | NONE =>
        error ("Missing generated file " ^ Path.print path ^
          " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
  end;

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 *)

fun check_files_in ctxt (files, opt_thy) =
  let
    val thy =
      (case opt_thy of
        SOME name => Theory.check {long = false} ctxt name
      | NONE => Proof_Context.theory_of ctxt);
  in (map Path.explode_binding files, thy) end;

fun write_file dir (file: file) =
  let
    val path = Path.expand (dir + #path file);
    val _ = Isabelle_System.make_directory (Path.dir path);
    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) (Bytes.contents_blob (#content file));

(* file types *)

fun get_file_type thy ext =
  if ext = "" then error "Bad file extension"
  else
    (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
      (fn (_, file_type) => fn res =>
        if #ext file_type = ext then SOME file_type else res)
    |> (fn SOME file_type => file_type
         | NONE => error ("Unknown file type for extension " ^ quote ext));

fun file_type binding {ext, make_comment, make_string} thy =
  let
    val name = Binding.name_of binding;
    val pos = Binding.pos_of binding;
    val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};

    val table = #2 (Data.get thy);
    val space = Name_Space.space_of_table table;
    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
    val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);

    val _ =
      (case try (#name o get_file_type thy) ext of
        NONE => ()
      | SOME name' =>
          error ("Extension " ^ quote ext ^ " already registered for file type " ^
            quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
  in thy |> (Data.map o @{apply 3(2)}) (K data') end;

(* antiquotations *)

val get_antiquotations = #3 o Data.get o Proof_Context.theory_of;

fun antiquotation name scan body thy =
  let
    fun ant src ctxt file_type : string =
      let val (x, ctxt') = Token.syntax scan src ctxt
      in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
  in
    thy
    |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
  end;

val scan_antiq =
  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
  Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);

fun read_source ctxt (file_type: file_type) source =
  let
    val _ =
      Context_Position.report ctxt (Input.pos_of source)
        (Markup.language
          {name = #name file_type, symbols = false, antiquotes = true,
            delimited = Input.is_delimited source});

    val (input, _) =
      Input.source_explode source
      |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));

    val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);

    fun expand antiq =
      (case antiq of
        Antiquote.Text s => s
      | Antiquote.Control {name, body, ...} =>
          let
            val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
            val (src', ant) = Token.check_src ctxt get_antiquotations src;
          in ant src' ctxt file_type end
      | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
  in implode (map expand input) end;

(** Isar commands **)

(* generate_file *)

fun generate_file (binding, source) lthy =
  let
    val thy = Proof_Context.theory_of lthy;

    val (path, pos) = Path.dest_binding binding;
    val file_type =
      get_file_type thy (Path.get_ext path)
        handle ERROR msg => error (msg ^ Position.here pos);

    val header = #make_comment file_type " generated by Isabelle ";
    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 =
  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 map #1 (maps get_files_in args) of
      [] => ()
    | files =>
       (List.app (export_file thy) files;
        writeln (Export.message thy Path.current);
        writeln (cat_lines (map (prefix " " o print_file) files))))
  end;

fun export_generated_files_cmd ctxt args =
  export_generated_files ctxt (map (check_files_in ctxt) args);

(* external files *)

fun check_external_files ctxt (raw_files, raw_base_dir) =
  let
    val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
    val files = raw_files |> map (fn source =>
     (Resources.check_file ctxt (SOME base_dir) source;
      Path.explode (Input.string_of source)));
  in (files, base_dir) end;

fun get_external_files dir (files, base_dir) =
  files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir);

(* scala_build_generated_files *)

fun scala_build_generated_files ctxt args external =
  Isabelle_System.with_tmp_dir "scala_build" (fn dir =>
    let
      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 _ = List.app (get_external_files dir) external;
      val [jar_name, jar_bytes, output] =
        \<^scala>\<open>scala_build\<close> [Bytes.string (Isabelle_System.absolute_path dir)];
      val _ = writeln (Bytes.content output);
    in
      Export.export (Proof_Context.theory_of ctxt)
        (Path.explode_binding0 (Bytes.content jar_name))
        (Bytes.contents_blob jar_bytes)
    end);

fun scala_build_generated_files_cmd ctxt args external =
  scala_build_generated_files ctxt
    (map (check_files_in ctxt) args)
    (map (check_external_files ctxt) external)

(* 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 _ = List.app (get_external_files dir) external;
      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 binding0 =>
            let
              val binding = binding0
                |> Path.map_binding (executable = SOME true ? Path.platform_exe);
              val (path, pos) = Path.dest_binding binding;
              val content =
                (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 (Context.Theory thy) (Context.theory_long_name 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 (check_external_files ctxt) external)
    ((map o apfst o map) Path.explode_binding export)
    (Path.explode_binding export_prefix)
    source;

(* execute compiler -- auxiliary *)

fun execute dir title compile =
  Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir)
  |> Process_Result.check
  |> Process_Result.out
    handle ERROR msg =>
      let val (s, pos) = Input.source_content title
      in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;

(** concrete file types **)

val _ =
  Theory.setup
    (file_type \<^binding>\<open>Haskell\<close>
      {ext = "hs",
       make_comment = enclose "{-" "-}",
       make_string = GHC.print_string} #>
     file_type \<^binding>\<open>Java\<close>
      {ext = "java",
       make_comment = enclose "/*" "*/",
       make_string = Java.print_string} #>
     file_type \<^binding>\<open>Scala\<close>
      {ext = "scala",
       make_comment = enclose "/*" "*/",
       make_string = Java.print_string} #>
     file_type \<^binding>\<open>Properties\<close>
      {ext = "props",
       make_comment = enclose "#" "",
       make_string = I});

(** concrete antiquotations **)

(* ML expression as string literal *)

structure Local_Data = Proof_Data
(
  type T = string option;
  fun init _ = NONE;
);

val set_string = Local_Data.put o SOME;

fun the_string ctxt =
  (case Local_Data.get ctxt of
    SOME s => s
  | NONE => raise Fail "No result string");

val _ =
  Theory.setup
    (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
      (fn {context = ctxt, file_type, argument, ...} =>
        ctxt |> Context.proof_map
          (ML_Context.expression (Input.pos_of argument)
            (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
             ML_Lex.read_source argument @ ML_Lex.read "))"))
        |> the_string |> #make_string file_type));

(* file-system paths *)

fun path_antiquotation binding check =
  antiquotation binding
    (Args.context -- Scan.lift Parse.path_input >>
      (fn (ctxt, source) => (check ctxt (SOME Path.current) source |> Path.implode)))
    (fn {file_type, argument, ...} => #make_string file_type argument);

val _ =
  Theory.setup
   (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
    path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
    path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);

end;

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.17Bemerkung: (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.