blob: d21a46fcbe699a9f6e48220a6e47a7e10454c5cb (
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
|
(*** Define the backends we support as an enum *)
type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp]
(* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
let all = [ Coq; Lean; FStar ]
let of_string = function
| "coq" -> Coq
| "lean" -> Lean
| "fstar" -> FStar
| "hol4" -> HOL4
| backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
let to_string = function
| Coq -> "coq"
| Lean -> "lean"
| FStar -> "fstar"
| HOL4 -> "hol4"
module Map = struct
(* Hack to be able to include things from the parent module with the same names *)
type backend_t = t
let backend_compare = compare
include Map.Make (struct
type t = backend_t
let compare = backend_compare
end)
(* Make a new map with one entry per backend, given by `f` *)
let make (f : backend_t -> 'a) : 'a t =
List.fold_left (fun map backend -> add backend (f backend) map) empty all
(* Set this value for all the backends in `backends` *)
let add_each (backends : backend_t list) (v : 'a) (map : 'a t) : 'a t =
List.fold_left (fun map backend -> add backend v map) map backends
(* Updates all the backends in `backends` with `f` *)
let update_each (backends : backend_t list) (f : 'a -> 'a) (map : 'a t) : 'a t
=
List.fold_left
(fun map backend -> update backend (Option.map f) map)
map backends
end
|
