1 files changed, 47 insertions, 0 deletions
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml
new file mode 100644
index 00000000..d21a46fc
--- /dev/null
+++ b/tests/test_runner/Backend.ml
@@ -0,0 +1,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