src/HOL/Tools/res_atp_setup.ML
author mengj
Fri Nov 18 07:07:47 2005 +0100 (2005-11-18)
changeset 18197 082a2bd6f655
parent 18141 89e2e8bed08f
child 18273 e15a825da262
permissions -rw-r--r--
-- added combinator reduction axioms (typed and untyped) for HOL goals.
-- combined make_nnf functions for HOL and FOL goals.
-- hypothesis of goals are now also skolemized by inference.
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
(* set up the output paths                             *)
mengj@17905
    15
(*******************************************************)
mengj@17905
    16
mengj@18197
    17
fun typed_comb () = 
mengj@18197
    18
    if !ResHolClause.include_combS then 
mengj@18197
    19
	(ResAtp.helper_path "E_HOME" "additionals/comb_inclS"
mengj@18197
    20
	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/comb_inclS")
mengj@18197
    21
    else 
mengj@18197
    22
	(ResAtp.helper_path "E_HOME" "additionals/comb_noS"
mengj@18197
    23
	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/comb_noS");
mengj@18197
    24
mengj@18197
    25
fun untyped_comb () = 
mengj@18197
    26
    if !ResHolClause.include_combS then 
mengj@18197
    27
	(ResAtp.helper_path "E_HOME" "additionals/u_comb_inclS"
mengj@18197
    28
	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS")
mengj@18197
    29
    else
mengj@18197
    30
	(ResAtp.helper_path "E_HOME" "additionals/u_comb_noS"
mengj@18197
    31
	 handle _ => ResAtp.helper_path "VAMPIRE_HOME" "additionals/u_comb_noS");
mengj@18197
    32
mengj@17905
    33
val claset_file = File.tmp_path (Path.basic "claset");
mengj@17905
    34
val simpset_file = File.tmp_path (Path.basic "simp");
mengj@18086
    35
val local_lemma_file = File.tmp_path (Path.basic "locallemmas");
mengj@17905
    36
mengj@17905
    37
val prob_file = File.tmp_path (Path.basic "prob");
mengj@17905
    38
val hyps_file = File.tmp_path (Path.basic "hyps");
mengj@17905
    39
mengj@18001
    40
val types_sorts_file =  File.tmp_path (Path.basic "typsorts");
mengj@17905
    41
mengj@17905
    42
(*******************************************************)
mengj@17905
    43
(* operations on Isabelle theorems:                    *)
mengj@17905
    44
(* retrieving from ProofContext,                       *)
mengj@17905
    45
(* modifying local theorems,                           *)
mengj@17905
    46
(* CNF                                                 *)
mengj@17905
    47
(*******************************************************)
mengj@17905
    48
mengj@17905
    49
(* a special version of repeat_RS *)
mengj@18001
    50
fun repeat_someI_ex thm = ResAxioms.repeat_RS thm someI_ex;
mengj@17905
    51
mengj@17905
    52
val include_simpset = ref false;
mengj@17905
    53
val include_claset = ref false; 
mengj@17905
    54
mengj@17905
    55
val add_simpset = (fn () => include_simpset:=true);
mengj@17905
    56
val add_claset = (fn () => include_claset:=true);
mengj@17905
    57
val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
mengj@17905
    58
val rm_simpset = (fn () => include_simpset:=false);
mengj@17905
    59
val rm_claset = (fn () => include_claset:=false);
mengj@17905
    60
val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
mengj@17905
    61
mengj@17905
    62
mengj@17905
    63
fun get_local_claR ctxt = 
mengj@17905
    64
    let val cla_rules = rep_cs (Classical.get_local_claset ctxt) 
mengj@17905
    65
	val safeEs = #safeEs cla_rules
mengj@17905
    66
	val safeIs = #safeIs cla_rules
mengj@17905
    67
	val hazEs = #hazEs cla_rules
mengj@17905
    68
	val hazIs = #hazIs cla_rules
mengj@17905
    69
    in
mengj@17905
    70
	map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
mengj@17905
    71
    end;
mengj@17905
    72
mengj@17905
    73
mengj@17905
    74
fun get_local_simpR ctxt = 
mengj@17905
    75
    let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
mengj@17905
    76
    in
mengj@17905
    77
	map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
mengj@17905
    78
mengj@17905
    79
mengj@17905
    80
mengj@17905
    81
(***************************************************************)
mengj@17905
    82
(* prover-specific output format:                              *)
mengj@17905
    83
(* TPTP                                                        *)
mengj@17905
    84
(***************************************************************)
mengj@17905
    85
mengj@17905
    86
mengj@17905
    87
mengj@17905
    88
mengj@17905
    89
(***************** TPTP format *********************************)
mengj@17905
    90
mengj@17905
    91
(* 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
    92
mengj@18001
    93
fun mk_conjectures is_fol terms =
mengj@18001
    94
    if is_fol then
mengj@18001
    95
	ListPair.unzip (map ResClause.clause2tptp (ResClause.make_conjecture_clauses terms))
mengj@18001
    96
    else
mengj@18001
    97
	ListPair.unzip (map ResHolClause.clause2tptp (ResHolClause.make_conjecture_clauses terms));
mengj@18001
    98
mengj@18001
    99
mengj@18001
   100
fun tptp_form_g is_fol thms n tfrees =
mengj@18001
   101
    let val terms = map prop_of thms
mengj@18001
   102
	val (tptp_clss,tfree_litss) = mk_conjectures is_fol terms
mengj@17939
   103
	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
mengj@17905
   104
	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
mengj@17905
   105
	val out = TextIO.openOut(probfile)		 	
mengj@17905
   106
    in
mengj@18001
   107
	ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
mengj@17905
   108
	TextIO.closeOut out;
mengj@17905
   109
	warning probfile; (* show the location for debugging *)
mengj@17905
   110
	probfile (* return the location *)
mengj@17905
   111
	
mengj@17905
   112
    end;
mengj@17905
   113
mengj@17905
   114
mengj@18001
   115
val tptp_form = tptp_form_g true;
mengj@18001
   116
val tptp_formH = tptp_form_g false;
mengj@18001
   117
mengj@18001
   118
fun tptp_hyps_g _ [] = ([], [])
mengj@18001
   119
  | tptp_hyps_g is_fol thms =
mengj@18197
   120
    let val prems = ResClause.union_all (map ResAxioms.cnf_axiom_aux thms)
mengj@18197
   121
	val prems' = map prop_of prems
mengj@18197
   122
	val (tptp_clss,tfree_litss) = mk_conjectures is_fol prems'
mengj@17939
   123
	val tfree_lits = ResClause.union_all tfree_litss
mengj@17905
   124
	val tfree_clss = map ResClause.tfree_clause tfree_lits 
mengj@17905
   125
        val hypsfile = File.platform_path hyps_file
mengj@17905
   126
        val out = TextIO.openOut(hypsfile)
mengj@17905
   127
    in
mengj@18001
   128
        ResAtp.writeln_strs out (tfree_clss @ tptp_clss);
mengj@17905
   129
        TextIO.closeOut out; warning hypsfile;
mengj@17905
   130
        ([hypsfile],tfree_lits)
mengj@17905
   131
    end;
mengj@17905
   132
 
mengj@17905
   133
mengj@18001
   134
val tptp_hyps = tptp_hyps_g true;
mengj@18001
   135
val tptp_hypsH = tptp_hyps_g false;
mengj@18001
   136
mengj@18001
   137
fun mk_axioms is_fol rules =
mengj@18001
   138
    if is_fol then 
mengj@18001
   139
	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
mengj@18001
   140
	     val (clss',names) = ListPair.unzip clss
mengj@18001
   141
	     val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
mengj@18001
   142
	 in tptpclss end)
mengj@18001
   143
    else
mengj@18001
   144
	(let val  clss = ResClause.union_all(ResAxioms.clausify_rules_pairsH rules)
mengj@18001
   145
	     val (clss',names) = ListPair.unzip clss
mengj@18001
   146
	     val (tptpclss,_) = ListPair.unzip(map ResHolClause.clause2tptp clss')
mengj@18001
   147
	 in tptpclss end)
mengj@18001
   148
mengj@18001
   149
mengj@17905
   150
mengj@18001
   151
fun write_rules_g is_fol [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
mengj@18001
   152
  | write_rules_g is_fol rules file =
mengj@17905
   153
    let val out = TextIO.openOut(file)
mengj@18001
   154
	val tptpclss = mk_axioms is_fol rules
mengj@17905
   155
    in
mengj@18001
   156
	ResAtp.writeln_strs out tptpclss;
mengj@17905
   157
	TextIO.closeOut out; warning file;
mengj@17905
   158
	[file]
mengj@17905
   159
    end;
mengj@17905
   160
mengj@18001
   161
mengj@18001
   162
val write_rules = write_rules_g true;
mengj@18001
   163
val write_rulesH = write_rules_g false;
mengj@18001
   164
mengj@18086
   165
mengj@17905
   166
mengj@17905
   167
(* TPTP Isabelle theorems *)
mengj@18086
   168
fun tptp_cnf_rules_g write_rules ths (clasetR,simpsetR) =
mengj@17905
   169
    let val simpfile = File.platform_path simpset_file
mengj@17905
   170
	val clafile =  File.platform_path claset_file
mengj@18086
   171
	val local_lemfile = File.platform_path local_lemma_file
mengj@17905
   172
    in
mengj@18086
   173
	(write_rules clasetR clafile) @ (write_rules simpsetR simpfile) @ (write_rules ths local_lemfile)
mengj@17905
   174
    end;
mengj@17905
   175
mengj@18001
   176
val tptp_cnf_rules = tptp_cnf_rules_g write_rules;
mengj@18001
   177
val tptp_cnf_rulesH = tptp_cnf_rules_g write_rulesH;
mengj@18001
   178
mengj@17905
   179
mengj@18086
   180
fun tptp_cnf_clasimp_g tptp_cnf_rules ths ctxt (include_claset,include_simpset) =
mengj@18086
   181
    let val local_claR = if include_claset then get_local_claR ctxt else []
mengj@18086
   182
	val local_simpR = if include_simpset then get_local_simpR ctxt else []
mengj@18086
   183
	val ths_names = map ResAxioms.pairname ths
mengj@17905
   184
    in
mengj@18086
   185
	tptp_cnf_rules ths_names (local_claR,local_simpR)
mengj@17905
   186
    end;
mengj@17905
   187
mengj@17905
   188
mengj@18086
   189
val tptp_cnf_clasimp  = tptp_cnf_clasimp_g tptp_cnf_rules;
mengj@18001
   190
val tptp_cnf_clasimpH = tptp_cnf_clasimp_g tptp_cnf_rulesH;
mengj@18001
   191
mengj@18001
   192
mengj@18001
   193
fun tptp_types_sorts thy = 
mengj@18001
   194
    let val classrel_clauses = ResClause.classrel_clauses_thy thy
mengj@18001
   195
	val arity_clauses = ResClause.arity_clause_thy thy
mengj@18001
   196
	val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
mengj@18001
   197
	val arity_cls = map ResClause.tptp_arity_clause arity_clauses
mengj@18001
   198
	fun write_ts () =
mengj@18001
   199
	    let val tsfile = File.platform_path types_sorts_file
mengj@18001
   200
		val out = TextIO.openOut(tsfile)
mengj@18001
   201
	    in
mengj@18001
   202
		ResAtp.writeln_strs out (classrel_cls @ arity_cls);
mengj@18001
   203
		TextIO.closeOut out;
mengj@18001
   204
		[tsfile]
mengj@18001
   205
	    end
mengj@18001
   206
    in
mengj@18001
   207
	if (List.null arity_cls andalso List.null classrel_cls) then []
mengj@18001
   208
	else
mengj@18001
   209
	    write_ts ()
mengj@18001
   210
    end;
mengj@18001
   211
mengj@18001
   212
mengj@18001
   213
mengj@17905
   214
(*FIXME: a function that does not perform any filtering now *)
mengj@18086
   215
fun find_relevant_ax tptp_cnf_clasimp ths ctxt = tptp_cnf_clasimp ths ctxt (true,true);
mengj@17905
   216
mengj@17905
   217
mengj@17905
   218
(***************************************************************)
mengj@18086
   219
(* setup ATPs as Isabelle methods                              *)
mengj@17905
   220
(***************************************************************)
mengj@18197
   221
fun atp_meth_g helper_file tptp_hyps tptp_cnf_clasimp tac ths ctxt = 
mengj@18086
   222
    let val rules = if !filter_ax then find_relevant_ax tptp_cnf_clasimp ths ctxt 
mengj@18086
   223
		    else tptp_cnf_clasimp ths ctxt (!include_claset, !include_simpset) 
mengj@17905
   224
	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
mengj@18001
   225
	val thy = ProofContext.theory_of ctxt
mengj@18001
   226
	val tsfile = tptp_types_sorts thy
mengj@18197
   227
	val files = (helper_file,hyps @ rules @ tsfile)
mengj@17905
   228
    in
mengj@18086
   229
	Method.SIMPLE_METHOD' HEADGOAL
mengj@18086
   230
	(tac ctxt files tfrees)
mengj@17905
   231
    end;
mengj@18197
   232
fun atp_meth_f tac ths ctxt = atp_meth_g [] tptp_hyps tptp_cnf_clasimp tac ths ctxt;
mengj@18197
   233
fun atp_meth_h tac ths ctxt = 
mengj@18197
   234
    let val helper = if !ResHolClause.keep_types then [typed_comb ()] else [untyped_comb ()]
mengj@18197
   235
    in
mengj@18197
   236
	atp_meth_g helper tptp_hypsH tptp_cnf_clasimpH tac ths ctxt
mengj@18197
   237
    end;
mengj@17905
   238
mengj@17905
   239
mengj@18086
   240
fun atp_meth_G atp_meth tac ths ctxt =
mengj@18086
   241
    let val _  = ResClause.init (ProofContext.theory_of ctxt)
mengj@18086
   242
    in
mengj@18086
   243
	atp_meth tac ths ctxt
mengj@18086
   244
    end;
mengj@18086
   245
fun atp_meth_H tac ths ctxt = atp_meth_G atp_meth_h tac ths ctxt;
mengj@18086
   246
fun atp_meth_F tac ths ctxt = atp_meth_G atp_meth_f tac ths ctxt;
mengj@18001
   247
mengj@18086
   248
mengj@18086
   249
fun atp_method_H tac = Method.thms_ctxt_args (atp_meth_H tac);
mengj@18086
   250
fun atp_method_F tac = Method.thms_ctxt_args (atp_meth_F tac);
mengj@18001
   251
mengj@17905
   252
mengj@17905
   253
mengj@17905
   254
(*************Remove tmp files********************************)
mengj@17905
   255
fun rm_tmp_files1 [] = ()
mengj@17905
   256
  | rm_tmp_files1 (f::fs) =
mengj@17905
   257
    (OS.FileSys.remove f; rm_tmp_files1 fs);
mengj@17905
   258
mengj@17939
   259
fun cond_rm_tmp files = 
mengj@17939
   260
    if !keep_atp_input then warning "ATP input kept..." 
mengj@17939
   261
    else (warning "deleting ATP inputs..."; rm_tmp_files1 files);
mengj@17905
   262
mengj@17905
   263
mengj@17907
   264
end