summaryrefslogtreecommitdiff
path: root/tests/fstar/demo
diff options
context:
space:
mode:
authorSon HO2024-03-20 06:48:08 +0100
committerGitHub2024-03-20 06:48:08 +0100
commit0d52c3fe35d0b24de729bdfb917ad6c7104d0c6e (patch)
tree7748d3c19a0993edc710690491a2dc6ea3a2b58f /tests/fstar/demo
parent8111c970fcae9d609961eba2ad6716e8c9fc1046 (diff)
parent34850eed3c66f7f2c432294e4c589be53ad5d37b (diff)
Merge pull request #93 from AeneasVerif/son/examples
Add some examples and improve the shape of the generated code
Diffstat (limited to '')
-rw-r--r--tests/fstar/demo/Demo.fst47
1 files changed, 36 insertions, 11 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d13d2ba3..d93bc847 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* x = incr 0 in let* x1 = incr x in let* _ = incr x1 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,15 +104,15 @@ 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)))
=
- let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
+ list_nth_mut1_loop t n l i
(** [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