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