code streamlining
authorpaulson
Wed Jul 20 17:00:28 2005 +0200 (2005-07-20)
changeset 168977e5319d0f418
parent 16896 db2defb39f4c
child 16898 543ee8fabe1a
code streamlining
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 20 15:57:10 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Jul 20 17:00:28 2005 +0200
     1.3 @@ -185,7 +185,6 @@
     1.4                ReduceAxiomsN.relevant_filter (!relevant) goal 
     1.5                  (ResAxioms.claset_rules_of_thy thy);
     1.6  	val named_claset = List.filter has_name_pair claset_rules;
     1.7 -	val claset_names = map remove_spaces_pair (named_claset)
     1.8  	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
     1.9  
    1.10  	val simpset_rules =
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Jul 20 15:57:10 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Jul 20 17:00:28 2005 +0200
     2.3 @@ -71,11 +71,14 @@
     2.4  
     2.5  (**** for Isabelle/ML interface  ****)
     2.6  
     2.7 -fun is_proof_char ch =
     2.8 -  (33 <= ord ch andalso ord ch <= 126 andalso ord ch <> 63)
     2.9 -  orelse ch = " ";
    2.10 +(*Remove unwanted characters such as ? and newline from the textural 
    2.11 +  representation of a theorem (surely they don't need to be produced in 
    2.12 +  the first place?) *)
    2.13  
    2.14 -val proofstring = List.filter is_proof_char o explode;
    2.15 +fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
    2.16 +
    2.17 +val proofstring =
    2.18 +    String.translate (fn c => if is_proof_char c then str c else "");
    2.19  
    2.20  
    2.21  (*
    2.22 @@ -174,41 +177,31 @@
    2.23      val clasimpfile = (File.platform_path clasimp_file)
    2.24  
    2.25      fun make_atp_list [] sign n = []
    2.26 -      | make_atp_list ((sko_thm, sg_term)::xs) sign  n =
    2.27 +      | make_atp_list ((sko_thm, sg_term)::xs) sign n =
    2.28            let
    2.29 -            val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm)
    2.30 -            val thmproofstr = proofstring ( skothmstr)
    2.31 -            val no_returns = filter_out (equal "\n") thmproofstr
    2.32 -            val thmstr = implode no_returns
    2.33 -            val _ = warning ("thmstring in make_atp_lists is: "^thmstr)
    2.34 +            val thmstr = proofstring (Meson.concat_with_and (map string_of_thm sko_thm))
    2.35 +            val _ = warning ("thmstring in make_atp_lists is " ^ thmstr)
    2.36  
    2.37 -            val sgstr = Sign.string_of_term sign sg_term
    2.38 -            val goalproofstring = proofstring sgstr
    2.39 -            val no_returns = filter_out (equal "\n") goalproofstring
    2.40 -            val goalstring = implode no_returns
    2.41 -            val _ = warning ("goalstring in make_atp_lists is: "^goalstring)
    2.42 +            val goalstring = proofstring (Sign.string_of_term sign sg_term)
    2.43 +            val _ = warning ("goalstring in make_atp_lists is " ^ goalstring)
    2.44  
    2.45 -            val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    2.46 -
    2.47 -            val _ = (warning ("prob file in cal_res_tac is: "^probfile))
    2.48 +            val probfile = File.platform_path prob_file ^ "_" ^ (string_of_int n)
    2.49 +            val _ = warning ("prob file in call_resolve_tac is " ^ probfile)
    2.50            in
    2.51              if !SpassComm.spass
    2.52              then
    2.53 -              let val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    2.54 -              in  (*We've checked that SPASS is there for ATP/spassshell to run.*)
    2.55 -                if !full_spass
    2.56 -                then (*Allow SPASS to run in Auto mode, using all its inference rules*)
    2.57 -                  ([("spass", thmstr, goalstring (*,spass_home*),
    2.58 -
    2.59 -                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*),
    2.60 -                     "-DocProof%-TimeLimit=60%-SOS",
    2.61 -                     
    2.62 -                     clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    2.63 -                else (*Restrict SPASS to a small set of rules that we can parse*)
    2.64 -                  ([("spass", thmstr, goalstring (*,spass_home*),
    2.65 -                     getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*),
    2.66 -                     ("-" ^ space_implode "%-" (!custom_spass)),
    2.67 -                     clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1)))
    2.68 +              let val optionline = (*Custom SPASS options, or default?*)
    2.69 +		      if !full_spass (*Auto mode: all SPASS inference rules*)
    2.70 +                      then "-DocProof%-TimeLimit=60%-SOS"
    2.71 +                      else "-" ^ space_implode "%-" (!custom_spass)
    2.72 +                  val _ = warning ("SPASS option string is " ^ optionline)
    2.73 +                  val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    2.74 +                    (*We've checked that SPASS is there for ATP/spassshell to run.*)
    2.75 +              in 
    2.76 +                  ([("spass", thmstr, goalstring,
    2.77 +                     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    2.78 +                     optionline, clasimpfile, axfile, hypsfile, probfile)] @ 
    2.79 +                  (make_atp_list xs sign (n+1)))
    2.80                end
    2.81              else
    2.82                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel"
    2.83 @@ -219,8 +212,7 @@
    2.84                end
    2.85            end
    2.86  
    2.87 -    val thms_goals = ListPair.zip( thms, sg_terms)
    2.88 -    val atp_list = make_atp_list  thms_goals sign 1
    2.89 +    val atp_list = make_atp_list (ListPair.zip (thms, sg_terms)) sign 1
    2.90    in
    2.91      Watcher.callResProvers(childout,atp_list);
    2.92      warning "Sent commands to watcher!";
    2.93 @@ -356,7 +348,7 @@
    2.94          val ax_file = File.platform_path axiom_file
    2.95          val out = TextIO.openOut ax_file
    2.96      in
    2.97 -        (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
    2.98 +        (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is "^ax_file));TextIO.closeOut out)
    2.99      end;
   2.100  *)
   2.101  
     3.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Jul 20 15:57:10 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Jul 20 17:00:28 2005 +0200
     3.3 @@ -16,11 +16,6 @@
     3.4    val meta_cnf_axiom : thm -> thm list
     3.5    val cnf_rule : thm -> thm list
     3.6    val cnf_rules : (string*thm) list -> thm list -> thm list list * thm list
     3.7 -
     3.8 -  val cnf_classical_rules_thy : theory -> thm list list * thm list
     3.9 - 
    3.10 -  val cnf_simpset_rules_thy : theory -> thm list list * thm list
    3.11 - 
    3.12    val rm_Eps : (term * term) list -> thm list -> term list
    3.13    val claset_rules_of_thy : theory -> (string * thm) list
    3.14    val simpset_rules_of_thy : theory -> (string * thm) list
    3.15 @@ -378,14 +373,6 @@
    3.16        let val (ts,es) = cnf_rules thms err_list
    3.17        in  (cnf_axiom (name,th) :: ts,es) handle  _ => (ts, (th::es))  end;
    3.18  
    3.19 -(* CNF all rules from a given theory's classical reasoner *)
    3.20 -fun cnf_classical_rules_thy thy = 
    3.21 -    cnf_rules (claset_rules_of_thy thy) [];
    3.22 -
    3.23 -(* CNF all simplifier rules from a given theory's simpset *)
    3.24 -fun cnf_simpset_rules_thy thy =
    3.25 -    cnf_rules (simpset_rules_of_thy thy) [];
    3.26 -
    3.27  
    3.28  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
    3.29  
    3.30 @@ -395,18 +382,20 @@
    3.31          val isa_clauses' = rm_Eps [] isa_clauses
    3.32          val clauses_n = length isa_clauses
    3.33  	fun make_axiom_clauses _ [] []= []
    3.34 -	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
    3.35 +	  | make_axiom_clauses i (cls::clss) (cls'::clss') =
    3.36 +	      (ResClause.make_axiom_clause cls (thm_name,i), cls') :: 
    3.37 +	      make_axiom_clauses (i+1) clss clss'
    3.38      in
    3.39  	make_axiom_clauses 0 isa_clauses' isa_clauses		
    3.40      end;
    3.41  
    3.42  fun clausify_rules_pairs [] err_list = ([],err_list)
    3.43    | clausify_rules_pairs ((name,thm)::thms) err_list =
    3.44 -    let val (ts,es) = clausify_rules_pairs thms err_list
    3.45 -    in
    3.46 -	((clausify_axiom_pairs (name,thm))::ts,es) handle  _ => (ts,(thm::es))
    3.47 -    end;
    3.48 -(* classical rules *)
    3.49 +      let val (ts,es) = clausify_rules_pairs thms err_list
    3.50 +      in
    3.51 +	  ((clausify_axiom_pairs (name,thm))::ts, es) 
    3.52 +	  handle  _ => (ts, (thm::es))
    3.53 +      end;
    3.54  
    3.55  
    3.56  (*Setup function: takes a theory and installs ALL simprules and claset rules