diff options
Diffstat (limited to 'tests/fstar')
| -rw-r--r-- | tests/fstar/demo/Demo.fst | 45 |
1 files changed, 35 insertions, 10 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index d13d2ba3..5651b80f 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -28,14 +28,19 @@ let use_mul2_add1 (x : u32) (y : u32) : result u32 = let incr (x : u32) : result u32 = u32_add x 1 +(** [demo::use_incr]: + Source: 'src/demo.rs', lines 25:0-25:17 *) +let use_incr : result unit = + let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return () + (** [demo::CList] - Source: 'src/demo.rs', lines 27:0-27:17 *) + Source: 'src/demo.rs', lines 34:0-34: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 *) + Source: 'src/demo.rs', lines 39:0-39:56 *) let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = if is_zero n then Fail OutOfFuel @@ -48,7 +53,7 @@ let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t = end (** [demo::list_nth_mut]: - Source: 'src/demo.rs', lines 47:0-47:68 *) + Source: 'src/demo.rs', lines 54:0-54:68 *) let rec list_nth_mut (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -74,7 +79,7 @@ let rec list_nth_mut end (** [demo::list_nth_mut1]: loop 0: - Source: 'src/demo.rs', lines 62:0-71:1 *) + Source: 'src/demo.rs', lines 69:0-78:1 *) let rec list_nth_mut1_loop (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -99,7 +104,7 @@ let rec list_nth_mut1_loop end (** [demo::list_nth_mut1]: - Source: 'src/demo.rs', lines 62:0-62:77 *) + Source: 'src/demo.rs', lines 69:0-69:77 *) let list_nth_mut1 (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result (t & (t -> result (cList_t t))) @@ -107,7 +112,7 @@ let list_nth_mut1 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 *) + Source: 'src/demo.rs', lines 80:0-80:28 *) let rec i32_id (n : nat) (i : i32) : result i32 = if is_zero n then Fail OutOfFuel @@ -117,21 +122,41 @@ let rec i32_id (n : nat) (i : i32) : result i32 = then Return 0 else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1 +(** [demo::list_tail]: + Source: 'src/demo.rs', lines 88:0-88:64 *) +let rec list_tail + (t : Type0) (n : nat) (l : cList_t t) : + result ((cList_t t) & (cList_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 -> + let* (c, list_tail_back) = list_tail t n1 tl in + let back_'a = + fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1) + in + Return (c, back_'a) + | CList_CNil -> Return (CList_CNil, Return) + end + (** Trait declaration: [demo::Counter] - Source: 'src/demo.rs', lines 83:0-83:17 *) + Source: 'src/demo.rs', lines 97:0-97:17 *) noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); } (** [demo::{(demo::Counter for usize)}::incr]: - Source: 'src/demo.rs', lines 88:4-88:31 *) + Source: 'src/demo.rs', lines 102:4-102:31 *) let counterUsize_incr (self : usize) : result (usize & usize) = let* self1 = usize_add self 1 in Return (self, self1) (** Trait implementation: [demo::{(demo::Counter for usize)}] - Source: 'src/demo.rs', lines 87:0-87:22 *) + Source: 'src/demo.rs', lines 101:0-101:22 *) let counterUsize : counter_t usize = { incr = counterUsize_incr; } (** [demo::use_counter]: - Source: 'src/demo.rs', lines 95:0-95:59 *) + Source: 'src/demo.rs', lines 109:0-109:59 *) let use_counter (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) = counterInst.incr cnt |