1(* Title: HOL/Tools/SMT/smt_builtin.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Tables of types and terms directly supported by SMT solvers. 5*) 6 7signature SMT_BUILTIN = 8sig 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 43end; 44 45structure SMT_Builtin: SMT_BUILTIN = 46struct 47 48 49(* built-in tables *) 50 51datatype ('a, 'b) kind = Ext of 'a | Int of 'b 52 53type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Util.dict 54 55fun 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 65fun 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 69fun merge_ttab ttabp = SMT_Util.dict_merge (Ord_List.merge typ_ord) ttabp 70 71fun 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 77type ('a, 'b) btab = ('a, 'b) ttab Symtab.table 78 79fun insert_btab cs n T f = 80 Symtab.map_default (n, []) (insert_ttab cs T f) 81 82fun merge_btab btabp = Symtab.join (K merge_ttab) btabp 83 84fun 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 89type 'a bfun = Proof.context -> typ -> term list -> 'a 90 91type bfunr = string * int * term list * (term list -> term) 92 93structure 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 104fun filter_ttab keep_T = map (apsnd (filter (keep_T o fst))) 105 106fun 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 113fun add_builtin_typ cs (T, f, g) = 114 Builtins.map (apfst (insert_ttab cs T (Int (f, g)))) 115 116fun add_builtin_typ_ext (T, f) = Builtins.map (apfst (insert_ttab SMT_Util.basicC T (Ext f))) 117 118fun lookup_builtin_typ ctxt = 119 lookup_ttab ctxt (fst (Builtins.get (Context.Proof ctxt))) 120 121fun dest_builtin_typ ctxt T = 122 (case lookup_builtin_typ ctxt T of 123 SOME (_, Int (f, _)) => f T 124 | _ => NONE) 125 126fun 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 135fun 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 144val is_builtin_num = is_some oo dest_builtin_num 145 146fun 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 154fun add_builtin_fun cs ((n, T), f) = 155 Builtins.map (apsnd (insert_btab cs n T (Int f))) 156 157fun 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 164fun add_builtin_fun_ext ((n, T), f) = 165 Builtins.map (apsnd (insert_btab SMT_Util.basicC n T (Ext f))) 166 167fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, fn _ => fn _ => I) 168 169fun 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 173fun lookup_builtin_fun ctxt = 174 lookup_btab ctxt (snd (Builtins.get (Context.Proof ctxt))) 175 176fun 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 181fun dest_builtin_eq ctxt t u = 182 let 183 val aT = Term.aT \<^sort>\<open>type\<close> 184 val c = (\<^const_name>\<open>HOL.eq\<close>, aT --> aT --> \<^typ>\<open>bool\<close>) 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 191fun 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 196fun dest_builtin_pred ctxt = special_builtin_fun (equal \<^typ>\<open>bool\<close> o fst) ctxt 197 198fun dest_builtin_conn ctxt = 199 special_builtin_fun (forall (equal \<^typ>\<open>bool\<close>) o (op ::)) ctxt 200 201fun 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 209fun 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 215fun 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 219fun is_builtin_fun ctxt c ts = is_some (dest_builtin_fun ctxt c ts) 220 221fun is_builtin_fun_ext ctxt c ts = is_some (dest_builtin_fun_ext ctxt c ts) 222 223end; 224