diff options
| -rw-r--r-- | fstar/Primitives.fst | 3 | ||||
| -rw-r--r-- | src/ExtractToFStar.ml | 11 |
2 files changed, 13 insertions, 1 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index 6771fe93..b8da70c4 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -9,6 +9,9 @@ type result (a : Type0) : Type0 = | Return : a -> result a | Fail : result a +(*** Misc *) +type char = FStar.Char.char + (*** Scalars *) /// Rk.: most of the following code was at least partially generated let isize_min : int = -9223372036854775808 diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index d1e1176c..0781a811 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -310,7 +310,11 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) if tys = [] then F.pp_print_string fmt "unit" else ( F.pp_print_string fmt "("; - Collections.List.iter_link (F.pp_print_space fmt) + Collections.List.iter_link + (fun () -> + F.pp_print_space fmt (); + F.pp_print_string fmt "&"; + F.pp_print_space fmt ()) (extract_ty ctx fmt true) tys; F.pp_print_string fmt ")") | AdtId _ | Assumed _ -> @@ -956,6 +960,11 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) ctx) ctx def.inputs_lvs in + (* Print the return type *) + F.pp_print_space fmt (); + F.pp_print_string fmt ":"; + F.pp_print_space fmt (); + extract_ty ctx fmt false (Collections.List.to_cons_nil def.signature.outputs); (* Print the "=" *) F.pp_print_space fmt (); F.pp_print_string fmt "="; |