Sum_Of_Squares: proper configuration options;
authorwenzelm
Fri Aug 27 17:09:18 2010 +0200 (2010-08-27)
changeset 38805b09d8603f865
parent 38804 99cc7e748ab4
child 38806 0aafc7e81056
Sum_Of_Squares: proper configuration options;
src/HOL/Library/Sum_Of_Squares.thy
src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares.thy	Fri Aug 27 17:02:19 2010 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares.thy	Fri Aug 27 17:09:18 2010 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    without calling an external prover.
     1.5  *}
     1.6  
     1.7 +setup Sum_Of_Squares.setup
     1.8  setup SOS_Wrapper.setup
     1.9  
    1.10  text {* Tests *}
     2.1 --- a/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Fri Aug 27 17:02:19 2010 +0200
     2.2 +++ b/src/HOL/Library/Sum_Of_Squares/sos_wrapper.ML	Fri Aug 27 17:09:18 2010 +0200
     2.3 @@ -8,8 +8,8 @@
     2.4  sig
     2.5    datatype prover_result = Success | Failure | Error
     2.6    val setup: theory -> theory
     2.7 -  val destdir: string Unsynchronized.ref
     2.8 -  val prover_name: string Unsynchronized.ref
     2.9 +  val dest_dir: string Config.T
    2.10 +  val prover_name: string Config.T
    2.11  end
    2.12  
    2.13  structure SOS_Wrapper: SOS_WRAPPER =
    2.14 @@ -22,14 +22,9 @@
    2.15    | str_of_result Error = "Error"
    2.16  
    2.17  
    2.18 -(*** output control ***)
    2.19 -
    2.20 -fun debug s = if ! Sum_Of_Squares.debugging then writeln s else ()
    2.21 -
    2.22 -
    2.23  (*** calling provers ***)
    2.24  
    2.25 -val destdir = Unsynchronized.ref ""
    2.26 +val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
    2.27  
    2.28  fun filename dir name =
    2.29    let
    2.30 @@ -43,12 +38,12 @@
    2.31      else error ("No such directory: " ^ dir)
    2.32    end
    2.33  
    2.34 -fun run_solver name cmd find_failure input =
    2.35 +fun run_solver ctxt name cmd find_failure input =
    2.36    let
    2.37      val _ = warning ("Calling solver: " ^ name)
    2.38  
    2.39      (* create input file *)
    2.40 -    val dir = ! destdir
    2.41 +    val dir = Config.get ctxt dest_dir
    2.42      val input_file = filename dir "sos_in"
    2.43      val _ = File.write input_file input
    2.44  
    2.45 @@ -71,7 +66,10 @@
    2.46          (File.rm input_file; if File.exists output_file then File.rm output_file else ())
    2.47        else ()
    2.48  
    2.49 -    val _ = debug ("Solver output:\n" ^ output)
    2.50 +    val _ =
    2.51 +      if Config.get ctxt Sum_Of_Squares.trace
    2.52 +      then writeln ("Solver output:\n" ^ output)
    2.53 +      else ()
    2.54  
    2.55      val _ = warning (str_of_result res ^ ": " ^ res_msg)
    2.56    in
    2.57 @@ -120,13 +118,13 @@
    2.58    | prover "csdp" = csdp
    2.59    | prover name = error ("Unknown prover: " ^ name)
    2.60  
    2.61 -val prover_name = Unsynchronized.ref "remote_csdp"
    2.62 +val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
    2.63  
    2.64 -fun call_solver opt_name =
    2.65 +fun call_solver ctxt opt_name =
    2.66    let
    2.67 -    val name = the_default (! prover_name) opt_name
    2.68 +    val name = the_default (Config.get ctxt prover_name) opt_name
    2.69      val (cmd, find_failure) = prover name
    2.70 -  in run_solver name (Path.explode cmd) find_failure end
    2.71 +  in run_solver ctxt name (Path.explode cmd) find_failure end
    2.72  
    2.73  
    2.74  (* certificate output *)
    2.75 @@ -143,9 +141,13 @@
    2.76  fun sos_solver print method = SIMPLE_METHOD' o Sum_Of_Squares.sos_tac print method
    2.77  
    2.78  val setup =
    2.79 +  setup_dest_dir #>
    2.80 +  setup_prover_name #>
    2.81    Method.setup @{binding sos}
    2.82      (Scan.lift (Scan.option Parse.xname)
    2.83 -      >> (sos_solver print_cert o Sum_Of_Squares.Prover o call_solver))
    2.84 +      >> (fn opt_name => fn ctxt =>
    2.85 +        sos_solver print_cert
    2.86 +          (Sum_Of_Squares.Prover (call_solver ctxt opt_name)) ctxt))
    2.87      "prove universal problems over the reals using sums of squares" #>
    2.88    Method.setup @{binding sos_cert}
    2.89      (Scan.lift Parse.string
     3.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:02:19 2010 +0200
     3.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Fri Aug 27 17:09:18 2010 +0200
     3.3 @@ -9,7 +9,8 @@
     3.4  sig
     3.5    datatype proof_method = Certificate of RealArith.pss_tree | Prover of string -> string
     3.6    val sos_tac: (RealArith.pss_tree -> unit) -> proof_method -> Proof.context -> int -> tactic
     3.7 -  val debugging: bool Unsynchronized.ref
     3.8 +  val trace: bool Config.T
     3.9 +  val setup: theory -> theory
    3.10    exception Failure of string;
    3.11  end
    3.12  
    3.13 @@ -49,7 +50,8 @@
    3.14  val pow2 = rat_pow rat_2;
    3.15  val pow10 = rat_pow rat_10;
    3.16  
    3.17 -val debugging = Unsynchronized.ref false;
    3.18 +val (trace, setup_trace) = Attrib.config_bool "sos_trace" (K false);
    3.19 +val setup = setup_trace;
    3.20  
    3.21  exception Sanity;
    3.22  
    3.23 @@ -1059,7 +1061,7 @@
    3.24  (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
    3.25  
    3.26  
    3.27 -fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
    3.28 +fun real_positivnullstellensatz_general ctxt prover linf d eqs leqs pol =
    3.29  let
    3.30   val vars = fold_rev (union (op aconvc) o poly_variables)
    3.31     (pol :: eqs @ map fst leqs) []
    3.32 @@ -1129,7 +1131,7 @@
    3.33    fun find_rounding d =
    3.34     let
    3.35      val _ =
    3.36 -      if !debugging
    3.37 +      if Config.get ctxt trace
    3.38        then writeln ("Trying rounding with limit "^Rat.string_of_rat d ^ "\n")
    3.39        else ()
    3.40      val vec = nice_vector d raw_vec
    3.41 @@ -1245,7 +1247,7 @@
    3.42             let val e = multidegree pol
    3.43                 val k = if e = 0 then 0 else d div e
    3.44                 val eq' = map fst eq
    3.45 -           in tryfind (fn i => (d,i,real_positivnullstellensatz_general prover false d eq' leq
    3.46 +           in tryfind (fn i => (d,i,real_positivnullstellensatz_general ctxt prover false d eq' leq
    3.47                                   (poly_neg(poly_pow pol i))))
    3.48                     (0 upto k)
    3.49             end