src/Pure/Isar/proof_history.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6374 a67e4729efb2
child 6684 4f859545bd92
permissions -rw-r--r--
common qed and end of proofs;
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@5827
    12
  val init: Proof.state -> T
wenzelm@5827
    13
  val current: T -> Proof.state
wenzelm@5827
    14
  val clear: T -> T
wenzelm@5827
    15
  val undo: T -> T
wenzelm@5827
    16
  val redo: T -> T
wenzelm@5944
    17
  val undos: int -> T -> T
wenzelm@5944
    18
  val redos: int -> T -> T
wenzelm@5827
    19
  val position: T -> int
wenzelm@5827
    20
  val nesting: T -> int
wenzelm@5827
    21
  val prev: T -> T
wenzelm@5827
    22
  val up: T -> T
wenzelm@5827
    23
  val top: T -> T
wenzelm@5827
    24
  val back: T -> T
wenzelm@5827
    25
  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
wenzelm@5827
    26
  val applys_open: (Proof.state -> Proof.state Seq.seq) -> T -> T
wenzelm@5827
    27
  val applys_close: (Proof.state -> Proof.state Seq.seq) -> T -> T
wenzelm@5827
    28
  val apply: (Proof.state -> Proof.state) -> T -> T
wenzelm@5827
    29
  val apply_open: (Proof.state -> Proof.state) -> T -> T
wenzelm@5827
    30
  val apply_close: (Proof.state -> Proof.state) -> T -> T
wenzelm@6374
    31
  val apply_cond_open: bool -> (Proof.state -> Proof.state) -> T -> T
wenzelm@5827
    32
end;
wenzelm@5827
    33
wenzelm@5827
    34
structure ProofHistory: PROOF_HISTORY =
wenzelm@5827
    35
struct
wenzelm@5827
    36
wenzelm@5827
    37
wenzelm@5827
    38
(* datatype proof history *)
wenzelm@5827
    39
wenzelm@5827
    40
type node =
wenzelm@5827
    41
 (Proof.state *			(*first result*)
wenzelm@5827
    42
  Proof.state Seq.seq) *	(*alternative results*)
wenzelm@5827
    43
  int;				(*nest level*)
wenzelm@5827
    44
wenzelm@5827
    45
type proof = node * node list;
wenzelm@5827
    46
wenzelm@5827
    47
datatype T = ProofHistory of proof History.T;
wenzelm@5827
    48
wenzelm@5827
    49
exception FAIL of string;
wenzelm@5827
    50
wenzelm@5827
    51
fun app f (ProofHistory x) = ProofHistory (f x);
wenzelm@5827
    52
fun hist_app f = app (History.apply f);
wenzelm@5827
    53
wenzelm@5827
    54
wenzelm@5827
    55
(* generic history operations *)
wenzelm@5827
    56
wenzelm@5827
    57
fun init st = ProofHistory (History.init (((st, Seq.empty), 0), []));
wenzelm@5827
    58
fun current (ProofHistory prf) = fst (fst (fst (History.current prf)));
wenzelm@5827
    59
val clear = app History.clear;
wenzelm@5827
    60
val undo = app History.undo;
wenzelm@5827
    61
val redo = app History.redo;
wenzelm@5827
    62
wenzelm@5944
    63
fun undos n = funpow n undo;
wenzelm@5944
    64
fun redos n = funpow n redo;
wenzelm@5944
    65
wenzelm@5827
    66
wenzelm@5827
    67
(* navigate *)
wenzelm@5827
    68
wenzelm@5827
    69
fun position (ProofHistory prf) = length (snd (History.current prf));
wenzelm@5827
    70
fun nesting (ProofHistory prf) = snd (fst (History.current prf));
wenzelm@5827
    71
wenzelm@5827
    72
fun prev_until msg _ (_, []) = raise FAIL msg
wenzelm@5827
    73
  | prev_until msg pred (_, node :: nodes) =
wenzelm@5827
    74
      if pred node then (node, nodes)
wenzelm@5827
    75
      else prev_until msg pred (node, nodes);
wenzelm@5827
    76
wenzelm@5827
    77
val prev = hist_app (prev_until "no previous proof state" (K true));
wenzelm@5827
    78
fun up prf = hist_app (prev_until "no upper proof state" (fn (_, m) => m < nesting prf)) prf;
wenzelm@5827
    79
val top = hist_app (fn (node, nodes) => (last_elem (node :: nodes), []));
wenzelm@5827
    80
wenzelm@5827
    81
wenzelm@5827
    82
(* backtrack *)
wenzelm@5827
    83
wenzelm@5827
    84
fun back_fun (((_, stq), n), nodes) =
wenzelm@5827
    85
  (case Seq.pull stq of
wenzelm@5827
    86
    None =>
wenzelm@5827
    87
      (case nodes of
wenzelm@5827
    88
        [] => raise FAIL "back: no alternatives"
wenzelm@5827
    89
      | nd :: nds => (writeln "back: trying previous proof state ..."; back_fun (nd, nds)))
wenzelm@5827
    90
  | Some result => ((result, n), nodes));
wenzelm@5827
    91
wenzelm@5827
    92
val back = hist_app back_fun;
wenzelm@5827
    93
wenzelm@5827
    94
wenzelm@5827
    95
(* apply transformer *)
wenzelm@5827
    96
wenzelm@5827
    97
fun gen_apply d f (node as ((st, _), n): node, nodes) =
wenzelm@5827
    98
  (case Seq.pull (f st) of
wenzelm@5827
    99
    None => raise FAIL "empty result sequence -- command failed"
wenzelm@5827
   100
  | Some results => ((results, n + d), node :: nodes));
wenzelm@5827
   101
wenzelm@5827
   102
val applys = hist_app o gen_apply 0;
wenzelm@5827
   103
val applys_open = hist_app o gen_apply 1;
wenzelm@5827
   104
val applys_close = hist_app o gen_apply ~1;
wenzelm@5827
   105
wenzelm@5827
   106
fun apply f = applys (Seq.single o f);
wenzelm@5827
   107
fun apply_open f = applys_open (Seq.single o f);
wenzelm@5827
   108
fun apply_close f = applys_close (Seq.single o f);
wenzelm@6374
   109
fun apply_cond_open do_open f = if do_open then apply_open f else apply f;
wenzelm@5827
   110
wenzelm@5827
   111
end;