whyconf.ml 24 KB
Newer Older
1
2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4
5
6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8
9
10
11
12
13
14
15
16
17
18
19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
20
21

open Format
22
open Util
23
open Rc
24
open Stdlib
25

26
27
(* magicnumber for the configuration :
  - 0 before the magic number
28
  - 1 when no loadpath meant default loadpath
29
30
  - 2
  - 5 cvc3 native
Andrei Paskevich's avatar
Andrei Paskevich committed
31
  - 6 driver renaming
32
  - 7 yices native (used for release 0.70)
33
  - 8 for release 0.71
34
  - 9 coq realizations
35
  - 10 require %f in editor lines
36
  - 11 change prover identifiers in provers-detection-data.conf
37
  - 12 split editors out of provers
38
  - 13 add shortcuts
39
  - 14 use simple_family for prover and shortcut section
40

41
If a configuration doesn't contain the actual magic number we don't use it.*)
42

43
let magicnumber = 14
44

45
46
exception WrongMagicNumber

47
48
49
let why3_regexp_of_string s = (** define a regexp in why3 *)
  if s.[0] = '^' then Str.regexp s else Str.regexp ("^"^Str.quote s^"$")

50
51
(* lib and shared dirs *)

52
53
54
let default_loadpath =
  [ Filename.concat Config.datadir "theories";
    Filename.concat Config.datadir "modules"; ]
MARCHE Claude's avatar
MARCHE Claude committed
55

56
let default_conf_file =
57
  match Config.localdir with
58
59
    | None -> Filename.concat (Rc.get_home_dir ()) ".why3.conf"
    | Some d -> Filename.concat d "why3.conf"
60

61
62
63
(* Prover *)

type prover =
64
    { prover_name : string;
65
      prover_version : string;
66
      prover_altern : string;
67
68
69
    }

let print_prover fmt p =
70
71
72
  Format.fprintf fmt "%s (%s%s%s)"
    p.prover_name p.prover_version
    (if p.prover_altern = "" then "" else " ") p.prover_altern
73

74
75
76
77
78
let print_prover_parsable_format fmt p =
  Format.fprintf fmt "%s,%s,%s"
    p.prover_name p.prover_version p.prover_altern


79
80
81
82
83
84
85
module Prover = struct
  type t = prover
  let compare s1 s2 =
    if s1 == s2 then 0 else
    let c = String.compare s1.prover_name s2.prover_name in
    if c <> 0 then c else
    let c = String.compare s1.prover_version s2.prover_version in
86
87
    if c <> 0 then c else
    let c = String.compare s1.prover_altern s2.prover_altern in
88
89
90
    c

  let equal s1 s2 =
91
92
    s1 == s2 ||
      (s1.prover_name = s2.prover_name &&
93
94
       s1.prover_version = s2.prover_version &&
       s1.prover_altern = s2.prover_altern )
95
96

  let hash s1 =
97
      2 * Hashtbl.hash s1.prover_name +
98
99
      3 * Hashtbl.hash s1.prover_version +
      5 * Hashtbl.hash s1.prover_altern
100
101
102
103
104
105
end

module Mprover = Map.Make(Prover)
module Sprover = Mprover.Set
module Hprover = Hashtbl.Make(Prover)

106
107
108
109
110
111
112
module Editor = struct
  type t = string
  let compare = Pervasives.compare
end

module Meditor = Map.Make(Editor)

113
114
(* Configuration file *)

115
116
117
118
119
type prover_upgrade_policy =
  | CPU_keep
  | CPU_upgrade of prover
  | CPU_duplicate of prover

120
type config_prover = {
121
122
123
  prover  : prover;
  command : string;
  driver  : string;
124
  in_place: bool;
125
  editor  : string;
126
  interactive : bool;
127
128
  extra_options : string list;
  extra_drivers : string list;
129
130
}

