From 084480c807b58947b8487eb3a7c6a71bb388a832 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 3 Apr 2024 17:01:27 +0200 Subject: added Error and EError to expressions and propagated related changes --- compiler/Extract.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'compiler/Extract.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1f9c9117..ef5d5dce 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -297,6 +297,13 @@ let lets_require_wrap_in_do (meta : Meta.meta) - application argument: [f (exp)] - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _] *) + +let extract_errors (fmt : F.formatter) = + match !Config.backend with + | FStar | Coq -> F.pp_print_string fmt "admit" + | Lean -> F.pp_print_string fmt "sorry" + | HOL4 -> F.pp_print_string fmt "(* ERROR: could not generate the code *)" + let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = match e.e with @@ -323,6 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) | Loop _ -> (* The loop nodes should have been eliminated in {!PureMicroPasses} *) craise __FILE__ __LINE__ meta "Unreachable" + | EError (_, _) -> extract_errors fmt (* Extract an application *or* a top-level qualif (function extraction has * to handle top-level qualifiers, so it seemed more natural to merge the -- cgit v1.2.3 From a2a219145587deb0ade9fa7d60171765cd722162 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 3 Apr 2024 17:36:09 +0200 Subject: added extract_ty_errors and extract_texpression_errors to deal with the error case in their respective types --- compiler/Extract.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/Extract.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index ef5d5dce..af0bf98d 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -298,7 +298,7 @@ let lets_require_wrap_in_do (meta : Meta.meta) - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _] *) -let extract_errors (fmt : F.formatter) = +let extract_texpression_errors (fmt : F.formatter) = match !Config.backend with | FStar | Coq -> F.pp_print_string fmt "admit" | Lean -> F.pp_print_string fmt "sorry" @@ -330,7 +330,7 @@ let rec extract_texpression (meta : Meta.meta) (ctx : extraction_ctx) | Loop _ -> (* The loop nodes should have been eliminated in {!PureMicroPasses} *) craise __FILE__ __LINE__ meta "Unreachable" - | EError (_, _) -> extract_errors fmt + | EError (_, _) -> extract_texpression_errors fmt (* Extract an application *or* a top-level qualif (function extraction has * to handle top-level qualifiers, so it seemed more natural to merge the -- cgit v1.2.3 From 57b71cb1bfde1832097163c7169aaf97cf8c7583 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 4 Apr 2024 16:19:08 +0200 Subject: Update the extraction --- compiler/Extract.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/Extract.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 1f9c9117..27e9a62c 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2853,7 +2853,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "="; F.pp_print_space fmt (); let success = - ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | Coq -> @@ -2884,11 +2884,11 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt "=="; F.pp_print_space fmt (); let success = - ctx_get_variant def.meta (TAssumed TResult) result_return_id ctx + ctx_get_variant def.meta (TAssumed TResult) result_ok_id ctx in F.pp_print_string fmt (success ^ " ())") | HOL4 -> - F.pp_print_string fmt "val _ = assert_return ("; + F.pp_print_string fmt "val _ = assert_ok ("; F.pp_print_string fmt "“"; let fun_name = ctx_get_local_function def.meta def.def_id def.loop_id ctx -- cgit v1.2.3 From fc51bfd88076a66000dbfe76e832d3fdd72aee76 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 10:36:40 +0200 Subject: error catching should now be able to tell when code couldn't be generated --- compiler/Extract.ml | 181 ++++++++++++++++++++++++++-------------------------- 1 file changed, 92 insertions(+), 89 deletions(-) (limited to 'compiler/Extract.ml') 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) -- cgit v1.2.3 From 760e8374533bd7e13059e18c223428baab4535ea Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 12:29:33 +0200 Subject: resolved comments --- compiler/Extract.ml | 184 ++++++++++++++++++++++++++-------------------------- 1 file changed, 93 insertions(+), 91 deletions(-) (limited to 'compiler/Extract.ml') 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} *) -- cgit v1.2.3 From 581d5c0cb8e618382fa41e5a42175560283ff0a1 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 7 Apr 2024 14:27:14 +0200 Subject: Cleanup a bit and improve the error messages --- compiler/Extract.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler/Extract.ml') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index f7d08fdb..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 @@ -1884,6 +1884,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter) 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 = -- cgit v1.2.3