src/HOL/Tools/SMT/smt_builtin.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66551 4df6b0ae900d
child 67149 e61557884799
permissions -rw-r--r--
more symbols;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/smt_builtin.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Tables of types and terms directly supported by SMT solvers.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature SMT_BUILTIN =
blanchet@56078
     8
sig
blanchet@56078
     9
  (*for experiments*)
blanchet@56078
    10
  val filter_builtins: (typ -> bool) -> Proof.context -> Proof.context
blanchet@56078
    11
blanchet@56078
    12
  (*built-in types*)
blanchet@58061
    13
  val add_builtin_typ: SMT_Util.class ->
blanchet@66551
    14
    typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
blanchet@56090
    15
    Context.generic
blanchet@66298
    16
  val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
blanchet@56078
    17
    Context.generic
blanchet@66551
    18
  val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
blanchet@56078
    19
  val is_builtin_typ_ext: Proof.context -> typ -> bool
blanchet@56078
    20
blanchet@56078
    21
  (*built-in numbers*)
blanchet@56078
    22
  val dest_builtin_num: Proof.context -> term -> (string * typ) option
blanchet@56078
    23
  val is_builtin_num: Proof.context -> term -> bool
blanchet@56078
    24
  val is_builtin_num_ext: Proof.context -> term -> bool
blanchet@56078
    25
blanchet@56078
    26
  (*built-in functions*)
blanchet@56078
    27
  type 'a bfun = Proof.context -> typ -> term list -> 'a
blanchet@56078
    28
  type bfunr = string * int * term list * (term list -> term)
blanchet@58061
    29
  val add_builtin_fun: SMT_Util.class -> (string * typ) * bfunr option bfun -> Context.generic ->
blanchet@56078
    30
    Context.generic
blanchet@58061
    31
  val add_builtin_fun': SMT_Util.class -> term * string -> Context.generic -> Context.generic
blanchet@56103
    32
  val add_builtin_fun_ext: (string * typ) * term list bfun -> Context.generic -> Context.generic
blanchet@56078
    33
  val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
blanchet@56078
    34
  val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
blanchet@56103
    35
  val dest_builtin_fun: Proof.context -> string * typ -> term list -> bfunr option
blanchet@56078
    36
  val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
blanchet@56103
    37
  val dest_builtin_pred: Proof.context -> string * typ -> term list -> bfunr option
blanchet@56103
    38
  val dest_builtin_conn: Proof.context -> string * typ -> term list -> bfunr option
blanchet@56078
    39
  val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
blanchet@56103
    40
  val dest_builtin_ext: Proof.context -> string * typ -> term list -> term list option
blanchet@56078
    41
  val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
blanchet@56078
    42
  val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
blanchet@57229
    43
end;
blanchet@56078
    44
blanchet@58061
    45
structure SMT_Builtin: SMT_BUILTIN =
blanchet@56078
    46
struct
blanchet@56078
    47
blanchet@56078
    48
blanchet@56078
    49
(* built-in tables *)
blanchet@56078
    50
blanchet@56078
    51
datatype ('a, 'b) kind = Ext of 'a | Int of 'b
blanchet@56078
    52
blanchet@58061
    53
type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Util.dict
blanchet@56078
    54
blanchet@56078
    55
fun typ_ord ((T, _), (U, _)) =
blanchet@56078
    56
  let
blanchet@56078
    57
    fun tord (TVar _, Type _) = GREATER
blanchet@56078
    58
      | tord (Type _, TVar _) = LESS
blanchet@56078
    59
      | tord (Type (n, Ts), Type (m, Us)) =
blanchet@56078
    60
          if n = m then list_ord tord (Ts, Us)
blanchet@56078
    61
          else Term_Ord.typ_ord (T, U)
blanchet@56078
    62
      | tord TU = Term_Ord.typ_ord TU
blanchet@56078
    63
  in tord (T, U) end
blanchet@56078
    64
blanchet@56078
    65
fun insert_ttab cs T f =
blanchet@58061
    66
  SMT_Util.dict_map_default (cs, [])
blanchet@56078
    67
    (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f))
blanchet@56078
    68
blanchet@58061
    69
fun merge_ttab ttabp = SMT_Util.dict_merge (Ord_List.merge typ_ord) ttabp
blanchet@56078
    70
blanchet@56078
    71
fun lookup_ttab ctxt ttab T =
blanchet@56078
    72
  let fun match (U, _) = Sign.typ_instance (Proof_Context.theory_of ctxt) (T, U)
blanchet@56078
    73
  in
