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