# HG changeset patch # User nik # Date 1309882199 -3600 # Node ID 3b0b448b4d69e13c8050913cf307067fc94cda72 # Parent e8c80bbc0c5d6f4b555273b625e1de3d11358c95 add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order) diff -r e8c80bbc0c5d -r 3b0b448b4d69 src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r e8c80bbc0c5d -r 3b0b448b4d69 src/HOL/Tools/ATP/atp_translate.ML --- 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