diff options
| author | Son Ho | 2022-12-17 14:30:41 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | 960b7131afe3b7bb24e0abaca1e24100d0046b0e (patch) | |
| tree | 3b26f3a9439812ce4bc4631f95571d2d5f077802 /tests/fstar | |
| parent | acdfede396a36723258e0a6d7b264cec9ca99672 (diff) | |
Make another loop example work
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.Template.fst | 3 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Clauses.fst | 4 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 20 |
3 files changed, 27 insertions, 0 deletions
diff --git a/tests/fstar/misc/Loops.Clauses.Template.fst b/tests/fstar/misc/Loops.Clauses.Template.fst index a898e9fb..79a9dc4e 100644 --- a/tests/fstar/misc/Loops.Clauses.Template.fst +++ b/tests/fstar/misc/Loops.Clauses.Template.fst @@ -6,6 +6,9 @@ open Loops.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** [loops::sum]: decreases clause *) +unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = admit () + (** [loops::list_nth_mut_loop]: decreases clause *) unfold let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat = diff --git a/tests/fstar/misc/Loops.Clauses.fst b/tests/fstar/misc/Loops.Clauses.fst index e09eda9a..2087f2e7 100644 --- a/tests/fstar/misc/Loops.Clauses.fst +++ b/tests/fstar/misc/Loops.Clauses.fst @@ -5,6 +5,10 @@ open Loops.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** [loops::sum]: decreases clause *) +unfold let sum_decreases (max : u32) (i : u32) (s : u32) : nat = + if i <= max then max - i else 0 + (** [loops::list_nth_mut_loop]: decreases clause *) unfold let list_nth_mut_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : nat = diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index 870a2159..a2ae2563 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -7,6 +7,26 @@ include Loops.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" +(** [loops::sum] *) +let rec sum_loop0_fwd + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_decreases max i s)) + = + if i < max + then + begin match u32_add s i with + | Fail e -> Fail e + | Return s0 -> + begin match u32_add i 1 with + | Fail e -> Fail e + | Return i0 -> sum_loop0_fwd max i0 s0 + end + end + else u32_mul s 2 + +(** [loops::sum] *) +let sum_fwd (max : u32) : result u32 = sum_loop0_fwd max 0 0 + (** [loops::list_nth_mut_loop] *) let rec list_nth_mut_loop_loop0_fwd (t : Type0) (ls : list_t t) (i : u32) : |