1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 20 00:37:42 2011 +0200
     1.3 @@ -71,7 +71,6 @@
     1.4    val invert_const : string -> string
     1.5    val unproxify_const : string -> string
     1.6    val new_skolem_var_name_from_const : string -> string
     1.7 -  val num_type_args : theory -> string -> int
     1.8    val atp_irrelevant_consts : string list
     1.9    val atp_schematic_consts_of : term -> typ list Symtab.table
    1.10    val is_locality_global : locality -> bool
    1.11 @@ -126,6 +125,9 @@
    1.12  val type_const_prefix = "tc_"
    1.13  val class_prefix = "cl_"
    1.14  
    1.15 +(* TODO: Use a more descriptive prefix in "SMT_Translate.lift_lambdas". *)
    1.16 +val lambda_lifted_prefix = Name.uu
    1.17 +
    1.18  val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
    1.19  val old_skolem_const_prefix = skolem_const_prefix ^ "o"
    1.20  val new_skolem_const_prefix = skolem_const_prefix ^ "n"
    1.21 @@ -301,15 +303,6 @@
    1.22      nth ss (length ss - 2)
    1.23    end
    1.24  
    1.25 -(* The number of type arguments of a constant, zero if it's monomorphic. For
    1.26 -   (instances of) Skolem pseudoconstants, this information is encoded in the
    1.27 -   constant name. *)
    1.28 -fun num_type_args thy s =
    1.29 -  if String.isPrefix skolem_const_prefix s then
    1.30 -    s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the
    1.31 -  else
    1.32 -    (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.33 -
    1.34  (* These are either simplified away by "Meson.presimplify" (most of the time) or
    1.35     handled specially via "fFalse", "fTrue", ..., "fequal". *)
    1.36  val atp_irrelevant_consts =
    1.37 @@ -479,16 +472,16 @@
    1.38        val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
    1.39      in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
    1.40    | iterm_from_term thy _ (Const (c, T)) =
    1.41 -    let
    1.42 -      val tvar_list =
    1.43 -        (if String.isPrefix old_skolem_const_prefix c then
    1.44 -           [] |> Term.add_tvarsT T |> map TVar
    1.45 -         else
    1.46 -           (c, T) |> Sign.const_typargs thy)
    1.47 -      val c' = IConst (`make_fixed_const c, T, tvar_list)
    1.48 -    in (c', atyps_of T) end
    1.49 -  | iterm_from_term _ _ (Free (v, T)) =
    1.50 -    (IConst (`make_fixed_var v, T, []), atyps_of T)
    1.51 +    (IConst (`make_fixed_const c, T,
    1.52 +             if String.isPrefix old_skolem_const_prefix c then
    1.53 +               [] |> Term.add_tvarsT T |> map TVar
    1.54 +             else
    1.55 +               (c, T) |> Sign.const_typargs thy),
    1.56 +     atyps_of T)
    1.57 +  | iterm_from_term _ _ (Free (s, T)) =
    1.58 +    (IConst (`make_fixed_var s, T,
    1.59 +             if String.isPrefix lambda_lifted_prefix s then [T] else []),
    1.60 +     atyps_of T)
    1.61    | iterm_from_term _ _ (Var (v as (s, _), T)) =
    1.62      (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
    1.63         let
    1.64 @@ -1414,7 +1407,8 @@
    1.65      fold (fold_type_constrs f) Ts (f (s, x))
    1.66    | fold_type_constrs _ _ x = x
    1.67  
    1.68 -(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
    1.69 +(* Type constructors used to instantiate overloaded constants are the only ones
    1.70 +   needed. *)
    1.71  fun add_type_constrs_in_term thy =
    1.72    let
    1.73      fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
    1.74 @@ -1422,6 +1416,11 @@
    1.75        | add (Const (x as (s, _))) =
    1.76          if String.isPrefix skolem_const_prefix s then I
    1.77          else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
    1.78 +      | add (Free (s, T)) =
    1.79 +        if String.isPrefix lambda_lifted_prefix s then
    1.80 +          T |> fold_type_constrs set_insert
    1.81 +        else
    1.82 +          I
    1.83        | add (Abs (_, _, u)) = add u
    1.84        | add _ = I
    1.85    in add end
    1.86 @@ -1733,7 +1732,7 @@
    1.87        1 upto num_args |> map (`I o make_bound_var o string_of_int)
    1.88      val bounds =
    1.89        bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
    1.90 -    val sym_needs_arg_types = exists (curry (op =) dummyT) T_args)
    1.91 +    val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
    1.92      fun should_keep_arg_type T =
    1.93        sym_needs_arg_types orelse
    1.94        not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)