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