# HG changeset patch # User blanchet # Date 1355435348 -3600 # Node ID bec828f3364e90ba0e1f905a6d4547284b8ebe6f # Parent f2d33310337a471a41de05672e1f95961c4deac3 generate comments with original names for debugging diff -r f2d33310337a -r bec828f3364e src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Thu Dec 13 22:49:07 2012 +0100 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Dec 13 22:49:08 2012 +0100 @@ -34,8 +34,8 @@ fun inference infers ident = these (AList.lookup (op =) infers ident) |> inference_term fun add_inferences_to_problem_line infers - (Formula (ident, Axiom, phi, NONE, tms)) = - Formula (ident, Lemma, phi, inference infers ident, tms) + (Formula ((ident, alt), Axiom, phi, NONE, tms)) = + Formula ((ident, alt), Lemma, phi, inference infers ident, tms) | add_inferences_to_problem_line _ line = line fun add_inferences_to_problem infers = map (apsnd (map (add_inferences_to_problem_line infers))) @@ -44,7 +44,7 @@ | ident_of_problem_line (Type_Decl (ident, _, _)) = ident | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident - | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident + | ident_of_problem_line (Formula ((ident, _), _, _, _, _)) = ident fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN | atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN @@ -83,11 +83,12 @@ [@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] |> map (fact_name_of o Context.theory_name) -fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) = +fun is_problem_line_tautology ctxt format + (Formula ((ident, alt), _, phi, _, _)) = exists (fn prefix => String.isPrefix prefix ident) tautology_prefixes andalso is_none (run_some_atp ctxt format - [(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) + [(factsN, [Formula ((ident, alt), Conjecture, phi, NONE, [])])]) | is_problem_line_tautology _ _ _ = false fun order_facts ord = sort (ord o pairself ident_of_problem_line) diff -r f2d33310337a -r bec828f3364e src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 13 22:49:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Dec 13 22:49:08 2012 +0100 @@ -51,7 +51,7 @@ Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a ho_type | Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | - Formula of string * formula_role + Formula of (string * string) * formula_role * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula * (string, string ho_type) ho_term option * (string, string ho_type) ho_term list @@ -190,7 +190,7 @@ Type_Decl of string * 'a * int | Sym_Decl of string * 'a * 'a ho_type | Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a | - Formula of string * formula_role + Formula of (string * string) * formula_role * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula * (string, string ho_type) ho_term option * (string, string ho_type) ho_term list @@ -479,15 +479,18 @@ fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types +fun tptp_maybe_alt "" = "" + | tptp_maybe_alt s = " % " ^ s + fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) = tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary)) | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) = tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ " : " ^ string_for_type format ty ^ ").\n" - | tptp_string_for_line format (Formula (ident, kind, phi, source, _)) = + | tptp_string_for_line format (Formula ((ident, alt), kind, phi, source, _)) = tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ - tptp_string_for_role kind ^ ",\n (" ^ - tptp_string_for_formula format phi ^ ")" ^ + tptp_string_for_role kind ^ "," ^ tptp_maybe_alt alt ^ + "\n (" ^ tptp_string_for_formula format phi ^ ")" ^ (case source of SOME tm => ", " ^ tptp_string_for_term format tm | NONE => "") ^ ").\n" @@ -582,7 +585,7 @@ else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^ str_for_typ ty ^ ", " ^ cl ^ ")." fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")." - fun formula pred (Formula (ident, kind, phi, _, info)) = + fun formula pred (Formula ((ident, _), kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^ @@ -725,13 +728,13 @@ clausify_formula true (AConn (AImplies, rev phis)) | clausify_formula _ _ = raise CLAUSIFY () -fun clausify_formula_line (Formula (ident, kind, phi, source, info)) = +fun clausify_formula_line (Formula ((ident, alt), kind, phi, source, info)) = let val (n, phis) = phi |> try (clausify_formula true) |> these |> `length in map2 (fn phi => fn j => - Formula (ident ^ replicate_string (j - 1) "x", kind, phi, source, - info)) + Formula ((ident ^ replicate_string (j - 1) "x", alt), kind, phi, + source, info)) phis (1 upto n) end | clausify_formula_line _ = [] diff -r f2d33310337a -r bec828f3364e src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 13 22:49:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Dec 13 22:49:08 2012 +0100 @@ -2128,8 +2128,8 @@ the remote provers might care. *) fun line_for_fact ctxt prefix encode freshen pos mono type_enc rank (j, {name, stature = (_, status), role, iformula, atomic_types}) = - Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ - encode name, + Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ + encode name, name), role, iformula |> formula_from_iformula ctxt mono type_enc @@ -2139,7 +2139,7 @@ NONE, isabelle_info (string_of_status status) (rank j)) fun lines_for_subclass type_enc sub super = - Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom, + Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], @@ -2160,7 +2160,7 @@ prems, native_ho_type_from_typ type_enc false 0 T, `make_class cl) else - Formula (tcon_clause_prefix ^ name, Axiom, + Formula ((tcon_clause_prefix ^ name, ""), Axiom, mk_ahorn (maps (class_atoms type_enc) prems) (class_atom type_enc (cl, T)) |> bound_tvars type_enc true (snd (dest_Type T)), @@ -2168,7 +2168,7 @@ fun line_for_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) = - Formula (conjecture_prefix ^ name, role, + Formula ((conjecture_prefix ^ name, ""), role, iformula |> formula_from_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false) @@ -2186,7 +2186,7 @@ native_ho_type_from_typ type_enc false 0 T, `make_class cl) else - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, + Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis, class_atom type_enc (cl, T), NONE, []) val membs = fold (union (op =)) (map #atomic_types facts) [] @@ -2347,8 +2347,7 @@ end fun line_for_guards_mono_type ctxt mono type_enc T = - Formula (guards_sym_formula_prefix ^ - ascii_of (mangled_type type_enc T), + Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, IConst (`make_bound_var "X", T, []) |> type_guard_iterm type_enc T @@ -2361,8 +2360,7 @@ fun line_for_tags_mono_type ctxt mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in - Formula (tags_sym_formula_prefix ^ - ascii_of (mangled_type type_enc T), + Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, eq_formula type_enc (atomic_types_of T) [] false (tag_with_type ctxt mono type_enc NONE T x_var) x_var, @@ -2419,8 +2417,9 @@ end | _ => replicate ary NONE in - Formula (guards_sym_formula_prefix ^ s ^ - (if n > 1 then "_" ^ string_of_int j else ""), role, + Formula ((guards_sym_formula_prefix ^ s ^ + (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 @@ -2449,8 +2448,8 @@ val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym val tag_with = tag_with_type ctxt mono type_enc NONE fun formula c = - [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info - non_rec_defN helper_rank)] + [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE, + isabelle_info non_rec_defN helper_rank)] in if pred_sym orelse not (should_encode_type ctxt mono level res_T) then [] @@ -2549,8 +2548,9 @@ (ho_term_of tm1) (ho_term_of tm2) in ([tm1, tm2], - [Formula (uncurried_alias_eq_prefix ^ s2, role, eq |> maybe_negate, - NONE, isabelle_info non_rec_defN helper_rank)]) + [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, + eq |> maybe_negate, NONE, + isabelle_info non_rec_defN helper_rank)]) |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I else pair_append (do_alias (ary - 1))) end diff -r f2d33310337a -r bec828f3364e src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 13 22:49:07 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Dec 13 22:49:08 2012 +0100 @@ -364,7 +364,7 @@ | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false -fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) = +fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) = if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE diff -r f2d33310337a -r bec828f3364e src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Thu Dec 13 22:49:07 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Thu Dec 13 22:49:08 2012 +0100 @@ -161,7 +161,7 @@ fun metis_literals_from_atp type_enc (AConn (AOr, phis)) = maps (metis_literals_from_atp type_enc) phis | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi] -fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) = +fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) = let fun some isa = SOME (phi |> metis_literals_from_atp type_enc