131
type config_editor = {
MARCHE Claude's avatar
MARCHE Claude committed
132
  editor_name : string;
133
134
135
136
  editor_command : string;
  editor_options : string list;
}

137

138
type main = {
139
140
  libdir   : string;      (* "/usr/local/lib/why/" *)
  datadir  : string;      (* "/usr/local/share/why/" *)
141
  loadpath  : string list;  (* "/usr/local/lib/why/theories" *)
142
143
  timelimit : int;
  (* default prover time limit in seconds (0 unlimited) *)
144
  memlimit  : int;
145
  (* default prover memory limit in megabytes (0 unlimited)*)
146
  running_provers_max : int;
147
  (* max number of running prover processes *)
François Bobot's avatar
François Bobot committed
148
  plugins : string list;
149
  (* plugins to load, without extension, relative to [libdir]/plugins *)
150
151
}

MARCHE Claude's avatar
MARCHE Claude committed
152
153
154
let libdir m =
  try
    Sys.getenv "WHY3LIB"
155
  with Not_found -> m.libdir
MARCHE Claude's avatar
MARCHE Claude committed
156
157
158

let datadir m =
  try
159
160
161
162
163
    let d = Sys.getenv "WHY3DATA" in
(*
    eprintf "[Info] datadir set using WHY3DATA='%s'@." d;
*)
    d
164
  with Not_found -> m.datadir
MARCHE Claude's avatar
MARCHE Claude committed
165

166
let loadpath m =
167
168
169
170
171
  try
    let d = Sys.getenv "WHY3LOADPATH" in
(*
    eprintf "[Info] loadpath set using WHY3LOADPATH='%s'@." d;
*)
172
    Str.split (Str.regexp ":") d
173
174
175
176
177
178
179
180
181
  with Not_found -> m.loadpath

let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max

let set_limits m time mem running =
  { m with timelimit = time; memlimit = mem; running_provers_max = running }

François Bobot's avatar
François Bobot committed
182
183
184
185
let plugins m = m.plugins
let set_plugins m pl =
  (* TODO : sanitize? *)
  { m with plugins = pl}
186

François Bobot's avatar
François Bobot committed
187
188
189
190
191
let add_plugin m p =
  if List.mem p m.plugins
  then m
  else { m with plugins = List.rev (p::(List.rev m.plugins))}

Andrei Paskevich's avatar
Andrei Paskevich committed
192
let pluginsdir m = Filename.concat m.libdir "plugins"
François Bobot's avatar
François Bobot committed
193
194
let load_plugins m =
  let load x =
195
    try Plugin.load x
196
197
198
    with exn ->
      Format.eprintf "%s can't be loaded : %a@." x
        Exn_printer.exn_printer exn in
François Bobot's avatar
François Bobot committed
199
200
  List.iter load m.plugins

201
type config = {
202
  conf_file : string;       (* "/home/innocent_user/.why3.conf" *)
203
  config    : Rc.t;
204
  main      : main;
205
  provers   : config_prover Mprover.t;
206
  prover_shortcuts : prover Mstr.t;
207
  editors   : config_editor Meditor.t;
208
  provers_upgrade_policy : prover_upgrade_policy Mprover.t;
209
210
}

211
212
let default_main =
  {
213
214
215
    libdir = Config.libdir;
    datadir = Config.datadir;
    loadpath = default_loadpath;
216
217
218
    timelimit = 5;   (* 5 seconds *)
    memlimit = 1000; (* 1 Mb *)
    running_provers_max = 2; (* two provers run in parallel *)
François Bobot's avatar
François Bobot committed
219
    plugins = [];
220
  }
221

222
let set_main rc main =
223
  let section = empty_section in
224
  let section = set_int section "magic" magicnumber in
225
226
227
228
229
  let section = set_string ~default:default_main.libdir
    section "libdir" main.libdir in
  let section = set_string ~default:default_main.datadir
    section "datadir" main.datadir in
  let section = set_stringl section "loadpath" main.loadpath in
