diff options
| author | Son Ho | 2022-01-06 18:25:09 +0100 |
|---|---|---|
| committer | Son Ho | 2022-01-06 18:25:09 +0100 |
| commit | 1d0254f555e26968badf05d605cd630c018dcaa8 (patch) | |
| tree | d11e8d89ec4f398cbbe9f45703cab86e25cb6ff5 /src/InterpreterProjectors.ml | |
| parent | f3982cbe9782405b50b04c948ba7cb0bd89ef85f (diff) | |
Cleanup
Diffstat (limited to 'src/InterpreterProjectors.ml')
| -rw-r--r-- | src/InterpreterProjectors.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index 3fa824ab..036082eb 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -5,8 +5,6 @@ module C = Contexts module Subst = Substitute module L = Logging open TypesUtils -open ValuesUtils -open Utils open InterpreterUtils open InterpreterBorrowsCore @@ -471,8 +469,7 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list) - a function to apply the reborrows in a context Those functions are of course stateful. *) -let prepare_reborrows (config : C.config) (allow_reborrows : bool) - (ctx : C.eval_ctx) : +let prepare_reborrows (config : C.config) (allow_reborrows : bool) : (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) = let reborrows : (V.BorrowId.id * V.BorrowId.id) list ref = ref [] in (* The function to generate and register fresh reborrows *) @@ -502,7 +499,7 @@ let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) let allow_reborrows = true in (* Prepare the reborrows *) let fresh_reborrow, apply_registered_reborrows = - prepare_reborrows config allow_reborrows ctx + prepare_reborrows config allow_reborrows in (* Apply the projector *) let av = |