# HG changeset patch # User blanchet # Date 1314713265 -7200 # Node ID ccf40af26ae91642a1d910f0f02cbdd9630f7028 # Parent 54906b0337ab99b75bc44528e9efe1963948057b implement more of the polymorphic simply typed format TFF(1) diff -r 54906b0337ab -r ccf40af26ae9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Aug 30 16:07:45 2011 +0200 @@ -17,7 +17,9 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c - datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type + datatype 'a ho_type = + AType of 'a * 'a ho_type list | + AFun of 'a ho_type * 'a ho_type datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic datatype tff_explicitness = TFF_Implicit | TFF_Explicit @@ -118,7 +120,9 @@ AConn of connective * ('a, 'b, 'c) formula list | AAtom of 'c -datatype 'a ho_type = AType of 'a | AFun of 'a ho_type * 'a ho_type +datatype 'a ho_type = + AType of 'a * 'a ho_type list | + AFun of 'a ho_type * 'a ho_type datatype tff_polymorphism = TFF_Monomorphic | TFF_Polymorphic datatype tff_explicitness = TFF_Implicit | TFF_Explicit @@ -225,25 +229,29 @@ | string_for_kind Hypothesis = "hypothesis" | string_for_kind Conjecture = "conjecture" -fun strip_tff_type (AFun (AType s, ty)) = strip_tff_type ty |>> cons s - | strip_tff_type (AFun (AFun _, _)) = +fun strip_tff_type (AFun (AFun _, _)) = raise Fail "unexpected higher-order type in first-order format" - | strip_tff_type (AType s) = ([], s) + | strip_tff_type (AFun (ty1, ty2)) = strip_tff_type ty2 |>> cons ty1 + | strip_tff_type ty = ([], ty) -fun string_for_type (THF0 _) ty = - let - fun aux _ (AType s) = s - | aux rhs (AFun (ty1, ty2)) = - aux false ty1 ^ " " ^ tptp_fun_type ^ " " ^ aux true ty2 - |> not rhs ? enclose "(" ")" - in aux true ty end +fun general_string_for_type ty = + let + fun str _ (AType (s, [])) = s + | str _ (AType (s, tys)) = s ^ "(" ^ commas (map (str false) tys) ^ ")" + | str rhs (AFun (ty1, ty2)) = + str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 + |> not rhs ? enclose "(" ")" + in str true ty end + +fun string_for_type (THF0 _) ty = general_string_for_type ty | string_for_type (TFF _) ty = (case strip_tff_type ty of - ([], s) => s - | ([s'], s) => s' ^ " " ^ tptp_fun_type ^ " " ^ s - | (ss, s) => - "(" ^ space_implode (" " ^ tptp_product_type ^ " ") ss ^ ") " ^ - tptp_fun_type ^ " " ^ s) + ([], ty) => general_string_for_type ty + | ([ty1], ty2) => general_string_for_type (AFun (ty1, ty2)) + | (tys, ty) => + "(" ^ space_implode (" " ^ tptp_product_type ^ " ") + (map general_string_for_type tys) ^ ") " ^ tptp_fun_type ^ " " ^ + general_string_for_type ty) | string_for_type _ _ = raise Fail "unexpected type in untyped format" fun string_for_quantifier AForall = tptp_forall @@ -256,11 +264,13 @@ | string_for_connective AIff = tptp_iff fun string_for_bound_var format (s, ty) = - s ^ (if is_format_typed format then - " " ^ tptp_has_type ^ " " ^ - string_for_type format (ty |> the_default (AType tptp_individual_type)) - else - "") + s ^ + (if is_format_typed format then + " " ^ tptp_has_type ^ " " ^ + (ty |> the_default (AType (tptp_individual_type, [])) + |> string_for_type format) + else + "") fun string_for_term _ (ATerm (s, [])) = s | string_for_term format (ATerm (s, ts)) = @@ -440,9 +450,9 @@ symbols (with "$i" as the type of individuals), but some provers (e.g., SNARK) require explicit declarations. The situation is similar for THF. *) -val atype_of_types = AType (`I tptp_type_of_types) -val bool_atype = AType (`I tptp_bool_type) -val individual_atype = AType (`I tptp_individual_type) +val atype_of_types = AType (`I tptp_type_of_types, []) +val bool_atype = AType (`I tptp_bool_type, []) +val individual_atype = AType (`I tptp_individual_type, []) fun default_type pred_sym = let @@ -459,8 +469,9 @@ let fun do_sym name ty = if member (op =) declared name then I else AList.default (op =) (name, ty) - fun do_type (AFun (ty1, ty2)) = fold do_type [ty1, ty2] - | do_type (AType name) = do_sym name (K atype_of_types) + fun do_type (AType (name, tys)) = + do_sym name (K atype_of_types) #> fold do_type tys + | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2 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)) @@ -557,7 +568,8 @@ end in add 0 |> apsnd SOME end -fun nice_type (AType name) = nice_name name #>> AType +fun nice_type (AType (name, tys)) = + nice_name name ##>> pool_map nice_type tys #>> 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 diff -r 54906b0337ab -r ccf40af26ae9 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:07:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 16:07:45 2011 +0200 @@ -763,11 +763,25 @@ | iterm_vars (IAbs (_, tm)) = iterm_vars tm fun close_iformula_universally phi = close_universally iterm_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 +fun term_vars type_enc = + let + fun vars bounds (ATerm (name as (s, _), tms)) = + (if is_tptp_variable s andalso not (member (op =) bounds name) then + (case type_enc of + Simple_Types (_, Polymorphic, _) => + if String.isPrefix tvar_prefix s then + SOME (AType (`I tptp_type_of_types, [])) + else + NONE + | _ => NONE) + |> pair name |> insert (op =) + else + I) + #> fold (vars bounds) tms + | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm + in vars end +fun close_formula_universally type_enc = + close_universally (term_vars type_enc []) val homo_infinite_type_name = @{type_name ind} (* any infinite type *) val homo_infinite_type = Type (homo_infinite_type_name, []) @@ -804,7 +818,7 @@ fun mangled_type format type_enc = generic_mangled_type_name fst o ho_term_from_typ format type_enc -val bool_atype = AType (`I tptp_bool_type) +val bool_atype = AType (`I tptp_bool_type, []) fun make_simple_type s = if s = tptp_bool_type orelse s = tptp_fun_type orelse @@ -815,9 +829,14 @@ fun ho_type_from_ho_term type_enc pred_sym ary = let - fun to_atype ty = + fun to_mangled_atype ty = AType ((make_simple_type (generic_mangled_type_name fst ty), - generic_mangled_type_name snd ty)) + generic_mangled_type_name snd ty), []) + fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) + | to_poly_atype _ = raise Fail "unexpected type abstraction" + val to_atype = + if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype + else to_mangled_atype 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 @@ -1454,7 +1473,7 @@ (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2]) else AAtom (ATerm (`I tptp_equal, [tm1, tm2]))) |> bound_tvars type_enc atomic_Ts - |> close_formula_universally + |> close_formula_universally type_enc val type_tag = `(make_fixed_const NONE) type_tag_name @@ -1717,7 +1736,7 @@ should_guard_var_in_formula (if pos then SOME true else NONE) |> bound_tvars type_enc atomic_types - |> close_formula_universally, + |> close_formula_universally type_enc, NONE, case locality of Intro => isabelle_info introN @@ -1726,13 +1745,13 @@ | _ => NONE) |> Formula -fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...} - : class_rel_clause) = +fun formula_line_for_class_rel_clause type_enc + ({name, subclass, superclass, ...} : class_rel_clause) = let val ty_arg = ATerm (`I "T", []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), AAtom (ATerm (superclass, [ty_arg]))]) - |> close_formula_universally, isabelle_info introN, NONE) + |> close_formula_universally type_enc, isabelle_info introN, NONE) end fun fo_literal_from_arity_literal (TConsLit (c, t, args)) = @@ -1740,14 +1759,14 @@ | fo_literal_from_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...} - : arity_clause) = +fun formula_line_for_arity_clause type_enc + ({name, prem_lits, concl_lits, ...} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, mk_ahorn (map (formula_from_fo_literal o apfst not o fo_literal_from_arity_literal) prem_lits) (formula_from_fo_literal (fo_literal_from_arity_literal concl_lits)) - |> close_formula_universally, isabelle_info introN, NONE) + |> close_formula_universally type_enc, isabelle_info introN, NONE) fun formula_line_for_conjecture ctxt format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -1756,7 +1775,7 @@ should_guard_var_in_formula (SOME false) (close_iformula_universally iformula) |> bound_tvars type_enc atomic_types - |> close_formula_universally, NONE, NONE) + |> close_formula_universally type_enc, NONE, NONE) fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) = atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree @@ -1921,7 +1940,7 @@ |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> bound_tvars type_enc (atyps_of T) - |> close_formula_universally, + |> close_formula_universally type_enc, isabelle_info introN, NONE) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = @@ -1983,7 +2002,7 @@ |> formula_from_iformula ctxt format mono type_enc (K (K (K (K true)))) (SOME true) |> n > 1 ? bound_tvars type_enc (atyps_of T) - |> close_formula_universally + |> close_formula_universally type_enc |> maybe_negate, isabelle_info introN, NONE) end @@ -2174,8 +2193,9 @@ (not exporter) (not exporter) mono type_enc) (0 upto length facts - 1 ~~ facts)), - (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses), - (aritiesN, map formula_line_for_arity_clause arity_clauses), + (class_relsN, + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), + (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), (helpersN, helper_lines), (conjsN, map (formula_line_for_conjecture ctxt format mono type_enc) conjs),