src/HOL/Tools/SMT/smt_builtin.ML
author boehmes
Tue Dec 07 14:53:12 2010 +0100 (2010-12-07)
changeset 41059 d2b1fc1b8e19
parent 40691 a68f64f99832
child 41072 9f9bc1bdacef
permissions -rw-r--r--
centralized handling of built-in types and constants;
also store types and constants which are rewritten during preprocessing;
interfaces are identified by classes (supporting inheritance, at least on the level of built-in symbols);
removed term_eq in favor of type replacements: term-level occurrences of type bool are replaced by type term_bool (only for the translation)
boehmes@40277
     1
(*  Title:      HOL/Tools/SMT/smt_builtin.ML
boehmes@40277
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@40277
     3
boehmes@41059
     4
Tables of types and terms directly supported by SMT solvers.
boehmes@40277
     5
*)
boehmes@40277
     6
boehmes@40277
     7
signature SMT_BUILTIN =
boehmes@40277
     8
sig
boehmes@41059
     9
  (*built-in types*)
boehmes@41059
    10
  val add_builtin_typ: SMT_Config.class ->
boehmes@41059
    11
    typ * (typ -> string option) * (typ -> int -> string option) -> theory ->
boehmes@41059
    12
    theory
boehmes@41059
    13
  val add_builtin_typ_ext: typ * (typ -> bool) -> theory -> theory
boehmes@41059
    14
  val builtin_typ: Proof.context -> typ -> string option
boehmes@41059
    15
  val is_builtin_typ: Proof.context -> typ -> bool
boehmes@41059
    16
  val is_builtin_typ_ext: Proof.context -> typ -> bool
boehmes@41059
    17
boehmes@41059
    18
  (*built-in numbers*)
boehmes@41059
    19
  val builtin_num: Proof.context -> term -> string option
boehmes@41059
    20
  val is_builtin_num: Proof.context -> term -> bool
boehmes@41059
    21
  val is_builtin_num_ext: Proof.context -> term -> bool
boehmes@41059
    22
boehmes@41059
    23
  (*built-in functions*)
boehmes@41059
    24
  type 'a bfun = Proof.context -> typ -> term list -> 'a
boehmes@41059
    25
  val add_builtin_fun: SMT_Config.class ->
boehmes@41059
    26
    (string * typ) * (string * term list) option bfun -> theory -> theory
boehmes@41059
    27
  val add_builtin_fun': SMT_Config.class -> term * string -> theory -> theory
boehmes@41059
    28
  val add_builtin_fun_ext: (string * typ) * bool bfun -> theory -> theory
boehmes@41059
    29
  val add_builtin_fun_ext': string * typ -> theory -> theory
boehmes@41059
    30
  val add_builtin_fun_ext'': string -> theory -> theory
boehmes@41059
    31
  val builtin_fun: Proof.context -> string * typ -> term list ->
boehmes@41059
    32
    (string * term list) option
boehmes@41059
    33
  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    34
  val is_builtin_pred: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    35
  val is_builtin_conn: Proof.context -> string * typ -> term list -> bool
boehmes@41059
    36
  val is_builtin_ext: Proof.context -> string * typ -> term list -> bool
boehmes@40277
    37
end
boehmes@40277
    38
boehmes@40277
    39
structure SMT_Builtin: SMT_BUILTIN =
boehmes@40277
    40
struct
boehmes@40277
    41
boehmes@41059
    42
structure C = SMT_Config
boehmes@41059
    43
boehmes@41059
    44
boehmes@41059
    45
(* built-in tables *)
boehmes@41059
    46
boehmes@41059
    47
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
boehmes@41059
    48
boehmes@41059
    49
type ('a, 'b) ttab = (C.class * (typ * ('a, 'b) kind) Ord_List.T) list 
blanchet@40677
    50
boehmes@41059
    51
fun empty_ttab () = []
boehmes@40277
    52
boehmes@41059
    53
fun typ_ord ((T, _), (U, _)) =
boehmes@41059
    54
  let
boehmes@41059
    55
    fun tord (TVar _, Type _) = GREATER
boehmes@41059
    56
      | tord (Type _, TVar _) = LESS
boehmes@41059
    57
      | tord (Type (n, Ts), Type (m, Us)) =
boehmes@41059
    58
          if n = m then list_ord tord (Ts, Us)
boehmes@41059
    59
          else Term_Ord.typ_ord (T, U)
boehmes@41059
    60
      | tord TU = Term_Ord.typ_ord TU
boehmes@41059
    61
  in tord (T, U) end
boehmes@40277
    62
boehmes@41059
    63
fun insert_ttab cs T f =
boehmes@41059
    64
  AList.map_default (op =) (cs, [])
