package timed
-
timed.compat
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package timed
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
The Time module provides an abstract representation of time, used to set a point from which updates to references are recorded to allow undoing (of redoing) the corresponding changes.
val save : unit -> tsave () registers the position of the program in its “timeline”. The returned value can then be used to “time-travel” toward this point, by calling restore. The saving operation runs in constant time. In the process one block of memory of three words is allocated. Note that two consecutive calls to save (i.e., with no interleaved (:=) or restore) return the same value, and the second one does not allocate any memory.
Note that when a saved “time” becomes unaccessible, memory previously allocated by (:=) may itself become unaccessible if none of the remaining saved “times” can undo the corresponding updates. If that is the case, the memory related to these update is collected. The memory footprint of the library is thus minimal.
val restore : t -> unitrestore t has the effect of “traveling in time” towards a previously recorded point t. After calling this function, the reference updates made between t and the “time before the call” are undone. Note that this is the only basic operation that is not constant time. Complexity (time and space) is discussed below.
The time complexity of restore is O(MT) where:
- M is the maximum number of different references that were updated between two consecutive calls to
save. - T is the number of saved time between t and the current time. The number of memory blocks allocated by the
restorefunction is proportional to the above T.
A better expression of its time complexity is “Σ Mₖtₖ” (for 0 ≤ k < n) where tₖ is the k-th (saved) time between t = t₀ and current time tₙ, and Mₖ is the number of different updated references between the times tₖ and tₖ₊₁.