diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/Constants.v | 17 | ||||
| -rw-r--r-- | tests/coq/traits/Traits.v | 100 | ||||
| -rw-r--r-- | tests/fstar/misc/Constants.fst | 14 | ||||
| -rw-r--r-- | tests/fstar/traits/Traits.fst | 77 | ||||
| -rw-r--r-- | tests/lean/Constants.lean | 15 | ||||
| -rw-r--r-- | tests/lean/Traits.lean | 78 |
6 files changed, 289 insertions, 12 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 5fa952b4..fcafed53 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -158,4 +158,21 @@ Definition s3 : Pair_t u32 u32 := s3_body%global. Definition s4_body : result (Pair_t u32 u32) := mk_pair1 7%u32 8%u32. Definition s4 : Pair_t u32 u32 := s4_body%global. +(** [constants::V] + Source: 'src/constants.rs', lines 86:0-86:31 *) +Record V_t (T : Type) (N : usize) := mkV_t { v_x : array T N; }. + +Arguments mkV_t { _ _ }. +Arguments v_x { _ _ }. + +(** [constants::{constants::V<T, N>#1}::LEN] + Source: 'src/constants.rs', lines 91:4-91:24 *) +Definition v_len_body (T : Type) (N : usize) : result usize := Return N. +Definition v_len (T : Type) (N : usize) : usize := (v_len_body T N)%global. + +(** [constants::use_v]: + Source: 'src/constants.rs', lines 94:0-94:42 *) +Definition use_v (T : Type) (N : usize) : result usize := + Return (v_len T N). + End Constants. diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index a9cd7e91..a861c114 100644 --- a/tests/coq/traits/Traits.v +++ b/tests/coq/traits/Traits.v @@ -283,9 +283,12 @@ Definition ToTypetraitsBoolWrapperT (T : Type) (toTypeBoolTInst : ToType_t bool (** [traits::WithConstTy::LEN2] Source: 'src/traits.rs', lines 164:4-164:21 *) -Definition with_const_ty_len2_default_body : result usize := Return 32%usize. -Definition with_const_ty_len2_default : usize := - with_const_ty_len2_default_body%global +Definition with_const_ty_len2_default_body (Self : Type) (LEN : usize) + : result usize := + Return 32%usize +. +Definition with_const_ty_len2_default (Self : Type) (LEN : usize) : usize := + (with_const_ty_len2_default_body Self LEN)%global . (** Trait declaration: [traits::WithConstTy] @@ -326,7 +329,7 @@ Definition withConstTyBool32_f Source: 'src/traits.rs', lines 174:0-174:29 *) Definition WithConstTyBool32 : WithConstTy_t bool 32%usize := {| WithConstTy_tWithConstTy_t_LEN1 := with_const_ty_bool32_len1; - WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default; + WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_default bool 32%usize; WithConstTy_tWithConstTy_t_V := u8; WithConstTy_tWithConstTy_t_W := u64; WithConstTy_tWithConstTy_t_W_clause_0 := ToU64U64; @@ -613,4 +616,93 @@ Definition test_get_trait getTraitInst.(GetTrait_t_get_w) x . +(** Trait declaration: [traits::Trait] + Source: 'src/traits.rs', lines 310:0-310:15 *) +Record Trait_t (Self : Type) := mkTrait_t { Trait_tTrait_t_LEN : usize; }. + +Arguments mkTrait_t { _ }. +Arguments Trait_tTrait_t_LEN { _ }. + +(** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN] + Source: 'src/traits.rs', lines 315:4-315:20 *) +Definition trait_array_len_body (T : Type) (N : usize) : result usize := + Return N +. +Definition trait_array_len (T : Type) (N : usize) : usize := + (trait_array_len_body T N)%global +. + +(** Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}] + Source: 'src/traits.rs', lines 314:0-314:40 *) +Definition TraitArray (T : Type) (N : usize) : Trait_t (array T N) := {| + Trait_tTrait_t_LEN := trait_array_len T N; +|}. + +(** [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN] + Source: 'src/traits.rs', lines 319:4-319:20 *) +Definition traittraits_wrapper_len_body (T : Type) (traitInst : Trait_t T) + : result usize := + Return 0%usize +. +Definition traittraits_wrapper_len (T : Type) (traitInst : Trait_t T) + : usize := + (traittraits_wrapper_len_body T traitInst)%global +. + +(** Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}] + Source: 'src/traits.rs', lines 318:0-318:35 *) +Definition TraittraitsWrapper (T : Type) (traitInst : Trait_t T) : Trait_t + (Wrapper_t T) := {| + Trait_tTrait_t_LEN := traittraits_wrapper_len T traitInst; +|}. + +(** [traits::use_wrapper_len]: + Source: 'src/traits.rs', lines 322:0-322:43 *) +Definition use_wrapper_len (T : Type) (traitInst : Trait_t T) : result usize := + Return (TraittraitsWrapper T traitInst).(Trait_tTrait_t_LEN) +. + +(** [traits::Foo] + Source: 'src/traits.rs', lines 326:0-326:20 *) +Record Foo_t (T U : Type) := mkFoo_t { foo_x : T; foo_y : U; }. + +Arguments mkFoo_t { _ _ }. +Arguments foo_x { _ _ }. +Arguments foo_y { _ _ }. + +(** [core::result::Result] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *) +Inductive core_result_Result_t (T E : Type) := +| Core_result_Result_Ok : T -> core_result_Result_t T E +| Core_result_Result_Err : E -> core_result_Result_t T E +. + +Arguments Core_result_Result_Ok { _ _ }. +Arguments Core_result_Result_Err { _ _ }. + +(** [traits::{traits::Foo<T, U>#16}::FOO] + Source: 'src/traits.rs', lines 332:4-332:33 *) +Definition foo_foo_body (T U : Type) (traitInst : Trait_t T) + : result (core_result_Result_t T i32) := + Return (Core_result_Result_Err 0%i32) +. +Definition foo_foo (T U : Type) (traitInst : Trait_t T) + : core_result_Result_t T i32 := + (foo_foo_body T U traitInst)%global +. + +(** [traits::use_foo1]: + Source: 'src/traits.rs', lines 335:0-335:48 *) +Definition use_foo1 + (T U : Type) (traitInst : Trait_t T) : result (core_result_Result_t T i32) := + Return (foo_foo T U traitInst) +. + +(** [traits::use_foo2]: + Source: 'src/traits.rs', lines 339:0-339:48 *) +Definition use_foo2 + (T U : Type) (traitInst : Trait_t U) : result (core_result_Result_t U i32) := + Return (foo_foo U T traitInst) +. + End Traits. diff --git a/tests/fstar/misc/Constants.fst b/tests/fstar/misc/Constants.fst index 66429c80..8d1cf3ce 100644 --- a/tests/fstar/misc/Constants.fst +++ b/tests/fstar/misc/Constants.fst @@ -143,3 +143,17 @@ let s3 : pair_t u32 u32 = eval_global s3_body let s4_body : result (pair_t u32 u32) = mk_pair1 7 8 let s4 : pair_t u32 u32 = eval_global s4_body +(** [constants::V] + Source: 'src/constants.rs', lines 86:0-86:31 *) +type v_t (t : Type0) (n : usize) = { x : array t n; } + +(** [constants::{constants::V<T, N>#1}::LEN] + Source: 'src/constants.rs', lines 91:4-91:24 *) +let v_len_body (t : Type0) (n : usize) : result usize = Return n +let v_len (t : Type0) (n : usize) : usize = eval_global (v_len_body t n) + +(** [constants::use_v]: + Source: 'src/constants.rs', lines 94:0-94:42 *) +let use_v (t : Type0) (n : usize) : result usize = + Return (v_len t n) + diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 466fb482..fba564a5 100644 --- a/tests/fstar/traits/Traits.fst +++ b/tests/fstar/traits/Traits.fst @@ -229,9 +229,11 @@ let toTypetraitsBoolWrapperT (t : Type0) (toTypeBoolTInst : toType_t bool t) : (** [traits::WithConstTy::LEN2] Source: 'src/traits.rs', lines 164:4-164:21 *) -let with_const_ty_len2_default_body : result usize = Return 32 -let with_const_ty_len2_default : usize = - eval_global with_const_ty_len2_default_body +let with_const_ty_len2_default_body (self : Type0) (len : usize) + : result usize = + Return 32 +let with_const_ty_len2_default (self : Type0) (len : usize) : usize = + eval_global (with_const_ty_len2_default_body self len) (** Trait declaration: [traits::WithConstTy] Source: 'src/traits.rs', lines 161:0-161:39 *) @@ -259,7 +261,7 @@ let withConstTyBool32_f (i : u64) (a : array u8 32) : result u64 = Source: 'src/traits.rs', lines 174:0-174:29 *) let withConstTyBool32 : withConstTy_t bool 32 = { cLEN1 = with_const_ty_bool32_len1; - cLEN2 = with_const_ty_len2_default; + cLEN2 = with_const_ty_len2_default bool 32; tV = u8; tW = u64; tW_clause_0 = toU64U64; @@ -460,3 +462,70 @@ let test_get_trait (t : Type0) (getTraitInst : getTrait_t t) (x : t) : result getTraitInst.tW = getTraitInst.get_w x +(** Trait declaration: [traits::Trait] + Source: 'src/traits.rs', lines 310:0-310:15 *) +noeq type trait_t (self : Type0) = { cLEN : usize; } + +(** [traits::{(traits::Trait for @Array<T, N>)#14}::LEN] + Source: 'src/traits.rs', lines 315:4-315:20 *) +let trait_array_len_body (t : Type0) (n : usize) : result usize = Return n +let trait_array_len (t : Type0) (n : usize) : usize = + eval_global (trait_array_len_body t n) + +(** Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}] + Source: 'src/traits.rs', lines 314:0-314:40 *) +let traitArray (t : Type0) (n : usize) : trait_t (array t n) = { + cLEN = trait_array_len t n; +} + +(** [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN] + Source: 'src/traits.rs', lines 319:4-319:20 *) +let traittraits_wrapper_len_body (t : Type0) (traitInst : trait_t t) + : result usize = + Return 0 +let traittraits_wrapper_len (t : Type0) (traitInst : trait_t t) : usize = + eval_global (traittraits_wrapper_len_body t traitInst) + +(** Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}] + Source: 'src/traits.rs', lines 318:0-318:35 *) +let traittraitsWrapper (t : Type0) (traitInst : trait_t t) : trait_t (wrapper_t + t) = { + cLEN = traittraits_wrapper_len t traitInst; +} + +(** [traits::use_wrapper_len]: + Source: 'src/traits.rs', lines 322:0-322:43 *) +let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize = + Return (traittraitsWrapper t traitInst).cLEN + +(** [traits::Foo] + Source: 'src/traits.rs', lines 326:0-326:20 *) +type foo_t (t u : Type0) = { x : t; y : u; } + +(** [core::result::Result] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *) +type core_result_Result_t (t e : Type0) = +| Core_result_Result_Ok : t -> core_result_Result_t t e +| Core_result_Result_Err : e -> core_result_Result_t t e + +(** [traits::{traits::Foo<T, U>#16}::FOO] + Source: 'src/traits.rs', lines 332:4-332:33 *) +let foo_foo_body (t u : Type0) (traitInst : trait_t t) + : result (core_result_Result_t t i32) = + Return (Core_result_Result_Err 0) +let foo_foo (t u : Type0) (traitInst : trait_t t) + : core_result_Result_t t i32 = + eval_global (foo_foo_body t u traitInst) + +(** [traits::use_foo1]: + Source: 'src/traits.rs', lines 335:0-335:48 *) +let use_foo1 + (t u : Type0) (traitInst : trait_t t) : result (core_result_Result_t t i32) = + Return (foo_foo t u traitInst) + +(** [traits::use_foo2]: + Source: 'src/traits.rs', lines 339:0-339:48 *) +let use_foo2 + (t u : Type0) (traitInst : trait_t u) : result (core_result_Result_t u i32) = + Return (foo_foo u t traitInst) + diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index 7949a25c..40f590d4 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -149,4 +149,19 @@ def S3 : Pair U32 U32 := eval_global S3_body def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32 def S4 : Pair U32 U32 := eval_global S4_body +/- [constants::V] + Source: 'src/constants.rs', lines 86:0-86:31 -/ +structure V (T : Type) (N : Usize) where + x : Array T N + +/- [constants::{constants::V<T, N>#1}::LEN] + Source: 'src/constants.rs', lines 91:4-91:24 -/ +def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N +def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N) + +/- [constants::use_v]: + Source: 'src/constants.rs', lines 94:0-94:42 -/ +def use_v (T : Type) (N : Usize) : Result Usize := + Result.ret (V.LEN T N) + end constants diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 26dac252..acddd1a9 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -242,9 +242,10 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) : /- [traits::WithConstTy::LEN2] Source: 'src/traits.rs', lines 164:4-164:21 -/ -def WithConstTy.LEN2_default_body : Result Usize := Result.ret 32#usize -def WithConstTy.LEN2_default : Usize := - eval_global WithConstTy.LEN2_default_body +def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize := + Result.ret 32#usize +def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize := + eval_global (WithConstTy.LEN2_default_body Self LEN) /- Trait declaration: [traits::WithConstTy] Source: 'src/traits.rs', lines 161:0-161:39 -/ @@ -270,7 +271,7 @@ def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 := Source: 'src/traits.rs', lines 174:0-174:29 -/ def WithConstTyBool32 : WithConstTy Bool 32#usize := { LEN1 := WithConstTyBool32.LEN1 - LEN2 := WithConstTy.LEN2_default + LEN2 := WithConstTy.LEN2_default Bool 32#usize V := U8 W := U64 W_clause_0 := ToU64U64 @@ -467,4 +468,73 @@ def test_get_trait (T : Type) (GetTraitInst : GetTrait T) (x : T) : Result GetTraitInst.W := GetTraitInst.get_w x +/- Trait declaration: [traits::Trait] + Source: 'src/traits.rs', lines 310:0-310:15 -/ +structure Trait (Self : Type) where + LEN : Usize + +/- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN] + Source: 'src/traits.rs', lines 315:4-315:20 -/ +def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N +def TraitArray.LEN (T : Type) (N : Usize) : Usize := + eval_global (TraitArray.LEN_body T N) + +/- Trait implementation: [traits::{(traits::Trait for @Array<T, N>)#14}] + Source: 'src/traits.rs', lines 314:0-314:40 -/ +def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := { + LEN := TraitArray.LEN T N +} + +/- [traits::{(traits::Trait for traits::Wrapper<T>)#15}::LEN] + Source: 'src/traits.rs', lines 319:4-319:20 -/ +def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T) + : Result Usize := + Result.ret 0#usize +def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize := + eval_global (TraittraitsWrapper.LEN_body T TraitInst) + +/- Trait implementation: [traits::{(traits::Trait for traits::Wrapper<T>)#15}] + Source: 'src/traits.rs', lines 318:0-318:35 -/ +def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T) + := { + LEN := TraittraitsWrapper.LEN T TraitInst +} + +/- [traits::use_wrapper_len]: + Source: 'src/traits.rs', lines 322:0-322:43 -/ +def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize := + Result.ret (TraittraitsWrapper T TraitInst).LEN + +/- [traits::Foo] + Source: 'src/traits.rs', lines 326:0-326:20 -/ +structure Foo (T U : Type) where + x : T + y : U + +/- [core::result::Result] + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/ +inductive core.result.Result (T E : Type) := +| Ok : T → core.result.Result T E +| Err : E → core.result.Result T E + +/- [traits::{traits::Foo<T, U>#16}::FOO] + Source: 'src/traits.rs', lines 332:4-332:33 -/ +def Foo.FOO_body (T U : Type) (TraitInst : Trait T) + : Result (core.result.Result T I32) := + Result.ret (core.result.Result.Err 0#i32) +def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 := + eval_global (Foo.FOO_body T U TraitInst) + +/- [traits::use_foo1]: + Source: 'src/traits.rs', lines 335:0-335:48 -/ +def use_foo1 + (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) := + Result.ret (Foo.FOO T U TraitInst) + +/- [traits::use_foo2]: + Source: 'src/traits.rs', lines 339:0-339:48 -/ +def use_foo2 + (T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) := + Result.ret (Foo.FOO U T TraitInst) + end traits |