src/Pure/Isar/proof_node.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 33390 5b499f36dd25
child 49863 b5fb6e7f8d81
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
wenzelm@27561
     1
(*  Title:      Pure/Isar/proof_node.ML
wenzelm@27561
     2
    Author:     Makarius
wenzelm@27561
     3
wenzelm@27561
     4
Proof nodes with linear position and backtracking.
wenzelm@27561
     5
*)
wenzelm@27561
     6
wenzelm@27561
     7
signature PROOF_NODE =
wenzelm@27561
     8
sig
wenzelm@27561
     9
  type T
wenzelm@27561
    10
  val init: Proof.state -> T
wenzelm@27561
    11
  val current: T -> Proof.state
wenzelm@27561
    12
  val position: T -> int
wenzelm@27561
    13
  val back: T -> T
wenzelm@27561
    14
  val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
wenzelm@27561
    15
  val apply: (Proof.state -> Proof.state) -> T -> T
wenzelm@27561
    16
end;
wenzelm@27561
    17
wenzelm@33390
    18
structure Proof_Node: PROOF_NODE =
wenzelm@27561
    19
struct
wenzelm@27561
    20
wenzelm@27561
    21
(* datatype *)
wenzelm@27561
    22
wenzelm@33390
    23
datatype T = Proof_Node of
wenzelm@27561
    24
  (Proof.state *                (*first result*)
wenzelm@27561
    25
   Proof.state Seq.seq) *       (*alternative results*)
wenzelm@27561
    26
  int;                          (*linear proof position*)
wenzelm@27561
    27
wenzelm@33390
    28
fun init st = Proof_Node ((st, Seq.empty), 0);
wenzelm@27561
    29
wenzelm@33390
    30
fun current (Proof_Node ((st, _), _)) = st;
wenzelm@33390
    31
fun position (Proof_Node (_, n)) = n;
wenzelm@27561
    32
wenzelm@27561
    33
wenzelm@27561
    34
(* backtracking *)
wenzelm@27561
    35
wenzelm@33390
    36
fun back (Proof_Node ((_, stq), n)) =
wenzelm@27561
    37
  (case Seq.pull stq of
wenzelm@27561
    38
    NONE => error "back: no alternatives"
wenzelm@33390
    39
  | SOME res => Proof_Node (res, n));
wenzelm@27561
    40
wenzelm@27561
    41
wenzelm@27561
    42
(* apply transformer *)
wenzelm@27561
    43
wenzelm@33390
    44
fun applys f (Proof_Node ((st, _), n)) =
wenzelm@27561
    45
  (case Seq.pull (f st) of
wenzelm@27561
    46
    NONE => error "empty result sequence -- proof command failed"
wenzelm@33390
    47
  | SOME res => Proof_Node (res, n + 1));
wenzelm@27561
    48
wenzelm@27561
    49
fun apply f = applys (Seq.single o f);
wenzelm@27561
    50
wenzelm@27561
    51
end;