Extraction: extract unit when mask is MaskGhost but the expression is not ghost

drivers/ocaml64.drv

@@ -253,6 +253,21 @@ module mach.int.State63
   syntax val random_int63 "SHOULD_NOT_BE_HERE"
 end
 
+module set.Fset
+  syntax val mem      "SHOULD_NOT_BE_HERE"
+  syntax val (==)     "SHOULD_NOT_BE_HERE"
+  syntax val subset   "SHOULD_NOT_BE_HERE"
+  syntax val is_empty "SHOULD_NOT_BE_HERE"
+  syntax val empty    "SHOULD_NOT_BE_HERE"
+  syntax val add      "SHOULD_NOT_BE_HERE"
+  syntax val remove   "SHOULD_NOT_BE_HERE"
+  syntax val union    "SHOULD_NOT_BE_HERE"
+  syntax val inter    "SHOULD_NOT_BE_HERE"
+  syntax val diff     "SHOULD_NOT_BE_HERE"
+  syntax val choose   "SHOULD_NOT_BE_HERE"
+  syntax val cardinal "SHOULD_NOT_BE_HERE"
+end
+
 module mach.peano.Peano
   syntax type t      "int"
   syntax val  to_int "Z.of_int %1"

src/mlw/compile.ml

@@ -655,6 +655,9 @@ module Translate = struct
     (* assert (mask <> MaskGhost); *)
     match e.e_node with
     | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
+    | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole when mask = MaskGhost ->
+        ML.e_unit
+    | Econst _ | Evar _   | Efun _ | Eassign _ | Ewhile _
     | Efor   _ | Eraise _ | Eexn _ | Eabsurd   | Ehole    -> e
     | Eapp (rs, el) when is_rs_tuple rs ->
         begin match visible_of_mask mask el with

src/mlw/ocaml_printer.ml

@@ -534,9 +534,6 @@ module Print = struct
           (print_uident info) xs.xs_name (print_ty ~paren:true info) t
           (print_expr info) e
     | Eignore e -> fprintf fmt "ignore (%a)" (print_expr info) e
-  (* | Enot _ -> (\* TODO *\) assert false *)
-  (* | Ebinop _ -> (\* TODO *\) assert false *)
-  (* | Ecast _ -> (\* TODO *\) assert false *)
 
   and print_branch info fmt (p, e) =
     fprintf fmt "@[<hov 2>| %a ->@ @[%a@]@]"