src/HOL/Tools/res_atp.ML
author paulson
Wed Sep 07 18:14:26 2005 +0200 (2005-09-07)
changeset 17306 5cde710a8a23
parent 17305 6cef3aedd661
child 17317 3f12de2e2e6e
permissions -rw-r--r--
Progress on eprover linkup, also massive tidying
paulson@15608
     1
(*  Author: Jia Meng, Cambridge University Computer Laboratory
paulson@15608
     2
    ID: $Id$
paulson@15608
     3
    Copyright 2004 University of Cambridge
paulson@15347
     4
paulson@15347
     5
ATPs with TPTP format input.
paulson@15347
     6
*)
paulson@15452
     7
wenzelm@16802
     8
signature RES_ATP =
wenzelm@16802
     9
sig
wenzelm@16802
    10
  val axiom_file : Path.T
paulson@17306
    11
  val prover: string ref
wenzelm@16802
    12
  val custom_spass: string list ref
quigley@17150
    13
  val hook_count: int ref
paulson@15347
    14
end;
paulson@15347
    15
wenzelm@16802
    16
structure ResAtp: RES_ATP =
paulson@15347
    17
struct
paulson@15347
    18
quigley@17150
    19
quigley@17150
    20
val call_atp = ref false;
quigley@17150
    21
val hook_count = ref 0;
quigley@17150
    22
paulson@16904
    23
fun debug_tac tac = (debug "testing"; tac);
quigley@16478
    24
paulson@17306
    25
val prover = ref "spass";   (* use spass as default prover *)
paulson@17305
    26
val custom_spass =   (*specialized options for SPASS*)
paulson@17305
    27
      ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
paulson@17305
    28
           "-DocProof","-TimeLimit=60"];
paulson@15347
    29
quigley@15644
    30
val axiom_file = File.tmp_path (Path.basic "axioms");
quigley@15644
    31
val hyps_file = File.tmp_path (Path.basic "hyps");
quigley@15644
    32
val prob_file = File.tmp_path (Path.basic "prob");
quigley@15644
    33
wenzelm@16802
    34
paulson@15347
    35
(**** for Isabelle/ML interface  ****)
paulson@15347
    36
paulson@16897
    37
(*Remove unwanted characters such as ? and newline from the textural 
paulson@16897
    38
  representation of a theorem (surely they don't need to be produced in 
paulson@16897
    39
  the first place?) *)
paulson@15608
    40
paulson@16897
    41
fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
paulson@16897
    42
paulson@16897
    43
val proofstring =
paulson@16897
    44
    String.translate (fn c => if is_proof_char c then str c else "");
paulson@15608
    45
paulson@15452
    46
paulson@15347
    47
(**** For running in Isar ****)
paulson@15347
    48
paulson@15608
    49
(* same function as that in res_axioms.ML *)
paulson@15608
    50
fun repeat_RS thm1 thm2 =
paulson@15608
    51
    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
paulson@15608
    52
    in
wenzelm@16802
    53
        if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
paulson@15608
    54
    end;
paulson@15608
    55
paulson@15608
    56
(* a special version of repeat_RS *)
paulson@15608
    57
fun repeat_someI_ex thm = repeat_RS thm someI_ex;
paulson@15608
    58
paulson@16925
    59
quigley@15644
    60
(*********************************************************************)
paulson@15608
    61
(* convert clauses from "assume" to conjecture. write to file "hyps" *)
quigley@15644
    62
(* hypotheses of the goal currently being proved                     *)
quigley@15644
    63
(*********************************************************************)
paulson@17305
    64
(*perhaps have 2 different versions of this, depending on whether or not spass is set *)
paulson@15608
    65
fun isar_atp_h thms =
paulson@15608
    66
    let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
quigley@15644
    67
        val prems' = map repeat_someI_ex prems
quigley@15644
    68
        val prems'' = make_clauses prems'
quigley@15644
    69
        val prems''' = ResAxioms.rm_Eps [] prems''
quigley@15644
    70
        val clss = map ResClause.make_conjecture_clause prems'''
