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