{-# language DataKinds            #-}
{-# language FlexibleInstances    #-}
{-# language PolyKinds            #-}
{-# language ScopedTypeVariables  #-}
{-# language TypeApplications     #-}
{-# language TypeFamilies         #-}
{-# language TypeOperators        #-}
{-# language UndecidableInstances #-}
{-|
Description : Definition of schemas

This module gives a set of combinators
to define schemas in the sense of Avro
or Protocol Buffers.

In order to re-use definitions at both
the type and term levels, the actual
constructors are defined in types ending
with @B@, and are parametrized by the type
used to describe identifiers.
The versions without the suffix set this
parameter to 'Type', and are thought as the
API to be used in the type-level.
If you use 'reflectSchema' to obtain a term-
level representation, the parameter is set
to 'TypeRep'.
-}
module Mu.Schema.Definition (
-- * Definition of schemas
  Schema', Schema, SchemaB
, TypeDef, TypeDefB(..)
, ChoiceDef(..)
, FieldDef, FieldDefB(..)
, FieldType, FieldTypeB(..)
, (:/:)
-- * One-to-one mappings
, Mapping(..), Mappings
-- ** Finding correspondences
, MappingRight, MappingLeft
-- * Reflection to term-level
, reflectSchema
, reflectFields, reflectChoices
, reflectFieldTypes, reflectFieldType
-- * Supporting type classes
, KnownName(..)
) where

import           Data.Kind
import           Data.Proxy
import           Data.Typeable
import           GHC.TypeLits

-- | A set of type definitions,
--   where the names of types and fields are
--   defined by type-level strings ('Symbol's).
type Schema' = Schema Symbol Symbol

-- | Type names and field names can be of any
--   kind, but for many uses we need a way
--   to turn them into strings at run-time.
--   This class generalizes 'KnownSymbol'.
class KnownName (a :: k) where
  nameVal :: proxy a -> String
instance KnownSymbol s => KnownName (s :: Symbol) where
  nameVal :: proxy s -> String
nameVal = proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal
instance KnownName 'True where
  nameVal :: proxy 'True -> String
nameVal proxy 'True
_ = String
"True"
instance KnownName 'False where
  nameVal :: proxy 'False -> String
nameVal proxy 'False
_ = String
"False"
instance KnownNat n => KnownName (n :: Nat) where
  nameVal :: proxy n -> String
nameVal = Integer -> String
forall a. Show a => a -> String
show (Integer -> String) -> (proxy n -> Integer) -> proxy n -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal

-- | A set of type definitions.
--   In general, we can use any kind we want for
--   both type and field names, although in practice
--   you always want to use 'Symbol'.
type Schema typeName fieldName
  = SchemaB Type typeName fieldName
-- | A set of type definitions,
--   parametric on type representations.
type SchemaB builtin typeName fieldName
  = [TypeDefB builtin typeName fieldName]

-- | Defines a type in a schema.
--   Each type can be:
--   * a record: a list of key-value pairs,
--   * an enumeration: an element of a list of choices,
--   * a reference to a primitive type.
type TypeDef = TypeDefB Type
-- | Defines a type in a schema,
--   parametric on type representations.
data TypeDefB builtin typeName fieldName
  = -- | A list of key-value pairs.
    DRecord typeName [FieldDefB builtin typeName fieldName]
    -- | An element of a list of choices.
  | DEnum   typeName [ChoiceDef fieldName]
    -- | A reference to a primitive type.
  | DSimple (FieldTypeB builtin typeName)

-- | Defines each of the choices in an enumeration.
newtype ChoiceDef fieldName
  = -- | One single choice from an enumeration.
    ChoiceDef fieldName

-- | Defines a field in a record
--   by a name and the corresponding type.
type FieldDef = FieldDefB Type
-- | Defines a field in a record,
--   parametric on type representations.
data FieldDefB builtin typeName fieldName
  = -- | One single field in a record.
    FieldDef fieldName (FieldTypeB builtin typeName)

-- | Types of fields of a record.
--   References to other types in the same schema
--   are done via the 'TSchematic' constructor.
type FieldType = FieldTypeB Type
-- | Types of fields of a record,
--   parametric on type representations.
data FieldTypeB builtin typeName
  = -- | Null, as found in Avro.
    TNull
    -- | Reference to a primitive type, such as integers or Booleans.
    --   The set of supported primitive types depends on the protocol.
  | TPrimitive builtin
    -- | Reference to another type in the schema.
  | TSchematic typeName
    -- | Optional value.
  | TOption (FieldTypeB builtin typeName)
    -- | List of values.
  | TList   (FieldTypeB builtin typeName)
    -- | Map of values.
    --   The set of supported key types depends on the protocol.
  | TMap    (FieldTypeB builtin typeName) (FieldTypeB builtin typeName)
    -- | Represents a choice between types.
  | TUnion  [FieldTypeB builtin typeName]

instance KnownName n => KnownName ('DRecord n fields) where
  nameVal :: proxy ('DRecord n fields) -> String
nameVal proxy ('DRecord n fields)
_ = Proxy n -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
instance KnownName n => KnownName ('DEnum n choices) where
  nameVal :: proxy ('DEnum n choices) -> String
nameVal proxy ('DEnum n choices)
_ = Proxy n -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
instance KnownName n => KnownName ('ChoiceDef n) where
  nameVal :: proxy ('ChoiceDef n) -> String
nameVal proxy ('ChoiceDef n)
_ = Proxy n -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
instance KnownName n => KnownName ('FieldDef n t) where
  nameVal :: proxy ('FieldDef n t) -> String
nameVal proxy ('FieldDef n t)
_ = Proxy n -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy n
forall k (t :: k). Proxy t
Proxy @n)

-- | Lookup a type in a schema by its name.
type family (sch :: Schema t f) :/: (name :: t) :: TypeDef t f where
  '[] :/: name = TypeError ('Text "Cannot find type " ':<>: 'ShowType name ':<>: 'Text " in the schema")
  ('DRecord name fields  ': rest) :/: name = 'DRecord name fields
  ('DEnum   name choices ': rest) :/: name = 'DEnum   name choices
  (other                 ': rest) :/: name = rest :/: name

-- | Defines a mapping between two elements.
data Mapping  a b = a :-> b
-- | Defines a set of mappings between elements of @a@ and @b@.
type Mappings a b = [Mapping a b]

-- | Finds the corresponding right value of @v@
--   in a mapping @ms@. When the kinds are 'Symbol',
--   return the same value if not found.
--   When the return type is 'Type', return ' ()'
--   if the value is not found.
type family MappingRight (ms :: Mappings a b) (v :: a) :: b where
  MappingRight '[] (v :: Symbol) = (v :: Symbol)
  MappingRight '[] (v :: Symbol) = (() :: Type)
  MappingRight '[] v             = TypeError ('Text "Cannot find value " ':<>: 'ShowType v)
  MappingRight ((x ':-> y) ': rest) x = y
  MappingRight (other      ': rest) x = MappingRight rest x

-- | Finds the corresponding left value of @v@
--   in a mapping @ms@. When the kinds are 'Symbol',
--   return the same value if not found.
--   When the return type is 'Type', return ' ()'
--   if the value is not found.
type family MappingLeft (ms :: Mappings a b) (v :: b) :: a where
  MappingLeft '[] (v :: Symbol) = (v :: Symbol)
  MappingLeft '[] (v :: Symbol) = (() :: Type)
  MappingLeft '[] v             = TypeError ('Text "Cannot find value " ':<>: 'ShowType v)
  MappingLeft ((x ':-> y) ': rest) y = x
  MappingLeft (other      ': rest) y = MappingLeft rest y

class ReflectSchema (s :: Schema tn fn) where
  -- | Reflect a schema into term-level.
  reflectSchema :: Proxy s -> SchemaB TypeRep String String
instance ReflectSchema '[] where
  reflectSchema :: Proxy '[] -> SchemaB TypeRep String String
reflectSchema Proxy '[]
_ = []
instance (ReflectFields fields, KnownName name, ReflectSchema s)
         => ReflectSchema ('DRecord name fields ': s) where
  reflectSchema :: Proxy ('DRecord name fields : s) -> SchemaB TypeRep String String
reflectSchema Proxy ('DRecord name fields : s)
_ = String
-> [FieldDefB TypeRep String String]
-> TypeDefB TypeRep String String
forall builtin typeName fieldName.
typeName
-> [FieldDefB builtin typeName fieldName]
-> TypeDefB builtin typeName fieldName
DRecord (Proxy name -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name)) (Proxy fields -> [FieldDefB TypeRep String String]
forall tn fn (fs :: [FieldDef tn fn]).
ReflectFields fs =>
Proxy fs -> [FieldDefB TypeRep String String]
reflectFields (Proxy fields
forall k (t :: k). Proxy t
Proxy @fields))
                  TypeDefB TypeRep String String
-> SchemaB TypeRep String String -> SchemaB TypeRep String String
forall a. a -> [a] -> [a]
: Proxy s -> SchemaB TypeRep String String
forall tn fn (s :: Schema tn fn).
ReflectSchema s =>
Proxy s -> SchemaB TypeRep String String
reflectSchema (Proxy s
forall k (t :: k). Proxy t
Proxy @s)
instance (ReflectChoices choices, KnownName name, ReflectSchema s)
         => ReflectSchema ('DEnum name choices ': s) where
  reflectSchema :: Proxy ('DEnum name choices : s) -> SchemaB TypeRep String String
reflectSchema Proxy ('DEnum name choices : s)
_ = String -> [ChoiceDef String] -> TypeDefB TypeRep String String
forall builtin typeName fieldName.
typeName
-> [ChoiceDef fieldName] -> TypeDefB builtin typeName fieldName
DEnum (Proxy name -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name)) (Proxy choices -> [ChoiceDef String]
forall fn (cs :: [ChoiceDef fn]).
ReflectChoices cs =>
Proxy cs -> [ChoiceDef String]
reflectChoices (Proxy choices
forall k (t :: k). Proxy t
Proxy @choices))
                  TypeDefB TypeRep String String
-> SchemaB TypeRep String String -> SchemaB TypeRep String String
forall a. a -> [a] -> [a]
: Proxy s -> SchemaB TypeRep String String
forall tn fn (s :: Schema tn fn).
ReflectSchema s =>
Proxy s -> SchemaB TypeRep String String
reflectSchema (Proxy s
forall k (t :: k). Proxy t
Proxy @s)
instance (ReflectFieldType ty, ReflectSchema s)
         => ReflectSchema ('DSimple ty ': s) where
  reflectSchema :: Proxy ('DSimple ty : s) -> SchemaB TypeRep String String
reflectSchema Proxy ('DSimple ty : s)
_ = FieldTypeB TypeRep String -> TypeDefB TypeRep String String
forall builtin typeName fieldName.
FieldTypeB builtin typeName -> TypeDefB builtin typeName fieldName
DSimple (Proxy ty -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy ty
forall k (t :: k). Proxy t
Proxy @ty))
                  TypeDefB TypeRep String String
-> SchemaB TypeRep String String -> SchemaB TypeRep String String
forall a. a -> [a] -> [a]
: Proxy s -> SchemaB TypeRep String String
forall tn fn (s :: Schema tn fn).
ReflectSchema s =>
Proxy s -> SchemaB TypeRep String String
reflectSchema (Proxy s
forall k (t :: k). Proxy t
Proxy @s)

class ReflectFields (fs :: [FieldDef tn fn]) where
  -- | Reflect a list of fields into term-level.
  reflectFields :: Proxy fs -> [FieldDefB TypeRep String String]
instance ReflectFields '[] where
  reflectFields :: Proxy '[] -> [FieldDefB TypeRep String String]
reflectFields Proxy '[]
_ = []
instance (KnownName name, ReflectFieldType ty, ReflectFields fs)
         => ReflectFields ('FieldDef name ty ': fs) where
  reflectFields :: Proxy ('FieldDef name ty : fs) -> [FieldDefB TypeRep String String]
reflectFields Proxy ('FieldDef name ty : fs)
_ = String
-> FieldTypeB TypeRep String -> FieldDefB TypeRep String String
forall builtin typeName fieldName.
fieldName
-> FieldTypeB builtin typeName
-> FieldDefB builtin typeName fieldName
FieldDef (Proxy name -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name)) (Proxy ty -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy ty
forall k (t :: k). Proxy t
Proxy @ty))
                  FieldDefB TypeRep String String
-> [FieldDefB TypeRep String String]
-> [FieldDefB TypeRep String String]
forall a. a -> [a] -> [a]
: Proxy fs -> [FieldDefB TypeRep String String]
forall tn fn (fs :: [FieldDef tn fn]).
ReflectFields fs =>
Proxy fs -> [FieldDefB TypeRep String String]
reflectFields (Proxy fs
forall k (t :: k). Proxy t
Proxy @fs)

class ReflectChoices (cs :: [ChoiceDef fn]) where
  -- | Reflect a list of enumeration choices into term-level.
  reflectChoices :: Proxy cs -> [ChoiceDef String]
instance ReflectChoices '[] where
  reflectChoices :: Proxy '[] -> [ChoiceDef String]
reflectChoices Proxy '[]
_ = []
instance (KnownName name, ReflectChoices cs)
         => ReflectChoices ('ChoiceDef name ': cs) where
  reflectChoices :: Proxy ('ChoiceDef name : cs) -> [ChoiceDef String]
reflectChoices Proxy ('ChoiceDef name : cs)
_ = String -> ChoiceDef String
forall fieldName. fieldName -> ChoiceDef fieldName
ChoiceDef (Proxy name -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy name
forall k (t :: k). Proxy t
Proxy @name))
                   ChoiceDef String -> [ChoiceDef String] -> [ChoiceDef String]
forall a. a -> [a] -> [a]
: Proxy cs -> [ChoiceDef String]
forall fn (cs :: [ChoiceDef fn]).
ReflectChoices cs =>
Proxy cs -> [ChoiceDef String]
reflectChoices (Proxy cs
forall k (t :: k). Proxy t
Proxy @cs)

class ReflectFieldType (ty :: FieldType tn) where
  -- | Reflect a schema type into term-level.
  reflectFieldType :: Proxy ty -> FieldTypeB TypeRep String
instance ReflectFieldType 'TNull where
  reflectFieldType :: Proxy 'TNull -> FieldTypeB TypeRep String
reflectFieldType Proxy 'TNull
_ = FieldTypeB TypeRep String
forall builtin typeName. FieldTypeB builtin typeName
TNull
instance (Typeable ty) => ReflectFieldType ('TPrimitive ty) where
  reflectFieldType :: Proxy ('TPrimitive ty) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TPrimitive ty)
_ = TypeRep -> FieldTypeB TypeRep String
forall builtin typeName. builtin -> FieldTypeB builtin typeName
TPrimitive (Proxy ty -> TypeRep
forall k (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy ty
forall k (t :: k). Proxy t
Proxy @ty))
instance (KnownName nm) => ReflectFieldType ('TSchematic nm) where
  reflectFieldType :: Proxy ('TSchematic nm) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TSchematic nm)
_ = String -> FieldTypeB TypeRep String
forall builtin typeName. typeName -> FieldTypeB builtin typeName
TSchematic (Proxy nm -> String
forall k (a :: k) (proxy :: k -> *).
KnownName a =>
proxy a -> String
nameVal (Proxy nm
forall k (t :: k). Proxy t
Proxy @nm))
instance (ReflectFieldType t) => ReflectFieldType ('TOption t) where
  reflectFieldType :: Proxy ('TOption t) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TOption t)
_ = FieldTypeB TypeRep String -> FieldTypeB TypeRep String
forall builtin typeName.
FieldTypeB builtin typeName -> FieldTypeB builtin typeName
TOption (Proxy t -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy t
forall k (t :: k). Proxy t
Proxy @t))
instance (ReflectFieldType t) => ReflectFieldType ('TList t) where
  reflectFieldType :: Proxy ('TList t) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TList t)
_ = FieldTypeB TypeRep String -> FieldTypeB TypeRep String
forall builtin typeName.
FieldTypeB builtin typeName -> FieldTypeB builtin typeName
TList (Proxy t -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy t
forall k (t :: k). Proxy t
Proxy @t))
instance (ReflectFieldType k, ReflectFieldType v)
         => ReflectFieldType ('TMap k v) where
  reflectFieldType :: Proxy ('TMap k v) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TMap k v)
_ = FieldTypeB TypeRep String
-> FieldTypeB TypeRep String -> FieldTypeB TypeRep String
forall builtin typeName.
FieldTypeB builtin typeName
-> FieldTypeB builtin typeName -> FieldTypeB builtin typeName
TMap (Proxy k -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy k
forall k (t :: k). Proxy t
Proxy @k)) (Proxy v -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy v
forall k (t :: k). Proxy t
Proxy @v))
instance (ReflectFieldTypes ts) => ReflectFieldType ('TUnion ts) where
  reflectFieldType :: Proxy ('TUnion ts) -> FieldTypeB TypeRep String
reflectFieldType Proxy ('TUnion ts)
_ = [FieldTypeB TypeRep String] -> FieldTypeB TypeRep String
forall builtin typeName.
[FieldTypeB builtin typeName] -> FieldTypeB builtin typeName
TUnion (Proxy ts -> [FieldTypeB TypeRep String]
forall tn (ts :: [FieldType tn]).
ReflectFieldTypes ts =>
Proxy ts -> [FieldTypeB TypeRep String]
reflectFieldTypes (Proxy ts
forall k (t :: k). Proxy t
Proxy @ts))

class ReflectFieldTypes (ts :: [FieldType tn]) where
  -- | Reflect a list of schema types into term-level.
  reflectFieldTypes :: Proxy ts -> [FieldTypeB TypeRep String]
instance ReflectFieldTypes '[] where
  reflectFieldTypes :: Proxy '[] -> [FieldTypeB TypeRep String]
reflectFieldTypes Proxy '[]
_ = []
instance (ReflectFieldType t, ReflectFieldTypes ts)
         => ReflectFieldTypes (t ': ts) where
  reflectFieldTypes :: Proxy (t : ts) -> [FieldTypeB TypeRep String]
reflectFieldTypes Proxy (t : ts)
_ = Proxy t -> FieldTypeB TypeRep String
forall tn (ty :: FieldType tn).
ReflectFieldType ty =>
Proxy ty -> FieldTypeB TypeRep String
reflectFieldType (Proxy t
forall k (t :: k). Proxy t
Proxy @t) FieldTypeB TypeRep String
-> [FieldTypeB TypeRep String] -> [FieldTypeB TypeRep String]
forall a. a -> [a] -> [a]
: Proxy ts -> [FieldTypeB TypeRep String]
forall tn (ts :: [FieldType tn]).
ReflectFieldTypes ts =>
Proxy ts -> [FieldTypeB TypeRep String]
reflectFieldTypes (Proxy ts
forall k (t :: k). Proxy t
Proxy @ts)