# HG changeset patch # User wenzelm # Date 1193421512 -7200 # Node ID 36cf92f63a4435a6e1d4bbd582be09516c3f9e52 # Parent e5b2dd8db7c88a060ebde6366519c07080ac13ec replaced Secure.evaluate by ML_Context.evaluate; diff -r e5b2dd8db7c8 -r 36cf92f63a44 src/Pure/General/secure.ML --- 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; diff -r e5b2dd8db7c8 -r 36cf92f63a44 src/Pure/ML/ml_context.ML --- 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 *) diff -r e5b2dd8db7c8 -r 36cf92f63a44 src/Tools/code/code_target.ML --- 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; diff -r e5b2dd8db7c8 -r 36cf92f63a44 src/Tools/nbe.ML --- 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 *)