diff options
author | Son Ho | 2021-11-25 17:12:56 +0100 |
---|---|---|
committer | Son Ho | 2021-11-25 17:12:56 +0100 |
commit | d546fcc5a1a1e964275d90a3822930b8f04f17ac (patch) | |
tree | c5945abd4597e5140e6cc4f0fe6b045185c6d0d4 /src/Interpreter.ml | |
parent | a9995fe949d31e0f53b1e3e26908de8f98972ca5 (diff) |
Start working on function calls
Diffstat (limited to '')
-rw-r--r-- | src/Interpreter.ml | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 74cbe70d..77af0b54 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -1933,4 +1933,27 @@ let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement) and eval_function_call (config : C.config) (ctx : C.eval_ctx) (call : A.call) : (C.eval_ctx * statement_eval_res) eval_result = + (* There are two cases * + - this is a local function, in which case we execute its body + - this is a non-local function, in which case there is a special treatment + *) + match call.func with + | A.Local fid -> + eval_local_function_call fid call.region_params call.type_params call.args + call.dest + | A.Assumed fid -> + eval_assumed_function_call fid call.region_params call.type_params + call.args call.dest + +and eval_local_function_call (fid : A.FunDefId.id) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : + (C.eval_ctx * statement_eval_res) eval_result = + (* Retrieve the (correctly instantiated) body *) + raise Unimplemented + +and eval_assumed_function_call (fid : A.assumed_fun_id) + (region_params : T.erased_region list) (type_params : T.ety list) + (args : E.operand list) (dest : E.place) : + (C.eval_ctx * statement_eval_res) eval_result = raise Unimplemented |