diff options
author | Son Ho | 2022-02-04 13:33:45 +0100 |
---|---|---|
committer | Son Ho | 2022-02-04 13:33:45 +0100 |
commit | 3ead957cf13ddd3b48ee85c008c6d56e44726eb4 (patch) | |
tree | 51e694665a3623cea8250bb0c3e4523c321fada1 /src/ExtractToFStar.ml | |
parent | 25200ad9664980d3276dd7462b4845a1a21c3e64 (diff) |
Work on decomposition of monadic let-bindings for F*
Diffstat (limited to '')
-rw-r--r-- | src/ExtractToFStar.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 7e4a11fe..1d45b239 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -824,15 +824,23 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); (* Open a box for the branch *) F.pp_open_hvbox fmt 0; + (* Print the `begin` if necessary *) let parenth = PureUtils.expression_requires_parentheses e_branch in - if parenth then F.pp_print_string fmt "("; + if parenth then ( + F.pp_print_string fmt "begin"; + F.pp_print_space fmt ()); + (* Print the branch expression *) extract_texpression ctx fmt false e_branch; - if parenth then F.pp_print_string fmt ")"; + (* Close the `begin ... end ` *) + if parenth then ( + F.pp_print_space fmt (); + F.pp_print_string fmt "end"); (* Close the box for the branch *) F.pp_close_box fmt (); (* Close the box for the then/else+branch *) F.pp_close_box fmt () in + extract_branch true e_then; extract_branch false e_else; (* Close the box for the whole `if ... then ... else ...` *) |