diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 0decbff1..2f1898b3 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -791,7 +791,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) else Z.pp_print fmt sv.value; F.pp_print_string fmt " (by intlit))") | Bool b -> - let b = if b then "true" else "false" in + let b = + match !backend with + | HOL4 -> if b then "T" else "F" + | Coq | FStar | Lean -> if b then "true" else "false" + in F.pp_print_string fmt b | Char c -> ( match !backend with @@ -2262,14 +2266,15 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) * let* x = y in // monadic * ... * ]} + * TODO: cleanup * *) - if monadic && !backend = Coq then ( + if monadic && (!backend = Coq || !backend = HOL4) then ( let ctx = extract_typed_pattern ctx fmt true lv in F.pp_print_space fmt (); let arrow = match !backend with - | Coq -> "<-" - | FStar | Lean | HOL4 -> raise (Failure "impossible") + | Coq | HOL4 -> "<-" + | FStar | Lean -> raise (Failure "impossible") in F.pp_print_string fmt arrow; F.pp_print_space fmt (); @@ -2304,15 +2309,14 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_print_string fmt eq; F.pp_print_space fmt (); extract_texpression ctx fmt false re; - (* End the monadic let-binding *) + (* End the let-binding *) (match !backend with | Lean -> - (* In Lean, monadic let-bindings don't require to end with anything *) + (* In Lean, (monadic) let-bindings don't require to end with anything *) () - | Coq | FStar -> + | Coq | FStar | HOL4 -> F.pp_print_space fmt (); - F.pp_print_string fmt "in" - | HOL4 -> F.pp_print_string fmt ";"); + F.pp_print_string fmt "in"); ctx) in (* Close the box for the let-binding *) |