author | boehmes |
Wed, 15 Dec 2010 08:39:24 +0100 | |
changeset 41124 | 1de17a2de5ad |
parent 41073 | 07b454783ed8 |
child 41126 | e0bd443c0fdd |
permissions | -rw-r--r-- |
40277 | 1 |
(* Title: HOL/Tools/SMT/smt_builtin.ML |
2 |
Author: Sascha Boehme, TU Muenchen |
|
3 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
4 |
Tables of types and terms directly supported by SMT solvers. |
40277 | 5 |
*) |
6 |
||
7 |
signature SMT_BUILTIN = |
|
8 |
sig |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
9 |
(*built-in types*) |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
10 |
val add_builtin_typ: SMT_Utils.class -> |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
11 |
typ * (typ -> string option) * (typ -> int -> string option) -> |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
12 |
Context.generic -> Context.generic |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
13 |
val add_builtin_typ_ext: typ * (typ -> bool) -> Context.generic -> |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
14 |
Context.generic |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
15 |
val builtin_typ: Proof.context -> typ -> string option |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
16 |
val is_builtin_typ: Proof.context -> typ -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
17 |
val is_builtin_typ_ext: Proof.context -> typ -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
18 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
19 |
(*built-in numbers*) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
20 |
val builtin_num: Proof.context -> term -> string option |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
21 |
val is_builtin_num: Proof.context -> term -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
22 |
val is_builtin_num_ext: Proof.context -> term -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
23 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
24 |
(*built-in functions*) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
25 |
type 'a bfun = Proof.context -> typ -> term list -> 'a |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
26 |
val add_builtin_fun: SMT_Utils.class -> |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
27 |
(string * typ) * (string * term list) option bfun -> Context.generic -> |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
28 |
Context.generic |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
29 |
val add_builtin_fun': SMT_Utils.class -> term * string -> Context.generic -> |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
30 |
Context.generic |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
31 |
val add_builtin_fun_ext: (string * typ) * bool bfun -> Context.generic -> |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
32 |
Context.generic |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
33 |
val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
34 |
val add_builtin_fun_ext'': string -> Context.generic -> Context.generic |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
35 |
val builtin_fun: Proof.context -> string * typ -> term list -> |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
36 |
(string * term list) option |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
37 |
val is_builtin_fun: Proof.context -> string * typ -> term list -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
38 |
val is_builtin_pred: Proof.context -> string * typ -> term list -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
39 |
val is_builtin_conn: Proof.context -> string * typ -> term list -> bool |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
40 |
val is_builtin_ext: Proof.context -> string * typ -> term list -> bool |
40277 | 41 |
end |
42 |
||
43 |
structure SMT_Builtin: SMT_BUILTIN = |
|
44 |
struct |
|
45 |
||
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
46 |
structure U = SMT_Utils |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
47 |
structure C = SMT_Config |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
48 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
49 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
50 |
(* built-in tables *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
51 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
52 |
datatype ('a, 'b) kind = Ext of 'a | Int of 'b |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
53 |
|
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
54 |
type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict |
40677
f5caf58e9cdb
more precise characterization of built-in constants "number_of", "0", and "1"
blanchet
parents:
40664
diff
changeset
|
55 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
56 |
fun typ_ord ((T, _), (U, _)) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
57 |
let |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
58 |
fun tord (TVar _, Type _) = GREATER |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
59 |
| tord (Type _, TVar _) = LESS |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
60 |
| tord (Type (n, Ts), Type (m, Us)) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
61 |
if n = m then list_ord tord (Ts, Us) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
62 |
else Term_Ord.typ_ord (T, U) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
63 |
| tord TU = Term_Ord.typ_ord TU |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
64 |
in tord (T, U) end |
40277 | 65 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
66 |
fun insert_ttab cs T f = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
67 |
U.dict_map_default (cs, []) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
68 |
(Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
69 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
70 |
fun merge_ttab ttabp = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
71 |
U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp |
40277 | 72 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
73 |
fun lookup_ttab ctxt ttab T = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
74 |
let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U) |
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
75 |
in |
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
76 |
get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt)) |
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
77 |
end |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
78 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
79 |
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
80 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
81 |
fun empty_btab () = Symtab.empty |
40277 | 82 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
83 |
fun insert_btab cs n T f = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
84 |
Symtab.map_default (n, []) (insert_ttab cs T f) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
85 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
86 |
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp |
40277 | 87 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
88 |
fun lookup_btab ctxt btab (n, T) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
89 |
(case Symtab.lookup btab n of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
90 |
NONE => NONE |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
91 |
| SOME ttab => lookup_ttab ctxt ttab T) |
40277 | 92 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
93 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
94 |
(* built-in types *) |
40277 | 95 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
96 |
structure Builtin_Types = Generic_Data |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
97 |
( |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
98 |
type T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
99 |
(typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
100 |
val empty = [] |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
101 |
val extend = I |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
102 |
val merge = merge_ttab |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
103 |
) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
104 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
105 |
fun add_builtin_typ cs (T, f, g) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
106 |
Builtin_Types.map (insert_ttab cs T (Int (f, g))) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
107 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
108 |
fun add_builtin_typ_ext (T, f) = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
109 |
Builtin_Types.map (insert_ttab U.basicC T (Ext f)) |
40277 | 110 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
111 |
fun lookup_builtin_typ ctxt = |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
112 |
lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt)) |
40277 | 113 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
114 |
fun builtin_typ ctxt T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
115 |
(case lookup_builtin_typ ctxt T of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
116 |
SOME (_, Int (f, _)) => f T |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
117 |
| _ => NONE) |
40277 | 118 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
119 |
fun is_builtin_typ ctxt T = is_some (builtin_typ ctxt T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
120 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
121 |
fun is_builtin_typ_ext ctxt T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
122 |
(case lookup_builtin_typ ctxt T of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
123 |
SOME (_, Int (f, _)) => is_some (f T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
124 |
| SOME (_, Ext f) => f T |
40277 | 125 |
| NONE => false) |
126 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
127 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
128 |
(* built-in numbers *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
129 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
130 |
fun builtin_num ctxt t = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
131 |
(case try HOLogic.dest_number t of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
132 |
NONE => NONE |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
133 |
| SOME (T, i) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
134 |
(case lookup_builtin_typ ctxt T of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
135 |
SOME (_, Int (_, g)) => g T i |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
136 |
| _ => NONE)) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
137 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
138 |
val is_builtin_num = is_some oo builtin_num |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
139 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
140 |
fun is_builtin_num_ext ctxt t = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
141 |
(case try HOLogic.dest_number t of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
142 |
NONE => false |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
143 |
| SOME (T, _) => is_builtin_typ_ext ctxt T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
144 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
145 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
146 |
(* built-in functions *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
147 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
148 |
type 'a bfun = Proof.context -> typ -> term list -> 'a |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
149 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
150 |
fun true3 _ _ _ = true |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
151 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
152 |
fun raw_add_builtin_fun_ext thy cs n = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
153 |
insert_btab cs n (Sign.the_const_type thy n) (Ext true3) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
154 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
155 |
val basic_builtin_fun_names = [ |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
156 |
@{const_name SMT.pat}, @{const_name SMT.nopat}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
157 |
@{const_name SMT.trigger}, @{const_name SMT.weight}] |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
158 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
159 |
type builtin_funcs = (bool bfun, (string * term list) option bfun) btab |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
160 |
|
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
161 |
fun basic_builtin_funcs () : builtin_funcs = |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
162 |
empty_btab () |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
163 |
|> fold (raw_add_builtin_fun_ext @{theory} U.basicC) basic_builtin_fun_names |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
164 |
(* FIXME: SMT_Normalize should check that they are properly used *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
165 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
166 |
structure Builtin_Funcs = Generic_Data |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
167 |
( |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
168 |
type T = builtin_funcs |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
169 |
val empty = basic_builtin_funcs () |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
170 |
val extend = I |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
171 |
val merge = merge_btab |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
172 |
) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
173 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
174 |
fun add_builtin_fun cs ((n, T), f) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
175 |
Builtin_Funcs.map (insert_btab cs n T (Int f)) |
40277 | 176 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
177 |
fun add_builtin_fun' cs (t, n) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
178 |
add_builtin_fun cs (Term.dest_Const t, fn _ => fn _ => SOME o pair n) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
179 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
180 |
fun add_builtin_fun_ext ((n, T), f) = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
181 |
Builtin_Funcs.map (insert_btab U.basicC n T (Ext f)) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
182 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
183 |
fun add_builtin_fun_ext' c = add_builtin_fun_ext (c, true3) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
184 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
185 |
fun add_builtin_fun_ext'' n context = |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
186 |
let val thy = Context.theory_of context |
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
187 |
in add_builtin_fun_ext' (n, Sign.the_const_type thy n) context end |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
188 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
189 |
fun lookup_builtin_fun ctxt = |
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
190 |
lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt)) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
191 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
192 |
fun builtin_fun ctxt (c as (_, T)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
193 |
(case lookup_builtin_fun ctxt c of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
194 |
SOME (_, Int f) => f ctxt T ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
195 |
| _ => NONE) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
196 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
197 |
fun is_builtin_fun ctxt c ts = is_some (builtin_fun ctxt c ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
198 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
199 |
fun is_special_builtin_fun pred ctxt (c as (_, T)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
200 |
(case lookup_builtin_fun ctxt c of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
201 |
SOME (U, Int f) => pred U andalso is_some (f ctxt T ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
202 |
| _ => false) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
203 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
204 |
fun is_pred_type T = Term.body_type T = @{typ bool} |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
205 |
fun is_conn_type T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
206 |
forall (equal @{typ bool}) (Term.body_type T :: Term.binder_types T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
207 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
208 |
fun is_builtin_pred ctxt = is_special_builtin_fun is_pred_type ctxt |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
209 |
fun is_builtin_conn ctxt = is_special_builtin_fun is_conn_type ctxt |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
210 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
211 |
fun is_builtin_fun_ext ctxt (c as (_, T)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
212 |
(case lookup_builtin_fun ctxt c of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
213 |
SOME (_, Int f) => is_some (f ctxt T ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
214 |
| SOME (_, Ext f) => f ctxt T ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
215 |
| NONE => false) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
216 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
217 |
(* FIXME: move this information to the interfaces *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
218 |
val only_partially_supported = [ |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
219 |
@{const_name times}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
220 |
@{const_name div_class.div}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
221 |
@{const_name div_class.mod}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
222 |
@{const_name inverse_class.divide} ] |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
223 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
224 |
fun is_builtin_ext ctxt (c as (n, _)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
225 |
if member (op =) only_partially_supported n then false |
41073 | 226 |
else |
227 |
is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse |
|
228 |
is_builtin_fun_ext ctxt c ts |
|
40277 | 229 |
|
230 |
end |