src/Pure/library.ML
changeset 2175 21fde76bc742
parent 2157 50c26585e523
child 2182 29e56f003599
     1.1 --- a/src/Pure/library.ML	Tue Nov 12 11:36:44 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Tue Nov 12 11:38:51 1996 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  *)
     1.5  
     1.6  infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
     1.7 -      mem mem_int mem_string union union_string union_int inter inter_int
     1.8 -      inter_string subset subset_int subset_string subdir_of;
     1.9 +      mem mem_int mem_string union union_int union_string  
    1.10 +      inter inter_int inter_string subset subset_int subset_string subdir_of;
    1.11  
    1.12  
    1.13  structure Library =
    1.14 @@ -28,7 +28,7 @@
    1.15  fun (x |> f) = f x;
    1.16  
    1.17  (*combine two functions forming the union of their domains*)
    1.18 -fun f orelf g = fn x => f x handle Match => g x;
    1.19 +fun (f orelf g) = fn x => f x handle Match => g x;
    1.20  
    1.21  (*application of (infix) operator to its left or right argument*)
    1.22  fun apl (x, f) y = f (x, y);
    1.23 @@ -97,9 +97,9 @@
    1.24  
    1.25  (* operators for combining predicates *)
    1.26  
    1.27 -fun p orf q = fn x => p x orelse q x;
    1.28 +fun (p orf q) = fn x => p x orelse q x;
    1.29  
    1.30 -fun p andf q = fn x => p x andalso q x;
    1.31 +fun (p andf q) = fn x => p x andalso q x;
    1.32  
    1.33  fun notf p x = not (p x);
    1.34  
    1.35 @@ -318,11 +318,11 @@
    1.36  (* lists of integers *)
    1.37  
    1.38  (*make the list [from, from + 1, ..., to]*)
    1.39 -fun from upto to =
    1.40 +fun (from upto to) =
    1.41    if from > to then [] else from :: ((from + 1) upto to);
    1.42  
    1.43  (*make the list [from, from - 1, ..., to]*)
    1.44 -fun from downto to =
    1.45 +fun (from downto to) =
    1.46    if from < to then [] else from :: ((from - 1) downto to);
    1.47  
    1.48  (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
    1.49 @@ -417,11 +417,11 @@
    1.50  fun x mem [] = false
    1.51    | x mem (y :: ys) = x = y orelse x mem ys;
    1.52  
    1.53 -(*membership in a list, optimized version for int lists*)
    1.54 +(*membership in a list, optimized version for ints*)
    1.55  fun (x:int) mem_int [] = false
    1.56    | x mem_int (y :: ys) = x = y orelse x mem_int ys;
    1.57  
    1.58 -(*membership in a list, optimized version for string lists*)
    1.59 +(*membership in a list, optimized version for strings*)
    1.60  fun (x:string) mem_string [] = false
    1.61    | x mem_string (y :: ys) = x = y orelse x mem_string ys;
    1.62  
    1.63 @@ -431,13 +431,13 @@
    1.64  
    1.65  
    1.66  (*insertion into list if not already there*)
    1.67 -fun x ins xs = if x mem xs then xs else x :: xs;
    1.68 +fun (x ins xs) = if x mem xs then xs else x :: xs;
    1.69  
    1.70 -(*insertion into list if not already there, optimized version for int lists*)
    1.71 -fun (x:int) ins_int xs = if x mem_int xs then xs else x :: xs;
    1.72 +(*insertion into list, optimized version for ints*)
    1.73 +fun (x ins_int xs) = if x mem_int xs then xs else x :: xs;
    1.74  
    1.75 -(*insertion into list if not already there, optimized version for string lists*)
    1.76 -fun (x:string) ins_string xs = if x mem_string xs then xs else x :: xs;
    1.77 +(*insertion into list, optimized version for strings*)
    1.78 +fun (x ins_string xs) = if x mem_string xs then xs else x :: xs;
    1.79  
    1.80  (*generalized insertion*)
    1.81  fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
    1.82 @@ -448,12 +448,12 @@
    1.83    | [] union ys = ys
    1.84    | (x :: xs) union ys = xs union (x ins ys);
    1.85  
    1.86 -(*union of sets represented as lists: no repetitions, optimized version for int lists*)
    1.87 +(*union of sets, optimized version for ints*)
    1.88  fun (xs:int list) union_int [] = xs
    1.89    | [] union_int ys = ys
    1.90    | (x :: xs) union_int ys = xs union_int (x ins_int ys);
    1.91  
    1.92 -(*union of sets represented as lists: no repetitions, optimized version for string lists*)
    1.93 +(*union of sets, optimized version for strings*)
    1.94  fun (xs:string list) union_string [] = xs
    1.95    | [] union_string ys = ys
    1.96    | (x :: xs) union_string ys = xs union_string (x ins_string ys);
    1.97 @@ -469,12 +469,12 @@
    1.98    | (x :: xs) inter ys =
    1.99        if x mem ys then x :: (xs inter ys) else xs inter ys;
   1.100  
   1.101 -(*intersection, optimized version for int lists*)
   1.102 +(*intersection, optimized version for ints*)
   1.103  fun ([]:int list) inter_int ys = []
   1.104    | (x :: xs) inter_int ys =
   1.105        if x mem_int ys then x :: (xs inter_int ys) else xs inter_int ys;
   1.106  
   1.107 -(*intersection, optimized version for string lists *)
   1.108 +(*intersection, optimized version for strings *)
   1.109  fun ([]:string list) inter_string ys = []
   1.110    | (x :: xs) inter_string ys =
   1.111        if x mem_string ys then x :: (xs inter_string ys) else xs inter_string ys;
   1.112 @@ -484,11 +484,11 @@
   1.113  fun [] subset ys = true
   1.114    | (x :: xs) subset ys = x mem ys andalso xs subset ys;
   1.115  
   1.116 -(*subset, optimized version for int lists*)
   1.117 +(*subset, optimized version for ints*)
   1.118  fun ([]:int list) subset_int ys = true
   1.119    | (x :: xs) subset_int ys = x mem_int ys andalso xs subset_int ys;
   1.120  
   1.121 -(*subset, optimized version for string lists*)
   1.122 +(*subset, optimized version for strings*)
   1.123  fun ([]:string list) subset_string ys = true
   1.124    | (x :: xs) subset_string ys = x mem_string ys andalso xs subset_string ys;
   1.125  
   1.126 @@ -500,12 +500,12 @@
   1.127  fun eq_set (xs, ys) =
   1.128    xs = ys orelse (xs subset ys andalso ys subset xs);
   1.129  
   1.130 -(*eq_set, optimized version for int lists*)
   1.131 +(*eq_set, optimized version for ints*)
   1.132  
   1.133  fun eq_set_int ((xs:int list), ys) =
   1.134    xs = ys orelse (xs subset_int ys andalso ys subset_int xs);
   1.135  
   1.136 -(*eq_set, optimized version for string lists*)
   1.137 +(*eq_set, optimized version for strings*)
   1.138  
   1.139  fun eq_set_string ((xs:string list), ys) =
   1.140    xs = ys orelse (xs subset_string ys andalso ys subset_string xs);
   1.141 @@ -571,17 +571,17 @@
   1.142    | assoc ((keyi, xi) :: pairs, key) =
   1.143        if key = keyi then Some xi else assoc (pairs, key);
   1.144  
   1.145 -(*association list lookup, optimized version for int lists*)
   1.146 +(*association list lookup, optimized version for ints*)
   1.147  fun assoc_int ([], (key:int)) = None
   1.148    | assoc_int ((keyi, xi) :: pairs, key) =
   1.149        if key = keyi then Some xi else assoc_int (pairs, key);
   1.150  
   1.151 -(*association list lookup, optimized version for string lists*)
   1.152 +(*association list lookup, optimized version for strings*)
   1.153  fun assoc_string ([], (key:string)) = None
   1.154    | assoc_string ((keyi, xi) :: pairs, key) =
   1.155        if key = keyi then Some xi else assoc_string (pairs, key);
   1.156  
   1.157 -(*association list lookup, optimized version for string*int lists*)
   1.158 +(*association list lookup, optimized version for string*ints*)
   1.159  fun assoc_string_int ([], (key:string*int)) = None
   1.160    | assoc_string_int ((keyi, xi) :: pairs, key) =
   1.161        if key = keyi then Some xi else assoc_string_int (pairs, key);