use core::marker::PhantomData;

/**
 A marker trait that is used to represent unique type in Rust.
 `mononym` guarantees that any two `impl Name` generated by
 the library are always considered distinct types by Rust.

 This is mainly used as a type parameter inside types such as
 [`Seed`]. For example, the type `Seed<impl Name>`
 is used to represent a unique seed type with a fresh type
 `impl Name` being its name.
*/
pub trait Name: Send + Sync + Sealed
{
}

/**
 A marker trait that is used to mark a type-level name being bound to
 a Rust value of the given type `T`. This helps ensure that functions
 that are generic over type-level names are "well-typed", with
 each name "having" their own type through `HasType`.

 With `Name` being a supertrait of `HasType`, this means that any
 name type can have their "type" erased by downcasting the type from
 `impl HasType<T>` to `impl Name`.

 This trait is used as a type parameter inside [`Named`], so that the
 type `Named<impl HasType<T>, T>` also attaches the type information
 to the type-level name associated with the named value.
*/
pub trait HasType<T>: Name
{
}

/**
 Represents a named value with a unique type-level name. `monoym`
 guarantees that there can never be two Rust values of the same
 type `Named<N, T>`. With that, the name type `N` can be used to
 uniquely identify the underlying value at the type level.

 To ensure that functions that are generic over names are well-typed
 `Named` also requires the name type `N` to satisfy the trait bound
 [`HasType<T>`]. Although this may introduce more boilerplate,
 it also helps programmers to always annotate the type of names
 when defining new generic functions.
*/
pub struct Named<N: HasType<T>, T>(T, PhantomData<N>);

/**
 A unique seed type for generating new unique names. `mononym`
 guarantees that there can never be two seed value of the same type
 `Seed<N>` with the same name type `N`.

 A `Seed` value is required to generate new names for values to be
 used in types such as [`Named`]. A seed value can be obtained by
 either making functions accept a `Seed<impl Name>` as its argument,
 or creating fresh `Seed` value using [`with_seed`].
*/
pub struct Seed<N>(PhantomData<N>);

/**
 Turns a lifetime `'name` into a unique type `Life<'name>`
 with an invariant phantom lifetime. `Life` implements [`Name`]
 so that it can be turned into a unique `impl Name`.

 The body [`PhantomData`] has a phantom type `*mut &'name ()`
 to ensure that overlapping lifetimes such as
 `'name1: 'name2` are treated as distinct types and cannot be
 coerced into one another, unless they are exactly the same.

 For example, the following test should fail:

 ```rust,compile_fail
 # use mononym::*;
 fn same<T>(_: T, _: T) {}
 fn same_life<'name1, 'name2: 'name1>(
   life1: Life<'name1>,
   life2: Life<'name2>
 ) {
   same(life1, life2); // error
 }
 ```
*/
pub struct Life<'name>(PhantomData<*mut &'name ()>);

struct SomeName<N>(PhantomData<N>);

impl<N: HasType<T>, T> Named<N, T>
{
  /**
   Get a reference to the underlying value of the named value.
   `mononym` does not provide access to mutable reference to
   the underlying value, as mutation may invalidate the proofs
   of pre-conditions constructed from the original value.

   When using `Named`, it is up to the user to ensure that there
   is no accidental
   [interior mutability](https://doc.rust-lang.org/reference/interior-mutability.html)
   provided by the value type `T`. Otherwise, user must take
   into consideration of the possibility of interior mutability
   and ensure that the invariants assumed by the proofs defined
   cannot be violated.
  */
  pub fn value<'a>(&'a self) -> &'a T
  {
    &self.0
  }

  /**
   Consume the named value and turn it back into the underlying value.
   After this, the underlying value is no longer associated with the
   type-level name, and can be safely mutated.

   Even though the named value is destroyed, the type-level name
   can still continue to present in other places such as proof objects.
   This can be useful for functions that only require proofs about
   a value, without requiring access to the value itself.
  */
  pub fn into_value(self) -> T
  {
    self.0
  }
}

impl<N> Seed<N>
{
  /**
   Consumes the seed and returns a value with a unique type
   `impl Name`. The value on its own do not have much use,
   however it can be used as a proxy type for users to
   define their own name-based abstractions.
  */
  pub fn new_name(self) -> impl Name
  {
    unsafe_new_name(|| {})
  }

  /**
   Consumes the seed and a value of type `T` and turn it into
   a named value [`Named<impl HasType<T>, T>`]. The returned
   named value have a unique type-level name that implements
   both [`Name`] and [`HasType<T>`].
  */
  pub fn new_named<T>(
    self,
    value: T,
  ) -> Named<impl HasType<T>, T>
  {
    unsafe_new_named(unsafe_new_name_with_type(|| {}), value)
  }

