diff options
Diffstat (limited to '')
66 files changed, 641 insertions, 369 deletions
diff --git a/tests/coq/array/Array.v b/tests/coq/array/Array.v index 99ff3b03..105ce21f 100644 --- a/tests/coq/array/Array.v +++ b/tests/coq/array/Array.v @@ -528,4 +528,4 @@ Definition ite : result unit := Return tt . -End Array . +End Array. diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v index 8e48b17d..aadaa20d 100644 --- a/tests/coq/betree/BetreeMain_Funs.v +++ b/tests/coq/betree/BetreeMain_Funs.v @@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export BetreeMain_Types. -Import BetreeMain_Types. -Require Export BetreeMain_Opaque. -Import BetreeMain_Opaque. +Require Import BetreeMain_Types. +Include BetreeMain_Types. +Require Import BetreeMain_FunsExternal. +Include BetreeMain_FunsExternal. Module BetreeMain_Funs. (** [betree_main::betree::load_internal_node]: forward function @@ -1230,4 +1230,4 @@ Definition main : result unit := (** Unit test for [betree_main::main] *) Check (main )%return. -End BetreeMain_Funs . +End BetreeMain_Funs. diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_FunsExternal.v index a065c8a3..07dba263 100644 --- a/tests/coq/betree/BetreeMain_Opaque.v +++ b/tests/coq/betree/BetreeMain_FunsExternal.v @@ -1,5 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) +(** [betree_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. @@ -8,7 +9,7 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export BetreeMain_Types. Import BetreeMain_Types. -Module BetreeMain_Opaque. +Module BetreeMain_FunsExternal. (** [betree_main::betree_utils::load_internal_node]: forward function Source: 'src/betree_utils.rs', lines 98:0-98:63 *) @@ -42,4 +43,4 @@ Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . -End BetreeMain_Opaque . +End BetreeMain_FunsExternal. diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v new file mode 100644 index 00000000..36022a20 --- /dev/null +++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v @@ -0,0 +1,46 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import BetreeMain_Types. +Include BetreeMain_Types. +Module BetreeMain_FunsExternal_Template. + +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) +Axiom betree_utils_load_internal_node + : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) +. + +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) +Axiom betree_utils_store_internal_node + : + u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * + unit) +. + +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) +Axiom betree_utils_load_leaf_node + : u64 -> state -> result (state * (betree_List_t (u64 * u64))) +. + +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) +Axiom betree_utils_store_leaf_node + : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) +. + +(** [core::option::{core::option::Option<T>}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) +Axiom core_option_Option_unwrap : + forall(T : Type), option T -> state -> result (state * T) +. + +End BetreeMain_FunsExternal_Template. diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v index b729d1c3..22989256 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/BetreeMain_Types.v @@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. +Require Import BetreeMain_TypesExternal. +Include BetreeMain_TypesExternal. Module BetreeMain_Types. (** [betree_main::betree::List] @@ -113,7 +115,4 @@ mkbetree_BeTree_t { } . -(** The state type used in the state-error monad *) -Axiom state : Type. - -End BetreeMain_Types . +End BetreeMain_Types. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v new file mode 100644 index 00000000..50c4a4f8 --- /dev/null +++ b/tests/coq/betree/BetreeMain_TypesExternal.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module BetreeMain_TypesExternal. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End BetreeMain_TypesExternal. diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/BetreeMain_TypesExternal_Template.v new file mode 100644 index 00000000..651de2b7 --- /dev/null +++ b/tests/coq/betree/BetreeMain_TypesExternal_Template.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module BetreeMain_TypesExternal_Template. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End BetreeMain_TypesExternal_Template. diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 42c62421..13e4b9c1 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -4,6 +4,9 @@ -arg all BetreeMain_Types.v +BetreeMain_TypesExternal_Template.v Primitives.v +BetreeMain_FunsExternal_Template.v BetreeMain_Funs.v -BetreeMain_Opaque.v +BetreeMain_TypesExternal.v +BetreeMain_FunsExternal.v diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index c08f7f7d..64de44a6 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -6,8 +6,8 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export Hashmap_Types. -Import Hashmap_Types. +Require Import Hashmap_Types. +Include Hashmap_Types. Module Hashmap_Funs. (** [hashmap::hash_key]: forward function @@ -668,4 +668,4 @@ Definition test1 (n : nat) : result unit := end)) . -End Hashmap_Funs . +End Hashmap_Funs. diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v index bfb5ae4b..80a43593 100644 --- a/tests/coq/hashmap/Hashmap_Types.v +++ b/tests/coq/hashmap/Hashmap_Types.v @@ -35,4 +35,4 @@ Arguments hashMap_max_load_factor { _ }. Arguments hashMap_max_load { _ }. Arguments hashMap_slots { _ }. -End Hashmap_Types . +End Hashmap_Types. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v index 46d3ee29..faba0afe 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v @@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export HashmapMain_Types. -Import HashmapMain_Types. -Require Export HashmapMain_Opaque. -Import HashmapMain_Opaque. +Require Import HashmapMain_Types. +Include HashmapMain_Types. +Require Import HashmapMain_FunsExternal. +Include HashmapMain_FunsExternal. Module HashmapMain_Funs. (** [hashmap_main::hashmap::hash_key]: forward function @@ -717,4 +717,4 @@ Definition insert_on_disk Definition main : result unit := Return tt. -End HashmapMain_Funs . +End HashmapMain_Funs. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v index a0e9003d..a03dc407 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v @@ -8,7 +8,7 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export HashmapMain_Types. Import HashmapMain_Types. -Module HashmapMain_Opaque. +Module HashmapMain_FunsExternal. (** [hashmap_main::hashmap_utils::deserialize]: forward function Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *) @@ -22,4 +22,4 @@ Axiom hashmap_utils_serialize : hashmap_HashMap_t u64 -> state -> result (state * unit) . -End HashmapMain_Opaque . +End HashmapMain_FunsExternal. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v new file mode 100644 index 00000000..e10d02f6 --- /dev/null +++ b/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v @@ -0,0 +1,26 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import HashmapMain_Types. +Include HashmapMain_Types. +Module HashmapMain_FunsExternal_Template. + +(** [hashmap_main::hashmap_utils::deserialize]: forward function + Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *) +Axiom hashmap_utils_deserialize + : state -> result (state * (hashmap_HashMap_t u64)) +. + +(** [hashmap_main::hashmap_utils::serialize]: forward function + Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *) +Axiom hashmap_utils_serialize + : hashmap_HashMap_t u64 -> state -> result (state * unit) +. + +End HashmapMain_FunsExternal_Template. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v index 039b7e72..8d3d72aa 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v @@ -6,6 +6,8 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. +Require Import HashmapMain_TypesExternal. +Include HashmapMain_TypesExternal. Module HashmapMain_Types. (** [hashmap_main::hashmap::List] @@ -35,7 +37,4 @@ Arguments hashmap_HashMap_max_load_factor { _ }. Arguments hashmap_HashMap_max_load { _ }. Arguments hashmap_HashMap_slots { _ }. -(** The state type used in the state-error monad *) -Axiom state : Type. - -End HashmapMain_Types . +End HashmapMain_Types. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v new file mode 100644 index 00000000..87568232 --- /dev/null +++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module HashmapMain_TypesExternal. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End HashmapMain_TypesExternal. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v new file mode 100644 index 00000000..391b2775 --- /dev/null +++ b/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module HashmapMain_TypesExternal_Template. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End HashmapMain_TypesExternal_Template. diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index b78c7b5f..41945494 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -6,4 +6,7 @@ HashmapMain_Types.v Primitives.v HashmapMain_Funs.v -HashmapMain_Opaque.v +HashmapMain_TypesExternal.v +HashmapMain_FunsExternal_Template.v +HashmapMain_FunsExternal.v +HashmapMain_TypesExternal_Template.v diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 20edb2b1..ad899f25 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -157,4 +157,4 @@ Definition s3_c : Pair_t u32 u32 := s3_body%global. Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32. Definition s4_c : Pair_t u32 u32 := s4_body%global. -End Constants . +End Constants. diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 0a14c7d1..e9d39f66 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -6,10 +6,10 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export External_Types. -Import External_Types. -Require Export External_Opaque. -Import External_Opaque. +Require Import External_Types. +Include External_Types. +Require Import External_FunsExternal. +Include External_FunsExternal. Module External_Funs. (** [external::swap]: forward function @@ -115,4 +115,4 @@ Definition test_swap_non_zero (x : u32) (st : state) : result (state * u32) := if x0 s= 0%u32 then Fail_ Failure else Return (st1, x0) . -End External_Funs . +End External_Funs. diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_FunsExternal.v index b482431f..a8c5756a 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -7,8 +7,8 @@ Require Import List. Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. -Import External_Types. -Module External_Opaque. +Include External_Types. +Module External_FunsExternal. (** [core::mem::swap]: forward function Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) @@ -40,4 +40,4 @@ Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . -End External_Opaque . +End External_FunsExternal. diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v new file mode 100644 index 00000000..31e69c39 --- /dev/null +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -0,0 +1,44 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import External_Types. +Include External_Types. +Module External_FunsExternal_Template. + +(** [core::mem::swap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap : + forall(T : Type), T -> T -> state -> result (state * unit) +. + +(** [core::mem::swap]: backward function 0 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap_back0 : + forall(T : Type), T -> T -> state -> state -> result (state * T) +. + +(** [core::mem::swap]: backward function 1 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap_back1 : + forall(T : Type), T -> T -> state -> state -> result (state * T) +. + +(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) +Axiom core_num_nonzero_NonZeroU32_new + : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t)) +. + +(** [core::option::{core::option::Option<T>}::unwrap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) +Axiom core_option_Option_unwrap : + forall(T : Type), option T -> state -> result (state * T) +. + +End External_FunsExternal_Template. diff --git a/tests/coq/misc/External_Types.v b/tests/coq/misc/External_Types.v index c638670c..b42c2ecf 100644 --- a/tests/coq/misc/External_Types.v +++ b/tests/coq/misc/External_Types.v @@ -6,13 +6,8 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. +Require Import External_TypesExternal. +Include External_TypesExternal. Module External_Types. -(** [core::num::nonzero::NonZeroU32] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *) -Axiom core_num_nonzero_NonZeroU32_t : Type. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End External_Types . +End External_Types. diff --git a/tests/coq/misc/External_TypesExternal.v b/tests/coq/misc/External_TypesExternal.v new file mode 100644 index 00000000..3f02b839 --- /dev/null +++ b/tests/coq/misc/External_TypesExternal.v @@ -0,0 +1,19 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module External_TypesExternal. + +(** [core::num::nonzero::NonZeroU32] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *) +Axiom core_num_nonzero_NonZeroU32_t : Type. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End External_TypesExternal. diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v new file mode 100644 index 00000000..7ba79d8e --- /dev/null +++ b/tests/coq/misc/External_TypesExternal_Template.v @@ -0,0 +1,19 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module External_TypesExternal_Template. + +(** [core::num::nonzero::NonZeroU32] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *) +Axiom core_num_nonzero_NonZeroU32_t : Type. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End External_TypesExternal_Template. diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 4929ddd0..83c249c1 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -914,4 +914,4 @@ Definition list_nth_shared_mut_loop_pair_merge_back list_nth_shared_mut_loop_pair_merge_loop_back T n ls0 ls1 i ret . -End Loops . +End Loops. diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index b044d24f..16a2e816 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -586,4 +586,4 @@ Definition test_shared_borrow_enum1 (l : List_t u32) : result u32 := Definition test_shared_borrow_enum2 : result u32 := Return 0%u32. -End NoNestedBorrows . +End NoNestedBorrows. diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index 4a49096f..6b110193 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -128,4 +128,4 @@ Definition call_choose (p : (u32 * u32)) : result u32 := Return px0 . -End Paper . +End Paper. diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index a0820e40..2371b1cc 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -41,4 +41,4 @@ Fixpoint get_list_at_x_back end . -End PoloniusList . +End PoloniusList. diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index db6c2742..0828bced 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -4,11 +4,14 @@ -arg all Loops.v +External_Types.v Primitives.v External_Funs.v +Paper.v +External_TypesExternal.v Constants.v PoloniusList.v -External_Types.v NoNestedBorrows.v -External_Opaque.v -Paper.v +External_FunsExternal.v +External_TypesExternal_Template.v +External_FunsExternal_Template.v diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index 0952a1df..ebdca4ec 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -382,15 +382,11 @@ Definition test_where2 Return tt . -(** [alloc::string::String] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *) -Axiom alloc_string_String_t : Type. - (** Trait declaration: [traits::ParentTrait0] Source: 'src/traits.rs', lines 200:0-200:22 *) Record ParentTrait0_t (Self : Type) := mkParentTrait0_t { ParentTrait0_tParentTrait0_t_W : Type; - ParentTrait0_t_get_name : Self -> result alloc_string_String_t; + ParentTrait0_t_get_name : Self -> result string; ParentTrait0_t_get_w : Self -> result ParentTrait0_tParentTrait0_t_W; }. @@ -419,9 +415,7 @@ Arguments ChildTrait_tChildTrait_t_ParentTrait1SelfInst { _ }. (** [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 *) Definition test_child_trait1 - (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : - result alloc_string_String_t - := + (T : Type) (childTraitTInst : ChildTrait_t T) (x : T) : result string := childTraitTInst.(ChildTrait_tChildTrait_t_ParentTrait0SelfInst).(ParentTrait0_t_get_name) x . @@ -617,4 +611,4 @@ Arguments CFn_t_call_mut { _ _ }. Definition incr_u32 (x : u32) : result u32 := u32_add x 1%u32. -End Traits . +End Traits. diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst index 537ec32e..fef8a8e1 100644 --- a/tests/fstar/betree/BetreeMain.Funs.fst +++ b/tests/fstar/betree/BetreeMain.Funs.fst @@ -3,7 +3,7 @@ module BetreeMain.Funs open Primitives include BetreeMain.Types -include BetreeMain.Opaque +include BetreeMain.FunsExternal include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti index b89c8718..cd2f956f 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external function declarations *) -module BetreeMain.Opaque +module BetreeMain.FunsExternal open Primitives include BetreeMain.Types diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fst index a098ec19..b87219b2 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti +++ b/tests/fstar/betree/BetreeMain.Types.fst @@ -2,6 +2,7 @@ (** [betree_main]: type definitions *) module BetreeMain.Types open Primitives +include BetreeMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -58,6 +59,3 @@ type betree_BeTree_t = root : betree_Node_t; } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti new file mode 100644 index 00000000..1b2c53a6 --- /dev/null +++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external type declarations *) +module BetreeMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst index a2586431..b912a316 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst +++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst @@ -3,7 +3,7 @@ module BetreeMain.Funs open Primitives include BetreeMain.Types -include BetreeMain.Opaque +include BetreeMain.FunsExternal include BetreeMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/betree/BetreeMain.Opaque.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti index b89c8718..cd2f956f 100644 --- a/tests/fstar/betree/BetreeMain.Opaque.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [betree_main]: external function declarations *) -module BetreeMain.Opaque +module BetreeMain.FunsExternal open Primitives include BetreeMain.Types diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst index a098ec19..b87219b2 100644 --- a/tests/fstar/betree/BetreeMain.Types.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst @@ -2,6 +2,7 @@ (** [betree_main]: type definitions *) module BetreeMain.Types open Primitives +include BetreeMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -58,6 +59,3 @@ type betree_BeTree_t = root : betree_Node_t; } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti new file mode 100644 index 00000000..1b2c53a6 --- /dev/null +++ b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external type declarations *) +module BetreeMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst index fa570309..f2d09a38 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst @@ -3,7 +3,7 @@ module HashmapMain.Funs open Primitives include HashmapMain.Types -include HashmapMain.Opaque +include HashmapMain.FunsExternal include HashmapMain.Clauses #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti index 1f47eb33..b00bbcde 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Opaque.fsti +++ b/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [hashmap_main]: external function declarations *) -module HashmapMain.Opaque +module HashmapMain.FunsExternal open Primitives include HashmapMain.Types diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst index e77954ad..afebcde3 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst @@ -2,6 +2,7 @@ (** [hashmap_main]: type definitions *) module HashmapMain.Types open Primitives +include HashmapMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) = slots : alloc_vec_Vec (hashmap_List_t t); } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti new file mode 100644 index 00000000..75747408 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external type declarations *) +module HashmapMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst index 4d13fb71..00995634 100644 --- a/tests/fstar/misc/External.Funs.fst +++ b/tests/fstar/misc/External.Funs.fst @@ -3,7 +3,7 @@ module External.Funs open Primitives include External.Types -include External.Opaque +include External.FunsExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/misc/External.Opaque.fsti b/tests/fstar/misc/External.FunsExternal.fsti index ea1a70c2..923a1101 100644 --- a/tests/fstar/misc/External.Opaque.fsti +++ b/tests/fstar/misc/External.FunsExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) (** [external]: external function declarations *) -module External.Opaque +module External.FunsExternal open Primitives include External.Types diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst new file mode 100644 index 00000000..4fbcec47 --- /dev/null +++ b/tests/fstar/misc/External.Types.fst @@ -0,0 +1,8 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: type definitions *) +module External.Types +open Primitives +include External.TypesExternal + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.TypesExternal.fsti index 0cb9fd0e..4bfbe0c5 100644 --- a/tests/fstar/misc/External.Types.fsti +++ b/tests/fstar/misc/External.TypesExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: type definitions *) -module External.Types +(** [external]: external type declarations *) +module External.TypesExternal open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 4cb9fbf1..895a1cac 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -307,15 +307,11 @@ let test_where2 = Return () -(** [alloc::string::String] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 *) -assume type alloc_string_String_t : Type0 - (** Trait declaration: [traits::ParentTrait0] Source: 'src/traits.rs', lines 200:0-200:22 *) noeq type parentTrait0_t (self : Type0) = { tW : Type0; - get_name : self -> result alloc_string_String_t; + get_name : self -> result string; get_w : self -> result tW; } @@ -333,9 +329,7 @@ noeq type childTrait_t (self : Type0) = { (** [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 *) let test_child_trait1 - (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : - result alloc_string_String_t - = + (t : Type0) (childTraitTInst : childTrait_t t) (x : t) : result string = childTraitTInst.parentTrait0SelfInst.get_name x (** [traits::test_child_trait2]: forward function diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean index 4832f469..b49add96 100644 --- a/tests/lean/Array.lean +++ b/tests/lean/Array.lean @@ -31,10 +31,10 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) := /- [array::array_to_mut_slice_]: backward function 0 Source: 'src/array.rs', lines 21:0-21:58 -/ def array_to_mut_slice__back - (T : Type) (s : Array T 32#usize) (ret0 : Slice T) : + (T : Type) (s : Array T 32#usize) (ret : Slice T) : Result (Array T 32#usize) := - Array.from_slice T 32#usize s ret0 + Array.from_slice T 32#usize s ret /- [array::array_len]: forward function Source: 'src/array.rs', lines 25:0-25:40 -/ @@ -82,10 +82,10 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := /- [array::index_mut_array]: backward function 0 Source: 'src/array.rs', lines 52:0-52:62 -/ def index_mut_array_back - (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) : + (T : Type) (s : Array T 32#usize) (i : Usize) (ret : T) : Result (Array T 32#usize) := - Array.update_usize T 32#usize s i ret0 + Array.update_usize T 32#usize s i ret /- [array::index_slice]: forward function Source: 'src/array.rs', lines 56:0-56:46 -/ @@ -100,8 +100,8 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T := /- [array::index_mut_slice]: backward function 0 Source: 'src/array.rs', lines 60:0-60:58 -/ def index_mut_slice_back - (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) := - Slice.update_usize T s i ret0 + (T : Type) (s : Slice T) (i : Usize) (ret : T) : Result (Slice T) := + Slice.update_usize T s i ret /- [array::slice_subslice_shared_]: forward function Source: 'src/array.rs', lines 64:0-64:70 -/ @@ -122,12 +122,12 @@ def slice_subslice_mut_ /- [array::slice_subslice_mut_]: backward function 0 Source: 'src/array.rs', lines 68:0-68:75 -/ def slice_subslice_mut__back - (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) : + (x : Slice U32) (y : Usize) (z : Usize) (ret : Slice U32) : Result (Slice U32) := core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x - { start := y, end_ := z } ret0 + { start := y, end_ := z } ret /- [array::array_to_slice_shared_]: forward function Source: 'src/array.rs', lines 72:0-72:54 -/ @@ -142,8 +142,8 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) := /- [array::array_to_slice_mut_]: backward function 0 Source: 'src/array.rs', lines 76:0-76:59 -/ 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 + (x : Array U32 32#usize) (ret : Slice U32) : Result (Array U32 32#usize) := + Array.from_slice U32 32#usize x ret /- [array::array_subslice_shared_]: forward function Source: 'src/array.rs', lines 80:0-80:74 -/ @@ -166,13 +166,13 @@ def array_subslice_mut_ /- [array::array_subslice_mut_]: backward function 0 Source: 'src/array.rs', lines 84:0-84:79 -/ def array_subslice_mut__back - (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) : + (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret : Slice U32) : Result (Array U32 32#usize) := core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x - { start := y, end_ := z } ret0 + { start := y, end_ := z } ret /- [array::index_slice_0]: forward function Source: 'src/array.rs', lines 88:0-88:38 -/ @@ -417,7 +417,7 @@ 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 + then Result.fail .panic else sum2_loop s s2 0#u32 0#usize /- [array::f0]: forward function diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 45548884..4c862225 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -121,7 +121,7 @@ divergent def betree.List.split_at let (ls0, ls1) := p let l := ls0 Result.ret (betree.List.Cons hd l, ls1) - | betree.List.Nil => Result.fail Error.panic + | betree.List.Nil => Result.fail .panic /- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function (there is a single backward function, and the forward function returns ()) @@ -138,7 +138,7 @@ def betree.List.pop_front (T : Type) (self : betree.List T) : Result T := let ls := core.mem.replace (betree.List T) self betree.List.Nil match ls with | betree.List.Cons x tl => Result.ret x - | betree.List.Nil => Result.fail Error.panic + | betree.List.Nil => Result.fail .panic /- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0 Source: 'src/betree.rs', lines 306:4-306:32 -/ @@ -147,14 +147,14 @@ def betree.List.pop_front_back let ls := core.mem.replace (betree.List T) self betree.List.Nil match ls with | betree.List.Cons x tl => Result.ret tl - | betree.List.Nil => Result.fail Error.panic + | betree.List.Nil => Result.fail .panic /- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function Source: 'src/betree.rs', lines 318:4-318:22 -/ def betree.List.hd (T : Type) (self : betree.List T) : Result T := match self with | betree.List.Cons hd l => Result.ret hd - | betree.List.Nil => Result.fail Error.panic + | betree.List.Nil => Result.fail .panic /- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function Source: 'src/betree.rs', lines 327:4-327:44 -/ @@ -241,20 +241,20 @@ divergent def betree.Node.lookup_first_message_for_key Source: 'src/betree.rs', lines 789:4-792:34 -/ divergent def betree.Node.lookup_first_message_for_key_back (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret0 : betree.List (U64 × betree.Message)) : + (ret : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) := match msgs with | betree.List.Cons x next_msgs => let (i, m) := x if i >= key - then Result.ret ret0 + then Result.ret ret else do let next_msgs0 ← - betree.Node.lookup_first_message_for_key_back key next_msgs ret0 + betree.Node.lookup_first_message_for_key_back key next_msgs ret Result.ret (betree.List.Cons (i, m) next_msgs0) - | betree.List.Nil => Result.ret ret0 + | betree.List.Nil => Result.ret ret /- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function Source: 'src/betree.rs', lines 819:4-819:90 -/ @@ -271,8 +271,8 @@ divergent def betree.Node.apply_upserts let msg ← betree.List.pop_front (U64 × betree.Message) msgs let (_, m) := msg match m with - | betree.Message.Insert i => Result.fail Error.panic - | betree.Message.Delete => Result.fail Error.panic + | betree.Message.Insert i => Result.fail .panic + | betree.Message.Delete => Result.fail .panic | betree.Message.Upsert s => do let v ← betree.upsert_update prev s @@ -302,8 +302,8 @@ divergent def betree.Node.apply_upserts_back let msg ← betree.List.pop_front (U64 × betree.Message) msgs let (_, m) := msg match m with - | betree.Message.Insert i => Result.fail Error.panic - | betree.Message.Delete => Result.fail Error.panic + | betree.Message.Insert i => Result.fail .panic + | betree.Message.Delete => Result.fail .panic | betree.Message.Upsert s => do let v ← betree.upsert_update prev s @@ -542,7 +542,7 @@ divergent def betree.Node.lookup_first_message_after_key Source: 'src/betree.rs', lines 689:4-692:34 -/ divergent def betree.Node.lookup_first_message_after_key_back (key : U64) (msgs : betree.List (U64 × betree.Message)) - (ret0 : betree.List (U64 × betree.Message)) : + (ret : betree.List (U64 × betree.Message)) : Result (betree.List (U64 × betree.Message)) := match msgs with @@ -552,10 +552,10 @@ divergent def betree.Node.lookup_first_message_after_key_back then do let next_msgs0 ← - betree.Node.lookup_first_message_after_key_back key next_msgs ret0 + betree.Node.lookup_first_message_after_key_back key next_msgs ret Result.ret (betree.List.Cons (k, m) next_msgs0) - else Result.ret ret0 - | betree.List.Nil => Result.ret ret0 + else Result.ret ret + | betree.List.Nil => Result.ret ret /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function (there is a single backward function, and the forward function returns ()) @@ -658,19 +658,19 @@ divergent def betree.Node.lookup_mut_in_bindings Source: 'src/betree.rs', lines 653:4-656:32 -/ divergent def betree.Node.lookup_mut_in_bindings_back (key : U64) (bindings : betree.List (U64 × U64)) - (ret0 : betree.List (U64 × U64)) : + (ret : betree.List (U64 × U64)) : Result (betree.List (U64 × U64)) := match bindings with | betree.List.Cons hd tl => let (i, i0) := hd if i >= key - then Result.ret ret0 + then Result.ret ret else do - let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0 + let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret Result.ret (betree.List.Cons (i, i0) tl0) - | betree.List.Nil => Result.ret ret0 + | betree.List.Nil => Result.ret ret /- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function (there is a single backward function, and the forward function returns ()) @@ -1069,6 +1069,6 @@ def main : Result Unit := Result.ret () /- Unit test for [betree_main::main] -/ -#assert (main == .ret ()) +#assert (main == Result.ret ()) end betree_main diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean index 6e528437..877508f6 100644 --- a/tests/lean/BetreeMain/Types.lean +++ b/tests/lean/BetreeMain/Types.lean @@ -1,6 +1,7 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [betree_main]: type definitions import Base +import BetreeMain.TypesExternal open Primitives namespace betree_main @@ -63,7 +64,4 @@ structure betree.BeTree where node_id_cnt : betree.NodeIdCounter root : betree.Node -/- The state type used in the state-error monad -/ -axiom State : Type - end betree_main diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean new file mode 100644 index 00000000..1701eaaf --- /dev/null +++ b/tests/lean/BetreeMain/TypesExternal.lean @@ -0,0 +1,7 @@ +-- [betree_main]: external types. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean new file mode 100644 index 00000000..bbac7e99 --- /dev/null +++ b/tests/lean/BetreeMain/TypesExternal_Template.lean @@ -0,0 +1,9 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [betree_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index e5655c7e..48ec6ad5 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -45,7 +45,7 @@ def test_vec : Result Unit := Result.ret () /- Unit test for [external::test_vec] -/ -#assert (test_vec == .ret ()) +#assert (test_vec == Result.ret ()) /- [external::custom_swap]: forward function Source: 'src/external.rs', lines 24:0-24:66 -/ @@ -60,14 +60,14 @@ def custom_swap /- [external::custom_swap]: backward function 0 Source: 'src/external.rs', lines 24:0-24:66 -/ def custom_swap_back - (T : Type) (x : T) (y : T) (st : State) (ret0 : T) (st0 : State) : + (T : Type) (x : T) (y : T) (st : State) (ret : T) (st0 : State) : Result (State × (T × T)) := do let (st1, _) ← core.mem.swap T x y st let (st2, _) ← core.mem.swap_back0 T x y st st1 let (_, y0) ← core.mem.swap_back1 T x y st st2 - Result.ret (st0, (ret0, y0)) + Result.ret (st0, (ret, y0)) /- [external::test_custom_swap]: forward function Source: 'src/external.rs', lines 29:0-29:59 -/ @@ -92,7 +92,7 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) := let (st0, _) ← swap U32 x 0#u32 st let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0 if x0 = 0#u32 - then Result.fail Error.panic + then Result.fail .panic else Result.ret (st1, x0) end external diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean index 40f20cda..961f3e8a 100644 --- a/tests/lean/External/Types.lean +++ b/tests/lean/External/Types.lean @@ -1,15 +1,9 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [external]: type definitions import Base +import External.TypesExternal open Primitives namespace external -/- [core::num::nonzero::NonZeroU32] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/ -axiom core.num.nonzero.NonZeroU32 : Type - -/- The state type used in the state-error monad -/ -axiom State : Type - end external diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean new file mode 100644 index 00000000..7c30f792 --- /dev/null +++ b/tests/lean/External/TypesExternal.lean @@ -0,0 +1,11 @@ +-- [external]: external types. +import Base +open Primitives + +/- [core::num::nonzero::NonZeroU32] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/ +axiom core.num.nonzero.NonZeroU32 : Type + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean new file mode 100644 index 00000000..85fef236 --- /dev/null +++ b/tests/lean/External/TypesExternal_Template.lean @@ -0,0 +1,13 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [external]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Base +open Primitives + +/- [core::num::nonzero::NonZeroU32] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/ +axiom core.num.nonzero.NonZeroU32 : Type + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 95c501f6..e03981a2 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -295,7 +295,7 @@ divergent def HashMap.get_in_list_loop if ckey = key then Result.ret cvalue else HashMap.get_in_list_loop T key tl - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap<T>}::get_in_list]: forward function Source: 'src/hashmap.rs', lines 224:4-224:70 -/ @@ -324,7 +324,7 @@ divergent def HashMap.get_mut_in_list_loop if ckey = key then Result.ret cvalue else HashMap.get_mut_in_list_loop T tl key - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: forward function Source: 'src/hashmap.rs', lines 245:4-245:86 -/ @@ -335,22 +335,22 @@ def HashMap.get_mut_in_list /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0 Source: 'src/hashmap.rs', lines 245:4-254:5 -/ divergent def HashMap.get_mut_in_list_loop_back - (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := + (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) := match ls with | List.Cons ckey cvalue tl => if ckey = key - then Result.ret (List.Cons ckey ret0 tl) + then Result.ret (List.Cons ckey ret tl) else do - let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0 + let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret Result.ret (List.Cons ckey cvalue tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: backward function 0 Source: 'src/hashmap.rs', lines 245:4-245:86 -/ def HashMap.get_mut_in_list_back - (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) := - HashMap.get_mut_in_list_loop_back T ls key ret0 + (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) := + HashMap.get_mut_in_list_loop_back T ls key ret /- [hashmap::{hashmap::HashMap<T>}::get_mut]: forward function Source: 'src/hashmap.rs', lines 257:4-257:67 -/ @@ -368,9 +368,7 @@ def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T := /- [hashmap::{hashmap::HashMap<T>}::get_mut]: backward function 0 Source: 'src/hashmap.rs', lines 257:4-257:67 -/ def HashMap.get_mut_back - (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) : - Result (HashMap T) - := + (T : Type) (self : HashMap T) (key : Usize) (ret : T) : Result (HashMap T) := do let hash ← hash_key key let i := alloc.vec.Vec.len (List T) self.slots @@ -379,7 +377,7 @@ def HashMap.get_mut_back alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod - let l0 ← HashMap.get_mut_in_list_back T l key ret0 + let l0 ← HashMap.get_mut_in_list_back T l key ret let v ← alloc.vec.Vec.index_mut_back (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots @@ -397,7 +395,7 @@ divergent def HashMap.remove_from_list_loop let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret (some cvalue) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic else HashMap.remove_from_list_loop T key tl | List.Nil => Result.ret none @@ -418,7 +416,7 @@ divergent def HashMap.remove_from_list_loop_back let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil match mv_ls with | List.Cons i cvalue tl0 => Result.ret tl0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic else do let tl0 ← HashMap.remove_from_list_loop_back T key tl @@ -493,37 +491,37 @@ def test1 : Result Unit := let hm3 ← HashMap.insert U64 hm2 1056#usize 256#u64 let i ← HashMap.get U64 hm3 128#usize if not (i = 18#u64) - then Result.fail Error.panic + then Result.fail .panic else do let hm4 ← HashMap.get_mut_back U64 hm3 1024#usize 56#u64 let i0 ← HashMap.get U64 hm4 1024#usize if not (i0 = 56#u64) - then Result.fail Error.panic + then Result.fail .panic else do let x ← HashMap.remove U64 hm4 1024#usize match x with - | none => Result.fail Error.panic + | none => Result.fail .panic | some x0 => if not (x0 = 56#u64) - then Result.fail Error.panic + then Result.fail .panic else do let hm5 ← HashMap.remove_back U64 hm4 1024#usize let i1 ← HashMap.get U64 hm5 0#usize if not (i1 = 42#u64) - then Result.fail Error.panic + then Result.fail .panic else do let i2 ← HashMap.get U64 hm5 128#usize if not (i2 = 18#u64) - then Result.fail Error.panic + then Result.fail .panic else do let i3 ← HashMap.get U64 hm5 1056#usize if not (i3 = 256#u64) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () end hashmap diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean index abe84bbf..f87ad355 100644 --- a/tests/lean/HashmapMain/Funs.lean +++ b/tests/lean/HashmapMain/Funs.lean @@ -309,7 +309,7 @@ divergent def hashmap.HashMap.get_in_list_loop if ckey = key then Result.ret cvalue else hashmap.HashMap.get_in_list_loop T key tl - | hashmap.List.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail .panic /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: forward function Source: 'src/hashmap.rs', lines 224:4-224:70 -/ @@ -340,7 +340,7 @@ divergent def hashmap.HashMap.get_mut_in_list_loop if ckey = key then Result.ret cvalue else hashmap.HashMap.get_mut_in_list_loop T tl key - | hashmap.List.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail .panic /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: forward function Source: 'src/hashmap.rs', lines 245:4-245:86 -/ @@ -351,26 +351,26 @@ def hashmap.HashMap.get_mut_in_list /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0 Source: 'src/hashmap.rs', lines 245:4-254:5 -/ divergent def hashmap.HashMap.get_mut_in_list_loop_back - (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) : Result (hashmap.List T) := match ls with | hashmap.List.Cons ckey cvalue tl => if ckey = key - then Result.ret (hashmap.List.Cons ckey ret0 tl) + then Result.ret (hashmap.List.Cons ckey ret tl) else do - let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0 + let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret Result.ret (hashmap.List.Cons ckey cvalue tl0) - | hashmap.List.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail .panic /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: backward function 0 Source: 'src/hashmap.rs', lines 245:4-245:86 -/ def hashmap.HashMap.get_mut_in_list_back - (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) : + (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) : Result (hashmap.List T) := - hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0 + hashmap.HashMap.get_mut_in_list_loop_back T ls key ret /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: forward function Source: 'src/hashmap.rs', lines 257:4-257:67 -/ @@ -389,7 +389,7 @@ def hashmap.HashMap.get_mut /- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: backward function 0 Source: 'src/hashmap.rs', lines 257:4-257:67 -/ def hashmap.HashMap.get_mut_back - (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) : + (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret : T) : Result (hashmap.HashMap T) := do @@ -400,7 +400,7 @@ def hashmap.HashMap.get_mut_back alloc.vec.Vec.index_mut (hashmap.List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots hash_mod - let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0 + let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret let v ← alloc.vec.Vec.index_mut_back (hashmap.List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) @@ -420,7 +420,7 @@ divergent def hashmap.HashMap.remove_from_list_loop hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret (some cvalue) - | hashmap.List.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail .panic else hashmap.HashMap.remove_from_list_loop T key tl | hashmap.List.Nil => Result.ret none @@ -443,7 +443,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back hashmap.List.Nil match mv_ls with | hashmap.List.Cons i cvalue tl0 => Result.ret tl0 - | hashmap.List.Nil => Result.fail Error.panic + | hashmap.List.Nil => Result.fail .panic else do let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl @@ -520,37 +520,37 @@ def hashmap.test1 : Result Unit := let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64 let i ← hashmap.HashMap.get U64 hm3 128#usize if not (i = 18#u64) - then Result.fail Error.panic + then Result.fail .panic else do let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64 let i0 ← hashmap.HashMap.get U64 hm4 1024#usize if not (i0 = 56#u64) - then Result.fail Error.panic + then Result.fail .panic else do let x ← hashmap.HashMap.remove U64 hm4 1024#usize match x with - | none => Result.fail Error.panic + | none => Result.fail .panic | some x0 => if not (x0 = 56#u64) - then Result.fail Error.panic + then Result.fail .panic else do let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize let i1 ← hashmap.HashMap.get U64 hm5 0#usize if not (i1 = 42#u64) - then Result.fail Error.panic + then Result.fail .panic else do let i2 ← hashmap.HashMap.get U64 hm5 128#usize if not (i2 = 18#u64) - then Result.fail Error.panic + then Result.fail .panic else do let i3 ← hashmap.HashMap.get U64 hm5 1056#usize if not (i3 = 256#u64) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- [hashmap_main::insert_on_disk]: forward function diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean index f7be6719..ae9ac999 100644 --- a/tests/lean/HashmapMain/Types.lean +++ b/tests/lean/HashmapMain/Types.lean @@ -1,6 +1,7 @@ -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS -- [hashmap_main]: type definitions import Base +import HashmapMain.TypesExternal open Primitives namespace hashmap_main @@ -19,7 +20,4 @@ structure hashmap.HashMap (T : Type) where max_load : Usize slots : alloc.vec.Vec (hashmap.List T) -/- The state type used in the state-error monad -/ -axiom State : Type - end hashmap_main diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/HashmapMain/TypesExternal.lean new file mode 100644 index 00000000..4e1cdbe9 --- /dev/null +++ b/tests/lean/HashmapMain/TypesExternal.lean @@ -0,0 +1,7 @@ +-- [hashmap_main]: external types. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/HashmapMain/TypesExternal_Template.lean new file mode 100644 index 00000000..cfa8bbb1 --- /dev/null +++ b/tests/lean/HashmapMain/TypesExternal_Template.lean @@ -0,0 +1,9 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +import Base +open Primitives + +/- The state type used in the state-error monad -/ +axiom State : Type + diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index ae1d87aa..08aa08a5 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -107,7 +107,7 @@ divergent def list_nth_mut_loop_loop else do let i0 ← i - 1#u32 list_nth_mut_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop]: forward function Source: 'src/loops.rs', lines 78:0-78:71 -/ @@ -117,23 +117,23 @@ def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T := /- [loops::list_nth_mut_loop]: loop 0: backward function 0 Source: 'src/loops.rs', lines 78:0-88:1 -/ divergent def list_nth_mut_loop_loop_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) := match ls with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0 + let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop]: backward function 0 Source: 'src/loops.rs', lines 78:0-78:71 -/ 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 + (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) := + list_nth_mut_loop_loop_back T ls i ret /- [loops::list_nth_shared_loop]: loop 0: forward function Source: 'src/loops.rs', lines 91:0-101:1 -/ @@ -146,7 +146,7 @@ divergent def list_nth_shared_loop_loop else do let i0 ← i - 1#u32 list_nth_shared_loop_loop T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_loop]: forward function Source: 'src/loops.rs', lines 91:0-91:66 -/ @@ -160,7 +160,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize := | List.Cons y tl => if y = x then Result.ret y else get_elem_mut_loop x tl - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::get_elem_mut]: forward function Source: 'src/loops.rs', lines 103:0-103:73 -/ @@ -175,28 +175,28 @@ def get_elem_mut /- [loops::get_elem_mut]: loop 0: backward function 0 Source: 'src/loops.rs', lines 103:0-117:1 -/ divergent def get_elem_mut_loop_back - (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) := + (x : Usize) (ls : List Usize) (ret : Usize) : Result (List Usize) := match ls with | List.Cons y tl => if y = x - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do - let tl0 ← get_elem_mut_loop_back x tl ret0 + let tl0 ← get_elem_mut_loop_back x tl ret Result.ret (List.Cons y tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::get_elem_mut]: backward function 0 Source: 'src/loops.rs', lines 103:0-103:73 -/ def get_elem_mut_back - (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) : + (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret : Usize) : Result (alloc.vec.Vec (List Usize)) := do let l ← alloc.vec.Vec.index_mut (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize - let l0 ← get_elem_mut_loop_back x l ret0 + let l0 ← get_elem_mut_loop_back x l ret alloc.vec.Vec.index_mut_back (List Usize) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize l0 @@ -209,7 +209,7 @@ divergent def get_elem_shared_loop | List.Cons y tl => if y = x then Result.ret y else get_elem_shared_loop x tl - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::get_elem_shared]: forward function Source: 'src/loops.rs', lines 119:0-119:68 -/ @@ -228,8 +228,8 @@ def id_mut (T : Type) (ls : List T) : Result (List T) := /- [loops::id_mut]: backward function 0 Source: 'src/loops.rs', lines 135:0-135:50 -/ -def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) := - Result.ret ret0 +def id_mut_back (T : Type) (ls : List T) (ret : List T) : Result (List T) := + Result.ret ret /- [loops::id_shared]: forward function Source: 'src/loops.rs', lines 139:0-139:45 -/ @@ -247,7 +247,7 @@ divergent def list_nth_mut_loop_with_id_loop else do let i0 ← i - 1#u32 list_nth_mut_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_with_id]: forward function Source: 'src/loops.rs', lines 144:0-144:75 -/ @@ -259,25 +259,25 @@ def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T := /- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 Source: 'src/loops.rs', lines 144:0-155:1 -/ divergent def list_nth_mut_loop_with_id_loop_back - (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) := + (T : Type) (i : U32) (ls : List T) (ret : T) : Result (List T) := match ls with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0 + let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_with_id]: backward function 0 Source: 'src/loops.rs', lines 144:0-144:75 -/ def list_nth_mut_loop_with_id_back - (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) := + (T : Type) (ls : List T) (i : U32) (ret : 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 + let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret id_mut_back T ls l /- [loops::list_nth_shared_loop_with_id]: loop 0: forward function @@ -291,7 +291,7 @@ divergent def list_nth_shared_loop_with_id_loop else do let i0 ← i - 1#u32 list_nth_shared_loop_with_id_loop T i0 tl - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_loop_with_id]: forward function Source: 'src/loops.rs', lines 158:0-158:70 -/ @@ -314,8 +314,8 @@ divergent def list_nth_mut_loop_pair_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_pair]: forward function Source: 'src/loops.rs', lines 174:0-178:27 -/ @@ -326,7 +326,7 @@ def list_nth_mut_loop_pair /- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 Source: 'src/loops.rs', lines 174:0-195:1 -/ divergent def list_nth_mut_loop_pair_loop_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -334,27 +334,27 @@ divergent def list_nth_mut_loop_pair_loop_back'a match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) + then Result.ret (List.Cons ret tl0) else do let i0 ← i - 1#u32 - let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0 + let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_pair]: backward function 0 Source: 'src/loops.rs', lines 174:0-178:27 -/ def list_nth_mut_loop_pair_back'a - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0 + list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret /- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 Source: 'src/loops.rs', lines 174:0-195:1 -/ divergent def list_nth_mut_loop_pair_loop_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -362,22 +362,22 @@ divergent def list_nth_mut_loop_pair_loop_back'b match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) + then Result.ret (List.Cons ret tl1) else do let i0 ← i - 1#u32 - let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0 + let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_pair]: backward function 1 Source: 'src/loops.rs', lines 174:0-178:27 -/ def list_nth_mut_loop_pair_back'b - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0 + list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret /- [loops::list_nth_shared_loop_pair]: loop 0: forward function Source: 'src/loops.rs', lines 198:0-219:1 -/ @@ -392,8 +392,8 @@ divergent def list_nth_shared_loop_pair_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_loop_pair]: forward function Source: 'src/loops.rs', lines 198:0-202:19 -/ @@ -415,8 +415,8 @@ divergent def list_nth_mut_loop_pair_merge_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_pair_merge]: forward function Source: 'src/loops.rs', lines 223:0-227:27 -/ @@ -427,7 +427,7 @@ def list_nth_mut_loop_pair_merge /- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 Source: 'src/loops.rs', lines 223:0-238:1 -/ divergent def list_nth_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) : Result ((List T) × (List T)) := match ls0 with @@ -435,24 +435,24 @@ divergent def list_nth_mut_loop_pair_merge_loop_back match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then let (t, t0) := ret0 + then let (t, t0) := ret 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 + list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret Result.ret (List.Cons x0 tl00, List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_loop_pair_merge]: backward function 0 Source: 'src/loops.rs', lines 223:0-227:27 -/ def list_nth_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) : Result ((List T) × (List T)) := - list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret /- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function Source: 'src/loops.rs', lines 241:0-256:1 -/ @@ -468,8 +468,8 @@ divergent def list_nth_shared_loop_pair_merge_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_loop_pair_merge]: forward function Source: 'src/loops.rs', lines 241:0-245:19 -/ @@ -491,8 +491,8 @@ divergent def list_nth_mut_shared_loop_pair_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_shared_loop_pair]: forward function Source: 'src/loops.rs', lines 259:0-263:23 -/ @@ -503,7 +503,7 @@ def list_nth_mut_shared_loop_pair /- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 Source: 'src/loops.rs', lines 259:0-274:1 -/ divergent def list_nth_mut_shared_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -511,23 +511,22 @@ divergent def list_nth_mut_shared_loop_pair_loop_back match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) + then Result.ret (List.Cons ret tl0) else do let i0 ← i - 1#u32 - let tl00 ← - list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0 + let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_shared_loop_pair]: backward function 0 Source: 'src/loops.rs', lines 259:0-263:23 -/ def list_nth_mut_shared_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0 + list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function Source: 'src/loops.rs', lines 278:0-293:1 -/ @@ -543,8 +542,8 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_shared_loop_pair_merge]: forward function Source: 'src/loops.rs', lines 278:0-282:23 -/ @@ -555,7 +554,7 @@ def list_nth_mut_shared_loop_pair_merge /- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 Source: 'src/loops.rs', lines 278:0-293:1 -/ divergent def list_nth_mut_shared_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -563,23 +562,23 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl0) + then Result.ret (List.Cons ret tl0) else do let i0 ← i - 1#u32 let tl00 ← - list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret Result.ret (List.Cons x0 tl00) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 Source: 'src/loops.rs', lines 278:0-282:23 -/ def list_nth_mut_shared_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0 + list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret /- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function Source: 'src/loops.rs', lines 297:0-312:1 -/ @@ -595,8 +594,8 @@ divergent def list_nth_shared_mut_loop_pair_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_mut_loop_pair]: forward function Source: 'src/loops.rs', lines 297:0-301:23 -/ @@ -607,7 +606,7 @@ def list_nth_shared_mut_loop_pair /- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 Source: 'src/loops.rs', lines 297:0-312:1 -/ divergent def list_nth_shared_mut_loop_pair_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -615,23 +614,22 @@ divergent def list_nth_shared_mut_loop_pair_loop_back match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) + then Result.ret (List.Cons ret tl1) else do let i0 ← i - 1#u32 - let tl10 ← - list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0 + let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_mut_loop_pair]: backward function 1 Source: 'src/loops.rs', lines 297:0-301:23 -/ def list_nth_shared_mut_loop_pair_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0 + list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function Source: 'src/loops.rs', lines 316:0-331:1 -/ @@ -647,8 +645,8 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop 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 + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_mut_loop_pair_merge]: forward function Source: 'src/loops.rs', lines 316:0-320:23 -/ @@ -659,7 +657,7 @@ def list_nth_shared_mut_loop_pair_merge /- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 Source: 'src/loops.rs', lines 316:0-331:1 -/ divergent def list_nth_shared_mut_loop_pair_merge_loop_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := match ls0 with @@ -667,22 +665,22 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back match ls1 with | List.Cons x1 tl1 => if i = 0#u32 - then Result.ret (List.Cons ret0 tl1) + then Result.ret (List.Cons ret tl1) else do let i0 ← i - 1#u32 let tl10 ← - list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0 + list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret Result.ret (List.Cons x1 tl10) - | List.Nil => Result.fail Error.panic - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic + | List.Nil => Result.fail .panic /- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 Source: 'src/loops.rs', lines 316:0-320:23 -/ def list_nth_shared_mut_loop_pair_merge_back - (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) : + (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) : Result (List T) := - list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0 + list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret end loops diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 3b1c3f9f..ca66c628 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -101,7 +101,7 @@ def test2 : Result Unit := Result.ret () /- Unit test for [no_nested_borrows::test2] -/ -#assert (test2 == .ret ()) +#assert (test2 == Result.ret ()) /- [no_nested_borrows::get_max]: forward function Source: 'src/no_nested_borrows.rs', lines 111:0-111:37 -/ @@ -118,11 +118,11 @@ def test3 : Result Unit := let y ← get_max 10#u32 11#u32 let z ← x + y if not (z = 15#u32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test3] -/ -#assert (test3 == .ret ()) +#assert (test3 == Result.ret ()) /- [no_nested_borrows::test_neg1]: forward function Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 -/ @@ -130,40 +130,39 @@ def test_neg1 : Result Unit := do let y ← - 3#i32 if not (y = (-(3:Int))#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_neg1] -/ -#assert (test_neg1 == .ret ()) +#assert (test_neg1 == Result.ret ()) /- [no_nested_borrows::refs_test1]: forward function Source: 'src/no_nested_borrows.rs', lines 133:0-133:19 -/ def refs_test1 : Result Unit := if not (1#i32 = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::refs_test1] -/ -#assert (refs_test1 == .ret ()) +#assert (refs_test1 == Result.ret ()) /- [no_nested_borrows::refs_test2]: forward function Source: 'src/no_nested_borrows.rs', lines 144:0-144:19 -/ def refs_test2 : Result Unit := if not (2#i32 = 2#i32) - then Result.fail Error.panic + then Result.fail .panic else if not (0#i32 = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else if not (2#i32 = 2#i32) - then Result.fail Error.panic - else - if not (2#i32 = 2#i32) - then Result.fail Error.panic - else Result.ret () + then Result.fail .panic + else if not (2#i32 = 2#i32) + then Result.fail .panic + else Result.ret () /- Unit test for [no_nested_borrows::refs_test2] -/ -#assert (refs_test2 == .ret ()) +#assert (refs_test2 == Result.ret ()) /- [no_nested_borrows::test_list1]: forward function Source: 'src/no_nested_borrows.rs', lines 160:0-160:19 -/ @@ -171,7 +170,7 @@ def test_list1 : Result Unit := Result.ret () /- Unit test for [no_nested_borrows::test_list1] -/ -#assert (test_list1 == .ret ()) +#assert (test_list1 == Result.ret ()) /- [no_nested_borrows::test_box1]: forward function Source: 'src/no_nested_borrows.rs', lines 165:0-165:18 -/ @@ -181,11 +180,11 @@ def test_box1 : Result Unit := let b0 ← alloc.boxed.Box.deref_mut_back I32 b 1#i32 let x ← alloc.boxed.Box.deref I32 b0 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_box1] -/ -#assert (test_box1 == .ret ()) +#assert (test_box1 == Result.ret ()) /- [no_nested_borrows::copy_int]: forward function Source: 'src/no_nested_borrows.rs', lines 175:0-175:30 -/ @@ -196,14 +195,14 @@ def copy_int (x : I32) : Result I32 := Source: 'src/no_nested_borrows.rs', lines 181:0-181:32 -/ def test_unreachable (b : Bool) : Result Unit := if b - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- [no_nested_borrows::test_panic]: forward function Source: 'src/no_nested_borrows.rs', lines 189:0-189:26 -/ def test_panic (b : Bool) : Result Unit := if b - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- [no_nested_borrows::test_copy_int]: forward function @@ -212,11 +211,11 @@ def test_copy_int : Result Unit := do let y ← copy_int 0#i32 if not (0#i32 = y) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_copy_int] -/ -#assert (test_copy_int == .ret ()) +#assert (test_copy_int == Result.ret ()) /- [no_nested_borrows::is_cons]: forward function Source: 'src/no_nested_borrows.rs', lines 203:0-203:38 -/ @@ -232,18 +231,18 @@ def test_is_cons : Result Unit := let l := List.Nil let b ← is_cons I32 (List.Cons 0#i32 l) if not b - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_is_cons] -/ -#assert (test_is_cons == .ret ()) +#assert (test_is_cons == Result.ret ()) /- [no_nested_borrows::split_list]: forward function Source: 'src/no_nested_borrows.rs', lines 216:0-216:48 -/ def split_list (T : Type) (l : List T) : Result (T × (List T)) := match l with | List.Cons hd tl => Result.ret (hd, tl) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [no_nested_borrows::test_split_list]: forward function Source: 'src/no_nested_borrows.rs', lines 224:0-224:24 -/ @@ -253,11 +252,11 @@ def test_split_list : Result Unit := let p ← split_list I32 (List.Cons 0#i32 l) let (hd, _) := p if not (hd = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_split_list] -/ -#assert (test_split_list == .ret ()) +#assert (test_split_list == Result.ret ()) /- [no_nested_borrows::choose]: forward function Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/ @@ -269,10 +268,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T := /- [no_nested_borrows::choose]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/ def choose_back - (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) := + (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) := if b - then Result.ret (ret0, y) - else Result.ret (x, ret0) + then Result.ret (ret, y) + else Result.ret (x, ret) /- [no_nested_borrows::choose_test]: forward function Source: 'src/no_nested_borrows.rs', lines 239:0-239:20 -/ @@ -281,18 +280,18 @@ def choose_test : Result Unit := let z ← choose I32 true 0#i32 0#i32 let z0 ← z + 1#i32 if not (z0 = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else do let (x, y) ← choose_back I32 true 0#i32 0#i32 z0 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else if not (y = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::choose_test] -/ -#assert (choose_test == .ret ()) +#assert (choose_test == Result.ret ()) /- [no_nested_borrows::test_char]: forward function Source: 'src/no_nested_borrows.rs', lines 251:0-251:26 -/ @@ -334,7 +333,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := else do let i0 ← i - 1#u32 list_nth_shared T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [no_nested_borrows::list_nth_mut]: forward function Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/ @@ -346,22 +345,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T := else do let i0 ← i - 1#u32 list_nth_mut T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [no_nested_borrows::list_nth_mut]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/ divergent def list_nth_mut_back - (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := + (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) := match l with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_back T tl i0 ret0 + let tl0 ← list_nth_mut_back T tl i0 ret Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [no_nested_borrows::list_rev_aux]: forward function Source: 'src/no_nested_borrows.rs', lines 336:0-336:63 -/ @@ -387,43 +386,43 @@ def test_list_functions : Result Unit := let l1 := List.Cons 1#i32 l0 let i ← list_length I32 (List.Cons 0#i32 l1) if not (i = 3#u32) - then Result.fail Error.panic + then Result.fail .panic else do let i0 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32 if not (i0 = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else do let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32 if not (i1 = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else do let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32 if not (i2 = 2#i32) - then Result.fail Error.panic + then Result.fail .panic else do let ls ← list_nth_mut_back I32 (List.Cons 0#i32 l1) 1#u32 3#i32 let i3 ← list_nth_shared I32 ls 0#u32 if not (i3 = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else do let i4 ← list_nth_shared I32 ls 1#u32 if not (i4 = 3#i32) - then Result.fail Error.panic + then Result.fail .panic else do let i5 ← list_nth_shared I32 ls 2#u32 if not (i5 = 2#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_list_functions] -/ -#assert (test_list_functions == .ret ()) +#assert (test_list_functions == Result.ret ()) /- [no_nested_borrows::id_mut_pair1]: forward function Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/ @@ -433,8 +432,8 @@ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) := /- [no_nested_borrows::id_mut_pair1]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/ def id_mut_pair1_back - (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : Result (T1 × T2) := - let (t, t0) := ret0 + (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 × T2)) : Result (T1 × T2) := + let (t, t0) := ret Result.ret (t, t0) /- [no_nested_borrows::id_mut_pair2]: forward function @@ -446,8 +445,8 @@ def id_mut_pair2 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) := /- [no_nested_borrows::id_mut_pair2]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 375:0-375:88 -/ def id_mut_pair2_back - (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : Result (T1 × T2) := - let (t, t0) := ret0 + (T1 T2 : Type) (p : (T1 × T2)) (ret : (T1 × T2)) : Result (T1 × T2) := + let (t, t0) := ret Result.ret (t, t0) /- [no_nested_borrows::id_mut_pair3]: forward function @@ -458,14 +457,14 @@ def id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) := /- [no_nested_borrows::id_mut_pair3]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/ def id_mut_pair3_back'a - (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T1) : Result T1 := - Result.ret ret0 + (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : Result T1 := + Result.ret ret /- [no_nested_borrows::id_mut_pair3]: backward function 1 Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/ def id_mut_pair3_back'b - (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T2) : Result T2 := - Result.ret ret0 + (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : Result T2 := + Result.ret ret /- [no_nested_borrows::id_mut_pair4]: forward function Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/ @@ -476,14 +475,14 @@ def id_mut_pair4 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) := /- [no_nested_borrows::id_mut_pair4]: backward function 0 Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/ def id_mut_pair4_back'a - (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T1) : Result T1 := - Result.ret ret0 + (T1 T2 : Type) (p : (T1 × T2)) (ret : T1) : Result T1 := + Result.ret ret /- [no_nested_borrows::id_mut_pair4]: backward function 1 Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/ def id_mut_pair4_back'b - (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T2) : Result T2 := - Result.ret ret0 + (T1 T2 : Type) (p : (T1 × T2)) (ret : T2) : Result T2 := + Result.ret ret /- [no_nested_borrows::StructWithTuple] Source: 'src/no_nested_borrows.rs', lines 390:0-390:34 -/ @@ -522,28 +521,28 @@ def test_constants : Result Unit := let swt ← new_tuple1 let (i, _) := swt.p if not (i = 1#u32) - then Result.fail Error.panic + then Result.fail .panic else do let swt0 ← new_tuple2 let (i0, _) := swt0.p if not (i0 = 1#i16) - then Result.fail Error.panic + then Result.fail .panic else do let swt1 ← new_tuple3 let (i1, _) := swt1.p if not (i1 = 1#u64) - then Result.fail Error.panic + then Result.fail .panic else do let swp ← new_pair1 if not (swp.p.x = 1#u32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [no_nested_borrows::test_constants] -/ -#assert (test_constants == .ret ()) +#assert (test_constants == Result.ret ()) /- [no_nested_borrows::test_weird_borrows1]: forward function Source: 'src/no_nested_borrows.rs', lines 428:0-428:28 -/ @@ -551,7 +550,7 @@ def test_weird_borrows1 : Result Unit := Result.ret () /- Unit test for [no_nested_borrows::test_weird_borrows1] -/ -#assert (test_weird_borrows1 == .ret ()) +#assert (test_weird_borrows1 == Result.ret ()) /- [no_nested_borrows::test_mem_replace]: merged forward/backward function (there is a single backward function, and the forward function returns ()) @@ -559,7 +558,7 @@ def test_weird_borrows1 : Result Unit := def test_mem_replace (px : U32) : Result U32 := let y := core.mem.replace U32 px 1#u32 if not (y = 0#u32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret 2#u32 /- [no_nested_borrows::test_shared_borrow_bool1]: forward function diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 37e0e70e..08386bb7 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -17,11 +17,11 @@ def test_incr : Result Unit := do let x ← ref_incr 0#i32 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_incr] -/ -#assert (test_incr == .ret ()) +#assert (test_incr == Result.ret ()) /- [paper::choose]: forward function Source: 'src/paper.rs', lines 15:0-15:70 -/ @@ -33,10 +33,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T := /- [paper::choose]: backward function 0 Source: 'src/paper.rs', lines 15:0-15:70 -/ def choose_back - (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) := + (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) := if b - then Result.ret (ret0, y) - else Result.ret (x, ret0) + then Result.ret (ret, y) + else Result.ret (x, ret) /- [paper::test_choose]: forward function Source: 'src/paper.rs', lines 23:0-23:20 -/ @@ -45,18 +45,18 @@ def test_choose : Result Unit := let z ← choose I32 true 0#i32 0#i32 let z0 ← z + 1#i32 if not (z0 = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else do let (x, y) ← choose_back I32 true 0#i32 0#i32 z0 if not (x = 1#i32) - then Result.fail Error.panic + then Result.fail .panic else if not (y = 0#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_choose] -/ -#assert (test_choose == .ret ()) +#assert (test_choose == Result.ret ()) /- [paper::List] Source: 'src/paper.rs', lines 35:0-35:16 -/ @@ -74,22 +74,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T := else do let i0 ← i - 1#u32 list_nth_mut T tl i0 - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [paper::list_nth_mut]: backward function 0 Source: 'src/paper.rs', lines 42:0-42:67 -/ divergent def list_nth_mut_back - (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) := + (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) := match l with | List.Cons x tl => if i = 0#u32 - then Result.ret (List.Cons ret0 tl) + then Result.ret (List.Cons ret tl) else do let i0 ← i - 1#u32 - let tl0 ← list_nth_mut_back T tl i0 ret0 + let tl0 ← list_nth_mut_back T tl i0 ret Result.ret (List.Cons x tl0) - | List.Nil => Result.fail Error.panic + | List.Nil => Result.fail .panic /- [paper::sum]: forward function Source: 'src/paper.rs', lines 57:0-57:32 -/ @@ -112,11 +112,11 @@ def test_nth : Result Unit := let l2 ← list_nth_mut_back I32 (List.Cons 1#i32 l1) 2#u32 x0 let i ← sum l2 if not (i = 7#i32) - then Result.fail Error.panic + then Result.fail .panic else Result.ret () /- Unit test for [paper::test_nth] -/ -#assert (test_nth == .ret ()) +#assert (test_nth == Result.ret ()) /- [paper::call_choose]: forward function Source: 'src/paper.rs', lines 76:0-76:44 -/ diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean index 0ef71791..37f0dffb 100644 --- a/tests/lean/PoloniusList.lean +++ b/tests/lean/PoloniusList.lean @@ -24,15 +24,15 @@ divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) := /- [polonius_list::get_list_at_x]: backward function 0 Source: 'src/polonius_list.rs', lines 13:0-13:76 -/ divergent def get_list_at_x_back - (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) := + (ls : List U32) (x : U32) (ret : List U32) : Result (List U32) := match ls with | List.Cons hd tl => if hd = x - then Result.ret ret0 + then Result.ret ret else do - let tl0 ← get_list_at_x_back tl x ret0 + let tl0 ← get_list_at_x_back tl x ret Result.ret (List.Cons hd tl0) - | List.Nil => Result.ret ret0 + | List.Nil => Result.ret ret end polonius_list diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 9ac4736c..e7795d9c 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -326,15 +326,11 @@ def test_where2 := Result.ret () -/- [alloc::string::String] - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 -/ -axiom alloc.string.String : Type - /- Trait declaration: [traits::ParentTrait0] Source: 'src/traits.rs', lines 200:0-200:22 -/ structure ParentTrait0 (Self : Type) where W : Type - get_name : Self → Result alloc.string.String + get_name : Self → Result String get_w : Self → Result W /- Trait declaration: [traits::ParentTrait1] @@ -350,9 +346,7 @@ structure ChildTrait (Self : Type) where /- [traits::test_child_trait1]: forward function Source: 'src/traits.rs', lines 209:0-209:56 -/ def test_child_trait1 - (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : - Result alloc.string.String - := + (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String := ChildTraitTInst.ParentTrait0SelfInst.get_name x /- [traits::test_child_trait2]: forward function |