summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-12-22 18:47:50 +0100
committerSon Ho2023-12-22 18:47:50 +0100
commit455ba366f9c8d07a1f1848ec0960b1f2d161e7cf (patch)
tree03493e0e2eddef8187296befceeda40eba102c4c /compiler
parente799ef503dda30b6dcbecb042ecb0fae1a71fa81 (diff)
Update the library for F*
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractBuiltin.ml8
-rw-r--r--compiler/Translate.ml8
2 files changed, 15 insertions, 1 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index 24d16dca..ee8d4831 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -232,6 +232,14 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info list) list
let mk_fun (rust_name : string) (extract_name : string option)
(filter : bool list option) (with_back : bool) (back_no_suffix : bool) :
pattern * bool list option * builtin_fun_info list =
+ (* [back_no_suffix] is used to control whether the backward function should
+ have the suffix "_back" or not (if not, then the forward function has the
+ prefix "_fwd", and is filtered anyway). This is pertinent only if we split
+ the fwd/back functions. *)
+ let back_no_suffix = back_no_suffix && not !Config.return_back_funs in
+ (* Same for the [with_back] option: this is pertinent only if we split
+ the fwd/back functions *)
+ let with_back = with_back && not !Config.return_back_funs in
let rust_name =
try parse_pattern rust_name
with Failure _ ->
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index ccc46420..55a94302 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -1171,7 +1171,13 @@ let translate_crate (filename : string) (dest_dir : string) (crate : crate) :
let exe_dir = Filename.dirname Sys.argv.(0) in
let primitives_src_dest =
match !Config.backend with
- | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst")
+ | FStar ->
+ let src =
+ if !Config.return_back_funs then
+ "/backends/fstar/merge/Primitives.fst"
+ else "/backends/fstar/split/Primitives.fst"
+ in
+ Some (src, "Primitives.fst")
| Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v")
| Lean -> None
| HOL4 -> None