paulson@15774
    71
	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
paulson@15608
    72
	val tfree_lits = ResLib.flat_noDup tfree_litss
quigley@16767
    73
        (* tfree clause is different in tptp and dfg versions *)
paulson@15608
    74
	val tfree_clss = map ResClause.tfree_clause tfree_lits 
wenzelm@16259
    75
        val hypsfile = File.platform_path hyps_file
wenzelm@16802
    76
        val out = TextIO.openOut(hypsfile)
paulson@15608
    77
    in
paulson@16904
    78
        ResLib.writeln_strs out (tfree_clss @ tptp_clss);
paulson@16904
    79
        TextIO.closeOut out; debug hypsfile;
paulson@16904
    80
        tfree_lits
paulson@15608
    81
    end;
paulson@15347
    82
quigley@15644
    83
quigley@15644
    84
(*********************************************************************)
quigley@15644
    85
(* write out a subgoal as tptp clauses to the file "probN"           *)
quigley@15644
    86
(* where N is the number of this subgoal                             *)
quigley@15644
    87
(*********************************************************************)
quigley@15644
    88
paulson@17305
    89
fun tptp_inputs_tfrees thms n tfrees axclauses =
wenzelm@16802
    90
    let
paulson@16904
    91
      val _ = debug ("in tptp_inputs_tfrees 0")
wenzelm@16802
    92
      val clss = map (ResClause.make_conjecture_clause_thm) thms
paulson@16904
    93
      val _ = debug ("in tptp_inputs_tfrees 1")
wenzelm@16802
    94
      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
paulson@16904
    95
      val _ = debug ("in tptp_inputs_tfrees 2")
wenzelm@16802
    96
      val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees)
paulson@16904
    97
      val _ = debug ("in tptp_inputs_tfrees 3")
wenzelm@16802
    98
      val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
wenzelm@16802
    99
      val out = TextIO.openOut(probfile)
paulson@15608
   100
    in
paulson@17305
   101
      ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
wenzelm@16802
   102
      ResLib.writeln_strs out (tfree_clss @ tptp_clss);
wenzelm@16802
   103
      TextIO.closeOut out;
paulson@16904
   104
      debug probfile
paulson@15608
   105
    end;
paulson@15452
   106
paulson@15608
   107
quigley@16767
   108
(*********************************************************************)
quigley@16767
   109
(* write out a subgoal as DFG clauses to the file "probN"           *)
quigley@16767
   110
(* where N is the number of this subgoal                             *)
quigley@16767
   111
(*********************************************************************)
quigley@17150
   112
quigley@17150
   113
fun dfg_inputs_tfrees thms n tfrees axclauses = 
quigley@17150
   114
    let val clss = map (ResClause.make_conjecture_clause_thm) thms
quigley@16767
   115
        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
paulson@17231
   116
        val _ = debug ("about to write out dfg prob file " ^ probfile)
quigley@17150
   117
       	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
quigley@17150
   118
        val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
paulson@17234
   119
        val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
paulson@17231
   120
                        axclauses [] [] [] tfrees   
quigley@16767
   121
	val out = TextIO.openOut(probfile)
quigley@16767
   122
    in
paulson@17234
   123
	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
paulson@17231
   124
