Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Print name patterns when ignoring definitions #199

Merged
merged 2 commits into from
May 24, 2024
Merged

Print name patterns when ignoring definitions #199

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
0b46354
Print the name patterns of the definitions which fail to extract
sonmarcho May 24, 2024
f37e029
Fix a crash which happens when type definitions are ignored
sonmarcho May 24, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions compiler/SymbolicToPure.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
37 changes: 24 additions & 13 deletions compiler/Translate.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *)
Expand Down Expand Up @@ -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
Expand All @@ -262,27 +265,31 @@ 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

(* 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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
Loading