diff options
Diffstat (limited to 'tests/coq/misc')
| -rw-r--r-- | tests/coq/misc/Loops.v | 39 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 4 |
2 files changed, 12 insertions, 31 deletions
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index e235b60d..85b54510 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -183,7 +183,7 @@ Definition list_nth_mut_loop (T : Type) (n : nat) (ls : List_t T) (i : u32) : result (T * (T -> result (List_t T))) := - p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back) + list_nth_mut_loop_loop T n ls i . (** [loops::list_nth_shared_loop]: loop 0: @@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T))) := - t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i; - let '(p, back_'a, back_'b) := t in - Return (p, back_'a, back_'b) + list_nth_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair]: loop 0: @@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T)))) := - p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_loop_pair_merge]: loop 0: @@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: @@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair]: loop 0: @@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i; - let (p1, back_'b) := p in - Return (p1, back_'b) + list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i . (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: @@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) : result ((T * T) * (T -> result (List_t T))) := - p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i; - let (p1, back_'a) := p in - Return (p1, back_'a) + list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i . (** [loops::ignore_input_mut_borrow]: loop 0: @@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- incr_ignore_input_mut_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1) else Return tt end . @@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit := | O => Fail_ OutOfFuel | S n1 => if i s> 0%u32 - then ( - i1 <- u32_sub i 1%u32; - _ <- ignore_input_shared_borrow_loop n1 i1; - Return tt) + then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1) else Return tt end . diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 869cdb4d..308de4f4 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -3,6 +3,7 @@ -arg -w -arg all +External_FunsExternal_Template.v Loops.v External_Types.v Primitives.v @@ -10,9 +11,8 @@ External_Funs.v External_TypesExternal.v Constants.v PoloniusList.v -Paper.v NoNestedBorrows.v External_FunsExternal.v Bitwise.v External_TypesExternal_Template.v -External_FunsExternal_Template.v +Paper.v |