fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 16:29:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Dec 15 16:32:45 2010 +0100
@@ -141,7 +141,7 @@
"must have the same kind: " ^ Syntax.string_of_term ctxt t)
fun check_trigger_conv ctxt ct =
- if proper_quant false proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+ if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
else check_trigger_error ctxt (Thm.term_of ct)
@@ -256,20 +256,20 @@
fun is_weight (@{const SMT.weight} $ w $ t) =
(case try HOLogic.dest_number w of
- SOME (_, i) => i > 0 andalso has_no_weight t
+ SOME (_, i) => i >= 0 andalso has_no_weight t
| _ => false)
| is_weight t = has_no_weight t
fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
- | proper_trigger t = has_no_weight t
+ | proper_trigger t = is_weight t
fun check_weight_error ctxt t =
- error ("SMT weight must be a positive number and must only occur " ^
+ error ("SMT weight must be a non-negative number and must only occur " ^
"under the top-most quantifier and an optional trigger: " ^
Syntax.string_of_term ctxt t)
fun check_weight_conv ctxt ct =
- if U.under_quant proper_trigger (Thm.term_of ct) then Conv.all_conv ct
+ if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
else check_weight_error ctxt (Thm.term_of ct)
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 16:29:56 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Dec 15 16:32:45 2010 +0100
@@ -147,6 +147,8 @@
fun mark t =
(case Term.strip_comb t of
(u as Const (@{const_name If}, _), ts) => marks u ts
+ | (u as @{const SMT.weight}, [t1, t2]) =>
+ mark t2 #>> (fn t2' => u $ t1 $ t2')
| (u as Const c, ts) =>
(case B.builtin_num ctxt t of
SOME (n, T) =>
@@ -494,14 +496,7 @@
| group_quant _ Ts t = (Ts, t)
fun dest_weight (@{const SMT.weight} $ w $ t) =
- ((SOME (snd (HOLogic.dest_number w)), t)
- handle TERM _ =>
- (case w of
- Var ((s, _), _) => (* FIXME: temporary workaround *)
- (case Int.fromString s of
- SOME n => (SOME n, t)
- | NONE => raise TERM ("bad weight", [w]))
- | _ => raise TERM ("bad weight", [w])))
+ (SOME (snd (HOLogic.dest_number w)), t)
| dest_weight t = (NONE, t)
fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)