Timed references for imperative state. This module provides an alternative type for references (or mutable cells) supporting undo/redo operations. In particular, an abstract notion of time is used to capture the state of the references at any given point, so that it can be restored. Note that usual reference operations only have a constant time / memory overhead (compared to those of the standard library).
Moreover, we provide an alternative implementation based on the references of the standard library (Pervasives module). However, it is less efficient than the first one.
Published: 05 Aug 2022
Timed references for imperative state
This minimal library allows the encapsulation of reference updates in an abstract notion of state. It can be used to emulate a pure interface while working with references.
Authors: Rodolphe Lepigre & Christophe Raffalli
The library has no dependency, but it is built using
dune. You can use the following commands to compile and install.
make make install
open Timed let _ = let r1 = ref 0 in let r2 = ref 42 in let t1 = Time.save () in r1 := 73; let t2 = Time.save () in Time.restore t1; assert(!r1 = 0 && !r2 = 42) r1 := 17; Time.restore t2; assert(!r1 = 73 && !r2 = 42)