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
type FKindTerm = Natural
type FKindType = NaturalK
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
class FKinded (a :: Type) where
type FKindOf (x :: a) :: FKindType
type FKindDefault :: a
printFKind :: a -> FKindTerm
parseFKind :: FKindTerm -> Maybe a
data SingCmp (l :: k) (r :: k)
= SingEq (l :~: r)
| SingLt
| SingGt
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