src/Pure/Tools/generated_files.ML
author wenzelm
Sat Feb 02 15:52:14 2019 +0100 (4 months ago)
changeset 69784 24bbc4e30e5b
parent 69662 fd86ed39aea4
child 70012 36aeb535a801
permissions -rw-r--r--
clarified signature: Path.T as in Generated_Files;
     1 (*  Title:      Pure/Tools/generated_files.ML
     2     Author:     Makarius
     3 
     4 Generated source files for other languages: with antiquotations, without Isabelle symbols.
     5 *)
     6 
     7 signature GENERATED_FILES =
     8 sig
     9   val add_files: (Path.T * Position.T) * string -> theory -> theory
    10   val get_files: theory -> {path: Path.T, pos: Position.T, text: string} list
    11   val write_files: theory -> Path.T -> (Path.T * Position.T) list
    12   val export_files: theory -> theory list -> (Path.T * Position.T) list
    13   type file_type =
    14     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
    15   val file_type:
    16     binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
    17     theory -> theory
    18   val antiquotation: binding -> 'a Token.context_parser ->
    19     ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
    20     theory -> theory
    21   val set_string: string -> Proof.context -> Proof.context
    22   val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
    23 end;
    24 
    25 structure Generated_Files: GENERATED_FILES =
    26 struct
    27 
    28 (** context data **)
    29 
    30 type file_type =
    31   {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
    32 
    33 type antiquotation = Token.src -> Proof.context -> file_type -> string;
    34 
    35 structure Data = Theory_Data
    36 (
    37   type T =
    38     (Path.T * (Position.T * string)) list *  (*files for current theory*)
    39     file_type Name_Space.table *  (*file types*)
    40     antiquotation Name_Space.table;  (*antiquotations*)
    41   val empty =
    42     ([],
    43      Name_Space.empty_table Markup.file_typeN,
    44      Name_Space.empty_table Markup.antiquotationN);
    45   val extend = @{apply 3(1)} (K []);
    46   fun merge ((_, types1, antiqs1), (_, types2, antiqs2)) =
    47     ([],
    48      Name_Space.merge_tables (types1, types2),
    49      Name_Space.merge_tables (antiqs1, antiqs2));
    50 );
    51 
    52 
    53 (* files *)
    54 
    55 fun add_files ((path0, pos), text) =
    56   let
    57     val path = Path.expand path0;
    58     fun err msg ps = error (msg ^ ": " ^ Path.print path ^ Position.here_list ps);
    59     val _ =
    60       if Path.is_absolute path then err "Illegal absolute path" [pos]
    61       else if Path.has_parent path then err "Illegal parent path" [pos]
    62       else ();
    63   in
    64     (Data.map o @{apply 3(1)}) (fn files =>
    65       (case AList.lookup (op =) files path of
    66         SOME (pos', _) => err "Duplicate generated file" [pos, pos']
    67       | NONE => (path, (pos, text)) :: files))
    68   end;
    69 
    70 val get_files =
    71   map (fn (path, (pos, text)) => {path = path, pos = pos, text = text}) o rev o #1 o Data.get;
    72 
    73 fun write_files thy dir =
    74   get_files thy |> map (fn {path, pos, text} =>
    75     let
    76       val path' = Path.expand (Path.append dir path);
    77       val _ = Isabelle_System.mkdirs (Path.dir path');
    78       val _ = File.generate path' text;
    79     in (path, pos) end);
    80 
    81 fun export_files thy other_thys =
    82   other_thys |> maps (fn other_thy =>
    83     get_files other_thy |> map (fn {path, pos, text} =>
    84       (Export.export thy path [text]; (path, pos))));
    85 
    86 
    87 (* file types *)
    88 
    89 fun the_file_type thy ext =
    90   if ext = "" then error "Bad file extension"
    91   else
    92     (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
    93       (fn (_, file_type) => fn res =>
    94         if #ext file_type = ext then SOME file_type else res)
    95     |> (fn SOME file_type => file_type
    96          | NONE => error ("Unknown file type for extension " ^ quote ext));
    97 
    98 fun file_type binding {ext, make_comment, make_string} thy =
    99   let
   100     val name = Binding.name_of binding;
   101     val pos = Binding.pos_of binding;
   102     val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
   103 
   104     val table = #2 (Data.get thy);
   105     val space = Name_Space.space_of_table table;
   106     val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
   107     val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
   108 
   109     val _ =
   110       (case try (#name o the_file_type thy) ext of
   111         NONE => ()
   112       | SOME name' =>
   113           error ("Extension " ^ quote ext ^ " already registered for file type " ^
   114             quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
   115   in thy |> (Data.map o @{apply 3(2)}) (K data') end;
   116 
   117 
   118 (* antiquotations *)
   119 
   120 val get_antiquotations = #3 o Data.get o Proof_Context.theory_of;
   121 
   122 fun antiquotation name scan body thy =
   123   let
   124     fun ant src ctxt file_type : string =
   125       let val (x, ctxt') = Token.syntax scan src ctxt
   126       in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
   127   in
   128     thy
   129     |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
   130   end;
   131 
   132 val scan_antiq =
   133   Antiquote.scan_control >> Antiquote.Control ||
   134   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
   135 
   136 fun read_source ctxt (file_type: file_type) source =
   137   let
   138     val _ =
   139       Context_Position.report ctxt (Input.pos_of source)
   140         (Markup.language
   141           {name = #name file_type, symbols = false, antiquotes = true,
   142             delimited = Input.is_delimited source});
   143 
   144     val (input, _) =
   145       Input.source_explode source
   146       |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
   147 
   148     val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
   149 
   150     fun expand antiq =
   151       (case antiq of
   152         Antiquote.Text s => s
   153       | Antiquote.Control {name, body, ...} =>
   154           let
   155             val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
   156             val (src', ant) = Token.check_src ctxt get_antiquotations src;
   157           in ant src' ctxt file_type end
   158       | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
   159   in implode (map expand input) end;
   160 
   161 
   162 (* generate files *)
   163 
   164 fun generate_file_cmd ((file, pos), source) lthy =
   165   let
   166     val thy = Proof_Context.theory_of lthy;
   167 
   168     val path = Path.explode file;
   169     val file_type =
   170       the_file_type thy (#2 (Path.split_ext path))
   171         handle ERROR msg => error (msg ^ Position.here pos);
   172 
   173     val header = #make_comment file_type " generated by Isabelle ";
   174     val text = header ^ "\n" ^ read_source lthy file_type source;
   175   in lthy |> (Local_Theory.background_theory o add_files) ((path, pos), text) end;
   176 
   177  
   178 
   179 (** concrete file types **)
   180 
   181 val _ =
   182   Theory.setup
   183     (file_type \<^binding>\<open>Haskell\<close>
   184       {ext = "hs",
   185        make_comment = enclose "{-" "-}",
   186        make_string = GHC.print_string});
   187 
   188 
   189 
   190 (** concrete antiquotations **)
   191 
   192 (* ML expression as string literal *)
   193 
   194 structure Local_Data = Proof_Data
   195 (
   196   type T = string option;
   197   fun init _ = NONE;
   198 );
   199 
   200 val set_string = Local_Data.put o SOME;
   201 
   202 fun the_string ctxt =
   203   (case Local_Data.get ctxt of
   204     SOME s => s
   205   | NONE => raise Fail "No result string");
   206 
   207 val _ =
   208   Theory.setup
   209     (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
   210       (fn {context = ctxt, file_type, argument, ...} =>
   211         ctxt |> Context.proof_map
   212           (ML_Context.expression (Input.pos_of argument)
   213             (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
   214              ML_Lex.read_source argument @ ML_Lex.read "))"))
   215         |> the_string |> #make_string file_type));
   216 
   217 
   218 (* file-system paths *)
   219 
   220 fun path_antiquotation binding check =
   221   antiquotation binding
   222     (Args.context -- Scan.lift (Parse.position Parse.path) >>
   223       (fn (ctxt, (name, pos)) => (check ctxt Path.current (name, pos) |> Path.implode)))
   224     (fn {file_type, argument, ...} => #make_string file_type argument);
   225 
   226 val _ =
   227   Theory.setup
   228    (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
   229     path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
   230     path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
   231 
   232 end;