summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEscherichia2024-04-05 12:29:33 +0200
committerEscherichia2024-04-05 12:29:33 +0200
commit760e8374533bd7e13059e18c223428baab4535ea (patch)
tree6434cf31965e9dee501b54eb49fb1afd04ed9500
parentfc51bfd88076a66000dbfe76e832d3fdd72aee76 (diff)
resolved comments
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml184
-rw-r--r--compiler/SymbolicToPure.ml5
-rw-r--r--compiler/Translate.ml23
3 files changed, 113 insertions, 99 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1fc8a97f..f7d08fdb 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1879,102 +1879,104 @@ 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)
- (global : global_decl option) (body : fun_decl) (interface : bool) : unit =
+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;
sanity_check __FILE__ __LINE__ (body.signature.inputs = []) meta;
- match global with
- | Some global -> (
- (* Add a break then the name of the corresponding LLBC declaration *)
+ (* 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));
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 ();
+ (* 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 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)
+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} *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index b4c55d80..eac4adb9 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3865,7 +3865,10 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list =
(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
+ let () =
+ save_error __FILE__ __LINE__ meta
+ "Could not generate code, see previous error"
+ in
None)
(TypeDeclId.Map.values ctx.type_ctx.type_decls)
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 28e5531d..c23b2a47 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_hook (trans_ctx : trans_ctx)
+let translate_function_to_pure_aux (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 =
@@ -201,9 +201,12 @@ let translate_function_to_pure (trans_ctx : trans_ctx)
pure_fun_translation_no_loops option =
try
Some
- (translate_function_to_pure_hook trans_ctx pure_type_decls fun_dsigs fdef)
+ (translate_function_to_pure_aux 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
+ let () =
+ save_error __FILE__ __LINE__ meta
+ "Could not translate function because of previous error"
+ in
None
(* TODO: factor out the return type *)
@@ -240,7 +243,8 @@ let translate_crate_to_pure (crate : crate) :
trans_ctx fdef )
with CFailure (meta, _) ->
let () =
- save_error __FILE__ __LINE__ meta "Could not generate code, see previous error"
+ save_error __FILE__ __LINE__ meta
+ "Could not translate function because of previous error"
in
None)
(FunDeclId.Map.values crate.fun_decls))
@@ -260,7 +264,8 @@ let translate_crate_to_pure (crate : crate) :
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"
+ save_error __FILE__ __LINE__ meta
+ "Could not translate trait decl because of previous error"
in
None)
(TraitDeclId.Map.values trans_ctx.trait_decls_ctx.trait_decls)
@@ -273,7 +278,8 @@ let translate_crate_to_pure (crate : crate) :
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"
+ save_error __FILE__ __LINE__ meta
+ "Could not translate trait impl because of previous error"
in
None)
(TraitImplId.Map.values trans_ctx.trait_impls_ctx.trait_impls)
@@ -504,7 +510,10 @@ let export_global (fmt : Format.formatter) (config : gen_config) (ctx : gen_ctx)
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
+ let () =
+ save_error __FILE__ __LINE__ meta
+ "Could not translate global because of previous error"
+ in
None
in
Extract.extract_global_decl ctx fmt global body config.interface