src/Pure/Isar/proof_history.ML
author wenzelm
Thu, 26 Aug 1999 19:01:22 +0200
changeset 7366 22a64baa7013
parent 6902 5f126c495771
child 7731 51d59734743d
permissions -rw-r--r--
back: recur flag;
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
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    12
  val position: T -> int
6684
4f859545bd92 adapted to History changes;
wenzelm
parents: 6374
diff changeset
    13
  val init: int option -> Proof.state -> T
4f859545bd92 adapted to History changes;
wenzelm
parents: 6374
diff changeset
    14
  val is_initial: T -> bool
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    15
  val current: T -> Proof.state
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    16
  val clear: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    17
  val undo: T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    18
  val redo: T -> T
7366
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    19
  val back: bool -> T -> T
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    20
  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
    21
  val apply: (Proof.state -> Proof.state) -> T -> T
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    22
end;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    23
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    24
structure ProofHistory: PROOF_HISTORY =
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    25
struct
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    26
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    27
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    28
(* datatype proof history *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    29
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    30
type node =
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    31
  Proof.state *			(*first result*)
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    32
  Proof.state Seq.seq; 		(*alternative results*)
5827
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
type proof = node * node list;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    35
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    36
datatype T = ProofHistory of proof History.T;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    37
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    38
exception FAIL of string;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    39
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    40
fun app f (ProofHistory x) = ProofHistory (f x);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    41
fun hist_app f = app (History.apply f);
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    42
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    43
fun position (ProofHistory prf) = length (snd (History.current prf));
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    44
5827
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
(* generic history operations *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    47
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    48
fun init lim st = ProofHistory (History.init lim ((st, Seq.empty), []));
6684
4f859545bd92 adapted to History changes;
wenzelm
parents: 6374
diff changeset
    49
fun is_initial (ProofHistory prf) = History.is_initial prf;
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    50
fun current (ProofHistory prf) = fst (fst (History.current prf));
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    51
val clear = app History.clear;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    52
val undo = app History.undo;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    53
val redo = app History.redo;
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    54
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    55
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    56
(* backtrack *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    57
7366
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    58
fun back_fun recur ((_, stq), nodes) =
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    59
  (case Seq.pull stq of
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    60
    None =>
7366
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    61
      if recur andalso not (null nodes) then
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    62
        (writeln "back: trying previous proof state ..."; back_fun recur (hd nodes, tl nodes))
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    63
      else raise FAIL "back: no alternatives"
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    64
  | Some result => (result, nodes));
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    65
7366
22a64baa7013 back: recur flag;
wenzelm
parents: 6902
diff changeset
    66
val back = hist_app o back_fun;
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    67
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    68
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    69
(* apply transformer *)
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    70
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    71
fun applys f = hist_app (fn (node as (st, _), nodes) =>
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    72
  (case Seq.pull (f st) of
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    73
    None => raise FAIL "empty result sequence -- proof command failed"
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    74
  | Some results => (results, node :: nodes)));
5827
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
fun apply f = applys (Seq.single o f);
6902
5f126c495771 removed nesting (unused);
wenzelm
parents: 6684
diff changeset
    77
5827
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    78
77071ac7c7b5 Histories of proof states, with undo / redo and prev / back.
wenzelm
parents:
diff changeset
    79
end;