--- a/src/Pure/General/secure.ML Fri Oct 26 17:55:33 2007 +0200
+++ b/src/Pure/General/secure.ML Fri Oct 26 19:58:32 2007 +0200
@@ -10,8 +10,6 @@
val set_secure: unit -> unit
val is_secure: unit -> bool
val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
- val evaluate: string * (unit -> 'a) option ref -> string
- -> (string -> unit) * (string -> 'b) -> bool -> string -> 'a
val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
val use_noncritical: string -> unit
val use: string -> unit
@@ -45,18 +43,6 @@
fun use_text name pr verbose txt = NAMED_CRITICAL "ML" (fn () =>
(secure_mltext (); orig_use_text name pr verbose txt));
-(* compiler invocation as evaluation *)
-fun evaluate (ref_name, reff) name pr verbose txt = NAMED_CRITICAL name (fn () =>
- let
- val _ = secure_mltext ();
- val txt' = "val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))";
- val _ = reff := NONE;
- val _ = orig_use_text name pr verbose txt';
- in case !reff
- of NONE => error ("evaluate (" ^ ref_name ^ ")")
- | SOME f => f
- end) ();
-
fun use_file pr verbose name = NAMED_CRITICAL "ML" (fn () =>
(secure_mltext (); orig_use_file pr verbose name));
@@ -83,7 +69,6 @@
(*override previous toplevel bindings!*)
val use_text = Secure.use_text;
-val evaluate = Secure.evaluate;
val use_file = Secure.use_file;
fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
val execute = Secure.execute;
--- a/src/Pure/ML/ml_context.ML Fri Oct 26 17:55:33 2007 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Oct 26 19:58:32 2007 +0200
@@ -10,7 +10,7 @@
val the_context: unit -> theory
val thm: xstring -> thm
val thms: xstring -> thm list
-end;
+end
signature ML_CONTEXT =
sig
@@ -37,7 +37,9 @@
val use_mltext_update: string -> bool -> Context.generic -> Context.generic
val use_let: string -> string -> string -> Context.generic -> Context.generic
val use: Path.T -> unit
-end;
+ val evaluate: (string -> unit) * (string -> 'b) -> bool ->
+ string * (unit -> 'a) option ref -> string -> 'a
+end
structure ML_Context: ML_CONTEXT =
struct
@@ -162,30 +164,31 @@
|> #1 |> split_list |> pairself implode;
in (isabelle_struct decls, body) end);
-fun eval name verbose txt = use_text name Output.ml_output verbose txt;
-
in
val eval_antiquotes_fn = ref eval_antiquotes;
val trace = ref false;
-fun eval_wrapper name verbose txt =
+fun eval_wrapper name pr verbose txt =
let
- val (txt1, txt2) = ! eval_antiquotes_fn txt;
+ val (txt1, txt2) = ! eval_antiquotes_fn txt; (* FIXME tmp hook *)
val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
+ fun eval nm = use_text nm pr;
in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
+fun ML_wrapper pr = eval_wrapper "ML" pr;
+
end;
(* ML evaluation *)
fun use_mltext txt verbose opt_context =
- setmp opt_context (fn () => eval_wrapper "ML" verbose txt) ();
+ setmp opt_context (fn () => ML_wrapper Output.ml_output verbose txt) ();
fun use_mltext_update txt verbose context =
- #2 (pass_context context (eval_wrapper "ML" verbose) txt);
+ #2 (pass_context context (ML_wrapper Output.ml_output verbose) txt);
fun use_context txt = use_mltext_update
("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
@@ -193,7 +196,13 @@
fun use_let bind body txt =
use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
-fun use path = eval_wrapper (Path.implode path) true (File.read path);
+fun use path = eval_wrapper (Path.implode path) Output.ml_output true (File.read path);
+
+fun evaluate pr verbose (ref_name, r) txt = CRITICAL (fn () =>
+ let
+ val _ = r := NONE;
+ val _ = ML_wrapper pr verbose ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))");
+ in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
(* basic antiquotations *)
--- a/src/Tools/code/code_target.ML Fri Oct 26 17:55:33 2007 +0200
+++ b/src/Tools/code/code_target.ML Fri Oct 26 19:58:32 2007 +0200
@@ -1709,7 +1709,7 @@
val code' = CodeThingol.add_value_stmt (t, ty) code;
val label = "evaluation in SML";
fun eval () = (seri (SOME [CodeName.value_name]) code';
- evaluate (ref_name, reff) label Output.ml_output (!eval_verbose) val_args);
+ ML_Context.evaluate Output.ml_output (!eval_verbose) (ref_name, reff) val_args);
in NAMED_CRITICAL label eval end;
--- a/src/Tools/nbe.ML Fri Oct 26 17:55:33 2007 +0200
+++ b/src/Tools/nbe.ML Fri Oct 26 19:58:32 2007 +0200
@@ -10,7 +10,7 @@
val norm_conv: cterm -> thm
val norm_term: theory -> term -> term
- datatype Univ =
+ datatype Univ =
Const of string * Univ list (*named (uninterpreted) constants*)
| Free of string * Univ list
| DFree of string (*free (uninterpreted) dictionary parameters*)
@@ -21,7 +21,7 @@
val abs: int -> (Univ list -> Univ) -> Univ
(*abstractions as closures*)
- val univs_ref: (unit -> Univ list -> Univ list) option ref
+ val univs_ref: (unit -> Univ list -> Univ list) option ref
val trace: bool ref
val setup: theory -> theory
end;
@@ -55,7 +55,7 @@
and the number of arguments we're still waiting for.
*)
-datatype Univ =
+datatype Univ =
Const of string * Univ list (*named (uninterpreted) constants*)
| Free of string * Univ list (*free variables*)
| DFree of string (*free (uninterpreted) dictionary parameters*)
@@ -145,12 +145,12 @@
val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
-val compile =
+val compile =
tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
- #> evaluate ("Nbe.univs_ref", univs_ref) "normalization by evaluation"
+ #> ML_Context.evaluate
(Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
- (!trace);
+ (!trace) ("Nbe.univs_ref", univs_ref);
(* code generation with greetings to Tarski *)