diff options
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/demo/Demo.fst | 138 |
1 files changed, 138 insertions, 0 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst new file mode 100644 index 00000000..f9082979 --- /dev/null +++ b/tests/fstar/demo/Demo.fst @@ -0,0 +1,138 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [demo] *) +module Demo +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [demo::choose]: + Source: 'src/demo.rs', lines 5:0-5:70 *) +let choose + (t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) = + if b + then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a) + else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a) + +(** [demo::mul2_add1]: + 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]: + 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]: + 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]: + 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]: + 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 & (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 + let back_'a = fun ret -> Return (CList_CCons ret tl) in + Return (x, back_'a) + else + let* i1 = u32_sub i 1 in + let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in + let back_'a = + fun ret -> + let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in + Return (x1, back_'a) + | CList_CNil -> Fail Failure + end + +(** [demo::list_nth_mut1]: loop 0: + 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 & (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 + let back_'a = fun ret -> Return (CList_CCons ret tl) in + Return (x, back_'a) + else + let* i1 = u32_sub i 1 in + let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in + let back_'a1 = + fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in + Return (x1, back_'a1) + | CList_CNil -> Fail Failure + end + +(** [demo::list_nth_mut1]: + 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 & (t -> result (cList_t t))) + = + let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a) + +(** [demo::i32_id]: + 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 & self); } + +(** [demo::{usize}::incr]: + Source: 'src/demo.rs', lines 88:4-88:31 *) +let usize_incr (self : usize) : result (usize & usize) = + let* self1 = usize_add self 1 in Return (self, self1) + +(** Trait implementation: [demo::{usize}] + Source: 'src/demo.rs', lines 87:0-87:22 *) +let demo_CounterUsizeInst : counter_t usize = { incr = usize_incr; } + +(** [demo::use_counter]: + Source: 'src/demo.rs', lines 95:0-95:59 *) +let use_counter + (t : Type0) (counterTInst : counter_t t) (cnt : t) : result (usize & t) = + counterTInst.incr cnt + |