# HG changeset patch
# User boehmes
# Date 1419866493 -3600
# Node ID 27931bf7720a9961b310e8b60608e4dd1ae73da9
# Parent  ef5e68575bc48e61d0ad31d68f598146a4b92316
avoid more than one data slot per module

diff -r ef5e68575bc4 -r 27931bf7720a src/HOL/Tools/SMT/smt_config.ML
--- 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}