summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-02-05 22:13:05 +0100
committerSon HO2023-06-04 21:44:33 +0200
commit6cc10dc67f74cb0abb3062b02c8a94bf34cc938d (patch)
treef8055d159fb99cec735a1607288ec8fa895dc86c /compiler
parentc6913b8bf90689d8961c47f59896443e7fae164d (diff)
Improve formatting further by removing useless spaces
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml37
1 files changed, 22 insertions, 15 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 4c23989e..df7f37e1 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1848,8 +1848,12 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(scrut : texpression) (body : switch_body) : unit =
- (* Open a box for the whole expression *)
- F.pp_open_hvbox fmt 0;
+ (* Open a box for the whole expression.
+
+ In the case of Lean, we rely on indentation to delimit the end of the
+ branches, and need to insert line breaks: we thus use a vbox.
+ *)
+ if !Config.backend = Lean then F.pp_open_vbox fmt 0 else F.pp_open_hvbox fmt 0;
(* Open parentheses *)
if inside then F.pp_print_string fmt "(";
(* Extract the switch *)
@@ -1863,6 +1867,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
extract_texpression ctx fmt scrut_inside scrut;
(* Close the box for the [if e] *)
F.pp_close_box fmt ();
+
(* Extract the branches *)
let extract_branch (is_then : bool) (e_branch : texpression) : unit =
F.pp_print_space fmt ();
@@ -1954,10 +1959,10 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
List.iter extract_branch branches;
- (* End the match *)
- F.pp_print_space fmt ();
- (* Relying on indentation in Lean *)
- if !backend <> Lean then F.pp_print_string fmt "end");
+ (* End the match - we rely on indentation in Lean *)
+ if !backend <> Lean then (
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "end"));
(* Close parentheses *)
if inside then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
@@ -2370,9 +2375,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ();
(* Coq: add a "." *)
print_decl_end_delimiter fmt kind;
- (* Close the outer box for the definition *)
- F.pp_close_box fmt ();
- (* Termination clause *)
+ (* Termination clause and proof for Lean *)
if has_decreases_clause && !backend = Lean then (
let def_body = Option.get def.body in
let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in
@@ -2381,14 +2384,14 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
in
let vars = Collections.List.prefix num_fwd_inputs all_vars in
- (* terminates_by *)
+ (* termination_by *)
let terminates_name =
ctx_get_terminates_clause def.def_id def.loop_id ctx
in
F.pp_print_break fmt 0 0;
- (* Open a box for the whole [terminates_by CALL => DECREASES] *)
+ (* Open a box for the whole [termination_by CALL => DECREASES] *)
F.pp_open_hvbox fmt ctx.indent_incr;
- (* Open a box for {terminates_by CALL =>} *)
+ (* Open a box for {termination_by CALL =>} *)
F.pp_open_hovbox fmt ctx.indent_incr;
F.pp_print_string fmt "termination_by";
F.pp_print_space fmt ();
@@ -2400,7 +2403,7 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
all_vars;
F.pp_print_space fmt ();
F.pp_print_string fmt "=>";
- (* Close the box for [terminates_by CALL =>] *)
+ (* Close the box for [termination_by CALL =>] *)
F.pp_close_box fmt ();
F.pp_print_space fmt ();
(* Open the box for [DECREASES] *)
@@ -2419,12 +2422,13 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
vars;
(* Close the box for [DECREASES] *)
F.pp_close_box fmt ();
- (* Close the box for the whole [terminates_by CALL => DECREASES] *)
+ (* Close the box for the whole [termination_by CALL => DECREASES] *)
F.pp_close_box fmt ();
- let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
F.pp_print_break fmt 0 0;
+ (* Open a box for the [decreasing by ...] *)
F.pp_open_hvbox fmt ctx.indent_incr;
+ let decreases_name = ctx_get_decreases_clause def.def_id def.loop_id ctx in
F.pp_print_string fmt "decreasing_by";
F.pp_print_space fmt ();
F.pp_open_hvbox fmt ctx.indent_incr;
@@ -2435,7 +2439,10 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_string fmt (ctx_get_var v ctx_body))
vars;
F.pp_close_box fmt ();
+ (* Close the box for the [decreasing by ...] *)
F.pp_close_box fmt ());
+ (* Close the outer box for the definition *)
+ F.pp_close_box fmt ();
(* Add breaks to insert new lines between definitions *)
F.pp_print_break fmt 0 0