src/HOL/Tools/res_atp.ML
changeset 16897 7e5319d0f418
parent 16802 6eeee59dac4c
child 16904 6fb188ca5f91
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jul 20 15:57:10 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jul 20 17:00:28 2005 +0200
     1.3 @@ -71,11 +71,14 @@
     1.4  
     1.5  (**** for Isabelle/ML interface  ****)
     1.6  
     1.7 -fun is_proof_char ch =
     1.8 -  (33 <= ord ch andalso ord ch <= 126 andalso ord ch <> 63)
     1.9 -  orelse ch = " ";
    1.10 +(*Remove unwanted characters such as ? and newline from the textural 
    1.11 +  representation of a theorem (surely they don't need to be produced in 
    1.12 +  the first place?) *)
    1.13  
    1.14 -val proofstring = List.filter is_proof_char o explode;
    1.15 +fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
    1.16 +
    1.17 +val proofstring =
    1.18 +    String.translate (fn c => if is_proof_char c then str c else "");
    1.19  
    1.20  
    1.21  (*
    1.22 @@ -174,41 +177,31 @@
    1.23      val clasimpfile = (File.platform_path clasimp_file)
    1.24  
    1.25      fun make_atp_list [] sign n = []
    1.26 -      | make_atp_list ((sko_thm, sg_term)::xs) sign  n =
    1.27 +      | make_atp_list ((sko_thm, sg_term)::xs) sign n =
    1.28            let
    1.29 -            val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm)
    1.30 -            val thmproofstr = proofstring ( skothmstr)
    1.31 -            val no_returns = filter_out (equal "\n") thmproofstr
    1.32 -            val thmstr = implode no_returns
    1.33 -            val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
    1.34 +            val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
    1.35 +            val _ = warning ("thmstring in make_atp_lists is " ^ thmstr)
    1.36  
    1.37 -            val sgstr = Sign.string_of_term sign sg_term
    1.38 -            val goalproofstring = proofstring sgstr
    1.39 -            val no_returns = filter_out (equal "\n") goalproofstring
    1.40 -            val goalstring = implode no_returns
    1.41 -            val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    1.42 +            val goalstring = proofstring (Sign.string_of_term sign sg_term)
    1.43 +            val _ = warning ("goalstring in make_atp_lists is " ^ goalstring)
    1.44  
    1.45 -            val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.46 -
    1.47 -            val _ = (warning ("prob file in cal_res_tac is: "^probfile))
    1.48 +            val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    1.49 +            val _ = warning ("prob file in call_resolve_tac is " ^ probfile)
    1.50            in
    1.51              if !SpassComm.spass
    1.52              then
    1.53 -              let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.54 -              in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.55 -                if !full_spass
    1.56 -                then (*Allow SPASS to run in Auto mode, using all its inference rules*)
    1.57 -                  ([("spass", thmstr, goalstring (*,spass_home*),
    1.58 -
    1.59 -                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),
    1.60 -                     "-DocProof%-TimeLimit=60%-SOS",
    1.61 -                     
    1.62 -                     clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    1.63 -                else (*Restrict SPASS to a small set of rules that we can parse*)
    1.64 -                  ([("spass", thmstr, goalstring (*,spass_home*),
    1.65 -                     getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),
    1.66 -                     ("-" ^ space_implode "%-" (!custom_spass)),
    1.67 -                     clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    1.68 +              let val optionline = (*Custom SPASS options, or default?*)
    1.69 +		      if !full_spass (*Auto mode: all SPASS inference rules*)
    1.70 +                      then "-DocProof%-TimeLimit=60%-SOS"
    1.71 +                      else "-" ^ space_implode "%-" (!custom_spass)
    1.72 +                  val _ = warning ("SPASS option string is " ^ optionline)
    1.73 +                  val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    1.74 +                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
    1.75 +              in 
    1.76 +                  ([("spass", thmstr, goalstring,
    1.77 +                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    1.78 +                     optionline, clasimpfile, axfile, hypsfile, probfile)] @ 
    1.79 +                  (make_atp_list xs sign (n+1)))
    1.80                end
    1.81              else
    1.82                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    1.83 @@ -219,8 +212,7 @@
    1.84                end
    1.85            end
    1.86  
    1.87 -    val thms_goals = ListPair.zip( thms, sg_terms)
    1.88 -    val atp_list = make_atp_list  thms_goals sign 1
    1.89 +    val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
    1.90    in
    1.91      Watcher.callResProvers(childout,atp_list);
    1.92      warning "Sent commands to watcher!";
    1.93 @@ -356,7 +348,7 @@
    1.94          val ax_file = File.platform_path axiom_file
    1.95          val out = TextIO.openOut ax_file
    1.96      in
    1.97 -        (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
    1.98 +        (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is "^ax_file));TextIO.closeOut out)
    1.99      end;
   1.100  *)
   1.101