3 #![feature(box_syntax)]
5 // Iota-reduction is a rule in the Calculus of (Co-)Inductive Constructions,
6 // which "says that a destructor applied to an object built from a constructor
7 // behaves as expected". -- https://coq.inria.fr/doc/language/core/conversion.html#iota-reduction
9 // It's a little more complicated here, because of pointers and regions and
10 // trying to get assert failure messages that at least identify which case
13 enum E
<T
> { Thing(isize, T), Nothing((), ((), ()), [i8; 0]) }
15 fn is_none(&self) -> bool
{
17 E
::Thing(..) => false,
18 E
::Nothing(..) => true
21 fn get_ref(&self) -> (isize, &T
) {
23 E
::Nothing(..) => panic
!("E::get_ref(Nothing::<{}>)", stringify
!(T
)),
24 E
::Thing(x
, ref y
) => (x
, y
)
29 macro_rules
! check_option
{
30 ($e
:expr
, $T
:ty
) => {{
31 check_option
!($e
, $T
, |ptr
| assert_eq
!(*ptr
, $e
));
33 ($e
:expr
, $T
:ty
, |$v
:ident
| $chk
:expr
) => {{
34 assert
!(None
::<$T
>.is_none());
36 let s_
= Some
::<$T
>(e
);
37 let $v
= s_
.as_ref().unwrap();
42 macro_rules
! check_fancy
{
43 ($e
:expr
, $T
:ty
) => {{
44 check_fancy
!($e
, $T
, |ptr
| assert_eq
!(*ptr
, $e
));
46 ($e
:expr
, $T
:ty
, |$v
:ident
| $chk
:expr
) => {{
47 assert
!(E
::Nothing
::<$T
>((), ((), ()), [23; 0]).is_none());
49 let t_
= E
::Thing
::<$T
>(23, e
);
52 _
=> panic
!("Thing::<{}>(23, {}).get_ref() != (23, _)",
53 stringify
!($T
), stringify
!($e
))
58 macro_rules
! check_type
{
60 check_option
!($
($a
)*);
66 check_type
!(&17, &isize);
67 check_type
!(box 18, Box
<isize>);
68 check_type
!("foo".to_string(), String
);
69 check_type
!(vec
![20, 22], Vec
<isize>);
70 check_type
!(main
, fn(), |pthing
| {
71 assert_eq
!(main
as fn(), *pthing
as fn())