diff options
author | Son Ho | 2022-04-27 14:17:20 +0200 |
---|---|---|
committer | Son Ho | 2022-04-27 14:17:20 +0200 |
commit | 003d039b5b51619699e96669007f6d095928251c (patch) | |
tree | 0e16580853aab447dedbfb4baad27eabe4bc9089 /src | |
parent | 150e1eab80cebbd0da44e38edd4a4ed434af380f (diff) |
Make minor modifications
Diffstat (limited to 'src')
-rw-r--r-- | src/ExtractToFStar.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0ca3c73a..5e65d560 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -884,6 +884,7 @@ let rec extract_typed_rvalue (ctx : extraction_ctx) (fmt : F.formatter) (** [inside]: controls the introduction of parentheses. See [extract_ty] TODO: replace the formatting boolean [inside] with something more general? + Also, it seems we don't really use it... *) let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = @@ -943,14 +944,14 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) if inside then F.pp_print_string fmt ")" | _ -> raise (Failure "Unreachable")) | _ -> - let use_parentheses = inside && args <> [] in (* "Regular" expression *) (* Open parentheses *) - if use_parentheses then F.pp_print_string fmt "("; + if inside then F.pp_print_string fmt "("; (* Open a box for the application *) F.pp_open_hovbox fmt ctx.indent_incr; (* Print the app expression *) - extract_texpression ctx fmt true app; + let app_inside = inside && args <> [] in + extract_texpression ctx fmt app_inside app; (* Print the arguments *) List.iter (fun ve -> @@ -960,7 +961,7 @@ and extract_App (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Close the box for the application *) F.pp_close_box fmt (); (* Close parentheses *) - if use_parentheses then F.pp_print_string fmt ")" + if inside then F.pp_print_string fmt ")" and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (xl : typed_lvalue list) (e : texpression) : unit = |