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/SymbolicToPure.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 0c30f44c..1701891f 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1963,6 +1963,9 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info +let translate_meta (meta : Meta.meta option) (msg : string) : texpression = + { e = EError (meta, msg); ty = Error } + let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = match e with | S.Return (ectx, opt_v) -> @@ -1989,6 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx + | Error (meta, msg) -> translate_meta meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because -- cgit v1.2.3 From 78cc58e3076ffd61add6d78b64371b6eb36d6ab2 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Wed, 3 Apr 2024 17:52:10 +0200 Subject: resolved requested changes --- compiler/SymbolicToPure.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 1701891f..53ab1c08 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1963,7 +1963,7 @@ let eval_ctx_to_symbolic_assignments_info (ctx : bs_ctx) (* Return the computed information *) !info -let translate_meta (meta : Meta.meta option) (msg : string) : texpression = +let translate_error (meta : Meta.meta option) (msg : string) : texpression = { e = EError (meta, msg); ty = Error } let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = @@ -1992,7 +1992,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = *) translate_forward_end ectx loop_input_values e back_e ctx | Loop loop -> translate_loop loop ctx - | Error (meta, msg) -> translate_meta meta msg + | Error (meta, msg) -> translate_error meta msg and translate_panic (ctx : bs_ctx) : texpression = (* Here we use the function return type - note that it is ok because -- 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/SymbolicToPure.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'compiler/SymbolicToPure.ml') 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) -- 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/SymbolicToPure.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'compiler/SymbolicToPure.ml') 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) -- cgit v1.2.3 From 3a470ec6661a494631a12594989126804aeb044d Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 5 Apr 2024 14:44:17 +0200 Subject: Resolved comments and added the name of the not translated element --- compiler/SymbolicToPure.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index eac4adb9..607da445 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3865,9 +3865,12 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = (fun a -> try Some (translate_type_decl ctx a) with CFailure (meta, _) -> + let env = PrintPure.decls_ctx_to_fmt_env ctx in + let name = PrintPure.name_to_string env a.name in let () = save_error __FILE__ __LINE__ meta - "Could not generate code, see previous error" + ("Could not translate type decl '" ^ name + ^ "' because of previous error") in None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) -- 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/SymbolicToPure.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'compiler/SymbolicToPure.ml') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 607da445..93f9ef75 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -3867,11 +3867,9 @@ let translate_type_decls (ctx : Contexts.decls_ctx) : type_decl list = with CFailure (meta, _) -> let env = PrintPure.decls_ctx_to_fmt_env ctx in let name = PrintPure.name_to_string env a.name in - let () = - save_error __FILE__ __LINE__ meta - ("Could not translate type decl '" ^ name - ^ "' because of previous error") - in + save_error __FILE__ __LINE__ meta + ("Could not translate type decl '" ^ name + ^ "' because of previous error"); None) (TypeDeclId.Map.values ctx.type_ctx.type_decls) -- cgit v1.2.3