blanchet@58061
    74
    get_first (find_first match) (SMT_Util.dict_lookup ttab (SMT_Config.solver_class_of ctxt))
blanchet@56078
    75
  end
blanchet@56078
    76
blanchet@56078
    77
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table
blanchet@56078
    78
blanchet@56078
    79
fun insert_btab cs n T f =
blanchet@56078
    80
  Symtab.map_default (n, []) (insert_ttab cs T f)
blanchet@56078
    81
blanchet@56078
    82
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp
blanchet@56078
    83
blanchet@56078
    84
fun lookup_btab ctxt btab (n, T) =
blanchet@56078
    85
  (case Symtab.lookup btab n of
blanchet@56078
    86
    NONE => NONE
blanchet@56078
    87
  | SOME ttab => lookup_ttab ctxt ttab T)
blanchet@56078
    88
blanchet@56078
    89
type 'a bfun = Proof.context -> typ -> term list -> 'a
blanchet@56078
    90
blanchet@56078
    91
type bfunr = string * int * term list * (term list -> term)
blanchet@56078
    92
blanchet@56078
    93
structure Builtins = Generic_Data
blanchet@56078
    94
(
blanchet@56078
    95
  type T =
blanchet@66551
    96
    (Proof.context -> typ -> bool,
blanchet@66551
    97
     (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
blanchet@56078
    98
    (term list bfun, bfunr option bfun) btab
blanchet@56078
    99
  val empty = ([], Symtab.empty)
blanchet@56078
   100
  val extend = I
blanchet@56078
   101
  fun merge ((t1, b1), (t2, b2)) = (merge_ttab (t1, t2), merge_btab (b1, b2))
blanchet@56078
   102
)
blanchet@56078
   103
blanchet@56078
   104
fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst)))
blanchet@56078
   105
blanchet@56078
   106
fun filter_builtins keep_T =
blanchet@56078
   107
  Context.proof_map (Builtins.map (fn (ttab, btab) =>
blanchet@56078
   108
    (filter_ttab keep_T ttab, Symtab.map (K (filter_ttab keep_T)) btab)))
blanchet@56078
   109
blanchet@56078
   110
blanchet@56078
   111
(* built-in types *)
blanchet@56078
   112
blanchet@56078
   113
fun add_builtin_typ cs (T, f, g) =
blanchet@56078
   114
  Builtins.map (apfst (insert_ttab cs T (Int (f, g))))
blanchet@56078
   115
blanchet@58061
   116
fun add_builtin_typ_ext (T, f) = Builtins.map (apfst (insert_ttab SMT_Util.basicC T (Ext f)))
blanchet@56078
   117
blanchet@56078
   118
fun lookup_builtin_typ ctxt =
blanchet@56078
   119
  lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt)))
blanchet@56078
   120
blanchet@56078
   121
fun dest_builtin_typ ctxt T =
blanchet@56078
   122
  (case lookup_builtin_typ ctxt T of
blanchet@56078
   123
    SOME (_, Int (f, _)) => f T
blanchet@57230
   124
  | _ => NONE)
blanchet@56078
   125
blanchet@56078
   126
fun is_builtin_typ_ext ctxt T =
blanchet@56078
   127
  (case lookup_builtin_typ ctxt T of
blanchet@56078
   128
    SOME (_, Int (f, _)) => is_some (f T)
blanchet@66298
   129
  | SOME (_, Ext f) => f ctxt T
blanchet@56078
   130
  | NONE => false)
blanchet@56078
   131
blanchet@56078
   132
blanchet@56078
   133
(* built-in numbers *)
blanchet@56078
   134
blanchet@56078
   135
fun dest_builtin_num ctxt t =
blanchet@56078
   136
  (case try HOLogic.dest_number t of
blanchet@56078
   137
    NONE => NONE
blanchet@56078
   138
  | SOME (T, i) =>
blanchet@56078
   139
      if i < 0 then NONE else
blanchet@56078
   140
        (case lookup_builtin_typ ctxt T of
blanchet@56078
   141
          SOME (_, Int (_, g)) => g T i |> Option.map (rpair T)
blanchet@56078
   142
        | _ => NONE))
blanchet@56078
   143
blanchet@56078
   144
val is_builtin_num = is_some oo dest_builtin_num
blanchet@56078
   145
blanchet@56078
   146
fun is_builtin_num_ext ctxt t =
blanchet@56078
   147
  (case try HOLogic.dest_number t of
blanchet@56078
   148
    NONE => false
blanchet@56078
   149
  | SOME (T, _) => is_builtin_typ_ext ctxt T)
blanchet@56078
   150
blanchet@56078
   151