230
231
232
233
  let section = set_int section "timelimit" main.timelimit in
  let section = set_int section "memlimit" main.memlimit in
  let section =
    set_int section "running_provers_max" main.running_provers_max in
François Bobot's avatar
François Bobot committed
234
  let section = set_stringl section "plugin" main.plugins in
235
  set_section rc "main" section
236

237
238
exception NonUniqueId

239
let set_prover _ (prover,shortcuts) family =
240
  let section = empty_section in
241
  let section = set_string section "name" prover.prover.prover_name in
242
243
  let section = set_string section "command" prover.command in
  let section = set_string section "driver" prover.driver in
244
  let section = set_string section "version" prover.prover.prover_version in
245
246
  let section =
    set_string ~default:"" section "alternative"prover.prover.prover_altern in
247
  let section = set_string section "editor" prover.editor in
248
  let section = set_bool section "interactive" prover.interactive in
249
  let section = set_bool section "in_place" prover.in_place in
250
  let section = set_stringl section "shortcut" shortcuts in
251
  section::family
252

253
let set_provers rc provers =
254
  let family = Mprover.fold set_prover provers [] in
255
  set_simple_family rc "prover" family
256

257
let set_prover_shortcut prover shortcuts family =
258
259
260
261
262
  let section = empty_section in
  let section = set_string section "name" prover.prover_name in
  let section = set_string section "version" prover.prover_version in
  let section =
    set_string ~default:"" section "alternative" prover.prover_altern in
263
  let section = set_stringl section "shortcut" shortcuts in
264
  section::family
265
266

let set_prover_shortcuts rc shortcuts =
267
  let family = Mprover.fold set_prover_shortcut shortcuts [] in
268
  set_simple_family rc "shortcut" family
269

270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
let set_provers_shortcuts rc shortcuts provers =
  (** inverse the shortcut map *)
  let shortcuts = Mstr.fold (fun shortcut prover acc ->
    Mprover.change (function
    | None -> Some [shortcut]
    | Some l -> Some (shortcut::l)) prover acc) shortcuts Mprover.empty in
  (** the shortcut to unknown prover *)
  let shortcuts_prover_unknown = Mprover.set_diff shortcuts provers in
  let rc = set_prover_shortcuts rc shortcuts_prover_unknown in
  (** merge the known *)
  let _,shortcuts_provers_known =
    Mprover.mapi_fold (fun k v acc ->
      let acc = Mprover.next_ge_enum k acc in
      match Mprover.val_enum acc with
      | None -> acc,(v,[])
      | Some (ks,vs) ->
        let c = Prover.compare k ks in
        if c = 0 then acc,(v,vs)
        else (* c < 0 *) acc,(v,[])
    ) provers (Mprover.start_enum shortcuts) in
  let rc = set_provers rc shortcuts_provers_known in
  rc

293
294
295
let set_editor id editor (ids, family) =
  if Sstr.mem id ids then raise NonUniqueId;
  let section = empty_section in
MARCHE Claude's avatar
MARCHE Claude committed
296
  let section = set_string section "name" editor.editor_name in
297
298
299
300
301
302
303
  let section = set_string section "command" editor.editor_command in
  (Sstr.add id ids, (id, section)::family)

let set_editors rc editors =
  let _,family = Meditor.fold set_editor editors (Sstr.empty,[]) in
  set_family rc "editor" family

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
let set_prover_upgrade_policy prover policy (i, family) =
  let section = empty_section in
  let section = set_string section "name" prover.prover_name in
  let section = set_string section "version" prover.prover_version in
  let section = set_string section "alternative" prover.prover_altern in
  let section =
    match policy with
      | CPU_keep -> 
        set_string section "policy" "keep"
      | CPU_upgrade p ->
        let section = set_string section "target_name" p.prover_name in
        let section = set_string section "target_version" p.prover_version in
        let section = set_string section "target_alternative" p.prover_altern in
        set_string section "policy" "upgrade"
      | CPU_duplicate p ->
        let section = set_string section "target_name" p.prover_name in
        let section = set_string section "target_version" p.prover_version in
        let section = set_string section "target_alternative" p.prover_altern in
        set_string section "policy" "duplicate"
  in
  (i+1,("policy" ^ string_of_int i, section)::family)

