-- | This module defines locations (AKA parties)
--   and functions/relations pertaining to type-level lists of locations.
module Choreography.Locations where

import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)

-- * Type aliases

-- | Term-level locations.
type LocTm = String

-- | Type-level locations.
type LocTy = Symbol

-- * Membership and Subset proofs

-- | A term-level proof that a `LocTy` is a member of a @[LocTy]@.
--   These are frequently used both for proofs /per se/ and to identify individuals in lists of locations.
--
--   For example: @player :: Member players census@ is a proof that the type-level `Symbol`, @player@, is in @census@,
--   and it can also be used as a __term-level__ identifier for the __type-level__ @player@,
--   similar to how a @proxy@ might be used.
--
--   Pattern matching on these values is like pattern matching on a successor-based @Nat@;
--   in this sense a @Member x xs@ is an index into @xs@ at which @x@ can be found.
data Member (x :: k) (xs :: [k]) where
  First :: forall xs x xs'. (xs ~ (x ': xs')) => Member x (x ': xs')
  Later :: Member x xs -> Member x (y ': xs)

-- | A term level proof that one type-level list represents a subset of another,
--   embodied by a total function from proof-of-membership in the sublist to proof-of-membership in the superlist.
--   (If you make one with a partial funciton, all bets are off.)
newtype Subset xs ys = Subset
  { -- | Convert a proof of membership in the sublist to a proof of membership in the superlist.
    -- Frequently used to show that a location is part of a larger set of locations.
    forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper :: forall x. Member x xs -> Member x ys
  }

-- | The subset relation is reflexive.
refl :: Subset xs xs
refl :: forall {k} (xs :: [k]). Subset xs xs
refl = (forall (x :: k). Member x xs -> Member x xs) -> Subset xs xs
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset Member x xs -> Member x xs
forall (x :: k). Member x xs -> Member x xs
forall a. a -> a
id

-- | The sublist relation is transitive.
transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs
transitive :: forall {k} (xs :: [k]) (ys :: [k]) (zs :: [k]).
Subset xs ys -> Subset ys zs -> Subset xs zs
transitive Subset xs ys
sxy Subset ys zs
syz = (forall (x :: k). Member x xs -> Member x zs) -> Subset xs zs
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset ((forall (x :: k). Member x xs -> Member x zs) -> Subset xs zs)
-> (forall (x :: k). Member x xs -> Member x zs) -> Subset xs zs
forall a b. (a -> b) -> a -> b
$ Subset ys zs -> forall (x :: k). Member x ys -> Member x zs
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset ys zs
syz (Member x ys -> Member x zs)
-> (Member x xs -> Member x ys) -> Member x xs -> Member x zs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset xs ys
sxy

-- | The `[]` case of subset proofs.
-- Typlically used to build subset proofs using membership proofs using `@@`.
nobody :: Subset '[] ys
nobody :: forall {k} (ys :: [k]). Subset '[] ys
nobody = (forall (x :: k). Member x '[] -> Member x ys) -> Subset '[] ys
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset \case {}

-- | Any lists is a subset of the list made by consing itself with any other item.
consSet :: forall xs x xs'. (xs ~ (x ': xs')) => Subset xs' (x ': xs')
consSet :: forall {a} (xs :: [a]) (x :: a) (xs' :: [a]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
consSet = (forall (x :: a). Member x xs' -> Member x (x : xs'))
-> Subset xs' (x : xs')
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset Member x xs' -> Member x (x : xs')
forall (x :: a). Member x xs' -> Member x (x : xs')
forall {k} (x :: k) (h :: [k]) (ts :: k).
Member x h -> Member x (ts : h)
Later

