diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 13 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 4 |
2 files changed, 12 insertions, 5 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 3ca003a4..d1e1176c 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -37,6 +37,7 @@ let fstar_keywords = "with"; "assert"; "Type0"; + "unit"; ] let fstar_int_name (int_ty : integer_type) = @@ -304,10 +305,14 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Adt (type_id, tys) -> ( match type_id with | Tuple -> - F.pp_print_string fmt "("; - Collections.List.iter_link (F.pp_print_space fmt) - (extract_ty ctx fmt true) tys; - F.pp_print_string fmt ")" + (* This is a bit annoying, but in F* `()` is not the unit type: + * we have to write `unit`... *) + if tys = [] then F.pp_print_string fmt "unit" + else ( + F.pp_print_string fmt "("; + Collections.List.iter_link (F.pp_print_space fmt) + (extract_ty ctx fmt true) tys; + F.pp_print_string fmt ")") | AdtId _ | Assumed _ -> if inside then F.pp_print_string fmt "("; F.pp_print_string fmt (ctx_get_type type_id ctx); diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index cbc2409d..1ef4b325 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -633,7 +633,9 @@ let to_monadic (def : fun_def) : fun_def = let id, _ = VarId.fresh var_cnt in let var = { id; basename = None; ty = unit_ty } in let inputs = [ var ] in - { def with signature; inputs }) + let input_lv = mk_typed_lvalue_from_var var None in + let inputs_lvs = [ input_lv ] in + { def with signature; inputs; inputs_lvs }) else def in (* Then the output type *) |