let set_policies rc policy =
  let _,family =
    Mprover.fold set_prover_upgrade_policy policy (0,[])
  in
  set_family rc "uninstalled_prover" family

332
let absolute_filename = Sysutil.absolutize_filename
333

334
335
336
337
338
339
340
341
342
343
exception DuplicateShortcut of string

let add_prover_shortcuts acc prover shortcuts =
  List.fold_left (fun acc shortcut ->
    if shortcut.[0] = '^' then
      invalid_arg "prover shortcut can't start with a ^";
    Mstr.add_new (DuplicateShortcut shortcut) shortcut prover acc
  ) acc shortcuts


344
let load_prover dirname (provers,shortcuts) section =
345
  let name = get_string section "name" in
346
  let version = get_string ~default:"" section "version" in
347
  let altern = get_string ~default:"" section "alternative" in
348
  let prover =
349
350
    { prover_name = name;
      prover_version = version;
351
352
      prover_altern = altern;
    }
353
  in
354
  let provers = Mprover.add prover
355
    { prover  = prover;
356
357
      command = get_string section "command";
      driver  = absolute_filename dirname (get_string section "driver");
358
      in_place = get_bool ~default:false section "in_place";
359
      editor  = get_string ~default:"" section "editor";
360
      interactive = get_bool ~default:false section "interactive";
361
362
      extra_options = [];
      extra_drivers = [];
363
364
365
366
    } provers in
  let lshort = get_stringl section ~default:[] "shortcut" in
  let shortcuts = add_prover_shortcuts shortcuts prover lshort in
  provers,shortcuts
367

368
let load_shortcut acc section =
369
370
371
372
373
374
375
  let name = get_string section "name" in
  let version = get_string section "version" in
  let altern = get_string ~default:"" section "alternative" in
  let shortcuts = get_stringl section "shortcut" in
  let prover = { prover_name = name;
                 prover_version = version;
                 prover_altern= altern} in
376
  add_prover_shortcuts acc prover shortcuts
377

378
379
let load_editor editors (id, section) =
  Meditor.add id
MARCHE Claude's avatar
MARCHE Claude committed
380
381
    { editor_name = get_string ~default:id section "name";
      editor_command = get_string section "command";
382
383
384
      editor_options = [];
    } editors

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
let load_policy provers acc (_,section) =
  let source =
    {prover_name = get_string section "name";
     prover_version = get_string section "version";
     prover_altern = get_string ~default:"" section "alternative"
    } in
  try
    match get_string section "policy" with
      | "keep" -> Mprover.add source CPU_keep acc
      | "upgrade" ->
        let target =
          { prover_name = get_string section "target_name";
            prover_version = get_string section "target_version";
            prover_altern = get_string ~default:"" section "target_alternative";
          }
        in
        let _target = Mprover.find target provers in
        Mprover.add source (CPU_upgrade target) acc
      | "duplicate" -> 
        let target =
          { prover_name = get_string section "target_name";
            prover_version = get_string section "target_version";
            prover_altern = get_string ~default:"" section "target_alternative";
          }
        in
        let _target = Mprover.find target provers in
        Mprover.add source (CPU_duplicate target) acc
      | _ -> raise Not_found
  with Not_found -> acc

415
let load_main dirname section =
416
417
  if get_int ~default:0 section "magic" <> magicnumber then
    raise WrongMagicNumber;
