Merge pull request #199 from AeneasVerif/son/errors

Print name patterns when ignoring definitions

2 files changed, 29 insertions, 17 deletions

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6c925bcd..4aa24fcf 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3923,14 +3923,15 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
 
 let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
   List.filter_map
-    (fun a ->
-      try Some (translate_type_decl ctx a)
+    (fun d ->
+      try Some (translate_type_decl ctx d)
       with CFailure (meta, _) ->
         let env = PrintPure.decls_ctx_to_fmt_env ctx in
-        let name = PrintPure.name_to_string env a.name in
+        let name = PrintPure.name_to_string env d.name in
+        let name_pattern = TranslateCore.name_to_pattern_string ctx d.name in
         save_error __FILE__ __LINE__ meta
           ("Could not translate type decl '" ^ name
-         ^ "' because of previous error");
+         ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
         None)
     (TypeDeclId.Map.values ctx.type_ctx.type_decls)
 
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 72a98c3d..60ae99f9 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -206,9 +206,10 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
       (translate_function_to_pure_aux trans_ctx pure_type_decls fun_dsigs fdef)
   with CFailure (meta, _) ->
     let name = name_to_string trans_ctx fdef.name in
+    let name_pattern = name_to_pattern_string trans_ctx fdef.name in
     save_error __FILE__ __LINE__ meta
       ("Could not translate the function '" ^ name
-     ^ "' because of previous error");
+     ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
     None
 
 (* TODO: factor out the return type *)
@@ -245,9 +246,11 @@ let translate_crate_to_pure (crate : crate) :
                    trans_ctx fdef )
            with CFailure (meta, _) ->
              let name = name_to_string trans_ctx fdef.name in
+             let name_pattern = name_to_pattern_string trans_ctx fdef.name in
              save_error __FILE__ __LINE__ meta
                ("Could not translate the function signature of '" ^ name
-              ^ "' because of previous error");
+              ^ " because of previous error\nName pattern: '" ^ name_pattern
+              ^ "'");
              None)
          (FunDeclId.Map.values crate.fun_decls))
   in
@@ -262,13 +265,15 @@ let translate_crate_to_pure (crate : crate) :
   (* Translate the trait declarations *)
   let trait_decls =
     List.filter_map
-      (fun a ->
-        try Some (SymbolicToPure.translate_trait_decl trans_ctx a)
+      (fun d ->
+        try Some (SymbolicToPure.translate_trait_decl trans_ctx d)
         with CFailure (meta, _) ->
-          let name = name_to_string trans_ctx a.name in
+          let name = name_to_string trans_ctx d.name in
+          let name_pattern = name_to_pattern_string trans_ctx d.name in
           save_error __FILE__ __LINE__ meta
             ("Could not translate the trait declaration '" ^ name
-           ^ "' because of previous error");
+           ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"
+            );
           None)
       (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
   in
@@ -276,13 +281,15 @@ let translate_crate_to_pure (crate : crate) :
   (* Translate the trait implementations *)
   let trait_impls =
     List.filter_map
-      (fun a ->
-        try Some (SymbolicToPure.translate_trait_impl trans_ctx a)
+      (fun d ->
+        try Some (SymbolicToPure.translate_trait_impl trans_ctx d)
         with CFailure (meta, _) ->
-          let name = name_to_string trans_ctx a.name in
+          let name = name_to_string trans_ctx d.name in
+          let name_pattern = name_to_pattern_string trans_ctx d.name in
           save_error __FILE__ __LINE__ meta
             ("Could not translate the trait instance '" ^ name
-           ^ "' because of previous error");
+           ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'"
+            );
           None)
       (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
   in
@@ -410,9 +417,12 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
     else ExtractBase.MutRecInner
   in
 
-  (* Retrieve the declarations *)
+  (* Retrieve the declarations - note that some of them might have been ignored in
+     case of errors *)
   let defs =
-    List.map (fun id -> Pure.TypeDeclId.Map.find id ctx.trans_types) ids
+    List.filter_map
+      (fun id -> Pure.TypeDeclId.Map.find_opt id ctx.trans_types)
+      ids
   in
 
   (* Check if the definition are builtin - if yes they must be ignored.
@@ -513,9 +523,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
       try Some (SymbolicToPure.translate_global ctx.trans_ctx global)
       with CFailure (meta, _) ->
         let name = name_to_string ctx.trans_ctx global.name in
+        let name_pattern = name_to_pattern_string ctx.trans_ctx global.name in
         save_error __FILE__ __LINE__ meta
           ("Could not translate the global declaration '" ^ name
-         ^ "' because of previous error");
+         ^ " because of previous error\nName pattern: '" ^ name_pattern ^ "'");
         None
     in
     Extract.extract_global_decl ctx fmt global body config.interface