src/HOL/Tools/res_atp.ML
changeset 17484 f6a225f97f0a
parent 17435 0eed5a1c00c1
child 17488 67376a311a2b
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Sep 19 14:20:45 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Sep 19 15:12:13 2005 +0200
     1.3 @@ -9,24 +9,30 @@
     1.4  sig
     1.5    val prover: string ref
     1.6    val custom_spass: string list ref
     1.7 +  val destdir: string ref
     1.8    val hook_count: int ref
     1.9 +  val problem_name: string ref
    1.10  end;
    1.11  
    1.12  structure ResAtp: RES_ATP =
    1.13  struct
    1.14  
    1.15 -
    1.16  val call_atp = ref false;
    1.17  val hook_count = ref 0;
    1.18  
    1.19 -fun debug_tac tac = (debug "testing"; tac);
    1.20 -
    1.21  val prover = ref "E";   (* use E as the default prover *)
    1.22  val custom_spass =   (*specialized options for SPASS*)
    1.23        ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    1.24             "-DocProof","-TimeLimit=60"];
    1.25  
    1.26 -val prob_file = File.tmp_path (Path.basic "prob");
    1.27 +val destdir = ref "";   (*Empty means write files to /tmp*)
    1.28 +val problem_name = ref "prob";
    1.29 +
    1.30 +fun prob_pathname() = 
    1.31 +  if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    1.32 +  else if File.exists (File.unpack_platform_path (!destdir))
    1.33 +  then !destdir ^ "/" ^ !problem_name
    1.34 +  else error ("No such directory: " ^ !destdir);
    1.35  
    1.36  
    1.37  (**** for Isabelle/ML interface  ****)
    1.38 @@ -68,7 +74,7 @@
    1.39        val _ = debug ("in tptp_inputs_tfrees 2")
    1.40        val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
    1.41        val _ = debug ("in tptp_inputs_tfrees 3")
    1.42 -      val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    1.43 +      val probfile = prob_pathname() ^ "_" ^ string_of_int n
    1.44        val out = TextIO.openOut(probfile)
    1.45      in
    1.46        ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.47 @@ -85,7 +91,7 @@
    1.48  
    1.49  fun dfg_inputs_tfrees thms n axclauses = 
    1.50      let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.51 -        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.52 +        val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
    1.53          val _ = debug ("about to write out dfg prob file " ^ probfile)
    1.54          val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    1.55                          axclauses [] [] []    
    1.56 @@ -108,7 +114,7 @@
    1.57              val goalstring = proofstring (Sign.string_of_term sign sg_term)
    1.58              val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
    1.59  
    1.60 -            val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    1.61 +            val probfile = prob_pathname() ^ "_" ^ string_of_int n
    1.62              val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
    1.63            in
    1.64              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    1.65 @@ -116,7 +122,7 @@
    1.66              if !prover = "spass"
    1.67              then
    1.68                let val optionline = 
    1.69 -		      if !SpassComm.reconstruct 
    1.70 +		      if !AtpCommunication.reconstruct 
    1.71  		          (*Proof reconstruction works for only a limited set of 
    1.72  		            inference rules*)
    1.73                        then "-" ^ space_implode "%-" (!custom_spass)
    1.74 @@ -170,30 +176,31 @@
    1.75          ());
    1.76  
    1.77  
    1.78 +(*FIXME: WHAT IS THMS FOR????*)
    1.79 +
    1.80  (******************************************************************)
    1.81  (* called in Isar automatically                                   *)
    1.82  (* writes out the current clasimpset to a tptp file               *)
    1.83  (* turns off xsymbol at start of function, restoring it at end    *)
    1.84  (******************************************************************)
    1.85  (*FIX changed to clasimp_file *)
    1.86 -val isar_atp' = setmp print_mode [] 
    1.87 +val isar_atp = setmp print_mode [] 
    1.88   (fn (ctxt, thms, thm) =>
    1.89    if Thm.no_prems thm then ()
    1.90    else
    1.91      let
    1.92 -      val _= debug ("in isar_atp'")
    1.93 +      val _= debug ("in isar_atp")
    1.94        val thy = ProofContext.theory_of ctxt
    1.95        val prems = Thm.prems_of thm
    1.96        val thms_string = Meson.concat_with_and (map string_of_thm thms)
    1.97        val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
    1.98  
    1.99        (*set up variables for writing out the clasimps to a tptp file*)
   1.100 -      val (clause_arr, num_of_clauses, axclauses) =
   1.101 -        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   1.102 -      val _ = debug ("claset and simprules total " ^ (string_of_int num_of_clauses)^
   1.103 -                  " clauses")
   1.104 -      val (childin, childout, pid) = 
   1.105 -          Watcher.createWatcher (thm, clause_arr, num_of_clauses)
   1.106 +      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   1.107 +              (*FIXME: hack!! need to consider relevance for all prems*)
   1.108 +      val _ = debug ("claset and simprules total clauses = " ^ 
   1.109 +                     string_of_int (Array.length clause_arr))
   1.110 +      val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
   1.111        val pid_string =
   1.112          string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   1.113      in
   1.114 @@ -205,43 +212,17 @@
   1.115      end);
   1.116  
   1.117  val isar_atp_writeonly = setmp print_mode [] 
   1.118 - (fn (ctxt, thms, thm) =>
   1.119 + (fn (ctxt, thms: thm list, thm) =>
   1.120    if Thm.no_prems thm then ()
   1.121    else
   1.122 -    let
   1.123 -      val thy = ProofContext.theory_of ctxt
   1.124 -      val prems = Thm.prems_of thm
   1.125 -
   1.126 -      (*set up variables for writing out the clasimps to a tptp file*)
   1.127 -      val (clause_arr, num_of_clauses, axclauses) =
   1.128 -        ResClasimp.get_clasimp_lemmas thy (hd prems) (*FIXME: hack!! need to do all prems*)
   1.129 +    let val prems = Thm.prems_of thm
   1.130 +        val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   1.131      in
   1.132        write_problem_files axclauses thm (length prems)
   1.133      end);
   1.134  
   1.135 -fun get_thms_cs claset =
   1.136 -  let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset
   1.137 -  in safeEs @ safeIs @ hazEs @ hazIs end;
   1.138  
   1.139 -fun append_name name [] _ = []
   1.140 -  | append_name name (thm :: thms) k =
   1.141 -      Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1);
   1.142 -
   1.143 -fun append_names (name :: names) (thms :: thmss) =
   1.144 -  append_name name thms 0 :: append_names names thmss;
   1.145 -
   1.146 -fun get_thms_ss [] = []
   1.147 -  | get_thms_ss thms =
   1.148 -      let
   1.149 -        val names = map Thm.name_of_thm thms
   1.150 -        val thms' = map (mksimps mksimps_pairs) thms
   1.151 -        val thms'' = append_names names thms'
   1.152 -      in
   1.153 -        ResLib.flat_noDup thms''
   1.154 -      end;
   1.155 -
   1.156 -
   1.157 -(* convert locally declared rules to axiom clauses *)
   1.158 +(* convert locally declared rules to axiom clauses: UNUSED *)
   1.159  
   1.160  fun subtract_simpset thy ctxt =
   1.161    let
   1.162 @@ -265,12 +246,7 @@
   1.163      val proof = Toplevel.proof_of state
   1.164      val (ctxt, (_, goal)) = Proof.get_goal proof
   1.165          handle Proof.STATE _ => error "No goal present";
   1.166 -
   1.167      val thy = ProofContext.theory_of ctxt;
   1.168 -
   1.169 -    (* FIXME presently unused *)
   1.170 -    val ss_thms = subtract_simpset thy ctxt;
   1.171 -    val cs_thms = subtract_claset thy ctxt;
   1.172    in
   1.173      debug ("initial thm in isar_atp: " ^ 
   1.174             Pretty.string_of (ProofContext.pretty_thm ctxt goal));
   1.175 @@ -278,10 +254,12 @@
   1.176             Pretty.string_of (ProofContext.pretty_term ctxt
   1.177               (Logic.mk_conjunction_list (Thm.prems_of goal))));
   1.178      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
   1.179 +    debug ("current theory: " ^ Context.theory_name thy);
   1.180      hook_count := !hook_count +1;
   1.181      debug ("in hook for time: " ^(string_of_int (!hook_count)) );
   1.182      ResClause.init thy;
   1.183 -    isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
   1.184 +    if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
   1.185 +    else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
   1.186    end);
   1.187  
   1.188  val call_atpP =