From 952c4c964e33eeb6956d84efce3ef1b7575f311f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 17 Sep 2023 00:56:51 +0200
Subject: Fix more issues with the extraction

---
 compiler/LlbcAstUtils.ml | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

(limited to 'compiler/LlbcAstUtils.ml')

diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 8c8bbabe..a982af30 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -15,13 +15,22 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
 
 (** Return the opaque declarations found in the crate.
 
+    [filter_assumed]: if [true], do not consider as opaque the external definitions
+    that we will map to definitions from the standard library.
+
     Remark: the list of functions also contains the list of opaque global bodies.
  *)
-let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list =
+let crate_get_opaque_decls (k : crate) (filter_assumed : bool) :
+    T.type_decl list * fun_decl list =
   let open ExtractAssumed in
   let is_opaque_fun (d : fun_decl) : bool =
     let sname = name_to_simple_name d.name in
-    d.body = None && not (SimpleNameMap.mem sname assumed_globals_map)
+    d.body = None
+    (* Something to pay attention to: we must ignore trait method *declarations*
+       (which don't have a body but must not be considered as opaque) *)
+    && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
+    && ((not filter_assumed)
+       || not (SimpleNameMap.mem sname assumed_globals_map))
   in
   let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in
   (* Note that by checking the function bodies we also the globals *)
@@ -30,5 +39,5 @@ let crate_get_opaque_decls (k : crate) : T.type_decl list * fun_decl list =
 
 (** Return true if the crate contains opaque declarations, ignoring the assumed
     definitions. *)
-let crate_has_opaque_decls (k : crate) : bool =
-  crate_get_opaque_decls k <> ([], [])
+let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool =
+  crate_get_opaque_decls k filter_assumed <> ([], [])
-- 
cgit v1.2.3