(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
quigley@17150
   125
    end;
quigley@17150
   126
quigley@16357
   127
quigley@15644
   128
(*********************************************************************)
paulson@17306
   129
(* call prover with settings and problem file for the current subgoal *)
quigley@15644
   130
(*********************************************************************)
quigley@16357
   131
(* now passing in list of skolemized thms and list of sgterms to go with them *)
wenzelm@16802
   132
fun call_resolve_tac  (thms: thm list list)  sign (sg_terms:  term list) (childin, childout,pid) n  =
wenzelm@16802
   133
  let
wenzelm@16802
   134
    val axfile = (File.platform_path axiom_file)
quigley@16520
   135
quigley@16520
   136
    val hypsfile = (File.platform_path hyps_file)
quigley@16520
   137
wenzelm@16802
   138
    fun make_atp_list [] sign n = []
paulson@16897
   139
      | make_atp_list ((sko_thm, sg_term)::xs) sign n =
wenzelm@16802
   140
          let
paulson@16897
   141
            val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
paulson@16904
   142
            val _ = debug ("thmstring in make_atp_lists is " ^ thmstr)
paulson@15608
   143
paulson@16897
   144
            val goalstring = proofstring (Sign.string_of_term sign sg_term)
paulson@16904
   145
            val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
quigley@16357
   146
paulson@16897
   147
            val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
paulson@16904
   148
            val _ = debug ("prob file in call_resolve_tac is " ^ probfile)
wenzelm@16802
   149
          in
paulson@17306
   150
            if !prover = "spass"
wenzelm@16802
   151
            then
paulson@17306
   152
              let val optionline = 
paulson@17306
   153
		      if !SpassComm.reconstruct 
paulson@17306
   154
		          (*Proof reconstruction works for only a limited set of 
paulson@17306
   155
		            inference rules*)
paulson@17306
   156
                      then "-" ^ space_implode "%-" (!custom_spass)
paulson@17306
   157
                      else "-DocProof%-TimeLimit=60%-SOS" (*Auto mode*)
paulson@16904
   158
                  val _ = debug ("SPASS option string is " ^ optionline)
paulson@16897
   159
                  val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
paulson@16897
   160
                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
paulson@16897
   161
              in 
paulson@16897
   162
                  ([("spass", thmstr, goalstring,
paulson@16897
   163
                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
paulson@17305
   164
                     optionline, axfile, hypsfile, probfile)] @ 
paulson@16897
   165
                  (make_atp_list xs sign (n+1)))
wenzelm@16802
   166
              end
paulson@17306
   167
            else if !prover = "vampire"
quigley@17235
   168
	    then 
wenzelm@16802
   169
              let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
wenzelm@16802
   170
              in
wenzelm@16802
   171
                ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000",
paulson@17305
   172
                   axfile, hypsfile, probfile)] @
wenzelm@16802
   173
                 (make_atp_list xs sign (n+1)))
wenzelm@16802
   174
              end
paulson@17306
   175
      	     else if !prover = "E"
paulson@17306
   176
      	     then
paulson@17306
   177
	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
paulson@17306
   178
	       in
paulson@17306
   179
		  ([("E", thmstr, goalstring, Eprover, 
paulson@17306
   180
		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
paulson@17306
   181
		     axfile, hypsfile, probfile)] @
paulson@17306
   182
		   (make_atp_list xs sign (n+1)))
paulson@17306
   183
	       end
paulson@17306
   184
	     else error ("Invalid prover name: " ^ !prover)
wenzelm@16802
   185
          end
paulson@15452
   186
paulson@16897
   187
    val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
wenzelm@16802
   188
  in
wenzelm@16802
   189
    Watcher.callResProvers(childout,atp_list);
paulson@16904
   190
    debug "Sent commands to watcher!";
paulson@17234
   191
    all_tac
wenzelm@16802
   192
  end
quigley@16357
   193
quigley@15644
   194
(**********************************************************)
quigley@15644
   195
(* write out the current subgoal as a tptp file, probN,   *)
paulson@17234
   196
(* then call all_tac - should be call_res_tac           *)
quigley@15644
   197
(**********************************************************)
quigley@15679
   198
quigley@17150
   199
quigley@17150
   200
fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms axclauses =
quigley@17150
   201
    if n=0 then 
quigley@17150
   202
       (call_resolve_tac  (rev sko_thms)
quigley@17150
   203
        sign  sg_terms (childin, childout, pid) (List.length sg_terms);
paulson@17234
   204
        all_tac thm)
quigley@17150
   205
     else
quigley@17150
   206
	
