src/Pure/Isar/proof_node.ML
author wenzelm
Mon May 03 14:25:56 2010 +0200 (2010-05-03)
changeset 36610 bafd82950e24
parent 33390 5b499f36dd25
child 49863 b5fb6e7f8d81
permissions -rw-r--r--
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
     1 (*  Title:      Pure/Isar/proof_node.ML
     2     Author:     Makarius
     3 
     4 Proof nodes with linear position and backtracking.
     5 *)
     6 
     7 signature PROOF_NODE =
     8 sig
     9   type T
    10   val init: Proof.state -> T
    11   val current: T -> Proof.state
    12   val position: T -> int
    13   val back: T -> T
    14   val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T
    15   val apply: (Proof.state -> Proof.state) -> T -> T
    16 end;
    17 
    18 structure Proof_Node: PROOF_NODE =
    19 struct
    20 
    21 (* datatype *)
    22 
    23 datatype T = Proof_Node of
    24   (Proof.state *                (*first result*)
    25    Proof.state Seq.seq) *       (*alternative results*)
    26   int;                          (*linear proof position*)
    27 
    28 fun init st = Proof_Node ((st, Seq.empty), 0);
    29 
    30 fun current (Proof_Node ((st, _), _)) = st;
    31 fun position (Proof_Node (_, n)) = n;
    32 
    33 
    34 (* backtracking *)
    35 
    36 fun back (Proof_Node ((_, stq), n)) =
    37   (case Seq.pull stq of
    38     NONE => error "back: no alternatives"
    39   | SOME res => Proof_Node (res, n));
    40 
    41 
    42 (* apply transformer *)
    43 
    44 fun applys f (Proof_Node ((st, _), n)) =
    45   (case Seq.pull (f st) of
    46     NONE => error "empty result sequence -- proof command failed"
    47   | SOME res => Proof_Node (res, n + 1));
    48 
    49 fun apply f = applys (Seq.single o f);
    50 
    51 end;