src/HOL/Tools/SMT/smt_translate.ML
changeset 66134 a1fb6beb2731
parent 61782 7d754aca6a75
child 66136 dd006934a719
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Tue Jun 20 14:33:45 2017 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    datatype sterm =
     1.5      SVar of int |
     1.6      SApp of string * sterm list |
     1.7 -    SLet of string * sterm * sterm |
     1.8      SQua of squant * string list * sterm spattern list * sterm
     1.9  
    1.10    (*translation configuration*)
    1.11 @@ -47,12 +46,12 @@
    1.12  
    1.13  datatype squant = SForall | SExists
    1.14  
    1.15 -datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
    1.16 +datatype 'a spattern =
    1.17 +  SPat of 'a list | SNoPat of 'a list
    1.18  
    1.19  datatype sterm =
    1.20    SVar of int |
    1.21    SApp of string * sterm list |
    1.22 -  SLet of string * sterm * sterm |
    1.23    SQua of squant * string list * sterm spattern list * sterm
    1.24  
    1.25  
    1.26 @@ -204,7 +203,6 @@
    1.27        | expand ((q as Const (@{const_name Ex}, _)) $ Abs a) = q $ abs_expand a
    1.28        | expand ((q as Const (@{const_name Ex}, T)) $ t) = q $ exp expand T t
    1.29        | expand (q as Const (@{const_name Ex}, T)) = exp2 T q
    1.30 -      | expand (Const (@{const_name Let}, _) $ t $ u) = expand (Term.betapply (u, t))
    1.31        | expand (Const (@{const_name Let}, T) $ t) =
    1.32            let val U = Term.domain_type (Term.range_type T)
    1.33            in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
    1.34 @@ -213,7 +211,9 @@
    1.35            in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end
    1.36        | expand t =
    1.37            (case Term.strip_comb t of
    1.38 -            (u as Const (c as (_, T)), ts) =>
    1.39 +            (Const (@{const_name Let}, _), t1 :: t2 :: ts) =>
    1.40 +            betapplys (Term.betapply (expand t2, expand t1), map expand ts)
    1.41 +          | (u as Const (c as (_, T)), ts) =>
    1.42                (case SMT_Builtin.dest_builtin ctxt c ts of
    1.43                  SOME (_, k, us, mk) =>
    1.44                    if k = length us then mk (map expand us)
    1.45 @@ -438,8 +438,6 @@
    1.46                fold_map transT Ts ##>> fold_map (fold_map_pat trans) ps ##>>
    1.47                trans b #>> (fn ((Ts', ps'), b') => SQua (q, Ts', ps', b'))
    1.48            | NONE => raise TERM ("unsupported quantifier", [t]))
    1.49 -      | (Const (@{const_name Let}, _), [t1, Abs (_, T, t2)]) =>
    1.50 -          transT T ##>> trans t1 ##>> trans t2 #>> (fn ((U, u1), u2) => SLet (U, u1, u2))
    1.51        | (u as Const (c as (_, T)), ts) =>
    1.52            (case builtin ctxt c ts of
    1.53              SOME (n, _, us, _) => fold_map trans us #>> app n
    1.54 @@ -516,7 +514,6 @@
    1.55  
    1.56      val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
    1.57        |>> apfst (cons fun_app_eq)
    1.58 -val _ = dtyps : (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list (*###*)
    1.59    in
    1.60      (ts4, tr_context)
    1.61      |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2