paulson@17306
   207
      (SELECT_GOAL
paulson@17305
   208
        (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
paulson@17231
   209
          METAHYPS(fn negs => 
paulson@17306
   210
            (if !prover = "spass" 
paulson@17231
   211
             then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
paulson@17305
   212
             else tptp_inputs_tfrees (make_clauses negs) n tfrees axclauses;
paulson@17231
   213
             get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
paulson@17306
   214
                          thm (n-1) (negs::sko_thms) axclauses; 
paulson@17306
   215
             all_tac))]) n thm)
quigley@17150
   216
quigley@15644
   217
quigley@15644
   218
quigley@15644
   219
(**********************************************)
quigley@15644
   220
(* recursively call atp_tac_g on all subgoals *)
quigley@15644
   221
(* sg_term is the nth subgoal as a term - used*)
quigley@15644
   222
(* in proof reconstruction                    *)
quigley@15644
   223
(**********************************************)
quigley@15644
   224
paulson@17306
   225
fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
paulson@17306
   226
  let val tfree_lits = isar_atp_h thms
paulson@17306
   227
      val prems = Thm.prems_of thm
paulson@17306
   228
      val sign = sign_of_thm thm
paulson@17306
   229
      val thmstring = string_of_thm thm
wenzelm@16802
   230
  in
paulson@17306
   231
    debug ("in isar_atp_aux");
paulson@16904
   232
    debug("thmstring in isar_atp_goal': " ^ thmstring);
wenzelm@16802
   233
    (* go and call callResProvers with this subgoal *)
wenzelm@16802
   234
    (* isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; *)
wenzelm@16802
   235
    (* recursive call to pick up the remaining subgoals *)
wenzelm@16802
   236
    (* isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) *)
paulson@17306
   237
    get_sko_thms tfree_lits sign prems (childin, childout, pid) 
paulson@17306
   238
                 thm n_subgoals []  axclauses
wenzelm@16802
   239
  end;
quigley@15644
   240
quigley@15644
   241
(******************************************************************)
quigley@15644
   242
(* called in Isar automatically                                   *)
quigley@15644
   243
(* writes out the current clasimpset to a tptp file               *)
quigley@15644
   244
(* passes all subgoals on to isar_atp_aux for further processing  *)
quigley@15644
   245
(* turns off xsymbol at start of function, restoring it at end    *)
quigley@15644
   246
(******************************************************************)
quigley@15779
   247
(*FIX changed to clasimp_file *)
wenzelm@16802
   248
val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) =>
wenzelm@16802
   249
  if Thm.no_prems thm then ()
wenzelm@16802
   250
  else
wenzelm@16802
   251
    let
paulson@16904
   252
      val _= debug ("in isar_atp'")
wenzelm@16802
   253
      val thy = ProofContext.theory_of ctxt
wenzelm@16802
   254
      val prems = Thm.prems_of thm
wenzelm@16802
   255
      val thms_string = Meson.concat_with_and (map string_of_thm thms)
wenzelm@16802
   256
      val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
wenzelm@16802
   257
wenzelm@16802
   258
      (*set up variables for writing out the clasimps to a tptp file*)
quigley@17150
   259
      val (clause_arr, num_of_clauses, axclauses) =
paulson@17305
   260
        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
paulson@17305
   261
      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^ " clauses")
wenzelm@16802
   262
      val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses)
wenzelm@16802
   263
      val pid_string =
wenzelm@16802
   264
        string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
paulson@15608
   265
    in
paulson@16904
   266
      debug ("initial thms: " ^ thms_string);
paulson@16904
   267
      debug ("subgoals: " ^ prems_string);
paulson@16904
   268
      debug ("pid: "^ pid_string);
quigley@17150
   269
      isar_atp_aux thms thm (length prems) (childin, childout, pid) axclauses;
wenzelm@16802
   270
      ()
wenzelm@16802
   271
    end);
paulson@15608
   272
paulson@15452
   273
paulson@15608
   274
fun get_thms_cs claset =
wenzelm@16802
   275
  let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
wenzelm@16802
   276
  in safeEs @ safeIs @ hazEs @ hazIs end;
