src/Pure/library.ML
changeset 1576 af8f43f742a0
parent 1460 5a6f2aabd538
child 1580 e3fd931e6095
--- a/src/Pure/library.ML	Wed Mar 13 11:56:15 1996 +0100
+++ b/src/Pure/library.ML	Thu Mar 14 10:40:21 1996 +0100
@@ -8,8 +8,9 @@
 input / output, timing, filenames, misc functions.
 *)
 
-infix |> ~~ \ \\ orelf ins orf andf prefix upto downto mem union inter subset
-      subdir_of;
+infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
+      mem mem_int mem_string union union_string union_int inter inter_int
+      inter_string subset subset_int subset_string subdir_of;
 
 
 structure Library =
@@ -430,6 +431,14 @@
 fun x mem [] = false
   | x mem (y :: ys) = x = y orelse x mem ys;
 
+(*membership in a list, optimized version for int lists*)
+fun (x:int) mem_int [] = false
+  | x mem_int (y :: ys) = x = y orelse x mem_int ys;
+
+(*membership in a list, optimized version for string lists*)
+fun (x:string) mem_string [] = false
+  | x mem_string (y :: ys) = x = y orelse x mem_string ys;
+
 (*generalized membership test*)
 fun gen_mem eq (x, []) = false
   | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
@@ -438,6 +447,12 @@
 (*insertion into list if not already there*)
 fun x ins xs = if x mem xs then xs else x :: xs;
 
+(*insertion into list if not already there, optimized version for int lists*)
+fun (x:int) ins_int xs = if x mem_int xs then xs else x :: xs;
+
+(*insertion into list if not already there, optimized version for string lists*)
+fun (x:string) ins_string xs = if x mem_string xs then xs else x :: xs;
+
 (*generalized insertion*)
 fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
 
@@ -447,6 +462,16 @@
   | [] union ys = ys
   | (x :: xs) union ys = xs union (x ins ys);
 
+(*union of sets represented as lists: no repetitions, optimized version for int lists*)
+fun (xs:int list) union_int [] = xs
+  | [] union_int ys = ys
+  | (x :: xs) union_int ys = xs union_int (x ins_int ys);
+
+(*union of sets represented as lists: no repetitions, optimized version for string lists*)
+fun (xs:string list) union_string [] = xs
+  | [] union_string ys = ys
+  | (x :: xs) union_string ys = xs union_string (x ins_string ys);
+
 (*generalized union*)
 fun gen_union eq (xs, []) = xs
   | gen_union eq ([], ys) = ys
@@ -458,11 +483,29 @@
   | (x :: xs) inter ys =
       if x mem ys then x :: (xs inter ys) else xs inter ys;
 
+(*intersection, optimized version for int lists*)
+fun ([]:int list) inter_int ys = []
+  | (x :: xs) inter_int ys =
+      if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
+
+(*intersection, optimized version for string lists *)
+fun ([]:string list) inter_string ys = []
+  | (x :: xs) inter_string ys =
+      if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
+
 
 (*subset*)
 fun [] subset ys = true
   | (x :: xs) subset ys = x mem ys andalso xs subset ys;
 
+(*subset, optimized version for int lists*)
+fun ([]:int list) subset_int ys = true
+  | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
+
+(*subset, optimized version for string lists*)
+fun ([]:string list) subset_string ys = true
+  | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
+
 fun gen_subset eq (xs, ys) = forall (fn x => gen_mem eq (x, ys)) xs;
 
 
@@ -471,6 +514,16 @@
 fun eq_set (xs, ys) =
   xs = ys orelse (xs subset ys andalso ys subset xs);
 
+(*eq_set, optimized version for int lists*)
+
+fun eq_set_int ((xs:int list), ys) =
+  xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
+
+(*eq_set, optimized version for string lists*)
+
+fun eq_set_string ((xs:string list), ys) =
+  xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
+
 
 (*removing an element from a list WITHOUT duplicates*)
 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
@@ -532,6 +585,21 @@
   | assoc ((keyi, xi) :: pairs, key) =
       if key = keyi then Some xi else assoc (pairs, key);
 
+(*association list lookup, optimized version for int lists*)
+fun assoc_int ([], (key:int)) = None
+  | assoc_int ((keyi, xi) :: pairs, key) =
+      if key = keyi then Some xi else assoc_int (pairs, key);
+
+(*association list lookup, optimized version for string lists*)
+fun assoc_string ([], (key:string)) = None
+  | assoc_string ((keyi, xi) :: pairs, key) =
+      if key = keyi then Some xi else assoc_string (pairs, key);
+
+(*association list lookup, optimized version for string*int lists*)
+fun assoc_string_int ([], (key:string*int)) = None
+  | assoc_string_int ((keyi, xi) :: pairs, key) =
+      if key = keyi then Some xi else assoc_string_int (pairs, key);
+
 fun assocs ps x =
   (case assoc (ps, x) of
     None => []