Merge pull request #83 from AeneasVerif/son/backs

Remove the option to split the forward/backward functions

1 files changed, 0 insertions, 107 deletions

diff --git a/compiler/Config.ml b/compiler/Config.ml
index 3b0070c0..af0e62d1 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -92,69 +92,6 @@ let loop_fixed_point_max_num_iters = 2
 
 (** {1 Translation} *)
 
-(** If true, do not define separate forward/backward functions, but make the
-    forward functions return the backward function.
-
-    Example:
-    {[
-      (* Rust *)
-      pub fn list_nth<'a, T>(l: &'a mut List<T>, i: u32) -> &'a mut T {
-          match l {
-              List::Nil => {
-                  panic!()
-              }
-              List::Cons(x, tl) => {
-                  if i == 0 {
-                      x
-                  } else {
-                      list_nth(tl, i - 1)
-                  }
-              }
-          }
-      }
-
-      (* Translation, if return_back_funs = false *)
-      def list_nth (T : Type) (l : List T) (i : U32) : Result T :=
-        match l with
-        | List.Cons x tl =>
-          if i = 0#u32
-          then Result.ret x
-          else do
-                 let i0 ← i - 1#u32
-                 list_nth T tl i0
-        | List.Nil => Result.fail .panic
-
-      def list_nth_back
-        (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
-        match l with
-        | List.Cons x tl =>
-          if i = 0#u32
-          then Result.ret (List.Cons ret tl)
-          else
-            do
-              let i0 ← i - 1#u32
-              let tl0 ← list_nth_back T tl i0 ret
-              Result.ret (List.Cons x tl0)
-        | List.Nil => Result.fail .panic
-
-      (* Translation, if return_back_funs = true *)
-      def list_nth (T: Type) (ls : List T) (i : U32) :
-        Result (T × (T → Result (List T))) :=
-        match ls with
-        | List.Cons x tl =>
-          if i = 0#u32
-          then Result.ret (x, (λ ret => return (ret :: ls)))
-          else do
-            let i0 ← i - 1#u32
-            let (x, back) ← list_nth ls i0
-            Return.ret (x,
-              (λ ret => do
-               let ls ← back ret
-               return (x :: ls)))
-    ]}
- *)
-let return_back_funs = ref true
-
 (** Forbids using field projectors for structures.
 
     If we don't use field projectors, whenever we symbolically expand a structure
@@ -326,50 +263,6 @@ let decompose_nested_let_patterns = ref false
  *)
 let unfold_monadic_let_bindings = ref false
 
-(** Controls whether we try to filter the calls to monadic functions
-    (which can fail) when their outputs are not used.
-
-    The useless calls are calls to backward functions which have no outputs.
-    This case happens if the original Rust function only takes *shared* borrows
-    as inputs, and is thus pretty common.
-
-    We are allowed to do this only because in this specific case,
-    the backward function fails *exactly* when the forward function fails
-    (they actually do exactly the same thing, the only difference being
-    that the forward function can potentially return a value), and upon
-    reaching the place where we should introduce a call to the backward
-    function, we know we have introduced a call to the forward function.
-
-    Also note that in general, backward functions "do more things" than
-    forward functions, and have more opportunities to fail (even though
-    in the generated code, calls to the backward functions should fail
-    exactly when the corresponding, previous call to the forward functions
-    failed).
-
-    This optimization is done in {!SymbolicToPure}.  We might want to move it to
-    the micro-passes subsequent to the translation from symbolic to pure, but it
-    is really super easy to do it when going from symbolic to pure. Note that
-    we later filter the useless *forward* calls in the micro-passes, where it is
-    more natural to do.
-
-    See the comments for {!PureMicroPasses.expression_contains_child_call_in_all_paths}
-    for additional explanations.
- *)
-let filter_useless_monadic_calls = ref true
-
-(** If {!filter_useless_monadic_calls} is activated, some functions
-    become useless: if this option is true, we don't extract them.
-
-    The calls to functions which always get filtered are:
-    - the forward functions with unit return value
-    - the backward functions which don't output anything (backward
-      functions coming from rust functions with no mutable borrows
-      as input values - note that if a function doesn't take mutable
-      borrows as inputs, it can't return mutable borrows; we actually
-      dynamically check for that).
- *)
-let filter_useless_functions = ref true
-
 (** Simplify the forward/backward functions, in case we merge them
     (i.e., the forward functions return the backward functions).