Merge pull request #83 from AeneasVerif/son/backs

Remove the option to split the forward/backward functions

1 files changed, 0 insertions, 187 deletions

diff --git a/tests/fstar-split/demo/Demo.fst b/tests/fstar-split/demo/Demo.fst
deleted file mode 100644
index ab746157..00000000
--- a/tests/fstar-split/demo/Demo.fst
+++ /dev/null
@@ -1,187 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [demo] *)
-module Demo
-open Primitives
-
-#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
-
-(** [demo::choose]: forward function
-    Source: 'src/demo.rs', lines 5:0-5:70 *)
-let choose (t : Type0) (b : bool) (x : t) (y : t) : result t =
-  if b then Return x else Return y
-
-(** [demo::choose]: backward function 0
-    Source: 'src/demo.rs', lines 5:0-5:70 *)
-let choose_back
-  (t : Type0) (b : bool) (x : t) (y : t) (ret : t) : result (t & t) =
-  if b then Return (ret, y) else Return (x, ret)
-
-(** [demo::mul2_add1]: forward function
-    Source: 'src/demo.rs', lines 13:0-13:31 *)
-let mul2_add1 (x : u32) : result u32 =
-  let* i = u32_add x x in u32_add i 1
-
-(** [demo::use_mul2_add1]: forward function
-    Source: 'src/demo.rs', lines 17:0-17:43 *)
-let use_mul2_add1 (x : u32) (y : u32) : result u32 =
-  let* i = mul2_add1 x in u32_add i y
-
-(** [demo::incr]: merged forward/backward function
-    (there is a single backward function, and the forward function returns ())
-    Source: 'src/demo.rs', lines 21:0-21:31 *)
-let incr (x : u32) : result u32 =
-  u32_add x 1
-
-(** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
-type cList_t (t : Type0) =
-| CList_CCons : t -> cList_t t -> cList_t t
-| CList_CNil : cList_t t
-
-(** [demo::list_nth]: forward function
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
-let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    begin match l with
-    | CList_CCons x tl ->
-      if i = 0 then Return x else let* i1 = u32_sub i 1 in list_nth t n1 tl i1
-    | CList_CNil -> Fail Failure
-    end
-
-(** [demo::list_nth_mut]: forward function
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
-let rec list_nth_mut
-  (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    begin match l with
-    | CList_CCons x tl ->
-      if i = 0
-      then Return x
-      else let* i1 = u32_sub i 1 in list_nth_mut t n1 tl i1
-    | CList_CNil -> Fail Failure
-    end
-
-(** [demo::list_nth_mut]: backward function 0
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
-let rec list_nth_mut_back
-  (t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
-  result (cList_t t)
-  =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    begin match l with
-    | CList_CCons x tl ->
-      if i = 0
-      then Return (CList_CCons ret tl)
-      else
-        let* i1 = u32_sub i 1 in
-        let* tl1 = list_nth_mut_back t n1 tl i1 ret in
-        Return (CList_CCons x tl1)
-    | CList_CNil -> Fail Failure
-    end
-
-(** [demo::list_nth_mut1]: loop 0: forward function
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
-let rec list_nth_mut1_loop
-  (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    begin match l with
-    | CList_CCons x tl ->
-      if i = 0
-      then Return x
-      else let* i1 = u32_sub i 1 in list_nth_mut1_loop t n1 tl i1
-    | CList_CNil -> Fail Failure
-    end
-
-(** [demo::list_nth_mut1]: forward function
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
-let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
-  list_nth_mut1_loop t n l i
-
-(** [demo::list_nth_mut1]: loop 0: backward function 0
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
-let rec list_nth_mut1_loop_back
-  (t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
-  result (cList_t t)
-  =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    begin match l with
-    | CList_CCons x tl ->
-      if i = 0
-      then Return (CList_CCons ret tl)
-      else
-        let* i1 = u32_sub i 1 in
-        let* tl1 = list_nth_mut1_loop_back t n1 tl i1 ret in
-        Return (CList_CCons x tl1)
-    | CList_CNil -> Fail Failure
-    end
-
-(** [demo::list_nth_mut1]: backward function 0
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
-let list_nth_mut1_back
-  (t : Type0) (n : nat) (l : cList_t t) (i : u32) (ret : t) :
-  result (cList_t t)
-  =
-  list_nth_mut1_loop_back t n l i ret
-
-(** [demo::i32_id]: forward function
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
-let rec i32_id (n : nat) (i : i32) : result i32 =
-  if is_zero n
-  then Fail OutOfFuel
-  else
-    let n1 = decrease n in
-    if i = 0
-    then Return 0
-    else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
-
-(** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
-noeq type counter_t (self : Type0) = {
-  incr : self -> result usize;
-  incr_back : self -> result self;
-}
-
-(** [demo::{usize}::incr]: forward function
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
-let usize_incr (self : usize) : result usize =
-  let* _ = usize_add self 1 in Return self
-
-(** [demo::{usize}::incr]: backward function 0
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
-let usize_incr_back (self : usize) : result usize =
-  usize_add self 1
-
-(** Trait implementation: [demo::{usize}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
-let demo_CounterUsizeInst : counter_t usize = {
-  incr = usize_incr;
-  incr_back = usize_incr_back;
-}
-
-(** [demo::use_counter]: forward function
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
-let use_counter
-  (t : Type0) (counterTInst : counter_t t) (cnt : t) : result usize =
-  counterTInst.incr cnt
-
-(** [demo::use_counter]: backward function 0
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
-let use_counter_back
-  (t : Type0) (counterTInst : counter_t t) (cnt : t) : result t =
-  counterTInst.incr_back cnt
-