--- 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
--- 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 ());
--- 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
--- 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 =
--- 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;
--- 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))
--- 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
--- 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_";
--- 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 @
--- 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