diff options
| author | Son Ho | 2022-02-03 21:20:43 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-03 21:20:43 +0100 |
| commit | 4cb88548f08098b7b479c30d48a35b1cf9ee1ac6 (patch) | |
| tree | 20e4292e78a0d489d739eb6833f76c5a353b8532 /src/ExtractToFStar.ml | |
| parent | 15d8fa0043c8fe07fe1ccc7a36ad21e883abdfc3 (diff) | |
Improve the way the matches/switches are extracted
Diffstat (limited to 'src/ExtractToFStar.ml')
| -rw-r--r-- | src/ExtractToFStar.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index c217b6ab..7da5adb8 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -745,12 +745,12 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) extract_texpression ctx fmt false re; F.pp_print_space fmt (); F.pp_print_string fmt "in"; - F.pp_print_space fmt (); ctx) in (* Close the box for the let-binding *) F.pp_close_box fmt (); (* Print the next expression *) + F.pp_print_space fmt (); extract_texpression ctx fmt inside next_e | Switch (scrut, body) -> ( match body with @@ -801,7 +801,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) let extract_branch (sv : scalar_value option) (e_branch : texpression) : unit = F.pp_print_space fmt (); - (* Open a box for the branch *) + (* Open a box for the pattern+branch *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "|"; (* Print the pattern *) @@ -811,10 +811,14 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) | None -> F.pp_print_string fmt "_"); F.pp_print_space fmt (); F.pp_print_string fmt "->"; - (* Print the branch itself *) F.pp_print_space fmt (); + (* Open a box for the branch *) + F.pp_open_hvbox fmt 0; + (* Print the branch itself *) extract_texpression ctx fmt false e_branch; (* Close the box for the branch *) + F.pp_close_box fmt (); + (* Close the box for the pattern+branch *) F.pp_close_box fmt () in @@ -846,7 +850,7 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) (* Extract the branches *) let extract_branch (br : match_branch) : unit = F.pp_print_space fmt (); - (* Open a box for the branch *) + (* Open a box for the pattern+branch *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "|"; (* Print the pattern *) @@ -854,10 +858,14 @@ let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) let ctx = extract_typed_lvalue ctx fmt false br.pat in F.pp_print_space fmt (); F.pp_print_string fmt "->"; - (* Print the branch itself *) F.pp_print_space fmt (); + (* Open a box for the branch *) + F.pp_open_hvbox fmt 0; + (* Print the branch itself *) extract_texpression ctx fmt false br.branch; (* Close the box for the branch *) + F.pp_close_box fmt (); + (* Close the box for the pattern+branch *) F.pp_close_box fmt () in |