Extraction: believe the ghost field for checking executability

examples/in_progress/prover/Firstorder_formula_impl.mlw

@@ -4259,7 +4259,7 @@ module Impl
           res
       | NL_FTrue ->
         assert { t.model_fo_formula_field = FTrue } ;
-          let () =
+          let _ =
             match t.model_fo_formula_field with | Forall x0 -> absurd
               | Exists x0 -> absurd | And x0 x1 -> absurd
               | Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> ()
@@ -4268,7 +4268,7 @@ module Impl
           in let res = NLC_FTrue in res
       | NL_FFalse ->
         assert { t.model_fo_formula_field = FFalse } ;
-          let () =
+          let _ =
             match t.model_fo_formula_field with | Forall x0 -> absurd
               | Exists x0 -> absurd | And x0 x1 -> absurd
               | Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> absurd

examples/in_progress/prover/Firstorder_formula_list_impl.mlw

@@ -1082,7 +1082,7 @@ module Impl
     match t.nlrepr_fo_formula_list_field with
       | NL_FOFNil ->
         assert { t.model_fo_formula_list_field = FOFNil } ;
-          let () =
+          let _ =
             match t.model_fo_formula_list_field with | FOFNil -> ()
               | FOFCons x0 x1 -> absurd
             end

examples/in_progress/prover/Firstorder_term_impl.mlw

@@ -1910,7 +1910,7 @@ module Impl
     match t.nlrepr_fo_term_list_field with
       | NL_FONil ->
         assert { t.model_fo_term_list_field = FONil } ;
-          let () =
+          let _ =
             match t.model_fo_term_list_field with | FONil -> ()
               | FOCons x0 x1 -> absurd
             end

src/whyml/mlw_exec.ml

@@ -163,7 +163,11 @@ let is_ghost_lv = function
   | LetV pv -> pv.pv_ghost
   | LetA ps -> ps.ps_ghost
 
-let is_exec_pdecl ctx pd = match pd.pd_node with
+let is_exec_pdecl ctx pd =
+  (* don't traverse expr to check for executability: believe
+     the e_ghost field instead *)
+  let is_exec_expr _ctx e = not e.e_ghost in
+  match pd.pd_node with
   | PDtype _
   | PDexn _
   | PDdata _ ->

src/whyml/mlw_ocaml.ml

@@ -681,8 +681,9 @@ module Translate = struct
         | PDrec fdl ->
            List.iter
              (fun {fun_ps=ps} ->
-              Debug.dprintf debug "ignoring non-executable declaration %s@."
-                            ps.ps_name.id_string) fdl
+              Debug.dprintf debug
+                "ignoring non-executable declaration %s (ghost = %b)@."
+                ps.ps_name.id_string ps.ps_ghost) fdl
         | _ -> ()
         end;
         []