From 5ca36bfc50083a01af2b7ae5f75993a520757ef5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:17:58 +0200
Subject: Simplify the names used in Primitives.lean

---
 compiler/Extract.ml | 49 +++++++++++++++++++++++++++++++++----------------
 1 file changed, 33 insertions(+), 16 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 821bf4f7..180ca7ca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -300,23 +300,40 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
         (Option, option_none_id, "NONE");
       ]
 
-let assumed_llbc_functions :
+let assumed_llbc_functions () :
     (A.assumed_fun_id * T.RegionGroupId.id option * string) list =
   let rg0 = Some T.RegionGroupId.zero in
-  [
-    (Replace, None, "mem_replace_fwd");
-    (Replace, rg0, "mem_replace_back");
-    (VecNew, None, "vec_new");
-    (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
-    (VecPush, rg0, "vec_push_back");
-    (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
-    (VecInsert, rg0, "vec_insert_back");
-    (VecLen, None, "vec_len");
-    (VecIndex, None, "vec_index_fwd");
-    (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
-    (VecIndexMut, None, "vec_index_mut_fwd");
-    (VecIndexMut, rg0, "vec_index_mut_back");
-  ]
+  match !backend with
+  | FStar | Coq | HOL4 ->
+      [
+        (Replace, None, "mem_replace_fwd");
+        (Replace, rg0, "mem_replace_back");
+        (VecNew, None, "vec_new");
+        (VecPush, None, "vec_push_fwd") (* Shouldn't be used *);
+        (VecPush, rg0, "vec_push_back");
+        (VecInsert, None, "vec_insert_fwd") (* Shouldn't be used *);
+        (VecInsert, rg0, "vec_insert_back");
+        (VecLen, None, "vec_len");
+        (VecIndex, None, "vec_index_fwd");
+        (VecIndex, rg0, "vec_index_back") (* shouldn't be used *);
+        (VecIndexMut, None, "vec_index_mut_fwd");
+        (VecIndexMut, rg0, "vec_index_mut_back");
+      ]
+  | Lean ->
+      [
+        (Replace, None, "mem.replace_fwd");
+        (Replace, rg0, "mem.replace_back");
+        (VecNew, None, "Vec.new");
+        (VecPush, None, "Vec.push_fwd") (* Shouldn't be used *);
+        (VecPush, rg0, "Vec.push");
+        (VecInsert, None, "Vec.insert_fwd") (* Shouldn't be used *);
+        (VecInsert, rg0, "Vec.insert");
+        (VecLen, None, "Vec.len");
+        (VecIndex, None, "Vec.index");
+        (VecIndex, rg0, "Vec.index_back") (* shouldn't be used *);
+        (VecIndexMut, None, "Vec.index_mut");
+        (VecIndexMut, rg0, "Vec.index_mut_back");
+      ]
 
 let assumed_pure_functions () : (pure_assumed_fun_id * string) list =
   match !backend with
@@ -344,7 +361,7 @@ let names_map_init () : names_map_init =
     assumed_adts = assumed_adts ();
     assumed_structs;
     assumed_variants = assumed_variants ();
-    assumed_llbc_functions;
+    assumed_llbc_functions = assumed_llbc_functions ();
     assumed_pure_functions = assumed_pure_functions ();
   }
 
-- 
cgit v1.2.3