From 00104884e101d3125e62dde9757b9c1cacb3feec Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 3 Mar 2022 17:36:33 +0100 Subject: Make good progress on adding support for external and opaque declarations --- src/LlbcOfJson.ml | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'src/LlbcOfJson.ml') diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml index e293b030..6e0adfb6 100644 --- a/src/LlbcOfJson.ml +++ b/src/LlbcOfJson.ml @@ -607,6 +607,16 @@ and switch_targets_of_json (js : json) : (A.switch_targets, string) result = Ok (A.SwitchInt (int_ty, tgts, otherwise)) | _ -> Error "") +let fun_body_of_json (js : json) : (A.fun_body, string) result = + combine_error_msgs js "fun_body_of_json" + (match js with + | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] -> + let* arg_count = int_of_json arg_count in + let* locals = list_of_json var_of_json locals in + let* body = statement_of_json body in + Ok { A.arg_count; locals; body } + | _ -> Error "") + let fun_decl_of_json (js : json) : (A.fun_decl, string) result = combine_error_msgs js "fun_decl_of_json" (match js with @@ -615,17 +625,13 @@ let fun_decl_of_json (js : json) : (A.fun_decl, string) result = ("def_id", def_id); ("name", name); ("signature", signature); - ("arg_count", arg_count); - ("locals", locals); ("body", body); ] -> let* def_id = A.FunDeclId.id_of_json def_id in let* name = fun_name_of_json name in let* signature = fun_sig_of_json signature in - let* arg_count = int_of_json arg_count in - let* locals = list_of_json var_of_json locals in - let* body = statement_of_json body in - Ok { A.def_id; name; signature; arg_count; locals; body } + let* body = option_of_json fun_body_of_json body in + Ok { A.def_id; name; signature; body } | _ -> Error "") let g_declaration_group_of_json (id_of_json : json -> ('id, string) result) -- cgit v1.2.3