src/HOL/Tools/SMT/smt_translate.ML
changeset 40664 e023788a91a1
parent 40663 e080c9e68752
child 40681 872b08416fb4
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 15:45:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Mon Nov 22 23:37:00 2010 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4      SVar of int |
     1.5      SApp of string * sterm list |
     1.6      SLet of string * sterm * sterm |
     1.7 -    SQua of squant * string list * sterm spattern list * sterm
     1.8 +    SQua of squant * string list * sterm spattern list * int option * sterm
     1.9  
    1.10    (* configuration options *)
    1.11    type prefixes = {sort_prefix: string, func_prefix: string}
    1.12 @@ -65,7 +65,7 @@
    1.13    SVar of int |
    1.14    SApp of string * sterm list |
    1.15    SLet of string * sterm * sterm |
    1.16 -  SQua of squant * string list * sterm spattern list * sterm
    1.17 +  SQua of squant * string list * sterm spattern list * int option * sterm
    1.18  
    1.19  
    1.20  
    1.21 @@ -119,6 +119,10 @@
    1.22        if q = qname then group_quant qname (T :: Ts) u else (Ts, t)
    1.23    | group_quant _ Ts t = (Ts, t)
    1.24  
    1.25 +fun dest_weight (@{const SMT.weight} $ w $ t) =
    1.26 +      (SOME (snd (HOLogic.dest_number w)), t)
    1.27 +  | dest_weight t = (NONE, t)
    1.28 +
    1.29  fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)
    1.30    | dest_pat (Const (@{const_name nopat}, _) $ t) = (t, false)
    1.31    | dest_pat t = raise TERM ("dest_pat", [t])
    1.32 @@ -137,8 +141,9 @@
    1.33  fun dest_quant qn T t = quantifier qn |> Option.map (fn q =>
    1.34    let
    1.35      val (Ts, u) = group_quant qn [T] t
    1.36 -    val (ps, b) = dest_trigger u
    1.37 -  in (q, rev Ts, ps, b) end)
    1.38 +    val (ps, p) = dest_trigger u
    1.39 +    val (w, b) = dest_weight p
    1.40 +  in (q, rev Ts, ps, w, b) end)
    1.41  
    1.42  fun fold_map_pat f (SPat ts) = fold_map f ts #>> SPat
    1.43    | fold_map_pat f (SNoPat ts) = fold_map f ts #>> SNoPat
    1.44 @@ -214,6 +219,9 @@
    1.45        | (h as Free _, ts) => Term.list_comb (h, map in_term ts)
    1.46        | _ => t)
    1.47  
    1.48 +    and in_weight ((c as @{const SMT.weight}) $ w $ t) = c $ w $ in_form t
    1.49 +      | in_weight t = in_form t 
    1.50 +
    1.51      and in_pat ((c as Const (@{const_name pat}, _)) $ t) = c $ in_term t
    1.52        | in_pat ((c as Const (@{const_name nopat}, _)) $ t) = c $ in_term t
    1.53        | in_pat t = raise TERM ("in_pat", [t])
    1.54 @@ -221,8 +229,8 @@
    1.55      and in_pats ps =
    1.56        in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
    1.57  
    1.58 -    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
    1.59 -      | in_trig t = in_form t
    1.60 +    and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_weight t
    1.61 +      | in_trig t = in_weight t
    1.62  
    1.63      and in_form t =
    1.64        (case Term.strip_comb t of
    1.65 @@ -366,9 +374,9 @@
    1.66        (case Term.strip_comb t of
    1.67          (Const (qn, _), [Abs (_, T, t1)]) =>
    1.68            (case dest_quant qn T t1 of
    1.69 -            SOME (q, Ts, ps, b) =>
    1.70 +            SOME (q, Ts, ps, w, b) =>
    1.71                fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
    1.72 -              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
    1.73 +              trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', w, b'))
    1.74            | NONE => raise TERM ("intermediate", [t]))
    1.75        | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    1.76            transT T ##>> trans t1 ##>> trans t2 #>>