From 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 May 2023 15:23:48 +0200
Subject: Make the unfolding theorems collection from evalLib persistent

---
 compiler/Extract.ml | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

(limited to 'compiler')

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 *)
-- 
cgit v1.2.3