summaryrefslogtreecommitdiff
path: root/tests/fstar/demo
diff options
context:
space:
mode:
authorSon Ho2024-06-04 13:52:44 +0200
committerSon Ho2024-06-04 13:52:44 +0200
commit3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (patch)
tree89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /tests/fstar/demo
parent2a7a18d6a07ea4967ba9ec0763e6b7d04849dc7e (diff)
parent4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff)
Merge branch 'main' into son/loops2
Diffstat (limited to 'tests/fstar/demo')
-rw-r--r--tests/fstar/demo/Demo.fst32
1 files changed, 16 insertions, 16 deletions
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 41fd9804..d89f32e0 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -6,7 +6,7 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [demo::choose]:
- Source: 'tests/src/demo.rs', lines 5:0-5:70 *)
+ Source: 'tests/src/demo.rs', lines 7:0-7:70 *)
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
@@ -14,33 +14,33 @@ let choose
else let back = fun ret -> Ok (x, ret) in Ok (y, back)
(** [demo::mul2_add1]:
- Source: 'tests/src/demo.rs', lines 13:0-13:31 *)
+ Source: 'tests/src/demo.rs', lines 15:0-15:31 *)
let mul2_add1 (x : u32) : result u32 =
let* i = u32_add x x in u32_add i 1
(** [demo::use_mul2_add1]:
- Source: 'tests/src/demo.rs', lines 17:0-17:43 *)
+ Source: 'tests/src/demo.rs', lines 19:0-19:43 *)
let use_mul2_add1 (x : u32) (y : u32) : result u32 =
let* i = mul2_add1 x in u32_add i y
(** [demo::incr]:
- Source: 'tests/src/demo.rs', lines 21:0-21:31 *)
+ Source: 'tests/src/demo.rs', lines 23:0-23:31 *)
let incr (x : u32) : result u32 =
u32_add x 1
(** [demo::use_incr]:
- Source: 'tests/src/demo.rs', lines 25:0-25:17 *)
+ Source: 'tests/src/demo.rs', lines 27:0-27:17 *)
let use_incr : result unit =
let* x = incr 0 in let* x1 = incr x in let* _ = incr x1 in Ok ()
(** [demo::CList]
- Source: 'tests/src/demo.rs', lines 34:0-34:17 *)
+ Source: 'tests/src/demo.rs', lines 36:0-36:17 *)
type cList_t (t : Type0) =
| CList_CCons : t -> cList_t t -> cList_t t
| CList_CNil : cList_t t
(** [demo::list_nth]:
- Source: 'tests/src/demo.rs', lines 39:0-39:56 *)
+ Source: 'tests/src/demo.rs', lines 41:0-41:56 *)
let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
if is_zero n
then Fail OutOfFuel
@@ -53,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: 'tests/src/demo.rs', lines 54:0-54:68 *)
+ Source: 'tests/src/demo.rs', lines 56:0-56:68 *)
let rec list_nth_mut
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
@@ -77,7 +77,7 @@ let rec list_nth_mut
end
(** [demo::list_nth_mut1]: loop 0:
- Source: 'tests/src/demo.rs', lines 69:0-78:1 *)
+ Source: 'tests/src/demo.rs', lines 71:0-80: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 +99,7 @@ let rec list_nth_mut1_loop
end
(** [demo::list_nth_mut1]:
- Source: 'tests/src/demo.rs', lines 69:0-69:77 *)
+ Source: 'tests/src/demo.rs', lines 71:0-71:77 *)
let list_nth_mut1
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
@@ -107,7 +107,7 @@ let list_nth_mut1
list_nth_mut1_loop t n l i
(** [demo::i32_id]:
- Source: 'tests/src/demo.rs', lines 80:0-80:28 *)
+ Source: 'tests/src/demo.rs', lines 82:0-82:28 *)
let rec i32_id (n : nat) (i : i32) : result i32 =
if is_zero n
then Fail OutOfFuel
@@ -118,7 +118,7 @@ let rec i32_id (n : nat) (i : i32) : result i32 =
else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
(** [demo::list_tail]:
- Source: 'tests/src/demo.rs', lines 88:0-88:64 *)
+ Source: 'tests/src/demo.rs', lines 90:0-90:64 *)
let rec list_tail
(t : Type0) (n : nat) (l : cList_t t) :
result ((cList_t t) & (cList_t t -> result (cList_t t)))
@@ -137,20 +137,20 @@ let rec list_tail
end
(** Trait declaration: [demo::Counter]
- Source: 'tests/src/demo.rs', lines 97:0-97:17 *)
+ Source: 'tests/src/demo.rs', lines 99:0-99:17 *)
noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
(** [demo::{(demo::Counter for usize)}::incr]:
- Source: 'tests/src/demo.rs', lines 102:4-102:31 *)
+ Source: 'tests/src/demo.rs', lines 104:4-104:31 *)
let counterUsize_incr (self : usize) : result (usize & usize) =
let* self1 = usize_add self 1 in Ok (self, self1)
(** Trait implementation: [demo::{(demo::Counter for usize)}]
- Source: 'tests/src/demo.rs', lines 101:0-101:22 *)
+ Source: 'tests/src/demo.rs', lines 103:0-103:22 *)
let counterUsize : counter_t usize = { incr = counterUsize_incr; }
(** [demo::use_counter]:
- Source: 'tests/src/demo.rs', lines 109:0-109:59 *)
+ Source: 'tests/src/demo.rs', lines 111:0-111:59 *)
let use_counter
(t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
counterInst.incr cnt