57 fun word_num (Type (@{type_name word}, [T])) i = |
57 fun word_num (Type (@{type_name word}, [T])) i = |
58 Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T) |
58 Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T) |
59 | word_num _ _ = NONE |
59 | word_num _ _ = NONE |
60 |
60 |
61 fun if_fixed n T ts = |
61 fun if_fixed n T ts = |
62 let val (Ts, T) = Term.strip_type T |
62 let val (Us, U) = Term.strip_type T |
63 in if forall (can dest_wordT) (T :: Ts) then SOME (n, ts) else NONE end |
63 in |
|
64 if forall (can dest_wordT) (U :: Us) then |
|
65 SOME (((n, length Us), T), ts, T) |
|
66 else NONE |
|
67 end |
64 |
68 |
65 fun if_fixed' n T ts = |
69 fun if_fixed' n T ts = |
66 if forall (can dest_wordT) (Term.binder_types T) then SOME (n, ts) |
70 let val Ts = Term.binder_types T |
67 else NONE |
71 in |
|
72 if forall (can dest_wordT) Ts then SOME (((n, length Ts), T), ts, T) |
|
73 else NONE |
|
74 end |
68 |
75 |
69 fun add_word_fun f (t, n) = |
76 fun add_word_fun f (t, n) = |
70 B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n)) |
77 B.add_builtin_fun smtlibC (Term.dest_Const t, K (f n)) |
71 |
78 |
72 fun add_word_fun' f (t, n) = add_word_fun f (t, n) |
79 fun add_word_fun' f (t, n) = add_word_fun f (t, n) |
77 | dest_nat ts = raise TERM ("dest_nat", ts) |
84 | dest_nat ts = raise TERM ("dest_nat", ts) |
78 fun dest_nat_word_funT (T, ts) = |
85 fun dest_nat_word_funT (T, ts) = |
79 (dest_word_funT (Term.range_type T), dest_nat ts) |
86 (dest_word_funT (Term.range_type T), dest_nat ts) |
80 |
87 |
81 fun shift n T ts = |
88 fun shift n T ts = |
82 let val U = Term.domain_type T |
89 let |
|
90 val U = Term.domain_type T |
|
91 val T' = [U, U] ---> U |
83 in |
92 in |
84 (case (can dest_wordT U, ts) of |
93 (case (can dest_wordT T', ts) of |
85 (true, [t, u]) => |
94 (true, [t, u]) => |
86 (case try HOLogic.dest_number u of |
95 (case try HOLogic.dest_number u of |
87 SOME (_,i) => SOME (n, [t, HOLogic.mk_number U i]) |
96 SOME (_, i) => SOME (((n, 2), T'), [t, HOLogic.mk_number T' i], T') |
88 | NONE => NONE) (* FIXME: also support non-numerical shifts *) |
97 | NONE => NONE) (* FIXME: also support non-numerical shifts *) |
89 | _ => NONE) |
98 | _ => NONE) |
90 end |
99 end |
91 |
100 |
92 fun extract n T ts = |
101 fun extract n T ts = |
93 try dest_nat_word_funT (T, ts) |
102 try dest_nat_word_funT (T, ts) |
94 |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts')) |
103 |> Option.map (fn ((_, i), (lb, ts')) => |
|
104 let val T' = Term.range_type T |
|
105 in (((index2 n (i + lb - 1) lb, 1), T'), ts', T') end) |
95 |
106 |
96 fun extend n T ts = |
107 fun extend n T ts = |
97 (case try dest_word_funT T of |
108 (case try dest_word_funT T of |
98 SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE |
109 SOME (i, j) => |
|
110 if j-i >= 0 then SOME (((index1 n (j-i), 1), T), ts, T) |
|
111 else NONE |
99 | _ => NONE) |
112 | _ => NONE) |
100 |
113 |
101 fun rotate n T ts = |
114 fun rotate n T ts = |
102 try dest_nat ts |
115 let val T' = Term.range_type T |
103 |> Option.map (fn (i, ts') => (index1 n i, ts')) |
116 in |
|
117 try dest_nat ts |
|
118 |> Option.map (fn (i, ts') => (((index1 n i, 1), T'), ts', T')) |
|
119 end |
104 in |
120 in |
105 |
121 |
106 val setup_builtins = |
122 val setup_builtins = |
107 B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #> |
123 B.add_builtin_typ smtlibC (wordT, word_typ, word_num) #> |
108 fold (add_word_fun' if_fixed) [ |
124 fold (add_word_fun' if_fixed) [ |