fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
authorboehmes
Wed, 15 Dec 2010 16:32:45 +0100
changeset 41173 7c6178d45cc8
parent 41172 a17c2d669c40
child 41174 10eb369f8c01
fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_translate.ML
--- 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)