418
419
  { libdir    = get_string ~default:default_main.libdir section "libdir";
    datadir   = get_string ~default:default_main.datadir section "datadir";
420
    loadpath  = List.map (absolute_filename dirname)
421
      (get_stringl ~default:[] section "loadpath");
422
423
    timelimit = get_int ~default:default_main.timelimit section "timelimit";
    memlimit  = get_int ~default:default_main.memlimit section "memlimit";
424
425
    running_provers_max = get_int ~default:default_main.running_provers_max
      section "running_provers_max";
François Bobot's avatar
François Bobot committed
426
    plugins = get_stringl ~default:[] section "plugin";
427
428
  }

429
let read_config_rc conf_file =
430
431
  let filename = match conf_file with
    | Some filename -> filename
432
    | None -> begin try Sys.getenv "WHY3CONFIG" with Not_found ->
433
434
          if Sys.file_exists default_conf_file then default_conf_file
          else raise Exit
435
436
        end
  in
437
438
439
440
  filename, Rc.from_file filename

exception ConfigFailure of string (* filename *) * string

441
442
443
444
let get_config (filename,rc) =
  let dirname = Filename.dirname filename in
  let rc, main =
    match get_section rc "main" with
445
      | None      -> raise (ConfigFailure (filename, "no main section"))
446
      | Some main -> rc, load_main dirname main
447
  in
448
  let provers = get_simple_family rc "prover" in
449
450
  let provers,shortcuts = List.fold_left (load_prover dirname)
    (Mprover.empty,Mstr.empty) provers in
451
  let fam_shortcuts = get_simple_family rc "shortcut" in
452
  let shortcuts = List.fold_left load_shortcut shortcuts fam_shortcuts in
453
454
  let editors = get_family rc "editor" in
  let editors = List.fold_left load_editor Meditor.empty editors in
455
456
  let policy = get_family rc "uninstalled_prover" in
  let policy = List.fold_left (load_policy provers) Mprover.empty policy in
457
  { conf_file = filename;
458
459
460
    config    = rc;
    main      = main;
    provers   = provers;
461
    prover_shortcuts = shortcuts;
462
    editors   = editors;
463
    provers_upgrade_policy = policy;
464
  }
465

466
let default_config conf_file =
467
  get_config (conf_file, set_main Rc.empty default_main)
468

469
let read_config conf_file =
470
471
  let filenamerc =
    try
472
      read_config_rc conf_file
473
    with Exit ->
474
475
      default_conf_file, set_main Rc.empty default_main
  in
476
  try
477
    get_config filenamerc
478
479
480
481
  with e when not (Debug.test_flag Debug.stack_trace) ->
    let b = Buffer.create 40 in
    Format.bprintf b "%a" Exn_printer.exn_printer e;
    raise (ConfigFailure (fst filenamerc, Buffer.contents b))
482

483
(** filter prover *)
484
485
486
487
type regexp_desc = { reg : Str.regexp; desc : string}

let mk_regexp s = { reg = why3_regexp_of_string s; desc = s}

488
type filter_prover =
489
490
491
  { filter_name    : regexp_desc;
    filter_version : regexp_desc option;
    filter_altern  : regexp_desc option;
492
493
  }

494
495
496
497
498
499
500
501
let mk_filter_prover ?version ?altern name =
  begin match version with
  | Some "" -> invalid_arg "mk_filter_prover: version can't be an empty string"
  | _ -> () end;
  { filter_name    = mk_regexp name;
    filter_version = option_map mk_regexp version;
    filter_altern  = option_map mk_regexp altern;
  }
502
503

let print_filter_prover fmt fp =
504
505
506
507
508
  match fp.filter_version, fp.filter_altern with
  | None  , None -> fprintf fmt "%s" fp.filter_name.desc
  | Some v, None -> fprintf fmt "%s,%s" fp.filter_name.desc v.desc
  | None  , Some a -> fprintf fmt "%s,,%s" fp.filter_name.desc a.desc
  | Some v, Some a -> fprintf fmt "%s,%s,%s" fp.filter_name.desc v.desc a.desc
509
510
511
512
513
514
515
516
517

