src/HOL/Tools/ATP/recon_order_clauses.ML
author paulson
Fri Apr 15 18:16:05 2005 +0200 (2005-04-15)
changeset 15739 bb2acfed8212
parent 15702 2677db44c795
child 15774 9df37a0e935d
permissions -rw-r--r--
yet more tidying up: removal of some references to Main
quigley@15642
     1
(*----------------------------------------------*)
quigley@15642
     2
(* Reorder clauses for use in binary resolution *)
quigley@15642
     3
(*----------------------------------------------*)
quigley@15642
     4
quigley@15642
     5
fun drop n [] = []
quigley@15642
     6
|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
quigley@15642
     7
quigley@15642
     8
fun remove_nth n [] = []
paulson@15697
     9
|   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
quigley@15642
    10
quigley@15642
    11
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
quigley@15642
    12
quigley@15642
    13
quigley@15642
    14
exception Not_in_list;  
quigley@15642
    15
quigley@15642
    16
quigley@15642
    17
fun zip xs [] = []
quigley@15642
    18
|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
quigley@15642
    19
quigley@15642
    20
quigley@15642
    21
fun unzip [] = ([],[])
quigley@15642
    22
    | unzip((x,y)::pairs) =
quigley@15642
    23
	  let val (xs,ys) = unzip pairs
quigley@15642
    24
	  in  (x::xs, y::ys)  end;
quigley@15642
    25
quigley@15642
    26
fun numlist 0 = []
quigley@15642
    27
|   numlist n = (numlist (n - 1))@[n]
quigley@15642
    28
quigley@15642
    29
quigley@15642
    30
quigley@15642
    31
quigley@15642
    32
fun last(x::xs) = if xs=[] then x else last xs
quigley@15642
    33
fun butlast []= []
quigley@15642
    34
|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
quigley@15642
    35
quigley@15642
    36
quigley@15642
    37
fun minus a b = b - a;
quigley@15642
    38
quigley@15642
    39
quigley@15642
    40
(* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
quigley@15642
    41
paulson@15684
    42
fun assoc3 a [] = raise Recon_Base.Noassoc
quigley@15642
    43
  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
quigley@15642
    44
quigley@15642
    45
quigley@15642
    46
fun third (a,b,c) = c;
quigley@15642
    47
quigley@15642
    48
quigley@15642
    49
 fun takeUntil ch [] res  = (res, [])
quigley@15642
    50
 |   takeUntil ch (x::xs) res = if   x = ch 
quigley@15642
    51
                                then
quigley@15642
    52
                                     (res, xs)
quigley@15642
    53
                                else
quigley@15642
    54
                                     takeUntil ch xs (res@[x])
quigley@15642
    55
fun contains_eq str = inlist "=" str 
quigley@15642
    56
quigley@15642
    57
fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
quigley@15642
    58
                     in
quigley@15642
    59
                        if ((last uptoeq) = "~")
quigley@15642
    60
                        then 
quigley@15642
    61
                            false
quigley@15642
    62
                        else
quigley@15642
    63
                            true
quigley@15642
    64
                     end
quigley@15642
    65
                   
quigley@15642
    66
quigley@15642
    67
quigley@15642
    68
quigley@15642
    69
fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
quigley@15642
    70
                       then 
quigley@15642
    71
                           let val (left, right) = takeUntil "=" str []
quigley@15642
    72
                           in
quigley@15642
    73
                               ((butlast left), (drop 1 right))
quigley@15642
    74
                           end
quigley@15642
    75
                       else                  (* is an inequality *)
quigley@15642
    76
                           let val (left, right) = takeUntil "~" str []
quigley@15642
    77
                           in 
quigley@15642
    78
                              ((butlast left), (drop 2 right))
quigley@15642
    79
                           end
quigley@15642
    80
                
quigley@15642
    81
quigley@15642
    82
quigley@15642
    83
fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
quigley@15642
    84
                           val (x_lhs, x_rhs) = get_eq_strs x
quigley@15642
    85
quigley@15642
    86
                       in
quigley@15642
    87
                           (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
quigley@15642
    88
                       end
quigley@15642
    89
quigley@15642
    90
fun equal_pair (a,b) = equal a b
quigley@15642
    91
quigley@15642
    92
fun is_var_pair (a,b) vars = (a mem vars) andalso (b mem vars)
quigley@15642
    93
quigley@15642
    94
fun var_equiv vars (a,b)  = (equal_pair (a,b)) orelse (is_var_pair (a,b) vars)
quigley@15642
    95
quigley@15642
    96
fun all_true [] = false
quigley@15642
    97
|   all_true xs = let val falselist = List.filter (equal false ) xs 
quigley@15642
    98
                  in
quigley@15642
    99
                      falselist = []
quigley@15642
   100
                  end
quigley@15642
   101
quigley@15642
   102
quigley@15642
   103
quigley@15642
   104
fun var_pos_eq vars x y = let val xs = explode x
quigley@15642
   105
                              val ys = explode y
quigley@15642
   106
                          in
quigley@15642
   107
                              if not_equal (length xs) (length ys)
quigley@15642
   108
                              then 
quigley@15642
   109
                                  false
quigley@15642
   110
                              else
quigley@15642
   111
                                  let val xsys = zip xs ys
quigley@15642
   112
                                      val are_var_pairs = map (var_equiv vars) xsys
quigley@15642
   113
                                  in
quigley@15642
   114
                                      all_true are_var_pairs 
quigley@15642
   115
                                  end
quigley@15642
   116
                          end
quigley@15642
   117
quigley@15642
   118
quigley@15642
   119
quigley@15642
   120
quigley@15642
   121
fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
quigley@15642
   122
    |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
quigley@15642
   123
                                 let val y = explode x 
quigley@15642
   124
                                     val b = explode a
quigley@15642
   125
                                 in
quigley@15642
   126
                                    if  b = y
quigley@15642
   127
                                    then 
quigley@15642
   128
                                         (pos_num, symlist, nsymlist)
quigley@15642
   129
                                    else 
quigley@15642
   130
                                         if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
quigley@15642
   131
                                         then 
quigley@15642
   132
                                             (pos_num, symlist, nsymlist)
quigley@15642
   133
                                         else 
quigley@15642
   134
                                             if (contains_eq b) andalso (contains_eq y)
quigley@15642
   135
                                             then 
quigley@15642
   136
                                                 if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
quigley@15642
   137
                                                 then 
quigley@15642
   138
                                                     (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
quigley@15642
   139
                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   140
                                                      then 
quigley@15642
   141
                                                          (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   142
                                                      else 
quigley@15642
   143
                                                           raise Not_in_list
quigley@15642
   144
                                             else 
quigley@15642
   145
                                                  raise Not_in_list
quigley@15642
   146
                                              
quigley@15642
   147
                                 end   
quigley@15642
   148
                                 
quigley@15642
   149
    | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
quigley@15642
   150
                                 let val y = explode x 
quigley@15642
   151
                                     val b = explode a
quigley@15642
   152
                                 in
quigley@15642
   153
                                    if  b = y
quigley@15642
   154
                                    then 
quigley@15642
   155
                                         (pos_num, symlist, nsymlist)
quigley@15642
   156
                                    
quigley@15642
   157
                                    else
quigley@15642
   158
                                          if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
quigley@15642
   159
                                          then 
quigley@15642
   160
                                             (pos_num, symlist, nsymlist)
quigley@15642
   161
                                          else 
quigley@15642
   162
                                              if (contains_eq b) andalso (contains_eq y)
quigley@15642
   163
                                              then 
quigley@15642
   164
                                                  if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
quigley@15642
   165
                                                  then 
quigley@15642
   166
                                                      (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
quigley@15642
   167
                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   168
                                                      then 
quigley@15642
   169
                                                           (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   170
                                                      else 
quigley@15642
   171
                                                           pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
quigley@15642
   172
                                              else 
quigley@15642
   173
                                                    pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
quigley@15642
   174
                                              
quigley@15642
   175
                                 end   
quigley@15642
   176
quigley@15642
   177
quigley@15642
   178
quigley@15642
   179
quigley@15642
   180
quigley@15642
   181
quigley@15642
   182
quigley@15642
   183
                                (* in
quigley@15642
   184
                                    if  b = y
quigley@15642
   185
                                    then 
quigley@15642
   186
                                         (pos_num, symlist, nsymlist)
quigley@15642
   187
                                    else if (contains_eq b) andalso (contains_eq y)
quigley@15642
   188
                                         then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
quigley@15642
   189
                                              then if (switch_equal b y )              (* if they're equal under sym *)
quigley@15642
   190
                                                   then 
quigley@15642
   191
                                                       (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
quigley@15642
   192
                                                   else 
quigley@15642
   193
                                                         pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   194
                                              else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
quigley@15642
   195
                                                   then if (switch_equal b y )  (* if they're equal under not_sym *)
quigley@15642
   196
                                                        then 
quigley@15642
   197
                                                            (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
quigley@15642
   198
                                                        else 
quigley@15642
   199
                                                                 pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   200
                                                   else
quigley@15642
   201
                                                          pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   202
                                               else  
quigley@15642
   203
                                                       pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   204
                                          else 
quigley@15642
   205
                                                  pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
quigley@15642
   206
                                 end   
quigley@15642
   207
quigley@15642
   208
                                *)
quigley@15642
   209
quigley@15642
   210
quigley@15642
   211
(* checkorder Spass Isabelle [] *)
quigley@15642
   212
quigley@15642
   213
fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
quigley@15642
   214
|   checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =  
quigley@15642
   215
         let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) 
quigley@15642
   216
         in
quigley@15642
   217
             checkorder xs  strlist allvars ((numlist@[posnum]), symlist', not_symlist') 
quigley@15642
   218
         end
quigley@15642
   219
quigley@15642
   220
fun is_digit ch =
quigley@15642
   221
    ( ch >=  "0" andalso ch <=  "9")
quigley@15642
   222
quigley@15642
   223
quigley@15642
   224
fun is_alpha ch =
quigley@15642
   225
    (ch >=  "A" andalso  ch <=  "Z") orelse
quigley@15642
   226
    (ch >=  "a" andalso ch <=  "z")
quigley@15642
   227
quigley@15642
   228
quigley@15642
   229
fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
quigley@15642
   230
paulson@15739
   231
fun lit_string sg t = 
paulson@15739
   232
                   let val termstr = Sign.string_of_term sg t
quigley@15642
   233
                       val exp_term = explode termstr
quigley@15642
   234
                   in
quigley@15642
   235
                       implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
quigley@15642
   236
                   end
quigley@15642
   237
paulson@15739
   238
fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
quigley@15642
   239
quigley@15642
   240
paulson@15739
   241
fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
quigley@15642
   242
paulson@15739
   243
fun lit_string_bracket sg t = 
paulson@15739
   244
                   let val termstr = Sign.string_of_term sg t
quigley@15642
   245
                       val exp_term = explode termstr
quigley@15642
   246
                   in
quigley@15642
   247
                       implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
quigley@15642
   248
                   end
quigley@15642
   249
paulson@15739
   250
fun get_meta_lits_bracket thm = 
paulson@15739
   251
    map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
quigley@15642
   252
quigley@15642
   253
      
quigley@15642
   254
fun apply_rule rule [] thm = thm
quigley@15642
   255
|   apply_rule rule  (x::xs) thm = let val thm' = rule RSN ((x+1),thm)
quigley@15642
   256
                                  in
quigley@15642
   257
                                      apply_rule rule xs thm'
quigley@15642
   258
                                  end
quigley@15642
   259
quigley@15642
   260
quigley@15642
   261
quigley@15642
   262
                    (* resulting thm, clause-strs in spass order, vars *)
quigley@15642
   263
quigley@15642
   264
fun rearrange_clause thm res_strlist allvars = 
quigley@15642
   265
                          let val isa_strlist = get_meta_lits thm
quigley@15642
   266
                              val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
quigley@15642
   267
                              val symmed = apply_rule sym symlist thm
quigley@15642
   268
                              val not_symmed = apply_rule not_sym not_symlist symmed
quigley@15642
   269
                                           
quigley@15642
   270
                          in
quigley@15642
   271
                             ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
quigley@15642
   272
                          end