author | wenzelm |
Wed, 28 Dec 2011 13:00:51 +0100 | |
changeset 46003 | c0fe5e8e4864 |
parent 33390 | 5b499f36dd25 |
child 49863 | b5fb6e7f8d81 |
permissions | -rw-r--r-- |
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 |
a928e3439067
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff
changeset
|
14 |
val applys: (Proof.state -> Proof.state Seq.seq) -> T -> T |
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 | 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 | 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 | 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 | 30 |
fun current (Proof_Node ((st, _), _)) = st; |
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 | 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 | 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 | 44 |
fun applys f (Proof_Node ((st, _), n)) = |
27561
a928e3439067
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff
changeset
|
45 |
(case Seq.pull (f st) of |
a928e3439067
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff
changeset
|
46 |
NONE => error "empty result sequence -- proof command failed" |
33390 | 47 |
| SOME res => Proof_Node (res, n + 1)); |
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 |
fun apply f = applys (Seq.single o f); |
a928e3439067
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff
changeset
|
50 |
|
a928e3439067
Proof nodes with linear position and backtracking (replaces obsolete proof_history.ML).
wenzelm
parents:
diff
changeset
|
51 |
end; |