blob: 819081a2c719989eb17fbe5e3cdf16d7285252db (
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
|
(*** Define the backends we support as an enum *)
type t =
| Coq
| Lean
| FStar
| HOL4
| BorrowCheck
(** Borrow check: no backend.
We use this when we only want to borrow-check the program *)
[@@deriving ord, sexp]
(* TODO: reactivate HOL4 once traits are parameterized by their associated types *)
let all = [ Coq; Lean; FStar; BorrowCheck ]
let of_string = function
| "coq" -> Coq
| "lean" -> Lean
| "fstar" -> FStar
| "hol4" -> HOL4
| "borrow-check" -> BorrowCheck
| backend -> failwith ("Unknown backend: `" ^ backend ^ "`")
let to_string = function
| Coq -> "coq"
| Lean -> "lean"
| FStar -> "fstar"
| HOL4 -> "hol4"
| BorrowCheck -> "borrow-check"
let to_command = function
| BorrowCheck -> [ "-borrow-check" ]
| x -> [ "-backend"; to_string x ]
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
|
