From 0b463547ddc409c885859a8bdb577746d87260a2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 May 2024 08:04:30 +0200
Subject: Print the name patterns of the definitions which fail to extract
---
compiler/SymbolicToPure.ml | 9 +++++----
compiler/Translate.ml | 30 +++++++++++++++++++-----------
2 files changed, 24 insertions(+), 15 deletions(-)
(limited to 'compiler')
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..0f6aa7c1 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
@@ -513,9 +520,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
--
cgit v1.2.3
From f37e029fd7ec7dce9410f4baaaad9d09f934de57 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 May 2024 08:06:44 +0200
Subject: Fix a crash which happens when type definitions are ignored
---
compiler/Translate.ml | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
(limited to 'compiler')
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 0f6aa7c1..60ae99f9 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -417,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.
--
cgit v1.2.3