1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 09:54:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jul 05 17:09:59 2011 +0100
     1.3 @@ -7,7 +7,9 @@
     1.4  
     1.5  signature ATP_PROBLEM =
     1.6  sig
     1.7 -  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
     1.8 +  datatype ('a, 'b) ho_term =
     1.9 +    ATerm of 'a * ('a, 'b) ho_term list |
    1.10 +    AAbs of ('a * 'b) * ('a, 'b) ho_term
    1.11    datatype quantifier = AForall | AExists
    1.12    datatype connective = ANot | AAnd | AOr | AImplies | AIff
    1.13    datatype ('a, 'b, 'c) formula =
    1.14 @@ -21,8 +23,8 @@
    1.15    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.16    datatype 'a problem_line =
    1.17      Decl of string * 'a * 'a ho_type |
    1.18 -    Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
    1.19 -               * string fo_term option * string fo_term option
    1.20 +    Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    1.21 +               * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
    1.22    type 'a problem = (string * 'a problem_line list) list
    1.23  
    1.24    val tptp_cnf : string
    1.25 @@ -91,7 +93,9 @@
    1.26  
    1.27  (** ATP problem **)
    1.28  
    1.29 -datatype 'a fo_term = ATerm of 'a * 'a fo_term list
    1.30 +datatype ('a, 'b) ho_term =
    1.31 +  ATerm of 'a * ('a, 'b) ho_term list |
    1.32 +  AAbs of ('a * 'b) * ('a, 'b) ho_term
    1.33  datatype quantifier = AForall | AExists
    1.34  datatype connective = ANot | AAnd | AOr | AImplies | AIff
    1.35  datatype ('a, 'b, 'c) formula =
    1.36 @@ -105,8 +109,8 @@
    1.37  datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
    1.38  datatype 'a problem_line =
    1.39    Decl of string * 'a * 'a ho_type |
    1.40 -  Formula of string * formula_kind * ('a, 'a ho_type, 'a fo_term) formula
    1.41 -             * string fo_term option * string fo_term option
    1.42 +  Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    1.43 +             * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
    1.44  type 'a problem = (string * 'a problem_line list) list
    1.45  
    1.46  (* official TPTP syntax *)
    1.47 @@ -225,6 +229,9 @@
    1.48          else
    1.49            s ^ "(" ^ commas ss ^ ")"
    1.50        end
    1.51 +  | string_for_term THF (AAbs ((s, ty), tm)) =
    1.52 +    "^[" ^ s ^ ":" ^ string_for_type THF ty ^ "] : " ^ string_for_term THF tm
    1.53 +  | string_for_term _ _ = raise Fail "unexpected term in first-order format"
    1.54  
    1.55  fun string_for_quantifier AForall = tptp_forall
    1.56    | string_for_quantifier AExists = tptp_exists
    1.57 @@ -303,8 +310,9 @@
    1.58    | is_problem_line_cnf_ueq _ = false
    1.59  
    1.60  fun open_conjecture_term (ATerm ((s, s'), tms)) =
    1.61 -  ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
    1.62 -         else (s, s'), tms |> map open_conjecture_term)
    1.63 +    ATerm (if is_tptp_variable s then (s |> Name.desymbolize false, s')
    1.64 +           else (s, s'), tms |> map open_conjecture_term)
    1.65 +  | open_conjecture_term _ = raise Fail "unexpected higher-order term"
    1.66  fun open_formula conj =
    1.67    let
    1.68      (* We are conveniently assuming that all bound variable names are
    1.69 @@ -403,9 +411,10 @@
    1.70      fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2]
    1.71        | do_type (AType name) = do_sym name (K atype_of_types)
    1.72      fun do_term pred_sym (ATerm (name as (s, _), tms)) =
    1.73 -      is_tptp_user_symbol s
    1.74 -      ? do_sym name (fn _ => default_type pred_sym (length tms))
    1.75 -      #> fold (do_term false) tms
    1.76 +        is_tptp_user_symbol s
    1.77 +        ? do_sym name (fn _ => default_type pred_sym (length tms))
    1.78 +        #> fold (do_term false) tms
    1.79 +      | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
    1.80      fun do_formula (AQuant (_, xs, phi)) =
    1.81          fold do_type (map_filter snd xs) #> do_formula phi
    1.82        | do_formula (AConn (_, phis)) = fold do_formula phis
    1.83 @@ -496,10 +505,12 @@
    1.84            end
    1.85        in add 0 |> apsnd SOME end
    1.86  
    1.87 -fun nice_term (ATerm (name, ts)) =
    1.88 -  nice_name name ##>> pool_map nice_term ts #>> ATerm
    1.89  fun nice_type (AType name) = nice_name name #>> AType
    1.90    | nice_type (AFun (ty1, ty2)) = nice_type ty1 ##>> nice_type ty2 #>> AFun
    1.91 +fun nice_term (ATerm (name, ts)) =
    1.92 +    nice_name name ##>> pool_map nice_term ts #>> ATerm
    1.93 +  | nice_term (AAbs ((name, ty), tm)) =
    1.94 +    nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs
    1.95  fun nice_formula (AQuant (q, xs, phi)) =
    1.96      pool_map nice_name (map fst xs)
    1.97      ##>> pool_map (fn NONE => pair NONE

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 09:54:39 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 05 17:09:59 2011 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  
     2.5  signature ATP_TRANSLATE =
     2.6  sig
     2.7 -  type 'a fo_term = 'a ATP_Problem.fo_term
     2.8 +  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
     2.9    type connective = ATP_Problem.connective
    2.10    type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    2.11    type format = ATP_Problem.format
    2.12 @@ -83,7 +83,7 @@
    2.13    val choose_format : format list -> type_enc -> format * type_enc
    2.14    val mk_aconns :
    2.15      connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    2.16 -  val unmangled_const : string -> string * string fo_term list
    2.17 +  val unmangled_const : string -> string * (string, 'b) ho_term list
    2.18    val unmangled_const_name : string -> string
    2.19    val helper_table : ((string * bool) * thm list) list
    2.20    val factsN : string
    2.21 @@ -545,7 +545,8 @@
    2.22             ("simple", (NONE, _, Lightweight)) =>
    2.23             Simple_Types (First_Order, level)
    2.24           | ("simple_higher", (NONE, _, Lightweight)) =>
    2.25 -           Simple_Types (Higher_Order, level)
    2.26 +           if level = Noninf_Nonmono_Types then raise Same.SAME
    2.27 +           else Simple_Types (Higher_Order, level)
    2.28           | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
    2.29           | ("tags", (SOME Polymorphic, _, _)) =>
    2.30             Tags (Polymorphic, level, heaviness)
    2.31 @@ -698,14 +699,16 @@
    2.32    | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
    2.33  fun close_combformula_universally phi = close_universally combterm_vars phi
    2.34  
    2.35 -fun term_vars (ATerm (name as (s, _), tms)) =
    2.36 -  is_tptp_variable s ? insert (op =) (name, NONE) #> fold term_vars tms
    2.37 -fun close_formula_universally phi = close_universally term_vars phi
    2.38 +fun term_vars bounds (ATerm (name as (s, _), tms)) =
    2.39 +    (is_tptp_variable s andalso not (member (op =) bounds name))
    2.40 +    ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
    2.41 +  | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
    2.42 +fun close_formula_universally phi = close_universally (term_vars []) phi
    2.43  
    2.44  val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
    2.45  val homo_infinite_type = Type (homo_infinite_type_name, [])
    2.46  
    2.47 -fun fo_term_from_typ format type_enc =
    2.48 +fun ho_term_from_typ format type_enc =
    2.49    let
    2.50      fun term (Type (s, Ts)) =
    2.51        ATerm (case (is_type_enc_higher_order type_enc, s) of
    2.52 @@ -722,8 +725,8 @@
    2.53        ATerm ((make_schematic_type_var x, s), [])
    2.54    in term end
    2.55  
    2.56 -fun fo_term_for_type_arg format type_enc T =
    2.57 -  if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
    2.58 +fun ho_term_for_type_arg format type_enc T =
    2.59 +  if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
    2.60  
    2.61  (* This shouldn't clash with anything else. *)
    2.62  val mangled_type_sep = "\000"
    2.63 @@ -732,6 +735,7 @@
    2.64    | generic_mangled_type_name f (ATerm (name, tys)) =
    2.65      f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
    2.66      ^ ")"
    2.67 +  | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"
    2.68  
    2.69  val bool_atype = AType (`I tptp_bool_type)
    2.70  
    2.71 @@ -742,7 +746,7 @@
    2.72    else
    2.73      simple_type_prefix ^ ascii_of s
    2.74  
    2.75 -fun ho_type_from_fo_term type_enc pred_sym ary =
    2.76 +fun ho_type_from_ho_term type_enc pred_sym ary =
    2.77    let
    2.78      fun to_atype ty =
    2.79        AType ((make_simple_type (generic_mangled_type_name fst ty),
    2.80 @@ -750,17 +754,19 @@
    2.81      fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    2.82      fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
    2.83        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
    2.84 +      | to_fo ary _ = raise Fail "unexpected type abstraction"
    2.85      fun to_ho (ty as ATerm ((s, _), tys)) =
    2.86 -      if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
    2.87 +        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
    2.88 +      | to_ho _ = raise Fail "unexpected type abstraction"
    2.89    in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
    2.90  
    2.91  fun mangled_type format type_enc pred_sym ary =
    2.92 -  ho_type_from_fo_term type_enc pred_sym ary
    2.93 -  o fo_term_from_typ format type_enc
    2.94 +  ho_type_from_ho_term type_enc pred_sym ary
    2.95 +  o ho_term_from_typ format type_enc
    2.96  
    2.97  fun mangled_const_name format type_enc T_args (s, s') =
    2.98    let
    2.99 -    val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
   2.100 +    val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
   2.101      fun type_suffix f g =
   2.102        fold_rev (curry (op ^) o g o prefix mangled_type_sep
   2.103                  o generic_mangled_type_name f) ty_args ""
   2.104 @@ -1444,12 +1450,13 @@
   2.105  fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   2.106    | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
   2.107      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
   2.108 +  | is_var_positively_naked_in_term name _ _ _ = true
   2.109  fun should_predicate_on_var_in_formula pos phi (SOME true) name =
   2.110      formula_fold pos (is_var_positively_naked_in_term name) phi false
   2.111    | should_predicate_on_var_in_formula _ _ _ _ = true
   2.112  
   2.113  fun mk_const_aterm format type_enc x T_args args =
   2.114 -  ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
   2.115 +  ATerm (x, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
   2.116  
   2.117  fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
   2.118    CombConst (type_tag, T --> T, [T])
   2.119 @@ -1924,8 +1931,9 @@
   2.120  val type_info_default_weight = 0.8
   2.121  
   2.122  fun add_term_weights weight (ATerm (s, tms)) =
   2.123 -  is_tptp_user_symbol s ? Symtab.default (s, weight)
   2.124 -  #> fold (add_term_weights weight) tms
   2.125 +    is_tptp_user_symbol s ? Symtab.default (s, weight)
   2.126 +    #> fold (add_term_weights weight) tms
   2.127 +  | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
   2.128  fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
   2.129      formula_fold NONE (K (add_term_weights weight)) phi
   2.130    | add_problem_line_weights _ _ = I