diff options
author | Son Ho | 2022-02-10 10:33:46 +0100 |
---|---|---|
committer | Son Ho | 2022-02-10 10:33:46 +0100 |
commit | e9ef01432a7464a0d5472a528169696ae140fad0 (patch) | |
tree | 14a0fd64d0de54e8c3bb2572fed80bf4e95acd38 /src | |
parent | 8e3be66093318a4a31419ae5018f9d413d756cd5 (diff) |
Make more improvements to formatting
Diffstat (limited to 'src')
-rw-r--r-- | src/ExtractToFStar.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index cca2b22c..a668a5d0 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -956,7 +956,6 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) * with no input parameters *) (* The type parameters *) if def.signature.type_params <> [] then ( - F.pp_print_space fmt (); (* Open a box for the type parameters *) F.pp_open_hovbox fmt 0; F.pp_print_string fmt "("; @@ -970,12 +969,12 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "Type0)"; (* Close the box for the type parameters *) - F.pp_close_box fmt ()); + F.pp_close_box fmt (); + F.pp_print_space fmt ()); (* The input parameters - note that doing this adds bindings to the context *) let ctx_body = List.fold_left (fun ctx (lv : typed_lvalue) -> - F.pp_print_space fmt (); (* Open a box for the input parameter *) F.pp_open_hovbox fmt 0; F.pp_print_string fmt "("; @@ -987,6 +986,7 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ")"; (* Close the box for the input parameters *) F.pp_close_box fmt (); + F.pp_print_space fmt (); ctx) ctx def.inputs_lvs in @@ -1017,32 +1017,34 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) ("(** [" ^ Print.name_to_string def.basename ^ "]: decreases clause *)"); F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on - * one line - TODO: remove? *) + * one line *) F.pp_open_hvbox fmt 0; (* Add the `unfold` keyword *) F.pp_print_string fmt "unfold"; F.pp_print_space fmt (); - (* Open a box for "let FUN_NAME (PARAMS) =" *) + (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) + F.pp_open_hvbox fmt ctx.indent_incr; + (* Open a box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_open_hovbox fmt ctx.indent_incr; (* > "let FUN_NAME" *) F.pp_print_string fmt ("let " ^ def_name); + F.pp_print_space fmt (); (* Extract the parameters *) let _, _ = extract_fun_parameters ctx fmt def in - (* Print the signature *) - F.pp_print_space fmt (); F.pp_print_string fmt ":"; + (* Print the signature *) F.pp_print_space fmt (); F.pp_print_string fmt "nat"; (* Print the "=" *) F.pp_print_space fmt (); F.pp_print_string fmt "="; - (* Close the box for "let FUN_NAME (PARAMS) =" *) + (* Close the box for "let FUN_NAME (PARAMS) : EFFECT =" *) F.pp_close_box fmt (); - (* Add a space before the "admit" and increment the indentation if we need - * to break line *) - F.pp_print_break fmt 1 ctx.indent_incr; + F.pp_print_space fmt (); (* Print the "admit ()" *) F.pp_print_string fmt "admit ()"; + (* Close the box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *) + F.pp_close_box fmt (); (* Close the box for the whole definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) @@ -1080,6 +1082,7 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) match qualif with Let -> "let" | LetRec -> "let rec" | And -> "and" in F.pp_print_string fmt (qualif ^ " " ^ def_name); + F.pp_print_space fmt (); let ctx, ctx_body = extract_fun_parameters ctx fmt def in (* Print the return type - note that we have to be careful when * printing the input values for the decrease clause, because @@ -1087,7 +1090,6 @@ let extract_fun_def (ctx : extraction_ctx) (fmt : F.formatter) * the bindings we introduced above. * TODO: figure out a cleaner way *) let _ = - F.pp_print_space fmt (); F.pp_print_string fmt ":"; F.pp_print_space fmt (); (* Open a box for the return type *) |