Source file `config.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of the why3find.                                    *)
(*                                                                        *)
(*  Copyright (C) 2022-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the enclosed LICENSE.md for details.                              *)
(*                                                                        *)
(**************************************************************************)

type config = {
  fast : float ;
  time : float ;
  depth : int ;
  packages : string list ;
  provers : string list ;
  tactics : string list ;
  drivers : string list ;
  warnoff : string list ;
  preprocess : string option ;
  profile : Json.t option ; (* We'll keep it like that for now *)
}

let conf_file = "why3find.json"

let load_raw_config p =
  let p = Filename.concat p conf_file in
  if Sys.file_exists p
  then Json.of_file p
  else `Null

let get ~of_json ~default name json =
  try of_json (Json.jfield_exn name json) with
  | Not_found -> default

let gets name ?(default=[]) json =
  get ~of_json:Json.jstringlist ~default name json

let config_of_json json =
  if gets "configs" json <> [] then
    Log.warning "Support for extra config files was removed in why3find 1.1.0.\
                 @ If you need this feature, please report this at %%PKG_ISSUES%%.";
  {
    fast = get "fast" ~of_json:Json.jfloat ~default:0.2 json;
    time = get "time" ~of_json:Json.jfloat ~default:1.0 json;
    depth = get "depth" ~of_json:Json.jint ~default:4 json;
    packages = gets "packages" json;
    provers = gets "provers" json;
    tactics = gets "tactics" ~default:["split_vc"] json;
    drivers = gets "drivers" json;
    warnoff = gets "warnoff" json;
    preprocess = Json.(joption jstring @@ jfield "preprocess" json);
    profile = get ~of_json:Option.some ~default:None "profile" json;
  }

let default = config_of_json `Null

let lists fd =
  `List (List.map (fun s -> `String s) fd)

let config_to_json config =
  let fields = [
    "fast", `Float config.fast ;
    "time", `Float config.time ;
    "depth", `Int config.depth ;
    "packages", lists config.packages ;
    "provers", lists config.provers ;
    "tactics", lists config.tactics ;
    "drivers", lists config.drivers ;
    "warnoff", lists config.warnoff ;
    "preprocess", Json.option_map Json.string config.preprocess ;
    "profile", Json.option_map Fun.id config.profile
  ] in
  Json.assoc ~keepnull:false fields

let load_config p =
  config_of_json @@ load_raw_config p

let save_config p config =
  let p = Filename.concat p conf_file in
  Json.to_file p @@ config_to_json config

type wenv = {
  config : Why3.Whyconf.config ;
  env : Why3.Env.env ;
}

module WenvWhtbl = Why3.Weakhtbl.Make (struct
    type t = wenv
    let tag w = Why3.Env.env_tag w.env
  end)

let create_wenv ?(loadpath=[]) config =
  let loadpath = loadpath @ Why3.Whyconf.(loadpath @@ get_main config) in
  let env = Why3.Env.create_env loadpath in
  { config ; env }

type env = {
  config : config ;
  wenv : wenv ;
  pkgs : Meta.pkg list ;
}

let create_env ?(root=".") ~config () =
  let pkgs = Meta.find_all config.packages in
  let pkg_path = List.map (fun m -> m.Meta.path) pkgs in
  let wconfig = Why3.Whyconf.init_config ~extra_config:[] None in
  let wenv = create_wenv ~loadpath:(root :: pkg_path) wconfig in
  { config ; wenv ; pkgs }