summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml22
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 *)