author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 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 |
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 | 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)) = |
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; |