# HG changeset patch # User blanchet # Date 1337800788 -7200 # Node ID adc977fec17e8afcdd1210570c5979f50be24d01 # Parent 08d2dcc2dab907e3c5d94e0b953f0b857fe9badb order LEO-II/Satallax definitions so that they build on each other (cf. Satallax's THF policy) diff -r 08d2dcc2dab9 -r adc977fec17e src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 23 21:19:48 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 23 21:19:48 2012 +0200 @@ -12,7 +12,7 @@ type connective = ATP_Problem.connective type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula type atp_format = ATP_Problem.atp_format - type formula_kind = ATP_Problem.formula_kind + type formula_role = ATP_Problem.formula_role type 'a problem = 'a ATP_Problem.problem datatype mode = Metis | Sledgehammer | Sledgehammer_Aggressive | Exporter @@ -102,7 +102,7 @@ Proof.context -> type_enc -> string -> term list -> term list * term list val factsN : string val prepare_atp_problem : - Proof.context -> atp_format -> formula_kind -> type_enc -> mode -> string + Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list -> string problem * string Symtab.table * (string * stature) list vector @@ -267,7 +267,7 @@ thread. Also, the errors are impossible. *) val unascii_of = let - fun un rcs [] = String.implode(rev rcs) + fun un rcs [] = String.implode (rev rcs) | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *) (* Three types of _ escapes: __, _A to _P, _nnn *) | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs @@ -822,13 +822,13 @@ type translated_formula = {name : string, stature : stature, - kind : formula_kind, + role : formula_role, iformula : (name, typ, iterm) formula, atomic_types : typ list} -fun update_iformula f ({name, stature, kind, iformula, atomic_types} +fun update_iformula f ({name, stature, role, iformula, atomic_types} : translated_formula) = - {name = name, stature = stature, kind = kind, iformula = f iformula, + {name = name, stature = stature, role = role, iformula = f iformula, atomic_types = atomic_types} : translated_formula fun fact_lift f ({iformula, ...} : translated_formula) = f iformula @@ -1230,7 +1230,7 @@ let val (facts, lambda_ts) = facts |> map (snd o snd) |> trans_lams - |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts + |>> map2 (fn (name, (role, _)) => fn t => (name, (role, t))) facts val lam_facts = map2 (fn t => fn j => ((lam_fact_prefix ^ Int.toString j, (Global, Def)), (Axiom, t))) @@ -1285,15 +1285,15 @@ | should_use_iff_for_eq (THF _) format = not (is_type_enc_higher_order format) | should_use_iff_for_eq _ _ = true -fun make_formula ctxt format type_enc iff_for_eq name stature kind t = +fun make_formula ctxt format type_enc iff_for_eq name stature role t = let val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc val (iformula, atomic_Ts) = - iformula_from_prop ctxt type_enc iff_for_eq (SOME (kind <> Conjecture)) t + iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t [] |>> close_iformula_universally in - {name = name, stature = stature, kind = kind, iformula = iformula, + {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts} end @@ -1326,9 +1326,9 @@ *) fun make_conjecture ctxt format type_enc = - map (fn ((name, stature), (kind, t)) => - t |> kind = Conjecture ? s_not - |> make_formula ctxt format type_enc true name stature kind) + map (fn ((name, stature), (role, t)) => + t |> role = Conjecture ? s_not + |> make_formula ctxt format type_enc true name stature role) (** Finite and infinite type inference **) @@ -1893,7 +1893,31 @@ else error ("Unknown lambda translation scheme: " ^ quote lam_trans ^ ".") -fun translate_formulas ctxt prem_kind format type_enc lam_trans presimp hyp_ts +fun order_definitions facts = + let + fun add_consts (IApp (t, u)) = fold add_consts [t, u] + | add_consts (IAbs (_, t)) = add_consts t + | add_consts (IConst (name, _, _)) = insert (op =) name + | add_consts (IVar _) = I + fun consts_of_hs l_or_r (_, {iformula, ...} : translated_formula) = + case iformula of + AAtom (IApp (IApp (IConst _, t), u)) => add_consts (l_or_r (t, u)) [] + | _ => [] + (* Quadratic, but usually OK. *) + fun order [] [] = [] + | order (fact :: skipped) [] = fact :: order [] skipped (* break cycle *) + | order skipped (fact :: facts) = + let val rhs_consts = consts_of_hs snd fact in + if exists (exists (member (op =) rhs_consts o the_single + o consts_of_hs fst)) + [skipped, facts] then + order (fact :: skipped) facts + else + fact :: order [] (facts @ skipped) + end + in order [] facts end + +fun translate_formulas ctxt prem_role format type_enc lam_trans presimp hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt @@ -1906,7 +1930,7 @@ |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t) val facts = facts |> map (apsnd (pair Axiom)) val conjs = - map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_prop concl_t)] + map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)] |> map (apsnd freeze_term) |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts) @@ -1925,7 +1949,9 @@ |> map_filter (fn (name, (_, t)) => make_fact ctxt format type_enc true (name, t) |> Option.map (pair name)) - |> ListPair.unzip + |> List.partition (fn (_, {role, ...}) => role = Definition) + |>> order_definitions + |> op @ |> ListPair.unzip val lifted = lam_facts |> map (extract_lambda_def o snd o snd) val lam_facts = lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) @@ -2086,8 +2112,8 @@ of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun formula_line_for_fact ctxt polym_constrs prefix encode freshen pos - mono type_enc rank (j, {name, stature, kind, iformula, atomic_types}) = - (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, + mono type_enc rank (j, {name, stature, role, iformula, atomic_types}) = + (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, role, iformula |> formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var_in_formula (if pos then SOME true else NONE) @@ -2131,8 +2157,8 @@ NONE, isabelle_info inductiveN helper_rank) fun formula_line_for_conjecture ctxt polym_constrs mono type_enc - ({name, kind, iformula, atomic_types, ...} : translated_formula) = - Formula (conjecture_prefix ^ name, kind, + ({name, role, iformula, atomic_types, ...} : translated_formula) = + Formula (conjecture_prefix ^ name, role, iformula |> formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var_in_formula (SOME false) @@ -2304,8 +2330,8 @@ end | add_iterm_mononotonicity_info _ _ _ _ mono = mono fun add_fact_mononotonicity_info ctxt level - ({kind, iformula, ...} : translated_formula) = - formula_fold (SOME (kind <> Conjecture)) + ({role, iformula, ...} : translated_formula) = + formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula fun mononotonicity_info_for_facts ctxt type_enc facts = let val level = level_of_type_enc type_enc in @@ -2385,14 +2411,14 @@ ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args)) end -fun honor_conj_sym_kind in_conj = +fun honor_conj_sym_role in_conj = if in_conj then (Hypothesis, I) else (Axiom, I) fun formula_line_for_guards_sym_decl ctxt mono type_enc n s j (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt - val (kind, maybe_negate) = honor_conj_sym_kind in_conj + val (role, maybe_negate) = honor_conj_sym_role in_conj val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = @@ -2413,7 +2439,7 @@ replicate ary NONE in Formula (guards_sym_formula_prefix ^ s ^ - (if n > 1 then "_" ^ string_of_int j else ""), kind, + (if n > 1 then "_" ^ string_of_int j else ""), role, IConst ((s, s'), T, T_args) |> fold (curry (IApp o swap)) bounds |> type_guard_iterm type_enc res_T @@ -2435,7 +2461,7 @@ val ident_base = tags_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") - val (kind, maybe_negate) = honor_conj_sym_kind in_conj + val (role, maybe_negate) = honor_conj_sym_role in_conj val (arg_Ts, res_T) = chop_fun ary T val bound_names = 1 upto ary |> map (`I o make_bound_var o string_of_int) val bounds = bound_names |> map (fn name => ATerm (name, [])) @@ -2455,7 +2481,7 @@ else bounds in - cons (Formula (ident_base ^ "_res", kind, + cons (Formula (ident_base ^ "_res", role, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), NONE, isabelle_info defN helper_rank)) end @@ -2517,7 +2543,7 @@ fun do_alias ary = let val thy = Proof_Context.theory_of ctxt - val (kind, maybe_negate) = honor_conj_sym_kind in_conj + val (role, maybe_negate) = honor_conj_sym_role in_conj val base_name = base_s0 |> `(make_fixed_const (SOME type_enc)) val T = case types of [T] => T | _ => robust_const_type thy base_s0 val T_args = robust_const_typargs thy (base_s0, T) @@ -2550,7 +2576,7 @@ (ho_term_of tm1) (ho_term_of tm2) in ([tm1, tm2], - [Formula (uncurried_alias_eq_prefix ^ s2, kind, eq |> maybe_negate, + [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate, NONE, isabelle_info defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) @@ -2670,7 +2696,7 @@ val app_op_and_predicator_threshold = 50 -fun prepare_atp_problem ctxt format prem_kind type_enc mode lam_trans +fun prepare_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases readable_names preproc hyp_ts concl_t facts = let @@ -2700,7 +2726,7 @@ lam_trans val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses, lifted) = - translate_formulas ctxt prem_kind format type_enc lam_trans preproc hyp_ts + translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts concl_t facts val (_, sym_tab0) = sym_table_for_facts ctxt type_enc app_op_level conjs facts