src/Pure/Isar/proof_history.ML
author haftmann
Fri Nov 10 07:44:47 2006 +0100 (2006-11-10)
changeset 21286 b5e7b80caa6a
parent 18678 dd0c569fa43d
child 23362 de1476695aa6
permissions -rw-r--r--
introduces canonical AList functions for loop_tacs
wenzelm@5827
     1
(*  Title:      Pure/Isar/proof_history.ML
wenzelm@5827
     2
    ID:         $Id$
wenzelm@5827
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5827
     4
wenzelm@16490
     5
Histories of proof states, with undo / redo and backtracking.
wenzelm@5827
     6
*)
wenzelm@5827
     7
wenzelm@5827
     8
signature PROOF_HISTORY =
wenzelm@5827
     9
sig
wenzelm@5827
    10
  type T
wenzelm@6902
    11
  val position: T -> int
wenzelm@6684
    12
  val init: int option -> Proof.state -> T
wenzelm@6684
    13
  val is_initial: T -> bool
wenzelm@5827
    14
  val current: T -> Proof.state
wenzelm@16814
    15
  val previous: T -> Proof.state option
wenzelm@7731
    16
  val clear: int -> T -> T
wenzelm@5827
    17
  val undo: T -> T
wenzelm@5827
    18
  val redo: T -> T
wenzelm@17073
    19
  val back: T -> T
wenzelm@5827
    20
  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
wenzelm@5827
    21
  val apply: (Proof.state -> Proof.state) -> T -> T
wenzelm@5827
    22
end;
wenzelm@5827
    23
wenzelm@5827
    24
structure ProofHistory: PROOF_HISTORY =
wenzelm@5827
    25
struct
wenzelm@5827
    26
wenzelm@5827
    27
wenzelm@5827
    28
(* datatype proof history *)
wenzelm@5827
    29
wenzelm@5827
    30
type node =
wenzelm@16490
    31
  Proof.state *                 (*first result*)
wenzelm@16490
    32
  Proof.state Seq.seq;          (*alternative results*)
wenzelm@5827
    33
wenzelm@5827
    34
type proof = node * node list;
wenzelm@5827
    35
wenzelm@5827
    36
datatype T = ProofHistory of proof History.T;
wenzelm@5827
    37
wenzelm@5827
    38
fun app f (ProofHistory x) = ProofHistory (f x);
wenzelm@5827
    39
fun hist_app f = app (History.apply f);
wenzelm@5827
    40
wenzelm@6902
    41
fun position (ProofHistory prf) = length (snd (History.current prf));
wenzelm@6902
    42
wenzelm@5827
    43
wenzelm@5827
    44
(* generic history operations *)
wenzelm@5827
    45
wenzelm@6902
    46
fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), []));
wenzelm@6684
    47
fun is_initial (ProofHistory prf) = History.is_initial prf;
wenzelm@6902
    48
fun current (ProofHistory prf) = fst (fst (History.current prf));
wenzelm@16814
    49
fun previous (ProofHistory prf) = Option.map (fst o fst) (History.previous prf);
wenzelm@7731
    50
val clear = app o History.clear;
wenzelm@5827
    51
val undo = app History.undo;
wenzelm@5827
    52
val redo = app History.redo;
wenzelm@5827
    53
wenzelm@5827
    54
wenzelm@17073
    55
(* backtracking *)
wenzelm@5827
    56
wenzelm@17073
    57
val back = hist_app (fn ((_, stq), nodes) =>
wenzelm@5827
    58
  (case Seq.pull stq of
wenzelm@18678
    59
    NONE => error "back: no alternatives"
wenzelm@17073
    60
  | SOME result => (result, nodes)));
wenzelm@5827
    61
wenzelm@5827
    62
wenzelm@5827
    63
(* apply transformer *)
wenzelm@5827
    64
wenzelm@6902
    65
fun applys f = hist_app (fn (node as (st, _), nodes) =>
wenzelm@5827
    66
  (case Seq.pull (f st) of
wenzelm@18678
    67
    NONE => error "empty result sequence -- proof command failed"
skalberg@15531
    68
  | SOME results => (results, node :: nodes)));
wenzelm@5827
    69
wenzelm@5827
    70
fun apply f = applys (Seq.single o f);
wenzelm@6902
    71
wenzelm@5827
    72
wenzelm@5827
    73
end;