1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
type proof_node = {
(* In saw mode, identation depends directly from
* the remaining subgoals to be proven
* *)
remaining_subgoals : int;
(* A subgoal stack is a list of remaining subgoals
* at each "keypoint";
*
* Imagine you have to solve a subgoal "S", and you
* know that "n" subgoals remain to be proved.
*
* After running a tactic, let us call "m" the number of
* remaining subgoals to be proven; 3 cases occur:
* - if "m" > "n", then you know that you have entered a
* new indentation level and that you will close it
* once the remaining goals are below "n", so
* we push "n" in this case to keep track of it
* - if "m" = "n" then nothing changes
* - if "m" < "n" then according to the first case we
* have to look if the top of our stack is below "n";
* if so we pop our stack, so that our indentation
* level is always equal to depth of our stack
* *)
subgoals_stack : int list;
(* [first_step] means that the number of remaining
* subgoals has changed (cases 1 and 3 of previous enumeration)
* *)
first_step : bool;
}
type interp_node = {
opened_sections : int;
opened_modules : int;
interp_mode : proof_node option;
}
(* In the first step, we have not yet any interp node,
* but we need one to use [compute_interp_node],
* so we provide one
* *)
let first_interp_node = {
opened_sections = 0;
opened_modules = 0;
interp_mode = None;
}
(* this functions finds how many modules and sections are opened *)
let get_opened lstk =
let rec get_opened lstk (sections, modules) =
match lstk with
| [] -> (sections, modules)
| (_, node)::lstk -> get_opened lstk
( match node with
| Lib.OpenedModule(_,_,_)
| Lib.OpenedModtype(_,_) ->
sections, 1+modules
| Lib.OpenedSection(_,_) ->
1+sections, modules
(* | Lib.ClosedModule(_)
| Lib.ClosedModtype(_) ->
sections, modules-1
| Lib.ClosedSection(_) ->
sections-1, modules*)
| _ -> sections, modules
)
in
match lstk with
| Ide_blob.Fail(_,_) -> (0,0)
| Ide_blob.Good lstk -> get_opened lstk (0, 0)
(* given the current pftreestate
* (or None if we are neither in proof nor tactic mode)
* and the previous proof_node, we can compute the
* current proof_node
* *)
let compute_interp_node pftso pno lstk =
let (i_mode, o_msg) =
match pftso with
| Ide_blob.Fail(_,_) -> (None, None)
| Ide_blob.Good (Ide_blob.Message s) -> (None, None)
| Ide_blob.Good (Ide_blob.Goals goals) ->
(* we need the number of remaining subgoals in tactic mode *)
let rs = List.length goals in
(* and the indication that the proof is really terminated in case
* rs = 0 for declarative mode
* *)
if rs = 0
then (None, None)
else
let (fs, (ss, e_msg)) =
match pno.interp_mode with
| None -> (true, ([], None))
| Some pn ->
let (fs, (ss, e_msg)) =
if rs = pn.remaining_subgoals
then (false, (pn.subgoals_stack, None))
else (true,
if rs > pn.remaining_subgoals
then (pn.remaining_subgoals::pn.subgoals_stack, None)
else let rec unhead l = match l with
| [] -> ([], Some("Indentation system broken"))
|h::t-> if h = pn.remaining_subgoals
then unhead t
else (h::t, None)
in unhead pn.subgoals_stack)
in (fs, (ss, e_msg))
in
(Some { remaining_subgoals = rs;
subgoals_stack = ss;
first_step = fs;
},
e_msg)
in
let (s, m) = get_opened lstk in
{ opened_sections = s;
opened_modules = m;
interp_mode = i_mode;
}, o_msg
type nesting = {
module_levels : int; (* number of opened modules *)
section_levels : int; (* number of opened sections *)
subgoal_levels : int; (* number of remaining subgoals *)
tactic_levels : int; (* number of imbricated proofs *)
tactic_alinea : bool; (* are we entering a new node? *)
}
let compute_nesting pno =
let subgoals, tactic_depth, alinea =
match pno.interp_mode with
| None -> (0, 0, true)
| Some pn -> (pn.remaining_subgoals,
List.length pn.subgoals_stack,
pn.first_step)
in
{ section_levels = pno.opened_sections;
module_levels = pno.opened_modules;
subgoal_levels = subgoals;
tactic_levels = tactic_depth;
tactic_alinea = alinea;
}
|