blanchet@56078
   152
(* built-in functions *)
blanchet@56078
   153
blanchet@56078
   154
fun add_builtin_fun cs ((n, T), f) =
blanchet@56078
   155
  Builtins.map (apsnd (insert_btab cs n T (Int f)))
blanchet@56078
   156
blanchet@56078
   157
fun add_builtin_fun' cs (t, n) =
blanchet@56078
   158
  let
blanchet@56078
   159
    val c as (m, T) = Term.dest_Const t
blanchet@56078
   160
    fun app U ts = Term.list_comb (Const (m, U), ts)
blanchet@56078
   161
    fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U)
blanchet@56078
   162
  in add_builtin_fun cs (c, bfun) end
blanchet@56078
   163
blanchet@56078
   164
fun add_builtin_fun_ext ((n, T), f) =
blanchet@58061
   165
  Builtins.map (apsnd (insert_btab SMT_Util.basicC n T (Ext f)))
blanchet@56078
   166
blanchet@56078
   167
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I)
blanchet@56078
   168
blanchet@56078
   169
fun add_builtin_fun_ext'' n context =
blanchet@56078
   170
  let val thy = Context.theory_of context
blanchet@56078
   171
  in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end
blanchet@56078
   172
blanchet@56078
   173
fun lookup_builtin_fun ctxt =
blanchet@56078
   174
  lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt)))
blanchet@56078
   175
blanchet@56078
   176
fun dest_builtin_fun ctxt (c as (_, T)) ts =
blanchet@56078
   177
  (case lookup_builtin_fun ctxt c of
blanchet@56078
   178
    SOME (_, Int f) => f ctxt T ts
blanchet@56078
   179
  | _ => NONE)
blanchet@56078
   180
blanchet@56078
   181
fun dest_builtin_eq ctxt t u =
blanchet@56078
   182
  let
blanchet@56078
   183
    val aT = TFree (Name.aT, @{sort type})
blanchet@56078
   184
    val c = (@{const_name HOL.eq}, aT --> aT --> @{typ bool})
blanchet@56078
   185
    fun mk ts = Term.list_comb (HOLogic.eq_const (Term.fastype_of (hd ts)), ts)
blanchet@56078
   186
  in
blanchet@56078
   187
    dest_builtin_fun ctxt c []
blanchet@56078
   188
    |> Option.map (fn (n, i, _, _) => (n, i, [t, u], mk))
blanchet@56078
   189
  end
blanchet@56078
   190
blanchet@56078
   191
fun special_builtin_fun pred ctxt (c as (_, T)) ts =
blanchet@56078
   192
  if pred (Term.body_type T, Term.binder_types T) then
blanchet@56078
   193
    dest_builtin_fun ctxt c ts
blanchet@56078
   194
  else NONE
blanchet@56078
   195
blanchet@56078
   196
fun dest_builtin_pred ctxt = special_builtin_fun (equal @{typ bool} o fst) ctxt
blanchet@56078
   197
blanchet@56078
   198
fun dest_builtin_conn ctxt =
blanchet@56078
   199
  special_builtin_fun (forall (equal @{typ bool}) o (op ::)) ctxt
blanchet@56078
   200
blanchet@56078
   201
fun dest_builtin ctxt c ts =
blanchet@56078
   202
  let val t = Term.list_comb (Const c, ts)
blanchet@56078
   203
  in
blanchet@56078
   204
    (case dest_builtin_num ctxt t of
blanchet@56078
   205
      SOME (n, _) => SOME (n, 0, [], K t)
blanchet@56078
   206
    | NONE => dest_builtin_fun ctxt c ts)
blanchet@56078
   207
  end
blanchet@56078
   208
blanchet@57230
   209
fun dest_builtin_fun_ext ctxt (c as (_, T)) ts =
blanchet@56078
   210
  (case lookup_builtin_fun ctxt c of
blanchet@56078
   211
    SOME (_, Int f) => f ctxt T ts |> Option.map (fn (_, _, us, _) => us)
blanchet@56078
   212
  | SOME (_, Ext f) => SOME (f ctxt T ts)
blanchet@56078
   213
  | NONE => NONE)
blanchet@56078
   214
blanchet@56078
   215
fun dest_builtin_ext ctxt c ts =
blanchet@56078
   216
  if is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) then SOME []
blanchet@56078
   217
  else dest_builtin_fun_ext ctxt c ts
blanchet@56078
   218
blanchet@56078
   219
fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts)
blanchet@56078
   220
blanchet@56078
   221
fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts)
blanchet@56078
   222
blanchet@57229
   223
end;