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