diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 57 |
1 files changed, 46 insertions, 11 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 348183c5..28e5531d 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -41,7 +41,7 @@ let translate_function_to_symbolics (trans_ctx : trans_ctx) (fdef : fun_decl) : of backward functions, we also provide names for the outputs. TODO: maybe we should introduce a record for this. *) -let translate_function_to_pure (trans_ctx : trans_ctx) +let translate_function_to_pure_hook (trans_ctx : trans_ctx) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : pure_fun_translation_no_loops = @@ -195,6 +195,17 @@ let translate_function_to_pure (trans_ctx : trans_ctx) | None -> SymbolicToPure.translate_fun_decl ctx None | Some (_, ast) -> SymbolicToPure.translate_fun_decl ctx (Some ast) +let translate_function_to_pure (trans_ctx : trans_ctx) + (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) + (fun_dsigs : Pure.decomposed_fun_sig FunDeclId.Map.t) (fdef : fun_decl) : + pure_fun_translation_no_loops option = + try + Some + (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None + (* TODO: factor out the return type *) let translate_crate_to_pure (crate : crate) : trans_ctx @@ -220,32 +231,51 @@ let translate_crate_to_pure (crate : crate) : (* Compute the decomposed fun sigs for the whole crate *) let fun_dsigs = FunDeclId.Map.of_list - (List.map + (List.filter_map (fun (fdef : LlbcAst.fun_decl) -> - ( fdef.def_id, - SymbolicToPure.translate_fun_sig_from_decl_to_decomposed trans_ctx - fdef )) + try + Some + ( fdef.def_id, + SymbolicToPure.translate_fun_sig_from_decl_to_decomposed + trans_ctx fdef ) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (FunDeclId.Map.values crate.fun_decls)) in (* Translate all the *transparent* functions *) let pure_translations = - List.map + List.filter_map (translate_function_to_pure trans_ctx type_decls_map fun_dsigs) (FunDeclId.Map.values crate.fun_decls) in (* Translate the trait declarations *) let trait_decls = - List.map - (SymbolicToPure.translate_trait_decl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_decl trans_ctx a) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls) in (* Translate the trait implementations *) let trait_impls = - List.map - (SymbolicToPure.translate_trait_impl trans_ctx) + List.filter_map + (fun a -> + try Some (SymbolicToPure.translate_trait_impl trans_ctx a) + with CFailure (meta, _) -> + let () = + save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" + in + None) (TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls) in @@ -471,7 +501,12 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx) groups are always singletons, so the [extract_global_decl] function takes care of generating the delimiters. *) - let global = SymbolicToPure.translate_global ctx.trans_ctx global in + let global = + try Some (SymbolicToPure.translate_global ctx.trans_ctx global) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None + in Extract.extract_global_decl ctx fmt global body config.interface (** Utility. |