diff options
| author | Son HO | 2024-04-07 15:09:58 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-07 15:09:58 +0200 |
| commit | 05164f1ea87b7da14f60e6dbcc718a4f8d639ea1 (patch) | |
| tree | 7973a53f134c38a856376b6204a7c76900eaafe7 /compiler/Extract.ml | |
| parent | d8650bfc5c4dc78fda13953dac93c9e6c24489d1 (diff) | |
| parent | a9a2f81e365eeef4fd157fb56cd5107f95c91163 (diff) | |
Merge pull request #113 from AeneasVerif/escherichia/error_catching_translate
Error catching should tell when code couldn't be generated
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index af0bf98d..985fb470 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -219,7 +219,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list) ^ string_of_int (List.length types) ^ " type arguments" in - log#serror err; + save_error __FILE__ __LINE__ None err; Result.Error (types, err)) else let types = List.combine filter types in @@ -1879,7 +1879,7 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) [{start,end}_gloabl_decl_group], contrary to {!extract_type_decl} and {!extract_fun_decl}. *) -let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) +let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) (global : global_decl) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; @@ -1974,6 +1974,12 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break to insert lines between declarations *) F.pp_print_break fmt 0 0 +let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) + (global : global_decl option) (body : fun_decl) (interface : bool) : unit = + match global with + | Some global -> extract_global_decl_aux ctx fmt global body interface + | None -> () + (** Similar to {!extract_trait_decl_register_names} *) let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) (trait_decl : trait_decl) |