add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)

--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 09:54:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
@@ -7,7 +7,9 @@
 
 signature ATP_PROBLEM =
 sig
-  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+  datatype ('a, 'b) ho_term =
+    ATerm of 'a * ('a, 'b) ho_term list |
+    AAbs of ('a * 'b) * ('a, 'b) ho_term
   datatype quantifier = AForall | AExists
   datatype connective = ANot | AAnd | AOr | AImplies | AIff
   datatype ('a, 'b, 'c) formula =
@@ -21,8 +23,8 @@
   datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
   datatype 'a problem_line =
     Decl of string * 'a * 'a ho_type |
-    Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
-               * string fo_term option * string fo_term option
+    Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+               * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
   type 'a problem = (string * 'a problem_line list) list
 
   val tptp_cnf : string
@@ -91,7 +93,9 @@
 
 (** ATP problem **)
 
-datatype 'a fo_term = ATerm of 'a * 'a fo_term list
+datatype ('a, 'b) ho_term =
+  ATerm of 'a * ('a, 'b) ho_term list |
+  AAbs of ('a * 'b) * ('a, 'b) ho_term
 datatype quantifier = AForall | AExists
 datatype connective = ANot | AAnd | AOr | AImplies | AIff
 datatype ('a, 'b, 'c) formula =
@@ -105,8 +109,8 @@
 datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
 datatype 'a problem_line =
   Decl of string * 'a * 'a ho_type |
-  Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
-             * string fo_term option * string fo_term option
+  Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
+             * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
 type 'a problem = (string * 'a problem_line list) list
 
 (* official TPTP syntax *)
@@ -225,6 +229,9 @@
         else
           s ^ "(" ^ commas ss ^ ")"
       end
+  | string_for_term THF (AAbs ((s, ty), tm)) =
+    "^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm
+  | string_for_term _ _ = raise Fail "unexpected term in first-order format"
 
 fun string_for_quantifier AForall = tptp_forall
   | string_for_quantifier AExists = tptp_exists
