diff options
author | Son Ho | 2021-11-26 20:04:50 +0100 |
---|---|---|
committer | Son Ho | 2021-11-26 20:04:50 +0100 |
commit | 27f4f3dd837742b4d9b70347259d711766d019fd (patch) | |
tree | 8b55977d5175b1edc907b5f45d0386b59484b12f | |
parent | 46447ca337175ceafa26ce46b2d338ba83a78fbd (diff) |
Implement test_all_unit_functions
-rw-r--r-- | src/Interpreter.ml | 31 |
1 files changed, 26 insertions, 5 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 66eb7d87..abf5503b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -2311,11 +2311,11 @@ and eval_expression (config : C.config) (ctx : C.eval_ctx) (e : A.expression) : (** Test a unit function (taking no arguments) by evaluating it in an empty environment *) -let test_unit_function (type_decls : T.type_def T.TypeDefId.vector) - (fun_decls : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) : +let test_unit_function (type_defs : T.type_def T.TypeDefId.vector) + (fun_defs : A.fun_def A.FunDefId.vector) (fid : A.FunDefId.id) : unit eval_result = (* Retrieve the function declaration *) - let fdef = A.FunDefId.nth fun_decls fid in + let fdef = A.FunDefId.nth fun_defs fid in (* Sanity check - *) assert (T.RegionVarId.length fdef.A.signature.region_params = 0); @@ -2325,8 +2325,8 @@ let test_unit_function (type_decls : T.type_def T.TypeDefId.vector) (* Create the evaluation context *) let ctx = { - C.type_context = type_decls; - C.fun_context = fun_decls; + C.type_context = type_defs; + C.fun_context = fun_defs; C.type_vars = T.TypeVarId.empty_vector; C.env = []; C.symbolic_counter = V.SymbolicValueId.generator_zero; @@ -2339,3 +2339,24 @@ let test_unit_function (type_decls : T.type_def T.TypeDefId.vector) match eval_function_body config ctx fdef.A.body with | Error err -> Error err | Ok _ -> Ok () + +(** Small helper: return true if the function is a unit function (no parameters, + no arguments) - TODO: move *) +let fun_def_is_unit (def : A.fun_def) : bool = + def.A.arg_count = 0 + && V.VarId.length def.A.locals = 0 + && T.RegionVarId.length def.A.signature.region_params = 0 + && T.TypeVarId.length def.A.signature.type_params = 0 + && V.VarId.length def.A.signature.inputs = 0 + +(** Test all the unit functions in a list of function definitions *) +let test_all_unit_functions (type_defs : T.type_def T.TypeDefId.vector) + (fun_defs : A.fun_def A.FunDefId.vector) : bool = + let test_fun (def : A.fun_def) : bool = + if fun_def_is_unit def then + match test_unit_function type_defs fun_defs def.A.def_id with + | Error _ -> false + | Ok _ -> true + else true + in + A.FunDefId.for_all test_fun fun_defs |