--- a/src/HOL/Tools/res_atp_setup.ML Mon Nov 28 07:14:12 2005 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML Mon Nov 28 07:15:13 2005 +0100
@@ -8,7 +8,14 @@
val keep_atp_input = ref false;
val debug = ref true;
-val filter_ax = ref false;
+
+val fol_keep_types = ResClause.keep_types;
+val hol_keep_types = ResHolClause.keep_types;
+
+val include_combS = ResHolClause.include_combS;
+val include_min_comb = ResHolClause.include_min_comb;
+
+
(*******************************************************)
(* set up the output paths *)
@@ -30,6 +37,25 @@
(ResAtp.helper_path "E_HOME" "additionals/u_comb_noS"
handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS");
+
+fun typed_HOL_helper1 () =
+ ResAtp.helper_path "E_HOME" "additionals/helper1"
+ handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/helper1";
+
+
+fun untyped_HOL_helper1 () =
+ ResAtp.helper_path "E_HOME" "additionals/u_helper1"
+ handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_helper1";
+
+
+fun HOL_helper1 () =
+ if !hol_keep_types then typed_HOL_helper1 () else untyped_HOL_helper1 ();
+
+
+fun HOL_comb () =
+ if !hol_keep_types then typed_comb() else untyped_comb();
+
+
val claset_file = File.tmp_path (Path.basic "claset");
val simpset_file = File.tmp_path (Path.basic "simp");
val local_lemma_file = File.tmp_path (Path.basic "locallemmas");
@@ -60,21 +86,128 @@
val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
-fun get_local_claR ctxt =
- let val cla_rules = rep_cs (Classical.get_local_claset ctxt)
- val safeEs = #safeEs cla_rules
- val safeIs = #safeIs cla_rules
- val hazEs = #hazEs cla_rules
- val hazIs = #hazIs cla_rules
+(******************************************************************)
+(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
+(******************************************************************)
+
+datatype logic = FOL | HOL | HOLC | HOLCS;
+
+fun string_of_logic FOL = "FOL"
+ | string_of_logic HOL = "HOL"
+ | string_of_logic HOLC = "HOLC"
+ | string_of_logic HOLCS = "HOLCS";
+
+(*HOLCS will not occur here*)
+fun upgrade_lg HOLC _ = HOLC
+ | upgrade_lg HOL HOLC = HOLC
+ | upgrade_lg HOL _ = HOL
+ | upgrade_lg FOL lg = lg;
+
+(* check types *)
+fun has_bool (Type("bool",_)) = true
+ | has_bool (Type(_, Ts)) = exists has_bool Ts
+ | has_bool _ = false;
+
+fun has_bool_arg tp =
+ let val (targs,tr) = strip_type tp
in
- map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
+ exists has_bool targs
end;
+fun is_fn_tp (Type("fun",_)) = true
+ | is_fn_tp _ = false;
-fun get_local_simpR ctxt =
- let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
+
+exception FN_LG of term;
+
+fun fn_lg (t as Const(f,tp)) (lg,seen) =
+ if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen)
+ | fn_lg (t as Free(f,tp)) (lg,seen) =
+ if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen)
+ | fn_lg (t as Var(f,tp)) (lg,seen) =
+ if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
+ else (lg,t ins seen)
+ | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
+ | fn_lg f _ = raise FN_LG(f);
+
+
+fun term_lg [] (lg,seen) = (lg,seen)
+ | term_lg (tm::tms) (FOL,seen) =
+ let val (f,args) = strip_comb tm
+ val (lg',seen') = if f mem seen then (FOL,seen)
+ else fn_lg f (FOL,seen)
+
+ in
+ term_lg (args@tms) (lg',seen')
+ end
+ | term_lg _ (lg,seen) = (lg,seen)
+
+exception PRED_LG of term;
+
+fun pred_lg (t as Const(P,tp)) (lg,seen)=
+ if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
+ | pred_lg (t as Free(P,tp)) (lg,seen) =
+ if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
+ | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
+ | pred_lg P _ = raise PRED_LG(P);
+
+
+fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
+ | lit_lg P (lg,seen) =
+ let val (pred,args) = strip_comb P
+ val (lg',seen') = if pred mem seen then (lg,seen)
+ else pred_lg pred (lg,seen)
in
- map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
+ term_lg args (lg',seen')
+ end;
+
+fun lits_lg [] (lg,seen) = (lg,seen)
+ | lits_lg (lit::lits) (FOL,seen) =
+ lits_lg lits (lit_lg lit (FOL,seen))
+ | lits_lg lits (lg,seen) = (lg,seen);
+
+
+fun logic_of_clause tm (lg,seen) =
+ let val tm' = HOLogic.dest_Trueprop tm
+ val disjs = HOLogic.dest_disj tm'
+ in
+ lits_lg disjs (lg,seen)
+ end;
+
+fun lits_lg [] (lg,seen) = (lg,seen)
+ | lits_lg (lit::lits) (FOL,seen) =
+ lits_lg lits (lit_lg lit (FOL,seen))
+ | lits_lg lits (lg,seen) = (lg,seen);
+
+
+fun logic_of_clause tm (lg,seen) =
+ let val tm' = HOLogic.dest_Trueprop tm
+ val disjs = HOLogic.dest_disj tm'
+ in
+ lits_lg disjs (lg,seen)
+ end;
+
+fun logic_of_clauses [] (lg,seen) = (lg,seen)
+ | logic_of_clauses (cls::clss) (FOL,seen) =
+ logic_of_clauses clss (logic_of_clause cls (FOL,seen))
+ | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
+
+fun logic_of_nclauses [] (lg,seen) = (lg,seen)
+ | logic_of_nclauses (cls::clss) (FOL,seen) =
+ logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
+ | logic_of_nclauses clss (lg,seen) = (lg,seen);
+
+
+
+fun problem_logic (conj_cls,hyp_cls,userR,claR,simpR) =
+ let val (lg1,seen1) = logic_of_clauses conj_cls (FOL,[])
+ val (lg2,seen2) = logic_of_clauses hyp_cls (lg1,seen1)
+ val (lg3,seen3) = logic_of_nclauses userR (lg2,seen2)
+ val (lg4,seen4) = logic_of_nclauses claR (lg3,seen3)
+ val (lg5,seen5) = logic_of_nclauses simpR (lg4,seen4)
+ in
+ lg5
+ end;
@@ -83,113 +216,138 @@
(* TPTP *)
(***************************************************************)
+(**** CNF rules and hypothesis ****)
+fun cnf_rules_tms ctxt ths (include_claset,include_simpset) =
+ let val local_claR = if include_claset then ResAxioms.claset_rules_of_ctxt ctxt else []
+ val (local_claR_cls,err1) = ResAxioms.cnf_rules2 local_claR []
+ val local_simpR = if include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt else []
+ val (local_simpR_cls,err2) = ResAxioms.cnf_rules2 local_simpR []
+ val (user_ths_cls,err3) = ResAxioms.cnf_rules2 (map ResAxioms.pairname ths) []
+ val errs = err3 @ err2 @ err1
+ in
+ (user_ths_cls,local_simpR_cls,local_claR_cls,errs)
+ end;
+fun cnf_hyps_thms ctxt =
+ let val ths = ProofContext.prems_of ctxt
+ val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux ths)
+ in
+ prems
+ end;
+
+(**** clausification ****)
+fun cls_axiom_fol _ _ [] = []
+ | cls_axiom_fol name i (tm::tms) =
+ (ResClause.make_axiom_clause tm (name,i)) :: (cls_axiom_fol name (i+1) tms);
+
+fun cls_axiom_hol _ _ [] = []
+ | cls_axiom_hol name i (tm::tms) =
+ (ResHolClause.make_axiom_clause tm (name,i)) :: (cls_axiom_hol name (i+1) tms);
-(***************** TPTP format *********************************)
+fun filtered_tptp_axiom_fol name clss =
+ (fst(ListPair.unzip (map ResClause.clause2tptp (filter (fn c => not (ResClause.isTaut c)) (cls_axiom_fol name 0 clss)))),[])
+ handle _ => ([],[name]);
-(* convert each (sub)goal clause (Thm.thm) into one or more TPTP clauses. The additional TPTP clauses are tfree_lits. Write the output TPTP clauses to a problem file *)
+fun filtered_tptp_axiom_hol name clss =
+ (fst(ListPair.unzip (map ResHolClause.clause2tptp (filter (fn c => not (ResHolClause.isTaut c)) (cls_axiom_hol name 0 clss)))),[])
+ handle _ => ([],[name]);
-fun mk_conjectures is_fol terms =
- if is_fol then
- ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms))
- else
- ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms));
+fun tptp_axioms_g filt_ax_fn [] err = ([],err)
+ | tptp_axioms_g filt_ax_fn ((name,clss)::nclss) err =
+ let val (nclss1,err1) = tptp_axioms_g filt_ax_fn nclss err
+ val (clsstrs,err_name_list) = filt_ax_fn name clss
+ in
+ case clsstrs of [] => (nclss1,err_name_list @ err1)
+ | _ => (clsstrs::nclss1,err1)
+ end;
+
+fun tptp_axioms_fol rules = tptp_axioms_g filtered_tptp_axiom_fol rules [];
+
+fun tptp_axioms_hol rules = tptp_axioms_g filtered_tptp_axiom_hol rules [];
+
+
+fun atp_axioms_g tptp_ax_fn rules file =
+ let val out = TextIO.openOut file
+ val (clss,errs) = tptp_ax_fn rules
+ val clss' = ResClause.union_all clss
+ in
+ ResAtp.writeln_strs out clss';
+ TextIO.closeOut out;
+ ([file],errs)
+ end;
-fun tptp_form_g is_fol thms n tfrees =
- let val terms = map prop_of thms
- val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms
+fun atp_axioms_fol rules file = atp_axioms_g tptp_axioms_fol rules file;
+
+fun atp_axioms_hol rules file = atp_axioms_g tptp_axioms_hol rules file;
+
+
+fun filtered_tptp_conjectures_fol terms =
+ let val clss = ResClause.make_conjecture_clauses terms
+ val clss' = filter (fn c => not (ResClause.isTaut c)) clss
+ in
+ ListPair.unzip (map ResClause.clause2tptp clss')
+ end;
+
+fun filtered_tptp_conjectures_hol terms =
+ let val clss = ResHolClause.make_conjecture_clauses terms
+ val clss' = filter (fn c => not (ResHolClause.isTaut c)) clss
+ in
+ ListPair.unzip (map ResHolClause.clause2tptp clss')
+ end;
+
+fun atp_conjectures_h_g filt_conj_fn hyp_cls =
+ let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls
+ val tfree_lits = ResClause.union_all tfree_litss
+ val tfree_clss = map ResClause.tfree_clause tfree_lits
+ val hypsfile = File.platform_path hyps_file
+ val out = TextIO.openOut(hypsfile)
+ in
+ ResAtp.writeln_strs out (tfree_clss @ tptp_h_clss);
+ TextIO.closeOut out; warning hypsfile;
+ ([hypsfile],tfree_lits)
+ end;
+
+fun atp_conjectures_h_fol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_fol hyp_cls;
+
+fun atp_conjectures_h_hol hyp_cls = atp_conjectures_h_g filtered_tptp_conjectures_hol hyp_cls;
+
+fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees =
+ let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls
val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
val out = TextIO.openOut(probfile)
in
- ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
+ ResAtp.writeln_strs out (tfree_clss @ tptp_c_clss);
TextIO.closeOut out;
- warning probfile; (* show the location for debugging *)
- probfile (* return the location *)
-
+ warning probfile;
+ probfile
end;
-
-val tptp_form = tptp_form_g true;
-val tptp_formH = tptp_form_g false;
+fun atp_conjectures_c_fol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_fol conj_cls n tfrees;
-fun tptp_hyps_g _ [] = ([], [])
- | tptp_hyps_g is_fol thms =
- let val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux thms)
- val prems' = map prop_of prems
- val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'
- val tfree_lits = ResClause.union_all tfree_litss
- val tfree_clss = map ResClause.tfree_clause tfree_lits
- val hypsfile = File.platform_path hyps_file
- val out = TextIO.openOut(hypsfile)
- in
- ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
- TextIO.closeOut out; warning hypsfile;
- ([hypsfile],tfree_lits)
- end;
-
-
-val tptp_hyps = tptp_hyps_g true;
-val tptp_hypsH = tptp_hyps_g false;
-
-fun mk_axioms is_fol rules =
- if is_fol then
- (let val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
- val (clss',names) = ListPair.unzip clss
- val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
- in tptpclss end)
- else
- (let val clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules)
- val (clss',names) = ListPair.unzip clss
- val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss')
- in tptpclss end)
+fun atp_conjectures_c_hol conj_cls n tfrees = atp_conjectures_c_g filtered_tptp_conjectures_hol conj_cls n tfrees;
-
-fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
- | write_rules_g is_fol rules file =
- let val out = TextIO.openOut(file)
- val tptpclss = mk_axioms is_fol rules
+fun atp_conjectures_g atp_conj_h_fn atp_conj_c_fn [] conj_cls n =
+ let val probfile = atp_conj_c_fn conj_cls n []
in
- ResAtp.writeln_strs out tptpclss;
- TextIO.closeOut out; warning file;
- [file]
+ [probfile]
+ end
+ | atp_conjectures_g atp_conj_h_fn atp_conj_c_fn hyp_cls conj_cls n =
+ let val (hypsfile,tfree_lits) = atp_conj_h_fn hyp_cls
+ val probfile = atp_conj_c_fn conj_cls n tfree_lits
+ in
+ (probfile::hypsfile)
end;
+fun atp_conjectures_fol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_fol atp_conjectures_c_fol hyp_cls conj_cls n;
-val write_rules = write_rules_g true;
-val write_rulesH = write_rules_g false;
-
+fun atp_conjectures_hol hyp_cls conj_cls n = atp_conjectures_g atp_conjectures_h_hol atp_conjectures_c_hol hyp_cls conj_cls n;
-(* TPTP Isabelle theorems *)
-fun tptp_cnf_rules_g write_rules ths (clasetR,simpsetR) =
- let val simpfile = File.platform_path simpset_file
- val clafile = File.platform_path claset_file
- val local_lemfile = File.platform_path local_lemma_file
- in
- (write_rules clasetR clafile) @ (write_rules simpsetR simpfile) @ (write_rules ths local_lemfile)
- end;
-
-val tptp_cnf_rules = tptp_cnf_rules_g write_rules;
-val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH;
-
-
-fun tptp_cnf_clasimp_g tptp_cnf_rules ths ctxt (include_claset,include_simpset) =
- let val local_claR = if include_claset then get_local_claR ctxt else []
- val local_simpR = if include_simpset then get_local_simpR ctxt else []
- val ths_names = map ResAxioms.pairname ths
- in
- tptp_cnf_rules ths_names (local_claR,local_simpR)
- end;
-
-
-val tptp_cnf_clasimp = tptp_cnf_clasimp_g tptp_cnf_rules;
-val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH;
-
-
+(**** types and sorts ****)
fun tptp_types_sorts thy =
let val classrel_clauses = ResClause.classrel_clauses_thy thy
val arity_clauses = ResClause.arity_clause_thy thy
@@ -210,45 +368,80 @@
end;
+(******* write to files ******)
-(*FIXME: a function that does not perform any filtering now *)
-fun find_relevant_ax tptp_cnf_clasimp ths ctxt = tptp_cnf_clasimp ths ctxt (true,true);
+datatype mode = Auto | Fol | Hol;
+
+fun write_out_g logic atp_ax_fn atp_conj_fn (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
+ let val (files1,err1) = if (null claR) then ([],[]) else (atp_ax_fn claR (File.platform_path claset_file))
+ val (files2,err2) = if (null simpR) then ([],[]) else (atp_ax_fn simpR (File.platform_path simpset_file))
+ val (files3,err3) = if (null userR) then ([],[]) else (atp_ax_fn userR (File.platform_path local_lemma_file))
+ val files4 = atp_conj_fn hyp_cls conj_cls n
+ val errs = err1 @ err2 @ err3 @ err
+ val logic' = if !include_combS then HOLCS
+ else
+ if !include_min_comb then HOLC else logic
+ val _ = warning ("Problems are " ^ (string_of_logic logic'))
+ val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
+ val helpers = case logic' of FOL => []
+ | HOL => [HOL_helper1 ()]
+ | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
+ in
+ include_min_comb:=false; (*reset to false*)
+ include_combS:=false; (*reset to false*)
+ (helpers,files4 @ files1 @ files2 @ files3)
+ end;
+
+fun write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g FOL atp_axioms_fol atp_conjectures_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
+
+fun write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err) = write_out_g HOL atp_axioms_hol atp_conjectures_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err);
+
+fun write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
+ let val ts_file = if (!fol_keep_types) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
+ val (helpers,files) = write_out_fol (claR,simpR,userR,hyp_cls,conj_cls,n,err)
+ in
+ (helpers,files@ts_file)
+ end;
+
+fun write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
+ let val ts_file = if (!hol_keep_types) then tptp_types_sorts (ProofContext.theory_of ctxt) else []
+ val (helpers,files) = write_out_hol (claR,simpR,userR,hyp_cls,conj_cls,n,err)
+ in
+ (helpers,files@ts_file)
+ end;
+
+
+fun prep_atp_input mode ctxt conjectures user_thms n =
+ let val conj_cls = map prop_of (make_clauses conjectures)
+ val (userR,simpR,claR,errs) = cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset)
+ val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
+ val logic = case mode of Auto => problem_logic (conj_cls,hyp_cls,userR,claR,simpR)
+ | Fol => FOL
+ | Hol => HOL
+ in
+ case logic of FOL => write_out_fol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
+ | _ => write_out_hol_ts ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs)
+
+ end;
(***************************************************************)
(* setup ATPs as Isabelle methods *)
(***************************************************************)
-fun atp_meth_g helper_file tptp_hyps tptp_cnf_clasimp tac ths ctxt =
- let val rules = if !filter_ax then find_relevant_ax tptp_cnf_clasimp ths ctxt
- else tptp_cnf_clasimp ths ctxt (!include_claset, !include_simpset)
- val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
- val thy = ProofContext.theory_of ctxt
- val tsfile = tptp_types_sorts thy
- val files = (helper_file,hyps @ rules @ tsfile)
+
+
+fun atp_meth' tac ths ctxt =
+ Method.SIMPLE_METHOD' HEADGOAL
+ (tac ctxt ths);
+
+fun atp_meth tac ths ctxt =
+ let val _ = ResClause.init (ProofContext.theory_of ctxt)
in
- Method.SIMPLE_METHOD' HEADGOAL
- (tac ctxt files tfrees)
- end;
-fun atp_meth_f tac ths ctxt = atp_meth_g [] tptp_hyps tptp_cnf_clasimp tac ths ctxt;
-fun atp_meth_h tac ths ctxt =
- let val helper = if !ResHolClause.keep_types then [typed_comb ()] else [untyped_comb ()]
- in
- atp_meth_g helper tptp_hypsH tptp_cnf_clasimpH tac ths ctxt
+ atp_meth' tac ths ctxt
end;
-fun atp_meth_G atp_meth tac ths ctxt =
- let val _ = ResClause.init (ProofContext.theory_of ctxt)
- in
- atp_meth tac ths ctxt
- end;
-fun atp_meth_H tac ths ctxt = atp_meth_G atp_meth_h tac ths ctxt;
-fun atp_meth_F tac ths ctxt = atp_meth_G atp_meth_f tac ths ctxt;
-
-
-fun atp_method_H tac = Method.thms_ctxt_args (atp_meth_H tac);
-fun atp_method_F tac = Method.thms_ctxt_args (atp_meth_F tac);
-
+fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
(*************Remove tmp files********************************)