diff -r ea6695d58aad -r 2409b484e1cc src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 20 00:44:30 2012 +0100 @@ -108,7 +108,7 @@ -> string problem * string Symtab.table * (string * stature) list vector * (string * term) list * int Symtab.table val atp_problem_selection_weights : string problem -> (string * real) list - val atp_problem_term_order_weights : string problem -> (string * int) list + val atp_problem_term_order_info : string problem -> (string * int) list end; structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE = @@ -1671,7 +1671,7 @@ val type_tag = `(make_fixed_const NONE) type_tag_name -fun type_tag_idempotence_fact format type_enc = +fun type_tag_idempotence_fact type_enc = let fun var s = ATerm (`I s, []) fun tag tm = ATerm (type_tag, [var "A", tm]) @@ -1679,7 +1679,7 @@ in Formula (type_tag_idempotence_helper_name, Axiom, eq_formula type_enc [] [] false (tag tagged_var) tagged_var, - NONE, isabelle_info format spec_eqN helper_rank) + NONE, isabelle_info spec_eqN helper_rank) end fun should_specialize_helper type_enc t = @@ -2006,15 +2006,15 @@ NONE, let val rank = rank j in case snd stature of - Intro => isabelle_info format introN rank - | Elim => isabelle_info format elimN rank - | Simp => isabelle_info format simpN rank - | Spec_Eq => isabelle_info format spec_eqN rank - | _ => isabelle_info format "" rank + Intro => isabelle_info introN rank + | Elim => isabelle_info elimN rank + | Simp => isabelle_info simpN rank + | Spec_Eq => isabelle_info spec_eqN rank + | _ => isabelle_info "" rank end) |> Formula -fun formula_line_for_class_rel_clause format type_enc +fun formula_line_for_class_rel_clause type_enc ({name, subclass, superclass, ...} : class_rel_clause) = let val ty_arg = ATerm (tvar_a_name, []) in Formula (class_rel_clause_prefix ^ ascii_of name, Axiom, @@ -2023,21 +2023,21 @@ type_class_formula type_enc superclass ty_arg]) |> mk_aquant AForall [(tvar_a_name, atype_of_type_vars type_enc)], - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) end fun formula_from_arity_atom type_enc (class, t, args) = ATerm (t, map (fn arg => ATerm (arg, [])) args) |> type_class_formula type_enc class -fun formula_line_for_arity_clause format type_enc +fun formula_line_for_arity_clause type_enc ({name, prem_atoms, concl_atom} : arity_clause) = Formula (arity_clause_prefix ^ name, Axiom, mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms) (formula_from_arity_atom type_enc concl_atom) |> mk_aquant AForall (map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)), - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs format mono type_enc ({name, kind, iformula, atomic_types, ...} : translated_formula) = @@ -2246,7 +2246,7 @@ always_guard_var_in_formula (SOME true) |> close_formula_universally |> bound_tvars type_enc true (atomic_types_of T), - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) fun formula_line_for_tags_mono_type ctxt format mono type_enc T = let val x_var = ATerm (`make_bound_var "X", []) in @@ -2255,7 +2255,7 @@ Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt format mono type_enc NONE T x_var) x_var, - NONE, isabelle_info format spec_eqN helper_rank) + NONE, isabelle_info spec_eqN helper_rank) end fun problem_lines_for_mono_types ctxt format mono type_enc Ts = @@ -2326,7 +2326,7 @@ |> close_formula_universally |> bound_tvars type_enc (n > 1) (atomic_types_of T) |> maybe_negate, - NONE, isabelle_info format introN helper_rank) + NONE, isabelle_info introN helper_rank) end fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind mono type_enc n s @@ -2360,7 +2360,7 @@ in cons (Formula (ident_base ^ "_res", kind, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), - NONE, isabelle_info format spec_eqN helper_rank)) + NONE, isabelle_info spec_eqN helper_rank)) end else I @@ -2372,7 +2372,7 @@ cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind, eq (cst (bounds1 @ tag_with arg_T bound :: bounds2)) (cst bounds), - NONE, isabelle_info format spec_eqN helper_rank)) + NONE, isabelle_info spec_eqN helper_rank)) | _ => raise Fail "expected nonempty tail" else I @@ -2480,7 +2480,7 @@ in ([tm1, tm2], [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, - NONE, isabelle_info format spec_eqN helper_rank)]) + NONE, isabelle_info spec_eqN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end @@ -2663,7 +2663,7 @@ |> map (formula_line_for_fact ctxt polym_constrs format helper_prefix I false true mono type_enc (K default_rank)) |> (if needs_type_tag_idempotence ctxt type_enc then - cons (type_tag_idempotence_fact format type_enc) + cons (type_tag_idempotence_fact type_enc) else I) (* Reordering these might confuse the proof reconstruction code or the SPASS @@ -2673,10 +2673,8 @@ (uncurried_alias_eqsN, uncurried_alias_eq_lines), (factsN, fact_lines), (class_relsN, - map (formula_line_for_class_rel_clause format type_enc) - class_rel_clauses), - (aritiesN, - map (formula_line_for_arity_clause format type_enc) arity_clauses), + 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), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)), (conjsN, @@ -2756,22 +2754,26 @@ val max_term_order_weight = 2147483647 -fun atp_problem_term_order_weights problem = +fun atp_problem_term_order_info problem = let + fun add_edge s s' = + Graph.default_node (s, ()) + #> Graph.default_node (s', ()) + #> Graph.add_edge_acyclic (s, s') fun add_term_deps head (ATerm (s, args)) = - is_tptp_user_symbol s ? perhaps (try (Graph.add_edge_acyclic (s, head))) + is_tptp_user_symbol s ? perhaps (try (add_edge s head)) #> fold (add_term_deps head) args | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm fun add_eq_deps (ATerm (s, [lhs as _, rhs])) = if is_tptp_equal s then - let val (head, rest) = make_head_roll lhs in - fold (add_term_deps head) (rhs :: rest) - end + case make_head_roll lhs of + (head, rest as _ :: _) => + is_tptp_user_symbol head ? fold (add_term_deps head) (rhs :: rest) + | _ => I else I | add_eq_deps _ = I - fun add_line_deps _ (Decl (_, s, ty)) = - is_function_type ty ? Graph.default_node (s, ()) + fun add_line_deps _ (Decl _) = I | add_line_deps status (Formula (_, _, phi, _, info)) = if extract_isabelle_status info = SOME status then formula_fold NONE (K add_eq_deps) phi @@ -2787,6 +2789,8 @@ #> add_weights (next_weight weight) (fold (union (op =) o Graph.immediate_succs graph) syms []) in + (* Sorting is not just for aesthetics: It specifies the precedence order + for the term ordering (KBO or LPO), from smaller to larger values. *) [] |> add_weights 1 (Graph.minimals graph) |> sort (int_ord o pairself snd) end