# HG changeset patch # User blanchet # Date 1279739707 -7200 # Node ID e6ff246c0cdb4d4e26a56a34a23b8ea5d6554b79 # Parent 1188e6bff48dabc1248eb905f3fc157fb5134f1f renamings + only need second component of name pool to reconstruct proofs diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Jul 21 21:15:07 2010 +0200 @@ -9,7 +9,6 @@ signature ATP_MANAGER = sig type relevance_override = Sledgehammer_Fact_Filter.relevance_override - type name_pool = Sledgehammer_TPTP_Format.name_pool type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = {debug: bool, @@ -38,7 +37,7 @@ type prover_result = {outcome: failure option, message: string, - pool: name_pool option, + pool: string Symtab.table, relevant_thm_names: string list, atp_run_time_in_msecs: int, output: string, @@ -108,7 +107,7 @@ type prover_result = {outcome: failure option, message: string, - pool: name_pool option, + pool: string Symtab.table, relevant_thm_names: string list, atp_run_time_in_msecs: int, output: string, diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Wed Jul 21 21:15:07 2010 +0200 @@ -19,7 +19,6 @@ structure ATP_Systems : ATP_SYSTEMS = struct -open Clausifier open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter @@ -134,7 +133,7 @@ filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) = - (pos andalso c = "c_False") orelse (not pos andalso c = "c_True") + c = (if pos then "c_False" else "c_True") | is_false_literal _ = false fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) = (pol andalso c = "c_True") orelse @@ -185,7 +184,7 @@ fun cnf_helper_thms thy raw = map (`Thm.get_name_hint) - #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true) + #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true) val optional_helpers = [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})), @@ -256,7 +255,7 @@ (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt; - val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal) + val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal) val goal_cls = List.concat goal_clss val the_filtered_clauses = case filtered_clauses of @@ -265,7 +264,7 @@ relevance_convergence defs_relevant max_axiom_clauses (the_default prefers_theory_relevant theory_relevant) relevance_override goal goal_cls - |> cnf_rules_pairs thy true + |> Clausifier.cnf_rules_pairs thy true val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses val (internal_thm_names, clauses) = prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/metis_clauses.ML --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Wed Jul 21 21:15:07 2010 +0200 @@ -75,8 +75,6 @@ structure Metis_Clauses : METIS_CLAUSES = struct -open Clausifier - val type_wrapper_name = "ti" val schematic_var_prefix = "V_"; diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Jul 21 21:15:07 2010 +0200 @@ -18,7 +18,6 @@ structure Metis_Tactics : METIS_TACTICS = struct -open Clausifier open Metis_Clauses exception METIS of string * string @@ -70,10 +69,10 @@ fun metis_lit b c args = (b, (c, args)); -fun hol_type_to_fol (CombTVar (x, _)) = Metis.Term.Var x - | hol_type_to_fol (CombTFree (s, _)) = Metis.Term.Fn (s, []) - | hol_type_to_fol (CombType ((s, _), tps)) = - Metis.Term.Fn (s, map hol_type_to_fol tps); +fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s + | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, []) + | metis_term_from_combtyp (CombType ((s, _), tps)) = + Metis.Term.Fn (s, map metis_term_from_combtyp tps); (*These two functions insert type literals before the real literals. That is the opposite order from TPTP linkup, but maybe OK.*) @@ -81,7 +80,7 @@ fun hol_term_to_fol_FO tm = case strip_combterm_comb tm of (CombConst ((c, _), _, tys), tms) => - let val tyargs = map hol_type_to_fol tys + let val tyargs = map metis_term_from_combtyp tys val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end | (CombVar ((v, _), _), []) => Metis.Term.Var v @@ -89,12 +88,12 @@ fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = - Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) + Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist) | hol_term_to_fol_HO (CombApp (tm1, tm2)) = Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]); (*The fully-typed translation, to avoid type errors*) -fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); +fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]); fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty) | hol_term_to_fol_FT (CombConst((a, _), ty, _)) = @@ -105,7 +104,7 @@ fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) = let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm - val tylits = if p = "equal" then [] else map hol_type_to_fol tys + val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys val lits = map hol_term_to_fol_FO tms in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end | hol_literal_to_fol HO (FOLLiteral (pos, tm)) = @@ -223,22 +222,23 @@ fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) -fun fol_type_to_isa _ (Metis.Term.Var v) = +fun hol_type_from_metis_term _ (Metis.Term.Var v) = (case strip_prefix tvar_prefix v of SOME w => make_tvar w | NONE => make_tvar v) - | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = + | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) = (case strip_prefix type_const_prefix x of - SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys) + SOME tc => Term.Type (invert_const tc, + map (hol_type_from_metis_term ctxt) tys) | NONE => case strip_prefix tfree_prefix x of SOME tf => mk_tfree ctxt tf - | NONE => raise Fail ("fol_type_to_isa: " ^ x)); + | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); (*Maps metis terms to isabelle terms*) -fun hol_term_from_fol_PT ctxt fol_tm = +fun hol_term_from_metis_PT ctxt fol_tm = let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^ + val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = (case strip_prefix tvar_prefix v of @@ -298,8 +298,8 @@ end (*Maps fully-typed metis terms to isabelle terms*) -fun hol_term_from_fol_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^ +fun hol_term_from_metis_FT ctxt fol_tm = + let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = (case strip_prefix schematic_var_prefix v of @@ -312,8 +312,8 @@ SOME c => Const (invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix fixed_var_prefix x of - SOME v => Free (v, fol_type_to_isa ctxt ty) - | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x)) + SOME v => Free (v, hol_type_from_metis_term ctxt ty) + | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = cvt tm1 $ cvt tm2 | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) @@ -327,17 +327,17 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x); - hol_term_from_fol_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t); - hol_term_from_fol_PT ctxt t) + | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); + hol_term_from_metis_PT ctxt t)) + | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t); + hol_term_from_metis_PT ctxt t) in fol_tm |> cvt end -fun hol_term_from_fol FT = hol_term_from_fol_FT - | hol_term_from_fol _ = hol_term_from_fol_PT +fun hol_term_from_metis FT = hol_term_from_metis_FT + | hol_term_from_metis _ = hol_term_from_metis_PT fun hol_terms_from_fol ctxt mode skolems fol_tms = - let val ts = map (hol_term_from_fol mode ctxt) fol_tms + let val ts = map (hol_term_from_metis mode ctxt) fol_tms val _ = trace_msg (fn () => " calling type inference:") val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt @@ -398,7 +398,7 @@ fun subst_translation (x,y) = let val v = find_var x (* We call "reveal_skolem_terms" and "infer_types" below. *) - val t = hol_term_from_fol mode ctxt y + val t = hol_term_from_metis mode ctxt y in SOME (cterm_of thy (Var v), t) end handle Option => (trace_msg (fn() => "List.find failed for the variable " ^ x ^ @@ -599,7 +599,7 @@ (* ------------------------------------------------------------------------- *) fun cnf_helper_theorem thy raw th = - if raw then th else the_single (cnf_axiom thy false th) + if raw then th else the_single (Clausifier.cnf_axiom thy false th) fun type_ext thy tms = let val subs = tfree_classes_of_terms tms @@ -715,7 +715,7 @@ fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt val th_cls_pairs = - map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0 + map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0 val ths = maps #2 th_cls_pairs val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls @@ -774,15 +774,16 @@ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) fun generic_metis_tac mode ctxt ths i st0 = - let val _ = trace_msg (fn () => + let + val _ = trace_msg (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in if exists_type type_has_top_sort (prop_of st0) then (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) else - (Meson.MESON (maps neg_clausify) - (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) - ctxt i) st0 + Meson.MESON (maps Clausifier.neg_clausify) + (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) + ctxt i st0 handle ERROR msg => raise METIS ("generic_metis_tac", msg) end handle METIS (loc, msg) => @@ -800,7 +801,8 @@ fun method name mode = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => - SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths))) + METHOD (fn facts => HEADGOAL (CHANGED_PROP + o generic_metis_tac mode ctxt (facts @ ths))))) val setup = type_lits_setup diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Wed Jul 21 21:15:07 2010 +0200 @@ -18,7 +18,6 @@ structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER = struct -open Clausifier open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Proof_Reconstruct @@ -56,7 +55,7 @@ val _ = priority ("Testing " ^ string_of_int num_theorems ^ " theorem" ^ plural_s num_theorems ^ "...") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = cnf_rules_pairs thy true name_thm_pairs + val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Jul 21 21:15:07 2010 +0200 @@ -17,7 +17,6 @@ structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct -open Clausifier open Sledgehammer_Util open Sledgehammer_Fact_Filter open ATP_Manager diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Jul 21 21:15:07 2010 +0200 @@ -8,18 +8,17 @@ signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig type minimize_command = string list -> string - type name_pool = Sledgehammer_TPTP_Format.name_pool val metis_line: bool -> int -> int -> string list -> string val metis_proof_text: bool * minimize_command * string * string vector * thm * int -> string * string list val isar_proof_text: - name_pool option * bool * int * Proof.context * int list list + string Symtab.table * bool * int * Proof.context * int list list -> bool * minimize_command * string * string vector * thm * int -> string * string list val proof_text: - bool -> name_pool option * bool * int * Proof.context * int list list + bool -> string Symtab.table * bool * int * Proof.context * int list list -> bool * minimize_command * string * string vector * thm * int -> string * string list end; @@ -27,7 +26,6 @@ structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = struct -open Clausifier open Metis_Clauses open Sledgehammer_Util open Sledgehammer_Fact_Filter @@ -44,12 +42,6 @@ fun is_conjecture_clause_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 -fun ugly_name NONE s = s - | ugly_name (SOME the_pool) s = - case Symtab.lookup (snd the_pool) s of - SOME s' => s' - | NONE => s - fun smart_lambda v t = Abs (case v of Const (s, _) => @@ -104,7 +96,7 @@ | repair_name _ "$false" = "c_False" | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *) | repair_name _ "equal" = "c_equal" (* probably not needed *) - | repair_name pool s = ugly_name pool s + | repair_name pool s = Symtab.lookup pool s |> the_default s (* Generalized first-order terms, which include file names, numbers, etc. *) (* The "x" argument is not strictly necessary, but without it Poly/ML loops forever at compile time. *) @@ -144,12 +136,12 @@ fun ints_of_node (IntLeaf n) = cons n | ints_of_node (StrNode (_, us)) = fold ints_of_node us val parse_tstp_annotations = - Scan.optional ($$ "," |-- parse_term NONE - --| Scan.option ($$ "," |-- parse_terms NONE) + Scan.optional ($$ "," |-- parse_term Symtab.empty + --| Scan.option ($$ "," |-- parse_terms Symtab.empty) >> (fn source => ints_of_node source [])) [] fun parse_definition pool = - $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>" + $$ "(" |-- parse_literal pool --| Scan.this_string "<=>" -- parse_clause pool --| $$ ")" (* Syntax: cnf(, , ). diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Wed Jul 21 21:15:07 2010 +0200 @@ -10,13 +10,12 @@ type class_rel_clause = Metis_Clauses.class_rel_clause type arity_clause = Metis_Clauses.arity_clause type fol_clause = Metis_Clauses.fol_clause - type name_pool = string Symtab.table * string Symtab.table val write_tptp_file : theory -> bool -> bool -> bool -> Path.T -> fol_clause list * fol_clause list * fol_clause list * fol_clause list * class_rel_clause list * arity_clause list - -> name_pool option * int + -> string Symtab.table * int end; structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT = @@ -56,8 +55,6 @@ (** Nice names **) -type name_pool = string Symtab.table * string Symtab.table - fun empty_name_pool readable_names = if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE @@ -164,7 +161,7 @@ Cnf (hol_ident axiom_name clause_id, kind, atp_literals_for_axiom full_types clause) -fun problem_line_for_class_rel +fun problem_line_for_class_rel_clause (ClassRelClause {axiom_name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])), @@ -176,7 +173,8 @@ | atp_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) -fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) = +fun problem_line_for_arity_clause + (ArityClause {axiom_name, conclLit, premLits, ...}) = Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom, map atp_literal_for_arity_literal (conclLit :: premLits)) @@ -306,8 +304,9 @@ class_rel_clauses, arity_clauses) = let val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses - val class_rel_lines = map problem_line_for_class_rel class_rel_clauses - val arity_lines = map problem_line_for_arity arity_clauses + 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_clauses val conjecture_lines = map (problem_line_for_conjecture full_types) conjectures @@ -324,6 +323,9 @@ length axiom_lines + length class_rel_lines + length arity_lines + length helper_lines val _ = File.write_list file (strings_for_problem problem) - in (pool, conjecture_offset) end + in + (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty, + conjecture_offset) + end end; diff -r 1188e6bff48d -r e6ff246c0cdb src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Wed Jul 21 21:14:47 2010 +0200 +++ b/src/HOL/Tools/meson.ML Wed Jul 21 21:15:07 2010 +0200 @@ -584,8 +584,7 @@ fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls)); fun skolemize_prems_tac ctxt prems = - cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' - REPEAT o (etac exE); + cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE (*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions. Function mkcl converts theorems to clauses.*)