# HG changeset patch # User mengj # Date 1160182053 -7200 # Node ID ac772d489fde07950cd33d84d24eeaeb319f3d50 # Parent 784eefc906aa76a3477aae0eec6e86cbf269d68a Removed unused res_atp_setup.ML, since its functions have been put in res_atp.ML. diff -r 784eefc906aa -r ac772d489fde src/HOL/Tools/res_atp_setup.ML --- a/src/HOL/Tools/res_atp_setup.ML Sat Oct 07 01:31:23 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,510 +0,0 @@ -(* ID: $Id$ - Author: Jia Meng, NICTA - -*) -structure ResAtpSetup = - -struct - -val keep_atp_input = ref false; -val debug = ref true; - -val fol_keep_types = ResClause.keep_types; - -(* use them to set and find type levels of HOL clauses *) -val hol_full_types = ResHolClause.full_types; -val hol_partial_types = ResHolClause.partial_types; -val hol_const_types_only = ResHolClause.const_types_only; -val hol_no_types = ResHolClause.no_types; -fun hol_typ_level () = ResHolClause.find_typ_level (); - -fun is_typed_hol () = - let val tp_level = hol_typ_level() - in - not (tp_level = ResHolClause.T_NONE) - end; - -val include_combS = ResHolClause.include_combS; -val include_min_comb = ResHolClause.include_min_comb; - - - -(*******************************************************) -(* set up the output paths *) -(*******************************************************) -fun full_typed_comb () = - if !ResHolClause.include_combS then - (ResAtp.helper_path "E_HOME" "additionals/full_comb_inclS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS") - else - (ResAtp.helper_path "E_HOME" "additionals/full_comb_noS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_comb_noS"); - -fun partial_typed_comb () = - if !ResHolClause.include_combS then - (ResAtp.helper_path "E_HOME" "additionals/par_comb_inclS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS") - else - (ResAtp.helper_path "E_HOME" "additionals/par_comb_noS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_comb_noS"); - -fun const_typed_comb () = - if !ResHolClause.include_combS then - (ResAtp.helper_path "E_HOME" "additionals/const_comb_inclS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS") - else - (ResAtp.helper_path "E_HOME" "additionals/const_comb_noS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_comb_noS"); - -fun untyped_comb () = - if !ResHolClause.include_combS then - (ResAtp.helper_path "E_HOME" "additionals/u_comb_inclS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS") - else - (ResAtp.helper_path "E_HOME" "additionals/u_comb_noS" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS"); - - -fun full_typed_HOL_helper1 () = - ResAtp.helper_path "E_HOME" "additionals/full_helper1" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/full_helper1"; - -fun partial_typed_HOL_helper1 () = - ResAtp.helper_path "E_HOME" "additionals/par_helper1" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/par_helper1"; - -fun const_typed_HOL_helper1 () = - ResAtp.helper_path "E_HOME" "additionals/const_helper1" - handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/const_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 () = - let val tp_level = !ResHolClause.typ_level - in - case tp_level of ResHolClause.T_PARTIAL => (warning "Partial type helper"; partial_typed_HOL_helper1 ()) - | ResHolClause.T_FULL => (warning "Full type helper"; full_typed_HOL_helper1 ()) - | ResHolClause.T_CONST => (warning "Const type helper"; const_typed_HOL_helper1 ()) - | ResHolClause.T_NONE => (warning "Untyped helper"; untyped_HOL_helper1 ()) - end; - - -fun HOL_comb () = - let val tp_level = !ResHolClause.typ_level - in - case tp_level of ResHolClause.T_FULL => (warning "Full type comb"; full_typed_comb ()) - | ResHolClause.T_PARTIAL => (warning "Partial type comb"; partial_typed_comb ()) - | ResHolClause.T_CONST => (warning "Const type comb"; const_typed_comb ()) - | ResHolClause.T_NONE => (warning "Untyped comb"; untyped_comb ()) - end; - - -fun atp_input_file file = - let val file' = !ResAtp.problem_name ^ "_" ^ file - in - if !ResAtp.destdir = "" then File.platform_path (File.tmp_path (Path.basic file')) - else if File.exists (File.unpack_platform_path (!ResAtp.destdir)) - then !ResAtp.destdir ^ "/" ^ file' - else error ("No such directory: " ^ !ResAtp.destdir) - end; - -fun claset_file () = atp_input_file "claset"; -fun simpset_file () = atp_input_file "simp"; -fun local_lemma_file () = atp_input_file "locallemmas"; -fun hyps_file () = atp_input_file "hyps"; -fun prob_file _ = atp_input_file ""; - -fun types_sorts_file () = atp_input_file "typesorts"; - - - -(*******************************************************) -(* operations on Isabelle theorems: *) -(* retrieving from ProofContext, *) -(* modifying local theorems, *) -(* CNF *) -(*******************************************************) - -val include_simpset = ref false; -val include_claset = ref false; - -val add_simpset = (fn () => include_simpset:=true); -val add_claset = (fn () => include_claset:=true); -val add_clasimp = (fn () => include_simpset:=true;include_claset:=true); -val rm_simpset = (fn () => include_simpset:=false); -val rm_claset = (fn () => include_claset:=false); -val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false); - - -(******************************************************************) -(* 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"; - - -fun is_fol_logic FOL = true - | is_fol_logic _ = false - - -(*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 - exists has_bool targs - end; - -fun is_fn_tp (Type("fun",_)) = true - | is_fn_tp _ = false; - - -exception FN_LG of term; - -fun fn_lg (t as Const(f,tp)) (lg,seen) = - if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) - | fn_lg (t as Free(f,tp)) (lg,seen) = - if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) - | fn_lg (t as Var(f,tp)) (lg,seen) = - if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) - else (lg, insert (op =) t seen) - | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg, insert (op =) t 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, insert (op =) t seen) else (lg, insert (op =) t seen) - | pred_lg (t as Free(P,tp)) (lg,seen) = - if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) - | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t 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 - 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; - -(***************************************************************) -(* Clauses used by FOL ATPs *) -(***************************************************************) - -datatype clause = FOLClause of ResClause.clause - | HOLClause of ResHolClause.clause - - -fun isTaut (FOLClause cls) = ResClause.isTaut cls - | isTaut (HOLClause cls) = ResHolClause.isTaut cls - - -fun clause2tptp (FOLClause cls) = ResClause.clause2tptp cls - | clause2tptp (HOLClause cls) = ResHolClause.clause2tptp cls - - -fun make_clause_fol cls = FOLClause cls - -fun make_clause_hol cls = HOLClause cls - -fun make_conjecture_clauses is_fol terms = - if is_fol then map make_clause_fol (ResClause.make_conjecture_clauses terms) - else - map make_clause_hol (ResHolClause.make_conjecture_clauses terms) - -(***************************************************************) -(* prover-specific output format: *) -(* 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 - in - ResClause.union_all (map ResAxioms.skolem_thm ths) - end; - -(**** clausification ****) - -fun cls_axiom _ _ _ [] = [] - | cls_axiom is_fol name i (tm::tms) = - if is_fol then - (case ResClause.make_axiom_clause tm (name,i) of - SOME cls => (FOLClause cls) :: cls_axiom true name (i+1) tms - | NONE => cls_axiom true name i tms) - else - HOLClause (ResHolClause.make_axiom_clause tm (name,i)) :: - cls_axiom false name (i+1) tms; - - -fun filtered_tptp_axiom is_fol name clss = - (fst - (ListPair.unzip - (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))), - []) handle _ => ([],[name]); - -fun tptp_axioms_aux _ [] err = ([],err) - | tptp_axioms_aux is_fol ((name,clss)::nclss) err = - let val (nclss1,err1) = tptp_axioms_aux is_fol nclss err - val (clsstrs,err_name_list) = filtered_tptp_axiom is_fol name clss - in - case clsstrs of [] => (nclss1,err_name_list @ err1) - | _ => (clsstrs::nclss1,err1) - end; - -fun tptp_axioms is_fol rules = tptp_axioms_aux is_fol rules []; - -fun atp_axioms is_fol rules file = - let val out = TextIO.openOut file - val (clss,errs) = tptp_axioms is_fol rules - val clss' = ResClause.union_all clss - in - ResClause.writeln_strs out clss'; - TextIO.closeOut out; - ([file],errs) - end; - - -fun filtered_tptp_conjectures is_fol terms = - let val clss = make_conjecture_clauses is_fol terms - val clss' = filter (fn c => not (isTaut c)) clss - in - ListPair.unzip (map clause2tptp clss') - end; - - -fun atp_conjectures_h is_fol hyp_cls = - let val (tptp_h_clss,tfree_litss) = filtered_tptp_conjectures is_fol hyp_cls - val tfree_lits = ResClause.union_all tfree_litss - val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits - val hypsfile = hyps_file () - val out = TextIO.openOut(hypsfile) - in - ResClause.writeln_strs out (tfree_clss @ tptp_h_clss); - TextIO.closeOut out; warning hypsfile; - ([hypsfile],tfree_lits) - end; - - -fun atp_conjectures_c is_fol conj_cls n tfrees = - let val (tptp_c_clss,tfree_litss) = filtered_tptp_conjectures is_fol conj_cls - val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees) - val probfile = prob_file n - val out = TextIO.openOut(probfile) - in - ResClause.writeln_strs out (tfree_clss @ tptp_c_clss); - TextIO.closeOut out; - warning probfile; - probfile - end; - - -fun atp_conjectures is_fol [] conj_cls n = - let val probfile = atp_conjectures_c is_fol conj_cls n [] - in - [probfile] - end - | atp_conjectures is_fol hyp_cls conj_cls n = - let val (hypsfile,tfree_lits) = atp_conjectures_h is_fol hyp_cls - val probfile = atp_conjectures_c is_fol conj_cls n tfree_lits - in - (probfile::hypsfile) - end; - - -(**** 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 - val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses - val arity_cls = map ResClause.tptp_arity_clause arity_clauses - fun write_ts () = - let val tsfile = types_sorts_file () - val out = TextIO.openOut(tsfile) - in - ResClause.writeln_strs out (classrel_cls @ arity_cls); - TextIO.closeOut out; - [tsfile] - end - in - if (List.null arity_cls andalso List.null classrel_cls) then [] - else - write_ts () - end; - - -(******* write to files ******) - -datatype mode = Auto | Fol | Hol; - -fun write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) = - let val is_fol = is_fol_logic logic - val (files1,err1) = if (null claR) then ([],[]) - else (atp_axioms is_fol claR (claset_file())) - val (files2,err2) = if (null simpR) then ([],[]) - else (atp_axioms is_fol simpR (simpset_file ())) - val (files3,err3) = if (null userR) then ([],[]) - else (atp_axioms is_fol userR (local_lemma_file ())) - val files4 = atp_conjectures is_fol 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 - (helpers,files4 @ files1 @ files2 @ files3) - end; - - -fun write_out_ts is_fol ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) = - let val ts_file = if ((is_fol andalso (!fol_keep_types)) orelse ((not is_fol) andalso (is_typed_hol ()))) then tptp_types_sorts (ProofContext.theory_of ctxt) else [] - val logic = if is_fol then FOL else HOL - val (helpers,files) = write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) - in - (helpers,files) - 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_ts true ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs) - | _ => write_out_ts false ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,errs) - - end; - - -(***************************************************************) -(* setup ATPs as Isabelle methods *) -(***************************************************************) - - -fun atp_meth' tac ths ctxt = - Method.SIMPLE_METHOD' HEADGOAL - (tac ctxt ths); - -fun atp_meth tac ths ctxt = - let val thy = ProofContext.theory_of ctxt - val _ = ResClause.init thy - val _ = ResHolClause.init thy - in - atp_meth' tac ths ctxt - end; - - -fun atp_method tac = Method.thms_ctxt_args (atp_meth tac); - - -(*************Remove tmp files********************************) -fun rm_tmp_files1 [] = () - | rm_tmp_files1 (f::fs) = - (OS.FileSys.remove f; rm_tmp_files1 fs); - -fun cond_rm_tmp files = - if !keep_atp_input then warning "ATP input kept..." - else if !ResAtp.destdir <> "" then warning ("ATP input kept in directory " ^ (!ResAtp.destdir)) - else (warning "deleting ATP inputs..."; rm_tmp_files1 files); - -end