# HG changeset patch # User haftmann # Date 1404057738 -7200 # Node ID 312660c1a70a34eed3126c18c2010035a19081b1 # Parent 6ea8b8592787fba8d26cbc6995f8cd69f27cf4f3 modernized diagnostic options diff -r 6ea8b8592787 -r 312660c1a70a src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sun Jun 29 18:30:24 2014 +0200 +++ b/src/Tools/Code/code_runtime.ML Sun Jun 29 18:02:18 2014 +0200 @@ -32,7 +32,7 @@ -> string option -> theory -> theory datatype truth = Holds val put_truth: (unit -> truth) -> Proof.context -> Proof.context - val trace: bool Unsynchronized.ref + val trace: bool Config.T val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory end; @@ -65,10 +65,10 @@ #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]); (*avoid further pervasive infix names*) -val trace = Unsynchronized.ref false; +val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false); -fun exec verbose code = - (if ! trace then tracing code else (); +fun exec ctxt verbose code = + (if Config.get ctxt trace then tracing code else (); ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)); fun value ctxt (get, put, put_ml) (prelude, value) = @@ -78,7 +78,7 @@ ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); val ctxt' = ctxt |> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) - |> Context.proof_map (exec false code); + |> Context.proof_map (exec ctxt false code); in get ctxt' () end; @@ -112,7 +112,7 @@ fun dynamic_value_exn cookie ctxt some_target postproc t args = let val _ = reject_vars ctxt t; - val _ = if ! trace + val _ = if Config.get ctxt trace then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) else () fun evaluator program _ vs_ty_t deps = @@ -313,7 +313,7 @@ fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = thy |> Code_Target.add_reserved target module_name - |> Context.theory_map (exec true code) + |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code) |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map |> fold (add_eval_const o apsnd Code_Printer.str) const_map diff -r 6ea8b8592787 -r 312660c1a70a src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun Jun 29 18:30:24 2014 +0200 +++ b/src/Tools/nbe.ML Sun Jun 29 18:02:18 2014 +0200 @@ -22,7 +22,7 @@ val same: Univ * Univ -> bool val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context - val trace: bool Unsynchronized.ref + val trace: bool Config.T val add_const_alias: thm -> theory -> theory end; @@ -32,8 +32,8 @@ (* generic non-sense *) -val trace = Unsynchronized.ref false; -fun traced f x = if !trace then (tracing (f x); x) else x; +val trace = Attrib.setup_config_bool @{binding "nbe_trace"} (K false); +fun traced ctxt f x = if Config.get ctxt trace then (tracing (f x); x) else x; (** certificates and oracle for "trivial type classes" **) @@ -263,9 +263,10 @@ fun nbe_apps t [] = t | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)]; fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts); -fun nbe_apps_constr idx_of c ts = +fun nbe_apps_constr ctxt idx_of c ts = let - val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" + val c' = if Config.get ctxt trace + then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)" else string_of_int (idx_of c); in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end; @@ -282,7 +283,7 @@ (* code generation *) -fun assemble_eqnss idx_of deps eqnss = +fun assemble_eqnss ctxt idx_of deps eqnss = let fun prep_eqns (c, (vs, eqns)) = let @@ -301,7 +302,7 @@ end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts' | NONE => if member (op =) deps sym then nbe_apps (nbe_fun idx_of 0 sym) ts' - else nbe_apps_constr idx_of sym ts' + else nbe_apps_constr ctxt idx_of sym ts' end and assemble_classrels classrels = fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels @@ -358,7 +359,8 @@ val match_cont = if Code_Symbol.is_value sym then NONE else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args)); val assemble_arg = assemble_iterm - (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE; + (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_") + dss @ ts)) NONE; val assemble_rhs = assemble_iterm assemble_constapp match_cont; val (samepairs, args') = subst_nonlin_vars args; val s_args = map assemble_arg args'; @@ -379,7 +381,7 @@ val eqns' = map_index (assemble_eqn sym dicts default_args) eqns @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym, [([ml_list (rev (dicts @ default_args))], - nbe_apps_constr idx_of sym (dicts @ default_args))])]); + nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]); in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end; val (fun_vars, fun_vals) = map_split assemble_eqns eqnss'; @@ -398,11 +400,11 @@ |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep))) |> AList.lookup (op =) |> (fn f => the o f); - val s = assemble_eqnss idx_of deps eqnss; + val s = assemble_eqnss ctxt idx_of deps eqnss; val cs = map fst eqnss; in s - |> traced (fn s => "\n--- code to be evaluated:\n" ^ s) + |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s) |> pair "" |> Code_Runtime.value ctxt univs_cookie |> (fn f => f deps_vals) @@ -549,11 +551,11 @@ in compile_term ctxt nbe_program deps (vs, t) |> term_of_univ ctxt idx_tab - |> traced (fn t => "Normalized:\n" ^ string_of_term t) + |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t) |> type_infer - |> traced (fn t => "Types inferred:\n" ^ string_of_term t) + |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t) |> check_tvars - |> traced (fn _ => "---\n") + |> traced ctxt (fn _ => "---\n") end;