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