Sum_Of_Squares: proper configuration options;

--- a/src/HOL/Library/Sum_Of_Squares.thy	Fri Aug 27 17:02:19 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy	Fri Aug 27 17:09:18 2010 +0200
@@ -28,6 +28,7 @@
   without calling an external prover.
 *}
 
+setup Sum_Of_Squares.setup
 setup SOS_Wrapper.setup
 
 text {* Tests *}

--- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Fri Aug 27 17:02:19 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Fri Aug 27 17:09:18 2010 +0200
@@ -8,8 +8,8 @@
 sig
   datatype prover_result = Success | Failure | Error
   val setup: theory -> theory
-  val destdir: string Unsynchronized.ref
-  val prover_name: string Unsynchronized.ref
+  val dest_dir: string Config.T
+  val prover_name: string Config.T
 end
 
 structure SOS_Wrapper: SOS_WRAPPER =
@@ -22,14 +22,9 @@
   | str_of_result Error = "Error"
 
 
-(*** output control ***)
-
-fun debug s = if ! Sum_Of_Squares.debugging then writeln s else ()
-
-
 (*** calling provers ***)
 
-val destdir = Unsynchronized.ref ""
+val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
 
 fun filename dir name =
   let
@@ -43,12 +38,12 @@
     else error ("No such directory: " ^ dir)
   end
 
-fun run_solver name cmd find_failure input =
+fun run_solver ctxt name cmd find_failure input =
   let
     val _ = warning ("Calling solver: " ^ name)
 
     (* create input file *)
-    val dir = ! destdir
+    val dir = Config.get ctxt dest_dir
     val input_file = filename dir "sos_in"
     val _ = File.write input_file input
 
@@ -71,7 +66,10 @@
         (File.rm input_file; if File.exists output_file then File.rm output_file else ())
       else ()
 
-    val _ = debug ("Solver output:\n" ^ output)
+    val _ =
+      if Config.get ctxt Sum_Of_Squares.trace
+      then writeln ("Solver output:\n" ^ output)
+      else ()
 
     val _ = warning (str_of_result res ^ ": " ^ res_msg)
   in
@@ -120,13 +118,13 @@
   | prover "csdp" = csdp
   | prover name = error ("Unknown prover: " ^ name)
 
-val prover_name = Unsynchronized.ref "remote_csdp"
+val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
 
-fun call_solver opt_name =
+fun call_solver ctxt opt_name =
   let
-    val name = the_default (! prover_name) opt_name
+    val name = the_default (Config.get ctxt prover_name) opt_name
     val (cmd, find_failure) = prover name
-  in run_solver name (Path.explode cmd) find_failure end
+  in run_solver ctxt name (Path.explode cmd) find_failure end
 
 
 (* certificate output *)
@@ -143,9 +141,13 @@
 fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method
 
 val setup =
+  setup_dest_dir #>
+  setup_prover_name #>
   Method.setup @{binding sos}
     (Scan.lift (Scan.option Parse.xname)
-      >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
+      >> (fn opt_name => fn ctxt =>
+        sos_solver print_cert
+          (Sum_Of_Squares.Prover (call_solver ctxt opt_name)) ctxt))
     "prove universal problems over the reals using sums of squares" #>
   Method.setup @{binding sos_cert}
     (Scan.lift Parse.string

--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:02:19 2010 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:09:18 2010 +0200
@@ -9,7 +9,8 @@
 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 debugging: bool Unsynchronized.ref
+  val trace: bool Config.T
+  val setup: theory -> theory
   exception Failure of string;
 end
 
@@ -49,7 +50,8 @@
 val pow2 = rat_pow rat_2;
 val pow10 = rat_pow rat_10;
 
-val debugging = Unsynchronized.ref false;
+val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
+val setup = setup_trace;
 
 exception Sanity;
 
@@ -1059,7 +1061,7 @@
 (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
 
 
-fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
+fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol =
 let
  val vars = fold_rev (union (op aconvc) o poly_variables)
    (pol :: eqs @ map fst leqs) []
@@ -1129,7 +1131,7 @@
   fun find_rounding d =
    let
     val _ =
-      if !debugging
+      if Config.get ctxt trace
       then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
       else ()
     val vec = nice_vector d raw_vec
@@ -1245,7 +1247,7 @@
            let val e = multidegree pol
                val k = if e = 0 then 0 else d div e
                val eq' = map fst eq
-           in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
+           in tryfind (fn i => (d,i,real_positivnullstellensatz_general ctxt prover false d eq' leq
                                  (poly_neg(poly_pow pol i))))
                    (0 upto k)
            end