src/Pure/Isar/proof_node.ML

more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

(*  Title:      Pure/Isar/proof_node.ML
    Author:     Makarius

Proof nodes with linear position and backtracking.
*)

signature PROOF_NODE =
sig
  type T
  val init: Proof.state -> T
  val current: T -> Proof.state
  val position: T -> int
  val back: T -> T
  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
  val apply: (Proof.state -> Proof.state) -> T -> T
end;

structure Proof_Node: PROOF_NODE =
struct

(* datatype *)

datatype T = Proof_Node of
  (Proof.state *                (*first result*)
   Proof.state Seq.seq) *       (*alternative results*)
  int;                          (*linear proof position*)

fun init st = Proof_Node ((st, Seq.empty), 0);

fun current (Proof_Node ((st, _), _)) = st;
fun position (Proof_Node (_, n)) = n;


(* backtracking *)

fun back (Proof_Node ((_, stq), n)) =
  (case Seq.pull stq of
    NONE => error "back: no alternatives"
  | SOME res => Proof_Node (res, n));


(* apply transformer *)

fun applys f (Proof_Node ((st, _), n)) =
  (case Seq.pull (f st) of
    NONE => error "empty result sequence -- proof command failed"
  | SOME res => Proof_Node (res, n + 1));

fun apply f = applys (Seq.single o f);

end;