-- | Additional functions/relations pertaining to locations and type-level lists of locations.
module Choreography.Locations.Batteries where

import Choreography.Locations
import GHC.TypeLits (KnownSymbol)
import Language.Haskell.TH

-- * Misc

-- | Quickly build membership proofs, when the membership can be directly observed by GHC.
class ExplicitMember (x :: k) (xs :: [k]) where
  explicitMember :: Member x xs

instance {-# OVERLAPPABLE #-} (ExplicitMember x xs) => ExplicitMember x (y ': xs) where
  explicitMember :: Member x (y : xs)
explicitMember = Subset xs (y : xs)
-> forall (x :: a). Member x xs -> Member x (y : xs)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset xs (y : xs)
forall {a} (xs :: [a]) (x :: a) (xs' :: [a]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
consSet Member x xs
forall k (x :: k) (xs :: [k]). ExplicitMember x xs => Member x xs
explicitMember

instance {-# OVERLAPS #-} ExplicitMember x (x ': xs) where
  explicitMember :: Member x (x : xs)
explicitMember = Member x (x : xs)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First

-- | Quickly build subset proofs, when the subset relation can be directly observed by GHC.
class ExplicitSubset xs ys where
  explicitSubset :: Subset xs ys

instance {-# OVERLAPPABLE #-} (ExplicitSubset xs ys, ExplicitMember x ys) => ExplicitSubset (x ': xs) ys where
  explicitSubset :: Subset (x : xs) ys
explicitSubset = Member x ys
forall k (x :: k) (xs :: [k]). ExplicitMember x xs => Member x xs
explicitMember Member x ys -> Subset xs ys -> Subset (x : xs) ys
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset xs ys
forall {k} (xs :: [k]) (ys :: [k]).
ExplicitSubset xs ys =>
Subset xs ys
explicitSubset

instance {-# OVERLAPS #-} ExplicitSubset '[] ys where
  explicitSubset :: Subset '[] ys
explicitSubset = Subset '[] ys
forall k (ys :: [k]). Subset '[] ys
nobody

-- | Alias `refl`. When used as an identifier, this is more descriptive.
allOf :: forall ps. Subset ps ps
allOf :: forall {k} (ps :: [k]). Subset ps ps
allOf = Subset ps ps
forall {k} (ps :: [k]). Subset ps ps
refl

-- | Any element @p@ is a member of the list @'[p]@.
singleton :: forall p. Member p (p ': '[])
singleton :: forall {a} (p :: a). Member p '[p]
singleton = Member p '[p]
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First

-- * Easy indexing with `Member` objects.

-- | A `Member` value for the first item in a list.
--   Note that type-applicaiton is different than with `First`, to which this is otherwise redundant.
listedFirst :: forall p1 ps. Member p1 (p1 ': ps) -- Can we replace all of these with something using off-the-shelf type-level Nats?
listedFirst :: forall a (x :: a) (xs :: [a]). Member x (x : xs)
listedFirst = Member p1 (p1 : ps)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First

-- | A `Member` value for the second item in a list.
listedSecond :: forall p2 p1 ps. Member p2 (p1 ': p2 ': ps)
listedSecond :: forall {a} (p2 :: a) (p1 :: a) (ps :: [a]).
Member p2 (p1 : p2 : ps)
listedSecond = Subset (p2 : ps) (p1 : p2 : ps)
-> forall (x :: a). Member x (p2 : ps) -> Member x (p1 : p2 : ps)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper (Subset (p2 : ps) (p2 : ps) -> Subset (p2 : ps) (p1 : p2 : ps)
forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset (p2 : ps) (p2 : ps)
forall {k} (ps :: [k]). Subset ps ps
refl) Member p2 (p2 : ps)
forall a (x :: a) (xs :: [a]). Member x (x : xs)
listedFirst

-- | A `Member` value for the third item in a list.
listedThird :: forall p3 p2 p1 ps. Member p3 (p1 ': p2 ': p3 ': ps)
listedThird :: forall {a} (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]).
Member p3 (p1 : p2 : p3 : ps)
listedThird = Subset (p2 : p3 : ps) (p1 : p2 : p3 : ps)
-> forall (x :: a).
   Member x (p2 : p3 : ps) -> Member x (p1 : p2 : p3 : ps)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper (Subset (p2 : p3 : ps) (p2 : p3 : ps)
-> Subset (p2 : p3 : ps) (p1 : p2 : p3 : ps)
forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset (p2 : p3 : ps) (p2 : p3 : ps)
forall {k} (ps :: [k]). Subset ps ps
refl) Member p3 (p2 : p3 : ps)
forall {a} (p2 :: a) (p1 :: a) (ps :: [a]).
Member p2 (p1 : p2 : ps)
listedSecond

-- | A `Member` value for the forth item in a list.
listedForth :: forall p4 p3 p2 p1 ps. Member p4 (p1 ': p2 ': p3 ': p4 ': ps)
listedForth :: forall {a} (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]).
Member p4 (p1 : p2 : p3 : p4 : ps)
listedForth = Subset (p2 : p3 : p4 : ps) (p1 : p2 : p3 : p4 : ps)
-> forall (x :: a).
   Member x (p2 : p3 : p4 : ps) -> Member x (p1 : p2 : p3 : p4 : ps)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper (Subset (p2 : p3 : p4 : ps) (p2 : p3 : p4 : ps)
-> Subset (p2 : p3 : p4 : ps) (p1 : p2 : p3 : p4 : ps)
forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset (p2 : p3 : p4 : ps) (p2 : p3 : p4 : ps)
forall {k} (ps :: [k]). Subset ps ps
refl) Member p4 (p2 : p3 : p4 : ps)
forall {a} (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]).
Member p3 (p1 : p2 : p3 : ps)
listedThird

-- | A `Member` value for the fifth item in a list.
listedFifth :: forall p5 p4 p3 p2 p1 ps. Member p5 (p1 ': p2 ': p3 ': p4 ': p5 ': ps)
listedFifth :: forall {a} (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a)
       (ps :: [a]).
Member p5 (p1 : p2 : p3 : p4 : p5 : ps)
listedFifth = Subset (p2 : p3 : p4 : p5 : ps) (p1 : p2 : p3 : p4 : p5 : ps)
-> forall (x :: a).
   Member x (p2 : p3 : p4 : p5 : ps)
   -> Member x (p1 : p2 : p3 : p4 : p5 : ps)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper (Subset (p2 : p3 : p4 : p5 : ps) (p2 : p3 : p4 : p5 : ps)
-> Subset (p2 : p3 : p4 : p5 : ps) (p1 : p2 : p3 : p4 : p5 : ps)
forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset (p2 : p3 : p4 : p5 : ps) (p2 : p3 : p4 : p5 : ps)
forall {k} (ps :: [k]). Subset ps ps
refl) Member p5 (p2 : p3 : p4 : p5 : ps)
forall {a} (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a) (ps :: [a]).
Member p4 (p1 : p2 : p3 : p4 : ps)
listedForth

-- | A `Member` value for the sixth item in a list.
listedSixth :: forall p6 p5 p4 p3 p2 p1 ps. Member p6 (p1 ': p2 ': p3 ': p4 ': p5 ': p6 ': ps)
listedSixth :: forall {a} (p6 :: a) (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a)
       (p1 :: a) (ps :: [a]).
Member p6 (p1 : p2 : p3 : p4 : p5 : p6 : ps)
listedSixth = Subset
  (p2 : p3 : p4 : p5 : p6 : ps) (p1 : p2 : p3 : p4 : p5 : p6 : ps)
-> forall (x :: a).
   Member x (p2 : p3 : p4 : p5 : p6 : ps)
   -> Member x (p1 : p2 : p3 : p4 : p5 : p6 : ps)
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper (Subset (p2 : p3 : p4 : p5 : p6 : ps) (p2 : p3 : p4 : p5 : p6 : ps)
-> Subset
     (p2 : p3 : p4 : p5 : p6 : ps) (p1 : p2 : p3 : p4 : p5 : p6 : ps)
forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset (p2 : p3 : p4 : p5 : p6 : ps) (p2 : p3 : p4 : p5 : p6 : ps)
forall {k} (ps :: [k]). Subset ps ps
refl) Member p6 (p2 : p3 : p4 : p5 : p6 : ps)
forall {a} (p5 :: a) (p4 :: a) (p3 :: a) (p2 :: a) (p1 :: a)
       (ps :: [a]).
Member p5 (p1 : p2 : p3 : p4 : p5 : ps)
listedFifth

-- * Context manipulation

-- | Use any membership proof to to safely call code that only works on a non-empy list.
quorum1 ::
  forall ps p a.
  (KnownSymbols ps) =>
  Member p ps ->
  (forall q qs. (KnownSymbol q, KnownSymbols qs, ps ~ q ': qs) => a) ->
  a
quorum1 :: forall (ps :: [Symbol]) (p :: Symbol) a.
KnownSymbols ps =>
Member p ps
-> (forall (q :: Symbol) (qs :: [Symbol]).
    (KnownSymbol q, KnownSymbols qs, ps ~ (q : qs)) =>
    a)
-> a
quorum1 Member p ps
p forall (q :: Symbol) (qs :: [Symbol]).
(KnownSymbol q, KnownSymbols qs, ps ~ (q : qs)) =>
a
a = case (Member p ps
p, forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @ps) of
  (Member p ps
First, TySpine ps
TyCons) -> a
forall (q :: Symbol) (qs :: [Symbol]).
(KnownSymbol q, KnownSymbols qs, ps ~ (q : qs)) =>
a
a
  (Later Member p xs1
_, TySpine ps
TyCons) -> a
forall (q :: Symbol) (qs :: [Symbol]).
(KnownSymbol q, KnownSymbols qs, ps ~ (q : qs)) =>
a
a

-- * Template Haskell

-- | Declare a proof-value with the given string as the variable name, proving that that string is a member of any list in which it explicitly apprears.
mkLoc :: String -> Q [Dec]
mkLoc :: String -> Q [Dec]
mkLoc String
loc = do
  let locName :: Name
locName = String -> Name
mkName String
loc
  let tvar :: Name
tvar = String -> Name
mkName String
"xs"
  let m :: Name
m = String -> Name
mkName String
"Member"
  let eM :: Name
eM = String -> Name
mkName String
"ExplicitMember"
  let em :: Name
em = String -> Name
mkName String
"explicitMember"
  [Dec] -> Q [Dec]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    [ Name -> Type -> Dec
SigD
        Name
locName
        ( [TyVarBndr Specificity] -> Cxt -> Type -> Type
ForallT
            [Name -> Specificity -> TyVarBndr Specificity
forall flag. Name -> flag -> TyVarBndr flag
PlainTV Name
tvar Specificity
SpecifiedSpec]
            [Type -> Type -> Type
AppT (Type -> Type -> Type
AppT (Name -> Type
ConT Name
eM) (TyLit -> Type
LitT (String -> TyLit
StrTyLit String
loc))) (Name -> Type
VarT Name
tvar)]
            (Type -> Type -> Type
AppT (Type -> Type -> Type
AppT (Name -> Type
ConT Name
m) (TyLit -> Type
LitT (String -> TyLit
StrTyLit String
loc))) (Name -> Type
VarT Name
tvar))
        ),
      Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
locName) (Exp -> Body
NormalB (Name -> Exp
VarE Name
em)) []
    ]