import { Nat, NatOf, Suc, Zero, suc, zero } from "./typeLevelNats";

type GenericFunction = (...x: never[]) => unknown;
type Assume<T, U> = T extends U ? T : U;

abstract class TypeFunc<Arg, Ret, Param = unknown> {
  readonly _1?: Param;
  abstract new: (_: Arg) => Ret;
}

type Apply<Arg, Ret, F extends TypeFunc<Arg, Ret>, _1> = ReturnType<
  (F & {
    readonly _1: _1;
  })["new"]
>;

interface GetPrev<N extends Nat> extends TypeFunc<Suc<N>, N> {
  new: (arg: Suc<N>) => N;
}

// nat-elim : (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
// (M : T -> U) -> (cz : M z) -> (sz : (n : N) -> M n -> M (suc n)) -> (n : N) -> M n
//

interface ConstNat extends TypeFunc<any, Nat> {
  new: (_: any) => Nat;
}

type NatElim0<
  M extends TypeFunc<Nat, any>,
  ZCase,
  SCase extends TypeFunc<
    Nat,
    TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>
  >,
  N
> =
  /** --------------------------------------------------------------- */
  N extends Zero // // if N matches Zero
    ? ZCase //   return ZCase
    : N extends Suc<infer Prev> // if N matches Suc(Prev)
    ? Apply<
        any /* TODO: */,
        any /* TODO: */,
        Apply<
          Nat,
          TypeFunc<Apply<Nat, any, M, Nat>, Apply<Nat, any, M, Suc<Nat>>>,
          SCase,
          Prev
        >,
        Apply<Nat, any, M, Prev>
      >
    : never;

/*
export interface DoubleSuc extends TypeFunc<Nat, Nat> {
  new: (arg: Assume<this["_1"], Nat>) => Suc<Suc<typeof arg>>;
}
*/

interface ExampleM extends TypeFunc<Nat, null[]> {
  new: (
    arg: Nat
  ) => typeof arg extends Suc<infer Prev>
    ? ["x", ...Apply<Nat, null[], ExampleM, Prev>]
    : [];
}
export const _1: Apply<Nat, null[], ExampleM, Zero> = [];
export const _2: Apply<Nat, null[], ExampleM, Zero> = [null];

/**
 * M is the type family being mapped over
 * M : (n : N) -> U
 * M zero = Nat
 */
interface DoubleNat_M extends TypeFunc<Nat, any> {
  new: (arg: Nat) => Nat;
  /*
    typeof arg extends Suc<infer Prev>
    ? Suc<Suc<Apply<Nat, Nat, DoubleNat_M, Prev>>>
    : Zero; */
}

/**
 * DoubleNat_SCase_App1 is what happens after applying 1 arg to DoubleNat_SCase
 * (given n : N in the context)
 * SCase_App1 : (prev : M n) -> M (suc n)
 * SCase_App1 prev = prev + 2
 */
interface DoubleNat_SCase_App1<
  M extends TypeFunc<Nat<any>, Nat<any>, any>,
  N extends Nat<P>,
  P = unknown
> extends TypeFunc<
    Apply<Nat<P>, Nat<any>, M, N>,            // (prev : M n)
    Apply<Nat<Suc<P>>, Nat<any>, M, Suc<N>>,  // -> M (suc n)
    Nat<unknown>
  > {
  new: (prev: Assume<this["_1"], Nat<P>>) => Suc<Suc<typeof prev>>;
}

/**
 * This is the suc case for DoubleNat:
 *   SCase : (n : N) -> (prev : M n) -> M (suc n)
 */
interface DoubleNat_SCase<M extends TypeFunc<Nat, Nat>>
  extends TypeFunc<Nat, TypeFunc<Nat, Nat>> {
  new: (arg: Nat) => DoubleNat_SCase_App1<M, typeof arg>;
}
export const _3: Apply<
  Nat,
  Nat,
  Apply<Nat, TypeFunc<Nat, Nat>, DoubleNat_SCase<DoubleNat_M>, NatOf<4>>,
  NatOf<4>
> = suc(suc(suc(suc(suc(suc(zero))))));

function isNatOfFour<T extends NatOf<4>>(_: T) {}
/* 3 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Zero>>>);
/* 4 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Suc<Zero>>>>);
/* 5 */ isNatOfFour(undefined as unknown as Suc<Suc<Suc<Suc<Suc<Zero>>>>>);

interface DoubleNat extends TypeFunc<Nat, Nat> {
  new: (
    arg: Nat
  ) => NatElim0<ConstNat, Zero, DoubleNat_SCase<ConstNat>, typeof arg>;
}

type Two = Suc<Suc<Zero>>;
function isTwo<F extends Two>(_: F) {}
isTwo(suc(zero));
isTwo(suc(suc(zero)));
isTwo(suc(suc(suc(zero))));

const realThree: Suc<Suc<Suc<Zero>>> = suc(suc(suc(zero)));
const realFour: Suc<Suc<Suc<Suc<Zero>>>> = suc(suc(suc(suc(zero))));

function isFour<F extends Apply<Nat, Nat, DoubleNat, Two>>(_: F) {}
isFour(realThree);
isFour(realFour);

/*
interface NatElim<
  MRet,
  M extends TypeFunc<Nat, MRet>,
  ZCase extends Apply<infer A, infer R, M<A, R>, Z>,
  SCase extends TypeFunc
> extends TypeFunc {
  _unused: (_1: ZCase, _2: SCase) => never;
  new: (arg: Assume<this["_1"], Nat>) => Apply<M, typeof arg>;
}
*/

/////

type Length<T extends any[]> = T extends { length: infer L } ? L : never;

type BuildTuple<L extends number, T extends any[] = []> = T extends {
  length: L;
}
  ? T
  : BuildTuple<L, [...T, any]>;

type Add<A extends number, B extends number> = Length<
  [...BuildTuple<A>, ...BuildTuple<B>]
>;

type Equals<T, T1 extends T, T2 extends T> = { eq: [T1, T2] };

type Seven = Add<3, 4>; // 7

function isSeven(s: Seven) {}
isSeven(6);
isSeven(7);

///

class Eq<A, B> {
  private a: (_: A) => A;
  private b: (_: B) => B;
  private constructor() {}
  static refl<T>(): Eq<T, T> {
    return new Eq();
  }
}

function isEqual1(_: Eq<3, 3>) {}
isEqual1(Eq.refl());
function isEqual2(_: Eq<3, 4>) {}
isEqual2(Eq.refl());
function isEqual3(_: Eq<Add<3, 4>, 7>) {}
isEqual3(Eq.refl());
function isEqual4(_: Eq<Add<3, 4>, 8>) {}
isEqual4(Eq.refl());

///

type Commutative<A extends number, B extends number> = Eq<Add<A, B>, Add<B, A>>;
function comm<A extends number, B extends number>(): Commutative<A, B> {
  return Eq.refl();
}