# HG changeset patch
# User boehmes
# Date 1291793582 -3600
# Node ID 9f9bc1bdacef505398a946c6b4ff2b3ae99227d8
# Parent  7204024077a8c6edcf1390ffc9f949532b082506
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)

diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -8,9 +8,10 @@
 sig
   (*built-in types*)
   val add_builtin_typ: SMT_Config.class ->
-    typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
-    theory
-  val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
+    typ * (typ -> string option) * (typ -> int -> string option) ->
+    Context.generic -> Context.generic
+  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
+    Context.generic
   val builtin_typ: Proof.context -> typ -> string option
   val is_builtin_typ: Proof.context -> typ -> bool
   val is_builtin_typ_ext: Proof.context -> typ -> bool
@@ -23,11 +24,14 @@
   (*built-in functions*)
   type 'a bfun = Proof.context -> typ -> term list -> 'a
   val add_builtin_fun: SMT_Config.class ->
-    (string * typ) * (string * term list) option bfun -> theory -> theory
-  val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
-  val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
-  val add_builtin_fun_ext': string * typ -> theory -> theory
-  val add_builtin_fun_ext'': string -> theory -> theory
+    (string * typ) * (string * term list) option bfun -> Context.generic ->
+    Context.generic
+  val add_builtin_fun': SMT_Config.class -> term * string -> Context.generic ->
+    Context.generic
+  val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
+    Context.generic
+  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
+  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
   val builtin_fun: Proof.context -> string * typ -> term list ->
     (string * term list) option
   val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
@@ -48,8 +52,6 @@
 
 type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list 
 
-fun empty_ttab () = []
-
 fun typ_ord ((T, _), (U, _)) =
   let
     fun tord (TVar _, Type _) = GREATER
@@ -94,11 +96,11 @@
 
 (* built-in types *)
 
-structure Builtin_Types = Theory_Data
+structure Builtin_Types = Generic_Data
 (
   type T =
     (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
-  val empty = empty_ttab ()
+  val empty = []
   val extend = I
   val merge = merge_ttab
 )
@@ -110,7 +112,7 @@
   Builtin_Types.map (insert_ttab C.basicC T (Ext f))
 
 fun lookup_builtin_typ ctxt =
-  lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
+  lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
 
 fun builtin_typ ctxt T =
   (case lookup_builtin_typ ctxt T of
@@ -157,14 +159,16 @@
   @{const_name SMT.pat}, @{const_name SMT.nopat},
   @{const_name SMT.trigger}, @{const_name SMT.weight}]
 
-fun basic_builtin_funcs () =
+type builtin_funcs = (bool bfun, (string * term list) option bfun) btab
+
+fun basic_builtin_funcs () : builtin_funcs =
   empty_btab ()
   |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
        (* FIXME: SMT_Normalize should check that they are properly used *)
 
-structure Builtin_Funcs = Theory_Data
+structure Builtin_Funcs = Generic_Data
 (
-  type T = (bool bfun, (string * term list) option bfun) btab
+  type T = builtin_funcs
   val empty = basic_builtin_funcs ()
   val extend = I
   val merge = merge_btab
@@ -181,11 +185,12 @@
 
 fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
 
-fun add_builtin_fun_ext'' n thy =
-  add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
+fun add_builtin_fun_ext'' n context =
+  let val thy = Context.theory_of context
+  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
 
 fun lookup_builtin_fun ctxt =
-  lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
+  lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
 
 fun builtin_fun ctxt (c as (_, T)) ts =
   (case lookup_builtin_fun ctxt c of
diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -582,10 +582,10 @@
 
 (* setup *)
 
-val setup =
+val setup = Context.theory_map (
   setup_bool_case #>
   setup_nat_as_int #>
   setup_unfolded_quants #>
-  setup_atomize
+  setup_atomize)
 
 end
diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -106,9 +106,9 @@
 (* setup *)
 
 val setup =
-  setup_builtins #>
   Context.theory_map (
     SMTLIB_Interface.add_logic (10, smtlib_logic) #>
+    setup_builtins #>
     Z3_Interface.add_mk_builtins z3_mk_builtins #>
     fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
     Z3_Proof_Tools.add_simproc real_linarith_proc)
diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -9,8 +9,8 @@
   val smtlibC: SMT_Config.class
   val add_logic: int * (term list -> string option) -> Context.generic ->
     Context.generic
+  val interface: SMT_Solver.interface
   val setup: theory -> theory
-  val interface: SMT_Solver.interface
 end
 
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
@@ -106,7 +106,7 @@
     | distinct _ _ _ = NONE
 in
 
-val setup =
+val setup_builtins =
   B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
   fold (B.add_builtin_fun' smtlibC) [
     (@{const True}, "true"),
@@ -155,7 +155,7 @@
   in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
 
 
-(* serialization *)
+(** serialization **)
 
 val add = Buffer.add
 fun sep f = add " " #> f
@@ -216,7 +216,7 @@
 
 
 
-(** interfaces **)
+(* interface *)
 
 val interface = {
   class = smtlibC,
@@ -230,4 +230,6 @@
     has_datatypes = false,
     serialize = serialize}}
 
+val setup = Context.theory_map setup_builtins
+
 end
diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -7,8 +7,8 @@
 signature Z3_INTERFACE =
 sig
   val smtlib_z3C: SMT_Config.class
+  val interface: SMT_Solver.interface
   val setup: theory -> theory
-  val interface: SMT_Solver.interface
 
   datatype sym = Sym of string * sym list
   type mk_builtins = {
@@ -49,12 +49,12 @@
     else irules
 
   fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
+
+  val setup_builtins =
+    B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
+    B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
 in
 
-val setup =
-  B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
-  B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
-
 val interface = {
   class = smtlib_z3C,
   extra_norm = extra_norm',
@@ -65,6 +65,8 @@
     has_datatypes = true,
     serialize = serialize}}
 
+val setup = Context.theory_map setup_builtins
+
 end
 
 
diff -r 7204024077a8 -r 9f9bc1bdacef src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Tue Dec 07 21:58:36 2010 +0100
+++ b/src/HOL/Word/Tools/smt_word.ML	Wed Dec 08 08:33:02 2010 +0100
@@ -139,7 +139,8 @@
 (* setup *)
 
 val setup = 
-  Context.theory_map (SMTLIB_Interface.add_logic (20, smtlib_logic)) #>
-  setup_builtins
+  Context.theory_map (
+    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
+    setup_builtins)
 
 end