boehmes@41059
    65
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
boehmes@41059
    66
boehmes@41059
    67
fun merge_ttab ttabp =
boehmes@41059
    68
  AList.join (op =) (K (uncurry (Ord_List.union typ_ord) o swap)) ttabp
boehmes@40277
    69
boehmes@41059
    70
fun lookup_ttab ctxt ttab T =
boehmes@41059
    71
  let
boehmes@41059
    72
    val cs = C.solver_class_of ctxt
boehmes@41059
    73
    fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U)
boehmes@41059
    74
boehmes@41059
    75
    fun matching (cs', Txs) =
boehmes@41059
    76
      if is_prefix (op =) cs' cs then find_first match Txs
boehmes@41059
    77
      else NONE
boehmes@41059
    78
  in get_first matching ttab end
boehmes@41059
    79
boehmes@41059
    80
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
boehmes@41059
    81
boehmes@41059
    82
fun empty_btab () = Symtab.empty
boehmes@40277
    83
boehmes@41059
    84
fun insert_btab cs n T f =
boehmes@41059
    85
  Symtab.map_default (n, []) (insert_ttab cs T f)
boehmes@41059
    86
boehmes@41059
    87
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
boehmes@40277
    88
boehmes@41059
    89
fun lookup_btab ctxt btab (n, T) =
boehmes@41059
    90
  (case Symtab.lookup btab n of
boehmes@41059
    91
    NONE => NONE
boehmes@41059
    92
  | SOME ttab => lookup_ttab ctxt ttab T)
boehmes@40277
    93
boehmes@41059
    94
boehmes@41059
    95
(* built-in types *)
boehmes@40277
    96
boehmes@41059
    97
structure Builtin_Types = Theory_Data
boehmes@41059
    98
(
boehmes@41059
    99
  type T =
boehmes@41059
   100
    (typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab
boehmes@41059
   101
  val empty = empty_ttab ()
boehmes@41059
   102
  val extend = I
boehmes@41059
   103
  val merge = merge_ttab
boehmes@41059
   104
)
boehmes@41059
   105
boehmes@41059
   106
fun add_builtin_typ cs (T, f, g) =
boehmes@41059
   107
  Builtin_Types.map (insert_ttab cs T (Int (f, g)))
boehmes@41059
   108
boehmes@41059
   109
fun add_builtin_typ_ext (T, f) =
boehmes@41059
   110
  Builtin_Types.map (insert_ttab C.basicC T (Ext f))
boehmes@40277
   111
boehmes@41059
   112
fun lookup_builtin_typ ctxt =
boehmes@41059
   113
  lookup_ttab ctxt (Builtin_Types.get (ProofContext.theory_of ctxt))
boehmes@40277
   114
boehmes@41059
   115
fun builtin_typ ctxt T =
boehmes@41059
   116
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   117
    SOME (_, Int (f, _)) => f T
boehmes@41059
   118
  | _ => NONE) 
boehmes@40277
   119
boehmes@41059
   120
fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T)
boehmes@41059
   121
boehmes@41059
   122
fun is_builtin_typ_ext ctxt T =
boehmes@41059
   123
  (case lookup_builtin_typ ctxt T of
boehmes@41059
   124
    SOME (_, Int (f, _)) => is_some (f T)
boehmes@41059
   125
  | SOME (_, Ext f) => f T
boehmes@40277
   126
  | NONE => false)
boehmes@40277
   127
boehmes@41059
   128
boehmes@41059
   129
(* built-in numbers *)
boehmes@41059
   130
boehmes@41059
   131
fun builtin_num ctxt t =
boehmes@41059
   132
  (case try HOLogic.dest_number t of
boehmes@41059
   133
    NONE => NONE
boehmes@41059
   134
  | SOME (T, i) =>
boehmes@41059
   135
      (case lookup_builtin_typ ctxt T of
boehmes@41059
   136
        SOME (_, Int (_, g)) => g T i
boehmes@41059
   137
      | _ => NONE))
boehmes@41059
   138
boehmes@41059
   139
val is_builtin_num = is_some oo builtin_num
boehmes@41059
   140
boehmes@41059
   141
fun is_builtin_num_ext ctxt t =
boehmes@41059
   142
  (case try HOLogic.dest_number t of
boehmes@41059
   143
    NONE => false
boehmes@41059
   144
  | SOME (T, _) => is_builtin_typ_ext ctxt T)
boehmes@41059
   145
boehmes@41059
   146
boehmes@41059
   147
(* built-in functions *)
boehmes@41059
   148
boehmes@41059
   149
