author | boehmes |
Wed, 15 Dec 2010 10:12:44 +0100 | |
changeset 41127 | 2ea84c8535c6 |
parent 41126 | e0bd443c0fdd |
child 41280 | a7de9d36f4f2 |
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*) |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
20 |
val builtin_num: Proof.context -> term -> (string * typ) option |
41059
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 -> |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
27 |
(string * typ) * (((string * int) * typ) * term list * typ) option bfun -> |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
28 |
Context.generic -> 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 -> |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
36 |
(((string * int) * typ) * term list * typ) option |
41059
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 |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
38 |
val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
39 |
val is_builtin_ext: Proof.context -> string * typ -> term list -> bool |
40277 | 40 |
end |
41 |
||
42 |
structure SMT_Builtin: SMT_BUILTIN = |
|
43 |
struct |
|
44 |
||
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
45 |
structure U = SMT_Utils |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
46 |
structure C = SMT_Config |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
47 |
|
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 |
(* built-in tables *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
50 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
51 |
datatype ('a, 'b) kind = Ext of 'a | Int of 'b |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
52 |
|
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
53 |
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
|
54 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
55 |
fun typ_ord ((T, _), (U, _)) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
56 |
let |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
57 |
fun tord (TVar _, Type _) = GREATER |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
58 |
| tord (Type _, TVar _) = LESS |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
59 |
| tord (Type (n, Ts), Type (m, Us)) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
60 |
if n = m then list_ord tord (Ts, Us) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
61 |
else Term_Ord.typ_ord (T, U) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
62 |
| tord TU = Term_Ord.typ_ord TU |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
63 |
in tord (T, U) end |
40277 | 64 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
65 |
fun insert_ttab cs T f = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
66 |
U.dict_map_default (cs, []) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
67 |
(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
|
68 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
69 |
fun merge_ttab ttabp = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
70 |
U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp |
40277 | 71 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
72 |
fun lookup_ttab ctxt ttab T = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
73 |
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
|
74 |
in |
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
75 |
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
|
76 |
end |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
77 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
78 |
type ('a, 'b) btab = ('a, 'b) ttab Symtab.table |
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 |
fun insert_btab cs n T f = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
81 |
Symtab.map_default (n, []) (insert_ttab cs T f) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
82 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
83 |
fun merge_btab btabp = Symtab.join (K merge_ttab) btabp |
40277 | 84 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
85 |
fun lookup_btab ctxt btab (n, T) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
86 |
(case Symtab.lookup btab n of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
87 |
NONE => NONE |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
88 |
| SOME ttab => lookup_ttab ctxt ttab T) |
40277 | 89 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
90 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
91 |
(* built-in types *) |
40277 | 92 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
93 |
structure Builtin_Types = Generic_Data |
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 |
type T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
96 |
(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
|
97 |
val empty = [] |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
98 |
val extend = I |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
99 |
val merge = merge_ttab |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
100 |
) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
101 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
102 |
fun add_builtin_typ cs (T, f, g) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
103 |
Builtin_Types.map (insert_ttab cs T (Int (f, g))) |
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_ext (T, f) = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
106 |
Builtin_Types.map (insert_ttab U.basicC T (Ext f)) |
40277 | 107 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
108 |
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
|
109 |
lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt)) |
40277 | 110 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
111 |
fun builtin_typ ctxt T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
112 |
(case lookup_builtin_typ ctxt T of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
113 |
SOME (_, Int (f, _)) => f T |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
114 |
| _ => NONE) |
40277 | 115 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
116 |
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
|
117 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
118 |
fun is_builtin_typ_ext ctxt T = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
119 |
(case lookup_builtin_typ ctxt T of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
120 |
SOME (_, Int (f, _)) => is_some (f T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
121 |
| SOME (_, Ext f) => f T |
40277 | 122 |
| NONE => false) |
123 |
||
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
124 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
125 |
(* built-in numbers *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
126 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
127 |
fun builtin_num ctxt t = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
128 |
(case try HOLogic.dest_number t of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
129 |
NONE => NONE |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
130 |
| SOME (T, i) => |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
131 |
(case lookup_builtin_typ ctxt T of |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
132 |
SOME (_, Int (_, g)) => g T i |> Option.map (rpair T) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
133 |
| _ => NONE)) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
134 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
135 |
val is_builtin_num = is_some oo builtin_num |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
136 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
137 |
fun is_builtin_num_ext ctxt t = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
138 |
(case try HOLogic.dest_number t of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
139 |
NONE => false |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
140 |
| SOME (T, _) => is_builtin_typ_ext ctxt T) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
141 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
142 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
143 |
(* built-in functions *) |
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 |
type 'a bfun = Proof.context -> typ -> term list -> 'a |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
146 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
147 |
structure Builtin_Funcs = Generic_Data |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
148 |
( |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
149 |
type T = |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
150 |
(bool bfun, (((string * int) * typ) * term list * typ) option bfun) btab |
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
151 |
val empty = Symtab.empty |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
152 |
val extend = I |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
153 |
val merge = merge_btab |
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 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
156 |
fun add_builtin_fun cs ((n, T), f) = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
157 |
Builtin_Funcs.map (insert_btab cs n T (Int f)) |
40277 | 158 |
|
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
159 |
fun add_builtin_fun' cs (t, n) = |
41127
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
160 |
let |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
161 |
val T = Term.fastype_of t |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
162 |
fun bfun _ U ts = SOME (((n, length (Term.binder_types T)), U), ts, T) |
2ea84c8535c6
re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset
|
163 |
in add_builtin_fun cs (Term.dest_Const t, bfun) end |
41059
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 |
fun add_builtin_fun_ext ((n, T), f) = |
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41073
diff
changeset
|
166 |
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
|
167 |
|
41126
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
168 |
fun add_builtin_fun_ext' c = |
e0bd443c0fdd
re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset
|
169 |
add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
170 |
|
41072
9f9bc1bdacef
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents:
41059
diff
changeset
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
175 |
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
|
176 |
lookup_btab ctxt (Builtin_Funcs.get (Context.Proof ctxt)) |
41059
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
177 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
178 |
fun builtin_fun ctxt (c as (_, T)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
179 |
(case lookup_builtin_fun ctxt c of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
180 |
SOME (_, Int f) => f ctxt T ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
181 |
| _ => NONE) |
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 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
|
184 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
185 |
fun is_builtin_fun_ext ctxt (c as (_, T)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
186 |
(case lookup_builtin_fun ctxt c of |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
187 |
SOME (_, Int f) => is_some (f ctxt T ts) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
188 |
| SOME (_, Ext f) => f ctxt T ts |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
189 |
| NONE => false) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
190 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
191 |
(* FIXME: move this information to the interfaces *) |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
192 |
val only_partially_supported = [ |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
193 |
@{const_name times}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
194 |
@{const_name div_class.div}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
195 |
@{const_name div_class.mod}, |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
196 |
@{const_name inverse_class.divide} ] |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
197 |
|
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
198 |
fun is_builtin_ext ctxt (c as (n, _)) ts = |
d2b1fc1b8e19
centralized handling of built-in types and constants;
boehmes
parents:
40691
diff
changeset
|
199 |
if member (op =) only_partially_supported n then false |
41073 | 200 |
else |
201 |
is_builtin_num_ext ctxt (Term.list_comb (Const c, ts)) orelse |
|
202 |
is_builtin_fun_ext ctxt c ts |
|
40277 | 203 |
|
204 |
end |