1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

pub use paste::paste;

#[doc = include_str!("../docs/exists_macro.md")]
#[macro_export]
macro_rules! exists {
  ( $(
      $exists:ident
      ( $name:ident : $type:ty ) =>
      $proof:ident
      $( < $( $proof_param:ident ),+ $(,) ? > )?
      ( $( $suchthat:ident $( : $suchtype:ty )? ),* $(,)? );
    )*

  ) => {
    $(
      $crate::exists_single! {
        $exists
        ( $name : $type ) =>
        $proof
        $( < $( $proof_param ),* > )*
        ( $( $suchthat $( : $suchtype )* ),* );
      }
    )*
  }
}

#[macro_export]
macro_rules! exists_single {
  ( $exists:ident
    ( $name:ident : $type:ty ) =>
    $proof:ident
    $( < $( $proof_param:ident ),+ $(,) ? > )?
    ( $( $suchthat:ident $( : $suchtype:ty )? ),* $(,)? )
    $(;)?
  ) => {
    $crate::proof_single! {
      $proof
      $( < $( $proof_param ),* > )?
      ( $name : $type, $( $suchthat $( : $suchtype )? ),* )
    }

    $crate::macros::paste! {
      pub struct [< $exists:camel >]
      <
        [< $name:camel Val >] : $crate::HasType<$type>,
        $( $( $proof_param, )* )?
        $( [< $suchthat:camel Val >] $( : $crate::HasType<$suchtype> )?  ),*
      >
      {
        pub [< $name:snake >] : $crate::Named<
          [< $name:camel Val >],
          $type
        >,
        pub [< $proof:snake >] :
          [< $proof:camel >]
          <
            $( $( $proof_param, )* )?
            [< $name:camel Val >],
            $( [< $suchthat:camel Val >] ),*
          >,
      }

      fn [< new_ $exists:snake >]
      <
        $( $( $proof_param, )* )?
        $( [< $suchthat:camel Val >] $( : $crate::HasType<$suchtype> )?  ),*
      >
      (
        seed : $crate::Seed<impl $crate::Name>,
        [< $name:snake >] : $type,
      ) ->
        [< $exists:camel >]
        < impl $crate::HasType<$type>,
          $( $( $proof_param, )* )?
          $( [< $suchthat:camel Val >] ),*
        >
      {
        [< $exists:camel >] {
          [< $name:snake >]: $crate::Seed::new_named(seed, [< $name:snake >]),
          [< $proof:snake >] : [< $proof:camel >] ( ::core::marker::PhantomData )
        }
      }
    }
  }
}

#[doc = include_str!("../docs/proof_macro.md")]
#[macro_export]
macro_rules! proof {
  ( $(
      $proof:ident
      $( < $( $proof_param:ident ),+ $(,) ? > )?
      ( $( $suchthat:ident $( : $suchtype:ty )? ),* $(,)? );
    )+
  ) => {
    $(
      $crate::proof_single! {
        $proof
        $( < $( $proof_param ),* > )?
        ( $( $suchthat $( : $suchtype )? ),* );
      }
    )*
  }
}

#[macro_export]
macro_rules! proof_single {
  ( $proof:ident
    $( < $( $proof_param:ident ),+ $(,) ? > )?
    ( $( $suchthat:ident $( : $suchtype:ty )? ),* $(,)? )
    $(;)?
  ) => {
    $crate::macros::paste! {
      pub struct [< $proof:camel >] <
        $( $( $proof_param, )* )?
        $( [< $suchthat:camel Val >] $( : $crate::HasType<$suchtype> )?  ),*
      >
      (
        ::core::marker::PhantomData<(
          $( $( $proof_param, )* )?
          $( [< $suchthat:camel Val >] ),*
        )>
      );

      impl
      <
        $( $( $proof_param, )* )?
        $( [< $suchthat:camel Val >] $( : $crate::HasType<$suchtype> )?  ),*
      >
      [< $proof:camel >]
      <
        $( $( $proof_param, )* )?
        $( [< $suchthat:camel Val >]  ),*
      >
      {
        fn new () -> Self
        {
          [< $proof:camel >] (
            ::core::marker::PhantomData
          )
        }
      }
    }
  }
}