type 'a bfun = Proof.context -> typ -> term list -> 'a
boehmes@41059
   150
boehmes@41059
   151
fun true3 _ _ _ = true
boehmes@41059
   152
boehmes@41059
   153
fun raw_add_builtin_fun_ext thy cs n =
boehmes@41059
   154
  insert_btab cs n (Sign.the_const_type thy n) (Ext true3)
boehmes@41059
   155
boehmes@41059
   156
val basic_builtin_fun_names = [
boehmes@41059
   157
  @{const_name SMT.pat}, @{const_name SMT.nopat},
boehmes@41059
   158
  @{const_name SMT.trigger}, @{const_name SMT.weight}]
boehmes@41059
   159
boehmes@41059
   160
fun basic_builtin_funcs () =
boehmes@41059
   161
  empty_btab ()
boehmes@41059
   162
  |> fold (raw_add_builtin_fun_ext @{theory} C.basicC) basic_builtin_fun_names
boehmes@41059
   163
       (* FIXME: SMT_Normalize should check that they are properly used *)
boehmes@41059
   164
boehmes@41059
   165
structure Builtin_Funcs = Theory_Data
boehmes@41059
   166
(
boehmes@41059
   167
  type T = (bool bfun, (string * term list) option bfun) btab
boehmes@41059
   168
  val empty = basic_builtin_funcs ()
boehmes@41059
   169
  val extend = I
boehmes@41059
   170
  val merge = merge_btab
boehmes@41059
   171
)
boehmes@41059
   172
boehmes@41059
   173
fun add_builtin_fun cs ((n, T), f) =
boehmes@41059
   174
  Builtin_Funcs.map (insert_btab cs n T (Int f))
boehmes@40277
   175
boehmes@41059
   176
fun add_builtin_fun' cs (t, n) =
boehmes@41059
   177
  add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n)
boehmes@41059
   178
boehmes@41059
   179
fun add_builtin_fun_ext ((n, T), f) =
boehmes@41059
   180
  Builtin_Funcs.map (insert_btab C.basicC n T (Ext f))
boehmes@41059
   181
boehmes@41059
   182
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3)
boehmes@41059
   183
boehmes@41059
   184
fun add_builtin_fun_ext'' n thy =
boehmes@41059
   185
  add_builtin_fun_ext' (n, Sign.the_const_type thy n) thy
boehmes@41059
   186
boehmes@41059
   187
fun lookup_builtin_fun ctxt =
boehmes@41059
   188
  lookup_btab ctxt (Builtin_Funcs.get (ProofContext.theory_of ctxt))
boehmes@41059
   189
boehmes@41059
   190
fun builtin_fun ctxt (c as (_, T)) ts =
boehmes@41059
   191
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   192
    SOME (_, Int f) => f ctxt T ts
boehmes@41059
   193
  | _ => NONE)
boehmes@41059
   194
boehmes@41059
   195
fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts)
boehmes@41059
   196
boehmes@41059
   197
fun is_special_builtin_fun pred ctxt (c as (_, T)) ts =
boehmes@41059
   198
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   199
    SOME (U, Int f) => pred U andalso is_some (f ctxt T ts)
boehmes@41059
   200
  | _ => false)
boehmes@41059
   201
boehmes@41059
   202
fun is_pred_type T = Term.body_type T = @{typ bool}
boehmes@41059
   203
fun is_conn_type T =
boehmes@41059
   204
  forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T)
boehmes@41059
   205
boehmes@41059
   206
fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt
boehmes@41059
   207
fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt
boehmes@41059
   208
boehmes@41059
   209
fun is_builtin_fun_ext ctxt (c as (_, T)) ts =
boehmes@41059
   210
  (case lookup_builtin_fun ctxt c of
boehmes@41059
   211
    SOME (_, Int f) => is_some (f ctxt T ts)
boehmes@41059
   212
  | SOME (_, Ext f) => f ctxt T ts
boehmes@41059
   213
  | NONE => false)
boehmes@41059
   214
boehmes@41059
   215
(* FIXME: move this information to the interfaces *)
boehmes@41059
   216
val only_partially_supported = [
boehmes@41059
   217
  @{const_name times},
boehmes@41059
   218
  @{const_name div_class.div},
boehmes@41059
   219
  @{const_name div_class.mod},
boehmes@41059
   220
  @{const_name inverse_class.divide} ]
boehmes@41059
   221
boehmes@41059
   222
fun is_builtin_ext ctxt (c as (n, _)) ts =
boehmes@41059
   223
  if member (op =) only_partially_supported n then false
boehmes@41059
   224
  else is_builtin_fun_ext ctxt c ts
boehmes@40277
   225
boehmes@40277
   226
end