src/Pure/Isar/proof_history.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7366 22a64baa7013
child 7731 51d59734743d
permissions -rw-r--r--
removed extra shyps error;
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@5827
     5
Histories of proof states, with undo / redo and prev / back.
wenzelm@5827
     6
*)
wenzelm@5827
     7
wenzelm@5827
     8
signature PROOF_HISTORY =
wenzelm@5827
     9
sig
wenzelm@5827
    10
  type T
wenzelm@5827
    11
  exception FAIL of string
wenzelm@6902
    12
  val position: T -> int
wenzelm@6684
    13
  val init: int option -> Proof.state -> T
wenzelm@6684
    14
  val is_initial: T -> bool
wenzelm@5827
    15
  val current: T -> Proof.state
wenzelm@5827
    16
  val clear: T -> T
wenzelm@5827
    17
  val undo: T -> T
wenzelm@5827
    18
  val redo: T -> T
wenzelm@7366
    19
  val back: bool -> 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@6902
    31
  Proof.state *			(*first result*)
wenzelm@6902
    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
exception FAIL of string;
wenzelm@5827
    39
wenzelm@5827
    40
fun app f (ProofHistory x) = ProofHistory (f x);
wenzelm@5827
    41
fun hist_app f = app (History.apply f);
wenzelm@5827
    42
wenzelm@6902
    43
fun position (ProofHistory prf) = length (snd (History.current prf));
wenzelm@6902
    44
wenzelm@5827
    45
wenzelm@5827
    46
(* generic history operations *)
wenzelm@5827
    47
wenzelm@6902
    48
fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), []));
wenzelm@6684
    49
fun is_initial (ProofHistory prf) = History.is_initial prf;
wenzelm@6902
    50
fun current (ProofHistory prf) = fst (fst (History.current prf));
wenzelm@5827
    51
val clear = app History.clear;
wenzelm@5827
    52
val undo = app History.undo;
wenzelm@5827
    53
val redo = app History.redo;
wenzelm@5827
    54
wenzelm@5827
    55
wenzelm@5827
    56
(* backtrack *)
wenzelm@5827
    57
wenzelm@7366
    58
fun back_fun recur ((_, stq), nodes) =
wenzelm@5827
    59
  (case Seq.pull stq of
wenzelm@5827
    60
    None =>
wenzelm@7366
    61
      if recur andalso not (null nodes) then
wenzelm@7366
    62
        (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
wenzelm@7366
    63
      else raise FAIL "back: no alternatives"
wenzelm@6902
    64
  | Some result => (result, nodes));
wenzelm@5827
    65
wenzelm@7366
    66
val back = hist_app o back_fun;
wenzelm@5827
    67
wenzelm@5827
    68
wenzelm@5827
    69
(* apply transformer *)
wenzelm@5827
    70
wenzelm@6902
    71
fun applys f = hist_app (fn (node as (st, _), nodes) =>
wenzelm@5827
    72
  (case Seq.pull (f st) of
wenzelm@6902
    73
    None => raise FAIL "empty result sequence -- proof command failed"
wenzelm@6902
    74
  | Some results => (results, node :: nodes)));
wenzelm@5827
    75
wenzelm@5827
    76
fun apply f = applys (Seq.single o f);
wenzelm@6902
    77
wenzelm@5827
    78
wenzelm@5827
    79
end;