diff -r d10f0bbc7ea1 -r f595b7532dc9 src/HOL/Library/Old_SMT/old_smt_config.ML
--- a/src/HOL/Library/Old_SMT/old_smt_config.ML	Thu Apr 20 10:45:52 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,254 +0,0 @@
-(*  Title:      HOL/Library/Old_SMT/old_smt_config.ML
-    Author:     Sascha Boehme, TU Muenchen
-
-Configuration options and diagnostic tools for SMT.
-*)
-
-signature OLD_SMT_CONFIG =
-sig
-  (*solver*)
-  type solver_info = {
-    name: string,
-    class: Proof.context -> Old_SMT_Utils.class,
-    avail: unit -> bool,
-    options: Proof.context -> string list }
-  val add_solver: solver_info -> Context.generic -> Context.generic
-  val set_solver_options: string * string -> Context.generic -> Context.generic
-  val is_available: Proof.context -> string -> bool
-  val available_solvers_of: Proof.context -> string list
-  val select_solver: string -> Context.generic -> Context.generic
-  val solver_of: Proof.context -> string
-  val solver_class_of: Proof.context -> Old_SMT_Utils.class
-  val solver_options_of: Proof.context -> string list
-
-  (*options*)
-  val oracle: bool Config.T
-  val datatypes: bool Config.T
-  val timeout: real Config.T
-  val random_seed: int Config.T
-  val read_only_certificates: bool Config.T
-  val verbose: bool Config.T
-  val trace: bool Config.T
-  val trace_used_facts: bool Config.T
-  val monomorph_limit: int Config.T
-  val monomorph_instances: int Config.T
-  val infer_triggers: bool Config.T
-  val filter_only_facts: bool Config.T
-  val debug_files: string Config.T
-
-  (*tools*)
-  val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
-
-  (*diagnostics*)
-  val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit
-  val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit
-
-  (*certificates*)
-  val select_certificates: string -> Context.generic -> Context.generic
-  val certificates_of: Proof.context -> Cache_IO.cache option
-
-  (*setup*)
-  val setup: theory -> theory
-  val print_setup: Proof.context -> unit
-end
-
-structure Old_SMT_Config: OLD_SMT_CONFIG =
-struct
-
-(* solver *)
-
-type solver_info = {
-  name: string,
-  class: Proof.context -> Old_SMT_Utils.class,
-  avail: unit -> bool,
-  options: Proof.context -> string list }
-
-(* FIXME just one data slot (record) per program unit *)
-structure Solvers = Generic_Data
-(
-  type T = (solver_info * string list) Symtab.table * string option
-  val empty = (Symtab.empty, NONE)
-  val extend = I
-  fun merge ((ss1, s1), (ss2, s2)) =
-    (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
-)
-
-fun set_solver_options (name, options) =
-  let val opts = String.tokens (Symbol.is_ascii_blank o str) options
-  in Solvers.map (apfst (Symtab.map_entry name (apsnd (K opts)))) end
-
-fun add_solver (info as {name, ...} : solver_info) context =
-  if Symtab.defined (fst (Solvers.get context)) name then
-    error ("Solver already registered: " ^ quote name)
-  else
-    context
-    |> Solvers.map (apfst (Symtab.update (name, (info, []))))
-    |> Context.map_theory (Attrib.setup (Binding.name ("old_" ^ name ^ "_options"))
-        (Scan.lift (@{keyword "="} |-- Args.name) >>
-          (Thm.declaration_attribute o K o set_solver_options o pair name))
-        ("additional command line options for SMT solver " ^ quote name))
-
-fun all_solvers_of ctxt = Symtab.keys (fst (Solvers.get (Context.Proof ctxt)))
-
-fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
-
-fun is_available ctxt name =
-  (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
-    SOME ({avail, ...}, _) => avail ()
-  | NONE => false)
-
-fun available_solvers_of ctxt =
-  filter (is_available ctxt) (all_solvers_of ctxt)
-
-fun warn_solver (Context.Proof ctxt) name =
-      if Context_Position.is_visible ctxt then
-        warning ("The SMT solver " ^ quote name ^ " is not installed.")
-      else ()
-  | warn_solver _ _ = ();
-
-fun select_solver name context =
-  let
-    val ctxt = Context.proof_of context
-    val upd = Solvers.map (apsnd (K (SOME name)))
-  in
-    if not (member (op =) (all_solvers_of ctxt) name) then
-      error ("Trying to select unknown solver: " ^ quote name)
-    else if not (is_available ctxt name) then
-      (warn_solver context name; upd context)
-    else upd context
-  end
-
-fun no_solver_err () = error "No SMT solver selected"
-
-fun solver_of ctxt =
-  (case solver_name_of ctxt of
-    SOME name => name
-  | NONE => no_solver_err ())
-
-fun solver_info_of default select ctxt =
-  (case Solvers.get (Context.Proof ctxt) of
-    (solvers, SOME name) => select (Symtab.lookup solvers name)
-  | (_, NONE) => default ())
-
-fun solver_class_of ctxt =
-  let fun class_of ({class, ...}: solver_info, _) = class ctxt
-  in solver_info_of no_solver_err (class_of o the) ctxt end
-
-fun solver_options_of ctxt =
-  let
-    fun all_options NONE = []
-      | all_options (SOME ({options, ...} : solver_info, opts)) =
-          opts @ options ctxt
-  in solver_info_of (K []) all_options ctxt end
-
-val setup_solver =
-  Attrib.setup @{binding old_smt_solver}
-    (Scan.lift (@{keyword "="} |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_solver))
-    "SMT solver configuration"
-
-
-(* options *)
-
-val oracle = Attrib.setup_config_bool @{binding old_smt_oracle} (K true)
-val datatypes = Attrib.setup_config_bool @{binding old_smt_datatypes} (K false)
-val timeout = Attrib.setup_config_real @{binding old_smt_timeout} (K 30.0)
-val random_seed = Attrib.setup_config_int @{binding old_smt_random_seed} (K 1)
-val read_only_certificates = Attrib.setup_config_bool @{binding old_smt_read_only_certificates} (K false)
-val verbose = Attrib.setup_config_bool @{binding old_smt_verbose} (K true)
-val trace = Attrib.setup_config_bool @{binding old_smt_trace} (K false)
-val trace_used_facts = Attrib.setup_config_bool @{binding old_smt_trace_used_facts} (K false)
-val monomorph_limit = Attrib.setup_config_int @{binding old_smt_monomorph_limit} (K 10)
-val monomorph_instances = Attrib.setup_config_int @{binding old_smt_monomorph_instances} (K 500)
-val infer_triggers = Attrib.setup_config_bool @{binding old_smt_infer_triggers} (K false)
-val filter_only_facts = Attrib.setup_config_bool @{binding old_smt_filter_only_facts} (K false)
-val debug_files = Attrib.setup_config_string @{binding old_smt_debug_files} (K "")
-
-
-(* diagnostics *)
-
-fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else ()
-
-fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose)
-
-fun trace_msg ctxt = cond_trace (Config.get ctxt trace)
-
-
-(* tools *)
-
-fun with_timeout ctxt f x =
-  Timeout.apply (seconds (Config.get ctxt timeout)) f x
-    handle Timeout.TIMEOUT _ => raise Old_SMT_Failure.SMT Old_SMT_Failure.Time_Out
-
-
-(* certificates *)
-
-(* FIXME just one data slot (record) per program unit *)
-structure Certificates = Generic_Data
-(
-  type T = Cache_IO.cache option
-  val empty = NONE
-  val extend = I
-  fun merge (s, _) = s  (* FIXME merge options!? *)
-)
-
-val get_certificates_path =
-  Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
-
-fun select_certificates name context = context |> Certificates.put (
-  if name = "" then NONE
-  else
-    Path.explode name
-    |> Path.append (Resources.master_directory (Context.theory_of context))
-    |> SOME o Cache_IO.unsynchronized_init)
-
-val certificates_of = Certificates.get o Context.Proof
-
-val setup_certificates =
-  Attrib.setup @{binding old_smt_certificates}
-    (Scan.lift (@{keyword "="} |-- Args.name) >>
-      (Thm.declaration_attribute o K o select_certificates))
-    "SMT certificates configuration"
-
-
-(* setup *)
-
-val setup =
-  setup_solver #>
-  setup_certificates
-
-fun print_setup ctxt =
-  let
-    fun string_of_bool b = if b then "true" else "false"
-
-    val names = available_solvers_of ctxt
-    val ns = if null names then ["(none)"] else sort_strings names
-    val n = the_default "(none)" (solver_name_of ctxt)
-    val opts = solver_options_of ctxt
-    
-    val t = string_of_real (Config.get ctxt timeout)
-
-    val certs_filename =
-      (case get_certificates_path ctxt of
-        SOME path => Path.print path
-      | NONE => "(disabled)")
-  in
-    Pretty.writeln (Pretty.big_list "SMT setup:" [
-      Pretty.str ("Current SMT solver: " ^ n),
-      Pretty.str ("Current SMT solver options: " ^ space_implode " " opts),
-      Pretty.str_list "Available SMT solvers: "  "" ns,
-      Pretty.str ("Current timeout: " ^ t ^ " seconds"),
-      Pretty.str ("With proofs: " ^
-        string_of_bool (not (Config.get ctxt oracle))),
-      Pretty.str ("Certificates cache: " ^ certs_filename),
-      Pretty.str ("Fixed certificates: " ^
-        string_of_bool (Config.get ctxt read_only_certificates))])
-  end
-
-val _ =
-  Outer_Syntax.command @{command_keyword old_smt_status}
-    "show the available SMT solvers, the currently selected SMT solver, \
-    \and the values of SMT configuration options"
-    (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of)))
-
-end