-- --< Header >-- {{{
{-#
LANGUAGE
  GADTs, PatternSynonyms, ExplicitNamespaces, QuantifiedConstraints
#-}

{- |

Description : Evidence t'Data.Hetero.Evidence.AtLeast.AtLeast' as strong as that t'Data.Hetero.Evidence.Exactly.Exactly' corresponding to a given t'Data.Hetero.Role.Role'
Copyright   : (c) L. S. Leary, 2025

Evidence t'AtLeast' as strong as that 'Exactly' corresponding to a given 'Data.Hetero.Role.Role'.

-}

-- }}}

-- --< Exports >-- {{{

module Data.Hetero.Evidence.AtLeast (

  -- * AtLeast
  AtLeast(AtLeast, PhantAL, ReprAL, NomAL),
  reflAL,
  symAL,
  transAL,
  hetTransAL,
  maxAL,
  weakenAL,
  weakenALToEx,
  innerAL,

) where

-- }}}

-- --< Imports >-- {{{

-- base
import Prelude hiding (id, (.))
import Data.Type.Equality ((:~:)(..))
import Data.Type.Ord (Max)
import Data.Coerce (Coercible)

-- ord-axiomata
import Data.Type.Ord.Axiomata (type (<=), TotalOrder(..))
import Data.Type.Ord.Lemmata (maxMono)

-- heterogeneous-comparison
import Data.Hetero.Role (RoleKind(..), KnownRole(..), SuperPhantom)
import Data.Hetero.Evidence.Exactly
  (Exactly(..), symEx, maxEx, roleEx, weakenEx, innerEx)
import Data.Hetero.Evidence.AtLeast.Internal

-- }}}

-- --< AtLeast >-- {{{

{-# INLINE PhantAL #-}
{-# INLINE ReprAL  #-}
{-# INLINE NomAL   #-}
{-# COMPLETE PhantAL, ReprAL, NomAL #-}
pattern PhantAL
  :: () =>  r <= Phantom                            => AtLeast r a b
pattern ReprAL
  :: () => (r <= Representational, a `Coercible` b) => AtLeast r a b
pattern NomAL
  :: () => (r <= Nominal         , a      ~      b) => AtLeast r a b
pattern $mPhantAL :: forall {r} {k} {r :: RoleKind} {a :: k} {b :: k}.
AtLeast r a b -> ((r <= Phantom) => r) -> ((# #) -> r) -> r
$bPhantAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Phantom) =>
AtLeast r a b
PhantAL = AtLeast PhantEx
pattern $mReprAL :: forall {r} {k} {r :: RoleKind} {a :: k} {b :: k}.
AtLeast r a b
-> ((r <= Representational, Coercible a b) => r)
-> ((# #) -> r)
-> r
$bReprAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Representational, Coercible a b) =>
AtLeast r a b
ReprAL  = AtLeast ReprEx
pattern $mNomAL :: forall {r} {k} {r :: RoleKind} {a :: k} {b :: k}.
AtLeast r a b -> ((r <= Nominal, a ~ b) => r) -> ((# #) -> r) -> r
$bNomAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
(r <= Nominal, a ~ b) =>
AtLeast r a b
NomAL   = AtLeast NomEx

-- | Symmetry.
symAL :: AtLeast r a b -> AtLeast r b a
symAL :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
AtLeast r a b -> AtLeast r b a
symAL (AtLeast Exactly s a b
ex) = Exactly s b a -> AtLeast r b a
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast (Exactly s a b -> Exactly s b a
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Exactly r b a
symEx Exactly s a b
ex)

{- |

@t'AtLeast' _ a b@ is a monoid graded by the 'Max' monoid on 'RoleKind' with identity:

@
'PhantAL' :: t'AtLeast' t'Phantom' a b
@

-}
maxAL
  :: forall r s a b
  .  (KnownRole r, KnownRole s)
  => AtLeast r a b -> AtLeast s a b {- ^ -}
  -> AtLeast (Max r s) a b
maxAL :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, KnownRole s) =>
AtLeast r a b -> AtLeast s a b -> AtLeast (Max r s) a b
maxAL (AtLeast Exactly s a b
e1) (AtLeast Exactly s a b
e2) = case Proof (Max r s <= Max s s)
mono of
  OrdCond
  (CmpRole
     (OrdCond (CmpRole r s) s s r) (OrdCond (CmpRole s s) s s s))
  'True
  'True
  'False
:~: 'True
Proof (Max r s <= Max s s)
Refl -> Exactly (OrdCond (CmpRole s s) s s s) a b
-> AtLeast (OrdCond (CmpRole r s) s s r) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast (Exactly s a b -> Exactly s a b -> Exactly (Max s s) a b
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
Exactly r a b -> Exactly s a b -> Exactly (Max r s) a b
maxEx Exactly s a b
e1 Exactly s a b
e2)
 where
  mono :: Proof (Max r s <= Max s s)
mono = Sing RoleKind r
-> Sing RoleKind s
-> Sing RoleKind s
-> Sing RoleKind s
-> Proof (Max r s <= Max s s)
forall o (a :: o) (c :: o) (b :: o) (d :: o).
(TotalOrder o, a <= c, b <= d) =>
Sing o a
-> Sing o b -> Sing o c -> Sing o d -> Proof (Max a b <= Max c d)
maxMono
    (forall (r :: RoleKind). KnownRole r => Role r
knownRole @r) (forall (r :: RoleKind). KnownRole r => Role r
knownRole @s)
    (Exactly s a b -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s a b
e1) (Exactly s a b -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s a b
e2)

-- | Weaken evidence for one 'Data.Hetero.Role.Role' to evidence for a lesser @Role@.
weakenAL
  :: forall r s a b
  .  (KnownRole r, KnownRole s, r <= s)
  => AtLeast s a b {- ^ -}
  -> AtLeast r a b
weakenAL :: forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, KnownRole s, r <= s) =>
AtLeast s a b -> AtLeast r a b
weakenAL (AtLeast Exactly s a b
e) = case Proof (r <= s)
trans of
  OrdCond (CmpRole r s) 'True 'True 'False :~: 'True
Proof (r <= s)
Refl -> Exactly s a b -> AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast Exactly s a b
e
 where
  trans :: Proof (r <= s)
trans = Sing RoleKind r
-> Sing RoleKind s -> Sing RoleKind s -> Proof (r <= s)
forall o (a :: o) (b :: o) (c :: o).
(TotalOrder o, a <= b, b <= c) =>
Sing o a -> Sing o b -> Sing o c -> Proof (a <= c)
forall (a :: RoleKind) (b :: RoleKind) (c :: RoleKind).
(a <= b, b <= c) =>
Sing RoleKind a
-> Sing RoleKind b -> Sing RoleKind c -> Proof (a <= c)
transLeq (forall (r :: RoleKind). KnownRole r => Role r
knownRole @r) (forall (r :: RoleKind). KnownRole r => Role r
knownRole @s) (Exactly s a b -> Role s
forall {k} (r :: RoleKind) (a :: k) (b :: k).
Exactly r a b -> Role r
roleEx Exactly s a b
e)

-- | Weaken inexact evidence to exact evidence of the same role.
weakenALToEx :: KnownRole r => AtLeast r a b -> Exactly r a b
weakenALToEx :: forall {k} (r :: RoleKind) (a :: k) (b :: k).
KnownRole r =>
AtLeast r a b -> Exactly r a b
weakenALToEx (AtLeast Exactly s a b
ex) = Exactly s a b -> Exactly r a b
forall {k} (r :: RoleKind) (s :: RoleKind) (a :: k) (b :: k).
(KnownRole r, r <= s) =>
Exactly s a b -> Exactly r a b
weakenEx Exactly s a b
ex

-- | If applications by @'SuperPhantom' f@ are equivalent, then so are the arguments.
innerAL
  :: SuperPhantom f
  => AtLeast r (f a) (f b) {- ^ -}
  -> AtLeast r a b
innerAL :: forall {k} {k} (f :: k -> k) (r :: RoleKind) (a :: k) (b :: k).
SuperPhantom f =>
AtLeast r (f a) (f b) -> AtLeast r a b
innerAL (AtLeast Exactly s (f a) (f b)
ex) = Exactly s a b -> AtLeast r a b
forall {k} (r :: RoleKind) (a :: k) (b :: k) (s :: RoleKind).
(r <= s) =>
Exactly s a b -> AtLeast r a b
AtLeast (Exactly s (f a) (f b) -> Exactly s a b
forall {k1} {k2} (f :: k1 -> k2) (r :: RoleKind) (a :: k1)
       (b :: k1).
SuperPhantom f =>
Exactly r (f a) (f b) -> Exactly r a b
innerEx Exactly s (f a) (f b)
ex)

-- }}}