diff options
| author | Son Ho | 2022-05-04 15:39:05 +0200 |
|---|---|---|
| committer | Son Ho | 2022-05-04 15:39:05 +0200 |
| commit | 15d90db02086f8ecae9a93ebf39c3c0ae8caa50f (patch) | |
| tree | 3eb303b96c9233fd7745f06a0d4e2d211373ca03 /src/Translate.ml | |
| parent | fb6fdfd0c57de1ce16fb6bc373d5593c9446b0bb (diff) | |
Fix some issues when using states
Diffstat (limited to '')
| -rw-r--r-- | src/Translate.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Translate.ml b/src/Translate.ml index d69f1379..92261dba 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -232,8 +232,10 @@ let translate_function_to_pure (config : C.partial_config) let backward_sg = RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs in + (* We need to ignore the forward inputs, and the state input (if there is) *) let _, backward_inputs = - Collections.List.split_at backward_sg.sg.inputs num_forward_inputs + Collections.List.split_at backward_sg.sg.inputs + (num_forward_inputs + if use_state_monad then 1 else 0) in (* As we forbid nested borrows, the additional inputs for the backward * functions come from the borrows in the return value of the rust function: |