compiler: introduce Lean-only translations

On the long run, all backends will not have equivalent or equal support
for extraction.

This introduces a function to filter out some Lean-only definitions in
our various arrays of core functions.

Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>

1 files changed, 25 insertions, 10 deletions

diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index c59825d1..c6827bbe 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -47,6 +47,10 @@ let flatten_name (name : string list) : string =
   | FStar | Coq | HOL4 -> String.concat "_" name
   | Lean -> String.concat "." name
 
+(** Utility for Lean-only definitions **)
+let mk_lean_only (funs : 'a list) : 'a list =
+  match !backend with Lean -> funs | _ -> []
+
 let () =
   assert (split_on_separator "x::y::z" = [ "x"; "y"; "z" ]);
   assert (split_on_separator "x.y.z" = [ "x"; "y"; "z" ])
@@ -287,16 +291,9 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
   in
   [
     mk_fun "core::mem::replace" None None;
-    mk_fun "core::mem::swap" None None;
     mk_fun "core::slice::{[@T]}::len"
       (Some (backend_choice "slice::len" "Slice::len"))
       None;
-    mk_fun "core::option::{core::option::Option<@T>}::take"
-      (Some (backend_choice "option::take" "Option::take"))
-      None;
-    mk_fun "core::option::{core::option::Option<@T>}::is_none"
-      (Some (backend_choice "option::is_none" "Option::isNone"))
-      (Some [ false ]);
     mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"
       (Some "alloc::vec::Vec::new") None;
     mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None
@@ -445,6 +442,21 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
       (fun ty ->
         "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone")
+  (* Lean-only definitions *)
+  @ mk_lean_only
+      [
+        (* `backend_choice` first parameter is for non-Lean backends
+            By construction, we cannot write down that parameter in the output
+            in this list
+        *)
+        mk_fun "core::mem::swap" None None;
+        mk_fun "core::option::{core::option::Option<@T>}::take"
+          (Some (backend_choice "" "Option::take"))
+          None;
+        mk_fun "core::option::{core::option::Option<@T>}::is_none"
+          (Some (backend_choice "" "Option::isNone"))
+          (Some [ false ]);
+      ]
 
 let mk_builtin_funs_map () =
   let m =
@@ -521,16 +533,19 @@ let builtin_fun_effects =
       "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new";
       "alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
       "core::mem::replace";
-      "core::mem::swap";
       "core::mem::take";
-      "core::option::{core::option::Option<@T>}::take";
-      "core::option::{core::option::Option<@T>}::is_none";
       "core::clone::impls::{core::clone::Clone<bool>}::clone";
       "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity";
       "core::slice::{[@T]}::reverse";
       "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref";
     ]
     @ int_funs
+    @ mk_lean_only
+        [
+          "core::mem::swap";
+          "core::option::{core::option::Option<@T>}::take";
+          "core::option::{core::option::Option<@T>}::is_none";
+        ]
   in
   let no_fail_no_state_funs =
     List.map