package dev.posco.nui

import scala.compiletime.{erasedValue, error, ops, requireConst}

object NatExample {
  sealed trait Nat
  object Nat {
    case object Zero extends Nat
    case class Succ[N <: Nat](prev: N) extends Nat

    given zero: Zero.type = Zero
    given buildSucc[N <: Nat](using n: N): Succ[N] =
      Succ(n)

    def value[N <: Nat](using n: N): N = n

    type FromInt[I <: Int] <: Nat = I match {
      case 0 => Zero.type
      case _ =>
       // commented out trying to get fromInt to work
       // ops.int.<[I, 0] match {
         // case true => Nothing
         // case false =>
            Succ[FromInt[ops.int.-[I, 1]]]
       // }
    }

    inline def fromInt[I <: Int](inline i: I): FromInt[I] = {
      requireConst(i)
      inline i match {
        case _: 0 => Zero
        case _ =>
          inline if i < 0 then error("cannot convert negative to Nat")
          else {
            // obviously the cast is bad
            val prev: ops.int.-[I, 1] = (i - 1).asInstanceOf[ops.int.-[I, 1]]
            // this fails because prev is not a const even though this all should be inlined.
            Succ(fromInt[ops.int.-[I, 1]](prev))
          }
      }
    }
  }
}