From 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 18:04:03 +0100
Subject: Implement the generation of stateful backward functions (controlled
 by an option)

---
 compiler/ExtractToFStar.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'compiler/ExtractToFStar.ml')

diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index 2a7d6a6c..a995d4a6 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -1451,17 +1451,19 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
        * function (the additional input values "given back" to the
        * backward functions have no influence on termination: we thus
        * share the decrease clauses between the forward and the backward
-       * functions).
+       * functions - we also ignore the additional state received by the
+       * backward function, if there is one).
        *)
       let inputs_lvs =
         let all_inputs = (Option.get def.body).inputs_lvs in
         (* We have to count:
          * - the forward inputs
-         * - the state
+         * - the state (if there is one)
          *)
         let num_fwd_inputs = def.signature.info.num_fwd_inputs in
         let num_fwd_inputs =
-          if def.signature.info.effect_info.input_state then 1 + num_fwd_inputs
+          if def.signature.info.effect_info.stateful_group then
+            1 + num_fwd_inputs
           else num_fwd_inputs
         in
         Collections.List.prefix num_fwd_inputs all_inputs
-- 
cgit v1.2.3