# HG changeset patch # User blanchet # Date 1280440945 -7200 # Node ID 373351f5f834b97bf12a625665f8be2efb48842e # Parent 8fbf60c3379433e4d175768650182e63d79cc8ac don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names... diff -r 8fbf60c33794 -r 373351f5f834 src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 29 23:37:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Jul 30 00:02:25 2010 +0200 @@ -16,9 +16,9 @@ TConsLit of name * name * name list | TVarLit of name * name datatype arity_clause = - ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} datatype class_rel_clause = - ClassRelClause of {axiom_name: string, subclass: name, superclass: name} + ClassRelClause of {name: string, subclass: name, superclass: name} datatype combtyp = CombTVar of name | CombTFree of name | @@ -84,8 +84,6 @@ val tvar_prefix = "T_"; val tfree_prefix = "t_"; -val class_rel_clause_prefix = "clsrel_"; - val const_prefix = "c_"; val type_const_prefix = "tc_"; val class_prefix = "class_"; @@ -259,7 +257,7 @@ TVarLit of name * name datatype arity_clause = - ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list} + ArityClause of {name: string, conclLit: arLit, premLits: arLit list} fun gen_TVars 0 = [] @@ -271,12 +269,12 @@ (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt) (*Arity of type constructor tcon :: (arg1,...,argN)res*) -fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) = +fun make_axiom_arity_clause (tcons, name, (cls,args)) = let val tvars = gen_TVars (length args) val tvars_srts = ListPair.zip (tvars, args) in - ArityClause {axiom_name = axiom_name, + ArityClause {name = name, conclLit = TConsLit (`make_type_class cls, `make_fixed_type_const tcons, tvars ~~ tvars), @@ -287,7 +285,7 @@ (**** Isabelle class relations ****) datatype class_rel_clause = - ClassRelClause of {axiom_name: string, subclass: name, superclass: name} + ClassRelClause of {name: string, subclass: name, superclass: name} (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*) fun class_pairs _ [] _ = [] @@ -299,10 +297,9 @@ in fold add_supers subs [] end fun make_class_rel_clause (sub,super) = - ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^ - ascii_of super, + ClassRelClause {name = sub ^ "_" ^ super, subclass = `make_type_class sub, - superclass = `make_type_class super}; + superclass = `make_type_class super} fun make_class_rel_clauses thy subs supers = map make_class_rel_clause (class_pairs thy subs supers); diff -r 8fbf60c33794 -r 373351f5f834 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 23:37:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jul 30 00:02:25 2010 +0200 @@ -162,7 +162,7 @@ (* Clause preparation *) datatype fol_formula = - FOLFormula of {formula_name: string, + FOLFormula of {name: string, kind: kind, combformula: (name, combterm) formula, ctypes_sorts: typ list} @@ -296,7 +296,7 @@ in t |> exists_subterm is_Var t ? aux end (* making axiom and conjecture formulas *) -fun make_formula ctxt presimp (formula_name, kind, t) = +fun make_formula ctxt presimp (name, kind, t) = let val thy = ProofContext.theory_of ctxt val t = t |> transform_elim_term @@ -309,8 +309,8 @@ |> kind = Conjecture ? freeze_term val (combformula, ctypes_sorts) = combformula_for_prop thy t [] in - FOLFormula {formula_name = formula_name, combformula = combformula, - kind = kind, ctypes_sorts = ctypes_sorts} + FOLFormula {name = name, combformula = combformula, kind = kind, + ctypes_sorts = ctypes_sorts} end fun make_axiom ctxt presimp (name, th) = @@ -433,15 +433,14 @@ (type_literals_for_types ctypes_sorts)) (formula_for_combformula full_types combformula) -fun problem_line_for_axiom full_types - (formula as FOLFormula {formula_name, kind, ...}) = - Fof (axiom_prefix ^ ascii_of formula_name, kind, - formula_for_axiom full_types formula) +fun problem_line_for_fact prefix full_types + (formula as FOLFormula {name, kind, ...}) = + Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula) -fun problem_line_for_class_rel_clause - (ClassRelClause {axiom_name, subclass, superclass, ...}) = +fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, + superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in - Fof (ascii_of axiom_name, Axiom, + Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), AAtom (ATerm (superclass, [ty_arg]))])) end @@ -451,17 +450,17 @@ | fo_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun problem_line_for_arity_clause - (ArityClause {axiom_name, conclLit, premLits, ...}) = - Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, +fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, + ...}) = + Fof (arity_clause_prefix ^ ascii_of name, Axiom, mk_ahorn (map (formula_for_fo_literal o apfst not o fo_literal_for_arity_literal) premLits) (formula_for_fo_literal (fo_literal_for_arity_literal conclLit))) fun problem_line_for_conjecture full_types - (FOLFormula {formula_name, kind, combformula, ...}) = - Fof (conjecture_prefix ^ formula_name, kind, + (FOLFormula {name, kind, combformula, ...}) = + Fof (conjecture_prefix ^ name, kind, formula_for_combformula full_types combformula) fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) = @@ -608,14 +607,15 @@ file (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses) = let - val axiom_lines = map (problem_line_for_axiom full_types) axioms + val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms + val helper_lines = + map (problem_line_for_fact helper_prefix full_types) helper_facts + val conjecture_lines = + map (problem_line_for_conjecture full_types) conjectures + val tfree_lines = problem_lines_for_free_types conjectures val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses val arity_lines = map problem_line_for_arity_clause arity_clauses - val helper_lines = map (problem_line_for_axiom full_types) helper_facts - val conjecture_lines = - map (problem_line_for_conjecture full_types) conjectures - val tfree_lines = problem_lines_for_free_types conjectures (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) val problem = @@ -647,7 +647,8 @@ val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id + --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")" --| Scan.option ($$ ",") val parse_clause_formula_relation = Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" @@ -673,8 +674,8 @@ |> map (fn s => find_index (curry (op =) s) seq + 1) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map (the o AList.lookup (op =) name_map) - |> map (fn s => case try (unprefix axiom_prefix) s of + seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the + |> try (unprefix axiom_prefix) of SOME s' => undo_ascii_of s' | NONE => "") |> Vector.fromList) diff -r 8fbf60c33794 -r 373351f5f834 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 23:37:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 30 00:02:25 2010 +0200 @@ -12,6 +12,8 @@ val axiom_prefix : string val conjecture_prefix : string + val helper_prefix : string + val class_rel_clause_prefix : string val arity_clause_prefix : string val tfrees_name : string val metis_line: bool -> int -> int -> string list -> string @@ -40,7 +42,9 @@ val axiom_prefix = "ax_" val conjecture_prefix = "conj_" -val arity_clause_prefix = "clsarity_" +val helper_prefix = "help_" +val class_rel_clause_prefix = "clrel_"; +val arity_clause_prefix = "arity_" val tfrees_name = "tfrees" (* Simple simplifications to ensure that sort annotations don't leave a trail of @@ -500,7 +504,7 @@ | (pre, Inference (num', _, _) :: post) => pre @ map (replace_deps_in_line (num', [num])) post else if is_conjecture_number conjecture_shape num then - Inference (num, t, []) :: lines + Inference (num, negate_term t, []) :: lines else map (replace_deps_in_line (num, [])) lines | add_line _ _ (Inference (num, t, deps)) lines =