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