From a4efda3fd27364316bd65f34bc3eac3fd2cbf87d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 8 Mar 2024 16:13:19 +0100 Subject: Remove the split test files for F* --- tests/fstar-split/demo/Demo.fst | 187 ---------------------------------------- 1 file changed, 187 deletions(-) delete mode 100644 tests/fstar-split/demo/Demo.fst (limited to 'tests/fstar-split/demo/Demo.fst') 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 - -- cgit v1.2.3