--- a/src/HOL/Tools/SMT/smt_config.ML Mon Dec 29 14:57:13 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Dec 29 16:21:33 2014 +0100
@@ -62,37 +62,55 @@
avail: unit -> bool,
options: Proof.context -> string list}
-(* FIXME just one data slot (record) per program unit *)
-structure Solvers = Generic_Data
+type data = {
+ solvers: (solver_info * string list) Symtab.table,
+ solver: string option,
+ certs: Cache_IO.cache option}
+
+fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs}
+
+val empty_data = mk_data Symtab.empty NONE NONE
+
+fun solvers_of ({solvers, ...}: data) = solvers
+fun solver_of ({solver, ...}: data) = solver
+fun certs_of ({certs, ...}: data) = certs
+
+fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs
+fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs
+fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c
+
+fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) =
+ mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2))
+
+structure Data = Generic_Data
(
- type T = (solver_info * string list) Symtab.table * string option
- val empty = (Symtab.empty, NONE)
+ type T = data
+ val empty = empty_data
val extend = I
- fun merge ((ss1, s1), (ss2, s2)) =
- (Symtab.merge (K true) (ss1, ss2), merge_options (s1, s2))
+ val merge = merge_data
)
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
+ in Data.map (map_solvers (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
+ if Symtab.defined (solvers_of (Data.get context)) name then
error ("Solver already registered: " ^ quote name)
else
context
- |> Solvers.map (apfst (Symtab.update (name, (info, []))))
+ |> Data.map (map_solvers (Symtab.update (name, (info, []))))
|> Context.map_theory (Attrib.setup (Binding.name (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 all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt)))
-fun solver_name_of ctxt = snd (Solvers.get (Context.Proof ctxt))
+fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt))
fun is_available ctxt name =
- (case Symtab.lookup (fst (Solvers.get (Context.Proof ctxt))) name of
+ (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of
SOME ({avail, ...}, _) => avail ()
| NONE => false)
@@ -108,7 +126,7 @@
fun select_solver name context =
let
val ctxt = Context.proof_of context
- val upd = Solvers.map (apsnd (K (SOME name)))
+ val upd = Data.map (map_solver (K (SOME name)))
in
if not (member (op =) (all_solvers_of ctxt) name) then
error ("Trying to select unknown solver: " ^ quote name)
@@ -125,9 +143,9 @@
| 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 ())
+ (case solver_name_of ctxt of
+ NONE => default ()
+ | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name))
fun solver_class_of ctxt =
let fun class_of ({class, ...}: solver_info, _) = class ctxt
@@ -183,26 +201,16 @@
(* 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 certificates_of = certs_of o Data.get o Context.Proof
-val get_certificates_path =
- Option.map (Cache_IO.cache_path_of) o Certificates.get o Context.Proof
+val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of
-fun select_certificates name context = context |> Certificates.put (
+fun select_certificates name context = context |> Data.map (put_certs (
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
+ |> SOME o Cache_IO.unsynchronized_init))
val setup_certificates =
Attrib.setup @{binding smt_certificates}