diff options
| -rw-r--r-- | Makefile | 26 | ||||
| -rw-r--r-- | compiler/Config.ml | 4 | ||||
| -rw-r--r-- | compiler/Driver.ml | 14 | ||||
| -rw-r--r-- | tests/fstar/misc/Loops.fst | 784 | ||||
| -rw-r--r-- | tests/lean/Array.lean | 436 | ||||
| -rw-r--r-- | tests/lean/Loops.lean | 630 | ||||
| -rw-r--r-- | tests/lean/Loops/Funs.lean | 625 | ||||
| -rw-r--r-- | tests/lean/Loops/Types.lean | 13 | ||||
| -rw-r--r-- | tests/lean/Traits.lean | 411 | ||||
| -rw-r--r-- | tests/lean/Traits/Funs.lean | 275 | ||||
| -rw-r--r-- | tests/lean/Traits/Types.lean | 144 |
11 files changed, 2280 insertions, 1082 deletions
@@ -115,7 +115,7 @@ AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BA # Add specific options to some tests test-no_nested_borrows test-paper: \ - OPTIONS += -test-trans-units -no-split-files -no-state + OPTIONS += -test-trans-units test-no_nested_borrows test-paper: SUBDIR := misc tfstar-no_nested_borrows tfstar-paper: tlean-no_nested_borrows: SUBDIR := @@ -123,7 +123,7 @@ tlean-paper: SUBDIR := thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows thol4-paper: SUBDIR := misc-paper -test-array: OPTIONS += -no-state +test-array: OPTIONS += test-array: SUBDIR := array tfstar-array: OPTIONS += -decreases-clauses -template-clauses tcoq-array: OPTIONS += -use-fuel @@ -131,7 +131,7 @@ tlean-array: SUBDIR := tlean-array: OPTIONS += thol4-array: OPTIONS += -test-traits: OPTIONS += -no-state +test-traits: OPTIONS += test-traits: SUBDIR := traits tfstar-traits: OPTIONS += -decreases-clauses -template-clauses tcoq-traits: OPTIONS += -use-fuel @@ -147,15 +147,15 @@ thol4-array: thol4-traits: echo "Ignoring the traits test for HOL4" -test-loops: OPTIONS += -no-state +test-loops: OPTIONS += test-loops: SUBDIR := misc -tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -tcoq-loops: OPTIONS += -use-fuel -no-split-files +tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files +tcoq-loops: OPTIONS += -use-fuel tlean-loops: SUBDIR := thol4-loops: SUBDIR := misc-loops # TODO: reactivate -test-trans-units -test-hashmap: OPTIONS += -no-state +test-hashmap: OPTIONS += -split-files test-hashmap: SUBDIR := hashmap tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap: OPTIONS += -use-fuel @@ -164,14 +164,14 @@ tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hash thol4-hashmap: OPTIONS += # TODO: reactivate -test-trans-units -test-hashmap_main: OPTIONS += +test-hashmap_main: OPTIONS += -state -split-files test-hashmap_main: SUBDIR := hashmap_on_disk tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses tcoq-hashmap_main: OPTIONS += -use-fuel tlean-hashmap_main: SUBDIR := thol4-hashmap_main: OPTIONS += -testp-polonius_list: OPTIONS += -test-trans-units -no-split-files -no-state +testp-polonius_list: OPTIONS += -test-trans-units testp-polonius_list: SUBDIR := misc tfstarp-polonius_list: OPTIONS += tcoqp-polonius_list: OPTIONS += @@ -180,7 +180,7 @@ tleanp-polonius_list: OPTIONS += thol4p-polonius_list: SUBDIR := misc-polonius_list thol4p-polonius_list: OPTIONS += -test-constants: OPTIONS += -test-trans-units -no-split-files -no-state +test-constants: OPTIONS += -test-trans-units test-constants: SUBDIR := misc tfstar-constants: OPTIONS += tcoq-constants: OPTIONS += @@ -189,7 +189,7 @@ tlean-constants: OPTIONS += thol4-constants: SUBDIR := misc-constants thol4-constants: OPTIONS += -test-external: OPTIONS += -test-trans-units +test-external: OPTIONS += -test-trans-units -state -split-files test-external: SUBDIR := misc tfstar-external: OPTIONS += tcoq-external: OPTIONS += @@ -199,7 +199,7 @@ thol4-external: SUBDIR := misc-external thol4-external: OPTIONS += BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses -testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units +testp-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files testp-betree_main: SUBDIR:=betree tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) tcoqp-betree_main: OPTIONS += -use-fuel @@ -211,7 +211,7 @@ thol4-betree_main: OPTIONS += # This generates very ugly code, but is good to test the translation. .PHONY: ctest-testp-betree_main ctest-testp-betree_main: testp-betree_main -ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units +ctest-testp-betree_main: OPTIONS += -backend fstar -test-trans-units -state -split-files ctest-testp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS) ctest-testp-betree_main: BACKEND_SUBDIR := "fstar" ctest-testp-betree_main: SUBDIR:=betree_back_stateful diff --git a/compiler/Config.ml b/compiler/Config.ml index 8483c879..a487f9e2 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -124,7 +124,7 @@ let always_deconstruct_adts_with_matches = ref false (** Controls whether we need to use a state to model the external world (I/O, for instance). *) -let use_state = ref true +let use_state = ref false (** Controls whether we use fuel to control termination. *) @@ -160,7 +160,7 @@ let backward_no_state_update = ref false files for the types, clauses and functions, or if we group them in one file. *) -let split_files = ref true +let split_files = ref false (** Generate the library entry point, if the crate is split between different files. diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 14668632..128ae890 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -93,9 +93,9 @@ let () = Arg.Set extract_decreases_clauses, " Use decreases clauses/termination measures for the recursive \ definitions" ); - ( "-no-state", - Arg.Clear use_state, - " Do not use state-error monads, simply use error monads" ); + ( "-state", + Arg.Set use_state, + " Use a *state*-error monads, instead of an error monads" ); ( "-use-fuel", Arg.Set use_fuel, " Use a fuel parameter to control divergence" ); @@ -106,10 +106,10 @@ let () = Arg.Set extract_template_decreases_clauses, " Generate templates for the required decreases clauses/termination \ measures, in a dedicated file. Implies -decreases-clauses" ); - ( "-no-split-files", - Arg.Clear split_files, - " Do not split the definitions between different files for types, \ - functions, etc." ); + ( "-split-files", + Arg.Set split_files, + " Split the definitions between different files for types, functions, \ + etc." ); ( "-no-check-inv", Arg.Clear check_invariants, " Deactivate the invariant sanity checks performed at every evaluation \ diff --git a/tests/fstar/misc/Loops.fst b/tests/fstar/misc/Loops.fst new file mode 100644 index 00000000..823acdd4 --- /dev/null +++ b/tests/fstar/misc/Loops.fst @@ -0,0 +1,784 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [loops] *) +module Loops +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [loops::sum]: decreases clause *) +unfold let sum_loop_decreases (max : u32) (i : u32) (s : u32) : nat = admit () + +(** [loops::sum]: loop 0: forward function *) +let rec sum_loop + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_loop_decreases max i s)) + = + if i < max + then let* s0 = u32_add s i in let* i0 = u32_add i 1 in sum_loop max i0 s0 + else u32_mul s 2 + +(** [loops::sum]: forward function *) +let sum (max : u32) : result u32 = + sum_loop max 0 0 + +(** [loops::sum_with_mut_borrows]: decreases clause *) +unfold +let sum_with_mut_borrows_loop_decreases (max : u32) (mi : u32) (ms : u32) : nat + = + admit () + +(** [loops::sum_with_mut_borrows]: loop 0: forward function *) +let rec sum_with_mut_borrows_loop + (max : u32) (mi : u32) (ms : u32) : + Tot (result u32) (decreases (sum_with_mut_borrows_loop_decreases max mi ms)) + = + if mi < max + then + let* ms0 = u32_add ms mi in + let* mi0 = u32_add mi 1 in + sum_with_mut_borrows_loop max mi0 ms0 + else u32_mul ms 2 + +(** [loops::sum_with_mut_borrows]: forward function *) +let sum_with_mut_borrows (max : u32) : result u32 = + sum_with_mut_borrows_loop max 0 0 + +(** [loops::sum_with_shared_borrows]: decreases clause *) +unfold +let sum_with_shared_borrows_loop_decreases (max : u32) (i : u32) (s : u32) : + nat = + admit () + +(** [loops::sum_with_shared_borrows]: loop 0: forward function *) +let rec sum_with_shared_borrows_loop + (max : u32) (i : u32) (s : u32) : + Tot (result u32) (decreases (sum_with_shared_borrows_loop_decreases max i s)) + = + if i < max + then + let* i0 = u32_add i 1 in + let* s0 = u32_add s i0 in + sum_with_shared_borrows_loop max i0 s0 + else u32_mul s 2 + +(** [loops::sum_with_shared_borrows]: forward function *) +let sum_with_shared_borrows (max : u32) : result u32 = + sum_with_shared_borrows_loop max 0 0 + +(** [loops::clear]: decreases clause *) +unfold +let clear_loop_decreases (v : alloc_vec_Vec u32) (i : usize) : nat = admit () + +(** [loops::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let rec clear_loop + (v : alloc_vec_Vec u32) (i : usize) : + Tot (result (alloc_vec_Vec u32)) (decreases (clear_loop_decreases v i)) + = + let i0 = alloc_vec_Vec_len u32 v in + if i < i0 + then + let* i1 = usize_add i 1 in + let* v0 = + alloc_vec_Vec_index_mut_back u32 usize + (core_slice_index_usize_coresliceindexSliceIndexInst u32) v i 0 in + clear_loop v0 i1 + else Return v + +(** [loops::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +let clear (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) = + clear_loop v 0 + +(** [loops::List] *) +type list_t (t : Type0) = +| List_Cons : t -> list_t t -> list_t t +| List_Nil : list_t t + +(** [loops::list_mem]: decreases clause *) +unfold let list_mem_loop_decreases (x : u32) (ls : list_t u32) : nat = admit () + +(** [loops::list_mem]: loop 0: forward function *) +let rec list_mem_loop + (x : u32) (ls : list_t u32) : + Tot (result bool) (decreases (list_mem_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return true else list_mem_loop x tl + | List_Nil -> Return false + end + +(** [loops::list_mem]: forward function *) +let list_mem (x : u32) (ls : list_t u32) : result bool = + list_mem_loop x ls + +(** [loops::list_nth_mut_loop]: decreases clause *) +unfold +let list_nth_mut_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::list_nth_mut_loop]: loop 0: forward function *) +let rec list_nth_mut_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_mut_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_mut_loop_loop t tl i0 + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop]: forward function *) +let list_nth_mut_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_mut_loop_loop t ls i + +(** [loops::list_nth_mut_loop]: loop 0: backward function 0 *) +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_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return (List_Cons ret tl) + else + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_loop_back t tl i0 ret in + Return (List_Cons x tl0) + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop]: backward function 0 *) +let list_nth_mut_loop_back + (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = + list_nth_mut_loop_loop_back t ls i ret + +(** [loops::list_nth_shared_loop]: decreases clause *) +unfold +let list_nth_shared_loop_loop_decreases (t : Type0) (ls : list_t t) (i : u32) : + nat = + admit () + +(** [loops::list_nth_shared_loop]: loop 0: forward function *) +let rec list_nth_shared_loop_loop + (t : Type0) (ls : list_t t) (i : u32) : + Tot (result t) (decreases (list_nth_shared_loop_loop_decreases t ls i)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_shared_loop_loop t tl i0 + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop]: forward function *) +let list_nth_shared_loop (t : Type0) (ls : list_t t) (i : u32) : result t = + list_nth_shared_loop_loop t ls i + +(** [loops::get_elem_mut]: decreases clause *) +unfold +let get_elem_mut_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::get_elem_mut]: loop 0: forward function *) +let rec get_elem_mut_loop + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_mut_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return y else get_elem_mut_loop x tl + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_mut]: forward function *) +let get_elem_mut + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_mut_loop x l + +(** [loops::get_elem_mut]: loop 0: backward function 0 *) +let rec get_elem_mut_loop_back + (x : usize) (ls : list_t usize) (ret : usize) : + Tot (result (list_t usize)) (decreases (get_elem_mut_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> + if y = x + then Return (List_Cons ret tl) + else let* tl0 = get_elem_mut_loop_back x tl ret in Return (List_Cons y tl0) + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_mut]: backward function 0 *) +let get_elem_mut_back + (slots : alloc_vec_Vec (list_t usize)) (x : usize) (ret : usize) : + result (alloc_vec_Vec (list_t usize)) + = + let* l = + alloc_vec_Vec_index_mut (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + let* l0 = get_elem_mut_loop_back x l ret in + alloc_vec_Vec_index_mut_back (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) slots + 0 l0 + +(** [loops::get_elem_shared]: decreases clause *) +unfold +let get_elem_shared_loop_decreases (x : usize) (ls : list_t usize) : nat = + admit () + +(** [loops::get_elem_shared]: loop 0: forward function *) +let rec get_elem_shared_loop + (x : usize) (ls : list_t usize) : + Tot (result usize) (decreases (get_elem_shared_loop_decreases x ls)) + = + begin match ls with + | List_Cons y tl -> if y = x then Return y else get_elem_shared_loop x tl + | List_Nil -> Fail Failure + end + +(** [loops::get_elem_shared]: forward function *) +let get_elem_shared + (slots : alloc_vec_Vec (list_t usize)) (x : usize) : result usize = + let* l = + alloc_vec_Vec_index (list_t usize) usize + (core_slice_index_usize_coresliceindexSliceIndexInst (list_t usize)) + slots 0 in + get_elem_shared_loop x l + +(** [loops::id_mut]: forward function *) +let id_mut (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls + +(** [loops::id_mut]: backward function 0 *) +let id_mut_back + (t : Type0) (ls : list_t t) (ret : list_t t) : result (list_t t) = + Return ret + +(** [loops::id_shared]: forward function *) +let id_shared (t : Type0) (ls : list_t t) : result (list_t t) = + Return ls + +(** [loops::list_nth_mut_loop_with_id]: decreases clause *) +unfold +let list_nth_mut_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *) +let rec list_nth_mut_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result t) (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_mut_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_with_id]: forward function *) +let list_nth_mut_loop_with_id + (t : Type0) (ls : list_t t) (i : u32) : result t = + let* ls0 = id_mut t ls in list_nth_mut_loop_with_id_loop t i ls0 + +(** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_with_id_loop_back + (t : Type0) (i : u32) (ls : list_t t) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return (List_Cons ret tl) + else + let* i0 = u32_sub i 1 in + let* tl0 = list_nth_mut_loop_with_id_loop_back t i0 tl ret in + Return (List_Cons x tl0) + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_with_id]: backward function 0 *) +let list_nth_mut_loop_with_id_back + (t : Type0) (ls : list_t t) (i : u32) (ret : t) : result (list_t t) = + let* ls0 = id_mut t ls in + let* l = list_nth_mut_loop_with_id_loop_back t i ls0 ret in + id_mut_back t ls l + +(** [loops::list_nth_shared_loop_with_id]: decreases clause *) +unfold +let list_nth_shared_loop_with_id_loop_decreases (t : Type0) (i : u32) + (ls : list_t t) : nat = + admit () + +(** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *) +let rec list_nth_shared_loop_with_id_loop + (t : Type0) (i : u32) (ls : list_t t) : + Tot (result t) + (decreases (list_nth_shared_loop_with_id_loop_decreases t i ls)) + = + begin match ls with + | List_Cons x tl -> + if i = 0 + then Return x + else let* i0 = u32_sub i 1 in list_nth_shared_loop_with_id_loop t i0 tl + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_with_id]: forward function *) +let list_nth_shared_loop_with_id + (t : Type0) (ls : list_t t) (i : u32) : result t = + let* ls0 = id_shared t ls in list_nth_shared_loop_with_id_loop t i ls0 + +(** [loops::list_nth_mut_loop_pair]: decreases clause *) +unfold +let list_nth_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair]: loop 0: forward function *) +let rec list_nth_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: forward function *) +let list_nth_mut_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_pair_loop_back'a + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_loop_pair_loop_back'a t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: backward function 0 *) +let list_nth_mut_loop_pair_back'a + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_loop_pair_loop_back'a t ls0 ls1 i ret + +(** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *) +let rec list_nth_mut_loop_pair_loop_back'b + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_mut_loop_pair_loop_back'b t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair]: backward function 1 *) +let list_nth_mut_loop_pair_back'b + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_loop_pair_loop_back'b t ls0 ls1 i ret + +(** [loops::list_nth_shared_loop_pair]: decreases clause *) +unfold +let list_nth_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair]: loop 0: forward function *) +let rec list_nth_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else let* i0 = u32_sub i 1 in list_nth_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair]: forward function *) +let list_nth_shared_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in list_nth_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair_merge]: forward function *) +let list_nth_mut_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_mut_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : + Tot (result ((list_t t) & (list_t t))) + (decreases (list_nth_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) + else + let* i0 = u32_sub i 1 in + let* (tl00, tl10) = + list_nth_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00, List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *) +let list_nth_mut_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : (t & t)) : + result ((list_t t) & (list_t t)) + = + list_nth_mut_loop_pair_merge_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_loop_pair_merge_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_loop_pair_merge]: forward function *) +let list_nth_shared_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *) +let rec list_nth_mut_shared_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair]: forward function *) +let list_nth_mut_shared_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *) +let rec list_nth_mut_shared_loop_pair_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = list_nth_mut_shared_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *) +let list_nth_mut_shared_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_mut_shared_loop_pair_merge]: decreases clause *) +unfold +let list_nth_mut_shared_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_mut_shared_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *) +let list_nth_mut_shared_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_mut_shared_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_mut_shared_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl0) + else + let* i0 = u32_sub i 1 in + let* tl00 = + list_nth_mut_shared_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x0 tl00) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *) +let list_nth_mut_shared_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_mut_shared_loop_pair_merge_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_mut_loop_pair]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_loop_decreases (t : Type0) (ls0 : list_t t) + (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *) +let rec list_nth_shared_mut_loop_pair_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair]: forward function *) +let list_nth_shared_mut_loop_pair + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *) +let rec list_nth_shared_mut_loop_pair_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = list_nth_shared_mut_loop_pair_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *) +let list_nth_shared_mut_loop_pair_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_loop_back t ls0 ls1 i ret + +(** [loops::list_nth_shared_mut_loop_pair_merge]: decreases clause *) +unfold +let list_nth_shared_mut_loop_pair_merge_loop_decreases (t : Type0) + (ls0 : list_t t) (ls1 : list_t t) (i : u32) : nat = + admit () + +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *) +let rec list_nth_shared_mut_loop_pair_merge_loop + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : + Tot (result (t & t)) + (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (x0, x1) + else + let* i0 = u32_sub i 1 in + list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i0 + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *) +let list_nth_shared_mut_loop_pair_merge + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) : result (t & t) = + list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i + +(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *) +let rec list_nth_shared_mut_loop_pair_merge_loop_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + Tot (result (list_t t)) + (decreases (list_nth_shared_mut_loop_pair_merge_loop_decreases t ls0 ls1 i)) + = + begin match ls0 with + | List_Cons x0 tl0 -> + begin match ls1 with + | List_Cons x1 tl1 -> + if i = 0 + then Return (List_Cons ret tl1) + else + let* i0 = u32_sub i 1 in + let* tl10 = + list_nth_shared_mut_loop_pair_merge_loop_back t tl0 tl1 i0 ret in + Return (List_Cons x1 tl10) + | List_Nil -> Fail Failure + end + | List_Nil -> Fail Failure + end + +(** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *) +let list_nth_shared_mut_loop_pair_merge_back + (t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) (ret : t) : + result (list_t t) + = + list_nth_shared_mut_loop_pair_merge_loop_back t ls0 ls1 i ret + diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean index 277b63d9..20f02e97 100644 --- a/tests/lean/Array.lean +++ b/tests/lean/Array.lean @@ -1 +1,435 @@ -import Array.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [array] +import Base +open Primitives + +namespace array + +/- [array::AB] -/ +inductive AB := +| A : AB +| B : AB + +/- [array::incr]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def incr (x : U32) : Result U32 := + x + 1#u32 + +/- [array::array_to_shared_slice_]: forward function -/ +def array_to_shared_slice_ + (T : Type) (s : Array T 32#usize) : Result (Slice T) := + Array.to_slice T 32#usize s + +/- [array::array_to_mut_slice_]: forward function -/ +def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) := + Array.to_slice T 32#usize s + +/- [array::array_to_mut_slice_]: backward function 0 -/ +def array_to_mut_slice__back + (T : Type) (s : Array T 32#usize) (ret0 : Slice T) : + Result (Array T 32#usize) + := + Array.from_slice T 32#usize s ret0 + +/- [array::array_len]: forward function -/ +def array_len (T : Type) (s : Array T 32#usize) : Result Usize := + do + let s0 ← Array.to_slice T 32#usize s + let i := Slice.len T s0 + Result.ret i + +/- [array::shared_array_len]: forward function -/ +def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := + do + let s0 ← Array.to_slice T 32#usize s + let i := Slice.len T s0 + Result.ret i + +/- [array::shared_slice_len]: forward function -/ +def shared_slice_len (T : Type) (s : Slice T) : Result Usize := + let i := Slice.len T s + Result.ret i + +/- [array::index_array_shared]: forward function -/ +def index_array_shared + (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := + Array.index_usize T 32#usize s i + +/- [array::index_array_u32]: forward function -/ +def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := + Array.index_usize U32 32#usize s i + +/- [array::index_array_copy]: forward function -/ +def index_array_copy (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize + +/- [array::index_mut_array]: forward function -/ +def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := + Array.index_usize T 32#usize s i + +/- [array::index_mut_array]: backward function 0 -/ +def index_mut_array_back + (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) : + Result (Array T 32#usize) + := + Array.update_usize T 32#usize s i ret0 + +/- [array::index_slice]: forward function -/ +def index_slice (T : Type) (s : Slice T) (i : Usize) : Result T := + Slice.index_usize T s i + +/- [array::index_mut_slice]: forward function -/ +def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T := + Slice.index_usize T s i + +/- [array::index_mut_slice]: backward function 0 -/ +def index_mut_slice_back + (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) := + Slice.update_usize T s i ret0 + +/- [array::slice_subslice_shared_]: forward function -/ +def slice_subslice_shared_ + (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := + core.slice.index.Slice.index U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } + +/- [array::slice_subslice_mut_]: forward function -/ +def slice_subslice_mut_ + (x : Slice U32) (y : Usize) (z : Usize) : Result (Slice U32) := + core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } + +/- [array::slice_subslice_mut_]: backward function 0 -/ +def slice_subslice_mut__back + (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) : + Result (Slice U32) + := + core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32) x + { start := y, end_ := z } ret0 + +/- [array::array_to_slice_shared_]: forward function -/ +def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := + Array.to_slice U32 32#usize x + +/- [array::array_to_slice_mut_]: forward function -/ +def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) := + Array.to_slice U32 32#usize x + +/- [array::array_to_slice_mut_]: backward function 0 -/ +def array_to_slice_mut__back + (x : Array U32 32#usize) (ret0 : Slice U32) : Result (Array U32 32#usize) := + Array.from_slice U32 32#usize x ret0 + +/- [array::array_subslice_shared_]: forward function -/ +def array_subslice_shared_ + (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::array_subslice_mut_]: forward function -/ +def array_subslice_mut_ + (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::array_subslice_mut_]: backward function 0 -/ +def array_subslice_mut__back + (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) : + Result (Array U32 32#usize) + := + core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } ret0 + +/- [array::index_slice_0]: forward function -/ +def index_slice_0 (T : Type) (s : Slice T) : Result T := + Slice.index_usize T s 0#usize + +/- [array::index_array_0]: forward function -/ +def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := + Array.index_usize T 32#usize s 0#usize + +/- [array::index_index_array]: forward function -/ +def index_index_array + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + Result U32 + := + do + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + Array.index_usize U32 32#usize a j + +/- [array::update_update_array]: forward function -/ +def update_update_array + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + Result Unit + := + do + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + let a0 ← Array.update_usize U32 32#usize a j 0#u32 + let _ ← Array.update_usize (Array U32 32#usize) 32#usize s i a0 + Result.ret () + +/- [array::array_local_deep_copy]: forward function -/ +def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := + Result.ret () + +/- [array::take_array]: forward function -/ +def take_array (a : Array U32 2#usize) : Result Unit := + Result.ret () + +/- [array::take_array_borrow]: forward function -/ +def take_array_borrow (a : Array U32 2#usize) : Result Unit := + Result.ret () + +/- [array::take_slice]: forward function -/ +def take_slice (s : Slice U32) : Result Unit := + Result.ret () + +/- [array::take_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def take_mut_slice (s : Slice U32) : Result (Slice U32) := + Result.ret s + +/- [array::take_all]: forward function -/ +def take_all : Result Unit := + do + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_slice s + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s1 ← take_mut_slice s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + Result.ret () + +/- [array::index_array]: forward function -/ +def index_array (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::index_array_borrow]: forward function -/ +def index_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::index_slice_u32_0]: forward function -/ +def index_slice_u32_0 (x : Slice U32) : Result U32 := + Slice.index_usize U32 x 0#usize + +/- [array::index_mut_slice_u32_0]: forward function -/ +def index_mut_slice_u32_0 (x : Slice U32) : Result U32 := + Slice.index_usize U32 x 0#usize + +/- [array::index_mut_slice_u32_0]: backward function 0 -/ +def index_mut_slice_u32_0_back (x : Slice U32) : Result (Slice U32) := + do + let _ ← Slice.index_usize U32 x 0#usize + Result.ret x + +/- [array::index_all]: forward function -/ +def index_all : Result U32 := + do + let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i0 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i1 ← i + i0 + let i2 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i3 ← i1 + i2 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i4 ← index_slice_u32_0 s + let i5 ← i3 + i4 + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i6 ← index_mut_slice_u32_0 s0 + let i7 ← i5 + i6 + let s1 ← index_mut_slice_u32_0_back s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + Result.ret i7 + +/- [array::update_array]: forward function -/ +def update_array (x : Array U32 2#usize) : Result Unit := + do + let _ ← Array.update_usize U32 2#usize x 0#usize 1#u32 + Result.ret () + +/- [array::update_array_mut_borrow]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def update_array_mut_borrow + (x : Array U32 2#usize) : Result (Array U32 2#usize) := + Array.update_usize U32 2#usize x 0#usize 1#u32 + +/- [array::update_mut_slice]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def update_mut_slice (x : Slice U32) : Result (Slice U32) := + Slice.update_usize U32 x 0#usize 1#u32 + +/- [array::update_all]: forward function -/ +def update_all : Result Unit := + do + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← Array.to_slice U32 2#usize x + let s0 ← update_mut_slice s + let _ ← Array.from_slice U32 2#usize x s0 + Result.ret () + +/- [array::range_all]: forward function -/ +def range_all : Result Unit := + do + let s ← + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 + (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32)) + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } + let s0 ← update_mut_slice s + let _ ← + core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 4#usize + (core.slice.index.Slice.coreopsindexIndexMutInst U32 + (core.ops.range.Range Usize) + (core.slice.index.Range.coresliceindexSliceIndexInst U32)) + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } s0 + Result.ret () + +/- [array::deref_array_borrow]: forward function -/ +def deref_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::deref_array_mut_borrow]: forward function -/ +def deref_array_mut_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize + +/- [array::deref_array_mut_borrow]: backward function 0 -/ +def deref_array_mut_borrow_back + (x : Array U32 2#usize) : Result (Array U32 2#usize) := + do + let _ ← Array.index_usize U32 2#usize x 0#usize + Result.ret x + +/- [array::take_array_t]: forward function -/ +def take_array_t (a : Array AB 2#usize) : Result Unit := + Result.ret () + +/- [array::non_copyable_array]: forward function -/ +def non_copyable_array : Result Unit := + do + let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) + Result.ret () + +/- [array::sum]: loop 0: forward function -/ +divergent def sum_loop (s : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := + let i0 := Slice.len U32 s + if i < i0 + then + do + let i1 ← Slice.index_usize U32 s i + let sum1 ← sum0 + i1 + let i2 ← i + 1#usize + sum_loop s sum1 i2 + else Result.ret sum0 + +/- [array::sum]: forward function -/ +def sum (s : Slice U32) : Result U32 := + sum_loop s 0#u32 0#usize + +/- [array::sum2]: loop 0: forward function -/ +divergent def sum2_loop + (s : Slice U32) (s2 : Slice U32) (sum0 : U32) (i : Usize) : Result U32 := + let i0 := Slice.len U32 s + if i < i0 + then + do + let i1 ← Slice.index_usize U32 s i + let i2 ← Slice.index_usize U32 s2 i + let i3 ← i1 + i2 + let sum1 ← sum0 + i3 + let i4 ← i + 1#usize + sum2_loop s s2 sum1 i4 + else Result.ret sum0 + +/- [array::sum2]: forward function -/ +def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := + let i := Slice.len U32 s + let i0 := Slice.len U32 s2 + if not (i = i0) + then Result.fail Error.panic + else sum2_loop s s2 0#u32 0#usize + +/- [array::f0]: forward function -/ +def f0 : Result Unit := + do + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s0 ← Slice.update_usize U32 s 0#usize 1#u32 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) s0 + Result.ret () + +/- [array::f1]: forward function -/ +def f1 : Result Unit := + do + let _ ← + Array.update_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize 1#u32 + Result.ret () + +/- [array::f2]: forward function -/ +def f2 (i : U32) : Result Unit := + Result.ret () + +/- [array::f4]: forward function -/ +def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (core.slice.index.Slice.coreopsindexIndexInst U32 (core.ops.range.Range + Usize) (core.slice.index.Range.coresliceindexSliceIndexInst U32)) x + { start := y, end_ := z } + +/- [array::f3]: forward function -/ +def f3 : Result U32 := + do + let i ← + Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize + let _ ← f2 i + let b := Array.repeat U32 32#usize 0#u32 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s0 ← f4 b 16#usize 18#usize + sum2 s s0 + +/- [array::SZ] -/ +def sz_body : Result Usize := Result.ret 32#usize +def sz_c : Usize := eval_global sz_body (by simp) + +/- [array::f5]: forward function -/ +def f5 (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize + +/- [array::ite]: forward function -/ +def ite : Result Unit := + do + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s0 ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s1 ← index_mut_slice_u32_0_back s0 + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s1 + let s2 ← index_mut_slice_u32_0_back s + let _ ← + Array.from_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) s2 + Result.ret () + +end array diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 60c73776..c6360338 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -1 +1,629 @@ -import Loops.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [loops] +import Base +open Primitives + +namespace loops + +/- [loops::sum]: loop 0: forward function -/ +divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max + then do + let s0 ← s + i + let i0 ← i + 1#u32 + sum_loop max i0 s0 + else s * 2#u32 + +/- [loops::sum]: forward function -/ +def sum (max : U32) : Result U32 := + sum_loop max 0#u32 0#u32 + +/- [loops::sum_with_mut_borrows]: loop 0: forward function -/ +divergent def sum_with_mut_borrows_loop + (max : U32) (mi : U32) (ms : U32) : Result U32 := + if mi < max + then + do + let ms0 ← ms + mi + let mi0 ← mi + 1#u32 + sum_with_mut_borrows_loop max mi0 ms0 + else ms * 2#u32 + +/- [loops::sum_with_mut_borrows]: forward function -/ +def sum_with_mut_borrows (max : U32) : Result U32 := + sum_with_mut_borrows_loop max 0#u32 0#u32 + +/- [loops::sum_with_shared_borrows]: loop 0: forward function -/ +divergent def sum_with_shared_borrows_loop + (max : U32) (i : U32) (s : U32) : Result U32 := + if i < max + then + do + let i0 ← i + 1#u32 + let s0 ← s + i0 + sum_with_shared_borrows_loop max i0 s0 + else s * 2#u32 + +/- [loops::sum_with_shared_borrows]: forward function -/ +def sum_with_shared_borrows (max : U32) : Result U32 := + sum_with_shared_borrows_loop max 0#u32 0#u32 + +/- [loops::clear]: loop 0: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +divergent def clear_loop + (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := + let i0 := alloc.vec.Vec.len U32 v + if i < i0 + then + do + let i1 ← i + 1#usize + let v0 ← + alloc.vec.Vec.index_mut_back U32 Usize + (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32 + clear_loop v0 i1 + else Result.ret v + +/- [loops::clear]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := + clear_loop v 0#usize + +/- [loops::List] -/ +inductive List (T : Type) := +| Cons : T → List T → List T +| Nil : List T + +/- [loops::list_mem]: loop 0: forward function -/ +divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := + match ls with + | List.Cons y tl => if y = x + then Result.ret true + else list_mem_loop x tl + | List.Nil => Result.ret false + +/- [loops::list_mem]: forward function -/ +def list_mem (x : U32) (ls : List U32) : Result Bool := + list_mem_loop x ls + +/- [loops::list_nth_mut_loop]: loop 0: forward function -/ +divergent def list_nth_mut_loop_loop + (T : Type) (ls : List T) (i : U32) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_loop T tl i0 + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop]: forward function -/ +def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := + list_nth_mut_loop_loop T ls i + +/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_loop_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl) + else + do + let i0 ← i - 1#u32 + let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop]: backward function 0 -/ +def list_nth_mut_loop_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + list_nth_mut_loop_loop_back T ls i ret0 + +/- [loops::list_nth_shared_loop]: loop 0: forward function -/ +divergent def list_nth_shared_loop_loop + (T : Type) (ls : List T) (i : U32) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_loop T tl i0 + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop]: forward function -/ +def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := + list_nth_shared_loop_loop T ls i + +/- [loops::get_elem_mut]: loop 0: forward function -/ +divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := + match ls with + | List.Cons y tl => if y = x + then Result.ret y + else get_elem_mut_loop x tl + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_mut]: forward function -/ +def get_elem_mut + (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := + do + let l ← + alloc.vec.Vec.index_mut (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + get_elem_mut_loop x l + +/- [loops::get_elem_mut]: loop 0: backward function 0 -/ +divergent def get_elem_mut_loop_back + (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := + match ls with + | List.Cons y tl => + if y = x + then Result.ret (List.Cons ret0 tl) + else + do + let tl0 ← get_elem_mut_loop_back x tl ret0 + Result.ret (List.Cons y tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_mut]: backward function 0 -/ +def get_elem_mut_back + (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) : + Result (alloc.vec.Vec (List Usize)) + := + do + let l ← + alloc.vec.Vec.index_mut (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + let l0 ← get_elem_mut_loop_back x l ret0 + alloc.vec.Vec.index_mut_back (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots + 0#usize l0 + +/- [loops::get_elem_shared]: loop 0: forward function -/ +divergent def get_elem_shared_loop + (x : Usize) (ls : List Usize) : Result Usize := + match ls with + | List.Cons y tl => if y = x + then Result.ret y + else get_elem_shared_loop x tl + | List.Nil => Result.fail Error.panic + +/- [loops::get_elem_shared]: forward function -/ +def get_elem_shared + (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := + do + let l ← + alloc.vec.Vec.index (List Usize) Usize + (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) + slots 0#usize + get_elem_shared_loop x l + +/- [loops::id_mut]: forward function -/ +def id_mut (T : Type) (ls : List T) : Result (List T) := + Result.ret ls + +/- [loops::id_mut]: backward function 0 -/ +def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := + Result.ret ret0 + +/- [loops::id_shared]: forward function -/ +def id_shared (T : Type) (ls : List T) : Result (List T) := + Result.ret ls + +/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/ +divergent def list_nth_mut_loop_with_id_loop + (T : Type) (i : U32) (ls : List T) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_with_id_loop T i0 tl + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_with_id]: forward function -/ +def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := + do + let ls0 ← id_mut T ls + list_nth_mut_loop_with_id_loop T i ls0 + +/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_with_id_loop_back + (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl) + else + do + let i0 ← i - 1#u32 + let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 + Result.ret (List.Cons x tl0) + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/ +def list_nth_mut_loop_with_id_back + (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + do + let ls0 ← id_mut T ls + let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0 + id_mut_back T ls l + +/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/ +divergent def list_nth_shared_loop_with_id_loop + (T : Type) (i : U32) (ls : List T) : Result T := + match ls with + | List.Cons x tl => + if i = 0#u32 + then Result.ret x + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_with_id_loop T i0 tl + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_with_id]: forward function -/ +def list_nth_shared_loop_with_id + (T : Type) (ls : List T) (i : U32) : Result T := + do + let ls0 ← id_shared T ls + list_nth_shared_loop_with_id_loop T i ls0 + +/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/ +divergent def list_nth_mut_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else do + let i0 ← i - 1#u32 + list_nth_mut_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: forward function -/ +def list_nth_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_pair_loop_back'a + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: backward function 0 -/ +def list_nth_mut_loop_pair_back'a + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 + +/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/ +divergent def list_nth_mut_loop_pair_loop_back'b + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair]: backward function 1 -/ +def list_nth_mut_loop_pair_back'b + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/ +divergent def list_nth_shared_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else do + let i0 ← i - 1#u32 + list_nth_shared_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_pair]: forward function -/ +def list_nth_shared_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_mut_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair_merge]: forward function -/ +def list_nth_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_mut_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then let (t, t0) := ret0 + Result.ret (List.Cons t tl0, List.Cons t0 tl1) + else + do + let i0 ← i - 1#u32 + let (tl00, tl10) ← + list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/ +def list_nth_mut_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + Result ((List T) × (List T)) + := + list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_shared_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_loop_pair_merge]: forward function -/ +def list_nth_shared_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/ +divergent def list_nth_mut_shared_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair]: forward function -/ +def list_nth_mut_shared_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_shared_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/ +divergent def list_nth_mut_shared_loop_pair_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← + list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/ +def list_nth_mut_shared_loop_pair_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_mut_shared_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/ +def list_nth_mut_shared_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_mut_shared_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl0) + else + do + let i0 ← i - 1#u32 + let tl00 ← + list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x0 tl00) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/ +def list_nth_mut_shared_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/ +divergent def list_nth_shared_mut_loop_pair_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair]: forward function -/ +def list_nth_shared_mut_loop_pair + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_mut_loop_pair_loop T ls0 ls1 i + +/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/ +divergent def list_nth_shared_mut_loop_pair_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← + list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/ +def list_nth_shared_mut_loop_pair_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 + +/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/ +divergent def list_nth_shared_mut_loop_pair_merge_loop + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (x0, x1) + else + do + let i0 ← i - 1#u32 + list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/ +def list_nth_shared_mut_loop_pair_merge + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := + list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i + +/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/ +divergent def list_nth_shared_mut_loop_pair_merge_loop_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + match ls0 with + | List.Cons x0 tl0 => + match ls1 with + | List.Cons x1 tl1 => + if i = 0#u32 + then Result.ret (List.Cons ret0 tl1) + else + do + let i0 ← i - 1#u32 + let tl10 ← + list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + Result.ret (List.Cons x1 tl10) + | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail Error.panic + +/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/ +def list_nth_shared_mut_loop_pair_merge_back + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + Result (List T) + := + list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + +end loops diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean deleted file mode 100644 index f9c7569e..00000000 --- a/tests/lean/Loops/Funs.lean +++ /dev/null @@ -1,625 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [loops]: function definitions -import Base -import Loops.Types -open Primitives - -namespace loops - -/- [loops::sum]: loop 0: forward function -/ -divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := - if i < max - then do - let s0 ← s + i - let i0 ← i + 1#u32 - sum_loop max i0 s0 - else s * 2#u32 - -/- [loops::sum]: forward function -/ -def sum (max : U32) : Result U32 := - sum_loop max 0#u32 0#u32 - -/- [loops::sum_with_mut_borrows]: loop 0: forward function -/ -divergent def sum_with_mut_borrows_loop - (max : U32) (mi : U32) (ms : U32) : Result U32 := - if mi < max - then - do - let ms0 ← ms + mi - let mi0 ← mi + 1#u32 - sum_with_mut_borrows_loop max mi0 ms0 - else ms * 2#u32 - -/- [loops::sum_with_mut_borrows]: forward function -/ -def sum_with_mut_borrows (max : U32) : Result U32 := - sum_with_mut_borrows_loop max 0#u32 0#u32 - -/- [loops::sum_with_shared_borrows]: loop 0: forward function -/ -divergent def sum_with_shared_borrows_loop - (max : U32) (i : U32) (s : U32) : Result U32 := - if i < max - then - do - let i0 ← i + 1#u32 - let s0 ← s + i0 - sum_with_shared_borrows_loop max i0 s0 - else s * 2#u32 - -/- [loops::sum_with_shared_borrows]: forward function -/ -def sum_with_shared_borrows (max : U32) : Result U32 := - sum_with_shared_borrows_loop max 0#u32 0#u32 - -/- [loops::clear]: loop 0: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -divergent def clear_loop - (v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) := - let i0 := alloc.vec.Vec.len U32 v - if i < i0 - then - do - let i1 ← i + 1#usize - let v0 ← - alloc.vec.Vec.index_mut_back U32 Usize - (core.slice.index.usize.coresliceindexSliceIndexInst U32) v i 0#u32 - clear_loop v0 i1 - else Result.ret v - -/- [loops::clear]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := - clear_loop v 0#usize - -/- [loops::list_mem]: loop 0: forward function -/ -divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool := - match ls with - | List.Cons y tl => if y = x - then Result.ret true - else list_mem_loop x tl - | List.Nil => Result.ret false - -/- [loops::list_mem]: forward function -/ -def list_mem (x : U32) (ls : List U32) : Result Bool := - list_mem_loop x ls - -/- [loops::list_nth_mut_loop]: loop 0: forward function -/ -divergent def list_nth_mut_loop_loop - (T : Type) (ls : List T) (i : U32) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop]: forward function -/ -def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := - list_nth_mut_loop_loop T ls i - -/- [loops::list_nth_mut_loop]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_loop_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl) - else - do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 - Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop]: backward function 0 -/ -def list_nth_mut_loop_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - list_nth_mut_loop_loop_back T ls i ret0 - -/- [loops::list_nth_shared_loop]: loop 0: forward function -/ -divergent def list_nth_shared_loop_loop - (T : Type) (ls : List T) (i : U32) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop]: forward function -/ -def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T := - list_nth_shared_loop_loop T ls i - -/- [loops::get_elem_mut]: loop 0: forward function -/ -divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := - match ls with - | List.Cons y tl => if y = x - then Result.ret y - else get_elem_mut_loop x tl - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_mut]: forward function -/ -def get_elem_mut - (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := - do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - get_elem_mut_loop x l - -/- [loops::get_elem_mut]: loop 0: backward function 0 -/ -divergent def get_elem_mut_loop_back - (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := - match ls with - | List.Cons y tl => - if y = x - then Result.ret (List.Cons ret0 tl) - else - do - let tl0 ← get_elem_mut_loop_back x tl ret0 - Result.ret (List.Cons y tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_mut]: backward function 0 -/ -def get_elem_mut_back - (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) : - Result (alloc.vec.Vec (List Usize)) - := - do - let l ← - alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - let l0 ← get_elem_mut_loop_back x l ret0 - alloc.vec.Vec.index_mut_back (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) slots - 0#usize l0 - -/- [loops::get_elem_shared]: loop 0: forward function -/ -divergent def get_elem_shared_loop - (x : Usize) (ls : List Usize) : Result Usize := - match ls with - | List.Cons y tl => if y = x - then Result.ret y - else get_elem_shared_loop x tl - | List.Nil => Result.fail Error.panic - -/- [loops::get_elem_shared]: forward function -/ -def get_elem_shared - (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize := - do - let l ← - alloc.vec.Vec.index (List Usize) Usize - (core.slice.index.usize.coresliceindexSliceIndexInst (List Usize)) - slots 0#usize - get_elem_shared_loop x l - -/- [loops::id_mut]: forward function -/ -def id_mut (T : Type) (ls : List T) : Result (List T) := - Result.ret ls - -/- [loops::id_mut]: backward function 0 -/ -def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := - Result.ret ret0 - -/- [loops::id_shared]: forward function -/ -def id_shared (T : Type) (ls : List T) : Result (List T) := - Result.ret ls - -/- [loops::list_nth_mut_loop_with_id]: loop 0: forward function -/ -divergent def list_nth_mut_loop_with_id_loop - (T : Type) (i : U32) (ls : List T) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_with_id]: forward function -/ -def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := - do - let ls0 ← id_mut T ls - list_nth_mut_loop_with_id_loop T i ls0 - -/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_with_id_loop_back - (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl) - else - do - let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 - Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_with_id]: backward function 0 -/ -def list_nth_mut_loop_with_id_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := - do - let ls0 ← id_mut T ls - let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0 - id_mut_back T ls l - -/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function -/ -divergent def list_nth_shared_loop_with_id_loop - (T : Type) (i : U32) (ls : List T) : Result T := - match ls with - | List.Cons x tl => - if i = 0#u32 - then Result.ret x - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_with_id]: forward function -/ -def list_nth_shared_loop_with_id - (T : Type) (ls : List T) (i : U32) : Result T := - do - let ls0 ← id_shared T ls - list_nth_shared_loop_with_id_loop T i ls0 - -/- [loops::list_nth_mut_loop_pair]: loop 0: forward function -/ -divergent def list_nth_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: forward function -/ -def list_nth_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_pair_loop_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: backward function 0 -/ -def list_nth_mut_loop_pair_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 - -/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 -/ -divergent def list_nth_mut_loop_pair_loop_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair]: backward function 1 -/ -def list_nth_mut_loop_pair_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_loop_pair]: loop 0: forward function -/ -divergent def list_nth_shared_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_pair]: forward function -/ -def list_nth_shared_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair_merge]: forward function -/ -def list_nth_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : - Result ((List T) × (List T)) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then let (t, t0) := ret0 - Result.ret (List.Cons t tl0, List.Cons t0 tl1) - else - do - let i0 ← i - 1#u32 - let (tl00, tl10) ← - list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_loop_pair_merge]: backward function 0 -/ -def list_nth_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : - Result ((List T) × (List T)) - := - list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_shared_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_loop_pair_merge]: forward function -/ -def list_nth_shared_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function -/ -divergent def list_nth_mut_shared_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair]: forward function -/ -def list_nth_mut_shared_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 -/ -divergent def list_nth_mut_shared_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair]: backward function 0 -/ -def list_nth_mut_shared_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_mut_shared_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function -/ -def list_nth_mut_shared_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_mut_shared_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) - else - do - let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 -/ -def list_nth_mut_shared_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function -/ -divergent def list_nth_shared_mut_loop_pair_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair]: forward function -/ -def list_nth_shared_mut_loop_pair - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 -/ -divergent def list_nth_shared_mut_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair]: backward function 1 -/ -def list_nth_shared_mut_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 - -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function -/ -divergent def list_nth_shared_mut_loop_pair_merge_loop - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (x0, x1) - else - do - let i0 ← i - 1#u32 - list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0 - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function -/ -def list_nth_shared_mut_loop_pair_merge - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) := - list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i - -/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 -/ -divergent def list_nth_shared_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - match ls0 with - | List.Cons x0 tl0 => - match ls1 with - | List.Cons x1 tl1 => - if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) - else - do - let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 - Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic - -/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 -/ -def list_nth_shared_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : - Result (List T) - := - list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 - -end loops diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean deleted file mode 100644 index 018af901..00000000 --- a/tests/lean/Loops/Types.lean +++ /dev/null @@ -1,13 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [loops]: type definitions -import Base -open Primitives - -namespace loops - -/- [loops::List] -/ -inductive List (T : Type) := -| Cons : T → List T → List T -| Nil : List T - -end loops diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 5e812e95..94ae0bb0 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -1 +1,410 @@ -import Traits.Funs +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [traits] +import Base +open Primitives + +namespace traits + +/- Trait declaration: [traits::BoolTrait] -/ +structure BoolTrait (Self : Type) where + get_bool : Self → Result Bool + +/- [traits::Bool::{0}::get_bool]: forward function -/ +def Bool.get_bool (self : Bool) : Result Bool := + Result.ret self + +/- Trait implementation: [traits::Bool::{0}] -/ +def Bool.BoolTraitInst : BoolTrait Bool := { + get_bool := Bool.get_bool +} + +/- [traits::BoolTrait::ret_true]: forward function -/ +def BoolTrait.ret_true + {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := + Result.ret true + +/- [traits::test_bool_trait_bool]: forward function -/ +def test_bool_trait_bool (x : Bool) : Result Bool := + do + let b ← Bool.get_bool x + if b + then BoolTrait.ret_true Bool.BoolTraitInst x + else Result.ret false + +/- [traits::Option::{1}::get_bool]: forward function -/ +def Option.get_bool (T : Type) (self : Option T) : Result Bool := + match self with + | none => Result.ret false + | some t => Result.ret true + +/- Trait implementation: [traits::Option::{1}] -/ +def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := { + get_bool := Option.get_bool T +} + +/- [traits::test_bool_trait_option]: forward function -/ +def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := + do + let b ← Option.get_bool T x + if b + then BoolTrait.ret_true (Option.BoolTraitInst T) x + else Result.ret false + +/- [traits::test_bool_trait]: forward function -/ +def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool := + inst.get_bool x + +/- Trait declaration: [traits::ToU64] -/ +structure ToU64 (Self : Type) where + to_u64 : Self → Result U64 + +/- [traits::u64::{2}::to_u64]: forward function -/ +def u64.to_u64 (self : U64) : Result U64 := + Result.ret self + +/- Trait implementation: [traits::u64::{2}] -/ +def u64.ToU64Inst : ToU64 U64 := { + to_u64 := u64.to_u64 +} + +/- [traits::Tuple2::{3}::to_u64]: forward function -/ +def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 := + do + let (t, t0) := self + let i ← inst.to_u64 t + let i0 ← inst.to_u64 t0 + i + i0 + +/- Trait implementation: [traits::Tuple2::{3}] -/ +def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := { + to_u64 := Tuple2.to_u64 A inst +} + +/- [traits::f]: forward function -/ +def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 := + Tuple2.to_u64 T inst x + +/- [traits::g]: forward function -/ +def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 := + inst.to_u64 x + +/- [traits::h0]: forward function -/ +def h0 (x : U64) : Result U64 := + u64.to_u64 x + +/- [traits::Wrapper] -/ +structure Wrapper (T : Type) where + x : T + +/- [traits::Wrapper::{4}::to_u64]: forward function -/ +def Wrapper.to_u64 + (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 := + inst.to_u64 self.x + +/- Trait implementation: [traits::Wrapper::{4}] -/ +def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := { + to_u64 := Wrapper.to_u64 T inst +} + +/- [traits::h1]: forward function -/ +def h1 (x : Wrapper U64) : Result U64 := + Wrapper.to_u64 U64 u64.ToU64Inst x + +/- [traits::h2]: forward function -/ +def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 := + Wrapper.to_u64 T inst x + +/- Trait declaration: [traits::ToType] -/ +structure ToType (Self T : Type) where + to_type : Self → Result T + +/- [traits::u64::{5}::to_type]: forward function -/ +def u64.to_type (self : U64) : Result Bool := + Result.ret (self > 0#u64) + +/- Trait implementation: [traits::u64::{5}] -/ +def u64.ToTypeInst : ToType U64 Bool := { + to_type := u64.to_type +} + +/- Trait declaration: [traits::OfType] -/ +structure OfType (Self : Type) where + of_type : forall (T : Type) (inst : ToType T Self), T → Result Self + +/- [traits::h3]: forward function -/ +def h3 + (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) : + Result T1 + := + inst.of_type T2 inst0 y + +/- Trait declaration: [traits::OfTypeBis] -/ +structure OfTypeBis (Self T : Type) where + parent_clause_0 : ToType T Self + of_type : T → Result Self + +/- [traits::h4]: forward function -/ +def h4 + (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) : + Result T1 + := + inst.of_type y + +/- [traits::TestType] -/ +structure TestType (T : Type) where + _0 : T + +/- [traits::TestType::{6}::test::TestType1] -/ +structure TestType.test.TestType1 where + _0 : U64 + +/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/ +structure TestType.test.TestTrait (Self : Type) where + test : Self → Result Bool + +/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/ +def TestType.test.TestType1.test + (self : TestType.test.TestType1) : Result Bool := + Result.ret (self._0 > 1#u64) + +/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/ +def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait + TestType.test.TestType1 := { + test := TestType.test.TestType1.test +} + +/- [traits::TestType::{6}::test]: forward function -/ +def TestType.test + (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := + do + let x0 ← inst.to_u64 x + if x0 > 0#u64 + then TestType.test.TestType1.test { _0 := 0#u64 } + else Result.ret false + +/- [traits::BoolWrapper] -/ +structure BoolWrapper where + _0 : Bool + +/- [traits::BoolWrapper::{7}::to_type]: forward function -/ +def BoolWrapper.to_type + (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T := + inst.to_type self._0 + +/- Trait implementation: [traits::BoolWrapper::{7}] -/ +def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType + BoolWrapper T := { + to_type := BoolWrapper.to_type T inst +} + +/- [traits::WithConstTy::LEN2] -/ +def with_const_ty_len2_body : Result Usize := Result.ret 32#usize +def with_const_ty_len2_c : Usize := + eval_global with_const_ty_len2_body (by simp) + +/- Trait declaration: [traits::WithConstTy] -/ +structure WithConstTy (Self : Type) (LEN : Usize) where + LEN1 : Usize + LEN2 : Usize + V : Type + W : Type + W_clause_0 : ToU64 W + f : W → Array U8 LEN → Result W + +/- [traits::Bool::{8}::LEN1] -/ +def bool_len1_body : Result Usize := Result.ret 12#usize +def bool_len1_c : Usize := eval_global bool_len1_body (by simp) + +/- [traits::Bool::{8}::f]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) -/ +def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 := + Result.ret i + +/- Trait implementation: [traits::Bool::{8}] -/ +def Bool.WithConstTyInst : WithConstTy Bool 32#usize := { + LEN1 := bool_len1_c + LEN2 := with_const_ty_len2_c + V := U8 + W := U64 + W_clause_0 := u64.ToU64Inst + f := Bool.f +} + +/- [traits::use_with_const_ty1]: forward function -/ +def use_with_const_ty1 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize := + let i := inst.LEN1 + Result.ret i + +/- [traits::use_with_const_ty2]: forward function -/ +def use_with_const_ty2 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) : + Result Unit + := + Result.ret () + +/- [traits::use_with_const_ty3]: forward function -/ +def use_with_const_ty3 + (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) : + Result U64 + := + inst.W_clause_0.to_u64 x + +/- [traits::test_where1]: forward function -/ +def test_where1 (T : Type) (_x : T) : Result Unit := + Result.ret () + +/- [traits::test_where2]: forward function -/ +def test_where2 + (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := + Result.ret () + +/- [alloc::string::String] -/ +axiom alloc.string.String : Type + +/- Trait declaration: [traits::ParentTrait0] -/ +structure ParentTrait0 (Self : Type) where + W : Type + get_name : Self → Result alloc.string.String + get_w : Self → Result W + +/- Trait declaration: [traits::ParentTrait1] -/ +structure ParentTrait1 (Self : Type) where + +/- Trait declaration: [traits::ChildTrait] -/ +structure ChildTrait (Self : Type) where + parent_clause_0 : ParentTrait0 Self + parent_clause_1 : ParentTrait1 Self + +/- [traits::test_child_trait1]: forward function -/ +def test_child_trait1 + (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String := + inst.parent_clause_0.get_name x + +/- [traits::test_child_trait2]: forward function -/ +def test_child_trait2 + (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W := + inst.parent_clause_0.get_w x + +/- [traits::order1]: forward function -/ +def order1 + (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) : + Result Unit + := + Result.ret () + +/- Trait declaration: [traits::ChildTrait1] -/ +structure ChildTrait1 (Self : Type) where + parent_clause_0 : ParentTrait1 Self + +/- Trait implementation: [traits::usize::{9}] -/ +def usize.ParentTrait1Inst : ParentTrait1 Usize := { +} + +/- Trait implementation: [traits::usize::{10}] -/ +def usize.ChildTrait1Inst : ChildTrait1 Usize := { + parent_clause_0 := usize.ParentTrait1Inst +} + +/- Trait declaration: [traits::Iterator] -/ +structure Iterator (Self : Type) where + Item : Type + +/- Trait declaration: [traits::IntoIterator] -/ +structure IntoIterator (Self : Type) where + Item : Type + IntoIter : Type + IntoIter_clause_0 : Iterator IntoIter + into_iter : Self → Result IntoIter + +/- Trait declaration: [traits::FromResidual] -/ +structure FromResidual (Self T : Type) where + +/- Trait declaration: [traits::Try] -/ +structure Try (Self : Type) where + parent_clause_0 : FromResidual Self Residual + Residual : Type + +/- Trait declaration: [traits::CFnOnce] -/ +structure CFnOnce (Self Args : Type) where + Output : Type + call_once : Self → Args → Result Output + +/- Trait declaration: [traits::CFnMut] -/ +structure CFnMut (Self Args : Type) where + parent_clause_0 : CFnOnce Self Args + call_mut : Self → Args → Result parent_clause_0.Output + call_mut_back : Self → Args → parent_clause_0.Output → Result Self + +/- Trait declaration: [traits::CFn] -/ +structure CFn (Self Args : Type) where + parent_clause_0 : CFnMut Self Args + call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output + +/- Trait declaration: [core::ops::function::FnOnce] -/ +structure core.ops.function.FnOnce (Self Args : Type) where + Output : Type + call_once : Self → Args → Result Output + +/- Trait declaration: [core::ops::function::FnMut] -/ +structure core.ops.function.FnMut (Self Args : Type) where + parent_clause_0 : core.ops.function.FnOnce Self Args + call_mut : Self → Args → Result parent_clause_0.Output + call_mut_back : Self → Args → parent_clause_0.Output → Result Self + +/- Trait declaration: [core::ops::function::Fn] -/ +structure core.ops.function.Fn (Self Args : Type) where + parent_clause_0 : core.ops.function.FnMut Self Args + call : Self → Args → Result parent_clause_0.parent_clause_0.Output + +/- [traits::map_option]: forward function -/ +def map_option + (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) : + Result (Option T) + := + match x with + | none => Result.ret none + | some x0 => do + let t ← inst.call f0 x0 + Result.ret (some t) + +/- Trait declaration: [traits::WithTarget] -/ +structure WithTarget (Self : Type) where + Target : Type + +/- Trait declaration: [traits::ParentTrait2] -/ +structure ParentTrait2 (Self : Type) where + U : Type + U_clause_0 : WithTarget U + +/- Trait declaration: [traits::ChildTrait2] -/ +structure ChildTrait2 (Self : Type) where + parent_clause_0 : ParentTrait2 Self + convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target + +/- Trait implementation: [traits::u32::{11}] -/ +def u32.WithTargetInst : WithTarget U32 := { + Target := U32 +} + +/- Trait implementation: [traits::u32::{12}] -/ +def u32.ParentTrait2Inst : ParentTrait2 U32 := { + U := U32 + U_clause_0 := u32.WithTargetInst +} + +/- [traits::u32::{13}::convert]: forward function -/ +def u32.convert (x : U32) : Result U32 := + Result.ret x + +/- Trait implementation: [traits::u32::{13}] -/ +def u32.ChildTrait2Inst : ChildTrait2 U32 := { + parent_clause_0 := u32.ParentTrait2Inst + convert := u32.convert +} + +/- [traits::incr_u32]: forward function -/ +def incr_u32 (x : U32) : Result U32 := + x + 1#u32 + +end traits diff --git a/tests/lean/Traits/Funs.lean b/tests/lean/Traits/Funs.lean deleted file mode 100644 index 8d423280..00000000 --- a/tests/lean/Traits/Funs.lean +++ /dev/null @@ -1,275 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [traits]: function definitions -import Base -import Traits.Types -open Primitives - -namespace traits - -/- [traits::Bool::{0}::get_bool]: forward function -/ -def Bool.get_bool (self : Bool) : Result Bool := - Result.ret self - -/- Trait implementation: [traits::Bool::{0}] -/ -def Bool.BoolTraitInst : BoolTrait Bool := { - get_bool := Bool.get_bool -} - -/- [traits::BoolTrait::ret_true]: forward function -/ -def BoolTrait.ret_true - {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool := - Result.ret true - -/- [traits::test_bool_trait_bool]: forward function -/ -def test_bool_trait_bool (x : Bool) : Result Bool := - do - let b ← Bool.get_bool x - if b - then BoolTrait.ret_true Bool.BoolTraitInst x - else Result.ret false - -/- [traits::Option::{1}::get_bool]: forward function -/ -def Option.get_bool (T : Type) (self : Option T) : Result Bool := - match self with - | none => Result.ret false - | some t => Result.ret true - -/- Trait implementation: [traits::Option::{1}] -/ -def Option.BoolTraitInst (T : Type) : BoolTrait (Option T) := { - get_bool := Option.get_bool T -} - -/- [traits::test_bool_trait_option]: forward function -/ -def test_bool_trait_option (T : Type) (x : Option T) : Result Bool := - do - let b ← Option.get_bool T x - if b - then BoolTrait.ret_true (Option.BoolTraitInst T) x - else Result.ret false - -/- [traits::test_bool_trait]: forward function -/ -def test_bool_trait (T : Type) (inst : BoolTrait T) (x : T) : Result Bool := - inst.get_bool x - -/- [traits::u64::{2}::to_u64]: forward function -/ -def u64.to_u64 (self : U64) : Result U64 := - Result.ret self - -/- Trait implementation: [traits::u64::{2}] -/ -def u64.ToU64Inst : ToU64 U64 := { - to_u64 := u64.to_u64 -} - -/- [traits::Tuple2::{3}::to_u64]: forward function -/ -def Tuple2.to_u64 (A : Type) (inst : ToU64 A) (self : (A × A)) : Result U64 := - do - let (t, t0) := self - let i ← inst.to_u64 t - let i0 ← inst.to_u64 t0 - i + i0 - -/- Trait implementation: [traits::Tuple2::{3}] -/ -def Tuple2.ToU64Inst (A : Type) (inst : ToU64 A) : ToU64 (A × A) := { - to_u64 := Tuple2.to_u64 A inst -} - -/- [traits::f]: forward function -/ -def f (T : Type) (inst : ToU64 T) (x : (T × T)) : Result U64 := - Tuple2.to_u64 T inst x - -/- [traits::g]: forward function -/ -def g (T : Type) (inst : ToU64 (T × T)) (x : (T × T)) : Result U64 := - inst.to_u64 x - -/- [traits::h0]: forward function -/ -def h0 (x : U64) : Result U64 := - u64.to_u64 x - -/- [traits::Wrapper::{4}::to_u64]: forward function -/ -def Wrapper.to_u64 - (T : Type) (inst : ToU64 T) (self : Wrapper T) : Result U64 := - inst.to_u64 self.x - -/- Trait implementation: [traits::Wrapper::{4}] -/ -def Wrapper.ToU64Inst (T : Type) (inst : ToU64 T) : ToU64 (Wrapper T) := { - to_u64 := Wrapper.to_u64 T inst -} - -/- [traits::h1]: forward function -/ -def h1 (x : Wrapper U64) : Result U64 := - Wrapper.to_u64 U64 u64.ToU64Inst x - -/- [traits::h2]: forward function -/ -def h2 (T : Type) (inst : ToU64 T) (x : Wrapper T) : Result U64 := - Wrapper.to_u64 T inst x - -/- [traits::u64::{5}::to_type]: forward function -/ -def u64.to_type (self : U64) : Result Bool := - Result.ret (self > 0#u64) - -/- Trait implementation: [traits::u64::{5}] -/ -def u64.ToTypeInst : ToType U64 Bool := { - to_type := u64.to_type -} - -/- [traits::h3]: forward function -/ -def h3 - (T1 T2 : Type) (inst : OfType T1) (inst0 : ToType T2 T1) (y : T2) : - Result T1 - := - inst.of_type T2 inst0 y - -/- [traits::h4]: forward function -/ -def h4 - (T1 T2 : Type) (inst : OfTypeBis T1 T2) (inst0 : ToType T2 T1) (y : T2) : - Result T1 - := - inst.of_type y - -/- [traits::TestType::{6}::test::TestType1::{0}::test]: forward function -/ -def TestType.test.TestType1.test - (self : TestType.test.TestType1) : Result Bool := - Result.ret (self._0 > 1#u64) - -/- Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] -/ -def TestType.test.TestType1.TestTypetestTestTraitInst : TestType.test.TestTrait - TestType.test.TestType1 := { - test := TestType.test.TestType1.test -} - -/- [traits::TestType::{6}::test]: forward function -/ -def TestType.test - (T : Type) (inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := - do - let x0 ← inst.to_u64 x - if x0 > 0#u64 - then TestType.test.TestType1.test { _0 := 0#u64 } - else Result.ret false - -/- [traits::BoolWrapper::{7}::to_type]: forward function -/ -def BoolWrapper.to_type - (T : Type) (inst : ToType Bool T) (self : BoolWrapper) : Result T := - inst.to_type self._0 - -/- Trait implementation: [traits::BoolWrapper::{7}] -/ -def BoolWrapper.ToTypeInst (T : Type) (inst : ToType Bool T) : ToType - BoolWrapper T := { - to_type := BoolWrapper.to_type T inst -} - -/- [traits::WithConstTy::LEN2] -/ -def with_const_ty_len2_body : Result Usize := Result.ret 32#usize -def with_const_ty_len2_c : Usize := - eval_global with_const_ty_len2_body (by simp) - -/- [traits::Bool::{8}::LEN1] -/ -def bool_len1_body : Result Usize := Result.ret 12#usize -def bool_len1_c : Usize := eval_global bool_len1_body (by simp) - -/- [traits::Bool::{8}::f]: merged forward/backward function - (there is a single backward function, and the forward function returns ()) -/ -def Bool.f (i : U64) (a : Array U8 32#usize) : Result U64 := - Result.ret i - -/- Trait implementation: [traits::Bool::{8}] -/ -def Bool.WithConstTyInst : WithConstTy Bool 32#usize := { - LEN1 := bool_len1_c - LEN2 := with_const_ty_len2_c - V := U8 - W := U64 - W_clause_0 := u64.ToU64Inst - f := Bool.f -} - -/- [traits::use_with_const_ty1]: forward function -/ -def use_with_const_ty1 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) : Result Usize := - let i := inst.LEN1 - Result.ret i - -/- [traits::use_with_const_ty2]: forward function -/ -def use_with_const_ty2 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (w : inst.W) : - Result Unit - := - Result.ret () - -/- [traits::use_with_const_ty3]: forward function -/ -def use_with_const_ty3 - (H : Type) (LEN : Usize) (inst : WithConstTy H LEN) (x : inst.W) : - Result U64 - := - inst.W_clause_0.to_u64 x - -/- [traits::test_where1]: forward function -/ -def test_where1 (T : Type) (_x : T) : Result Unit := - Result.ret () - -/- [traits::test_where2]: forward function -/ -def test_where2 - (T : Type) (inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := - Result.ret () - -/- [traits::test_child_trait1]: forward function -/ -def test_child_trait1 - (T : Type) (inst : ChildTrait T) (x : T) : Result alloc.string.String := - inst.parent_clause_0.get_name x - -/- [traits::test_child_trait2]: forward function -/ -def test_child_trait2 - (T : Type) (inst : ChildTrait T) (x : T) : Result inst.parent_clause_0.W := - inst.parent_clause_0.get_w x - -/- [traits::order1]: forward function -/ -def order1 - (T U : Type) (inst : ParentTrait0 T) (inst0 : ParentTrait0 U) : - Result Unit - := - Result.ret () - -/- Trait implementation: [traits::usize::{9}] -/ -def usize.ParentTrait1Inst : ParentTrait1 Usize := { -} - -/- Trait implementation: [traits::usize::{10}] -/ -def usize.ChildTrait1Inst : ChildTrait1 Usize := { - parent_clause_0 := usize.ParentTrait1Inst -} - -/- [traits::map_option]: forward function -/ -def map_option - (T F : Type) (inst : core.ops.function.Fn F T) (x : Option T) (f0 : F) : - Result (Option T) - := - match x with - | none => Result.ret none - | some x0 => do - let t ← inst.call f0 x0 - Result.ret (some t) - -/- Trait implementation: [traits::u32::{11}] -/ -def u32.WithTargetInst : WithTarget U32 := { - Target := U32 -} - -/- Trait implementation: [traits::u32::{12}] -/ -def u32.ParentTrait2Inst : ParentTrait2 U32 := { - U := U32 - U_clause_0 := u32.WithTargetInst -} - -/- [traits::u32::{13}::convert]: forward function -/ -def u32.convert (x : U32) : Result U32 := - Result.ret x - -/- Trait implementation: [traits::u32::{13}] -/ -def u32.ChildTrait2Inst : ChildTrait2 U32 := { - parent_clause_0 := u32.ParentTrait2Inst - convert := u32.convert -} - -/- [traits::incr_u32]: forward function -/ -def incr_u32 (x : U32) : Result U32 := - x + 1#u32 - -end traits diff --git a/tests/lean/Traits/Types.lean b/tests/lean/Traits/Types.lean deleted file mode 100644 index 4c5dd874..00000000 --- a/tests/lean/Traits/Types.lean +++ /dev/null @@ -1,144 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [traits]: type definitions -import Base -open Primitives - -namespace traits - -/- Trait declaration: [traits::BoolTrait] -/ -structure BoolTrait (Self : Type) where - get_bool : Self → Result Bool - -/- Trait declaration: [traits::ToU64] -/ -structure ToU64 (Self : Type) where - to_u64 : Self → Result U64 - -/- [traits::Wrapper] -/ -structure Wrapper (T : Type) where - x : T - -/- Trait declaration: [traits::ToType] -/ -structure ToType (Self T : Type) where - to_type : Self → Result T - -/- Trait declaration: [traits::OfType] -/ -structure OfType (Self : Type) where - of_type : forall (T : Type) (inst : ToType T Self), T → Result Self - -/- Trait declaration: [traits::OfTypeBis] -/ -structure OfTypeBis (Self T : Type) where - parent_clause_0 : ToType T Self - of_type : T → Result Self - -/- [traits::TestType] -/ -structure TestType (T : Type) where - _0 : T - -/- [traits::TestType::{6}::test::TestType1] -/ -structure TestType.test.TestType1 where - _0 : U64 - -/- Trait declaration: [traits::TestType::{6}::test::TestTrait] -/ -structure TestType.test.TestTrait (Self : Type) where - test : Self → Result Bool - -/- [traits::BoolWrapper] -/ -structure BoolWrapper where - _0 : Bool - -/- Trait declaration: [traits::WithConstTy] -/ -structure WithConstTy (Self : Type) (LEN : Usize) where - LEN1 : Usize - LEN2 : Usize - V : Type - W : Type - W_clause_0 : ToU64 W - f : W → Array U8 LEN → Result W - -/- [alloc::string::String] -/ -axiom alloc.string.String : Type - -/- Trait declaration: [traits::ParentTrait0] -/ -structure ParentTrait0 (Self : Type) where - W : Type - get_name : Self → Result alloc.string.String - get_w : Self → Result W - -/- Trait declaration: [traits::ParentTrait1] -/ -structure ParentTrait1 (Self : Type) where - -/- Trait declaration: [traits::ChildTrait] -/ -structure ChildTrait (Self : Type) where - parent_clause_0 : ParentTrait0 Self - parent_clause_1 : ParentTrait1 Self - -/- Trait declaration: [traits::ChildTrait1] -/ -structure ChildTrait1 (Self : Type) where - parent_clause_0 : ParentTrait1 Self - -/- Trait declaration: [traits::Iterator] -/ -structure Iterator (Self : Type) where - Item : Type - -/- Trait declaration: [traits::IntoIterator] -/ -structure IntoIterator (Self : Type) where - Item : Type - IntoIter : Type - IntoIter_clause_0 : Iterator IntoIter - into_iter : Self → Result IntoIter - -/- Trait declaration: [traits::FromResidual] -/ -structure FromResidual (Self T : Type) where - -/- Trait declaration: [traits::Try] -/ -structure Try (Self : Type) where - parent_clause_0 : FromResidual Self Residual - Residual : Type - -/- Trait declaration: [traits::CFnOnce] -/ -structure CFnOnce (Self Args : Type) where - Output : Type - call_once : Self → Args → Result Output - -/- Trait declaration: [traits::CFnMut] -/ -structure CFnMut (Self Args : Type) where - parent_clause_0 : CFnOnce Self Args - call_mut : Self → Args → Result parent_clause_0.Output - call_mut_back : Self → Args → parent_clause_0.Output → Result Self - -/- Trait declaration: [traits::CFn] -/ -structure CFn (Self Args : Type) where - parent_clause_0 : CFnMut Self Args - call_mut : Self → Args → Result parent_clause_0.parent_clause_0.Output - -/- Trait declaration: [core::ops::function::FnOnce] -/ -structure core.ops.function.FnOnce (Self Args : Type) where - Output : Type - call_once : Self → Args → Result Output - -/- Trait declaration: [core::ops::function::FnMut] -/ -structure core.ops.function.FnMut (Self Args : Type) where - parent_clause_0 : core.ops.function.FnOnce Self Args - call_mut : Self → Args → Result parent_clause_0.Output - call_mut_back : Self → Args → parent_clause_0.Output → Result Self - -/- Trait declaration: [core::ops::function::Fn] -/ -structure core.ops.function.Fn (Self Args : Type) where - parent_clause_0 : core.ops.function.FnMut Self Args - call : Self → Args → Result parent_clause_0.parent_clause_0.Output - -/- Trait declaration: [traits::WithTarget] -/ -structure WithTarget (Self : Type) where - Target : Type - -/- Trait declaration: [traits::ParentTrait2] -/ -structure ParentTrait2 (Self : Type) where - U : Type - U_clause_0 : WithTarget U - -/- Trait declaration: [traits::ChildTrait2] -/ -structure ChildTrait2 (Self : Type) where - parent_clause_0 : ParentTrait2 Self - convert : parent_clause_0.U → Result parent_clause_0.U_clause_0.Target - -end traits |