--- a/src/HOL/Tools/refute.ML Wed Apr 20 18:01:50 2005 +0200
+++ b/src/HOL/Tools/refute.ML Wed Apr 20 18:57:05 2005 +0200
@@ -1947,7 +1947,8 @@
end) descr
(* the recursion operator is a function that maps every element of *)
(* the inductive datatype (and of mutually recursive types) to an *)
- (* element of some result type *)
+ (* element of some result type; an array entry of NONE means that *)
+ (* the actual result has not been computed yet *)
(* (int * interpretation option Array.array) list *)
val INTRS = map (fn (idx, _) =>
let
@@ -2043,7 +2044,21 @@
result
end
(* compute all entries in INTRS for the current datatype (given by 'index') *)
- val _ = Array.modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index), 0, NONE)
+ (* TODO: we can use Array.modify instead once PolyML conforms to the ML standard *)
+ (* (int * 'a -> 'a) -> 'a array -> unit *)
+ fun modifyi f arr =
+ let
+ val size = Array.length arr
+ fun modifyi_loop i =
+ if i < size then (
+ Array.update (arr, i, f (i, Array.sub (arr, i)));
+ modifyi_loop (i+1)
+ ) else
+ ()
+ in
+ modifyi_loop 0
+ end
+ val _ = modifyi (fn (i, _) => SOME (compute_array_entry index i)) ((valOf o assoc) (INTRS, index))
(* 'a Array.array -> 'a list *)
fun toList arr =
Array.foldr op:: [] arr