Source file goptions.ml
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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
open Util
open Summary.Stage
type option_name = string list
type option_value =
| BoolValue of bool
| IntValue of int option
| StringValue of string
| StringOptValue of string option
type table_value =
| StringRefValue of string
| QualidRefValue of Libnames.qualid
(** Summary of an option status *)
type option_state = {
opt_depr : Deprecation.t option;
opt_value : option_value;
}
let nickname table = String.concat " " table
let error_no_table_of_this_type ~kind key =
CErrors.user_err
Pp.(str ("There is no " ^ kind ^ "-valued table with this name: \""
^ nickname key ^ "\"."))
let error_undeclared_key key =
CErrors.user_err
Pp.(str ("There is no flag, option or table with this name: \""
^ nickname key ^ "\"."))
type 'a table_of_A = {
add : Environ.env -> 'a -> unit;
remove : Environ.env -> 'a -> unit;
mem : Environ.env -> 'a -> unit;
print : unit -> unit;
}
module MakeTable =
functor
(A : sig
type t
type key
module Set : CSig.SetS with type elt = t
val table : (string * key table_of_A) list ref
val encode : Environ.env -> key -> t
val subst : Mod_subst.substitution -> t -> t
val printer : t -> Pp.t
val key : option_name
val title : string
val member_message : t -> bool -> Pp.t
end) ->
struct
type option_mark =
| GOadd
| GOrmv
let nick = nickname A.key
let () =
if String.List.mem_assoc nick !A.table then
CErrors.user_err
Pp.(strbrk "Sorry, this table name (" ++ str nick
++ strbrk ") is already used.")
module MySet = A.Set
let t = Summary.ref ~stage:Summary.Stage.Synterp MySet.empty ~name:nick
let (add_option,remove_option) =
let cache_options (f,p) = match f with
| GOadd -> t := MySet.add p !t
| GOrmv -> t := MySet.remove p !t in
let load_options i o = if Int.equal i 1 then cache_options o in
let subst_options (subst,(f,p as obj)) =
let p' = A.subst subst p in
if p' == p then obj else
(f,p')
in
let inGo : option_mark * A.t -> Libobject.obj =
Libobject.declare_object {(Libobject.default_object nick) with
Libobject.object_stage = Summary.Stage.Synterp;
Libobject.load_function = load_options;
Libobject.open_function = Libobject.simple_open load_options;
Libobject.cache_function = cache_options;
Libobject.subst_function = subst_options;
Libobject.classify_function = (fun x -> Substitute)}
in
((fun c -> Lib.add_leaf (inGo (GOadd, c))),
(fun c -> Lib.add_leaf (inGo (GOrmv, c))))
let print_table table_name printer table =
let open Pp in
let pp = if MySet.is_empty table then str table_name ++ str " is empty."
else
str table_name ++ str ":" ++ spc() ++
(hov 0 (prlist_with_sep spc printer (MySet.elements table))) ++
str "."
in
Feedback.msg_notice pp
let table_of_A = {
add = (fun env x -> add_option (A.encode env x));
remove = (fun env x -> remove_option (A.encode env x));
mem = (fun env x ->
let y = A.encode env x in
let answer = MySet.mem y !t in
Feedback.msg_info (A.member_message y answer));
print = (fun () -> print_table A.title A.printer !t);
}
let _ = A.table := (nick, table_of_A)::!A.table
let v () = !t
let active x = A.Set.mem x !t
let set x b = if b then add_option x else remove_option x
end
let string_table = ref []
let get_string_table k = String.List.assoc (nickname k) !string_table
module type StringConvertArg =
sig
val key : option_name
val title : string
val member_message : string -> bool -> Pp.t
end
module StringConvert = functor (A : StringConvertArg) ->
struct
type t = string
type key = string
module Set = CString.Set
let table = string_table
let encode _env x = x
let subst _ x = x
let printer = Pp.str
let key = A.key
let title = A.title
let member_message = A.member_message
end
module MakeStringTable =
functor (A : StringConvertArg) -> MakeTable (StringConvert(A))
let ref_table = ref []
let get_ref_table k = String.List.assoc (nickname k) !ref_table
module type RefConvertArg =
sig
type t
module Set : CSig.SetS with type elt = t
val encode : Environ.env -> Libnames.qualid -> t
val subst : Mod_subst.substitution -> t -> t
val printer : t -> Pp.t
val key : option_name
val title : string
val member_message : t -> bool -> Pp.t
end
module RefConvert = functor (A : RefConvertArg) ->
struct
type t = A.t
type key = Libnames.qualid
module Set = A.Set
let table = ref_table
let encode = A.encode
let subst = A.subst
let printer = A.printer
let key = A.key
let title = A.title
let member_message = A.member_message
end
module MakeRefTable =
functor (A : RefConvertArg) -> MakeTable (RefConvert(A))
type iter_table_aux = { aux : 'a. 'a table_of_A -> Environ.env -> 'a -> unit }
let iter_table env f key lv =
let aux = function
| StringRefValue s ->
begin
try f.aux (get_string_table key) env s
with Not_found -> error_no_table_of_this_type ~kind:"string" key
end
| QualidRefValue locqid ->
begin
try f.aux (get_ref_table key) env locqid
with Not_found -> error_no_table_of_this_type ~kind:"qualid" key
end
in
List.iter aux lv
type 'a option_sig = {
optstage : Summary.Stage.t;
optdepr : Deprecation.t option;
optkey : option_name;
optread : unit -> 'a;
optwrite : 'a -> unit }
type option_locality = OptDefault | OptLocal | OptExport | OptGlobal
type option_mod = OptSet | OptAppend
module OptionOrd =
struct
type t = option_name
let compare opt1 opt2 = List.compare String.compare opt1 opt2
end
module OptionMap = Map.Make(OptionOrd)
let value_tab = ref OptionMap.empty
let get_option key = OptionMap.find key !value_tab
let check_key key = try
let _ = get_option key in
CErrors.user_err Pp.(str "Sorry, this option name ("
++ str (nickname key) ++ str ") is already used.")
with Not_found ->
if String.List.mem_assoc (nickname key) !string_table
|| String.List.mem_assoc (nickname key) !ref_table
then CErrors.user_err Pp.(str "Sorry, this option name ("
++ str (nickname key) ++ str ") is already used.")
open Libobject
let warn_deprecated_option =
Deprecation.create_warning ~object_name:"Option" ~warning_name_if_no_since:"deprecated-option"
(fun key -> Pp.str (nickname key))
let declare_option cast uncast append ?(preprocess = fun x -> x)
{ optstage=stage; optdepr=depr; optkey=key; optread=read; optwrite=write } =
check_key key;
let default = read() in
let change =
let () = Summary.declare_summary (nickname key)
{ stage;
Summary.freeze_function = read;
Summary.unfreeze_function = write;
Summary.init_function = (fun () -> write default) } in
let cache_options (l,m,v) =
match m with
| OptSet -> write v
| OptAppend -> write (append (read ()) v) in
let load_options i (l, _, _ as o) = match l with
| OptGlobal -> cache_options o
| OptExport -> ()
| OptLocal | OptDefault ->
assert false
in
let open_options i (l, _, _ as o) = match l with
| OptExport -> if Int.equal i 1 then cache_options o
| OptGlobal -> ()
| OptLocal | OptDefault ->
assert false
in
let subst_options (subst,obj) = obj in
let discharge_options (l,_,_ as o) =
match l with OptLocal -> None | (OptExport | OptGlobal | OptDefault) -> Some o in
let classify_options (l,_,_) =
match l with (OptExport | OptGlobal) -> Substitute | (OptLocal | OptDefault) -> Dispose in
let options : option_locality * option_mod * _ -> obj =
declare_object
{ (default_object (nickname key)) with
object_stage = stage;
load_function = load_options;
open_function = simple_open open_options;
cache_function = cache_options;
subst_function = subst_options;
discharge_function = discharge_options;
classify_function = classify_options } in
(fun l m v -> let v = preprocess v in Lib.add_leaf (options (l, m, v)))
in
let warn () = depr |> Option.iter (fun depr -> warn_deprecated_option (key,depr)) in
let cread () = cast (read ()) in
let cwrite l v = warn (); change l OptSet (uncast v) in
let cappend l v = warn (); change l OptAppend (uncast v) in
value_tab := OptionMap.add key (depr, stage, (cread,cwrite,cappend)) !value_tab
let declare_int_option =
declare_option
(fun v -> IntValue v)
(function IntValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
(fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
let declare_bool_option =
declare_option
(fun v -> BoolValue v)
(function BoolValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
(fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
let declare_string_option =
declare_option
(fun v -> StringValue v)
(function StringValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
(fun x y -> x^","^y)
let declare_stringopt_option =
declare_option
(fun v -> StringOptValue v)
(function StringOptValue v -> v | _ -> CErrors.anomaly (Pp.str "async_option."))
(fun _ _ -> CErrors.anomaly (Pp.str "async_option."))
type 'a getter = { get : unit -> 'a }
type 'a opt_decl = ?stage:Summary.Stage.t -> ?depr:Deprecation.t -> key:option_name -> value:'a -> unit -> 'a getter
let declare_int_option_and_ref ?(stage=Interp) ?depr ~key ~(value:int) () =
let r_opt = ref value in
let optwrite v = r_opt := Option.default value v in
let optread () = Some !r_opt in
let () = declare_int_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread;
optwrite;
} in
{ get = fun () -> !r_opt }
let declare_intopt_option_and_ref ?(stage=Interp) ?depr ~key ~value () =
let r_opt = ref value in
let optwrite v = r_opt := v in
let optread () = !r_opt in
let () = declare_int_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = optread }
let declare_nat_option_and_ref ?(stage=Interp) ?depr ~key ~(value:int) () =
assert (value >= 0);
let r_opt = ref value in
let optwrite v =
let v = Option.default value v in
if v < 0 then
CErrors.user_err Pp.(str "This option expects a non-negative value.");
r_opt := v
in
let optread () = Some !r_opt in
let () = declare_int_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = fun () -> !r_opt }
let declare_bool_option_and_ref ?(stage=Interp) ?depr ~key ~(value:bool) () =
let r_opt = ref value in
let optwrite v = r_opt := v in
let optread () = !r_opt in
let () = declare_bool_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = optread }
let declare_string_option_and_ref ?(stage=Interp) ?depr ~key ~(value:string) () =
let r_opt = ref value in
let optwrite v = r_opt := Option.default value v in
let optread () = Some !r_opt in
let () = declare_stringopt_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = fun () -> !r_opt }
let declare_stringopt_option_and_ref ?(stage=Interp) ?depr ~key ~value () =
let r_opt = ref value in
let optwrite v = r_opt := v in
let optread () = !r_opt in
let () = declare_stringopt_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = optread }
let declare_interpreted_string_option_and_ref from_string to_string ?(stage=Interp) ?depr ~key ~(value:'a) () =
let r_opt = ref value in
let optwrite v = r_opt := Option.default value @@ Option.map from_string v in
let optread () = Some (to_string !r_opt) in
let () = declare_stringopt_option {
optstage = stage;
optdepr = depr;
optkey = key;
optread; optwrite
} in
{ get = fun () -> !r_opt }
let warn_unknown_option =
CWarnings.create
~name:"unknown-option"
Pp.(fun key -> strbrk "There is no flag or option with this name: \"" ++
str (nickname key) ++ str "\".")
let get_option_value key =
try
let (_,_,(read,write,append)) = get_option key in
Some read
with Not_found -> None
(** Sets the option only if [stage] matches the option declaration or if [stage]
is omitted. If the option is not found, a warning is emitted only if the stage
is [Interp] or omitted. *)
let set_option_value ?(locality = OptDefault) ?stage check_and_cast key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> begin match stage with None | Some Summary.Stage.Interp -> warn_unknown_option key | _ -> () end
| Some (depr, option_stage, (read,write,append)) ->
if Option.cata (fun s -> s = option_stage) true stage then
write locality (check_and_cast v (read ()))
let bad_type_error ~expected ~got =
CErrors.user_err Pp.(strbrk "Bad type of value for this option:" ++ spc()
++ str "expected " ++ str expected ++ str ", got " ++ str got ++ str ".")
let error_flag () =
CErrors.user_err Pp.(str "This is a flag. It does not take a value.")
let check_int_value v = function
| BoolValue _ -> error_flag ()
| IntValue _ -> IntValue v
| StringValue _ | StringOptValue _ ->
bad_type_error ~expected:"string" ~got:"int"
let check_bool_value v = function
| BoolValue _ -> BoolValue v
| _ ->
CErrors.user_err
Pp.(str "This is an option. A value must be provided.")
let check_string_value v = function
| BoolValue _ -> error_flag ()
| IntValue _ -> bad_type_error ~expected:"int" ~got:"string"
| StringValue _ -> StringValue v
| StringOptValue _ -> StringOptValue (Some v)
let check_unset_value v = function
| BoolValue _ -> BoolValue false
| IntValue _ -> IntValue None
| StringOptValue _ -> StringOptValue None
| StringValue _ ->
CErrors.user_err
Pp.(str "This option does not support the \"Unset\" command.")
let set_int_option_value_gen ?locality ?stage =
set_option_value ?locality ?stage check_int_value
let set_bool_option_value_gen ?locality ?stage key v =
set_option_value ?locality ?stage check_bool_value key v
let set_string_option_value_gen ?locality ?stage =
set_option_value ?locality ?stage check_string_value
let unset_option_value_gen ?locality ?stage key =
set_option_value ?locality ?stage check_unset_value key ()
let set_string_option_append_value_gen ?(locality = OptDefault) ?stage key v =
let opt = try Some (get_option key) with Not_found -> None in
match opt with
| None -> warn_unknown_option key
| Some (depr, option_stage, (read,write,append)) ->
if Option.cata (fun s -> s = option_stage) true stage then
append locality (check_string_value v (read ()))
let set_int_option_value ?stage opt v = set_int_option_value_gen ?stage opt v
let set_bool_option_value ?stage opt v = set_bool_option_value_gen ?stage opt v
let set_string_option_value ?stage opt v = set_string_option_value_gen ?stage opt v
let msg_option_value = Pp.(function
| BoolValue true -> str "on"
| BoolValue false -> str "off"
| IntValue (Some n) -> int n
| IntValue None -> str "undefined"
| StringValue s -> quote (str s)
| StringOptValue None -> str "undefined"
| StringOptValue (Some s) -> quote (str s))
let print_option_value key =
let (depr, _stage, (read,_,_)) = get_option key in
let s = read () in
match s with
| BoolValue b ->
Feedback.msg_notice Pp.(prlist_with_sep spc str key ++ str " is "
++ str (if b then "on" else "off"))
| _ ->
Feedback.msg_notice Pp.(str "Current value of "
++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s)
let get_tables () =
let tables = !value_tab in
let fold key (depr, _stage, (read,_,_)) accu =
let state = {
opt_depr = depr;
opt_value = read ();
} in
OptionMap.add key state accu
in
OptionMap.fold fold tables OptionMap.empty
let print_tables () =
let open Pp in
let print_option key value depr =
let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value value in
let depr = pr_opt (fun depr ->
hov 2
(str "[DEPRECATED" ++
pr_opt (fun since -> str "since " ++ str since) depr.Deprecation.since ++
pr_opt str depr.Deprecation.note ++
str "]"))
depr
in
msg ++ depr ++ fnl()
in
str "Options:" ++ fnl () ++
OptionMap.fold
(fun key (depr, _stage, (read,_,_)) p ->
p ++ print_option key (read ()) depr)
!value_tab (mt ()) ++
str "Tables:" ++ fnl () ++
List.fold_right
(fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ())
!string_table (mt ()) ++
List.fold_right
(fun (nickkey,_) p -> p ++ str " " ++ str nickkey ++ fnl ())
!ref_table (mt ()) ++
fnl ()