diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/coq/misc/Loops.v | 19 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.Funs.fst | 18 |
2 files changed, 18 insertions, 19 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 72c47361..8d552b5b 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -7,20 +7,19 @@ Local Open Scope Primitives_scope. Module Loops. (** [loops::sum] *) -Fixpoint sum_loop0_fwd - (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := +Fixpoint sum_loop_fwd (n : nat) (max : u32) (i : u32) (s : u32) : result u32 := match n with | O => Fail_ OutOfFuel | S n0 => if i s< max - then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop0_fwd n0 max i0 s0) + then (s0 <- u32_add s i; i0 <- u32_add i 1%u32; sum_loop_fwd n0 max i0 s0) else u32_mul s 2%u32 end . (** [loops::sum] *) Definition sum_fwd (n : nat) (max : u32) : result u32 := - sum_loop0_fwd n max (0%u32) (0%u32) + sum_loop_fwd n max (0%u32) (0%u32) . (** [loops::List] *) @@ -33,7 +32,7 @@ Arguments ListCons {T} _ _. Arguments ListNil {T}. (** [loops::list_nth_mut_loop] *) -Fixpoint list_nth_mut_loop_loop0_fwd +Fixpoint list_nth_mut_loop_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := match n with | O => Fail_ OutOfFuel @@ -42,7 +41,7 @@ Fixpoint list_nth_mut_loop_loop0_fwd | ListCons x tl => if i s= 0%u32 then Return x - else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop0_fwd T n0 tl i0) + else (i0 <- u32_sub i 1%u32; list_nth_mut_loop_loop_fwd T n0 tl i0) | ListNil => Fail_ Failure end end @@ -51,11 +50,11 @@ Fixpoint list_nth_mut_loop_loop0_fwd (** [loops::list_nth_mut_loop] *) Definition list_nth_mut_loop_fwd (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T := - list_nth_mut_loop_loop0_fwd T n ls i + list_nth_mut_loop_loop_fwd T n ls i . (** [loops::list_nth_mut_loop] *) -Fixpoint list_nth_mut_loop_loop0_back +Fixpoint list_nth_mut_loop_loop_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) := @@ -68,7 +67,7 @@ Fixpoint list_nth_mut_loop_loop0_back then Return (ListCons ret tl) else ( i0 <- u32_sub i 1%u32; - l <- list_nth_mut_loop_loop0_back T n0 tl i0 ret; + l <- list_nth_mut_loop_loop_back T n0 tl i0 ret; Return (ListCons x l)) | ListNil => Fail_ Failure end @@ -80,7 +79,7 @@ Definition list_nth_mut_loop_back (T : Type) (n : nat) (ls : List_t T) (i : u32) (ret : T) : result (List_t T) := - list_nth_mut_loop_loop0_back T n ls i ret + list_nth_mut_loop_loop_back T n ls i ret . End Loops . diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst index a2ae2563..cf05b7f2 100644 --- a/tests/fstar/misc/Loops.Funs.fst +++ b/tests/fstar/misc/Loops.Funs.fst @@ -8,7 +8,7 @@ include Loops.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [loops::sum] *) -let rec sum_loop0_fwd +let rec sum_loop_fwd (max : u32) (i : u32) (s : u32) : Tot (result u32) (decreases (sum_decreases max i s)) = @@ -19,16 +19,16 @@ let rec sum_loop0_fwd | Return s0 -> begin match u32_add i 1 with | Fail e -> Fail e - | Return i0 -> sum_loop0_fwd max i0 s0 + | Return i0 -> sum_loop_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 +let sum_fwd (max : u32) : result u32 = sum_loop_fwd max 0 0 (** [loops::list_nth_mut_loop] *) -let rec list_nth_mut_loop_loop0_fwd +let rec list_nth_mut_loop_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : Tot (result t) (decreases (list_nth_mut_loop_decreases t ls i)) = @@ -39,17 +39,17 @@ let rec list_nth_mut_loop_loop0_fwd else begin match u32_sub i 1 with | Fail e -> Fail e - | Return i0 -> list_nth_mut_loop_loop0_fwd t tl i0 + | Return i0 -> list_nth_mut_loop_loop_fwd t tl i0 end | ListNil -> Fail Failure end (** [loops::list_nth_mut_loop] *) let list_nth_mut_loop_fwd (t : Type0) (ls : list_t t) (i : u32) : result t = - list_nth_mut_loop_loop0_fwd t ls i + list_nth_mut_loop_loop_fwd t ls i (** [loops::list_nth_mut_loop] *) -let rec list_nth_mut_loop_loop0_back +let rec list_nth_mut_loop_loop_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : Tot (result (list_t t)) (decreases (list_nth_mut_loop_decreases t ls i)) = @@ -61,7 +61,7 @@ let rec list_nth_mut_loop_loop0_back begin match u32_sub i 1 with | Fail e -> Fail e | Return i0 -> - begin match list_nth_mut_loop_loop0_back t tl i0 ret with + begin match list_nth_mut_loop_loop_back t tl i0 ret with | Fail e -> Fail e | Return l -> Return (ListCons x l) end @@ -72,5 +72,5 @@ let rec list_nth_mut_loop_loop0_back (** [loops::list_nth_mut_loop] *) let list_nth_mut_loop_back (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = - list_nth_mut_loop_loop0_back t ls i ret + list_nth_mut_loop_loop_back t ls i ret |