# HG changeset patch # User blanchet # Date 1268850365 -3600 # Node ID 1590abc3d42a6ea3fad5aa2f1d4c094e90a5dc8d # Parent a6aad5a70ed4c5a03e29a37e5c9481c0f2c84952 renamed Sledgehammer structures diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/ATP_Linkup.thy Wed Mar 17 19:26:05 2010 +0100 @@ -92,10 +92,10 @@ subsection {* Setup of external ATPs *} use "Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML" -setup Res_Axioms.setup +setup Sledgehammer_Fact_Preprocessor.setup use "Tools/Sledgehammer/sledgehammer_hol_clause.ML" use "Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML" -setup Res_Reconstruct.setup +setup Sledgehammer_Proof_Reconstruct.setup use "Tools/Sledgehammer/sledgehammer_fact_filter.ML" use "Tools/ATP_Manager/atp_wrapper.ML" @@ -125,6 +125,6 @@ subsection {* The Metis prover *} use "Tools/Sledgehammer/metis_tactics.ML" -setup MetisTools.setup +setup Metis_Tactics.setup end diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Mar 17 19:26:05 2010 +0100 @@ -263,7 +263,7 @@ val _ = register birth_time death_time (Thread.self (), desc); val problem = ATP_Wrapper.problem_of_goal (! full_types) i (ctxt, (facts, goal)); val message = #message (prover (! timeout) problem) - handle Res_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *) + handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (* FIXME !? *) "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis" | ERROR msg => ("Error: " ^ msg); val _ = unregister message (Thread.self ()); diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Mar 17 19:26:05 2010 +0100 @@ -116,7 +116,7 @@ let val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs - val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs + val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {with_full_types = ! ATP_Manager.full_types, @@ -170,7 +170,7 @@ (NONE, "Error in prover: " ^ msg) | (Failure, _) => (NONE, "Failure: No proof with the theorems supplied")) - handle Res_HOL_Clause.TOO_TRIVIAL => + handle Sledgehammer_HOL_Clause.TOO_TRIVIAL => (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis") | ERROR msg => (NONE, "Error: " ^ msg) end diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Mar 17 19:26:05 2010 +0100 @@ -52,6 +52,9 @@ structure ATP_Wrapper: ATP_WRAPPER = struct +structure SFF = Sledgehammer_Fact_Filter +structure SPR = Sledgehammer_Proof_Reconstruct + (** generic ATP wrapper **) (* external problem files *) @@ -117,8 +120,8 @@ (* get clauses and prepare them for writing *) val (ctxt, (chain_ths, th)) = goal; val thy = ProofContext.theory_of ctxt; - val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths; - val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoal); + val chain_ths = map (Thm.put_name_hint SPR.chained_hint) chain_ths; + val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal); val the_filtered_clauses = (case filtered_clauses of NONE => relevance_filter goal goal_cls @@ -181,7 +184,7 @@ with_path cleanup export run_on (prob_pathname subgoal); (* check for success and print out some information on failure *) - val failure = Res_Reconstruct.find_failure proof; + val failure = SPR.find_failure proof; val success = rc = 0 andalso is_none failure; val (message, real_thm_names) = if is_some failure then ("External prover failed.", []) @@ -203,13 +206,13 @@ prover_config; in external_prover - (Res_ATP.get_relevant max_new_clauses insert_theory_const) - (Res_ATP.prepare_clauses false) - Res_HOL_Clause.tptp_write_file + (SFF.get_relevant max_new_clauses insert_theory_const) + (SFF.prepare_clauses false) + Sledgehammer_HOL_Clause.tptp_write_file command (arguments timeout) - (if emit_structured_proof then Res_Reconstruct.structured_proof - else Res_Reconstruct.lemma_list false) + (if emit_structured_proof then SPR.structured_proof + else SPR.lemma_list false) name problem end; @@ -274,12 +277,12 @@ val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config; in external_prover - (Res_ATP.get_relevant max_new_clauses insert_theory_const) - (Res_ATP.prepare_clauses true) - Res_HOL_Clause.dfg_write_file + (SFF.get_relevant max_new_clauses insert_theory_const) + (SFF.prepare_clauses true) + Sledgehammer_HOL_Clause.dfg_write_file command (arguments timeout) - (Res_Reconstruct.lemma_list true) + (SPR.lemma_list true) name problem end; @@ -298,7 +301,7 @@ let val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w") in - if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer) + if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) else split_lines answer end; @@ -310,7 +313,7 @@ fun the_system prefix = (case get_system prefix of - NONE => error ("No system like " ^ quote prefix ^ " at SystemOnTPTP") + NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") | SOME sys => sys); fun remote_prover_config prover_prefix args max_new insert_tc: prover_config = diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/metis_tactics.ML --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,11 +1,11 @@ -(* Title: HOL/Tools/metis_tools.ML +(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory Copyright Cambridge University 2007 HOL setup for the Metis prover. *) -signature METIS_TOOLS = +signature METIS_TACTICS = sig val trace: bool Unsynchronized.ref val type_lits: bool Config.T @@ -15,15 +15,19 @@ val setup: theory -> theory end -structure MetisTools: METIS_TOOLS = +structure Metis_Tactics : METIS_TACTICS = struct +structure SFC = Sledgehammer_FOL_Clause +structure SHC = Sledgehammer_HOL_Clause +structure SPR = Sledgehammer_Proof_Reconstruct + val trace = Unsynchronized.ref false; -fun trace_msg msg = if ! trace then tracing (msg ()) else (); +fun trace_msg msg = if !trace then tracing (msg ()) else (); val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; -datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*) +datatype mode = FO | HO | FT (* first-order, higher-order, fully-typed *) (* ------------------------------------------------------------------------- *) (* Useful Theorems *) @@ -63,62 +67,62 @@ fun metis_lit b c args = (b, (c, args)); -fun hol_type_to_fol (Res_Clause.AtomV x) = Metis.Term.Var x - | hol_type_to_fol (Res_Clause.AtomF x) = Metis.Term.Fn(x,[]) - | hol_type_to_fol (Res_Clause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); +fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x + | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[]) + | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); (*These two functions insert type literals before the real literals. That is the opposite order from TPTP linkup, but maybe OK.*) fun hol_term_to_fol_FO tm = - case Res_HOL_Clause.strip_comb tm of - (Res_HOL_Clause.CombConst(c,_,tys), tms) => + case SHC.strip_comb tm of + (SHC.CombConst(c,_,tys), tms) => let val tyargs = map hol_type_to_fol tys val args = map hol_term_to_fol_FO tms in Metis.Term.Fn (c, tyargs @ args) end - | (Res_HOL_Clause.CombVar(v,_), []) => Metis.Term.Var v + | (SHC.CombVar(v,_), []) => Metis.Term.Var v | _ => error "hol_term_to_fol_FO"; -fun hol_term_to_fol_HO (Res_HOL_Clause.CombVar (a, _)) = Metis.Term.Var a - | hol_term_to_fol_HO (Res_HOL_Clause.CombConst (a, _, tylist)) = +fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a + | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) = Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) - | hol_term_to_fol_HO (Res_HOL_Clause.CombApp (tm1, tm2)) = + | hol_term_to_fol_HO (SHC.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 hol_term_to_fol_FT (Res_HOL_Clause.CombVar(a, ty)) = +fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty) - | hol_term_to_fol_FT (Res_HOL_Clause.CombConst(a, ty, _)) = + | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) = wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) - | hol_term_to_fol_FT (tm as Res_HOL_Clause.CombApp(tm1,tm2)) = + | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) = wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), - Res_HOL_Clause.type_of_combterm tm); + SHC.type_of_combterm tm); -fun hol_literal_to_fol FO (Res_HOL_Clause.Literal (pol, tm)) = - let val (Res_HOL_Clause.CombConst(p,_,tys), tms) = Res_HOL_Clause.strip_comb tm +fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) = + let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm val tylits = if p = "equal" then [] else map hol_type_to_fol tys val lits = map hol_term_to_fol_FO tms in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end - | hol_literal_to_fol HO (Res_HOL_Clause.Literal (pol, tm)) = - (case Res_HOL_Clause.strip_comb tm of - (Res_HOL_Clause.CombConst("equal",_,_), tms) => + | hol_literal_to_fol HO (SHC.Literal (pol, tm)) = + (case SHC.strip_comb tm of + (SHC.CombConst("equal",_,_), tms) => metis_lit pol "=" (map hol_term_to_fol_HO tms) | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) - | hol_literal_to_fol FT (Res_HOL_Clause.Literal (pol, tm)) = - (case Res_HOL_Clause.strip_comb tm of - (Res_HOL_Clause.CombConst("equal",_,_), tms) => + | hol_literal_to_fol FT (SHC.Literal (pol, tm)) = + (case SHC.strip_comb tm of + (SHC.CombConst("equal",_,_), tms) => metis_lit pol "=" (map hol_term_to_fol_FT tms) | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); fun literals_of_hol_thm thy mode t = - let val (lits, types_sorts) = Res_HOL_Clause.literals_of_term thy t + let val (lits, types_sorts) = SHC.literals_of_term thy t in (map (hol_literal_to_fol mode) lits, types_sorts) end; (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) -fun metis_of_typeLit pos (Res_Clause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] - | metis_of_typeLit pos (Res_Clause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; +fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] + | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; fun default_sort _ (TVar _) = false | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1))); @@ -132,9 +136,9 @@ (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th in if is_conjecture then - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), Res_Clause.add_typs types_sorts) + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts) else - let val tylits = Res_Clause.add_typs + let val tylits = SFC.add_typs (filter (not o default_sort ctxt) types_sorts) val mtylits = if Config.get ctxt type_lits then map (metis_of_typeLit false) tylits else [] @@ -145,13 +149,13 @@ (* ARITY CLAUSE *) -fun m_arity_cls (Res_Clause.TConsLit (c,t,args)) = - metis_lit true (Res_Clause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] - | m_arity_cls (Res_Clause.TVarLit (c,str)) = - metis_lit false (Res_Clause.make_type_class c) [Metis.Term.Var str]; +fun m_arity_cls (SFC.TConsLit (c,t,args)) = + metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] + | m_arity_cls (SFC.TVarLit (c,str)) = + metis_lit false (SFC.make_type_class c) [Metis.Term.Var str]; (*TrueI is returned as the Isabelle counterpart because there isn't any.*) -fun arity_cls (Res_Clause.ArityClause{conclLit,premLits,...}) = +fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) = (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits)))); @@ -160,7 +164,7 @@ fun m_classrel_cls subclass superclass = [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]]; -fun classrel_cls (Res_Clause.ClassrelClause {subclass, superclass, ...}) = +fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) = (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); (* ------------------------------------------------------------------------- *) @@ -209,14 +213,14 @@ | strip_happ args x = (x, args); fun fol_type_to_isa _ (Metis.Term.Var v) = - (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of - SOME w => Res_Reconstruct.make_tvar w - | NONE => Res_Reconstruct.make_tvar v) + (case SPR.strip_prefix SFC.tvar_prefix v of + SOME w => SPR.make_tvar w + | NONE => SPR.make_tvar v) | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = - (case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix x of - SOME tc => Term.Type (Res_Reconstruct.invert_type_const tc, map (fol_type_to_isa ctxt) tys) + (case SPR.strip_prefix SFC.tconst_prefix x of + SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys) | NONE => - case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix x of + case SPR.strip_prefix SFC.tfree_prefix x of SOME tf => mk_tfree ctxt tf | NONE => error ("fol_type_to_isa: " ^ x)); @@ -225,10 +229,10 @@ let val thy = ProofContext.theory_of ctxt val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) fun tm_to_tt (Metis.Term.Var v) = - (case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix v of - SOME w => Type (Res_Reconstruct.make_tvar w) + (case SPR.strip_prefix SFC.tvar_prefix v of + SOME w => Type (SPR.make_tvar w) | NONE => - case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of + case SPR.strip_prefix SFC.schematic_var_prefix v of SOME w => Term (mk_var (w, HOLogic.typeT)) | NONE => Term (mk_var (v, HOLogic.typeT)) ) (*Var from Metis with a name like _nnn; possibly a type variable*) @@ -245,14 +249,14 @@ and applic_to_tt ("=",ts) = Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) | applic_to_tt (a,ts) = - case Res_Reconstruct.strip_prefix Res_Clause.const_prefix a of + case SPR.strip_prefix SFC.const_prefix a of SOME b => - let val c = Res_Reconstruct.invert_const b - val ntypes = Res_Reconstruct.num_typargs thy c + let val c = SPR.invert_const b + val ntypes = SPR.num_typargs thy c val nterms = length ts - ntypes val tts = map tm_to_tt ts val tys = types_of (List.take(tts,ntypes)) - val ntyargs = Res_Reconstruct.num_typargs thy c + val ntyargs = SPR.num_typargs thy c in if length tys = ntyargs then apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ @@ -263,14 +267,14 @@ cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) end | NONE => (*Not a constant. Is it a type constructor?*) - case Res_Reconstruct.strip_prefix Res_Clause.tconst_prefix a of + case SPR.strip_prefix SFC.tconst_prefix a of SOME b => - Type (Term.Type (Res_Reconstruct.invert_type_const b, types_of (map tm_to_tt ts))) + Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts))) | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case Res_Reconstruct.strip_prefix Res_Clause.tfree_prefix a of + case SPR.strip_prefix SFC.tfree_prefix a of SOME b => Type (mk_tfree ctxt b) | NONE => (*a fixed variable? They are Skolem functions.*) - case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix a of + case SPR.strip_prefix SFC.fixed_var_prefix a of SOME b => let val opr = Term.Free(b, HOLogic.typeT) in apply_list opr (length ts) (map tm_to_tt ts) end @@ -281,16 +285,16 @@ fun fol_term_to_hol_FT ctxt fol_tm = let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = - (case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix v of + (case SPR.strip_prefix SFC.schematic_var_prefix v of SOME w => mk_var(w, dummyT) | NONE => mk_var(v, dummyT)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = Const ("op =", HOLogic.typeT) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = - (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of - SOME c => Const (Res_Reconstruct.invert_const c, dummyT) + (case SPR.strip_prefix SFC.const_prefix x of + SOME c => Const (SPR.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of + case SPR.strip_prefix SFC.fixed_var_prefix x of SOME v => Free (v, fol_type_to_isa ctxt ty) | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = @@ -301,10 +305,10 @@ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) = list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) | cvt (t as Metis.Term.Fn (x, [])) = - (case Res_Reconstruct.strip_prefix Res_Clause.const_prefix x of - SOME c => Const (Res_Reconstruct.invert_const c, dummyT) + (case SPR.strip_prefix SFC.const_prefix x of + SOME c => Const (SPR.invert_const c, dummyT) | NONE => (*Not a constant. Is it a fixed variable??*) - case Res_Reconstruct.strip_prefix Res_Clause.fixed_var_prefix x of + case SPR.strip_prefix SFC.fixed_var_prefix x of SOME v => Free (v, dummyT) | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) @@ -383,9 +387,9 @@ " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = - case Res_Reconstruct.strip_prefix Res_Clause.schematic_var_prefix a of + case SPR.strip_prefix SFC.schematic_var_prefix a of SOME b => SOME (b, t) - | NONE => case Res_Reconstruct.strip_prefix Res_Clause.tvar_prefix a of + | NONE => case SPR.strip_prefix SFC.tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) @@ -452,7 +456,7 @@ in cterm_instantiate [(refl_x, c_t)] REFL_THM end; fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (Res_Reconstruct.num_typargs thy c handle TYPE _ => 0) + | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0) | get_ty_arg_size _ _ = 0; (* INFERENCE RULE: EQUALITY *) @@ -538,7 +542,7 @@ | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = equality_inf ctxt mode f_lit f_p f_r; -fun real_literal (_, (c, _)) = not (String.isPrefix Res_Clause.class_prefix c); +fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c); fun translate _ _ thpairs [] = thpairs | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = @@ -564,23 +568,23 @@ (* Translation of HO Clauses *) (* ------------------------------------------------------------------------- *) -fun cnf_th thy th = hd (Res_Axioms.cnf_axiom thy th); +fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th); val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal}; -val comb_I = cnf_th @{theory} Res_HOL_Clause.comb_I; -val comb_K = cnf_th @{theory} Res_HOL_Clause.comb_K; -val comb_B = cnf_th @{theory} Res_HOL_Clause.comb_B; -val comb_C = cnf_th @{theory} Res_HOL_Clause.comb_C; -val comb_S = cnf_th @{theory} Res_HOL_Clause.comb_S; +val comb_I = cnf_th @{theory} SHC.comb_I; +val comb_K = cnf_th @{theory} SHC.comb_K; +val comb_B = cnf_th @{theory} SHC.comb_B; +val comb_C = cnf_th @{theory} SHC.comb_C; +val comb_S = cnf_th @{theory} SHC.comb_S; fun type_ext thy tms = - let val subs = Res_ATP.tfree_classes_of_terms tms - val supers = Res_ATP.tvar_classes_of_terms tms - and tycons = Res_ATP.type_consts_of_terms thy tms - val (supers', arity_clauses) = Res_Clause.make_arity_clauses thy tycons supers - val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers' + let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms + val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms + and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms + val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers + val classrel_clauses = SFC.make_classrel_clauses thy subs supers' in map classrel_cls classrel_clauses @ map arity_cls arity_clauses end; @@ -590,7 +594,7 @@ type logic_map = {axioms : (Metis.Thm.thm * thm) list, - tfrees : Res_Clause.type_literal list}; + tfrees : SFC.type_literal list}; fun const_in_metis c (pred, tm_list) = let @@ -602,7 +606,7 @@ (*Extract TFree constraints from context to include as conjecture clauses*) fun init_tfrees ctxt = let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts - in Res_Clause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; + in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; (*transform isabelle type / arity clause to metis clause *) fun add_type_thm [] lmap = lmap @@ -663,7 +667,8 @@ (* Main function to start metis prove and reconstruction *) 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, Res_Axioms.cnf_axiom thy th)) ths0 + val th_cls_pairs = + map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy 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 @@ -672,7 +677,7 @@ val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths val _ = if null tfrees then () else (trace_msg (fn () => "TFREE CLAUSES"); - app (fn tf => trace_msg (fn _ => Res_Clause.tptp_of_typeLit true tf)) tfrees) + app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees) val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms @@ -714,12 +719,12 @@ let val _ = trace_msg (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in - if exists_type Res_Axioms.type_has_topsort (prop_of st0) + if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0) then raise METIS "Metis: Proof state contains the universal sort {}" else - (Meson.MESON Res_Axioms.neg_clausify + (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i - THEN Res_Axioms.expand_defs_tac st0) st0 + THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0 end handle METIS s => (warning ("Metis: " ^ s); Seq.empty); @@ -736,7 +741,7 @@ method @{binding metisF} FO "METIS for FOL problems" #> method @{binding metisFT} FT "METIS with fully-typed translation" #> Method.setup @{binding finish_clausify} - (Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl)))) + (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl)))) "cleanup after conversion to clauses"; end; diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,9 +1,14 @@ -(* Title: HOL/Tools/res_atp.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *) -signature RES_ATP = +signature SLEDGEHAMMER_FACT_FILTER = sig + type classrelClause = Sledgehammer_FOL_Clause.classrelClause + type arityClause = Sledgehammer_FOL_Clause.arityClause + type axiom_name = Sledgehammer_HOL_Clause.axiom_name + type clause = Sledgehammer_HOL_Clause.clause + type clause_id = Sledgehammer_HOL_Clause.clause_id datatype mode = Auto | Fol | Hol val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list @@ -11,16 +16,25 @@ val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : bool -> thm list -> thm list -> - (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> - (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory -> - Res_HOL_Clause.axiom_name vector * - (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * - Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list) + (thm * (axiom_name * clause_id)) list -> + (thm * (axiom_name * clause_id)) list -> theory -> + axiom_name vector * + (clause list * clause list * clause list * + clause list * classrelClause list * arityClause list) end; -structure Res_ATP: RES_ATP = +structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER = struct +structure SFC = Sledgehammer_FOL_Clause +structure SFP = Sledgehammer_Fact_Preprocessor +structure SHC = Sledgehammer_HOL_Clause + +type classrelClause = SFC.classrelClause +type arityClause = SFC.arityClause +type axiom_name = SHC.axiom_name +type clause = SHC.clause +type clause_id = SHC.clause_id (********************************************************************) (* some settings for both background automatic ATP calling procedure*) @@ -238,10 +252,10 @@ let val cls = sort compare_pairs newpairs val accepted = List.take (cls, max_new) in - Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ + SFP.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ ", exceeds the limit of " ^ Int.toString (max_new))); - Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); - Res_Axioms.trace_msg (fn () => "Actually passed: " ^ + SFP.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted)))); + SFP.trace_msg (fn () => "Actually passed: " ^ space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted)); (map #1 accepted, map #1 (List.drop (cls, max_new))) @@ -256,7 +270,7 @@ val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts val newp = p + (1.0-p) / convergence in - Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); + SFP.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); (map #1 newrels) @ (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects)) end @@ -264,12 +278,12 @@ let val weight = clause_weight ctab rel_consts consts_typs in if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) - then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ + then (SFP.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ " passes: " ^ Real.toString weight)); relevant ((ax,weight)::newrels, rejects) axs) else relevant (newrels, ax::rejects) axs end - in Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); + in SFP.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); relevant ([],[]) end; @@ -278,12 +292,12 @@ then let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms val goal_const_tab = get_goal_consts_typs thy goals - val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^ + val _ = SFP.trace_msg (fn () => ("Initial constants: " ^ space_implode ", " (Symtab.keys goal_const_tab))); val rels = relevant_clauses max_new thy const_tab (pass_mark) goal_const_tab (map (pair_consts_typs_axiom theory_const thy) axioms) in - Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels))); + SFP.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels))); rels end else axioms; @@ -337,7 +351,7 @@ fun make_unique xs = let val ht = mk_clause_table 7000 in - Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); + SFP.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses")); app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht end; @@ -369,7 +383,7 @@ val name1 = Facts.extern facts name; val name2 = Name_Space.extern full_space name; - val ths = filter_out Res_Axioms.bad_for_atp ths0; + val ths = filter_out SFP.bad_for_atp ths0; in if Facts.is_concealed facts name orelse null ths orelse run_blacklist_filter andalso is_package_def name then I @@ -389,7 +403,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names (a, ths) pairs = - if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs + if (Long_Name.base_name a) mem_string SFP.multi_base_blacklist then pairs else add_single_names (a, ths) pairs; fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; @@ -411,7 +425,7 @@ fun get_all_lemmas ctxt = let val included_thms = - tap (fn ths => Res_Axioms.trace_msg + tap (fn ths => SFP.trace_msg (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems"))) (name_thm_pairs ctxt) in @@ -519,7 +533,7 @@ val thy = ProofContext.theory_of ctxt val isFO = isFO thy goal_cls val included_cls = get_all_lemmas ctxt - |> Res_Axioms.cnf_rules_pairs thy |> make_unique + |> SFP.cnf_rules_pairs thy |> make_unique |> restrict_to_logic thy isFO |> remove_unwanted_clauses in @@ -532,24 +546,24 @@ let (* add chain thms *) val chain_cls = - Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths)) + SFP.cnf_rules_pairs thy (filter check_named (map SFP.pairname chain_ths)) val axcls = chain_cls @ axcls val extra_cls = chain_cls @ extra_cls val isFO = isFO thy goal_cls val ccls = subtract_cls goal_cls extra_cls - val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls + val _ = app (fn th => SFP.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls val ccltms = map prop_of ccls and axtms = map (prop_of o #1) extra_cls val subs = tfree_classes_of_terms ccltms and supers = tvar_classes_of_terms axtms and tycons = type_consts_of_terms thy (ccltms@axtms) (*TFrees in conjecture clauses; TVars in axiom clauses*) - val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls - val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls) - val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls) - val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, []) - val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers - val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers' + val conjectures = SHC.make_conjecture_clauses dfg thy ccls + val (_, extra_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy extra_cls) + val (clnames,axiom_clauses) = ListPair.unzip (SHC.make_axiom_clauses dfg thy axcls) + val helper_clauses = SHC.get_helper_clauses dfg thy isFO (conjectures, extra_cls, []) + val (supers',arity_clauses) = SFC.make_arity_clauses_dfg dfg thy tycons supers + val classrel_clauses = SFC.make_classrel_clauses thy subs supers' in (Vector.fromList clnames, (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/Tools/res_axioms.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Author: Jia Meng, Cambridge University Computer Laboratory Transformation of axiom rules (elim/intro/etc) into CNF forms. *) -signature RES_AXIOMS = +signature SLEDGEHAMMER_FACT_PREPROCESSOR = sig val trace: bool Unsynchronized.ref val trace_msg: (unit -> string) -> unit @@ -23,7 +23,7 @@ val setup: theory -> theory end; -structure Res_Axioms: RES_AXIOMS = +structure Sledgehammer_Fact_Preprocessor : SLEDGEHAMMER_FACT_PREPROCESSOR = struct val trace = Unsynchronized.ref false; @@ -285,7 +285,7 @@ map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th); -(*** Blacklisting (duplicated in Res_ATP?) ***) +(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***) val max_lambda_nesting = 3; @@ -385,14 +385,16 @@ fun cnf_rules_pairs_aux _ pairs [] = pairs | cnf_rules_pairs_aux thy pairs ((name,th)::ths) = let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs - handle THM _ => pairs | Res_Clause.CLAUSE _ => pairs + handle THM _ => pairs | + Sledgehammer_FOL_Clause.CLAUSE _ => pairs in cnf_rules_pairs_aux thy pairs' ths end; (*The combination of rev and tail recursion preserves the original order*) fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l); -(**** Convert all facts of the theory into clauses (Res_Clause.clause, or Res_HOL_Clause.clause) ****) +(**** Convert all facts of the theory into clauses + (Sledgehammer_FOL_Clause.clause, or Sledgehammer_HOL_Clause.clause) ****) local diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Tools/res_clause.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Author: Jia Meng, Cambridge University Computer Laboratory Storing/printing FOL clauses and arity clauses. Typed equality is @@ -7,7 +7,7 @@ FIXME: combine with res_hol_clause! *) -signature RES_CLAUSE = +signature SLEDGEHAMMER_FOL_CLAUSE = sig val schematic_var_prefix: string val fixed_var_prefix: string @@ -77,7 +77,7 @@ val tptp_classrelClause : classrelClause -> string end -structure Res_Clause: RES_CLAUSE = +structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE = struct val schematic_var_prefix = "V_"; diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/Tools/res_hol_clause.ML +(* Title: HOL/Sledgehammer/sledgehammer_hol_clause.ML Author: Jia Meng, NICTA FOL clauses translated from HOL formulae. *) -signature RES_HOL_CLAUSE = +signature SLEDGEHAMMER_HOL_CLAUSE = sig val ext: thm val comb_I: thm @@ -17,13 +17,13 @@ type polarity = bool type clause_id = int datatype combterm = - CombConst of string * Res_Clause.fol_type * Res_Clause.fol_type list (*Const and Free*) - | CombVar of string * Res_Clause.fol_type + CombConst of string * Sledgehammer_FOL_Clause.fol_type * Sledgehammer_FOL_Clause.fol_type list (*Const and Free*) + | CombVar of string * Sledgehammer_FOL_Clause.fol_type | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, - kind: Res_Clause.kind,literals: literal list, ctypes_sorts: typ list} - val type_of_combterm: combterm -> Res_Clause.fol_type + kind: Sledgehammer_FOL_Clause.kind,literals: literal list, ctypes_sorts: typ list} + val type_of_combterm: combterm -> Sledgehammer_FOL_Clause.fol_type val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL @@ -38,18 +38,18 @@ clause list val tptp_write_file: bool -> Path.T -> clause list * clause list * clause list * clause list * - Res_Clause.classrelClause list * Res_Clause.arityClause list -> + Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> int * int val dfg_write_file: bool -> Path.T -> clause list * clause list * clause list * clause list * - Res_Clause.classrelClause list * Res_Clause.arityClause list -> + Sledgehammer_FOL_Clause.classrelClause list * Sledgehammer_FOL_Clause.arityClause list -> int * int end -structure Res_HOL_Clause: RES_HOL_CLAUSE = +structure Sledgehammer_HOL_Clause : SLEDGEHAMMER_HOL_CLAUSE = struct -structure RC = Res_Clause; (* FIXME avoid structure alias *) +structure SFC = Sledgehammer_FOL_Clause; (* theorems for combinators and function extensionality *) val ext = thm "HOL.ext"; @@ -86,8 +86,8 @@ type polarity = bool; type clause_id = int; -datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*) - | CombVar of string * RC.fol_type +datatype combterm = CombConst of string * SFC.fol_type * SFC.fol_type list (*Const and Free*) + | CombVar of string * SFC.fol_type | CombApp of combterm * combterm datatype literal = Literal of polarity * combterm; @@ -96,7 +96,7 @@ Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, - kind: RC.kind, + kind: SFC.kind, literals: literal list, ctypes_sorts: typ list}; @@ -119,20 +119,20 @@ fun type_of dfg (Type (a, Ts)) = let val (folTypes,ts) = types_of dfg Ts - in (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts) end + in (SFC.Comp(SFC.make_fixed_type_const dfg a, folTypes), ts) end | type_of _ (tp as TFree (a, _)) = - (RC.AtomF (RC.make_fixed_type_var a), [tp]) + (SFC.AtomF (SFC.make_fixed_type_var a), [tp]) | type_of _ (tp as TVar (v, _)) = - (RC.AtomV (RC.make_schematic_type_var v), [tp]) + (SFC.AtomV (SFC.make_schematic_type_var v), [tp]) and types_of dfg Ts = let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts) - in (folTyps, RC.union_all ts) end; + in (folTyps, SFC.union_all ts) end; (* same as above, but no gathering of sort information *) fun simp_type_of dfg (Type (a, Ts)) = - RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) - | simp_type_of _ (TFree (a, _)) = RC.AtomF(RC.make_fixed_type_var a) - | simp_type_of _ (TVar (v, _)) = RC.AtomV(RC.make_schematic_type_var v); + SFC.Comp(SFC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts) + | simp_type_of _ (TFree (a, _)) = SFC.AtomF(SFC.make_fixed_type_var a) + | simp_type_of _ (TVar (v, _)) = SFC.AtomV(SFC.make_schematic_type_var v); fun const_type_of dfg thy (c,t) = @@ -142,21 +142,21 @@ (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *) fun combterm_of dfg thy (Const(c,t)) = let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t) - val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list) + val c' = CombConst(SFC.make_fixed_const dfg c, tp, tvar_list) in (c',ts) end | combterm_of dfg _ (Free(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombConst(RC.make_fixed_var v, tp, []) + val v' = CombConst(SFC.make_fixed_var v, tp, []) in (v',ts) end | combterm_of dfg _ (Var(v,t)) = let val (tp,ts) = type_of dfg t - val v' = CombVar(RC.make_schematic_var v,tp) + val v' = CombVar(SFC.make_schematic_var v,tp) in (v',ts) end | combterm_of dfg thy (P $ Q) = let val (P',tsP) = combterm_of dfg thy P val (Q',tsQ) = combterm_of dfg thy Q in (CombApp(P',Q'), union (op =) tsP tsQ) end - | combterm_of _ _ (t as Abs _) = raise RC.CLAUSE ("HOL CLAUSE", t); + | combterm_of _ _ (t as Abs _) = raise SFC.CLAUSE ("HOL CLAUSE", t); fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity) | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity); @@ -189,7 +189,7 @@ fun add_axiom_clause dfg thy ((th,(name,id)), pairs) = - let val cls = make_clause dfg thy (id, name, RC.Axiom, th) + let val cls = make_clause dfg thy (id, name, SFC.Axiom, th) in if isTaut cls then pairs else (name,cls)::pairs end; @@ -198,7 +198,7 @@ fun make_conjecture_clauses_aux _ _ _ [] = [] | make_conjecture_clauses_aux dfg thy n (th::ths) = - make_clause dfg thy (n,"conjecture", RC.Conjecture, th) :: + make_clause dfg thy (n,"conjecture", SFC.Conjecture, th) :: make_conjecture_clauses_aux dfg thy (n+1) ths; fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0; @@ -211,7 +211,7 @@ (**********************************************************************) (*Result of a function type; no need to check that the argument type matches.*) -fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 +fun result_type (SFC.Comp ("tc_fun", [_, tp2])) = tp2 | result_type _ = error "result_type" fun type_of_combterm (CombConst (_, tp, _)) = tp @@ -231,10 +231,10 @@ fun wrap_type t_full (s, tp) = if t_full then - type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp] + type_wrapper ^ SFC.paren_pack [s, SFC.string_of_fol_type tp] else s; -fun apply ss = "hAPP" ^ RC.paren_pack ss; +fun apply ss = "hAPP" ^ SFC.paren_pack ss; fun rev_apply (v, []) = v | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; @@ -251,10 +251,10 @@ Int.toString nargs ^ " but is applied to " ^ space_implode ", " args) val args2 = List.drop(args, nargs) - val targs = if not t_full then map RC.string_of_fol_type tvars + val targs = if not t_full then map SFC.string_of_fol_type tvars else [] in - string_apply (c ^ RC.paren_pack (args1@targs), args2) + string_apply (c ^ SFC.paren_pack (args1@targs), args2) end | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args) | string_of_applic _ _ _ = error "string_of_applic"; @@ -271,13 +271,13 @@ (*Boolean-valued terms are here converted to literals.*) fun boolify params t = - "hBOOL" ^ RC.paren_pack [string_of_combterm params t]; + "hBOOL" ^ SFC.paren_pack [string_of_combterm params t]; fun string_of_predicate (params as (_,_,cnh)) t = case t of (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) => (*DFG only: new TPTP prefers infix equality*) - ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2]) + ("equal" ^ SFC.paren_pack [string_of_combterm params t1, string_of_combterm params t2]) | _ => case #1 (strip_comb t) of CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t @@ -293,28 +293,28 @@ fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = tptp_of_equality params pol (t1,t2) | tptp_literal params (Literal(pol,pred)) = - RC.tptp_sign pol (string_of_predicate params pred); + SFC.tptp_sign pol (string_of_predicate params pred); (*Given a clause, returns its literals paired with a list of literals concerning TFrees; the latter should only occur in conjecture clauses.*) fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = (map (tptp_literal params) literals, - map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts)); + map (SFC.tptp_of_typeLit pos) (SFC.add_typs ctypes_sorts)); fun clause2tptp params (cls as Clause {axiom_name, clause_id, kind, ...}) = - let val (lits,tylits) = tptp_type_lits params (kind = RC.Conjecture) cls + let val (lits,tylits) = tptp_type_lits params (kind = SFC.Conjecture) cls in - (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) + (SFC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits) end; (*** dfg format ***) -fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred); +fun dfg_literal params (Literal(pol,pred)) = SFC.dfg_sign pol (string_of_predicate params pred); fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) = (map (dfg_literal params) literals, - map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts)); + map (SFC.dfg_of_typeLit pos) (SFC.add_typs ctypes_sorts)); fun get_uvars (CombConst _) vars = vars | get_uvars (CombVar(v,_)) vars = (v::vars) @@ -322,20 +322,20 @@ fun get_uvars_l (Literal(_,c)) = get_uvars c []; -fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals); +fun dfg_vars (Clause {literals,...}) = SFC.union_all (map get_uvars_l literals); fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) = - let val (lits,tylits) = dfg_type_lits params (kind = RC.Conjecture) cls + let val (lits,tylits) = dfg_type_lits params (kind = SFC.Conjecture) cls val vars = dfg_vars cls - val tvars = RC.get_tvar_strs ctypes_sorts + val tvars = SFC.get_tvar_strs ctypes_sorts in - (RC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) + (SFC.gen_dfg_cls(clause_id, axiom_name, kind, lits, tylits, tvars@vars), tylits) end; (** For DFG format: accumulate function and predicate declarations **) -fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars; +fun addtypes tvars tab = List.foldl SFC.add_foltype_funcs tab tvars; fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) = if c = "equal" then (addtypes tvars funcs, preds) @@ -348,7 +348,7 @@ else (addtypes tvars funcs, addit preds) end | add_decls _ (CombVar(_,ctp), (funcs,preds)) = - (RC.add_foltype_funcs (ctp,funcs), preds) + (SFC.add_foltype_funcs (ctp,funcs), preds) | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls)); fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls); @@ -358,23 +358,23 @@ handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities") fun decls_of_clauses params clauses arity_clauses = - let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab) + let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) SFC.init_functab) val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses) in - (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses), + (Symtab.dest (List.foldl SFC.add_arityClause_funcs functab arity_clauses), Symtab.dest predtab) end; fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) = - List.foldl RC.add_type_sort_preds preds ctypes_sorts + List.foldl SFC.add_type_sort_preds preds ctypes_sorts handle Symtab.DUP a => error ("predicate " ^ a ^ " has multiple arities") (*Higher-order clauses have only the predicates hBOOL and type classes.*) fun preds_of_clauses clauses clsrel_clauses arity_clauses = Symtab.dest - (List.foldl RC.add_classrelClause_preds - (List.foldl RC.add_arityClause_preds + (List.foldl SFC.add_classrelClause_preds + (List.foldl SFC.add_arityClause_preds (List.foldl add_clause_preds Symtab.empty clauses) arity_clauses) clsrel_clauses) @@ -404,7 +404,8 @@ else ct; fun cnf_helper_thms thy = - Res_Axioms.cnf_rules_pairs thy o map Res_Axioms.pairname + Sledgehammer_Fact_Preprocessor.cnf_rules_pairs thy + o map Sledgehammer_Fact_Preprocessor.pairname fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) = if isFO then [] (*first-order*) @@ -454,7 +455,8 @@ fold count_constants_lit literals (const_min_arity, const_needs_hBOOL); fun display_arity const_needs_hBOOL (c,n) = - Res_Axioms.trace_msg (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ + Sledgehammer_Fact_Preprocessor.trace_msg (fn () => "Constant: " ^ c ^ + " arity:\t" ^ Int.toString n ^ (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else "")); fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) = @@ -476,14 +478,14 @@ val (cma, cnh) = count_constants clauses val params = (t_full, cma, cnh) val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures) - val tfree_clss = map RC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) + val tfree_clss = map SFC.tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss) val _ = File.write_list file ( map (#1 o (clause2tptp params)) axclauses @ tfree_clss @ tptp_clss @ - map RC.tptp_classrelClause classrel_clauses @ - map RC.tptp_arity_clause arity_clauses @ + map SFC.tptp_classrelClause classrel_clauses @ + map SFC.tptp_arity_clause arity_clauses @ map (#1 o (clause2tptp params)) helper_clauses) in (length axclauses + 1, length tfree_clss + length tptp_clss) end; @@ -500,20 +502,20 @@ val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures) and probname = Path.implode (Path.base file) val axstrs = map (#1 o (clause2dfg params)) axclauses - val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss) + val tfree_clss = map SFC.dfg_tfree_clause (SFC.union_all tfree_litss) val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses val _ = File.write_list file ( - RC.string_of_start probname :: - RC.string_of_descrip probname :: - RC.string_of_symbols (RC.string_of_funcs funcs) - (RC.string_of_preds (cl_preds @ ty_preds)) :: + SFC.string_of_start probname :: + SFC.string_of_descrip probname :: + SFC.string_of_symbols (SFC.string_of_funcs funcs) + (SFC.string_of_preds (cl_preds @ ty_preds)) :: "list_of_clauses(axioms,cnf).\n" :: axstrs @ - map RC.dfg_classrelClause classrel_clauses @ - map RC.dfg_arity_clause arity_clauses @ + map SFC.dfg_classrelClause classrel_clauses @ + map SFC.dfg_arity_clause arity_clauses @ helper_clauses_strs @ ["end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n"] @ tfree_clss @ diff -r a6aad5a70ed4 -r 1590abc3d42a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 17 18:16:31 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 17 19:26:05 2010 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/Tools/res_reconstruct.ML +(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory Transfer of proofs from external provers. *) -signature RES_RECONSTRUCT = +signature SLEDGEHAMMER_PROOF_RECONSTRUCT = sig val chained_hint: string @@ -24,13 +24,15 @@ string * string vector * (int * int) * Proof.context * thm * int -> string * string list end; -structure Res_Reconstruct : RES_RECONSTRUCT = +structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = struct +structure SFC = Sledgehammer_FOL_Clause + val trace_path = Path.basic "atp_trace"; fun trace s = - if ! Res_Axioms.trace then File.append (File.tmp_path trace_path) s + if ! Sledgehammer_Fact_Preprocessor.trace then File.append (File.tmp_path trace_path) s else (); fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); @@ -107,12 +109,12 @@ (*If string s has the prefix s1, return the result of deleting it.*) fun strip_prefix s1 s = if String.isPrefix s1 s - then SOME (Res_Clause.undo_ascii_of (String.extract (s, size s1, NONE))) + then SOME (SFC.undo_ascii_of (String.extract (s, size s1, NONE))) else NONE; (*Invert the table of translations between Isabelle and ATPs*) val type_const_trans_table_inv = - Symtab.make (map swap (Symtab.dest Res_Clause.type_const_trans_table)); + Symtab.make (map swap (Symtab.dest SFC.type_const_trans_table)); fun invert_type_const c = case Symtab.lookup type_const_trans_table_inv c of @@ -130,15 +132,15 @@ | Br (a,ts) => let val Ts = map type_of_stree ts in - case strip_prefix Res_Clause.tconst_prefix a of + case strip_prefix SFC.tconst_prefix a of SOME b => Type(invert_type_const b, Ts) | NONE => if not (null ts) then raise STREE t (*only tconsts have type arguments*) else - case strip_prefix Res_Clause.tfree_prefix a of + case strip_prefix SFC.tfree_prefix a of SOME b => TFree("'" ^ b, HOLogic.typeS) | NONE => - case strip_prefix Res_Clause.tvar_prefix a of + case strip_prefix SFC.tvar_prefix a of SOME b => make_tvar b | NONE => make_tvar a (*Variable from the ATP, say X1*) end; @@ -146,7 +148,7 @@ (*Invert the table of translations between Isabelle and ATPs*) val const_trans_table_inv = Symtab.update ("fequal", "op =") - (Symtab.make (map swap (Symtab.dest Res_Clause.const_trans_table))); + (Symtab.make (map swap (Symtab.dest SFC.const_trans_table))); fun invert_const c = case Symtab.lookup const_trans_table_inv c of @@ -167,7 +169,7 @@ | Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*) | Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t | Br (a,ts) => - case strip_prefix Res_Clause.const_prefix a of + case strip_prefix SFC.const_prefix a of SOME "equal" => list_comb(Const ("op =", HOLogic.typeT), List.map (term_of_stree [] thy) ts) | SOME b => @@ -181,10 +183,10 @@ | NONE => (*a variable, not a constant*) let val T = HOLogic.typeT val opr = (*a Free variable is typically a Skolem function*) - case strip_prefix Res_Clause.fixed_var_prefix a of + case strip_prefix SFC.fixed_var_prefix a of SOME b => Free(b,T) | NONE => - case strip_prefix Res_Clause.schematic_var_prefix a of + case strip_prefix SFC.schematic_var_prefix a of SOME b => make_var (b,T) | NONE => make_var (a,T) (*Variable from the ATP, say X1*) in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; @@ -194,7 +196,7 @@ | constraint_of_stree pol t = case t of Int _ => raise STREE t | Br (a,ts) => - (case (strip_prefix Res_Clause.class_prefix a, map type_of_stree ts) of + (case (strip_prefix SFC.class_prefix a, map type_of_stree ts) of (SOME b, [T]) => (pol, b, T) | _ => raise STREE t); @@ -444,12 +446,14 @@ val _ = trace (Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") val (_,lines) = List.foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines val _ = trace (Int.toString (length lines) ^ " lines extracted\n") - val (ccls,fixes) = Res_Axioms.neg_conjecture_clauses ctxt th sgno + val (ccls,fixes) = Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th sgno val _ = trace (Int.toString (length ccls) ^ " conjecture clauses\n") val ccls = map forall_intr_vars ccls val _ = - if ! Res_Axioms.trace then app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls - else () + if ! Sledgehammer_Fact_Preprocessor.trace then + app (fn th => trace ("\nccl: " ^ string_of_thm ctxt th)) ccls + else + () val ilines = isar_lines ctxt (map prop_of ccls) (stringify_deps thm_names [] lines) val _ = trace "\ndecode_tstp_file: finishing\n" in