module Language.Fortran.Repr.Type.Scalar.Common where

import Language.Fortran.Repr.Util
import Language.Fortran.Repr.Compat.Natural

import Data.Kind
import GHC.TypeNats

import Data.Type.Equality
import Data.Ord.Singletons
import Unsafe.Coerce

-- | Fortran kinds are represented by natural numbers. We use them on both type
--   and term levels.
type FKindTerm = Natural
type FKindType = NaturalK

-- | Reify a kind tag to its 'Natural' equivalent.
reifyKinded
    :: forall k (a :: k) n. (n ~ FKindOf a, KnownNat n)
    => Sing a -> FKindTerm
reifyKinded :: forall k (a :: k) (n :: FKindType).
(n ~ FKindOf a, KnownNat n) =>
Sing a -> FKindType
reifyKinded Sing a
_ = forall (a :: FKindType). KnownNat a => FKindType
natVal'' @n

-- | Fortran types which use simple integer kinds.
class FKinded (a :: Type) where
    type FKindOf (x :: a) :: FKindType
    type FKindDefault :: a

    -- | This we get via the type family, but require singletons.
    printFKind :: a -> FKindTerm

    -- | This we *should* get via the type family, but again require singletons.
    parseFKind :: FKindTerm -> Maybe a

{-
-- | Fortran strings
instance FKinded Natural where
    type FKindOf n = n
    type FKindDefault = 1 -- TODO ??
    printFKind = id
    parseFKind = Just
-}

--------------------------------------------------------------------------------

data SingCmp (l :: k) (r :: k)
  = SingEq (l :~: r)
  | SingLt
  | SingGt

-- | Upgrade an 'SOrdering' to include a proof of type equality for the equal
--   case.
--
-- We have no choice but to fake the 'Refl' with 'unsafeCoerce'. But assuming
-- 'SEQ' is used correctly, it should be safe.
singCompare
    :: forall k (a :: k) (b :: k). SOrd k
    => Sing a -> Sing b -> SingCmp a b
singCompare :: forall k (a :: k) (b :: k).
SOrd k =>
Sing a -> Sing b -> SingCmp a b
singCompare Sing a
a Sing b
b =
    case Sing a
a forall a (t1 :: a) (t2 :: a).
SOrd a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2)
`sCompare` Sing b
b of
      Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SEQ -> forall k (l :: k) (r :: k). (l :~: r) -> SingCmp l r
SingEq (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
      Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SLT -> forall k (l :: k) (r :: k). SingCmp l r
SingLt
      Sing (Apply (Apply CompareSym0 a) b)
SOrdering (Compare a b)
SGT -> forall k (l :: k) (r :: k). SingCmp l r
SingGt