From 59214186b817329342d9d72e23adf12f7a3b1348 Mon Sep 17 00:00:00 2001
From: stuebinm
Date: Sat, 29 Jun 2024 21:31:22 +0200
Subject: 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)
---
 compiler/ExtractBuiltin.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'compiler/ExtractBuiltin.ml')

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 37b676bb..f0460035 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -44,7 +44,7 @@ let split_on_separator (s : string) : string list =
 
 let flatten_name (name : string list) : string =
   match backend () with
-  | FStar | Coq | HOL4 -> String.concat "_" name
+  | FStar | Coq | HOL4 | IsabelleHOL -> String.concat "_" name
   | Lean -> String.concat "." name
 
 (** Utility for Lean-only definitions **)
@@ -61,7 +61,7 @@ let () =
     is F*, Coq or HOL4, and a different value if the target is Lean.
  *)
 let backend_choice (fstar_coq_hol4 : 'a) (lean : 'a) : 'a =
-  match backend () with Coq | FStar | HOL4 -> fstar_coq_hol4 | Lean -> lean
+  match backend () with Coq | FStar | HOL4 | IsabelleHOL -> fstar_coq_hol4 | Lean -> lean
 
 let builtin_globals : (string * string) list =
   [
@@ -135,10 +135,10 @@ type type_variant_kind =
 
 let mk_struct_constructor (type_name : string) : string =
   let prefix =
-    match backend () with FStar -> "Mk" | Coq | HOL4 -> "mk" | Lean -> ""
+    match backend () with FStar -> "Mk" | Coq | HOL4 | IsabelleHOL -> "mk" | Lean -> ""
   in
   let suffix =
-    match backend () with FStar | Coq | HOL4 -> "" | Lean -> ".mk"
+    match backend () with FStar | Coq | HOL4 | IsabelleHOL -> "" | Lean -> ".mk"
   in
   prefix ^ type_name ^ suffix
 
@@ -168,7 +168,7 @@ let builtin_types () : builtin_type_info list =
                 ( rname,
                   match backend () with
                   | FStar | Lean -> name
-                  | Coq | HOL4 -> extract_name ^ "_" ^ name ))
+                  | Coq | HOL4 | IsabelleHOL -> extract_name ^ "_" ^ name ))
               fields
           in
           let constructor = mk_struct_constructor extract_name in
@@ -201,7 +201,7 @@ let builtin_types () : builtin_type_info list =
       extract_name =
         (match backend () with
         | Lean -> "Option"
-        | Coq | FStar | HOL4 -> "option");
+        | Coq | FStar | HOL4 | IsabelleHOL -> "option");
       keep_params = None;
       body_info =
         Some
@@ -211,7 +211,7 @@ let builtin_types () : builtin_type_info list =
                  rust_variant_name = "None";
                  extract_variant_name =
                    (match backend () with
-                   | FStar | Coq -> "None"
+                   | FStar | Coq | IsabelleHOL -> "None"
                    | Lean -> "none"
                    | HOL4 -> "NONE");
                  fields = None;
@@ -220,7 +220,7 @@ let builtin_types () : builtin_type_info list =
                  rust_variant_name = "Some";
                  extract_variant_name =
                    (match backend () with
-                   | FStar | Coq -> "Some"
+                   | FStar | Coq | IsabelleHOL -> "Some"
                    | Lean -> "some"
                    | HOL4 -> "SOME");
                  fields = None;
@@ -574,7 +574,7 @@ let builtin_trait_decls_info () =
         in
         let type_name =
           match backend () with
-          | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter type_name
+          | FStar | Coq | HOL4 | IsabelleHOL -> StringUtils.lowercase_first_letter type_name
           | Lean -> type_name
         in
         let clauses = [] in
-- 
cgit v1.2.3