diff options
Diffstat (limited to 'tests/test_runner/Backend.ml')
| -rw-r--r-- | tests/test_runner/Backend.ml | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/tests/test_runner/Backend.ml b/tests/test_runner/Backend.ml index d21a46fc..819081a2 100644 --- a/tests/test_runner/Backend.ml +++ b/tests/test_runner/Backend.ml @@ -1,15 +1,24 @@ (*** Define the backends we support as an enum *) -type t = Coq | Lean | FStar | HOL4 [@@deriving ord, sexp] +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 ] +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 @@ -17,6 +26,11 @@ let to_string = function | 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 *) |