src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Fri Apr 15 13:35:53 2005 +0200 (2005-04-15)
changeset 15736 1bb0399a9517
parent 15700 970e0293dfb3
child 15774 9df37a0e935d
permissions -rw-r--r--
more tidying up of the SPASS interface
     1 (* Get claset rules *)
     2 
     3 fun remove_all [] rules = rules
     4 |   remove_all (x::xs) rules = let val rules' = List.filter (not_equal x) rules
     5                               in
     6                                   remove_all xs rules'
     7                               end; 
     8 
     9 fun has_name th = not((Thm.name_of_thm th)= "")
    10 
    11 fun rule_is_fol th = let val tm = prop_of th
    12                      in 
    13                         Term.is_first_order tm
    14                      end
    15 
    16 
    17 fun has_name_pair (a,b) = not_equal a "";
    18 fun good_pair c (a,b) = not_equal b c;
    19 
    20 
    21 
    22 val num_of_clauses = ref 0;
    23 val clause_arr = Array.array(3500, ("empty", 0));
    24 
    25 
    26 
    27 fun multi x 0 xlist = xlist
    28    |multi x n xlist = multi x (n -1 ) (x::xlist);
    29 
    30 
    31 fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
    32                                               val numbers = 0 upto (num_of_cls -1)
    33                                               val multi_name = multi name num_of_cls []
    34                                           in 
    35                                               zip multi_name numbers
    36                                           end;
    37 
    38 fun stick []  = []
    39 |   stick (x::xs)  = x@(stick xs )
    40 
    41 
    42 
    43 fun fill_cls_array array n [] = ()
    44 |   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
    45                                      in
    46                                         fill_cls_array array (n+1) (xs)
    47                                      end;
    48 
    49 
    50    	      	    
    51 val nc = ref (Symtab.empty : (thm list) Symtab.table)
    52 
    53  
    54 
    55 fun memo_add_clauses (name:string, cls)=
    56                         nc := Symtab.update((name , cls), !nc);
    57       	       
    58 
    59 
    60 fun memo_find_clause name = case Symtab.lookup (!nc,name) of
    61       	        NONE =>  []
    62                 |SOME cls  => cls ;
    63       	        	
    64 
    65 
    66 
    67 fun not_second c (a,b)  = not_equal b c;
    68 
    69 fun remove_all_simps [] name_rule_list:(string*thm) list = name_rule_list
    70 |   remove_all_simps ((x:thm)::xs) (name_rule_list:(string*thm) list) = 
    71                               let val name_rules' = List.filter (not_second  x) name_rule_list
    72                               in
    73                                   remove_all_simps xs name_rules'
    74                               end; 
    75 
    76 
    77 
    78 fun thm_is_fol (x, thm) = rule_is_fol thm
    79 
    80 
    81 fun get_simp_metas [] = [[]]
    82 |   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
    83                              in
    84                                  metas::(get_simp_metas xs)
    85                              end
    86                              handle THM _ => get_simp_metas xs
    87 
    88 
    89 (* re-jig all these later as smaller functions for each bit *)
    90   val num_of_clauses = ref 0;
    91 val clause_arr = Array.array(3500, ("empty", 0));
    92                                
    93 
    94 fun write_out_clasimp filename = let 
    95                                    (****************************************)
    96                                    (* add claset rules to array and write out as strings *)
    97                                    (****************************************)
    98                                    val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
    99                                    val claset = ResAxioms.clausify_classical_rules_thy (the_context())
   100                                    val (claset_clauses,badthms) =  claset;
   101                                    val clausifiable_rules = remove_all badthms claset_rules;
   102                                    val named_claset = List.filter has_name clausifiable_rules;
   103                                    val name_fol_cs = List.filter rule_is_fol  named_claset;
   104                                    (* length name_fol_cs is 93 *)
   105                                    val good_names = map Thm.name_of_thm name_fol_cs;
   106  
   107                                    (*******************************************)
   108                                     (* get (name, thm) pairs for claset rules *)
   109                                    (*******************************************)
   110 
   111                                    val names_rules = zip good_names name_fol_cs;
   112                                    
   113                                    val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
   114 
   115                                    val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
   116 
   117                                    (* list of lists of tptp string clauses *)
   118                                    val stick_clasrls =  map stick claset_tptp_strs;
   119                                    (* stick stick_clasrls length is 172*)
   120 
   121                                    val name_stick = zip good_names stick_clasrls;
   122 
   123                                    val cl_name_nums =map clause_numbering name_stick;
   124                                        
   125                                    val cl_long_name_nums = stick cl_name_nums;
   126                                    (*******************************************)
   127                                   (* create array and put clausename, number pairs into it *)
   128                                    (*******************************************)
   129 
   130                                         val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   131                                  
   132 
   133                                    val _= num_of_clauses := (List.length cl_long_name_nums);
   134                                    
   135                                    (*************************************)
   136                                    (* write claset out as tptp file      *)
   137                                     (*************************************)
   138                                   
   139                                     val claset_all_strs = stick stick_clasrls;
   140                                     val out = TextIO.openOut filename;
   141                                     val _=   ResLib.writeln_strs out claset_all_strs;
   142                                     val _= TextIO.flushOut out;
   143                                     val _=  TextIO.output (out,("\n \n"));
   144                                     val _= TextIO.flushOut out;
   145                                    (*val _= TextIO.closeOut out;*)
   146 
   147                                   (*********************)
   148                                   (* Get simpset rules *)
   149                                   (*********************)
   150                                   val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
   151                                   val named_simps = List.filter has_name_pair simpset_name_rules;
   152 
   153                                   val simp_names = map #1 named_simps;
   154                                   val simp_rules = map #2 named_simps;
   155                               
   156                                   val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
   157                                  (* 1137 clausif simps *)
   158                                   val clausifiable_simps = remove_all_simps badthms named_simps;
   159                                    
   160                                     val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
   161                                     val simp_names = map #1 name_fol_simps;
   162                                     val simp_rules = map #2 name_fol_simps;
   163                                     
   164                                      (* 995 of these *)
   165                                     (* need to get names of claset_cluases so we can make sure we've*)
   166                                     (* got the same ones (ie. the named ones ) as the claset rules *)
   167                                     (* length 1374*)
   168                                     val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
   169                                     val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
   170 
   171                                     val stick_strs = map stick simpset_tptp_strs;
   172                                     val name_stick = zip simp_names stick_strs;
   173 
   174                                     val name_nums =map clause_numbering name_stick;
   175                                     (* length 2409*)
   176                                     val long_name_nums = stick name_nums;
   177 
   178 
   179                                     val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
   180                                     val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
   181 
   182 
   183 
   184                                     val tptplist =  (stick stick_strs) 
   185 
   186 
   187                               in 
   188                                    ResLib.writeln_strs out tptplist;
   189                                    TextIO.flushOut out;
   190                                    TextIO.closeOut out
   191                               end;
   192 
   193 (*
   194 
   195  Array.sub(clause_arr,  2310);
   196 *)