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