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