src/HOL/Tools/res_atp_setup.ML
author mengj
Wed Oct 19 06:33:24 2005 +0200 (2005-10-19)
changeset 17905 1574533861b1
child 17907 c20e4bddcb11
permissions -rw-r--r--
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
     1 (* Author: Jia Meng
     2    Date: 12/09/2005
     3 
     4 *)
     5 structure ResAtpSetup =
     6 
     7 struct
     8 
     9 val keep_atp_input = ref false;
    10 val debug = ref true;
    11 val filter_ax = ref false;
    12 
    13 
    14 fun writeln_strs _   []      = ()
    15   | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    16 
    17 
    18 fun no_rep_add x []     = [x]
    19   | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
    20 
    21 fun no_rep_app l1 []     = l1
    22   | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
    23 
    24 
    25 fun flat_noDup []     = []
    26   | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    27 
    28 fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm));
    29 
    30 fun warning_thms_n n thms nm =
    31     let val _ = warning ("total " ^ (string_of_int n) ^ " " ^ nm)
    32 	fun warning_thms_aux [] = warning ("no more " ^ nm)
    33 	  | warning_thms_aux (th::ths) = (warning_thm th nm; warning_thms_aux ths)
    34     in
    35 	warning_thms_aux thms
    36     end;
    37 
    38 
    39 (*******************************************************)
    40 (* set up the output paths                             *)
    41 (*******************************************************)
    42 
    43 val claset_file = File.tmp_path (Path.basic "claset");
    44 val simpset_file = File.tmp_path (Path.basic "simp");
    45 
    46 val prob_file = File.tmp_path (Path.basic "prob");
    47 val hyps_file = File.tmp_path (Path.basic "hyps");
    48 
    49 
    50 
    51 (*******************************************************)
    52 (* operations on Isabelle theorems:                    *)
    53 (* retrieving from ProofContext,                       *)
    54 (* modifying local theorems,                           *)
    55 (* CNF                                                 *)
    56 (*******************************************************)
    57 
    58 fun repeat_RS thm1 thm2 =
    59     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    60     in
    61         if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    62     end;
    63 
    64 (* a special version of repeat_RS *)
    65 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    66 
    67 val include_simpset = ref false;
    68 val include_claset = ref false; 
    69 
    70 val add_simpset = (fn () => include_simpset:=true);
    71 val add_claset = (fn () => include_claset:=true);
    72 val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
    73 val rm_simpset = (fn () => include_simpset:=false);
    74 val rm_claset = (fn () => include_claset:=false);
    75 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
    76 
    77 
    78 
    79 val rules_modifiers =
    80   Simplifier.simp_modifiers @ Splitter.split_modifiers @
    81   Classical.cla_modifiers @ iff_modifiers;
    82 
    83 
    84 
    85 fun get_local_claR ctxt = 
    86     let val cla_rules = rep_cs (Classical.get_local_claset ctxt) 
    87 	val safeEs = #safeEs cla_rules
    88 	val safeIs = #safeIs cla_rules
    89 	val hazEs = #hazEs cla_rules
    90 	val hazIs = #hazIs cla_rules
    91     in
    92 	map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
    93     end;
    94 
    95 
    96 fun get_local_simpR ctxt = 
    97     let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
    98     in
    99 	map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
   100 
   101 
   102 
   103 (***************************************************************)
   104 (* prover-specific output format:                              *)
   105 (* TPTP                                                        *)
   106 (***************************************************************)
   107 
   108 
   109 
   110 
   111 (***************** TPTP format *********************************)
   112 
   113 (* 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 *)
   114 fun tptp_form thms n tfrees =
   115     let val clss = ResClause.make_conjecture_clauses (map prop_of thms)
   116 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
   117 	val tfree_clss = map ResClause.tfree_clause ((flat_noDup tfree_litss) \\ tfrees)
   118 	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
   119 	val out = TextIO.openOut(probfile)		 	
   120     in
   121 	writeln_strs out (tfree_clss @ tptp_clss);
   122 	TextIO.closeOut out;
   123 	warning probfile; (* show the location for debugging *)
   124 	probfile (* return the location *)
   125 	
   126     end;
   127 
   128 
   129 fun tptp_hyps [] = ([], [])
   130   | tptp_hyps thms =
   131     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
   132         val prems' = map repeat_someI_ex prems
   133         val prems'' = make_clauses prems'
   134         val prems''' = ResAxioms.rm_Eps [] prems''
   135         val clss = ResClause.make_conjecture_clauses prems'''
   136 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
   137 	val tfree_lits = flat_noDup tfree_litss
   138 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
   139         val hypsfile = File.platform_path hyps_file
   140         val out = TextIO.openOut(hypsfile)
   141     in
   142         writeln_strs out (tfree_clss @ tptp_clss);
   143         TextIO.closeOut out; warning hypsfile;
   144         ([hypsfile],tfree_lits)
   145     end;
   146  
   147 
   148 fun subtract_simpset thy ctxt =
   149   let
   150     val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   151     val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
   152   in map ResAxioms.pairname (map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2)) end;
   153 
   154 fun subtract_claset thy ctxt =
   155   let
   156     val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
   157     val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
   158     val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   159   in map ResAxioms.pairname (subtract netI1 netI2 @ subtract netE1 netE2) end;
   160 
   161 local
   162 
   163 fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
   164   | write_rules rules file =
   165     let val out = TextIO.openOut(file)
   166 	val clss = flat_noDup(ResAxioms.clausify_rules_pairs rules)
   167 	val (clss',names) = ListPair.unzip clss
   168 	val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
   169     in
   170 	writeln_strs out tptpclss;
   171 	TextIO.closeOut out; warning file;
   172 	[file]
   173     end;
   174 
   175 in
   176 
   177 (* TPTP Isabelle theorems *)
   178 fun tptp_cnf_rules (clasetR,simpsetR) =
   179     let val simpfile = File.platform_path simpset_file
   180 	val clafile =  File.platform_path claset_file
   181     in
   182 	(write_rules clasetR clafile) @ (write_rules simpsetR simpfile)
   183     end;
   184 
   185 end
   186 
   187 fun tptp_cnf_clasimp ctxt (include_claset,include_simpset) =
   188     let val local_claR = if include_claset then get_local_claR ctxt else (subtract_claset (ProofContext.theory_of ctxt) ctxt)
   189 	val local_simpR = if include_simpset then get_local_simpR ctxt else (subtract_simpset (ProofContext.theory_of ctxt) ctxt)
   190 
   191     in
   192 	tptp_cnf_rules (local_claR,local_simpR)
   193     end;
   194 
   195 
   196 (*FIXME: a function that does not perform any filtering now *)
   197 fun find_relevant_ax ctxt = tptp_cnf_clasimp ctxt (true,true);
   198 
   199 
   200 
   201 (***************************************************************)
   202 (* setup ATPs as Isabelle methods                               *)
   203 (***************************************************************)
   204 fun atp_meth' tac prems ctxt = 
   205     let val rules = if !filter_ax then (find_relevant_ax ctxt) else (tptp_cnf_clasimp ctxt (!include_claset, !include_simpset)) 
   206 	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
   207 	val files = hyps @ rules
   208     in
   209 	Method.METHOD (fn facts =>
   210 			  if !debug then ((warning_thms_n (length facts) facts "facts");HEADGOAL (tac ctxt files tfrees)) else (HEADGOAL (tac ctxt files tfrees)))
   211     end;
   212 
   213 
   214 fun atp_meth tac prems ctxt =
   215     let val _ = ResClause.init (ProofContext.theory_of ctxt)
   216     in    
   217 	if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth' tac prems ctxt)
   218 	else (atp_meth' tac prems ctxt)
   219     end;
   220 	
   221 val atp_method = Method.bang_sectioned_args rules_modifiers o atp_meth;
   222 
   223 
   224 
   225 
   226 (*************Remove tmp files********************************)
   227 fun rm_tmp_files1 [] = ()
   228   | rm_tmp_files1 (f::fs) =
   229     (OS.FileSys.remove f; rm_tmp_files1 fs);
   230 
   231 fun cond_rm_tmp files = (if (!keep_atp_input) then (warning "ATP input kept...") else (warning "deleting ATP inputs..."; rm_tmp_files1 files));
   232 
   233 
   234 end