src/Pure/Isar/proof_history.ML
author wenzelm
Mon, 09 Nov 1998 15:33:32 +0100
changeset 5827 77071ac7c7b5
child 5944 dcc446da8e19
permissions -rw-r--r--
Histories of proof states, with undo / redo and prev / back.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/proof_history.ML
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     4
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     5
Histories of proof states, with undo / redo and prev / back.
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     6
*)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     7
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     8
signature PROOF_HISTORY =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
     9
sig
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    10
  type T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    11
  exception FAIL of string
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    12
  val init: Proof.state -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    13
  val current: T -> Proof.state
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    14
  val clear: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    15
  val undo: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    16
  val redo: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    17
  val position: T -> int
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    18
  val nesting: T -> int
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    19
  val prev: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    20
  val up: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    21
  val top: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    22
  val back: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    23
  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    24
  val applys_open: (Proof.state -> Proof.state Seq.seq) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    25
  val applys_close: (Proof.state -> Proof.state Seq.seq) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    26
  val apply: (Proof.state -> Proof.state) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    27
  val apply_open: (Proof.state -> Proof.state) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    28
  val apply_close: (Proof.state -> Proof.state) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    29
end;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    30
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    31
structure ProofHistory: PROOF_HISTORY =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    32
struct
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    33
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    34
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    35
(* datatype proof history *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    36
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    37
type node =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    38
 (Proof.state *			(*first result*)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    39
  Proof.state Seq.seq) *	(*alternative results*)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    40
  int;				(*nest level*)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    41
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    42
type proof = node * node list;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    43
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    44
datatype T = ProofHistory of proof History.T;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    45
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    46
exception FAIL of string;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    47
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    48
fun app f (ProofHistory x) = ProofHistory (f x);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    49
fun hist_app f = app (History.apply f);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    50
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    51
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    52
(* generic history operations *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    53
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    54
fun init st = ProofHistory (History.init (((st, Seq.empty), 0), []));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    55
fun current (ProofHistory prf) = fst (fst (fst (History.current prf)));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    56
val clear = app History.clear;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    57
val undo = app History.undo;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    58
val redo = app History.redo;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    59
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    60
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    61
(* navigate *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    62
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    63
fun position (ProofHistory prf) = length (snd (History.current prf));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    64
fun nesting (ProofHistory prf) = snd (fst (History.current prf));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    65
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    66
fun prev_until msg _ (_, []) = raise FAIL msg
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    67
  | prev_until msg pred (_, node :: nodes) =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    68
      if pred node then (node, nodes)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    69
      else prev_until msg pred (node, nodes);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    70
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    71
val prev = hist_app (prev_until "no previous proof state" (K true));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    72
fun up prf = hist_app (prev_until "no upper proof state" (fn (_, m) => m < nesting prf)) prf;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    73
val top = hist_app (fn (node, nodes) => (last_elem (node :: nodes), []));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    74
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    75
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    76
(* backtrack *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    77
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    78
fun back_fun (((_, stq), n), nodes) =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    79
  (case Seq.pull stq of
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    80
    None =>
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    81
      (case nodes of
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    82
        [] => raise FAIL "back: no alternatives"
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    83
      | nd :: nds => (writeln "back: trying previous proof state ..."; back_fun (nd, nds)))
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    84
  | Some result => ((result, n), nodes));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    85
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    86
val back = hist_app back_fun;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    87
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    88
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    89
(* apply transformer *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    90
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    91
fun gen_apply d f (node as ((st, _), n): node, nodes) =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    92
  (case Seq.pull (f st) of
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    93
    None => raise FAIL "empty result sequence -- command failed"
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    94
  | Some results => ((results, n + d), node :: nodes));
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    95
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    96
val applys = hist_app o gen_apply 0;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    97
val applys_open = hist_app o gen_apply 1;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    98
val applys_close = hist_app o gen_apply ~1;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    99
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   100
fun apply f = applys (Seq.single o f);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   101
fun apply_open f = applys_open (Seq.single o f);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   102
fun apply_close f = applys_close (Seq.single o f);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   103
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   104
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
   105
end;