diff options
| author | Son Ho | 2022-01-26 16:29:30 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-26 16:29:30 +0100 |
| commit | 652e500bc2ad13f70db242e0c89234091769fe18 (patch) | |
| tree | 05e097d81b167f9f44b3341f149486f69cd0e099 /src | |
| parent | 3cf1d87a9bbfb7a1e29d4e3f919d3cd4ec3999c2 (diff) | |
Cleanup a bit
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 2 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 13 |
2 files changed, 7 insertions, 8 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 463ad447..4405c409 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -70,7 +70,7 @@ module Test = struct let type_params = List.map (fun tv -> T.TypeVar tv.T.index) sg.type_params in - let inst_sg = instantiate_fun_sig type_params sg ctx in + let inst_sg = instantiate_fun_sig type_params sg in (* Create fresh symbolic values for the inputs *) let input_svs = List.map diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index e2f6cf4d..78770adb 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -15,7 +15,6 @@ open InterpreterProjectors open InterpreterExpansion open InterpreterPaths open InterpreterExpressions -open Assumed (** The local logger *) let log = L.statements_log @@ -556,8 +555,8 @@ let eval_non_local_function_call_concrete (config : C.config) Note: there are no region parameters, because they should be erased. *) -let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) - (ctx : C.eval_ctx) : A.inst_fun_sig = +let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) : + A.inst_fun_sig = (* Generate fresh abstraction ids and create a substitution from region * group ids to abstraction ids *) let rg_abs_ids_bindings = @@ -923,7 +922,7 @@ and eval_local_function_call_symbolic (config : C.config) (fid : A.FunDefId.id) let sg = def.A.signature in (* Instantiate the signature and introduce fresh abstraction and region ids * while doing so *) - let inst_sg = instantiate_fun_sig type_params sg ctx in + let inst_sg = instantiate_fun_sig type_params sg in (* Sanity check *) assert (List.length args = def.A.arg_count); (* Evaluate the function call *) @@ -1050,11 +1049,11 @@ and eval_non_local_function_call_symbolic (config : C.config) * instantiated signatures, and delegate the work to an auxiliary function *) let inst_sig = match fid with - | A.BoxNew -> instantiate_fun_sig type_params Assumed.box_new_sig ctx + | A.BoxNew -> instantiate_fun_sig type_params Assumed.box_new_sig | A.BoxDeref -> - instantiate_fun_sig type_params Assumed.box_deref_shared_sig ctx + instantiate_fun_sig type_params Assumed.box_deref_shared_sig | A.BoxDerefMut -> - instantiate_fun_sig type_params Assumed.box_deref_mut_sig ctx + instantiate_fun_sig type_params Assumed.box_deref_mut_sig | A.BoxFree -> failwith "Unreachable" (* should have been treated above *) in |