{-# LANGUAGE Safe #-}

module Logic.Theory.Arithmetic (
  type Zero (),
  type Zeroable (..),
  sign,
  type Succ (),
  type One,
  type Oneable (..),
  type PositiveOrNull (..),
  type PositiveNonNull (..),
  type NegativeOrNull (..),
  type NegativeNonNull (..),
  type Opposite (),
  type Oppositeable (..),
  type IntMax,
  intMax,
  type (+) (),
) where

import Data.Int (Int)
import Data.Ord qualified as Ord
import Logic.Kernel
import Logic.Theory.Eq
import Logic.Theory.Ord
import Numeric.Natural (Natural)
import Prelude (Integer, maxBound)
import Prelude qualified

data Zero = ZeroAxiom

class Zeroable a where
  zero :: Zero ::: a
  default zero :: Prelude.Num a => Zero ::: a
  zero = ZeroAxiom ... 0
instance Zeroable Int
instance Zeroable Integer
instance Zeroable Natural

newtype Succ n = SuccAxiom n

type One = Succ Zero

class Oneable a where
  one :: One ::: a
  default one :: Prelude.Num a => One ::: a
  one = SuccAxiom ZeroAxiom ... 1
instance Oneable Int
instance Oneable Integer
instance Oneable Natural

class Signable a where
  sign :: x ::: a -> Compare Zero x ::: Ord.Ordering
  default sign :: Ord.Ord a => Prelude.Num a => x ::: a -> Compare Zero x ::: Ord.Ordering
  sign = compare (ZeroAxiom ... 0)
instance Signable Natural
instance Signable Int
instance Signable Integer

newtype PositiveOrNull a x = PositiveOrNull (x ::: a / x >= Zero)
instance Axiom (PositiveOrNull a Zero)
instance Axiom (PositiveOrNull a (Opposite (Zero)))
instance Axiom (PositiveOrNull a (Succ n))

newtype PositiveNonNull a x = PositiveNonNull (x ::: a / x > Zero)
instance Axiom (PositiveNonNull a (Succ n))

newtype NegativeOrNull a x = NegativeOrNull (x ::: a / x <= Zero)
instance Axiom (NegativeOrNull a Zero)
instance Axiom (NegativeOrNull a (Opposite (Zero)))
instance Axiom (NegativeOrNull a (Opposite ((Succ n))))

newtype NegativeNonNull a x = NegativeNonNull (x ::: a / x < Zero)
instance Axiom (NegativeNonNull a (Succ n))

data Opposite n = OppositeAxiom

class Oppositeable a where
  opposite :: x ::: a -> Opposite x ::: a
  opposite (Named x) = OppositeAxiom ... x

instance Oppositeable Int
instance Oppositeable Integer

instance Axiom (Opposite (Opposite (x ::: Integer)) == x)

data IntMax
intMax :: Int
intMax = maxBound

type AxiomUpperBound max i a = (i ::: a) < max -> (i ::: a) < ((i ::: a) + One)
instance Axiom (AxiomUpperBound IntMax i Int)

type AxiomNoUpperBound i a = (i ::: a) < Succ (i ::: a)
instance Axiom (AxiomNoUpperBound i Natural)
instance Axiom (AxiomNoUpperBound i Integer)

data (+) xs ys
type role (+) nominal nominal

-- | `(+)` commutes
instance Axiom (Commutative (+) x y)

-- | `(+)` is associative
instance Axiom (Associative (+) x y z)