'code_reflect' only supports new-style 'file_prefix';
authorwenzelm
Mon Apr 01 21:58:45 2019 +0200 (5 months ago)
changeset 7002249e178cbf923
parent 70021 e6e634836556
child 70023 5aef4e9966c4
'code_reflect' only supports new-style 'file_prefix';
avoid fragile file "$ISABELLE_TMP/rat.ML";
NEWS
src/Doc/Codegen/Further.thy
src/Doc/Isar_Ref/HOL_Specific.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Mon Apr 01 21:51:46 2019 +0200
     1.2 +++ b/NEWS	Mon Apr 01 21:58:45 2019 +0200
     1.3 @@ -148,6 +148,10 @@
     1.4  has been discontinued already: it is superseded by the file-browser in
     1.5  Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Command 'code_reflect' no longer supports the 'file' argument: it has
     1.8 +been superseded by 'file_prefix' for stateless file management as in
     1.9 +'export_code'. Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Code generation for OCaml: proper strings are used for literals.
    1.12  Minor INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/Doc/Codegen/Further.thy	Mon Apr 01 21:51:46 2019 +0200
     2.2 +++ b/src/Doc/Codegen/Further.thy	Mon Apr 01 21:58:45 2019 +0200
     2.3 @@ -48,7 +48,7 @@
     2.4    functions Fract
     2.5      "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     2.6      "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     2.7 -  file "$ISABELLE_TMP/rat.ML"
     2.8 +  file_prefix rat
     2.9  
    2.10  text \<open>
    2.11    \noindent This merely generates the referenced code to the given
     3.1 --- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Apr 01 21:51:46 2019 +0200
     3.2 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Apr 01 21:58:45 2019 +0200
     3.3 @@ -2367,7 +2367,7 @@
     3.4      ;
     3.5      @@{command (HOL) code_reflect} @{syntax string} \<newline>
     3.6        (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \<newline>
     3.7 -      (@'functions' (@{syntax string} +))? (@'file' @{syntax path})?
     3.8 +      (@'functions' (@{syntax string} +))? (@'file_prefix' @{syntax path})?
     3.9      ;
    3.10      @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
    3.11      ;
    3.12 @@ -2485,12 +2485,13 @@
    3.13    the discretion of the user to ensure that name prefixes of identifiers in
    3.14    compound statements like type classes or datatypes are still the same.
    3.15  
    3.16 -  \<^descr> @{command (HOL) "code_reflect"} without a ``\<open>file\<close>'' argument compiles
    3.17 -  code into the system runtime environment and modifies the code generator
    3.18 -  setup that future invocations of system runtime code generation referring to
    3.19 -  one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use these precompiled
    3.20 -  entities. With a ``\<open>file\<close>'' argument, the corresponding code is generated
    3.21 -  into that specified file without modifying the code generator setup.
    3.22 +  \<^descr> @{command (HOL) "code_reflect"} without a ``\<^theory_text>\<open>file_prefix\<close>'' argument
    3.23 +  compiles code into the system runtime environment and modifies the code
    3.24 +  generator setup that future invocations of system runtime code generation
    3.25 +  referring to one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use
    3.26 +  these precompiled entities. With a ``\<^theory_text>\<open>file_prefix\<close>'' argument, the
    3.27 +  corresponding code is generated/exported to the specified file (as for
    3.28 +  \<^theory_text>\<open>export_code\<close>) without modifying the code generator setup.
    3.29  
    3.30    \<^descr> @{command (HOL) "code_pred"} creates code equations for a predicate given
    3.31    a set of introduction rules. Optional mode annotations determine which
     4.1 --- a/src/Tools/Code/code_runtime.ML	Mon Apr 01 21:51:46 2019 +0200
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Mon Apr 01 21:58:45 2019 +0200
     4.3 @@ -19,7 +19,9 @@
     4.4      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
     4.5    val dynamic_holds_conv: Proof.context -> conv
     4.6    val code_reflect: (string * string list option) list -> string list -> string
     4.7 -    -> string option -> theory -> theory
     4.8 +    -> Path.binding option -> theory -> theory
     4.9 +  val code_reflect_cmd: (string * string list option) list -> string list -> string
    4.10 +    -> Path.binding option -> theory -> theory
    4.11    datatype truth = Holds
    4.12    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
    4.13    val mount_computation: Proof.context -> (string * typ) list -> typ
    4.14 @@ -711,18 +713,18 @@
    4.15        |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
    4.16        |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
    4.17        |> fold (add_eval_const o apsnd Code_Printer.str) const_map
    4.18 -  | process_reflection (code, _) _ (SOME file_name) thy =
    4.19 +  | process_reflection (code, _) _ (SOME binding) thy =
    4.20        let
    4.21 +        val code_binding = Path.map_binding Code_Target.code_path binding;
    4.22          val preamble =
    4.23            "(* Generated from " ^
    4.24              Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
    4.25            "; DO NOT EDIT! *)";
    4.26 -        val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
    4.27 -      in
    4.28 -        thy
    4.29 -      end;
    4.30 +        val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy;
    4.31 +        val _ = Code_Target.code_export_message thy';
    4.32 +      in thy' end;
    4.33  
    4.34 -fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
    4.35 +fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name file_prefix thy =
    4.36    let
    4.37      val ctxt = Proof_Context.init_global thy;
    4.38      val datatypes = map (fn (raw_tyco, raw_cos) =>
    4.39 @@ -736,7 +738,7 @@
    4.40        |> (apsnd o apsnd) (chop (length constrs));
    4.41    in
    4.42      thy
    4.43 -    |> process_reflection result module_name some_file
    4.44 +    |> process_reflection result module_name file_prefix
    4.45    end;
    4.46  
    4.47  val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
    4.48 @@ -780,9 +782,11 @@
    4.49      (Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
    4.50        ::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
    4.51      -- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
    4.52 -    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.embedded)
    4.53 -    >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
    4.54 -      (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
    4.55 +    -- Scan.option (\<^keyword>\<open>file_prefix\<close> |-- Parse.!!! (Parse.position Parse.embedded))
    4.56 +    >> (fn (((module_name, raw_datatypes), raw_functions), file_prefix) =>
    4.57 +      Toplevel.theory (fn thy =>
    4.58 +        code_reflect_cmd raw_datatypes raw_functions module_name
    4.59 +          (Option.map Path.explode_binding file_prefix) thy)));
    4.60  
    4.61  end; (*local*)
    4.62