boehmes@32618
|
1 |
(* Title: HOL/SMT/Tools/smt_builtin.ML
|
boehmes@32618
|
2 |
Author: Sascha Boehme, TU Muenchen
|
boehmes@32618
|
3 |
|
boehmes@32618
|
4 |
Tables for built-in symbols.
|
boehmes@32618
|
5 |
*)
|
boehmes@32618
|
6 |
|
boehmes@32618
|
7 |
signature SMT_BUILTIN =
|
boehmes@32618
|
8 |
sig
|
boehmes@32618
|
9 |
type sterm = (SMT_Translate.sym, typ) sterm
|
boehmes@32618
|
10 |
type builtin_fun = typ -> sterm list -> (string * sterm list) option
|
boehmes@32618
|
11 |
type table = (typ * builtin_fun) list Symtab.table
|
boehmes@32618
|
12 |
|
boehmes@32618
|
13 |
val make: (term * string) list -> table
|
boehmes@32618
|
14 |
val add: term * builtin_fun -> table -> table
|
boehmes@32618
|
15 |
val lookup: table -> theory -> string * typ -> sterm list ->
|
boehmes@32618
|
16 |
(string * sterm list) option
|
boehmes@32618
|
17 |
|
boehmes@32618
|
18 |
val bv_rotate: (int -> string) -> builtin_fun
|
boehmes@32618
|
19 |
val bv_extend: (int -> string) -> builtin_fun
|
boehmes@32618
|
20 |
val bv_extract: (int -> int -> string) -> builtin_fun
|
boehmes@32618
|
21 |
end
|
boehmes@32618
|
22 |
|
boehmes@32618
|
23 |
structure SMT_Builtin: SMT_BUILTIN =
|
boehmes@32618
|
24 |
struct
|
boehmes@32618
|
25 |
|
boehmes@32618
|
26 |
structure T = SMT_Translate
|
boehmes@32618
|
27 |
|
boehmes@32618
|
28 |
type sterm = (SMT_Translate.sym, typ) sterm
|
boehmes@32618
|
29 |
type builtin_fun = typ -> sterm list -> (string * sterm list) option
|
boehmes@32618
|
30 |
type table = (typ * builtin_fun) list Symtab.table
|
boehmes@32618
|
31 |
|
boehmes@32618
|
32 |
fun make entries =
|
boehmes@32618
|
33 |
let
|
boehmes@32618
|
34 |
fun dest (t, bn) =
|
boehmes@32618
|
35 |
let val (n, T) = Term.dest_Const t
|
boehmes@32618
|
36 |
in (n, (Logic.varifyT T, K (pair bn))) end
|
boehmes@32618
|
37 |
in Symtab.make (AList.group (op =) (map dest entries)) end
|
boehmes@32618
|
38 |
|
boehmes@32618
|
39 |
fun add (t, f) tab =
|
boehmes@32618
|
40 |
let val (n, T) = apsnd Logic.varifyT (Term.dest_Const t)
|
boehmes@32618
|
41 |
in Symtab.map_default (n, []) (AList.update (op =) (T, f)) tab end
|
boehmes@32618
|
42 |
|
boehmes@32618
|
43 |
fun lookup tab thy (n, T) =
|
boehmes@32618
|
44 |
AList.lookup (Sign.typ_instance thy) (Symtab.lookup_list tab n) T T
|
boehmes@32618
|
45 |
|
boehmes@32618
|
46 |
|
boehmes@32618
|
47 |
fun dest_binT T =
|
boehmes@32618
|
48 |
(case T of
|
boehmes@32618
|
49 |
Type (@{type_name "Numeral_Type.num0"}, _) => 0
|
boehmes@32618
|
50 |
| Type (@{type_name "Numeral_Type.num1"}, _) => 1
|
boehmes@32618
|
51 |
| Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
|
boehmes@32618
|
52 |
| Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
|
boehmes@32618
|
53 |
| _ => raise TYPE ("dest_binT", [T], []))
|
boehmes@32618
|
54 |
|
boehmes@32618
|
55 |
fun dest_wordT T =
|
boehmes@32618
|
56 |
(case T of
|
boehmes@32618
|
57 |
Type (@{type_name "word"}, [T]) => dest_binT T
|
boehmes@32618
|
58 |
| _ => raise TYPE ("dest_wordT", [T], []))
|
boehmes@32618
|
59 |
|
boehmes@32618
|
60 |
|
boehmes@32618
|
61 |
val dest_nat = (fn
|
boehmes@32618
|
62 |
SApp (SConst (@{const_name nat}, _), [SApp (SNum (i, _), _)]) => SOME i
|
boehmes@32618
|
63 |
| _ => NONE)
|
boehmes@32618
|
64 |
|
boehmes@32618
|
65 |
fun bv_rotate mk_name T ts =
|
boehmes@32618
|
66 |
dest_nat (hd ts) |> Option.map (fn i => (mk_name i, tl ts))
|
boehmes@32618
|
67 |
|
boehmes@32618
|
68 |
fun bv_extend mk_name T ts =
|
boehmes@32618
|
69 |
(case (try dest_wordT (domain_type T), try dest_wordT (range_type T)) of
|
boehmes@32618
|
70 |
(SOME i, SOME j) => if j - i >= 0 then SOME (mk_name (j - i), ts) else NONE
|
boehmes@32618
|
71 |
| _ => NONE)
|
boehmes@32618
|
72 |
|
boehmes@32618
|
73 |
fun bv_extract mk_name T ts =
|
boehmes@32618
|
74 |
(case (try dest_wordT (body_type T), dest_nat (hd ts)) of
|
boehmes@32618
|
75 |
(SOME i, SOME lb) => SOME (mk_name (i + lb - 1) lb, tl ts)
|
boehmes@32618
|
76 |
| _ => NONE)
|
boehmes@32618
|
77 |
|
boehmes@32618
|
78 |
end
|