src/Tools/Code/code_runtime.ML
changeset 39912 2ffe7060ca75
parent 39816 c7cec137c48a
child 39913 721ba2c1a799
     1.1 --- a/src/Tools/Code/code_runtime.ML	Fri Oct 01 17:06:49 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Oct 01 17:06:49 2010 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  signature CODE_RUNTIME =
     1.5  sig
     1.6    val target: string
     1.7 +  val value: Proof.context ->
     1.8 +    (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
     1.9 +    string * string -> 'a
    1.10    type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
    1.11    val dynamic_value: 'a cookie -> theory -> string option
    1.12      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
    1.13 @@ -56,6 +59,19 @@
    1.14    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]));
    1.15         (*avoid further pervasive infix names*)
    1.16  
    1.17 +fun exec verbose code =
    1.18 +  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false code);
    1.19 +
    1.20 +fun value ctxt (get, put, put_ml) (prelude, value) =
    1.21 +  let
    1.22 +    val code = (prelude
    1.23 +      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    1.24 +      ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
    1.25 +    val ctxt' = ctxt
    1.26 +      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.27 +      |> Context.proof_map (exec false code);
    1.28 +  in get ctxt' () end;
    1.29 +
    1.30  
    1.31  (* evaluation into target language values *)
    1.32  
    1.33 @@ -85,7 +101,7 @@
    1.34      val (program_code, [SOME value_name']) = serializer naming program' [value_name];
    1.35      val value_code = space_implode " "
    1.36        (value_name' :: "()" :: map (enclose "(" ")") args);
    1.37 -  in Exn.capture (ML_Context.value ctxt cookie) (program_code, value_code) end;
    1.38 +  in Exn.capture (value ctxt cookie) (program_code, value_code) end;
    1.39  
    1.40  fun partiality_as_none e = SOME (Exn.release e)
    1.41    handle General.Match => NONE
    1.42 @@ -276,20 +292,19 @@
    1.43  fun add_eval_const (const, const') = Code_Target.add_const_syntax target
    1.44    const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')));
    1.45  
    1.46 -fun process_reflection (code_body, (tyco_map, (constr_map, const_map))) module_name NONE thy =
    1.47 +fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
    1.48        thy
    1.49        |> Code_Target.add_reserved target module_name
    1.50 -      |> Context.theory_map
    1.51 -        (ML_Context.exec (fn () => ML_Context.eval_text true Position.none code_body))
    1.52 +      |> Context.theory_map (exec true code)
    1.53        |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
    1.54        |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
    1.55        |> fold (add_eval_const o apsnd Code_Printer.str) const_map
    1.56 -  | process_reflection (code_body, _) _ (SOME file_name) thy =
    1.57 +  | process_reflection (code, _) _ (SOME file_name) thy =
    1.58        let
    1.59          val preamble =
    1.60            "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
    1.61            ^ "; DO NOT EDIT! *)";
    1.62 -        val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
    1.63 +        val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
    1.64        in
    1.65          thy
    1.66        end;
    1.67 @@ -395,9 +410,10 @@
    1.68      val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
    1.69      val _ = Secure.use_text notifying_context
    1.70        (0, Path.implode filepath) false (File.read filepath);
    1.71 -    val thy'' = (Context.the_theory o the) (Context.thread_data ())
    1.72 -    val names = Loaded_Values.get thy''
    1.73 -  in (names, thy'') end;
    1.74 +    val thy'' = (Context.the_theory o the) (Context.thread_data ());
    1.75 +    val names = Loaded_Values.get thy'';
    1.76 +    val thy''' = Thy_Load.provide_file filepath thy'';
    1.77 +  in (names, thy''') end;
    1.78  
    1.79  end;
    1.80  
    1.81 @@ -407,7 +423,8 @@
    1.82    |> Specification.axiomatization [(b, SOME T, NoSyn)] []
    1.83    |-> (fn ([Const (const, _)], _) =>
    1.84       Code_Target.add_const_syntax target const
    1.85 -       (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))));
    1.86 +       (SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))
    1.87 +  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" []));
    1.88  
    1.89  fun process_file filepath (definienda, thy) =
    1.90    let