summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile5
-rw-r--r--src/ExtractToFStar.ml21
2 files changed, 25 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index cd98429e..c9839b45 100644
--- a/Makefile
+++ b/Makefile
@@ -30,7 +30,7 @@ build:
# Test the project
.PHONY: test
test: build translate-no_nested_borrows translate-hashmap translate-paper \
- translate-nll-betree_nll
+ translate-external translate-nll-betree_nll
# Add specific options to some tests
translate-no_nested_borrows translate-paper: \
@@ -42,6 +42,9 @@ translate-hashmap: SUBDIR:=hashmap
translate-nll-betree_nll: TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
translate-nll-betree_nll: SUBDIR:=misc
+translate-external: TRANS_OPTIONS +=
+translate-external: SUBDIR:=misc
+
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index eea52063..9ec74ff0 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1102,6 +1102,23 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
in
(ctx, ctx_body)
+(** A small utility to print the types of the input parameters in the form:
+ `u32 -> list u32 -> ...`
+ (we don't print the return type of the function)
+
+ This is used for opaque function declarations, in particular.
+ *)
+let extract_fun_input_parameters_types (ctx : extraction_ctx)
+ (fmt : F.formatter) (def : fun_decl) : unit =
+ let extract_param (ty : ty) : unit =
+ let inside = false in
+ extract_ty ctx fmt inside ty;
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "->";
+ F.pp_print_space fmt ()
+ in
+ List.iter extract_param def.signature.inputs
+
(** Extract a decrease clause function template body.
In order to help the user, we can generate a template for the functions
@@ -1220,6 +1237,10 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for the return type *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* Print the return type *)
+ (* For opaque definitions, as we don't have named parameters under the hand,
+ * we don't print parameters in the form `(x : a) (y : b) ...` above,
+ * but wait until here to print the types: `a -> b -> ...`. *)
+ if is_opaque then extract_fun_input_parameters_types ctx fmt def;
(* `Tot` *)
if has_decreases_clause then (
F.pp_print_string fmt "Tot";