be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
authorboehmes
Wed Dec 08 08:33:02 2010 +0100 (2010-12-08)
changeset 410729f9bc1bdacef
parent 41071 7204024077a8
child 41073 07b454783ed8
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
src/HOL/Tools/SMT/smt_builtin.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Word/Tools/smt_word.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_builtin.ML	Tue Dec 07 21:58:36 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Dec 08 08:33:02 2010 +0100
     1.3 @@ -8,9 +8,10 @@
     1.4  sig
     1.5    (*built-in types*)
     1.6    val add_builtin_typ: SMT_Config.class ->
     1.7 -    typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
     1.8 -    theory
     1.9 -  val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
    1.10 +    typ * (typ -> string option) * (typ -> int -> string option) ->
    1.11 +    Context.generic -> Context.generic
    1.12 +  val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic ->
    1.13 +    Context.generic
    1.14    val builtin_typ: Proof.context -> typ -> string option
    1.15    val is_builtin_typ: Proof.context -> typ -> bool
    1.16    val is_builtin_typ_ext: Proof.context -> typ -> bool
    1.17 @@ -23,11 +24,14 @@
    1.18    (*built-in functions*)
    1.19    type 'a bfun = Proof.context -> typ -> term list -> 'a
    1.20    val add_builtin_fun: SMT_Config.class ->
    1.21 -    (string * typ) * (string * term list) option bfun -> theory -> theory
    1.22 -  val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
    1.23 -  val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
    1.24 -  val add_builtin_fun_ext': string * typ -> theory -> theory
    1.25 -  val add_builtin_fun_ext'': string -> theory -> theory
    1.26 +    (string * typ) * (string * term list) option bfun -> Context.generic ->
    1.27 +    Context.generic
    1.28 +  val add_builtin_fun': SMT_Config.class -> term * string -> Context.generic ->
    1.29 +    Context.generic
    1.30 +  val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic ->
    1.31 +    Context.generic
    1.32 +  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
    1.33 +  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
    1.34    val builtin_fun: Proof.context -> string * typ -> term list ->
    1.35      (string * term list) option
    1.36    val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    1.37 @@ -48,8 +52,6 @@
    1.38  
    1.39  type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list 
    1.40  
    1.41 -fun empty_ttab () = []
    1.42 -
    1.43  fun typ_ord ((T, _), (U, _)) =
    1.44    let
    1.45      fun tord (TVar _, Type _) = GREATER
    1.46 @@ -94,11 +96,11 @@
    1.47  
    1.48  (* built-in types *)
    1.49  
    1.50 -structure Builtin_Types = Theory_Data
    1.51 +structure Builtin_Types = Generic_Data
    1.52  (
    1.53    type T =
    1.54      (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
    1.55 -  val empty = empty_ttab ()
    1.56 +  val empty = []
    1.57    val extend = I
    1.58    val merge = merge_ttab
    1.59  )
    1.60 @@ -110,7 +112,7 @@
    1.61    Builtin_Types.map (insert_ttab C.basicC T (Ext f))
    1.62  
    1.63  fun lookup_builtin_typ ctxt =
    1.64 -  lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
    1.65 +  lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt))
    1.66  
    1.67  fun builtin_typ ctxt T =
    1.68    (case lookup_builtin_typ ctxt T of
    1.69 @@ -157,14 +159,16 @@
    1.70    @{const_name SMT.pat}, @{const_name SMT.nopat},
    1.71    @{const_name SMT.trigger}, @{const_name SMT.weight}]
    1.72  
    1.73 -fun basic_builtin_funcs () =
    1.74 +type builtin_funcs = (bool bfun, (string * term list) option bfun) btab
    1.75 +
    1.76 +fun basic_builtin_funcs () : builtin_funcs =
    1.77    empty_btab ()
    1.78    |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
    1.79         (* FIXME: SMT_Normalize should check that they are properly used *)
    1.80  
    1.81 -structure Builtin_Funcs = Theory_Data
    1.82 +structure Builtin_Funcs = Generic_Data
    1.83  (
    1.84 -  type T = (bool bfun, (string * term list) option bfun) btab
    1.85 +  type T = builtin_funcs
    1.86    val empty = basic_builtin_funcs ()
    1.87    val extend = I
    1.88    val merge = merge_btab
    1.89 @@ -181,11 +185,12 @@
    1.90  
    1.91  fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
    1.92  
    1.93 -fun add_builtin_fun_ext'' n thy =
    1.94 -  add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
    1.95 +fun add_builtin_fun_ext'' n context =
    1.96 +  let val thy = Context.theory_of context
    1.97 +  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
    1.98  
    1.99  fun lookup_builtin_fun ctxt =
   1.100 -  lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
   1.101 +  lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt))
   1.102  
   1.103  fun builtin_fun ctxt (c as (_, T)) ts =
   1.104    (case lookup_builtin_fun ctxt c of
     2.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Dec 07 21:58:36 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 08 08:33:02 2010 +0100
     2.3 @@ -582,10 +582,10 @@
     2.4  
     2.5  (* setup *)
     2.6  
     2.7 -val setup =
     2.8 +val setup = Context.theory_map (
     2.9    setup_bool_case #>
    2.10    setup_nat_as_int #>
    2.11    setup_unfolded_quants #>
    2.12 -  setup_atomize
    2.13 +  setup_atomize)
    2.14  
    2.15  end
     3.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Dec 07 21:58:36 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Dec 08 08:33:02 2010 +0100
     3.3 @@ -106,9 +106,9 @@
     3.4  (* setup *)
     3.5  
     3.6  val setup =
     3.7 -  setup_builtins #>
     3.8    Context.theory_map (
     3.9      SMTLIB_Interface.add_logic (10, smtlib_logic) #>
    3.10 +    setup_builtins #>
    3.11      Z3_Interface.add_mk_builtins z3_mk_builtins #>
    3.12      fold Z3_Proof_Reconstruction.add_z3_rule real_rules #>
    3.13      Z3_Proof_Tools.add_simproc real_linarith_proc)
     4.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Dec 07 21:58:36 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Dec 08 08:33:02 2010 +0100
     4.3 @@ -9,8 +9,8 @@
     4.4    val smtlibC: SMT_Config.class
     4.5    val add_logic: int * (term list -> string option) -> Context.generic ->
     4.6      Context.generic
     4.7 +  val interface: SMT_Solver.interface
     4.8    val setup: theory -> theory
     4.9 -  val interface: SMT_Solver.interface
    4.10  end
    4.11  
    4.12  structure SMTLIB_Interface: SMTLIB_INTERFACE =
    4.13 @@ -106,7 +106,7 @@
    4.14      | distinct _ _ _ = NONE
    4.15  in
    4.16  
    4.17 -val setup =
    4.18 +val setup_builtins =
    4.19    B.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
    4.20    fold (B.add_builtin_fun' smtlibC) [
    4.21      (@{const True}, "true"),
    4.22 @@ -155,7 +155,7 @@
    4.23    in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
    4.24  
    4.25  
    4.26 -(* serialization *)
    4.27 +(** serialization **)
    4.28  
    4.29  val add = Buffer.add
    4.30  fun sep f = add " " #> f
    4.31 @@ -216,7 +216,7 @@
    4.32  
    4.33  
    4.34  
    4.35 -(** interfaces **)
    4.36 +(* interface *)
    4.37  
    4.38  val interface = {
    4.39    class = smtlibC,
    4.40 @@ -230,4 +230,6 @@
    4.41      has_datatypes = false,
    4.42      serialize = serialize}}
    4.43  
    4.44 +val setup = Context.theory_map setup_builtins
    4.45 +
    4.46  end
     5.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Tue Dec 07 21:58:36 2010 +0100
     5.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Dec 08 08:33:02 2010 +0100
     5.3 @@ -7,8 +7,8 @@
     5.4  signature Z3_INTERFACE =
     5.5  sig
     5.6    val smtlib_z3C: SMT_Config.class
     5.7 +  val interface: SMT_Solver.interface
     5.8    val setup: theory -> theory
     5.9 -  val interface: SMT_Solver.interface
    5.10  
    5.11    datatype sym = Sym of string * sym list
    5.12    type mk_builtins = {
    5.13 @@ -49,12 +49,12 @@
    5.14      else irules
    5.15  
    5.16    fun extra_norm' has_datatypes = extra_norm has_datatypes o add_div_mod
    5.17 +
    5.18 +  val setup_builtins =
    5.19 +    B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    5.20 +    B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    5.21  in
    5.22  
    5.23 -val setup =
    5.24 -  B.add_builtin_fun' smtlib_z3C (@{const z3div}, "div") #>
    5.25 -  B.add_builtin_fun' smtlib_z3C (@{const z3mod}, "mod")
    5.26 -
    5.27  val interface = {
    5.28    class = smtlib_z3C,
    5.29    extra_norm = extra_norm',
    5.30 @@ -65,6 +65,8 @@
    5.31      has_datatypes = true,
    5.32      serialize = serialize}}
    5.33  
    5.34 +val setup = Context.theory_map setup_builtins
    5.35 +
    5.36  end
    5.37  
    5.38  
     6.1 --- a/src/HOL/Word/Tools/smt_word.ML	Tue Dec 07 21:58:36 2010 +0100
     6.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Wed Dec 08 08:33:02 2010 +0100
     6.3 @@ -139,7 +139,8 @@
     6.4  (* setup *)
     6.5  
     6.6  val setup = 
     6.7 -  Context.theory_map (SMTLIB_Interface.add_logic (20, smtlib_logic)) #>
     6.8 -  setup_builtins
     6.9 +  Context.theory_map (
    6.10 +    SMTLIB_Interface.add_logic (20, smtlib_logic) #>
    6.11 +    setup_builtins)
    6.12  
    6.13  end