{-# LANGUAGE DataKinds #-}

-- | This module defines locations and located values.
module Choreography.Location where

import Data.Proxy
import Data.String
import GHC.TypeLits
import Language.Haskell.TH

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

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

-- | Convert a type-level location to a term-level location.
toLocTm :: forall (l :: LocTy). KnownSymbol l => Proxy l -> LocTm
toLocTm :: forall (l :: LocTy). KnownSymbol l => Proxy l -> LocTm
toLocTm = forall (n :: LocTy) (proxy :: LocTy -> *).
KnownSymbol n =>
proxy n -> LocTm
symbolVal

-- | Located values.
--
-- @a \@ l@ represents a value of type @a@ at location @l@.
data a @ (l :: LocTy)
  = Wrap a -- ^ A located value @a \@ l@ from location @l@'s perspective.
  | Empty  -- ^ A located value @a \@ l@ from locations other than @l@'s
           -- perspective.

-- | Wrap a value as a located value.
wrap :: a -> a @ l
wrap :: forall a (l :: LocTy). a -> a @ l
wrap = forall a (l :: LocTy). a -> a @ l
Wrap

-- | Unwrap a located value.
--
-- /Note:/ Unwrapping a empty located value will throw an exception.
unwrap :: a @ l-> a
unwrap :: forall a (l :: LocTy). (a @ l) -> a
unwrap (Wrap a
a) = a
a
unwrap a @ l
Empty    = forall a. HasCallStack => LocTm -> a
error LocTm
"this should never happen for a well-typed choreography"

-- | Define a location at both type and term levels.
mkLoc :: String -> Q [Dec]
mkLoc :: LocTm -> Q [Dec]
mkLoc LocTm
loc = do
  let locName :: Name
locName = LocTm -> Name
mkName LocTm
loc
  let p :: Name
p = LocTm -> Name
mkName LocTm
"Data.Proxy.Proxy"
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [Name -> Type -> Dec
SigD Name
locName (Type -> Type -> Type
AppT (Name -> Type
ConT Name
p) (TyLit -> Type
LitT (LocTm -> TyLit
StrTyLit LocTm
loc))),Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
locName) (Exp -> Body
NormalB (Name -> Exp
ConE Name
p)) []]