make tracing monotonicity easier
authorblanchet
Tue Aug 03 14:49:02 2010 +0200 (2010-08-03)
changeset 381797207321df8af
parent 38178 0cea0125339a
child 38180 7a88032f9265
make tracing monotonicity easier
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Aug 03 14:28:44 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Aug 03 14:49:02 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    type hol_context = Nitpick_HOL.hol_context
     1.6  
     1.7 +  val trace : bool Unsynchronized.ref
     1.8    val formulas_monotonic :
     1.9      hol_context -> bool -> typ -> term list * term list -> bool
    1.10    val finitize_funs :
    1.11 @@ -54,9 +55,8 @@
    1.12  exception MTYPE of string * mtyp list * typ list
    1.13  exception MTERM of string * mterm list
    1.14  
    1.15 -val debug_mono = false
    1.16 -
    1.17 -fun print_g f = () |> debug_mono ? tracing o f
    1.18 +val trace = Unsynchronized.ref false
    1.19 +fun trace_msg msg = if !trace then tracing (msg ()) else ()
    1.20  
    1.21  val string_for_var = signed_string_of_int
    1.22  fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
    1.23 @@ -402,10 +402,10 @@
    1.24                   [M1, M2], [])
    1.25  
    1.26  fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
    1.27 -    (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    1.28 -                       string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    1.29 +    (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    1.30 +                         string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    1.31       case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
    1.32 -       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.33 +       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.34       | SOME (lits, comps) => (lits, comps, sexps))
    1.35  
    1.36  val add_mtypes_equal = add_mtype_comp Eq
    1.37 @@ -447,11 +447,11 @@
    1.38      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
    1.39  
    1.40  fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
    1.41 -    (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
    1.42 -                       (case sn of Minus => "concrete" | Plus => "complete") ^
    1.43 -                       ".");
    1.44 +    (trace_msg (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
    1.45 +                         (case sn of Minus => "concrete" | Plus => "complete") ^
    1.46 +                         ".");
    1.47       case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
    1.48 -       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.49 +       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.50       | SOME (lits, sexps) => (lits, comps, sexps))
    1.51  
    1.52  val add_mtype_is_concrete = add_notin_mtype_fv Minus
    1.53 @@ -493,16 +493,16 @@
    1.54    subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
    1.55  
    1.56  fun print_problem lits comps sexps =
    1.57 -  print_g (fn () => "*** Problem:\n" ^
    1.58 -                    cat_lines (map string_for_literal lits @
    1.59 -                               map string_for_comp comps @
    1.60 -                               map string_for_sign_expr sexps))
    1.61 +  trace_msg (fn () => "*** Problem:\n" ^
    1.62 +                      cat_lines (map string_for_literal lits @
    1.63 +                                 map string_for_comp comps @
    1.64 +                                 map string_for_sign_expr sexps))
    1.65  
    1.66  fun print_solution lits =
    1.67    let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
    1.68 -    print_g (fn () => "*** Solution:\n" ^
    1.69 -                      "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    1.70 -                      "-: " ^ commas (map (string_for_var o fst) neg))
    1.71 +    trace_msg (fn () => "*** Solution:\n" ^
    1.72 +                        "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    1.73 +                        "-: " ^ commas (map (string_for_var o fst) neg))
    1.74    end
    1.75  
    1.76  fun solve max_var (lits, comps, sexps) =
    1.77 @@ -628,8 +628,8 @@
    1.78        end
    1.79      and do_term t (accum as (gamma as {bound_Ts, bound_Ms, frees, consts},
    1.80                               cset)) =
    1.81 -        (print_g (fn () => "  \<Gamma> \<turnstile> " ^
    1.82 -                           Syntax.string_of_term ctxt t ^ " : _?");
    1.83 +        (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
    1.84 +                             Syntax.string_of_term ctxt t ^ " : _?");
    1.85           case t of
    1.86             Const (x as (s, T)) =>
    1.87             (case AList.lookup (op =) consts x of
    1.88 @@ -652,9 +652,9 @@
    1.89                  end
    1.90                | @{const_name "op ="} => do_equals T accum
    1.91                | @{const_name The} =>
    1.92 -                (print_g (K "*** The"); raise UNSOLVABLE ())
    1.93 +                (trace_msg (K "*** The"); raise UNSOLVABLE ())
    1.94                | @{const_name Eps} =>
    1.95 -                (print_g (K "*** Eps"); raise UNSOLVABLE ())
    1.96 +                (trace_msg (K "*** Eps"); raise UNSOLVABLE ())
    1.97                | @{const_name If} =>
    1.98                  do_robust_set_operation (range_type T) accum
    1.99                  |>> curry3 MFun bool_M (S Minus)
   1.100 @@ -742,7 +742,7 @@
   1.101                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   1.102                        frees = (x, M) :: frees, consts = consts}, cset))
   1.103                end) |>> curry MRaw t
   1.104 -         | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ())
   1.105 +         | Var _ => (trace_msg (K "*** Var"); raise UNSOLVABLE ())
   1.106           | Bound j => (MRaw (t, nth bound_Ms j), accum)
   1.107           | Abs (s, T, t') =>
   1.108             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   1.109 @@ -793,8 +793,8 @@
   1.110                 val M2 = mtype_of_mterm m2
   1.111               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
   1.112             end)
   1.113 -        |> tap (fn (m, _) => print_g (fn () => "  \<Gamma> \<turnstile> " ^
   1.114 -                                               string_for_mterm ctxt m))
   1.115 +        |> tap (fn (m, _) => trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.116 +                                                 string_for_mterm ctxt m))
   1.117    in do_term end
   1.118  
   1.119  fun force_minus_funs 0 _ = I
   1.120 @@ -848,9 +848,9 @@
   1.121                Plus => do_term t accum
   1.122              | Minus => consider_general_equals mdata false x t1 t2 accum
   1.123          in
   1.124 -          (print_g (fn () => "  \<Gamma> \<turnstile> " ^
   1.125 -                           Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
   1.126 -                           string_for_sign sn ^ "?");
   1.127 +          (trace_msg (fn () => "  \<Gamma> \<turnstile> " ^
   1.128 +                               Syntax.string_of_term ctxt t ^ " : o\<^sup>" ^
   1.129 +                               string_for_sign sn ^ "?");
   1.130             case t of
   1.131               Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
   1.132               do_quantifier x s1 T1 t1
   1.133 @@ -898,9 +898,9 @@
   1.134             | _ => do_term t accum)
   1.135          end
   1.136          |> tap (fn (m, _) =>
   1.137 -                   print_g (fn () => "\<Gamma> \<turnstile> " ^
   1.138 -                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.139 -                                     string_for_sign sn))
   1.140 +                   trace_msg (fn () => "\<Gamma> \<turnstile> " ^
   1.141 +                                       string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.142 +                                       string_for_sign sn))
   1.143    in do_formula end
   1.144  
   1.145  (* The harmless axiom optimization below is somewhat too aggressive in the face
   1.146 @@ -983,7 +983,7 @@
   1.147    Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
   1.148  
   1.149  fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
   1.150 -  print_g (fn () =>
   1.151 +  trace_msg (fn () =>
   1.152        map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   1.153        map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   1.154        |> cat_lines)
   1.155 @@ -994,9 +994,9 @@
   1.156  fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   1.157            (nondef_ts, def_ts) =
   1.158    let
   1.159 -    val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^
   1.160 -                              string_for_mtype MAlpha ^ " is " ^
   1.161 -                              Syntax.string_of_typ ctxt alpha_T)
   1.162 +    val _ = trace_msg (fn () => "****** " ^ which ^ " analysis: " ^
   1.163 +                                string_for_mtype MAlpha ^ " is " ^
   1.164 +                                Syntax.string_of_typ ctxt alpha_T)
   1.165      val mdata as {max_fresh, constr_mcache, ...} =
   1.166        initial_mdata hol_ctxt binarize no_harmless alpha_T
   1.167      val accum = (initial_gamma, ([], [], []))