exception ProverNotFound  of config * filter_prover
exception ProverAmbiguity of config * filter_prover * config_prover  Mprover.t
exception ParseFilterProver of string

let parse_filter_prover s =
  let sl = Util.split_string_rev s ',' in
  (* reverse order *)
  match sl with
518
519
520
521
  | [name] -> mk_filter_prover name
  | [version;name] -> mk_filter_prover ~version name
  | [altern;"";name] -> mk_filter_prover ~altern name
  | [altern;version;name] -> mk_filter_prover ~version ~altern name
522
523
524
  | _ -> raise (ParseFilterProver s)

let filter_prover fp p =
525
526
527
528
  let check s schema = Str.string_match schema.reg s 0 in
  check p.prover_name fp.filter_name
  && option_apply true (check p.prover_version) fp.filter_version
  && option_apply true (check p.prover_altern) fp.filter_altern
529
530

let filter_provers whyconf fp =
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
  try
    if fp.filter_version = None && fp.filter_altern = None then
      let prover = (Mstr.find fp.filter_name.desc whyconf.prover_shortcuts) in
      try
        let prover_config = Mprover.find prover whyconf.provers in
        Mprover.singleton prover prover_config
      with Not_found ->
        (** shortcut send to nothing *)
        Mprover.empty
    else raise Not_found
  with Not_found ->
    Mprover.filter (fun p _ -> filter_prover fp p) whyconf.provers

let filter_one_prover whyconf fp =
  let provers = filter_provers whyconf fp in
546
547
548
  if Mprover.is_num_elt 1 provers then
    snd (Mprover.choose provers)
  else if Mprover.is_empty provers then
549
    raise $ ProverNotFound (whyconf,fp)
550
  else
551
    raise $ ProverAmbiguity (whyconf,fp,provers)
552
553
554

(** merge config *)

555
556
557
let merge_config config filename =
  let dirname = Filename.dirname filename in
  let rc = Rc.from_file filename in
558
  (** modify main *)
559
560
561
562
563
  let main = match get_section rc "main" with
    | None -> config.main
    | Some rc ->
      let loadpath = (List.map (absolute_filename dirname)
        (get_stringl ~default:[] rc "loadpath")) @ config.main.loadpath in
564
565
      let plugins =
        (get_stringl ~default:[] rc "plugin") @ config.main.plugins in
566
      { config.main with loadpath = loadpath; plugins = plugins } in
567
568
569
  (** modify provers *)
  let create_filter_prover section =
    let name = get_string section "name" in
570
571
572
    let version = get_stringo section "version" in
    let altern = get_stringo section "alternative" in
    mk_filter_prover ?version ?altern name in
573
  let prover_modifiers = get_simple_family rc "prover_modifiers" in
574
  let prover_modifiers =
575
    List.map (fun sec -> create_filter_prover sec, sec) prover_modifiers in
576
  (** add provers *)
577
  let provers = List.fold_left
578
579
580
581
582
583
584
585
586
587
588
589
    (fun provers (fp, section) ->
      Mprover.mapi (fun p c  ->
        if not (filter_prover fp p) then c
        else
          let opt = get_stringl ~default:[] section "option" in
          let drv = List.map (absolute_filename dirname)
            (get_stringl ~default:[] section "driver") in
          { c with
            extra_options = opt @ c.extra_options;
            extra_drivers = drv @ c.extra_drivers })
        provers
    ) config.provers prover_modifiers in
590
591
  let provers,shortcuts =
    List.fold_left (load_prover dirname)
592
      (provers,config.prover_shortcuts) (get_simple_family rc "prover") in
593
594
  (** modify editors *)
  let editor_modifiers = get_family rc "editor_modifiers" in
595
596
  let editors = List.fold_left
    (fun editors (id, section) ->
597
598
599
600
601
602
603
604
      Meditor.change (function
      | None -> None
      | Some c ->
        let opt = get_stringl ~default:[] section "option" in
        Some { c with editor_options = opt @ c.editor_options }) id  editors
    ) config.editors editor_modifiers in
  (** add editors *)
  let editors = List.fold_left load_editor editors (get_family rc "editor") in
