src/Pure/Isar/proof_node.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29606 fedb8be05f24
child 32784 1a5dde5079ac
permissions -rw-r--r--
use long names for old-style fold combinators;
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@27561
    18
structure ProofNode: PROOF_NODE =
wenzelm@27561
    19
struct
wenzelm@27561
    20
wenzelm@27561
    21
(* datatype *)
wenzelm@27561
    22
wenzelm@27561
    23
datatype T = ProofNode 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@27561
    28
fun init st = ProofNode ((st, Seq.empty), 0);
wenzelm@27561
    29
wenzelm@27561
    30
fun current (ProofNode ((st, _), _)) = st;
wenzelm@27561
    31
fun position (ProofNode (_, n)) = n;
wenzelm@27561
    32
wenzelm@27561
    33
wenzelm@27561
    34
(* backtracking *)
wenzelm@27561
    35
wenzelm@27561
    36
fun back (ProofNode ((_, stq), n)) =
wenzelm@27561
    37
  (case Seq.pull stq of
wenzelm@27561
    38
    NONE => error "back: no alternatives"
wenzelm@27561
    39
  | SOME res => ProofNode (res, n));
wenzelm@27561
    40
wenzelm@27561
    41
wenzelm@27561
    42
(* apply transformer *)
wenzelm@27561
    43
wenzelm@27561
    44
fun applys f (ProofNode (node as (st, _), n)) =
wenzelm@27561
    45
  (case Seq.pull (f st) of
wenzelm@27561
    46
    NONE => error "empty result sequence -- proof command failed"
wenzelm@27561
    47
  | SOME res => ProofNode (res, n + 1));
wenzelm@27561
    48
wenzelm@27561
    49
fun apply f = applys (Seq.single o f);
wenzelm@27561
    50
wenzelm@27561
    51
end;