author webertj Wed Apr 20 18:57:05 2005 +0200 (2005-04-20 ago) changeset 15783 82e40c9a0f3f parent 15782 a1863ea9052b child 15784 3a214de33d53
call to Array.modifyi replaced
 src/HOL/Tools/refute.ML file | annotate | diff | revisions
```     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
```