quigley@16357
   277
paulson@15608
   278
fun append_name name [] _ = []
wenzelm@16802
   279
  | append_name name (thm :: thms) k =
wenzelm@16802
   280
      Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1);
paulson@15608
   281
wenzelm@16802
   282
fun append_names (name :: names) (thms :: thmss) =
wenzelm@16802
   283
  append_name name thms 0 :: append_names names thmss;
quigley@16357
   284
paulson@15608
   285
fun get_thms_ss [] = []
paulson@15608
   286
  | get_thms_ss thms =
wenzelm@16802
   287
      let
wenzelm@16802
   288
        val names = map Thm.name_of_thm thms
paulson@15608
   289
        val thms' = map (mksimps mksimps_pairs) thms
paulson@15608
   290
        val thms'' = append_names names thms'
wenzelm@16802
   291
      in
wenzelm@16802
   292
        ResLib.flat_noDup thms''
wenzelm@16802
   293
      end;
paulson@15608
   294
paulson@15452
   295
paulson@15608
   296
(* convert locally declared rules to axiom clauses *)
paulson@15608
   297
wenzelm@16802
   298
fun subtract_simpset thy ctxt =
wenzelm@16802
   299
  let
wenzelm@16802
   300
    val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
wenzelm@16802
   301
    val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
wenzelm@16802
   302
  in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end;
quigley@15679
   303
wenzelm@16802
   304
fun subtract_claset thy ctxt =
wenzelm@16802
   305
  let
wenzelm@16802
   306
    val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
wenzelm@16802
   307
    val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
wenzelm@16802
   308
    val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
wenzelm@16802
   309
  in subtract netI1 netI2 @ subtract netE1 netE2 end;
paulson@15608
   310
paulson@15608
   311
quigley@16357
   312
wenzelm@16802
   313
(** the Isar toplevel hook **)
wenzelm@16802
   314
paulson@17091
   315
val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
wenzelm@16802
   316
  let
paulson@17091
   317
    val proof = Toplevel.proof_of state
paulson@17091
   318
    val (ctxt, (_, goal)) = Proof.get_goal proof
paulson@17091
   319
        handle Proof.STATE _ => error "No goal present";
quigley@17150
   320
wenzelm@16802
   321
    val thy = ProofContext.theory_of ctxt;
wenzelm@16802
   322
wenzelm@16802
   323
    (* FIXME presently unused *)
wenzelm@16802
   324
    val ss_thms = subtract_simpset thy ctxt;
wenzelm@16802
   325
    val cs_thms = subtract_claset thy ctxt;
wenzelm@16802
   326
  in
paulson@17091
   327
    debug ("initial thm in isar_atp: " ^ 
paulson@17091
   328
           Pretty.string_of (ProofContext.pretty_thm ctxt goal));
paulson@17091
   329
    debug ("subgoals in isar_atp: " ^ 
paulson@17091
   330
           Pretty.string_of (ProofContext.pretty_term ctxt
paulson@17091
   331
             (Logic.mk_conjunction_list (Thm.prems_of goal))));
paulson@16904
   332
    debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
quigley@17150
   333
    hook_count := !hook_count +1;
quigley@17150
   334
    debug ("in hook for time: " ^(string_of_int (!hook_count)) );
paulson@16925
   335
    ResClause.init thy;
wenzelm@16802
   336
    isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
wenzelm@16802
   337
  end);
quigley@16357
   338
paulson@17091
   339
val call_atpP =
paulson@17091
   340
  OuterSyntax.improper_command 
paulson@17091
   341
    "ProofGeneral.call_atp" 
paulson@17091
   342
    "call automatic theorem provers" 
paulson@17091
   343
    OuterKeyword.diag
paulson@17091
   344
    (Scan.succeed (Toplevel.no_timing o invoke_atp));
paulson@17091
   345
paulson@17091
   346
val _ = OuterSyntax.add_parsers [call_atpP];
paulson@17091
   347
paulson@15347
   348
end;