src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
changeset 38805 b09d8603f865
parent 38795 848be46708dc
child 39027 e4262f9e6a4e
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:02:19 2010 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:09:18 2010 +0200
     1.3 @@ -9,7 +9,8 @@
     1.4  sig
     1.5    datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
     1.6    val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
     1.7 -  val debugging: bool Unsynchronized.ref
     1.8 +  val trace: bool Config.T
     1.9 +  val setup: theory -> theory
    1.10    exception Failure of string;
    1.11  end
    1.12  
    1.13 @@ -49,7 +50,8 @@
    1.14  val pow2 = rat_pow rat_2;
    1.15  val pow10 = rat_pow rat_10;
    1.16  
    1.17 -val debugging = Unsynchronized.ref false;
    1.18 +val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
    1.19 +val setup = setup_trace;
    1.20  
    1.21  exception Sanity;
    1.22  
    1.23 @@ -1059,7 +1061,7 @@
    1.24  (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
    1.25  
    1.26  
    1.27 -fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
    1.28 +fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol =
    1.29  let
    1.30   val vars = fold_rev (union (op aconvc) o poly_variables)
    1.31     (pol :: eqs @ map fst leqs) []
    1.32 @@ -1129,7 +1131,7 @@
    1.33    fun find_rounding d =
    1.34     let
    1.35      val _ =
    1.36 -      if !debugging
    1.37 +      if Config.get ctxt trace
    1.38        then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
    1.39        else ()
    1.40      val vec = nice_vector d raw_vec
    1.41 @@ -1245,7 +1247,7 @@
    1.42             let val e = multidegree pol
    1.43                 val k = if e = 0 then 0 else d div e
    1.44                 val eq' = map fst eq
    1.45 -           in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
    1.46 +           in tryfind (fn i => (d,i,real_positivnullstellensatz_general ctxt prover false d eq' leq
    1.47                                   (poly_neg(poly_pow pol i))))
    1.48                     (0 upto k)
    1.49             end