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