summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorJonathan Protzenko2023-01-25 14:44:27 -0800
committerSon HO2023-06-04 21:44:33 +0200
commitd841397d93c06310a7e91087e15ba441c2b74f26 (patch)
tree468ff48e50bc6a94529ccced3858bd4f3773d363 /compiler
parent3d742e11a43e873e99bd371ec13c55b212f80ee6 (diff)
More cosmetic improvements
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml32
1 files changed, 20 insertions, 12 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 44bc5e1c..98a5f41a 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -137,13 +137,13 @@ let keywords () =
in
List.concat [ named_unops; named_binops; misc ]
-let assumed_adts : (assumed_ty * string) list =
+let assumed_adts () : (assumed_ty * string) list =
[
(State, "state");
(Result, "result");
(Error, "error");
(Fuel, "nat");
- (Option, "option");
+ (Option, if !backend = Lean then "Option" else "option");
(Vec, "vec");
]
@@ -180,8 +180,8 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
(Error, error_failure_id, "panic");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
- (Option, option_some_id, "@some");
- (Option, option_none_id, "@none");
+ (Option, option_some_id, "some");
+ (Option, option_none_id, "none");
]
let assumed_llbc_functions :
@@ -228,7 +228,7 @@ let assumed_pure_functions (): (pure_assumed_fun_id * string) list =
let names_map_init () : names_map_init =
{
keywords = keywords ();
- assumed_adts;
+ assumed_adts = assumed_adts ();
assumed_structs;
assumed_variants = assumed_variants ();
assumed_llbc_functions;
@@ -1380,6 +1380,9 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
TODO: we don't need something very generic anymore (some definitions used
to be polymorphic).
+
+ TODO: this does roughly the same thing as extract_adt_cons -- make the
+ latter call the former
*)
let extract_adt_g_value
(extract_value : extraction_ctx -> bool -> 'v -> extraction_ctx)
@@ -1696,7 +1699,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Open a box for the whole expression *)
F.pp_open_hvbox fmt 0;
(* Open parentheses *)
- if inside then F.pp_print_string fmt "(";
+ if inside && !backend <> Lean then F.pp_print_string fmt "(";
(* Extract the let-bindings *)
let extract_let (ctx : extraction_ctx) (monadic : bool) (lv : typed_pattern)
(re : texpression) : extraction_ctx =
@@ -1728,7 +1731,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_space fmt ();
let ctx = extract_typed_pattern ctx fmt true lv in
F.pp_print_space fmt ();
- let eq = match !backend with FStar -> "=" | Coq -> ":=" | Lean -> "<-" in
+ let eq = match !backend with FStar -> "=" | Coq -> ":=" | Lean -> if monadic then "<-" else ":=" in
F.pp_print_string fmt eq;
F.pp_print_space fmt ();
extract_texpression ctx fmt false re;
@@ -1743,9 +1746,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Return *)
ctx
in
+ let exists_monadic = List.exists (fun (m, _, _) -> m) lets in
(* If Lean, we rely on monadic blocks, so we insert a do and open a new box
immediately *)
- if !backend = Lean then begin
+ if !backend = Lean && exists_monadic then begin
F.pp_open_vbox fmt ctx.indent_incr;
F.pp_print_string fmt "do";
F.pp_print_space fmt ();
@@ -1762,10 +1766,10 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
(* Close the box for the next expression *)
F.pp_close_box fmt ();
(* do-box (Lean only) *)
- if !backend = Lean then
+ if !backend = Lean && exists_monadic then
F.pp_close_box fmt ();
(* Close parentheses *)
- if inside then F.pp_print_string fmt ")";
+ if inside && !backend <> Lean then F.pp_print_string fmt ")";
(* Close the box for the whole expression *)
F.pp_close_box fmt ()
@@ -1807,9 +1811,11 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
F.pp_print_space fmt ();
F.pp_print_string fmt "begin";
F.pp_print_space fmt ()
- | Coq | Lean ->
+ | Coq ->
F.pp_print_string fmt " (";
F.pp_print_cut fmt ()
+ | Lean ->
+ F.pp_print_cut fmt ()
);
(* Print the branch expression *)
extract_texpression ctx fmt false e_branch;
@@ -1819,7 +1825,9 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| FStar ->
F.pp_print_space fmt ();
F.pp_print_string fmt "end"
- | Coq | Lean -> F.pp_print_string fmt ")");
+ | Coq -> F.pp_print_string fmt ")"
+ | Lean -> ()
+ );
(* Close the box for the branch *)
if not parenth then F.pp_close_box fmt ();
(* Close the box for the then/else+branch *)