605
606
  { config with main = main; provers = provers;
    prover_shortcuts = shortcuts; editors = editors }
607

608
let save_config config =
609
  let filename = config.conf_file in
610
  Sysutil.backup_file filename;
611
  to_file filename config.config
612

613
614
let get_main config = config.main
let get_provers config = config.provers
615
let get_prover_shortcuts config = config.prover_shortcuts
616
617
618
let get_policies config = config.provers_upgrade_policy
let get_prover_upgrade_policy config p =
  Mprover.find p config.provers_upgrade_policy
619

620
621
622
623
let set_main config main =
  {config with
    config = set_main config.config main;
    main = main;
624
625
  }

626
627
let set_provers config ?shortcuts provers =
  let shortcuts = def_option config.prover_shortcuts shortcuts in
628
  {config with
629
    config = set_provers_shortcuts config.config shortcuts provers;
630
    provers = provers;
631
    prover_shortcuts = shortcuts;
632
  }
633

634
635
let set_prover_shortcuts config shortcuts =
  {config with
636
    config = set_provers_shortcuts config.config shortcuts config.provers;
637
638
639
    prover_shortcuts = shortcuts;
  }

640
641
642
643
644
645
let set_editors config editors =
  { config with
    config = set_editors config.config editors;
    editors = editors;
  }

646
647
648
649
650
651
652
653
654
655
656
657
658
659
let set_prover_upgrade_policy config prover target =
  let m = Mprover.add prover target config.provers_upgrade_policy in
  {config with
    config = set_policies config.config m;
    provers_upgrade_policy = m;
  }

let set_policies config policies = 
  { config with
    config = set_policies config.config policies;
    provers_upgrade_policy = policies }



660
661
(*******)

662
let set_conf_file config conf_file = {config with conf_file = conf_file}
663
let get_conf_file config           =  config.conf_file
664

665
666
667
668
669
(*******)

let is_prover_known whyconf prover =
  Mprover.mem prover (get_provers whyconf)

670
671
let get_editors c = c.editors

672
673
let editor_by_id whyconf id =
  Meditor.find id whyconf.editors
674
675
676

(******)

677
678
let get_section config name = assert (name <> "main");
  get_section config.config name
679

680
681
let get_family config name = assert (name <> "prover");
  get_family config.config name
682
683


684
685
let set_section config name section = assert (name <> "main");
  {config with config = set_section config.config name section}
686

687
688
let set_family config name section = assert (name <> "prover");
  {config with config = set_family config.config name section}
689

690
691
692
693
694
695
696
697
698

let () = Exn_printer.register (fun fmt e -> match e with
  | ConfigFailure (f, s) ->
      Format.fprintf fmt "error in config file %s: %s" f s
  | WrongMagicNumber ->
      Format.fprintf fmt "outdated config file; rerun why3config"
  | NonUniqueId ->
    Format.fprintf fmt "InternalError : two provers share the same id"
  | ProverNotFound (config,fp) ->
699
    fprintf fmt "No prover in %s corresponds to \"%a\"@."
700
701
      (get_conf_file config) print_filter_prover fp
  | ProverAmbiguity (config,fp,provers ) ->
702
    fprintf fmt "More than one prover@ in %s@ correspond@ to \"%a\":@ %a@."
703
704
705
706
707
708
709
      (get_conf_file config) print_filter_prover fp
      (Pp.print_iter2 Mprover.iter Pp.space Pp.nothing print_prover Pp.nothing)
      provers
  | ParseFilterProver s ->
    fprintf fmt
      "Syntax error prover identification '%s' : \
       name[,version[,alternative]|,,alternative]" s
710
711
712
  | DuplicateShortcut s ->
    fprintf fmt
      "Shortcut %s appears two times in the configuration file" s
713
  | _ -> raise e)