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