added some int constraints (ML_Parse.fix_ints not active here);
authorwenzelm
Sun Sep 16 14:52:26 2007 +0200 (2007-09-16)
changeset 245931547ea587f5a
parent 24592 dfea1edbf711
child 24594 6689effe75d1
added some int constraints (ML_Parse.fix_ints not active here);
src/Pure/General/symbol.ML
src/Pure/ML-Systems/multithreading_dummy.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/General/symbol.ML	Sat Sep 15 19:29:29 2007 +0200
     1.2 +++ b/src/Pure/General/symbol.ML	Sun Sep 16 14:52:26 2007 +0200
     1.3 @@ -499,7 +499,7 @@
     1.4  val xsymbolsN = "xsymbols";
     1.5  
     1.6  fun sym_len s =
     1.7 -  if not (is_printable s) then 0
     1.8 +  if not (is_printable s) then (0: int)
     1.9    else if String.isPrefix "\\<long" s then 2
    1.10    else if String.isPrefix "\\<Long" s then 2
    1.11    else if s = "\\<spacespace>" then 2
     2.1 --- a/src/Pure/ML-Systems/multithreading_dummy.ML	Sat Sep 15 19:29:29 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Sun Sep 16 14:52:26 2007 +0200
     2.3 @@ -22,11 +22,11 @@
     2.4  structure Multithreading: MULTITHREADING =
     2.5  struct
     2.6  
     2.7 -val trace = ref 0;
     2.8 +val trace = ref (0: int);
     2.9  fun tracing _ _ = ();
    2.10  
    2.11  val available = false;
    2.12 -val max_threads = ref 1;
    2.13 +val max_threads = ref (1: int);
    2.14  
    2.15  fun self_critical () = false;
    2.16  fun NAMED_CRITICAL _ e = e ();
     3.1 --- a/src/Pure/library.ML	Sat Sep 15 19:29:29 2007 +0200
     3.2 +++ b/src/Pure/library.ML	Sun Sep 16 14:52:26 2007 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4  fun (f oooo g) x y z w = f (g x y z w);
     3.5  
     3.6  (*function exponentiation: f(...(f x)...) with n applications of f*)
     3.7 -fun funpow 0 _ x = x
     3.8 +fun funpow (0: int) _ x = x
     3.9    | funpow n f x = funpow (n - 1) f (f x);
    3.10  
    3.11  
    3.12 @@ -406,17 +406,17 @@
    3.13  fun maps f [] = []
    3.14    | maps f (x :: xs) = f x @ maps f xs;
    3.15  
    3.16 -fun chop 0 xs = ([], xs)
    3.17 +fun chop (0: int) xs = ([], xs)
    3.18    | chop _ [] = ([], [])
    3.19    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    3.20  
    3.21  (*take the first n elements from a list*)
    3.22 -fun take (n, []) = []
    3.23 +fun take (n: int, []) = []
    3.24    | take (n, x :: xs) =
    3.25        if n > 0 then x :: take (n - 1, xs) else [];
    3.26  
    3.27  (*drop the first n elements from a list*)
    3.28 -fun drop (n, []) = []
    3.29 +fun drop (n: int, []) = []
    3.30    | drop (n, x :: xs) =
    3.31        if n > 0 then drop (n - 1, xs) else x :: xs;
    3.32  
    3.33 @@ -431,18 +431,18 @@
    3.34  
    3.35  fun nth_map 0 f (x :: xs) = f x :: xs
    3.36    | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    3.37 -  | nth_map _ _ [] = raise Subscript;
    3.38 +  | nth_map (_: int) _ [] = raise Subscript;
    3.39  
    3.40  fun map_index f =
    3.41    let
    3.42 -    fun mapp _ [] = []
    3.43 -      | mapp i (x :: xs) = f (i, x) :: mapp (i+1) xs
    3.44 +    fun mapp (_: int) [] = []
    3.45 +      | mapp i (x :: xs) = f (i, x) :: mapp (i + 1) xs
    3.46    in mapp 0 end;
    3.47  
    3.48  fun fold_index f =
    3.49    let
    3.50 -    fun fold_aux _ [] y = y
    3.51 -      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    3.52 +    fun fold_aux (_: int) [] y = y
    3.53 +      | fold_aux i (x :: xs) y = fold_aux (i + 1) xs (f (i, x) y);
    3.54    in fold_aux 0 end;
    3.55  
    3.56  val last_elem = List.last;
    3.57 @@ -454,7 +454,7 @@
    3.58  
    3.59  (*find the position of an element in a list*)
    3.60  fun find_index pred =
    3.61 -  let fun find _ [] = ~1
    3.62 +  let fun find (_: int) [] = ~1
    3.63          | find n (x :: xs) = if pred x then n else find (n + 1) xs;
    3.64    in find 0 end;
    3.65  
    3.66 @@ -472,7 +472,7 @@
    3.67  
    3.68  fun get_index f =
    3.69    let
    3.70 -    fun get _ [] = NONE
    3.71 +    fun get (_: int) [] = NONE
    3.72        | get i (x :: xs) =
    3.73            case f x
    3.74             of NONE => get (i + 1) xs
    3.75 @@ -497,7 +497,7 @@
    3.76    | separate _ xs = xs;
    3.77  
    3.78  (*make the list [x, x, ..., x] of length n*)
    3.79 -fun replicate n (x: 'a) : 'a list =
    3.80 +fun replicate (n: int) x =
    3.81    let fun rep (0, xs) = xs
    3.82          | rep (n, xs) = rep (n - 1, x :: xs)
    3.83    in
    3.84 @@ -595,18 +595,18 @@
    3.85  
    3.86  (** integers **)
    3.87  
    3.88 -fun inc i = (i := ! i + 1; ! i);
    3.89 -fun dec i = (i := ! i - 1; ! i);
    3.90 +fun inc i = (i := ! i + (1: int); ! i);
    3.91 +fun dec i = (i := ! i - (1: int); ! i);
    3.92  
    3.93  
    3.94  (* lists of integers *)
    3.95  
    3.96  (*make the list [from, from + 1, ..., to]*)
    3.97 -fun (i upto j) =
    3.98 +fun ((i: int) upto j) =
    3.99    if i > j then [] else i :: (i + 1 upto j);
   3.100  
   3.101  (*make the list [from, from - 1, ..., to]*)
   3.102 -fun (i downto j) =
   3.103 +fun ((i: int) downto j) =
   3.104    if i < j then [] else i :: (i - 1 downto j);
   3.105  
   3.106  
   3.107 @@ -732,7 +732,7 @@
   3.108    if String.isSuffix sffx s then String.substring (s, 0, size s - size sffx)
   3.109    else raise Fail "unsuffix";
   3.110  
   3.111 -fun replicate_string 0 _ = ""
   3.112 +fun replicate_string (0: int) _ = ""
   3.113    | replicate_string 1 a = a
   3.114    | replicate_string k a =
   3.115        if k mod 2 = 0 then replicate_string (k div 2) (a ^ a)
   3.116 @@ -1002,7 +1002,7 @@
   3.117              else
   3.118              let val (ns, rest) = List.partition (p k) xs;
   3.119              in  ns :: part(k+1)rest  end
   3.120 -  in  part i end;
   3.121 +  in  part (i: int) end;
   3.122  
   3.123  fun partition_eq (eq:'a * 'a -> bool) =
   3.124    let
   3.125 @@ -1027,7 +1027,7 @@
   3.126  val char_vec = Vector.tabulate (62, gensym_char);
   3.127  fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
   3.128  
   3.129 -val gensym_seed = ref 0;
   3.130 +val gensym_seed = ref (0: int);
   3.131  
   3.132  in
   3.133    fun gensym pre = pre ^ newid (NAMED_CRITICAL "gensym" (fn () => inc gensym_seed));
   3.134 @@ -1040,7 +1040,7 @@
   3.135  val stamp: unit -> stamp = ref;
   3.136  
   3.137  type serial = int;
   3.138 -local val count = ref 0
   3.139 +local val count = ref (0: int)
   3.140  in fun serial () = NAMED_CRITICAL "serial" (fn () => inc count) end;
   3.141  
   3.142  val serial_string = string_of_int o serial;