1(*---------------------------------------------------------------------------*)
2(* History provides "registers-with-bounded-history". You can read (via      *)
3(* "project"), write (via "apply"), and undo.                                *)
4(*---------------------------------------------------------------------------*)
5
6structure History :> History =
7struct
8
9open Feedback Lib;
10
11val HIST_ERR = mk_HOL_ERR "History";
12exception CANT_BACKUP_ANYMORE;
13
14datatype 'a history = HISTORY of {obj:'a, past:'a list, orig:'a, limit:int, save_points:'a list};
15
16fun new_history {obj, limit} = HISTORY{obj=obj, past=[], orig=obj, limit=limit, save_points = []}
17
18local fun chop n alist = fst (split_after n alist) handle _ => alist
19in
20fun apply f (HISTORY{obj, past, orig, limit, save_points}) =
21      HISTORY{obj=f obj, past=chop limit (obj::past), orig=orig, limit=limit, save_points=save_points}
22
23fun set_limit (HISTORY{obj,past,orig,limit,save_points}) n =
24  if n<0 then raise HIST_ERR "set_limit" "negative limit"
25  else HISTORY{obj=obj, past=chop n past, orig=orig, limit=n,save_points=save_points}
26end;
27
28fun remove_past (HISTORY{obj,past,orig,limit,save_points}) =
29  new_history {obj=obj,limit=limit};
30
31fun initialValue (HISTORY{orig, ...}) = orig;
32
33fun project f (HISTORY{obj, ...}) = f obj;
34
35fun undo (HISTORY{past=[], ...}) = raise CANT_BACKUP_ANYMORE
36  | undo (HISTORY{past=h::rst, limit, orig,save_points,...}) =
37          HISTORY{obj=h, past=rst, orig=orig, limit=limit,save_points=save_points}
38
39fun restore (HISTORY{obj,past,orig,limit,save_points}) =
40  let
41     val (save_points',obj') = if (null save_points) then ([], orig) else
42         (if not (null past) then (save_points, hd save_points) else
43             (if null (tl save_points) then ([], orig) else
44                 (tl save_points, hd (tl (save_points)))));
45  in
46     HISTORY{obj=obj', past=[], orig=orig, limit=limit, save_points=save_points'}
47  end;
48
49fun save (HISTORY{obj,past,orig,limit,save_points}) =
50     HISTORY{obj=obj, past=[], orig=orig, limit=limit, save_points=obj::save_points}
51
52end
53