src/HOL/Tools/res_atp_setup.ML
author mengj
Fri Oct 28 02:27:19 2005 +0200 (2005-10-28)
changeset 18001 6ca14bec7cd5
parent 17939 3925ab7b8a18
child 18014 8bedb073e628
permissions -rw-r--r--
Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
     1 (* ID: $Id$ 
     2    Author: Jia Meng, NICTA
     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 warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm));
    15 
    16 fun warning_thms_n n thms nm =
    17     let val _ = warning ("total " ^ (string_of_int n) ^ " " ^ nm)
    18 	fun warning_thms_aux [] = warning ("no more " ^ nm)
    19 	  | warning_thms_aux (th::ths) = (warning_thm th nm; warning_thms_aux ths)
    20     in
    21 	warning_thms_aux thms
    22     end;
    23 
    24 
    25 (*******************************************************)
    26 (* set up the output paths                             *)
    27 (*******************************************************)
    28 
    29 val claset_file = File.tmp_path (Path.basic "claset");
    30 val simpset_file = File.tmp_path (Path.basic "simp");
    31 
    32 val prob_file = File.tmp_path (Path.basic "prob");
    33 val hyps_file = File.tmp_path (Path.basic "hyps");
    34 
    35 val types_sorts_file =  File.tmp_path (Path.basic "typsorts");
    36 
    37 (*******************************************************)
    38 (* operations on Isabelle theorems:                    *)
    39 (* retrieving from ProofContext,                       *)
    40 (* modifying local theorems,                           *)
    41 (* CNF                                                 *)
    42 (*******************************************************)
    43 
    44 (* a special version of repeat_RS *)
    45 fun repeat_someI_ex thm = ResAxioms.repeat_RS thm someI_ex;
    46 
    47 val include_simpset = ref false;
    48 val include_claset = ref false; 
    49 
    50 val add_simpset = (fn () => include_simpset:=true);
    51 val add_claset = (fn () => include_claset:=true);
    52 val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
    53 val rm_simpset = (fn () => include_simpset:=false);
    54 val rm_claset = (fn () => include_claset:=false);
    55 val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
    56 
    57 
    58 
    59 val rules_modifiers =
    60   Simplifier.simp_modifiers @ Splitter.split_modifiers @
    61   Classical.cla_modifiers @ iff_modifiers;
    62 
    63 
    64 
    65 fun get_local_claR ctxt = 
    66     let val cla_rules = rep_cs (Classical.get_local_claset ctxt) 
    67 	val safeEs = #safeEs cla_rules
    68 	val safeIs = #safeIs cla_rules
    69 	val hazEs = #hazEs cla_rules
    70 	val hazIs = #hazIs cla_rules
    71     in
    72 	map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
    73     end;
    74 
    75 
    76 fun get_local_simpR ctxt = 
    77     let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
    78     in
    79 	map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
    80 
    81 
    82 
    83 (***************************************************************)
    84 (* prover-specific output format:                              *)
    85 (* TPTP                                                        *)
    86 (***************************************************************)
    87 
    88 
    89 
    90 
    91 (***************** TPTP format *********************************)
    92 
    93 (* 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 *)
    94 
    95 fun mk_conjectures is_fol terms =
    96     if is_fol then
    97 	ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms))
    98     else
    99 	ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms));
   100 
   101 
   102 fun tptp_form_g is_fol thms n tfrees =
   103     let val terms = map prop_of thms
   104 	val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms
   105 	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
   106 	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
   107 	val out = TextIO.openOut(probfile)		 	
   108     in
   109 	ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
   110 	TextIO.closeOut out;
   111 	warning probfile; (* show the location for debugging *)
   112 	probfile (* return the location *)
   113 	
   114     end;
   115 
   116 
   117 val tptp_form = tptp_form_g true;
   118 val tptp_formH = tptp_form_g false;
   119 
   120 fun tptp_hyps_g _ [] = ([], [])
   121   | tptp_hyps_g is_fol thms =
   122     let val mk_nnf = if is_fol then make_nnf else make_nnf1
   123 	val prems = map (skolemize o mk_nnf o ObjectLogic.atomize_thm) thms
   124         val prems' = map repeat_someI_ex prems
   125         val prems'' = make_clauses prems'
   126         val prems''' = ResAxioms.rm_Eps [] prems''
   127 	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'''
   128 	val tfree_lits = ResClause.union_all tfree_litss
   129 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
   130         val hypsfile = File.platform_path hyps_file
   131         val out = TextIO.openOut(hypsfile)
   132     in
   133         ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
   134         TextIO.closeOut out; warning hypsfile;
   135         ([hypsfile],tfree_lits)
   136     end;
   137  
   138 
   139 val tptp_hyps = tptp_hyps_g true;
   140 val tptp_hypsH = tptp_hyps_g false;
   141 
   142 fun subtract_simpset thy ctxt =
   143   let
   144     val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   145     val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
   146   in map ResAxioms.pairname (map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2)) end;
   147 
   148 fun subtract_claset thy ctxt =
   149   let
   150     val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
   151     val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
   152     val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   153   in map ResAxioms.pairname (subtract netI1 netI2 @ subtract netE1 netE2) end;
   154 
   155 
   156 fun mk_axioms is_fol rules =
   157     if is_fol then 
   158 	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
   159 	     val (clss',names) = ListPair.unzip clss
   160 	     val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
   161 	 in tptpclss end)
   162     else
   163 	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules)
   164 	     val (clss',names) = ListPair.unzip clss
   165 	     val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss')
   166 	 in tptpclss end)
   167 
   168 
   169 local
   170 
   171 fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
   172   | write_rules_g is_fol rules file =
   173     let val out = TextIO.openOut(file)
   174 	val tptpclss = mk_axioms is_fol rules
   175     in
   176 	ResAtp.writeln_strs out tptpclss;
   177 	TextIO.closeOut out; warning file;
   178 	[file]
   179     end;
   180 
   181 
   182 val write_rules = write_rules_g true;
   183 val write_rulesH = write_rules_g false;
   184 
   185 in
   186 
   187 (* TPTP Isabelle theorems *)
   188 fun tptp_cnf_rules_g write_rules (clasetR,simpsetR) =
   189     let val simpfile = File.platform_path simpset_file
   190 	val clafile =  File.platform_path claset_file
   191     in
   192 	(write_rules clasetR clafile) @ (write_rules simpsetR simpfile)
   193     end;
   194 
   195 val tptp_cnf_rules = tptp_cnf_rules_g write_rules;
   196 val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH;
   197 
   198 end
   199 
   200 fun tptp_cnf_clasimp_g tptp_cnf_rules ctxt (include_claset,include_simpset) =
   201     let val local_claR = if include_claset then get_local_claR ctxt else (subtract_claset (ProofContext.theory_of ctxt) ctxt)
   202 	val local_simpR = if include_simpset then get_local_simpR ctxt else (subtract_simpset (ProofContext.theory_of ctxt) ctxt)
   203 
   204     in
   205 	tptp_cnf_rules (local_claR,local_simpR)
   206     end;
   207 
   208 
   209 val tptp_cnf_clasimp = tptp_cnf_clasimp_g tptp_cnf_rules;
   210 val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH;
   211 
   212 
   213 fun tptp_types_sorts thy = 
   214     let val classrel_clauses = ResClause.classrel_clauses_thy thy
   215 	val arity_clauses = ResClause.arity_clause_thy thy
   216 	val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
   217 	val arity_cls = map ResClause.tptp_arity_clause arity_clauses
   218 	fun write_ts () =
   219 	    let val tsfile = File.platform_path types_sorts_file
   220 		val out = TextIO.openOut(tsfile)
   221 	    in
   222 		ResAtp.writeln_strs out (classrel_cls @ arity_cls);
   223 		TextIO.closeOut out;
   224 		[tsfile]
   225 	    end
   226     in
   227 	if (List.null arity_cls andalso List.null classrel_cls) then []
   228 	else
   229 	    write_ts ()
   230     end;
   231 
   232 
   233 
   234 (*FIXME: a function that does not perform any filtering now *)
   235 fun find_relevant_ax ctxt = tptp_cnf_clasimp ctxt (true,true);
   236 
   237 
   238 (***************************************************************)
   239 (* setup ATPs as Isabelle methods                               *)
   240 (***************************************************************)
   241 fun atp_meth_g tptp_hyps tptp_cnf_clasimp tac prems ctxt = 
   242     let val rules = if !filter_ax then find_relevant_ax ctxt 
   243 		    else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset) 
   244 	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
   245 	val thy = ProofContext.theory_of ctxt
   246 	val tsfile = tptp_types_sorts thy
   247 	val files = hyps @ rules @ tsfile
   248     in
   249 	Method.METHOD (fn facts =>
   250 			  if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees)) 
   251 			  else HEADGOAL (tac ctxt files tfrees))
   252     end;
   253 
   254 val atp_meth_f = atp_meth_g tptp_hyps tptp_cnf_clasimp;
   255 
   256 val atp_meth_h = atp_meth_g tptp_hypsH tptp_cnf_clasimpH;
   257 
   258 
   259 fun atp_meth_G atp_meth tac prems ctxt =
   260     let val _ = ResClause.init (ProofContext.theory_of ctxt)
   261     in    
   262 	if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth tac prems ctxt)
   263 	else (atp_meth tac prems ctxt)
   264     end;
   265 	
   266 
   267 val atp_meth_H = atp_meth_G atp_meth_h;
   268 
   269 val atp_meth_F = atp_meth_G atp_meth_f;
   270 
   271 
   272 val atp_method_H = Method.bang_sectioned_args rules_modifiers o atp_meth_H;
   273 
   274 val atp_method_F = Method.bang_sectioned_args rules_modifiers o atp_meth_F;
   275 
   276 
   277 
   278 (*************Remove tmp files********************************)
   279 fun rm_tmp_files1 [] = ()
   280   | rm_tmp_files1 (f::fs) =
   281     (OS.FileSys.remove f; rm_tmp_files1 fs);
   282 
   283 fun cond_rm_tmp files = 
   284     if !keep_atp_input then warning "ATP input kept..." 
   285     else (warning "deleting ATP inputs..."; rm_tmp_files1 files);
   286 
   287 
   288 end