diff options
| author | stuebinm | 2024-06-29 21:31:22 +0200 |
|---|---|---|
| committer | stuebinm | 2024-06-29 22:11:04 +0200 |
| commit | 59214186b817329342d9d72e23adf12f7a3b1348 (patch) | |
| tree | 8292abe4ca52e9742f6a4ff9d102565a6362e665 /compiler/Config.ml | |
| parent | 5590dc87a5426cbcb32a2387701d179e107a9792 (diff) | |
had some fun writing an IsabelleHOL backend
(do not actually use this, most things are broken, and the primitives
lib barely exists and is simply incorrect. But it is enough to create
syntax-correct Isabelle code for relatively simply rust code, as long
as it does not contain any uses of traits)
Diffstat (limited to '')
| -rw-r--r-- | compiler/Config.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml index 98a5eea1..0abe94a9 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -3,9 +3,9 @@ (** {1 Backend choice} *) (** The choice of backend *) -type backend = FStar | Coq | Lean | HOL4 +type backend = FStar | Coq | Lean | HOL4 | IsabelleHOL -let backend_names = [ "fstar"; "coq"; "lean"; "hol4" ] +let backend_names = [ "fstar"; "coq"; "lean"; "hol4"; "IsabelleHOL"] (** Utility to compute the backend from an input parameter *) let backend_of_string (b : string) : backend option = @@ -14,6 +14,7 @@ let backend_of_string (b : string) : backend option = | "coq" -> Some Coq | "lean" -> Some Lean | "hol4" -> Some HOL4 + | "IsabelleHOL" -> Some IsabelleHOL | _ -> None let opt_backend : backend option ref = ref None @@ -374,7 +375,7 @@ let variant_concatenate_type_name = ref true let use_tuple_structs = ref true let backend_has_tuple_projectors backend = - match backend with Lean -> true | Coq | FStar | HOL4 -> false + match backend with Lean -> true | Coq | FStar | HOL4 | IsabelleHOL -> false (** Toggle the use of tuple projectors *) let use_tuple_projectors = ref false |