src/HOL/Library/Sum_of_Squares/sum_of_squares.ML

 signature SUM_OF_SQUARES =
 sig
   datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
   val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
   val trace: bool Config.T
+  val debug: bool Config.T
+  val trace_message: Proof.context -> (unit -> string) -> unit
+  val debug_message: Proof.context -> (unit -> string) -> unit
   exception Failure of string;
 end
 
 structure Sum_of_Squares: SUM_OF_SQUARES =
 struct

 
 val abs_rat = Rat.abs;
 val pow2 = rat_pow rat_2;
 val pow10 = rat_pow rat_10;
 
+
 val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
+val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
+
+fun trace_message ctxt msg =
+  if Config.get ctxt trace orelse Config.get ctxt debug then tracing (msg ()) else ();
+fun debug_message ctxt msg = if Config.get ctxt debug then tracing (msg ()) else ();
 
 exception Sanity;
 
 exception Unsolvable;
 

     fun int_element (_, v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
 
     fun find_rounding d =
       let
         val _ =
-          if Config.get ctxt trace
-          then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
-          else ()
+          debug_message ctxt (fn () => "Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
         val vec = nice_vector d raw_vec
         val blockmat =
           iter (1, dim vec)
             (fn i => fn a => bmatrix_add (bmatrix_cmul (int_element vec i) (nth mats i)) a)
             (bmatrix_neg (nth mats 0))

   end
 
 
 (* Iterative deepening.                                                      *)
 
-fun deepen f n =
-  (writeln ("Searching with depth limit " ^ string_of_int n);
-    (f n handle Failure s => (writeln ("failed with message: " ^ s); deepen f (n + 1))));
+fun deepen ctxt f n =
+  (trace_message ctxt (fn () => "Searching with depth limit " ^ string_of_int n);
+    (f n handle Failure s =>
+      (trace_message ctxt (fn () => "failed with message: " ^ s); deepen ctxt f (n + 1))));
 
 
 (* Map back polynomials and their composites to a positivstellensatz.        *)
 
 fun cterm_of_sqterm (c, p) = RealArith.Product (RealArith.Rational_lt c, RealArith.Square p);

                         tryfind (fn i =>
                             (d, i, real_positivnullstellensatz_general ctxt prover false d eq' leq
                               (poly_neg(poly_pow pol i))))
                           (0 upto k)
                       end
-                    val (_,i,(cert_ideal,cert_cone)) = deepen tryall 0
+                    val (_,i,(cert_ideal,cert_cone)) = deepen ctxt tryall 0
                     val proofs_ideal =
                       map2 (fn q => fn (_,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
                     val proofs_cone = map cterm_of_sos cert_cone
                     val proof_ne =
                       if null ltp then RealArith.Rational_lt Rat.one