From 6395dbcc29480a37cd73b51deac5f1b289131e4f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Mar 2022 12:25:49 +0100
Subject: Fix a minor issue with external function declarations

---
 Makefile              |  5 ++++-
 src/ExtractToFStar.ml | 21 +++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)

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";
-- 
cgit v1.2.3