src/HOL/Tools/ATP/recon_order_clauses.ML
changeset 15774 9df37a0e935d
parent 15739 bb2acfed8212
child 15789 4cb16144c81b
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 19 15:15:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 19 18:08:44 2005 +0200
     1.3 @@ -2,27 +2,16 @@
     1.4  (* Reorder clauses for use in binary resolution *)
     1.5  (*----------------------------------------------*)
     1.6  
     1.7 -fun drop n [] = []
     1.8 -|   drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs)
     1.9 -
    1.10  fun remove_nth n [] = []
    1.11  |   remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n))
    1.12  
    1.13 -fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
    1.14 +(*Differs from List.nth: it counts from 1 rather than from 0*)
    1.15 +fun get_nth n (x::xs) = hd (Library.drop (n-1, x::xs))
    1.16  
    1.17  
    1.18  exception Not_in_list;  
    1.19  
    1.20  
    1.21 -fun zip xs [] = []
    1.22 -|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    1.23 -
    1.24 -
    1.25 -fun unzip [] = ([],[])
    1.26 -    | unzip((x,y)::pairs) =
    1.27 -	  let val (xs,ys) = unzip pairs
    1.28 -	  in  (x::xs, y::ys)  end;
    1.29 -
    1.30  fun numlist 0 = []
    1.31  |   numlist n = (numlist (n - 1))@[n]
    1.32  
    1.33 @@ -39,13 +28,6 @@
    1.34  
    1.35  (* code to rearrange clauses so that they're the same as the parsed in SPASS version *)
    1.36  
    1.37 -fun assoc3 a [] = raise Recon_Base.Noassoc
    1.38 -  | assoc3 a ((x, y, z)::t) = if a = x then z else assoc3 a t;
    1.39 -
    1.40 -
    1.41 -fun third (a,b,c) = c;
    1.42 -
    1.43 -
    1.44   fun takeUntil ch [] res  = (res, [])
    1.45   |   takeUntil ch (x::xs) res = if   x = ch 
    1.46                                  then
    1.47 @@ -70,12 +52,12 @@
    1.48                         then 
    1.49                             let val (left, right) = takeUntil "=" str []
    1.50                             in
    1.51 -                               ((butlast left), (drop 1 right))
    1.52 +                               (butlast left, tl right)
    1.53                             end
    1.54                         else                  (* is an inequality *)
    1.55                             let val (left, right) = takeUntil "~" str []
    1.56                             in 
    1.57 -                              ((butlast left), (drop 2 right))
    1.58 +                              (butlast left, tl (tl right))
    1.59                             end
    1.60                  
    1.61  
    1.62 @@ -101,23 +83,16 @@
    1.63  
    1.64  
    1.65  
    1.66 -fun var_pos_eq vars x y = let val xs = explode x
    1.67 +fun var_pos_eq vars x y = String.size x = String.size y andalso
    1.68 +			  let val xs = explode x
    1.69                                val ys = explode y
    1.70 +                              val xsys = ListPair.zip (xs,ys)
    1.71 +                              val are_var_pairs = map (var_equiv vars) xsys
    1.72                            in
    1.73 -                              if not_equal (length xs) (length ys)
    1.74 -                              then 
    1.75 -                                  false
    1.76 -                              else
    1.77 -                                  let val xsys = zip xs ys
    1.78 -                                      val are_var_pairs = map (var_equiv vars) xsys
    1.79 -                                  in
    1.80 -                                      all_true are_var_pairs 
    1.81 -                                  end
    1.82 +                              all_true are_var_pairs 
    1.83                            end
    1.84  
    1.85  
    1.86 -
    1.87 -
    1.88  fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
    1.89      |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
    1.90                                   let val y = explode x