diff options
| -rw-r--r-- | compiler/Extract.ml | 181 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 7 | ||||
| -rw-r--r-- | compiler/Translate.ml | 57 |
3 files changed, 144 insertions, 101 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index af0bf98d..1fc8a97f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1880,99 +1880,102 @@ let extract_global_decl_hol4_opaque (meta : Meta.meta) (ctx : extraction_ctx) and {!extract_fun_decl}. *) let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) - (global : global_decl) (body : fun_decl) (interface : bool) : unit = + (global : global_decl option) (body : fun_decl) (interface : bool) : unit = let meta = body.meta in sanity_check __FILE__ __LINE__ body.is_global_decl_body meta; sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta; - - (* Add a break then the name of the corresponding LLBC declaration *) - F.pp_print_break fmt 0 0; - let name = - if !Config.extract_external_name_patterns && not global.is_local then - Some global.llbc_name - else None - in - extract_comment_with_span ctx fmt - [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] - name global.meta.span; - F.pp_print_space fmt (); - - let decl_name = ctx_get_global meta global.def_id ctx in - let body_name = - ctx_get_function meta - (FromLlbc (Pure.FunId (FRegular global.body_id), None)) - ctx - in - let decl_ty, body_ty = - let ty = body.signature.output in - if body.signature.fwd_info.effect_info.can_fail then - (unwrap_result_ty meta ty, ty) - else (ty, mk_result_ty ty) - in - (* Add the type parameters *) - let ctx, type_params, cg_params, trait_clauses = - ctx_add_generic_params meta global.llbc_name global.llbc_generics - global.generics ctx - in - match body.body with - | None -> - (* No body: only generate a [val x_c : u32] declaration *) - let kind = if interface then Declared else Assumed in - if !backend = HOL4 then - extract_global_decl_hol4_opaque meta ctx fmt decl_name global.generics - decl_ty - else - extract_global_decl_body_gen meta ctx fmt kind decl_name global.generics - type_params cg_params trait_clauses decl_ty None - | Some body -> - (* There is a body *) - (* Generate: [let x_body : result u32 = Return 3] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name - global.generics type_params cg_params trait_clauses body_ty - (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); + match global with + | Some global -> ( + (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - (* Generate: [let x_c : u32 = eval_global x_body] *) - extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name - global.generics type_params cg_params trait_clauses decl_ty - (Some - (fun fmt -> - let all_params = - List.concat [ type_params; cg_params; trait_clauses ] - in - let extract_params () = - List.iter - (fun p -> - F.pp_print_space fmt (); - F.pp_print_string fmt p) - all_params - in - let use_brackets = all_params <> [] in - (* Extract the name *) - let before, after = - match !backend with - | FStar | Lean -> - ( (fun () -> - F.pp_print_string fmt "eval_global"; - F.pp_print_space fmt ()), - fun () -> () ) - | Coq -> - ((fun () -> ()), fun () -> F.pp_print_string fmt "%global") - | HOL4 -> - ( (fun () -> - F.pp_print_string fmt "get_return_value"; - F.pp_print_space fmt ()), - fun () -> () ) - in - before (); - if use_brackets then F.pp_print_string fmt "("; - F.pp_print_string fmt body_name; - (* Extract the generic params *) - extract_params (); - if use_brackets then F.pp_print_string fmt ")"; - (* *) - after ())); - (* Add a break to insert lines between declarations *) - F.pp_print_break fmt 0 0 + let name = + if !Config.extract_external_name_patterns && not global.is_local then + Some global.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ] + name global.meta.span; + F.pp_print_space fmt (); + + let decl_name = ctx_get_global meta global.def_id ctx in + let body_name = + ctx_get_function meta + (FromLlbc (Pure.FunId (FRegular global.body_id), None)) + ctx + in + let decl_ty, body_ty = + let ty = body.signature.output in + if body.signature.fwd_info.effect_info.can_fail then + (unwrap_result_ty meta ty, ty) + else (ty, mk_result_ty ty) + in + (* Add the type parameters *) + let ctx, type_params, cg_params, trait_clauses = + ctx_add_generic_params meta global.llbc_name global.llbc_generics + global.generics ctx + in + match body.body with + | None -> + (* No body: only generate a [val x_c : u32] declaration *) + let kind = if interface then Declared else Assumed in + if !backend = HOL4 then + extract_global_decl_hol4_opaque meta ctx fmt decl_name + global.generics decl_ty + else + extract_global_decl_body_gen meta ctx fmt kind decl_name + global.generics type_params cg_params trait_clauses decl_ty None + | Some body -> + (* There is a body *) + (* Generate: [let x_body : result u32 = Return 3] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec body_name + global.generics type_params cg_params trait_clauses body_ty + (Some (fun fmt -> extract_texpression meta ctx fmt false body.body)); + F.pp_print_break fmt 0 0; + (* Generate: [let x_c : u32 = eval_global x_body] *) + extract_global_decl_body_gen meta ctx fmt SingleNonRec decl_name + global.generics type_params cg_params trait_clauses decl_ty + (Some + (fun fmt -> + let all_params = + List.concat [ type_params; cg_params; trait_clauses ] + in + let extract_params () = + List.iter + (fun p -> + F.pp_print_space fmt (); + F.pp_print_string fmt p) + all_params + in + let use_brackets = all_params <> [] in + (* Extract the name *) + let before, after = + match !backend with + | FStar | Lean -> + ( (fun () -> + F.pp_print_string fmt "eval_global"; + F.pp_print_space fmt ()), + fun () -> () ) + | Coq -> + ( (fun () -> ()), + fun () -> F.pp_print_string fmt "%global" ) + | HOL4 -> + ( (fun () -> + F.pp_print_string fmt "get_return_value"; + F.pp_print_space fmt ()), + fun () -> () ) + in + before (); + if use_brackets then F.pp_print_string fmt "("; + F.pp_print_string fmt body_name; + (* Extract the generic params *) + extract_params (); + if use_brackets then F.pp_print_string fmt ")"; + (* *) + after ())); + (* Add a break to insert lines between declarations *) + F.pp_print_break fmt 0 0) + | None -> () (** Similar to {!extract_trait_decl_register_names} *) let extract_trait_decl_register_parent_clause_names (ctx : extraction_ctx) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index f036cc37..b4c55d80 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3861,7 +3861,12 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = def let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = - List.map (translate_type_decl ctx) + List.filter_map + (fun a -> + try Some (translate_type_decl ctx a) + with CFailure (meta, _) -> + let () = save_error __FILE__ __LINE__ meta "Could not generate code, see previous error" in + None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl) 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. |