  /**
   Consumes the seed and returns two new seeds `Seed<impl Name>`
   with unique names and thus of different types.

   `mononym` guarantees that each replicated seed will generate
   different names, thereby guarantee that the names are always
   unique.

   For example, the following code should fail with compile error:

   ```rust,compile_fail
   # use mononym::*;
   fn same<T>(_: T, _: T) {}
   fn test(seed: Seed<impl Name>) {
     let (seed1, seed2) = seed.replicate();
     same(seed1, seed2); // error
     same(seed1.new_named(()), seed2.new_named(())); // error
   }
   ```

   For convenience, `mononym` also provides the replicate functions
   from [`Seed::replicate_3`] up to [`Seed::replicate_8`] to allow
   easy replication of the seed for 2-8 times. User can call the
   replicate functions multiple times if they need more than
   8 seed replications, which should be rarely happen.
  */
  pub fn replicate(self) -> (Seed<impl Name>, Seed<impl Name>)
  {
    (unsafe_new_seed(|| {}), unsafe_new_seed(|| {}))
  }
}

/**
 This trait is not exported so that the Name trait
 becomes a [_sealed trait_](https://rust-lang.github.io/api-guidelines/future-proofing.html)
 which user cannot provide custom implementation to.
*/
pub trait Sealed
{
}

impl<N> Sealed for SomeName<N> where N: Send + Sync {}

impl<N> Name for SomeName<N> where N: Send + Sync {}

impl<N, T> HasType<T> for SomeName<N> where N: Send + Sync {}

unsafe impl<'name> Send for Life<'name> {}

unsafe impl<'name> Sync for Life<'name> {}

impl<'name> Sealed for Life<'name> {}

impl<'name> Name for Life<'name> {}

/**
 Provides the continuation closure with a unique [`Seed`] with a unique lifetime
 `'name` and a unique name [`Life<'name>`](Life).

 This is achieved using
 [higher-ranked trait bounds](https://doc.rust-lang.org/nomicon/hrtb.html)
 by requiring the continuation closure to work for all lifetime `'name`.

 It is safe to have multiple nested calls to `with_seed`, as each call
 will generate new seed type with a unique `'name` lifetime. For example,
 the following code should fail to compile:

 ```rust,compile_fail
 # use mononym::*;
 fn same<T>(_: T, _: T) {}
 with_seed(|seed1| {
   with_seed(|seed2| {
     same(seed1, seed2); // error
     same(seed1.new_named(1), seed2.new_named(1)); // error
   });
 });
 ```

 The function allows the continuation closure to return any concrete type
 `R`, provided that the return type `R` does not depend on the provided
 `Seed` type in some way. This means that types such as [`Name`],
 [`Named`], and [`Seed`] cannot be used as a return value, as Rust
 consider that as allowing the lifetime `'name` to escape. For example,
 the following code should fail to compile:

 ```rust,compile_fail
 # use mononym::*;
 let res = with_seed(|seed| { seed.new_named(42).into_value() }); // ok
 let res = with_seed(|seed| { seed }); // error
 let res = with_seed(|seed| { seed.new_name() }); // error
 let res = with_seed(|seed| { seed.new_named(42) }); // error
 ```
*/
pub fn with_seed<R>(cont: impl for<'name> FnOnce(Seed<Life<'name>>) -> R) -> R
{
  cont(Seed(PhantomData))
}

fn unsafe_new_name<F>(_: F) -> impl Name
where
  F: Send + Sync,
{
  SomeName(PhantomData::<F>)
}

fn unsafe_new_name_with_type<F, T>(_: F) -> impl HasType<T>
where
  F: Send + Sync,
{
  SomeName(PhantomData::<F>)
}

fn unsafe_new_seed<F>(_: F) -> Seed<impl Name>
where
  F: Send + Sync,
{
  Seed(PhantomData::<SomeName<F>>)
}

fn unsafe_new_named<Name: HasType<T>, T>(
  _: Name,
  value: T,
) -> Named<Name, T>
{
  Named(value, PhantomData)
}

impl<N: Name> Seed<N>
{
  pub fn replicate_3(
    self
  ) -> (Seed<impl Name>, Seed<impl Name>, Seed<impl Name>)
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }

  pub fn replicate_4(
    self
  ) -> (
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
  )
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }

  pub fn replicate_5(
    self
  ) -> (
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
  )
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }

  pub fn replicate_6(
    self
  ) -> (
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
  )
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }

  pub fn replicate_7(
    self
  ) -> (
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
  )
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }

  pub fn replicate_8(
    self
  ) -> (
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
    Seed<impl Name>,
  )
  {
    (
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
      unsafe_new_seed(|| {}),
    )
  }
}