modernized diagnostic options
authorhaftmann
Sun Jun 29 18:02:18 2014 +0200 (2014-06-29)
changeset 57435312660c1a70a
parent 57434 6ea8b8592787
child 57436 995f7ebd50ae
modernized diagnostic options
src/Tools/Code/code_runtime.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sun Jun 29 18:30:24 2014 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Jun 29 18:02:18 2014 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4      -> string option -> theory -> theory
     1.5    datatype truth = Holds
     1.6    val put_truth: (unit -> truth) -> Proof.context -> Proof.context
     1.7 -  val trace: bool Unsynchronized.ref
     1.8 +  val trace: bool Config.T
     1.9    val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -65,10 +65,10 @@
    1.13    #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
    1.14         (*avoid further pervasive infix names*)
    1.15  
    1.16 -val trace = Unsynchronized.ref false;
    1.17 +val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
    1.18  
    1.19 -fun exec verbose code =
    1.20 -  (if ! trace then tracing code else ();
    1.21 +fun exec ctxt verbose code =
    1.22 +  (if Config.get ctxt trace then tracing code else ();
    1.23    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
    1.24  
    1.25  fun value ctxt (get, put, put_ml) (prelude, value) =
    1.26 @@ -78,7 +78,7 @@
    1.27        ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
    1.28      val ctxt' = ctxt
    1.29        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    1.30 -      |> Context.proof_map (exec false code);
    1.31 +      |> Context.proof_map (exec ctxt false code);
    1.32    in get ctxt' () end;
    1.33  
    1.34  
    1.35 @@ -112,7 +112,7 @@
    1.36  fun dynamic_value_exn cookie ctxt some_target postproc t args =
    1.37    let
    1.38      val _ = reject_vars ctxt t;
    1.39 -    val _ = if ! trace
    1.40 +    val _ = if Config.get ctxt trace
    1.41        then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
    1.42        else ()
    1.43      fun evaluator program _ vs_ty_t deps =
    1.44 @@ -313,7 +313,7 @@
    1.45  fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
    1.46        thy
    1.47        |> Code_Target.add_reserved target module_name
    1.48 -      |> Context.theory_map (exec true code)
    1.49 +      |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code)
    1.50        |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
    1.51        |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
    1.52        |> fold (add_eval_const o apsnd Code_Printer.str) const_map
     2.1 --- a/src/Tools/nbe.ML	Sun Jun 29 18:30:24 2014 +0200
     2.2 +++ b/src/Tools/nbe.ML	Sun Jun 29 18:02:18 2014 +0200
     2.3 @@ -22,7 +22,7 @@
     2.4    val same: Univ * Univ -> bool
     2.5  
     2.6    val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
     2.7 -  val trace: bool Unsynchronized.ref
     2.8 +  val trace: bool Config.T
     2.9  
    2.10    val add_const_alias: thm -> theory -> theory
    2.11  end;
    2.12 @@ -32,8 +32,8 @@
    2.13  
    2.14  (* generic non-sense *)
    2.15  
    2.16 -val trace = Unsynchronized.ref false;
    2.17 -fun traced f x = if !trace then (tracing (f x); x) else x;
    2.18 +val trace = Attrib.setup_config_bool @{binding "nbe_trace"} (K false);
    2.19 +fun traced ctxt f x = if Config.get ctxt trace then (tracing (f x); x) else x;
    2.20  
    2.21  
    2.22  (** certificates and oracle for "trivial type classes" **)
    2.23 @@ -263,9 +263,10 @@
    2.24  fun nbe_apps t [] = t
    2.25    | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)];
    2.26  fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
    2.27 -fun nbe_apps_constr idx_of c ts =
    2.28 +fun nbe_apps_constr ctxt idx_of c ts =
    2.29    let
    2.30 -    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
    2.31 +    val c' = if Config.get ctxt trace
    2.32 +      then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
    2.33        else string_of_int (idx_of c);
    2.34    in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
    2.35  
    2.36 @@ -282,7 +283,7 @@
    2.37  
    2.38  (* code generation *)
    2.39  
    2.40 -fun assemble_eqnss idx_of deps eqnss =
    2.41 +fun assemble_eqnss ctxt idx_of deps eqnss =
    2.42    let
    2.43      fun prep_eqns (c, (vs, eqns)) =
    2.44        let
    2.45 @@ -301,7 +302,7 @@
    2.46              end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts'
    2.47          | NONE => if member (op =) deps sym
    2.48              then nbe_apps (nbe_fun idx_of 0 sym) ts'
    2.49 -            else nbe_apps_constr idx_of sym ts'
    2.50 +            else nbe_apps_constr ctxt idx_of sym ts'
    2.51        end
    2.52      and assemble_classrels classrels =
    2.53        fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
    2.54 @@ -358,7 +359,8 @@
    2.55          val match_cont = if Code_Symbol.is_value sym then NONE
    2.56            else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args));
    2.57          val assemble_arg = assemble_iterm
    2.58 -          (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE;
    2.59 +          (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_")
    2.60 +            dss @ ts)) NONE;
    2.61          val assemble_rhs = assemble_iterm assemble_constapp match_cont;
    2.62          val (samepairs, args') = subst_nonlin_vars args;
    2.63          val s_args = map assemble_arg args';
    2.64 @@ -379,7 +381,7 @@
    2.65          val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
    2.66            @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
    2.67              [([ml_list (rev (dicts @ default_args))],
    2.68 -              nbe_apps_constr idx_of sym (dicts @ default_args))])]);
    2.69 +              nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]);
    2.70        in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end;
    2.71  
    2.72      val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
    2.73 @@ -398,11 +400,11 @@
    2.74            |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep)))
    2.75            |> AList.lookup (op =)
    2.76            |> (fn f => the o f);
    2.77 -        val s = assemble_eqnss idx_of deps eqnss;
    2.78 +        val s = assemble_eqnss ctxt idx_of deps eqnss;
    2.79          val cs = map fst eqnss;
    2.80        in
    2.81          s
    2.82 -        |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
    2.83 +        |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s)
    2.84          |> pair ""
    2.85          |> Code_Runtime.value ctxt univs_cookie
    2.86          |> (fn f => f deps_vals)
    2.87 @@ -549,11 +551,11 @@
    2.88    in
    2.89      compile_term ctxt nbe_program deps (vs, t)
    2.90      |> term_of_univ ctxt idx_tab
    2.91 -    |> traced (fn t => "Normalized:\n" ^ string_of_term t)
    2.92 +    |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t)
    2.93      |> type_infer
    2.94 -    |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
    2.95 +    |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t)
    2.96      |> check_tvars
    2.97 -    |> traced (fn _ => "---\n")
    2.98 +    |> traced ctxt (fn _ => "---\n")
    2.99    end;
   2.100  
   2.101