diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 21 |
2 files changed, 25 insertions, 1 deletions
@@ -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"; |