call to Array.modifyi replaced
authorwebertj
Wed Apr 20 18:57:05 2005 +0200 (2005-04-20)
changeset 1578382e40c9a0f3f
parent 15782 a1863ea9052b
child 15784 3a214de33d53
call to Array.modifyi replaced
src/HOL/Tools/refute.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Apr 20 18:01:50 2005 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Apr 20 18:57:05 2005 +0200
     1.3 @@ -1947,7 +1947,8 @@
     1.4  										end) descr
     1.5  									(* the recursion operator is a function that maps every element of *)
     1.6  									(* the inductive datatype (and of mutually recursive types) to an  *)
     1.7 -									(* element of some result type                                     *)
     1.8 +									(* element of some result type; an array entry of NONE means that  *)
     1.9 +									(* the actual result has not been computed yet                     *)
    1.10  									(* (int * interpretation option Array.array) list *)
    1.11  									val INTRS = map (fn (idx, _) =>
    1.12  										let
    1.13 @@ -2043,7 +2044,21 @@
    1.14  												result
    1.15  											end
    1.16  									(* compute all entries in INTRS for the current datatype (given by 'index') *)
    1.17 -									val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index), 0, NONE)
    1.18 +									(* TODO: we can use Array.modify instead once PolyML conforms to the ML standard *)
    1.19 +									(* (int * 'a -> 'a) -> 'a array -> unit *)
    1.20 +									fun modifyi f arr =
    1.21 +										let
    1.22 +											val size = Array.length arr
    1.23 +											fun modifyi_loop i =
    1.24 +												if i < size then (
    1.25 +													Array.update (arr, i, f (i, Array.sub (arr, i)));
    1.26 +													modifyi_loop (i+1)
    1.27 +												) else
    1.28 +													()
    1.29 +										in
    1.30 +											modifyi_loop 0
    1.31 +										end
    1.32 +									val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
    1.33  									(* 'a Array.array -> 'a list *)
    1.34  									fun toList arr =
    1.35  										Array.foldr op:: [] arr