-- | Cons an element to the superset in a t`Subset` value.
consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys)
consSuper :: forall {a} (xs :: [a]) (ys :: [a]) (y :: a).
Subset xs ys -> Subset xs (y : ys)
consSuper Subset xs ys
sxy = Subset xs ys -> Subset ys (y : ys) -> Subset xs (y : ys)
forall {k} (xs :: [k]) (ys :: [k]) (zs :: [k]).
Subset xs ys -> Subset ys zs -> Subset xs zs
transitive Subset xs ys
sxy Subset ys (y : ys)
forall {a} (xs :: [a]) (x :: a) (xs' :: [a]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
consSet

-- | Cons an element to the subset in a t`Subset` value;
--   requires proof that the new head element is already a member of the superset.
--   Used like ":" for subset proofs.
--   Suppose you have @(alice :: Member "Alice" census)@
--   and we want a /subset/ proof instead of membership; we can write:
--
--   >>> proof :: Subset '["Alice"] census = alice @@ nobody
(@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys

infixr 5 @@

Member x ys
mxy @@ :: forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset xs ys
sxy = (forall (x :: k). Member x (x : xs) -> Member x ys)
-> Subset (x : xs) ys
forall {k} (xs :: [k]) (ys :: [k]).
(forall (x :: k). Member x xs -> Member x ys) -> Subset xs ys
Subset \case
  Member x (x : xs)
First -> Member x ys
Member x ys
mxy
  Later Member x xs
mxxs -> Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset xs ys
sxy Member x xs
Member x xs
mxxs

-- * Accessing parties' names

-- | Convert a proof-level location to a term-level location.
toLocTm ::
  forall (l :: LocTy) (ps :: [LocTy]).
  (KnownSymbol l) =>
  Member l ps ->
  LocTm
toLocTm :: forall (l :: LocTy) (ps :: [LocTy]).
KnownSymbol l =>
Member l ps -> LocTm
toLocTm Member l ps
_ = Proxy l -> LocTm
forall (n :: LocTy) (proxy :: LocTy -> *).
KnownSymbol n =>
proxy n -> LocTm
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: LocTy). Proxy t
Proxy @l)

-- | Get the term-level list of names-as-strings for a proof-level list of parties.
toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). (KnownSymbols ls) => Subset ls ps -> [LocTm]
toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]).
KnownSymbols ls =>
Subset ls ps -> [LocTm]
toLocs Subset ls ps
_ = case forall (ls :: [LocTy]). KnownSymbols ls => TySpine ls
tySpine @ls of -- this could be golfed by Quire, if that were defined here.
  TySpine ls
TyNil -> []
  TySpine ls
TyCons -> Member h (h : ts) -> LocTm
forall (l :: LocTy) (ps :: [LocTy]).
KnownSymbol l =>
Member l ps -> LocTm
toLocTm (forall (h :: [LocTy]) (x :: LocTy) (ts :: [LocTy]).
(h ~ (x : ts)) =>
Member x (x : ts)
forall {a} (h :: [a]) (x :: a) (ts :: [a]).
(h ~ (x : ts)) =>
Member x (x : ts)
First @ls) LocTm -> [LocTm] -> [LocTm]
forall a. a -> [a] -> [a]
: Subset ts (h : ts) -> [LocTm]
forall (ls :: [LocTy]) (ps :: [LocTy]).
KnownSymbols ls =>
Subset ls ps -> [LocTm]
toLocs (forall (xs :: [LocTy]) (x :: LocTy) (xs' :: [LocTy]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
forall {a} (xs :: [a]) (x :: a) (xs' :: [a]).
(xs ~ (x : xs')) =>
Subset xs' (x : xs')
consSet @ls)

-- * Handling type-level lists literals

-- $Handling
--
-- `KnownSymbols` constraints will often need to be declared in user code,
-- but using `tySpine` should only be necessary
-- when the behavior of the choreography depends on the structure of the type-level lists.
-- Most of the time the functions in "Choreography.Polymorphism" should do this for you.

-- | Term-level markers of the spine/structure of a type-level list.
--   Pattern matching on them recovers both the spine of the list and, if applicable,
--   `KnownSymbol`[@s@] instances for the head and tail.
data TySpine ps where
  -- | Denotes that the list has a head and tail, and exposes `KnownSymbol` and `KnownSymbols` constraints respectively.
  TyCons :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts)
  -- | Denotes that the list is empty.
  TyNil :: TySpine '[]

-- | The type-level-list version of `GHC.TypeList.KnownSymbol`.
--   Denotes that both the spine of the list and each of its elements is known at compile-time.
--   This knowlege is typically recovered by recursively pattern-matching on @tySpine \@ls@.
class KnownSymbols ls where
  -- | Pattern matching on @tySpine \@ls@ will normally have two cases, for when @ls@ is empty or not.
  --   Contextual knowledge may let one or the other case be skipped.
  --   Within those cases, the knowledge afforded by `tySpine`'s constructors can be used.
  tySpine :: TySpine ls

instance KnownSymbols '[] where
  tySpine :: TySpine '[]
tySpine = TySpine '[]
TyNil

instance (KnownSymbols ls, KnownSymbol l) => KnownSymbols (l ': ls) where
  tySpine :: TySpine (l : ls)
tySpine = TySpine (l : ls)
forall (h :: LocTy) (ts :: [LocTy]).
(KnownSymbol h, KnownSymbols ts) =>
TySpine (h : ts)
TyCons