src/HOL/Tools/SMT/smt_translate.ML
changeset 43554 9bece8cbb5be
parent 43507 d566714a9ce1
child 43829 fba9754b827e
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Sat Jun 25 20:03:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Sun Jun 26 19:10:02 2011 +0200
     1.3 @@ -333,7 +333,14 @@
     1.4      | (_, ts) => fold min_arities ts)
     1.5  
     1.6    fun minimize types t i =
     1.7 -    if i = 0 orelse Typtab.defined types (Term.type_of t) then 0 else i
     1.8 +    let
     1.9 +      fun find_min j [] _ = j
    1.10 +        | find_min j (U :: Us) T =
    1.11 +            if Typtab.defined types T then j
    1.12 +            else find_min (j + 1) Us (U --> T)
    1.13 +
    1.14 +      val (Ts, T) = Term.strip_type (Term.type_of t)
    1.15 +    in find_min 0 (take i (rev Ts)) T end
    1.16  
    1.17    fun app u (t, T) =
    1.18      (Const (@{const_name SMT.fun_app}, T --> T) $ t $ u, Term.range_type T)
    1.19 @@ -354,11 +361,15 @@
    1.20        if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
    1.21        else apply (the (Termtab.lookup arities' t)) t T ts
    1.22  
    1.23 +    fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
    1.24 +
    1.25      fun traverse Ts t =
    1.26        (case Term.strip_comb t of
    1.27 -        (q as Const (@{const_name All}, _), [u as Abs _]) => q $ traverse Ts u
    1.28 -      | (q as Const (@{const_name Ex}, _), [u as Abs _]) => q $ traverse Ts u
    1.29 -      | (q as Const (@{const_name Ex}, _), [u1 as Abs _, u2]) =>
    1.30 +        (q as Const (@{const_name All}, _), [Abs (x, T, u)]) =>
    1.31 +          q $ Abs (x, T, in_trigger (T :: Ts) u)
    1.32 +      | (q as Const (@{const_name Ex}, _), [Abs (x, T, u)]) =>
    1.33 +          q $ Abs (x, T, in_trigger (T :: Ts) u)
    1.34 +      | (q as Const (@{const_name Let}, _), [u1 as Abs _, u2]) =>
    1.35            q $ traverse Ts u1 $ traverse Ts u2
    1.36        | (u as Const (c as (_, T)), ts) =>
    1.37            (case SMT_Builtin.dest_builtin ctxt c ts of
    1.38 @@ -368,6 +379,20 @@
    1.39        | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
    1.40        | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
    1.41        | (u, ts) => traverses Ts u ts)
    1.42 +    and in_trigger Ts ((c as @{const SMT.trigger}) $ p $ t) =
    1.43 +          c $ in_pats Ts p $ in_weight Ts t
    1.44 +      | in_trigger Ts t = in_weight Ts t
    1.45 +    and in_pats Ts ps =
    1.46 +      in_list @{typ "SMT.pattern list"}
    1.47 +        (in_list @{typ SMT.pattern} (in_pat Ts)) ps
    1.48 +    and in_pat Ts ((p as Const (@{const_name SMT.pat}, _)) $ t) =
    1.49 +          p $ traverse Ts t
    1.50 +      | in_pat Ts ((p as Const (@{const_name SMT.nopat}, _)) $ t) =
    1.51 +          p $ traverse Ts t
    1.52 +      | in_pat _ t = raise TERM ("bad pattern", [t])
    1.53 +    and in_weight Ts ((c as @{const SMT.weight}) $ w $ t) =
    1.54 +          c $ w $ traverse Ts t
    1.55 +      | in_weight Ts t = traverse Ts t 
    1.56      and traverses Ts t ts = Term.list_comb (t, map (traverse Ts) ts)
    1.57    in map (traverse []) ts end
    1.58