1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4            s ^ "(" ^ commas ss ^ ")"
     1.5        end
     1.6    | string_for_term THF (AAbs ((s, ty), tm)) =
     1.7 -    "^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm
     1.8 +    "(^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm ^ ")"
     1.9    | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.10  
    1.11  fun string_for_quantifier AForall = tptp_forall

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     2.3 @@ -442,11 +442,13 @@
     2.4  datatype combterm =
     2.5    CombConst of name * typ * typ list |
     2.6    CombVar of name * typ |
     2.7 -  CombApp of combterm * combterm
     2.8 +  CombApp of combterm * combterm |
     2.9 +  CombAbs of (name * typ) * combterm
    2.10  
    2.11  fun combtyp_of (CombConst (_, T, _)) = T
    2.12    | combtyp_of (CombVar (_, T)) = T
    2.13    | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
    2.14 +  | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
    2.15  
    2.16  (*gets the head of a combinator application, along with the list of arguments*)
    2.17  fun strip_combterm_comb u =
    2.18 @@ -490,7 +492,11 @@
    2.19    | combterm_from_term _ bs (Bound j) =
    2.20      nth bs j
    2.21      |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
    2.22 -  | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
    2.23 +  | combterm_from_term thy bs (Abs (s, T, t)) =
    2.24 +    let val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t in
    2.25 +      (CombAbs ((`make_bound_var s, T), tm),
    2.26 +       union (op =) atomic_Ts (atyps_of T))
    2.27 +    end
    2.28  
    2.29  datatype locality =
    2.30    General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    2.31 @@ -697,6 +703,7 @@
    2.32  fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
    2.33    | combterm_vars (CombConst _) = I
    2.34    | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
    2.35 +  | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
    2.36  fun close_combformula_universally phi = close_universally combterm_vars phi
    2.37  
    2.38  fun term_vars bounds (ATerm (name as (s, _), tms)) =
    2.39 @@ -760,7 +767,7 @@
    2.40        | to_ho _ = raise Fail "unexpected type abstraction"
    2.41    in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
    2.42  
    2.43 -fun mangled_type format type_enc pred_sym ary =
    2.44 +fun ho_type_from_typ format type_enc pred_sym ary =
    2.45    ho_type_from_ho_term type_enc pred_sym ary
    2.46    o ho_term_from_typ format type_enc
    2.47  
    2.48 @@ -818,6 +825,7 @@
    2.49               (proxy_base |>> prefix const_prefix, T_args)
    2.50            | NONE => (name, T_args))
    2.51          |> (fn (name, T_args) => CombConst (name, T, T_args))
    2.52 +      | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
    2.53        | intro _ tm = tm
    2.54    in intro true end
    2.55  
    2.56 @@ -929,7 +937,7 @@
    2.57        | aux t = t
    2.58    in t |> exists_subterm is_Var t ? aux end
    2.59  
    2.60 -fun preprocess_prop ctxt presimp_consts kind t =
    2.61 +fun preprocess_prop ctxt type_enc presimp_consts kind t =
    2.62    let
    2.63      val thy = Proof_Context.theory_of ctxt
    2.64      val t = t |> Envir.beta_eta_contract
    2.65 @@ -942,7 +950,8 @@
    2.66        |> extensionalize_term ctxt
    2.67        |> presimplify_term ctxt presimp_consts
    2.68        |> perhaps (try (HOLogic.dest_Trueprop))
    2.69 -      |> introduce_combinators_in_term ctxt kind
    2.70 +      |> not (is_type_enc_higher_order type_enc)
    2.71 +         ? introduce_combinators_in_term ctxt kind
    2.72    end
    2.73  
    2.74  (* making fact and conjecture formulas *)
    2.75 @@ -958,7 +967,7 @@
    2.76  fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
    2.77                ((name, loc), t) =
    2.78    let val thy = Proof_Context.theory_of ctxt in
    2.79 -    case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
    2.80 +    case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
    2.81             |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
    2.82                             loc Axiom of
    2.83        formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
    2.84 @@ -982,7 +991,7 @@
    2.85                      else I)
    2.86                in
    2.87                  t |> preproc ?
    2.88 -                     (preprocess_prop ctxt presimp_consts kind #> freeze_term)
    2.89 +                     (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
    2.90                    |> make_formula thy type_enc (format <> CNF) (string_of_int j)
    2.91                                    Local kind
    2.92                    |> maybe_negate
    2.93 @@ -1260,6 +1269,7 @@
    2.94               | No_Type_Args => (name, [])
    2.95             end)
    2.96          |> (fn (name, T_args) => CombConst (name, T, T_args))
    2.97 +      | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
    2.98        | aux _ tm = tm
    2.99    in aux 0 end
   2.100  
   2.101 @@ -1455,32 +1465,36 @@
   2.102      formula_fold pos (is_var_positively_naked_in_term name) phi false
   2.103    | should_predicate_on_var_in_formula _ _ _ _ = true
   2.104  
   2.105 -fun mk_const_aterm format type_enc x T_args args =
   2.106 -  ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   2.107 +fun mk_aterm format type_enc name T_args args =
   2.108 +  ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   2.109  
   2.110  fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   2.111    CombConst (type_tag, T --> T, [T])
   2.112    |> enforce_type_arg_policy_in_combterm ctxt format type_enc
   2.113 -  |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   2.114 +  |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   2.115    |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
   2.116 -and term_from_combterm ctxt format nonmono_Ts type_enc =
   2.117 +and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
   2.118    let
   2.119      fun aux site u =
   2.120        let
   2.121          val (head, args) = strip_combterm_comb u
   2.122 -        val (x as (s, _), T_args) =
   2.123 +        val pos =
   2.124 +          case site of
   2.125 +            Top_Level pos => pos
   2.126 +          | Eq_Arg pos => pos
   2.127 +          | Elsewhere => NONE
   2.128 +        val t =
   2.129            case head of
   2.130 -            CombConst (name, _, T_args) => (name, T_args)
   2.131 -          | CombVar (name, _) => (name, [])
   2.132 +            CombConst (name as (s, _), _, T_args) =>
   2.133 +            let
   2.134 +              val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
   2.135 +            in
   2.136 +              mk_aterm format type_enc name T_args (map (aux arg_site) args)
   2.137 +            end
   2.138 +          | CombVar (name, _) => mk_aterm format type_enc name [] []
   2.139 +          | CombAbs ((name, T), tm) =>
   2.140 +            AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
   2.141            | CombApp _ => raise Fail "impossible \"CombApp\""
   2.142 -        val (pos, arg_site) =
   2.143 -          case site of
   2.144 -            Top_Level pos =>
   2.145 -            (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
   2.146 -          | Eq_Arg pos => (pos, Elsewhere)
   2.147 -          | Elsewhere => (NONE, Elsewhere)
   2.148 -        val t = mk_const_aterm format type_enc x T_args
   2.149 -                    (map (aux arg_site) args)
   2.150          val T = combtyp_of u
   2.151        in
   2.152          t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
   2.153 @@ -1493,12 +1507,12 @@
   2.154                               should_predicate_on_var =
   2.155    let
   2.156      fun do_term pos =
   2.157 -      term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   2.158 +      ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   2.159      val do_bound_type =
   2.160        case type_enc of
   2.161          Simple_Types (_, level) =>
   2.162          homogenized_type ctxt nonmono_Ts level 0
   2.163 -        #> mangled_type format type_enc false 0 #> SOME
   2.164 +        #> ho_type_from_typ format type_enc false 0 #> SOME
   2.165        | _ => K NONE
   2.166      fun do_out_of_bound_type pos phi universal (name, T) =
   2.167        if should_predicate_on_type ctxt nonmono_Ts type_enc
   2.168 @@ -1673,7 +1687,7 @@
   2.169    in
   2.170      Decl (sym_decl_prefix ^ s, (s, s'),
   2.171            (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
   2.172 -          |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
   2.173 +          |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
   2.174    end
   2.175  
   2.176  fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
   2.177 @@ -1723,7 +1737,7 @@
   2.178      val bound_names =
   2.179        1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
   2.180      val bounds = bound_names |> map (fn name => ATerm (name, []))
   2.181 -    val cst = mk_const_aterm format type_enc (s, s') T_args
   2.182 +    val cst = mk_aterm format type_enc (s, s') T_args
   2.183      val atomic_Ts = atyps_of T
   2.184      fun eq tms =
   2.185        (if pred_sym then AConn (AIff, map AAtom tms)