@@ -303,8 +310,9 @@
   | is_problem_line_cnf_ueq _ = false
 
 fun open_conjecture_term (ATerm ((s, s'), tms)) =
-  ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
-         else (s, s'), tms |> map open_conjecture_term)
+    ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
+           else (s, s'), tms |> map open_conjecture_term)
+  | open_conjecture_term _ = raise Fail "unexpected higher-order term"
 fun open_formula conj =
   let
     (* We are conveniently assuming that all bound variable names are
@@ -403,9 +411,10 @@
     fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
       | do_type (AType name) = do_sym name (K atype_of_types)
     fun do_term pred_sym (ATerm (name as (s, _), tms)) =
-      is_tptp_user_symbol s
-      ? do_sym name (fn _ => default_type pred_sym (length tms))
-      #> fold (do_term false) tms
+        is_tptp_user_symbol s
+        ? do_sym name (fn _ => default_type pred_sym (length tms))
+        #> fold (do_term false) tms
+      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
     fun do_formula (AQuant (_, xs, phi)) =
         fold do_type (map_filter snd xs) #> do_formula phi
       | do_formula (AConn (_, phis)) = fold do_formula phis
@@ -496,10 +505,12 @@
           end
       in add 0 |> apsnd SOME end
 
-fun nice_term (ATerm (name, ts)) =
-  nice_name name ##>> pool_map nice_term ts #>> ATerm
 fun nice_type (AType name) = nice_name name #>> AType
   | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
+fun nice_term (ATerm (name, ts)) =
+    nice_name name ##>> pool_map nice_term ts #>> ATerm
+  | nice_term (AAbs ((name, ty), tm)) =
+    nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
 fun nice_formula (AQuant (q, xs, phi)) =
     pool_map nice_name (map fst xs)
     ##>> pool_map (fn NONE => pair NONE

--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 09:54:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
@@ -8,7 +8,7 @@
 
 signature ATP_TRANSLATE =
 sig
-  type 'a fo_term = 'a ATP_Problem.fo_term
+  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
   type connective = ATP_Problem.connective
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type format = ATP_Problem.format
@@ -83,7 +83,7 @@
   val choose_format : format list -> type_enc -> format * type_enc
   val mk_aconns :
     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
-  val unmangled_const : string -> string * string fo_term list
+  val unmangled_const : string -> string * (string, 'b) ho_term list
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
@@ -545,7 +545,8 @@
            ("simple", (NONE, _, Lightweight)) =>
            Simple_Types (First_Order, level)
          | ("simple_higher", (NONE, _, Lightweight)) =>
-           Simple_Types (Higher_Order, level)
+           if level = Noninf_Nonmono_Types then raise Same.SAME
+           else Simple_Types (Higher_Order, level)
          | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
          | ("tags", (SOME Polymorphic, _, _)) =>
            Tags (Polymorphic, level, heaviness)
@@ -698,14 +699,16 @@
   | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
 fun close_combformula_universally phi = close_universally combterm_vars phi
 
-fun term_vars (ATerm (name as (s, _), tms)) =
-  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
-fun close_formula_universally phi = close_universally term_vars phi
+fun term_vars bounds (ATerm (name as (s, _), tms)) =
+    (is_tptp_variable s andalso not (member (op =) bounds name))
+    ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
+  | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
+fun close_formula_universally phi = close_universally (term_vars []) phi
 
 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
 val homo_infinite_type = Type (homo_infinite_type_name, [])
 
-fun fo_term_from_typ format type_enc =
+fun ho_term_from_typ format type_enc =
   let
     fun term (Type (s, Ts)) =
       ATerm (case (is_type_enc_higher_order type_enc, s) of
@@ -722,8 +725,8 @@
       ATerm ((make_schematic_type_var x, s), [])
   in term end
 
-fun fo_term_for_type_arg format type_enc T =
-  if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
+fun ho_term_for_type_arg format type_enc T =
+  if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
 
 (* This shouldn't clash with anything else. *)
 val mangled_type_sep = "\000"
@@ -732,6 +735,7 @@
   | generic_mangled_type_name f (ATerm (name, tys)) =
     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
     ^ ")"
+  | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"
 
 val bool_atype = AType (`I tptp_bool_type)
 
@@ -742,7 +746,7 @@
   else
     simple_type_prefix ^ ascii_of s
 
-fun ho_type_from_fo_term type_enc pred_sym ary =
+fun ho_type_from_ho_term type_enc pred_sym ary =
   let
     fun to_atype ty =
       AType ((make_simple_type (generic_mangled_type_name fst ty),
@@ -750,17 +754,19 @@
     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
+      | to_fo ary _ = raise Fail "unexpected type abstraction"
     fun to_ho (ty as ATerm ((s, _), tys)) =
-      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
+      | to_ho _ = raise Fail "unexpected type abstraction"
   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
 
 fun mangled_type format type_enc pred_sym ary =
-  ho_type_from_fo_term type_enc pred_sym ary
-  o fo_term_from_typ format type_enc
+  ho_type_from_ho_term type_enc pred_sym ary
+  o ho_term_from_typ format type_enc
 
 fun mangled_const_name format type_enc T_args (s, s') =
   let
-    val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
+    val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
     fun type_suffix f g =
       fold_rev (curry (op ^) o g o prefix mangled_type_sep
                 o generic_mangled_type_name f) ty_args ""
@@ -1444,12 +1450,13 @@
 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
+  | is_var_positively_naked_in_term name _ _ _ = true
 fun should_predicate_on_var_in_formula pos phi (SOME true) name =
     formula_fold pos (is_var_positively_naked_in_term name) phi false
   | should_predicate_on_var_in_formula _ _ _ _ = true
 
 fun mk_const_aterm format type_enc x T_args args =
-  ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
+  ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
 
 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   CombConst (type_tag, T --> T, [T])
@@ -1924,8 +1931,9 @@
 val type_info_default_weight = 0.8
 
 fun add_term_weights weight (ATerm (s, tms)) =
-  is_tptp_user_symbol s ? Symtab.default (s, weight)
-  #> fold (add_term_weights weight) tms
+    is_tptp_user_symbol s ? Symtab.default (s, weight)
+    #> fold (add_term_weights weight) tms
+  | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
     formula_fold NONE (K (add_term_weights weight)) phi
   | add_problem_line_weights _ _ = I