summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-07-05 15:17:58 +0200
committerSon Ho2023-07-05 15:17:58 +0200
commit5ca36bfc50083a01af2b7ae5f75993a520757ef5 (patch)
tree11660b73a27ad2e0807a18ac9286a1e87c560050 /compiler
parentc07721dedb2cfe4c726c42606e623395cdfe5b80 (diff)
Simplify the names used in Primitives.lean
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml49
1 files changed, 33 insertions, 16 deletions
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 ();
}