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
|
(* $Id$ *)
open Pp
open Util
open Names
open Library
(* The pattern table for tactics. *)
(* The idea is that we want to write tactic files which are only
"activated" when certain modules are loaded and imported. Already,
the question of how to store the tactics is hard, and we will not
address that here. However, the question arises of how to store
the patterns that we will want to use for term-destructuring, and
the solution proposed is that we will store patterns with a
"module-marker", telling us which modules have to be open in order
to use the pattern. So we will write:
let mark = make_module_marker ["<module-name>";<module-name>;...]
let p1 = put_pat mark "<parseable pattern goes here>"
And now, we can use:
(get p1)
to get the term which corresponds to this pattern, already parsed
and with the global names adjusted.
In other words, we will have the term which we would have had if we
had done an:
constr_of_com mt_ctxt (initial_sign()) "<text here>"
except that it will be computed at module-opening time, rather than
at tactic-application time. The ONLY difference will be that
no implicit syntax resolution will happen.
So the entries we provide are:
type module_mark
value make_module_marker : string list -> module_mark
type marked_term
value put_pat : module_mark -> string -> marked_term
value get_pat : marked_term -> constr
*)
type module_mark = Mmk of int
let path_mark_bij = ref (Bij.empty : (string list,module_mark) Bij.t)
let mmk_ctr = ref 0
let new_mmk () = (incr mmk_ctr; !mmk_ctr)
let make_module_marker sl =
let sorted_sl = Sort.list (<) sl in
try
Bij.map !path_mark_bij sorted_sl
with Not_found -> begin
let mmk = Mmk(new_mmk()) in
path_mark_bij := Bij.add !path_mark_bij (sorted_sl,mmk);
mmk
end
let mark_satisfied mmk =
let spl = Bij.pam !path_mark_bij mmk in
list_subset spl (loaded_modules())
(* src_tab: for each module_mark, stores the tickets of objects which
need to be compiled when that mark becomes active.
obj_tab: for each ticket, stores the (possibly nonexistent)
compiled object
ticket_tab: for each ticket, stores its module_mark and the string
(source)
string_tab: for each string * module_mark, stores the ticket. *)
type 'a stock_args = {
name : string;
proc : string -> 'a }
type 'a stock = {
mutable src_tab : (module_mark,int) Gmapl.t;
mutable obj_tab : (int,'a) Gmap.t;
mutable ticket_string_bij : (int,string * module_mark) Bij.t;
args : 'a stock_args }
type 'a stocked = int
let stock_ctr = ref 0
let new_stock () = (incr stock_ctr; !stock_ctr)
let make_stock args =
{ src_tab = Gmapl.empty;
obj_tab = Gmap.empty;
ticket_string_bij = Bij.empty;
args = args }
let stock stock mmk s =
try
Bij.pam stock.ticket_string_bij (s,mmk)
with Not_found -> begin
let idx = new_stock() in
stock.src_tab <- Gmapl.add mmk idx stock.src_tab;
stock.ticket_string_bij <- Bij.add stock.ticket_string_bij (idx,(s,mmk));
idx
end
let pr_mm mm =
let sl = Bij.pam !path_mark_bij mm in
prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) sl
(* TODO: traiter a part les erreurs provenant de stock.args.proc
( = parsing quand [so]pattern appelle retrieve)
-> eviter d'avoir l'erreur stocked datum *)
let retrieve stock idx =
try
Gmap.find idx stock.obj_tab
with Not_found ->
let (s,mmk) = Bij.map stock.ticket_string_bij idx in
if mark_satisfied mmk then
try
let c = stock.args.proc s in
stock.obj_tab <- Gmap.add idx c stock.obj_tab;
c
with e -> begin
mSGNL [< 'sTR"Processing of the stocked datum " ; 'sTR s ;
'sTR" failed." ; 'fNL;
Library.fmt_modules_state() >];
raise e
end
else
errorlabstrm "Stock.retrieve"
[< 'sTR"The stocked object "; 'sTR s; 'sTR" was not compilable";
'fNL; 'sTR"Its module mark was: "; pr_mm mmk ; 'fNL ;
Library.fmt_modules_state() >]
|
