src/Pure/library.ML
changeset 1576 af8f43f742a0
parent 1460 5a6f2aabd538
child 1580 e3fd931e6095
     1.1 --- a/src/Pure/library.ML	Wed Mar 13 11:56:15 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Mar 14 10:40:21 1996 +0100
     1.3 @@ -8,8 +8,9 @@
     1.4  input / output, timing, filenames, misc functions.
     1.5  *)
     1.6  
     1.7 -infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset
     1.8 -      subdir_of;
     1.9 +infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    1.10 +      mem mem_int mem_string union union_string union_int inter inter_int
    1.11 +      inter_string subset subset_int subset_string subdir_of;
    1.12  
    1.13  
    1.14  structure Library =
    1.15 @@ -430,6 +431,14 @@
    1.16  fun x mem [] = false
    1.17    | x mem (y :: ys) = x = y orelse x mem ys;
    1.18  
    1.19 +(*membership in a list, optimized version for int lists*)
    1.20 +fun (x:int) mem_int [] = false
    1.21 +  | x mem_int (y :: ys) = x = y orelse x mem_int ys;
    1.22 +
    1.23 +(*membership in a list, optimized version for string lists*)
    1.24 +fun (x:string) mem_string [] = false
    1.25 +  | x mem_string (y :: ys) = x = y orelse x mem_string ys;
    1.26 +
    1.27  (*generalized membership test*)
    1.28  fun gen_mem eq (x, []) = false
    1.29    | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    1.30 @@ -438,6 +447,12 @@
    1.31  (*insertion into list if not already there*)
    1.32  fun x ins xs = if x mem xs then xs else x :: xs;
    1.33  
    1.34 +(*insertion into list if not already there, optimized version for int lists*)
    1.35 +fun (x:int) ins_int xs = if x mem_int xs then xs else x :: xs;
    1.36 +
    1.37 +(*insertion into list if not already there, optimized version for string lists*)
    1.38 +fun (x:string) ins_string xs = if x mem_string xs then xs else x :: xs;
    1.39 +
    1.40  (*generalized insertion*)
    1.41  fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
    1.42  
    1.43 @@ -447,6 +462,16 @@
    1.44    | [] union ys = ys
    1.45    | (x :: xs) union ys = xs union (x ins ys);
    1.46  
    1.47 +(*union of sets represented as lists: no repetitions, optimized version for int lists*)
    1.48 +fun (xs:int list) union_int [] = xs
    1.49 +  | [] union_int ys = ys
    1.50 +  | (x :: xs) union_int ys = xs union_int (x ins_int ys);
    1.51 +
    1.52 +(*union of sets represented as lists: no repetitions, optimized version for string lists*)
    1.53 +fun (xs:string list) union_string [] = xs
    1.54 +  | [] union_string ys = ys
    1.55 +  | (x :: xs) union_string ys = xs union_string (x ins_string ys);
    1.56 +
    1.57  (*generalized union*)
    1.58  fun gen_union eq (xs, []) = xs
    1.59    | gen_union eq ([], ys) = ys
    1.60 @@ -458,11 +483,29 @@
    1.61    | (x :: xs) inter ys =
    1.62        if x mem ys then x :: (xs inter ys) else xs inter ys;
    1.63  
    1.64 +(*intersection, optimized version for int lists*)
    1.65 +fun ([]:int list) inter_int ys = []
    1.66 +  | (x :: xs) inter_int ys =
    1.67 +      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
    1.68 +
    1.69 +(*intersection, optimized version for string lists *)
    1.70 +fun ([]:string list) inter_string ys = []
    1.71 +  | (x :: xs) inter_string ys =
    1.72 +      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
    1.73 +
    1.74  
    1.75  (*subset*)
    1.76  fun [] subset ys = true
    1.77    | (x :: xs) subset ys = x mem ys andalso xs subset ys;
    1.78  
    1.79 +(*subset, optimized version for int lists*)
    1.80 +fun ([]:int list) subset_int ys = true
    1.81 +  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
    1.82 +
    1.83 +(*subset, optimized version for string lists*)
    1.84 +fun ([]:string list) subset_string ys = true
    1.85 +  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
    1.86 +
    1.87  fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
    1.88  
    1.89  
    1.90 @@ -471,6 +514,16 @@
    1.91  fun eq_set (xs, ys) =
    1.92    xs = ys orelse (xs subset ys andalso ys subset xs);
    1.93  
    1.94 +(*eq_set, optimized version for int lists*)
    1.95 +
    1.96 +fun eq_set_int ((xs:int list), ys) =
    1.97 +  xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
    1.98 +
    1.99 +(*eq_set, optimized version for string lists*)
   1.100 +
   1.101 +fun eq_set_string ((xs:string list), ys) =
   1.102 +  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
   1.103 +
   1.104  
   1.105  (*removing an element from a list WITHOUT duplicates*)
   1.106  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
   1.107 @@ -532,6 +585,21 @@
   1.108    | assoc ((keyi, xi) :: pairs, key) =
   1.109        if key = keyi then Some xi else assoc (pairs, key);
   1.110  
   1.111 +(*association list lookup, optimized version for int lists*)
   1.112 +fun assoc_int ([], (key:int)) = None
   1.113 +  | assoc_int ((keyi, xi) :: pairs, key) =
   1.114 +      if key = keyi then Some xi else assoc_int (pairs, key);
   1.115 +
   1.116 +(*association list lookup, optimized version for string lists*)
   1.117 +fun assoc_string ([], (key:string)) = None
   1.118 +  | assoc_string ((keyi, xi) :: pairs, key) =
   1.119 +      if key = keyi then Some xi else assoc_string (pairs, key);
   1.120 +
   1.121 +(*association list lookup, optimized version for string*int lists*)
   1.122 +fun assoc_string_int ([], (key:string*int)) = None
   1.123 +  | assoc_string_int ((keyi, xi) :: pairs, key) =
   1.124 +      if key = keyi then Some xi else assoc_string_int (pairs, key);
   1.125 +
   1.126  fun assocs ps x =
   1.127    (case assoc (ps, x) of
   1.128      None => []