more tidying up of the SPASS interface
authorpaulson
Fri Apr 15 13:35:53 2005 +0200 (2005-04-15)
changeset 157361bb0399a9517
parent 15735 953f188e16c6
child 15737 c7e522520910
more tidying up of the SPASS interface
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 15 12:00:00 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Apr 15 13:35:53 2005 +0200
     1.3 @@ -214,7 +214,6 @@
     1.4  val rev_ssubst = rotate_prems 1 ssubst;
     1.5  
     1.6  
     1.7 -(* have changed from negate_nead to negate_head.  God knows if this will actually work *)
     1.8  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
     1.9                            let 
    1.10                              val th1 =  Recon_Base.assoc clause1 thml
    1.11 @@ -403,14 +402,11 @@
    1.12  
    1.13  fun not_newline ch = not (ch = "\n");
    1.14  
    1.15 -fun concat_with_and [] str = str
    1.16 -|   concat_with_and (x::[]) str = str^"("^x^")"
    1.17 -|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    1.18  (*
    1.19  
    1.20  fun follow clauses [] allvars thml recons = 
    1.21                               let (* val _ = reset show_sorts*)
    1.22 -                              val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
    1.23 +                              val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
    1.24                                val thmproofstring = proofstring ( thmstring)
    1.25                              val no_returns =List.filter  not_newline ( thmproofstring)
    1.26                              val thmstr = implode no_returns
     2.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 15 12:00:00 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Fri Apr 15 13:35:53 2005 +0200
     2.3 @@ -62,20 +62,6 @@
     2.4                  |SOME cls  => cls ;
     2.5        	        	
     2.6  
     2.7 -fun retr_thms ([]:MetaSimplifier.rrule list) = []
     2.8 -	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
     2.9 -
    2.10 -fun snds [] = []
    2.11 -   | snds ((x,y)::l) = y::(snds l);
    2.12 -
    2.13 -fun simpset_rules_of_thy thy =
    2.14 -     let val simpset = simpset_of thy
    2.15 -	val rules = #rules(fst (rep_ss simpset))
    2.16 -	val thms = retr_thms (snds(Net.dest rules))
    2.17 -     in	thms  end;
    2.18 -
    2.19 -
    2.20 -
    2.21  
    2.22  
    2.23  fun not_second c (a,b)  = not_equal b c;
    2.24 @@ -124,7 +110,7 @@
    2.25  
    2.26                                     val names_rules = zip good_names name_fol_cs;
    2.27                                     
    2.28 -                                   val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
    2.29 +                                   val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
    2.30  
    2.31                                     val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
    2.32  
    2.33 @@ -161,25 +147,25 @@
    2.34                                    (*********************)
    2.35                                    (* Get simpset rules *)
    2.36                                    (*********************)
    2.37 -                                  val (simpset_name_rules) =simpset_rules_of_thy (the_context());
    2.38 +                                  val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
    2.39                                    val named_simps = List.filter has_name_pair simpset_name_rules;
    2.40  
    2.41 -                                  val simp_names = map fst named_simps;
    2.42 -                                  val simp_rules = map snd named_simps;
    2.43 +                                  val simp_names = map #1 named_simps;
    2.44 +                                  val simp_rules = map #2 named_simps;
    2.45                                
    2.46                                    val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
    2.47                                   (* 1137 clausif simps *)
    2.48                                    val clausifiable_simps = remove_all_simps badthms named_simps;
    2.49                                     
    2.50                                      val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
    2.51 -                                    val simp_names = map fst name_fol_simps;
    2.52 -                                    val simp_rules = map snd name_fol_simps;
    2.53 +                                    val simp_names = map #1 name_fol_simps;
    2.54 +                                    val simp_rules = map #2 name_fol_simps;
    2.55                                      
    2.56                                       (* 995 of these *)
    2.57                                      (* need to get names of claset_cluases so we can make sure we've*)
    2.58                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    2.59                                      (* length 1374*)
    2.60 -                                    val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
    2.61 +                                    val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
    2.62                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    2.63  
    2.64                                      val stick_strs = map stick simpset_tptp_strs;
     3.1 --- a/src/HOL/Tools/meson.ML	Fri Apr 15 12:00:00 2005 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Fri Apr 15 13:35:53 2005 +0200
     3.3 @@ -84,12 +84,10 @@
     3.4  	| has _ = false
     3.5    in  has  end;
     3.6  
     3.7 -(* for tracing statements *)
     3.8 - 
     3.9 -fun concat_with_and [] str = str
    3.10 -|   concat_with_and (x::[]) str = str^" ("^x^")"
    3.11 -|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    3.12 -
    3.13 +(* for tracing: encloses each string element in brackets. *)
    3.14 +fun concat_with_and [] = ""
    3.15 +  | concat_with_and [x] = "(" ^ x ^ ")"
    3.16 +  | concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs;
    3.17  
    3.18  
    3.19  (**** Clause handling ****)
    3.20 @@ -326,7 +324,8 @@
    3.21  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    3.22    The resulting clauses are HOL disjunctions.*)
    3.23  fun make_clauses ths =
    3.24 -   ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    3.25 +   (warning("in make_clauses ths = " ^ concat_with_and (map string_of_thm ths)); 
    3.26 +    sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
    3.27  
    3.28  (*Convert a list of clauses to (contrapositive) Horn clauses*)
    3.29  fun make_horns ths =
     4.1 --- a/src/HOL/Tools/res_atp.ML	Fri Apr 15 12:00:00 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Apr 15 13:35:53 2005 +0200
     4.3 @@ -64,12 +64,6 @@
     4.4  val dummy_tac = PRIMITIVE(fn thm => thm );
     4.5  
     4.6   
     4.7 -fun concat_with_and [] str = str
     4.8 -|   concat_with_and (x::[]) str = str^" ("^x^")"
     4.9 -|   concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
    4.10 -
    4.11 -
    4.12 -
    4.13  (**** for Isabelle/ML interface  ****)
    4.14  
    4.15  fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
    4.16 @@ -147,7 +141,7 @@
    4.17  (*********************************************************************)
    4.18  
    4.19  fun call_resolve_tac sign thms sg_term (childin, childout,pid) n  = let
    4.20 -                             val thmstring = concat_with_and (map string_of_thm thms) ""
    4.21 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    4.22                               val thm_no = length thms
    4.23                               val _ = warning ("number of thms is : "^(string_of_int thm_no))
    4.24                               val _ = warning ("thmstring in call_res is: "^thmstring)
    4.25 @@ -163,7 +157,7 @@
    4.26                               val clauses = make_clauses thms
    4.27                               val _ =( warning ("called make_clauses "))*)
    4.28                               (*val _ = tptp_inputs clauses prob_file*)
    4.29 -                             val thmstring = concat_with_and (map string_of_thm thms) ""
    4.30 +                             val thmstring = Meson.concat_with_and (map string_of_thm thms)
    4.31                             
    4.32                               val goalstr = Sign.string_of_term sign sg_term 
    4.33                               val goalproofstring = proofstring goalstr
    4.34 @@ -227,7 +221,8 @@
    4.35  (* dummy tac vs.  Doesn't call resolve_tac *)
    4.36  
    4.37  fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = 
    4.38 -                                         ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) ""));
    4.39 +                                         ( warning("ths for tptp: " ^ 
    4.40 +                                                   Meson.concat_with_and (map string_of_thm thms));
    4.41                                             warning("in call_atp_tac_tfrees");
    4.42                                             
    4.43                                             tptp_inputs_tfrees (make_clauses thms) n tfrees;
    4.44 @@ -243,7 +238,7 @@
    4.45  SELECT_GOAL
    4.46    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    4.47    METAHYPS(fn negs => (warning("calling  call_atp_tac_tfrees with negs"
    4.48 -                               ^ (concat_with_and (map string_of_thm negs) ""));
    4.49 +                               ^ Meson.concat_with_and (map string_of_thm negs));
    4.50             call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
    4.51  end;
    4.52  
    4.53 @@ -305,9 +300,9 @@
    4.54          val _= (warning ("in isar_atp'"))
    4.55          val prems = prems_of thm
    4.56          val sign = sign_of_thm thm
    4.57 -        val thms_string =concat_with_and (map  string_of_thm thms) ""
    4.58 +        val thms_string = Meson.concat_with_and (map string_of_thm thms)
    4.59          val thmstring = string_of_thm thm
    4.60 -        val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
    4.61 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems)
    4.62          (* set up variables for writing out the clasimps to a tptp file *)
    4.63          val _ = write_out_clasimp (File.sysify_path axiom_file)
    4.64          (* cq: add write out clasimps to file *)
    4.65 @@ -397,9 +392,8 @@
    4.66          val sg_prems = prems_of thm
    4.67          val sign = sign_of_thm thm
    4.68          val prem_no = length sg_prems
    4.69 -        val prems_string =  concat_with_and (map (Sign.string_of_term sign) sg_prems) ""
    4.70 +        val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems)
    4.71      in
    4.72 -         
    4.73            (warning ("initial thm in isar_atp: "^thmstring));
    4.74            (warning ("subgoals in isar_atp: "^prems_string));
    4.75      	   (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
     5.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Apr 15 12:00:00 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Apr 15 13:35:53 2005 +0200
     5.3 @@ -229,7 +229,7 @@
     5.4  val rm_Eps 
     5.5  : (Term.term * Term.term) list -> Thm.thm list -> Term.term list
     5.6  val claset_rules_of_thy : Theory.theory -> Thm.thm list
     5.7 -val simpset_rules_of_thy : Theory.theory -> Thm.thm list
     5.8 +val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list
     5.9  val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
    5.10  val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
    5.11  
    5.12 @@ -391,17 +391,8 @@
    5.13  (******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
    5.14  
    5.15  
    5.16 -local
    5.17 -
    5.18  fun retr_thms ([]:MetaSimplifier.rrule list) = []
    5.19 -	  | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
    5.20 -
    5.21 -
    5.22 -fun snds [] = []
    5.23 -  |   snds ((x,y)::l) = y::(snds l);
    5.24 -
    5.25 -in
    5.26 -
    5.27 +	  | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
    5.28  
    5.29  fun claset_rules_of_thy thy =
    5.30      let val clsset = rep_cs (claset_of thy)
    5.31 @@ -416,13 +407,11 @@
    5.32  fun simpset_rules_of_thy thy =
    5.33      let val simpset = simpset_of thy
    5.34  	val rules = #rules(fst (rep_ss simpset))
    5.35 -	val thms = retr_thms (snds(Net.dest rules))
    5.36 +	val thms = retr_thms (map #2 (Net.dest rules))
    5.37      in
    5.38  	thms
    5.39      end;
    5.40  
    5.41 -end;
    5.42 -
    5.43  
    5.44  (**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
    5.45  
    5.46 @@ -455,7 +444,7 @@
    5.47  
    5.48  (* CNF all simplifier rules from a given theory's simpset *)
    5.49  fun cnf_simpset_rules_thy thy =
    5.50 -    let val thms = simpset_rules_of_thy thy
    5.51 +    let val thms = map #2 (simpset_rules_of_thy thy)
    5.52      in
    5.53  	cnf_simpset_rules thms []
    5.54      end;
    5.55 @@ -474,7 +463,7 @@
    5.56  
    5.57  
    5.58  
    5.59 -(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
    5.60 +(* convert all classical rules from a given theory into Clause.clause format. *)
    5.61  fun clausify_classical_rules_thy thy =
    5.62      let val rules = claset_rules_of_thy thy
    5.63      in
    5.64 @@ -491,9 +480,9 @@
    5.65      end;
    5.66  
    5.67  
    5.68 -(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
    5.69 +(* convert all simplifier rules from a given theory into Clause.clause format. *)
    5.70  fun clausify_simpset_rules_thy thy =
    5.71 -    let val thms = simpset_rules_of_thy thy
    5.72 +    let val thms = map #2 (simpset_rules_of_thy thy)
    5.73      in
    5.74  	clausify_simpset_rules thms []
    5.75      end;