From 496a3849d1d6ba880bbd1e86c8ef5e2257bb702a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 10:55:57 +0100
Subject: Add the num_fwd_inputs_no_fuel_no_state field in Pure.fun_sig

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

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 0ae83007..d7aea0f7 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -860,8 +860,8 @@ type fun_effect_info = {
           the set [{ forward function } U { backward functions }].
 
           We need this because of the option {!val:Config.backward_no_state_update}:
-          if it is [true], then in case of a backward function {!stateful} is [false],
-          but we might need to know whether the corresponding forward function
+          if it is [true], then in case of a backward function {!stateful} might be
+          [false], but we might need to know whether the corresponding forward function
           is stateful or not.
        *)
   stateful : bool;  (** [true] if the function is stateful (updates a state) *)
@@ -876,7 +876,9 @@ type fun_effect_info = {
 (** Meta information about a function signature *)
 type fun_sig_info = {
   has_fuel : bool;
-  (* TODO: add [num_fwd_inputs_no_fuel_no_state] *)
+  num_fwd_inputs_no_fuel_no_state : int;
+      (** The number of input types for forward computation, ignoring the fuel (if used)
+          and ignoring the state (if used) *)
   num_fwd_inputs_with_fuel_no_state : int;
       (** The number of input types for forward computation, with the fuel (if used)
           and ignoring the state (if used) *)
-- 
cgit v1.2.3


From 0c814c97dd8e5167f24b0dbb14186d674e4d097b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 13 Dec 2023 11:44:58 +0100
Subject: Update Pure.fun_sig_info

---
 compiler/Pure.ml | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index d7aea0f7..80d8782b 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -873,23 +873,25 @@ type fun_effect_info = {
 }
 [@@deriving show]
 
-(** Meta information about a function signature *)
-type fun_sig_info = {
+type inputs_info = {
   has_fuel : bool;
-  num_fwd_inputs_no_fuel_no_state : int;
-      (** The number of input types for forward computation, ignoring the fuel (if used)
+  num_inputs_no_fuel_no_state : int;
+      (** The number of input types ignoring the fuel (if used)
           and ignoring the state (if used) *)
-  num_fwd_inputs_with_fuel_no_state : int;
-      (** The number of input types for forward computation, with the fuel (if used)
+  num_inputs_with_fuel_no_state : int;
+      (** The number of input types, with the fuel (if used)
           and ignoring the state (if used) *)
-  num_fwd_inputs_with_fuel_with_state : int;
-      (** The number of input types for forward computation, with fuel and state (if used) *)
-  num_back_inputs_no_state : int option;
-      (** The number of additional inputs for the backward computation (if pertinent),
-          ignoring the state (if there is one) *)
-  num_back_inputs_with_state : int option;
-      (** The number of additional inputs for the backward computation (if pertinent),
-          with the state (if there is one) *)
+  num_inputs_with_fuel_with_state : int;
+      (** The number of input types, with fuel and state (if used) *)
+}
+[@@deriving show]
+
+(** Meta information about a function signature *)
+type fun_sig_info = {
+  fwd_info : inputs_info;
+      (** Information about the inputs of the forward function *)
+  back_info : inputs_info option;
+      (** Information about the inputs of the backward function, if pertinent *)
   effect_info : fun_effect_info;
 }
 [@@deriving show]
-- 
cgit v1.2.3


From f69ac6a4a244c99a41a90ed57f74ea83b3835882 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 14 Dec 2023 17:11:01 +0100
Subject: Start updating Pure.fun_sig_info to handle merged forward and
 backward functions

---
 compiler/Pure.ml | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 80d8782b..bb522623 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -561,7 +561,7 @@ type fun_id_or_trait_method_ref =
 
 (** A function id for a non-assumed function *)
 type regular_fun_id =
-  fun_id_or_trait_method_ref * LoopId.id option * T.RegionGroupId.id option
+  fun_id_or_trait_method_ref * LoopId.id option * RegionGroupId.id option
 [@@deriving show, ord]
 
 (** A function identifier *)
@@ -886,12 +886,28 @@ type inputs_info = {
 }
 [@@deriving show]
 
+type 'a back_info =
+  | SingleBack of 'a option
+      (** Information about a single backward function, if pertinent.
+
+          We use this variant if we split the forward and the backward functions.
+       *)
+  | AllBacks of 'a RegionGroupId.Map.t
+      (** Information about the various backward functions.
+
+          We use this if we *do not* split the forward and the backward functions.
+          All the information is then carried by the forward function.
+       *)
+[@@deriving show]
+
+type back_inputs_info = inputs_info back_info [@@deriving show]
+
 (** Meta information about a function signature *)
 type fun_sig_info = {
   fwd_info : inputs_info;
       (** Information about the inputs of the forward function *)
-  back_info : inputs_info option;
-      (** Information about the inputs of the backward function, if pertinent *)
+  back_info : back_inputs_info;
+      (** Information about the inputs of the backward functions. *)
   effect_info : fun_effect_info;
 }
 [@@deriving show]
@@ -1024,7 +1040,7 @@ type fun_decl = {
        *)
   loop_id : LoopId.id option;
       (** [Some] if this definition was generated for a loop *)
-  back_id : T.RegionGroupId.id option;
+  back_id : RegionGroupId.id option;
   llbc_name : llbc_name;  (** The original LLBC name. *)
   name : string;
       (** We use the name only for printing purposes (for debugging):
-- 
cgit v1.2.3


From cf984f958da94154d0550060eb290a276ab52f23 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 10:17:06 +0100
Subject: Make minor modifications

---
 compiler/Pure.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index c3716001..34f3ef72 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -886,13 +886,13 @@ type inputs_info = {
 }
 [@@deriving show]
 
-type 'a back_info =
-  | SingleBack of 'a option
+type ('a, 'b) back_info =
+  | SingleBack of 'a
       (** Information about a single backward function, if pertinent.
 
           We use this variant if we split the forward and the backward functions.
        *)
-  | AllBacks of 'a RegionGroupId.Map.t
+  | AllBacks of 'b RegionGroupId.Map.t
       (** Information about the various backward functions.
 
           We use this if we *do not* split the forward and the backward functions.
@@ -900,7 +900,8 @@ type 'a back_info =
        *)
 [@@deriving show]
 
-type back_inputs_info = inputs_info back_info [@@deriving show]
+type back_inputs_info = (inputs_info option, inputs_info) back_info
+[@@deriving show]
 
 (** Meta information about a function signature *)
 type fun_sig_info = {
-- 
cgit v1.2.3


From 83c5be42e1750d329ad31bc9151d7b0446af5a0f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 12:14:01 +0100
Subject: Make progress on generalizing the signature information

---
 compiler/Pure.ml | 130 ++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 90 insertions(+), 40 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 34f3ef72..fb0509f4 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -907,12 +907,88 @@ type back_inputs_info = (inputs_info option, inputs_info) back_info
 type fun_sig_info = {
   fwd_info : inputs_info;
       (** Information about the inputs of the forward function *)
-  back_info : back_inputs_info;
-      (** Information about the inputs of the backward functions. *)
   effect_info : fun_effect_info;
 }
 [@@deriving show]
 
+type back_sg_info = {
+  inputs : ty list;  (** The additional inputs of the backward function *)
+  input_names : string option list;
+      (** The optional names for the additional inputs *)
+  outputs : ty list;
+      (** The "decomposed" list of outputs.
+
+          The list contains all the types of
+          all the given back values (there is at most one type per forward
+          input argument).
+
+          Ex.:
+          {[
+            fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
+          ]}
+          Decomposed outputs:
+          - forward function:  [[T]]
+          - backward function: [[T; T]] (for "x" and "y")
+
+          Non-decomposed ouputs (if the function can fail, but is not stateful):
+          - [result T]
+          - [[result (T * T)]]
+       *)
+  output_names : string option list;
+      (** The optional names for the backward outputs.
+          We derive those from the names of the inputs of the original LLBC
+          function. *)
+  effect_info : fun_effect_info;
+}
+[@@deriving show]
+
+(** A *decomposed* function signature. *)
+type decomposed_fun_sig = {
+  generics : generic_params;
+      (** TODO: we should analyse the signature to make the type parameters implicit whenever possible *)
+  llbc_generics : Types.generic_params;
+      (** We use the LLBC generics to generate "pretty" names, for instance
+          for the variables we introduce for the trait clauses: we derive
+          those names from the types, and when doing so it is more meaningful
+          to derive them from the original LLBC types from before the
+          simplification of types like boxes and references. *)
+  preds : predicates;
+  fwd_inputs : ty list;
+      (** The types of the inputs of the forward function.
+
+          Note that those input types take include the [fuel] parameter,
+          if the function uses fuel for termination, and the [state] parameter,
+          if the function is stateful.
+
+          For instance, if we have the following Rust function:
+          {[
+            fn f(x : int);
+          ]}
+
+          If we translate it to a stateful function which uses fuel we get:
+          {[
+            val f : nat -> int -> state -> result (state * unit);
+          ]}
+
+          In particular, the list of input types is: [[nat; int; state]].
+       *)
+  fwd_output : ty;
+      (** The "pure" output type of the forward function.
+
+          Note that this type doesn't contain the "effect" of the function (i.e.,
+          we haven't added the [state] if it is a stateful function and haven't
+          wrapped the type in a [result]). Also, this output type is only about
+          the forward function (it doesn't contain the type of the closures we
+          return for the backward functions, in case we merge the forward and
+          backward functions).
+       *)
+  back_sg : back_sg_info RegionGroupId.Map.t;
+      (** Information about the backward functions *)
+  fwd_info : fun_sig_info;
+      (** Additional information about the forward function *)
+}
+[@@deriving show]
+
 (** A function signature.
 
     We have the following cases:
@@ -927,15 +1003,15 @@ type fun_sig_info = {
       [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
        result (state & (back_out0 & ... & back_outp))] (* state-error *)
 
-       Note that a stateful backward function may take two states as inputs: the
-       state received by the associated forward function, and the state at which
-       the backward is called. This leads to code of the following shape:
+      Note that a stateful backward function may take two states as inputs: the
+      state received by the associated forward function, and the state at which
+      the backward is called. This leads to code of the following shape:
 
-       {[
-         (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
-         ... // the state may be updated
-         (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
-       ]}
+      {[
+        (st1, y)  <-- f_fwd x st0; // st0 is the state upon calling f_fwd
+        ... // the state may be updated
+        (st3, x') <-- f_back x st0 y' st2; // st2 is the state upon calling f_back
+      ]}
 
     The function's type should be given by [mk_arrows sig.inputs sig.output].
     We provide additional meta-information with {!fun_sig.info}:
@@ -983,40 +1059,14 @@ type fun_sig = {
           be a tuple with a [state] if the function is stateful, and will be wrapped
           in a [result] if the function can fail.
        *)
-  doutputs : ty list;
-      (** The "decomposed" list of outputs.
-
-          In case of a forward function, the list has length = 1, for the
-          type of the returned value.
-
-          In case of backward function, the list contains all the types of
-          all the given back values (there is at most one type per forward
-          input argument).
-
-          Ex.:
-          {[
-            fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
-          ]}
-          Decomposed outputs:
-          - forward function:  [[T]]
-          - backward function: [[T; T]] (for "x" and "y")
-
-          Non-decomposed ouputs (if the function can fail, but is not stateful):
-          - [result T]
-          - [[result (T * T)]]
-       *)
-  info : fun_sig_info;  (** Additional information *)
+  fwd_info : fun_sig_info;
+      (** Additional information about the forward function. *)
+  back_effect_info : fun_effect_info RegionGroupId.Map.t;
 }
 [@@deriving show]
 
 (** An instantiated function signature. See {!fun_sig} *)
-type inst_fun_sig = {
-  inputs : ty list;
-  output : ty;
-  doutputs : ty list;
-  info : fun_sig_info;
-}
-[@@deriving show]
+type inst_fun_sig = { inputs : ty list; output : ty } [@@deriving show]
 
 type fun_body = {
   inputs : var list;
-- 
cgit v1.2.3


From ea583d9f0f5e4a1a687b70f0e04e875969462157 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 17:20:30 +0100
Subject: Make good progress on updating SymbolicToPure

---
 compiler/Pure.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index fb0509f4..eb6b00c8 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -728,6 +728,7 @@ type expression =
   | Switch of texpression * switch_body
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
+  | Lambda of typed_pattern * texpression  (** [λ x => e] *)
   | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
 
 and switch_body = If of texpression * texpression | Match of match_branch list
@@ -912,9 +913,9 @@ type fun_sig_info = {
 [@@deriving show]
 
 type back_sg_info = {
-  inputs : ty list;  (** The additional inputs of the backward function *)
-  input_names : string option list;
-      (** The optional names for the additional inputs *)
+  inputs : (string option * ty) list;
+      (** The additional inputs of the backward function *)
+  inputs_no_state : (string option * ty) list;
   outputs : ty list;
       (** The "decomposed" list of outputs.
 
-- 
cgit v1.2.3


From 955fdab55304979ba2d61432ea654241f20abaa4 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 15 Dec 2023 18:14:12 +0100
Subject: Make progress on propagating the changes

---
 compiler/Pure.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index eb6b00c8..ddacf0c4 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -684,7 +684,7 @@ type expression =
           field accesses with calls to projectors over fields (when there
           are clashes of field names, some provers like F* get pretty bad...)
        *)
-  | Abs of typed_pattern * texpression  (** Lambda abstraction: [fun x -> e] *)
+  | Lambda of typed_pattern * texpression  (** Lambda abstraction: [λ x => e] *)
   | Qualif of qualif  (** A top-level qualifier *)
   | Let of bool * typed_pattern * texpression * texpression
       (** Let binding.
@@ -728,7 +728,6 @@ type expression =
   | Switch of texpression * switch_body
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
-  | Lambda of typed_pattern * texpression  (** [λ x => e] *)
   | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
 
 and switch_body = If of texpression * texpression | Match of match_branch list
-- 
cgit v1.2.3


From 2f681446b11739e650b1d6050b717da872be9022 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 19:23:29 +0100
Subject: Simplify the type of the merged fwd/back functions

---
 compiler/Pure.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ddacf0c4..05cdbd70 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -908,6 +908,11 @@ type fun_sig_info = {
   fwd_info : inputs_info;
       (** Information about the inputs of the forward function *)
   effect_info : fun_effect_info;
+  ignore_output : bool;
+      (** In case we merge the forward/backward functions: should we ignore
+          the output (happens for forward functions if the output type is
+          [unit] and there are non-filtered backward functions)?
+       *)
 }
 [@@deriving show]
 
@@ -939,6 +944,7 @@ type back_sg_info = {
           We derive those from the names of the inputs of the original LLBC
           function. *)
   effect_info : fun_effect_info;
+  filter : bool;  (** Should we filter this backward function? *)
 }
 [@@deriving show]
 
-- 
cgit v1.2.3


From 266db04e97778911c93cfd1aac251de04bb25f53 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Dec 2023 22:17:11 +0100
Subject: Fix several issues

---
 compiler/Pure.ml | 17 -----------------
 1 file changed, 17 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 05cdbd70..71531688 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -886,23 +886,6 @@ type inputs_info = {
 }
 [@@deriving show]
 
-type ('a, 'b) back_info =
-  | SingleBack of 'a
-      (** Information about a single backward function, if pertinent.
-
-          We use this variant if we split the forward and the backward functions.
-       *)
-  | AllBacks of 'b RegionGroupId.Map.t
-      (** Information about the various backward functions.
-
-          We use this if we *do not* split the forward and the backward functions.
-          All the information is then carried by the forward function.
-       *)
-[@@deriving show]
-
-type back_inputs_info = (inputs_info option, inputs_info) back_info
-[@@deriving show]
-
 (** Meta information about a function signature *)
 type fun_sig_info = {
   fwd_info : inputs_info;
-- 
cgit v1.2.3


From 70d506d148e5ae1a3e4115034161f449aff666ed Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 21:03:17 +0100
Subject: Fix the output type of the loops backward functions

---
 compiler/Pure.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/Pure.ml')

diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 71531688..a879ba37 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -754,9 +754,7 @@ and loop = {
   inputs : var list;
   inputs_lvs : typed_pattern list;
       (** The inputs seen as patterns. See {!fun_body}. *)
-  back_output_tys : ty list option;
-      (** The types of the given back values, if we ar esynthesizing a backward
-          function *)
+  output_ty : ty;  (** The output type of the loop *)
   loop_body : texpression;
 }
 
-- 
cgit v1.2.3