summaryrefslogtreecommitdiff
path: root/library/goptions.ml
blob: cbf585409528220a9a253f930908b1080442de6f (plain)
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
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* This module manages customization parameters at the vernacular level     *)

open Pp
open Util
open Libobject
open Names
open Libnames
open Term
open Nametab
open Mod_subst

open Goptionstyp

type option_name = Goptionstyp.option_name

(****************************************************************************)
(* 0- Common things                                                         *)

let nickname table = String.concat " " table

let error_undeclared_key key =
  error ((nickname key)^": no table or option of this type")

(****************************************************************************)
(* 1- Tables                                                                *)

class type ['a] table_of_A =
object
  method add : 'a -> unit
  method remove : 'a -> unit
  method mem : 'a -> unit
  method print : unit
end

module MakeTable =
  functor
   (A : sig
	  type t
	  type key
	  val table : (string * key table_of_A) list ref
	  val encode : key -> t
	  val subst : substitution -> t -> t
          val printer : t -> std_ppcmds
          val key : option_name
          val title : string
          val member_message : t -> bool -> std_ppcmds
          val synchronous : bool
        end) ->
  struct
    type option_mark =
      | GOadd
      | GOrmv

    let nick = nickname A.key

    let _ =
      if List.mem_assoc nick !A.table then
	error "Sorry, this table name is already used."

    module MySet = Set.Make (struct type t = A.t let compare = compare end)

    let t = ref (MySet.empty : MySet.t)

    let _ =
      if A.synchronous then
	let freeze () = !t in
	let unfreeze c = t := c in
	let init () = t := MySet.empty in
	Summary.declare_summary nick
          { Summary.freeze_function = freeze;
            Summary.unfreeze_function = unfreeze;
            Summary.init_function = init }

    let (add_option,remove_option) =
      if A.synchronous then
        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 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 -> obj =
          Libobject.declare_object {(Libobject.default_object nick) with
                Libobject.load_function = load_options;
		Libobject.open_function = load_options;
		Libobject.cache_function = cache_options;
		Libobject.subst_function = subst_options;
		Libobject.classify_function = (fun x -> Substitute x)}
	in
        ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
         (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
      else
        ((fun c -> t := MySet.add c !t),
         (fun c -> t := MySet.remove c !t))

    let print_table table_name printer table =
      msg (str table_name ++
	   (hov 0
	      (if MySet.is_empty table then str "None" ++ fnl ()
               else MySet.fold
		 (fun a b -> printer a ++ spc () ++ b)
		 table (mt ()) ++ fnl ())))

    class table_of_A () =
    object
      method add x = add_option (A.encode x)
      method remove x = remove_option (A.encode x)
      method mem x =
	let y = A.encode x in
        let answer = MySet.mem y !t in
        msg (A.member_message y answer ++ fnl ())
      method print = print_table A.title A.printer !t
    end

    let _ = A.table := (nick,new table_of_A ())::!A.table
    let active c = MySet.mem c !t
    let elements () = MySet.elements !t
  end

let string_table = ref []

let get_string_table k = List.assoc (nickname k) !string_table

module type StringConvertArg =
sig
  val key : option_name
  val title : string
  val member_message : string -> bool -> std_ppcmds
  val synchronous : bool
end

module StringConvert = functor (A : StringConvertArg) ->
struct
  type t = string
  type key = string
  let table = string_table
  let encode x = x
  let subst _ x = x
  let printer = str
  let key = A.key
  let title = A.title
  let member_message = A.member_message
  let synchronous = A.synchronous
end

module MakeStringTable =
  functor (A : StringConvertArg) -> MakeTable (StringConvert(A))

let ref_table = ref []

let get_ref_table k = List.assoc (nickname k) !ref_table

module type RefConvertArg =
sig
  type t
  val encode : reference -> t
  val subst : substitution -> t -> t
  val printer : t -> std_ppcmds
  val key : option_name
  val title : string
  val member_message : t -> bool -> std_ppcmds
  val synchronous : bool
end

module RefConvert = functor (A : RefConvertArg) ->
struct
  type t = A.t
  type key = reference
  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
  let synchronous = A.synchronous
end

module MakeRefTable =
  functor (A : RefConvertArg) -> MakeTable (RefConvert(A))

(****************************************************************************)
(* 2- Flags.                                                              *)

type 'a option_sig = {
  optsync  : bool;
  optdepr  : bool;
  optname  : string;
  optkey   : option_name;
  optread  : unit -> 'a;
  optwrite : 'a -> unit }

type option_type = bool * (unit -> option_value) -> (option_value -> unit)

module OptionMap =
  Map.Make (struct  type t = option_name let compare = compare end)

let value_tab = ref OptionMap.empty

(* This raises Not_found if option of key [key] is unknown *)

let get_option key = OptionMap.find key !value_tab

let check_key key = try
  let _ = get_option key in
  error "Sorry, this option name is already used."
with Not_found ->
  if List.mem_assoc (nickname key) !string_table
    or List.mem_assoc (nickname key) !ref_table
  then error "Sorry, this option name is already used."

open Summary
open Libobject
open Lib

let declare_option cast uncast
  { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
  check_key key;
  let default = read() in
  (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
      That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
       lists of strings *without* spaces. *)
  let (write,lwrite,gwrite) = if sync then
    let ldecl_obj = (* "Local": doesn't survive section or modules. *)
      declare_object {(default_object ("L  "^nickname key)) with
		       cache_function = (fun (_,v) -> write v);
		       classify_function = (fun _ -> Dispose)}
    in
    let decl_obj = (* default locality: survives sections but not modules. *)
      declare_object {(default_object (nickname key)) with
		       cache_function = (fun (_,v) -> write v);
		       classify_function = (fun _ -> Dispose);
		       discharge_function = (fun (_,v) -> Some v)}
    in
    let gdecl_obj = (* "Global": survives section and modules. *)
      declare_object {(default_object ("G  "^nickname key)) with
		       cache_function = (fun (_,v) -> write v);
		       classify_function = (fun v -> Substitute v);
		       subst_function = (fun (_,v) -> v);
		       discharge_function = (fun (_,v) -> Some v);
		       load_function = (fun _ (_,v) -> write v)}
    in
    let _ = declare_summary (nickname key)
	     { freeze_function = read;
	       unfreeze_function = write;
	       init_function = (fun () -> write default) }
    in
    begin fun v -> add_anonymous_leaf (decl_obj v) end ,
    begin fun v -> add_anonymous_leaf (ldecl_obj v) end ,
    begin fun v -> add_anonymous_leaf (gdecl_obj v) end
  else write,write,write
  in
  let cread () = cast (read ()) in
  let cwrite v = write (uncast v) in
  let clwrite v = lwrite (uncast v) in
  let cgwrite v = gwrite (uncast v) in
  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
  write

type 'a write_function = 'a -> unit

let declare_int_option =
  declare_option
    (fun v -> IntValue v)
    (function IntValue v -> v | _ -> anomaly "async_option")
let declare_bool_option =
  declare_option
    (fun v -> BoolValue v)
    (function BoolValue v -> v | _ -> anomaly "async_option")
let declare_string_option =
  declare_option
    (fun v -> StringValue v)
    (function StringValue v -> v | _ -> anomaly "async_option")

(* 3- User accessible commands *)

(* Setting values of options *)

let set_option_value locality check_and_cast key v =
  let (name, depr, (_,read,write,lwrite,gwrite)) =
    try get_option key
    with Not_found -> error ("There is no option "^(nickname key)^".")
  in
  let write = match locality with
    | None -> write
    | Some true -> lwrite
    | Some false -> gwrite
  in
  write (check_and_cast v (read ()))

let bad_type_error () = error "Bad type of value for this option."

let check_int_value v = function
  | IntValue _ -> IntValue v
  | _ -> bad_type_error ()

let check_bool_value v = function
  | BoolValue _ -> BoolValue v
  | _ -> bad_type_error ()

let check_string_value v = function
  | StringValue _ -> StringValue v
  | _ -> bad_type_error ()

let check_unset_value v = function
  | BoolValue _ -> BoolValue false
  | IntValue _ -> IntValue None
  | _ -> bad_type_error ()

(* Nota: For compatibility reasons, some errors are treated as
   warning. This allows a script to refer to an option that doesn't
   exist anymore *)

let set_int_option_value_gen locality =
  set_option_value locality check_int_value
let set_bool_option_value_gen locality key v =
  try set_option_value locality check_bool_value key v
  with UserError (_,s) -> Flags.if_warn msg_warning s
let set_string_option_value_gen locality =
  set_option_value locality check_string_value
let unset_option_value_gen locality key =
  try set_option_value locality check_unset_value key ()
  with UserError (_,s) -> Flags.if_warn msg_warning s

let set_int_option_value = set_int_option_value_gen None
let set_bool_option_value = set_bool_option_value_gen None
let set_string_option_value = set_string_option_value_gen None

(* Printing options/tables *)

let msg_option_value (name,v) =
  match v with
    | BoolValue true  -> str "true"
    | BoolValue false -> str "false"
    | IntValue (Some n) -> int n
    | IntValue None   -> str "undefined"
    | StringValue s   -> str s
(*     | IdentValue r    -> pr_global_env Idset.empty r *)

let print_option_value key =
  let (name, depr, (_,read,_,_,_)) = get_option key in
  let s = read () in
  match s with
    | BoolValue b ->
	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++
	     fnl ())
    | _ ->
	msg (str ("Current value of "^name^" is ") ++
	     msg_option_value (name,s) ++ fnl ())


let get_tables () =
  let tables = !value_tab in
  let fold key (name, depr, (sync,read,_,_,_)) accu =
    let state = {
      opt_sync = sync;
      opt_name = name;
      opt_depr = depr;
      opt_value = read ();
    } in
    OptionMap.add key state accu
  in
  OptionMap.fold fold tables OptionMap.empty

let print_tables () =
  let print_option key name value depr =
    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
    if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
    else msg ++ fnl ()
  in
  msg
    (str "Synchronous options:" ++ fnl () ++
     OptionMap.fold
       (fun key (name, depr, (sync,read,_,_,_)) p ->
	  if sync then p ++ print_option key name (read ()) depr
	  else p)
       !value_tab (mt ()) ++
     str "Asynchronous options:" ++ fnl () ++
     OptionMap.fold
       (fun key (name, depr, (sync,read,_,_,_)) p ->
	  if sync then p
	  else p ++ print_option key name (read ()) depr)
       !value_tab (mt ()) ++
     str "Tables:" ++ fnl () ++
     List.fold_right
       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
       !string_table (mt ()) ++
     List.fold_right
       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
       !ref_table (mt ()) ++
     fnl ()
    )