module TypelevelUnits where

import Prelude

import Data.EuclideanRing (class EuclideanRing)
import Data.Tuple (Tuple(..))
import Data.Typelevel.Num.Reps (D1, D0, d0, d1)
import Data.Typelevel.Num.Sets (toInt, class Pos, class Nat)
import Data.Unit (unit)
import Unsafe.Coerce (unsafeCoerce)

undefined :: ∀ a. a
undefined = unsafeCoerce unit

data UnitCons a b = UnitCons a b
infix 6 type UnitCons as .*

data Inverse a = Inverse a

instance showInverse :: (Show a) => Show (Inverse a) where show (Inverse a) = "1/" <> (show a)

type UnitDiv a b = UnitCons a (Inverse b)
infix 7 type UnitDiv as ./


data UnitValue a b = UnitValue a b
infix 5 type UnitValue as :::
infix 5 UnitValue as :::


instance showUnitValue :: (Show a, Show b) => Show (UnitValue a b) where show (UnitValue a b) = (show a) <> " [" <> (show b) <> "]"

data ZeroU
emptyT :: ZeroU
emptyT = undefined

data Meter
meter :: Meter
meter = undefined
data Sec
sec :: Sec
sec = undefined

data Quantity a b = Quantity a b

instance showQuantity :: (Show a, Show b) => Show (Quantity a b) where show (Quantity a b) = (show a) <> "^" <> (show b) <> " "

class Unit a where
  toArray :: a -> Array (Quantity String Int)

instance showMeter :: Show Meter where show _ = "m"
instance showSec :: Show Sec where show _ = "s"
instance showZeroU :: Show ZeroU where show _ = "--"
instance showUnitCons :: (Show a, Show b) => Show (a .* b) where show _ = (show (undefined :: a)) <> "*" <>(show (undefined :: b))

instance unitMeter :: Unit Meter where
  toArray _ = [Quantity "meter" 1]

instance unitSec :: Unit Sec where
  toArray _ = [Quantity "second" 1]

instance unitZeroU :: Unit ZeroU where toArray _ = []

instance unitUnitCons :: (Unit a, Unit b) => Unit (UnitCons a b) where
  toArray _ = (toArray (undefined :: a)) <> (toArray (undefined :: b))

class Eq a b | a -> b

instance equalInverseElement :: (Eq x x') => Eq (x .* ZeroU) x'
instance recurEqual :: (Eq x x', Eq y y', Eq (x' .* y') r) => Eq (x .* y) r
instance eliminateInverse :: (Eq x x') => Eq (x .* (Inverse x')) ZeroU
instance reflEq :: Eq x x

example :: Meter .* Sec
example = undefined

v1 :: Int ::: Meter ./ Sec
v1 = UnitValue 123 (undefined)

v2 :: Meter .* Meter ./ Meter
v2 = undefined

v2_eq :: ∀a. Eq (Meter .* (Meter ./ Meter)) a => a
v2_eq = undefined

multiply :: ∀a b d. Semiring a => a ::: b -> a ::: d -> a ::: (b .* d)
multiply (UnitValue a b) (UnitValue c d) = UnitValue (a+c) (undefined :: b .* d)

divide :: ∀a b d. EuclideanRing a => a ::: b -> a ::: d -> a ::: b ./ d
divide (UnitValue a b) (UnitValue c d) = UnitValue (a/c) (undefined :: b ./ d)

averageVelocity :: Int ::: Meter -> Int ::: Sec -> Int ::: (Meter .* Sec)
averageVelocity a b = multiply a b