added "trace_meson" configuration option, replacing old-fashioned reference
authorblanchet
Mon Oct 11 18:03:18 2010 +0700 (2010-10-11)
changeset 39979b13515940b53
parent 39978 11bfb7e7cc86
child 39980 f175e482dabe
added "trace_meson" configuration option, replacing old-fashioned reference
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Oct 11 18:02:14 2010 +0700
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Oct 11 18:03:18 2010 +0700
     1.3 @@ -8,7 +8,8 @@
     1.4  
     1.5  signature MESON =
     1.6  sig
     1.7 -  val trace: bool Unsynchronized.ref
     1.8 +  val trace : bool Config.T
     1.9 +  val max_clauses : int Config.T
    1.10    val term_pair_of: indexname * (typ * 'a) -> term * 'a
    1.11    val size_of_subgoals: thm -> int
    1.12    val has_too_many_clauses: Proof.context -> term -> bool
    1.13 @@ -39,17 +40,19 @@
    1.14    val make_meta_clause: thm -> thm
    1.15    val make_meta_clauses: thm list -> thm list
    1.16    val meson_tac: Proof.context -> thm list -> int -> tactic
    1.17 -  val setup: theory -> theory
    1.18 +  val setup : theory -> theory
    1.19  end
    1.20  
    1.21  structure Meson : MESON =
    1.22  struct
    1.23  
    1.24 -val trace = Unsynchronized.ref false;
    1.25 -fun trace_msg msg = if ! trace then tracing (msg ()) else ();
    1.26 +val (trace, trace_setup) = Attrib.config_bool "trace_meson" (K false)
    1.27 +
    1.28 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.29  
    1.30 -val max_clauses_default = 60;
    1.31 -val (max_clauses, setup) = Attrib.config_int "meson_max_clauses" (K max_clauses_default);
    1.32 +val max_clauses_default = 60
    1.33 +val (max_clauses, max_clauses_setup) =
    1.34 +  Attrib.config_int "meson_max_clauses" (K max_clauses_default)
    1.35  
    1.36  (*No known example (on 1-5-2007) needs even thirty*)
    1.37  val iter_deepen_limit = 50;
    1.38 @@ -366,7 +369,7 @@
    1.39        and cnf_nil th = cnf_aux (th,[])
    1.40        val cls =
    1.41              if has_too_many_clauses ctxt (concl_of th)
    1.42 -            then (trace_msg (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.43 +            then (trace_msg ctxt (fn () => "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
    1.44              else cnf_aux (th,ths)
    1.45    in  (cls, !ctxtr)  end;
    1.46  
    1.47 @@ -586,8 +589,8 @@
    1.48  (* "RS" can fail if "unify_search_bound" is too small. *)
    1.49  fun try_skolemize ctxt th =
    1.50    try (skolemize ctxt) th
    1.51 -  |> tap (fn NONE => trace_msg (fn () => "Failed to skolemize " ^
    1.52 -                                         Display.string_of_thm ctxt th)
    1.53 +  |> tap (fn NONE => trace_msg ctxt (fn () => "Failed to skolemize " ^
    1.54 +                                              Display.string_of_thm ctxt th)
    1.55             | _ => ())
    1.56  
    1.57  fun add_clauses th cls =
    1.58 @@ -678,7 +681,7 @@
    1.59      | goes =>
    1.60          let
    1.61            val horns = make_horns (cls @ ths)
    1.62 -          val _ = trace_msg (fn () =>
    1.63 +          val _ = trace_msg ctxt (fn () =>
    1.64              cat_lines ("meson method called:" ::
    1.65                map (Display.string_of_thm ctxt) (cls @ ths) @
    1.66                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.67 @@ -717,4 +720,8 @@
    1.68      name_thms "MClause#"
    1.69        (distinct Thm.eq_thm_prop (map make_meta_clause ths));
    1.70  
    1.71 +val setup =
    1.72 +  trace_setup
    1.73 +  #> max_clauses_setup
    1.74 +
    1.75  end;
     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 18:02:14 2010 +0700
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 18:03:18 2010 +0700
     2.3 @@ -9,6 +9,7 @@
     2.4  
     2.5  signature METIS_TACTICS =
     2.6  sig
     2.7 +  val trace : bool Config.T
     2.8    val type_lits : bool Config.T
     2.9    val new_skolemizer : bool Config.T
    2.10    val metis_tac : Proof.context -> thm list -> int -> tactic