src/Pure/Isar/proof_node.ML
author blanchet
Fri, 01 Aug 2014 14:43:57 +0200
changeset 57743 0af2d5dfb0ac
parent 49863 b5fb6e7f8d81
permissions -rw-r--r--
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/proof_node.ML
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     3
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     4
Proof nodes with linear position and backtracking.
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     5
*)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     6
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     7
signature PROOF_NODE =
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     8
sig
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
     9
  type T
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    10
  val init: Proof.state -> T
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    11
  val current: T -> Proof.state
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    12
  val position: T -> int
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    13
  val back: T -> T
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 33390
diff changeset
    14
  val applys: (Proof.state -> Proof.state Seq.result Seq.seq) -> T -> T
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    15
  val apply: (Proof.state -> Proof.state) -> T -> T
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    16
end;
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    17
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    18
structure Proof_Node: PROOF_NODE =
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    19
struct
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    20
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    21
(* datatype *)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    22
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    23
datatype T = Proof_Node of
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    24
  (Proof.state *                (*first result*)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    25
   Proof.state Seq.seq) *       (*alternative results*)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    26
  int;                          (*linear proof position*)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    27
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    28
fun init st = Proof_Node ((st, Seq.empty), 0);
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    29
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    30
fun current (Proof_Node ((st, _), _)) = st;
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    31
fun position (Proof_Node (_, n)) = n;
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    32
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    33
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    34
(* backtracking *)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    35
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    36
fun back (Proof_Node ((_, stq), n)) =
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    37
  (case Seq.pull stq of
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    38
    NONE => error "back: no alternatives"
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    39
  | SOME res => Proof_Node (res, n));
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    40
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    41
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    42
(* apply transformer *)
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    43
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 32784
diff changeset
    44
fun applys f (Proof_Node ((st, _), n)) =
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 33390
diff changeset
    45
  Proof_Node (Seq.first_result "Empty result sequence -- proof command failed" (f st), n + 1);
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    46
49863
b5fb6e7f8d81 more informative errors for 'proof' and 'apply' steps;
wenzelm
parents: 33390
diff changeset
    47
fun apply f = applys (Seq.single o Seq.Result o f);
27561
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    48
a928e3439067 Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff changeset
    49
end;