    {-# LANGUAGE DataKinds                 #-}
    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE FlexibleContexts          #-}
    {-# LANGUAGE FlexibleInstances         #-}
    {-# LANGUAGE GADTs                     #-}
    {-# LANGUAGE KindSignatures            #-}
    {-# LANGUAGE ScopedTypeVariables       #-}
    {-# LANGUAGE StandaloneDeriving        #-}
    {-# LANGUAGE Trustworthy               #-}
    {-# LANGUAGE TypeApplications          #-}
    {-# LANGUAGE TypeOperators             #-}
    {-# LANGUAGE UndecidableInstances      #-}
    -- |
    -- Description: Typing for Core.
    -- Copyright:   (c) 2011 National Institute of Aerospace / Galois, Inc.
    --
    -- All expressions and streams in Core are accompanied by a representation of
    -- the types of the underlying expressions used or carried by the streams.
    -- This information is needed by the compiler to generate code, since it must
    -- initialize variables and equivalent representations for those types in
    -- the target languages.
    module Copilot.Core.Type
        ( Type (..)
        , Typed (..)
        , typeOfDefault
        , UType (..)
        , SimpleType (..)

        , typeSize
        , typeLength

        , Value (..)
        , toValues
        , toValuesDefault
        , Field (..)
        , typeName
        , typeNameDefault

        , Struct
        , fieldName
        , accessorName
        , updateField
        , updateFieldDefault
        )
      where

    -- External imports
    import Data.Char          (isLower, isUpper, toLower)
    import Data.Coerce        (coerce)
    import Data.Int           (Int16, Int32, Int64, Int8)
    import Data.List          (intercalate)
    import Data.Proxy         (Proxy (..))
    import Data.Type.Equality as DE
    import Data.Typeable      (Typeable, eqT, typeRep)
    import Data.Word          (Word16, Word32, Word64, Word8)
    import GHC.Generics       (Datatype (..), D1, Generic (..), K1 (..), M1 (..),
                               U1 (..), (:*:) (..))
    import GHC.TypeLits       (KnownNat, KnownSymbol, Symbol, natVal, sameNat,
                               sameSymbol, symbolVal)

    -- Internal imports
    import Copilot.Core.Type.Array (Array)

    -- | The value of that is a product or struct, defined as a constructor with
    -- several fields.
    class Struct a where
      -- | Returns the name of struct in the target language.
      typeName :: a -> String

      -- | Transforms all the struct's fields into a list of values.
      toValues :: a -> [Value a]

      -- | Update the value of a struct field. This is only used by the Copilot
      -- interpreter.
      --
      -- If you do not plan to use the interpreter, you can omit an implementation
      -- of this method. If you do so, it is recommended that you derive a 'Generic'
      -- instance for the struct data type. This is because in a future release, the
      -- default implementation of 'updateField' (which will be picked if there is
      -- not a manually written implementation) will be changed to require a
      -- 'Generic' instance.
      --
      -- In order to implement 'updateField', pick one of the following approaches:
      --
      -- * Derive a 'Generic' instance for the struct data type and then define
      --   @'updateField' = 'updateFieldDefault'@ in the 'Struct' instance.
      --
      -- * Manually implement 'updateField' by doing the following for each 'Field'
      --   in a struct:
      --
      --   1. Check that the name of the 'Field' matches the name of the supplied
      --      'Value' (using 'GHC.TypeLits.sameSymbol').
      --
      --   2. Check that the type of the 'Field' matches the 'Type' of the supplied
      --      'Value' (using 'DE.testEquality').
      --
      --   3. If both (1) and (2) succeed, update the corresponding struct field
      --      using a record update.
      --
      --   For a complete end-to-end example that demonstrates how to manually
      --   implement 'updateField' and use it in the Copilot interpreter, see the
      --   @examples/StructsUpdateField.hs@ example in the @copilot@ library.
      updateField :: a -> Value t -> a
      updateField = [Char] -> a -> Value t -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a -> Value t -> a) -> [Char] -> a -> Value t -> a
    forall a b. (a -> b) -> a -> b
    $ [[Char]] -> [Char]
    unlines
        [ [Char]
    "Field updates not supported for this type."
        , [Char]
    "(Perhaps you need to implement 'updateField' for a 'Struct' instance?)"
        ]

    -- | The field of a struct, together with a representation of its type.
    data Value a =
      forall s t . (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)

    -- | A field in a struct. The name of the field is a literal at the type
    -- level.
    data Field (s :: Symbol) t = Field t

    -- | Extract the name of a field.
    fieldName :: forall s t . KnownSymbol s => Field s t -> String
    fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> [Char]
    fieldName Field s t
    _ = Proxy s -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (Proxy s
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy s)

    -- | Extract the name of an accessor (a function that returns a field of a
    -- struct).
    accessorName :: forall a s t . (Struct a, KnownSymbol s)
                 => (a -> Field s t) -> String
    accessorName :: forall a (s :: Symbol) t.
    (Struct a, KnownSymbol s) =>
    (a -> Field s t) -> [Char]
    accessorName a -> Field s t
    _ = Proxy s -> [Char]
    forall (n :: Symbol) (proxy :: Symbol -> *).
    KnownSymbol n =>
    proxy n -> [Char]
    symbolVal (Proxy s
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy s)

    instance (KnownSymbol s, Show t) => Show (Field s t) where
      show :: Field s t -> [Char]
    show f :: Field s t
    f@(Field t
    v) = Field s t -> [Char]
    forall (s :: Symbol) t. KnownSymbol s => Field s t -> [Char]
    fieldName Field s t
    f [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ":" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ t -> [Char]
    forall a. Show a => a -> [Char]
    show t
    v

    instance {-# OVERLAPPABLE #-} (Typed t, Struct t) => Show t where
      show :: t -> [Char]
    show t
    t = [Char]
    "<" [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    fields [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    ">"
        where
          fields :: [Char]
    fields = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ (Value t -> [Char]) -> [Value t] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Value t -> [Char]
    forall {a}. Value a -> [Char]
    showfield (t -> [Value t]
    forall a. Struct a => a -> [Value a]
    toValues t
    t)
          showfield :: Value a -> [Char]
    showfield (Value Type t
    _ Field s t
    field) = Field s t -> [Char]
    forall a. Show a => a -> [Char]
    show Field s t
    field

    -- | A Type representing the types of expressions or values handled by
    -- Copilot Core.
    --
    -- Note that both arrays and structs use dependently typed features. In the
    -- former, the length of the array is part of the type. In the latter, the
    -- names of the fields are part of the type.
    data Type :: * -> * where
      Bool   :: Type Bool
      Int8   :: Type Int8
      Int16  :: Type Int16
      Int32  :: Type Int32
      Int64  :: Type Int64
      Word8  :: Type Word8
      Word16 :: Type Word16
      Word32 :: Type Word32
      Word64 :: Type Word64
      Float  :: Type Float
      Double :: Type Double
      Array  :: forall n t . ( KnownNat n
                             , Typed t
                             ) => Type t -> Type (Array n t)
      Struct :: (Typed a, Struct a) => a -> Type a
    deriving instance Show (Type a)

    -- | Return the length of an array from its type
    typeLength :: forall n t . KnownNat n => Type (Array n t) -> Int
    typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeLength Type (Array n t)
    _ = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)

    -- | Return the total (nested) size of an array from its type
    typeSize :: forall n t . KnownNat n => Type (Array n t) -> Int
    typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeSize ty :: Type (Array n t)
    ty@(Array ty' :: Type t
    ty'@(Array Type t
    _)) = Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeLength Type (Array n t)
    ty Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeSize Type t
    Type (Array n t)
    ty'
    typeSize ty :: Type (Array n t)
    ty@(Array Type t
    _            ) = Type (Array n t) -> Int
    forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
    typeLength Type (Array n t)
    ty

    instance TestEquality Type where
      testEquality :: forall a b. Type a -> Type b -> Maybe (a :~: b)
    testEquality Type a
    Bool   Type b
    Bool   = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Int8   Type b
    Int8   = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Int16  Type b
    Int16  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Int32  Type b
    Int32  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Int64  Type b
    Int64  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Word8  Type b
    Word8  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Word16 Type b
    Word16 = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Word32 Type b
    Word32 = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Word64 Type b
    Word64 = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Float  Type b
    Float  = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality Type a
    Double Type b
    Double = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: a
    a :~: b
    forall {k} (a :: k). a :~: a
    DE.Refl
      testEquality (Array Type t
    t1) (Array Type t
    t2) =
          Type t -> Type t -> Maybe (Array n t :~: Array n t)
    forall (n1 :: Nat) a1 (n2 :: Nat) a2.
    (KnownNat n1, KnownNat n2) =>
    Type a1 -> Type a2 -> Maybe (Array n1 a1 :~: Array n2 a2)
    testArrayEquality Type t
    t1 Type t
    t2
        where
          testArrayEquality :: forall n1 a1 n2 a2.
                               (KnownNat n1, KnownNat n2)
                            => Type a1
                            -> Type a2
                            -> Maybe (Array n1 a1 :~: Array n2 a2)
          testArrayEquality :: forall (n1 :: Nat) a1 (n2 :: Nat) a2.
    (KnownNat n1, KnownNat n2) =>
    Type a1 -> Type a2 -> Maybe (Array n1 a1 :~: Array n2 a2)
    testArrayEquality Type a1
    ty1 Type a2
    ty2
            | Just n1 :~: n2
    DE.Refl <- Proxy n1 -> Proxy n2 -> Maybe (n1 :~: n2)
    forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
           (proxy2 :: Nat -> *).
    (KnownNat a, KnownNat b) =>
    proxy1 a -> proxy2 b -> Maybe (a :~: b)
    sameNat (Proxy n1
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n1) (Proxy n2
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n2)
            , Just a1 :~: a2
    DE.Refl <- Type a1 -> Type a2 -> Maybe (a1 :~: a2)
    forall a b. Type a -> Type b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Type a1
    ty1 Type a2
    ty2
            = (Array n1 a1 :~: Array n2 a2)
    -> Maybe (Array n1 a1 :~: Array n2 a2)
    forall a. a -> Maybe a
    Just Array n1 a1 :~: Array n1 a1
    Array n1 a1 :~: Array n2 a2
    forall {k} (a :: k). a :~: a
    DE.Refl
            | Bool
    otherwise
            = Maybe (Array n1 a1 :~: Array n2 a2)
    forall a. Maybe a
    Nothing
      testEquality (Struct a
    _) (Struct b
    _) = Maybe (a :~: b)
    forall {k} (a :: k) (b :: k).
    (Typeable a, Typeable b) =>
    Maybe (a :~: b)
    eqT
      testEquality Type a
    _ Type b
    _ = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    -- | A simple, monomorphic representation of types that facilitates putting
    -- variables in heterogeneous lists and environments in spite of their types
    -- being different.
    data SimpleType where
      SBool   :: SimpleType
      SInt8   :: SimpleType
      SInt16  :: SimpleType
      SInt32  :: SimpleType
      SInt64  :: SimpleType
      SWord8  :: SimpleType
      SWord16 :: SimpleType
      SWord32 :: SimpleType
      SWord64 :: SimpleType
      SFloat  :: SimpleType
      SDouble :: SimpleType
      SArray  :: Type t -> SimpleType
      SStruct :: SimpleType

    -- | Type equality, used to help type inference.

    -- This instance is necessary, otherwise the type of SArray can't be inferred.
    instance Eq SimpleType where
      SimpleType
    SBool   == :: SimpleType -> SimpleType -> Bool
    == SimpleType
    SBool   = Bool
    True
      SimpleType
    SInt8   == SimpleType
    SInt8   = Bool
    True
      SimpleType
    SInt16  == SimpleType
    SInt16  = Bool
    True
      SimpleType
    SInt32  == SimpleType
    SInt32  = Bool
    True
      SimpleType
    SInt64  == SimpleType
    SInt64  = Bool
    True
      SimpleType
    SWord8  == SimpleType
    SWord8  = Bool
    True
      SimpleType
    SWord16 == SimpleType
    SWord16 = Bool
    True
      SimpleType
    SWord32 == SimpleType
    SWord32 = Bool
    True
      SimpleType
    SWord64 == SimpleType
    SWord64 = Bool
    True
      SimpleType
    SFloat  == SimpleType
    SFloat  = Bool
    True
      SimpleType
    SDouble == SimpleType
    SDouble = Bool
    True
      (SArray Type t
    t1) == (SArray Type t
    t2) | Just t :~: t
    DE.Refl <- Type t -> Type t -> Maybe (t :~: t)
    forall a b. Type a -> Type b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Type t
    t1 Type t
    t2 = Bool
    True
                                 | Bool
    otherwise                          = Bool
    False
      SimpleType
    SStruct == SimpleType
    SStruct = Bool
    True
      SimpleType
    _ == SimpleType
    _ = Bool
    False

    -- | A typed expression, from which we can obtain the two type representations
    -- used by Copilot: 'Type' and 'SimpleType'.
    class (Show a, Typeable a) => Typed a where
      typeOf     :: Type a
      simpleType :: Type a -> SimpleType
      simpleType Type a
    _ = SimpleType
    SStruct

    instance Typed Bool where
      typeOf :: Type Bool
    typeOf       = Type Bool
    Bool
      simpleType :: Type Bool -> SimpleType
    simpleType Type Bool
    _ = SimpleType
    SBool

    instance Typed Int8 where
      typeOf :: Type Int8
    typeOf       = Type Int8
    Int8
      simpleType :: Type Int8 -> SimpleType
    simpleType Type Int8
    _ = SimpleType
    SInt8

    instance Typed Int16 where
      typeOf :: Type Int16
    typeOf       = Type Int16
    Int16
      simpleType :: Type Int16 -> SimpleType
    simpleType Type Int16
    _ = SimpleType
    SInt16

    instance Typed Int32 where
      typeOf :: Type Int32
    typeOf       = Type Int32
    Int32
      simpleType :: Type Int32 -> SimpleType
    simpleType Type Int32
    _ = SimpleType
    SInt32

    instance Typed Int64 where
      typeOf :: Type Int64
    typeOf       = Type Int64
    Int64
      simpleType :: Type Int64 -> SimpleType
    simpleType Type Int64
    _ = SimpleType
    SInt64

    instance Typed Word8 where
      typeOf :: Type Word8
    typeOf       = Type Word8
    Word8
      simpleType :: Type Word8 -> SimpleType
    simpleType Type Word8
    _ = SimpleType
    SWord8

    instance Typed Word16 where
      typeOf :: Type Word16
    typeOf       = Type Word16
    Word16
      simpleType :: Type Word16 -> SimpleType
    simpleType Type Word16
    _ = SimpleType
    SWord16

    instance Typed Word32 where
      typeOf :: Type Word32
    typeOf       = Type Word32
    Word32
      simpleType :: Type Word32 -> SimpleType
    simpleType Type Word32
    _ = SimpleType
    SWord32

    instance Typed Word64 where
      typeOf :: Type Word64
    typeOf       = Type Word64
    Word64
      simpleType :: Type Word64 -> SimpleType
    simpleType Type Word64
    _ = SimpleType
    SWord64

    instance Typed Float where
      typeOf :: Type Float
    typeOf       = Type Float
    Float
      simpleType :: Type Float -> SimpleType
    simpleType Type Float
    _ = SimpleType
    SFloat

    instance Typed Double where
      typeOf :: Type Double
    typeOf       = Type Double
    Double
      simpleType :: Type Double -> SimpleType
    simpleType Type Double
    _ = SimpleType
    SDouble

    instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
      typeOf :: Type (Array n t)
    typeOf               = Type t -> Type (Array n t)
    forall (t :: Nat) t.
    (KnownNat t, Typed t) =>
    Type t -> Type (Array t t)
    Array Type t
    forall a. Typed a => Type a
    typeOf
      simpleType :: Type (Array n t) -> SimpleType
    simpleType (Array Type t
    t) = Type t -> SimpleType
    forall t. Type t -> SimpleType
    SArray Type t
    t

    -- | A untyped type (no phantom type).
    data UType = forall a . Typeable a => UType (Type a)

    instance Eq UType where
      UType Type a
    ty1 == :: UType -> UType -> Bool
    == UType Type a
    ty2 = Type a -> TypeRep
    forall {k} (proxy :: k -> *) (a :: k).
    Typeable a =>
    proxy a -> TypeRep
    typeRep Type a
    ty1 TypeRep -> TypeRep -> Bool
    forall a. Eq a => a -> a -> Bool
    == Type a -> TypeRep
    forall {k} (proxy :: k -> *) (a :: k).
    Typeable a =>
    proxy a -> TypeRep
    typeRep Type a
    ty2

    -- * GHC.Generics-based defaults

    -- | A default implementation of 'typeName' that leverages 'Generic'. In order
    -- to use this, make sure you derive a 'Generic' instance for your data type and
    -- then define @'typeName' = 'typeNameDefault'@ in its 'Struct' instance.
    --
    -- This generates a struct name that consists of the name of the original
    -- Haskell data type, but converted to snake_case.
    typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String
    typeNameDefault :: forall a. (Generic a, GDatatype (Rep a)) => a -> [Char]
    typeNameDefault = ShowS
    convert ShowS -> (a -> [Char]) -> a -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rep a (ZonkAny 2) -> [Char]
    forall p. Rep a p -> [Char]
    forall (f :: * -> *) p. GDatatype f => f p -> [Char]
    gTypeName (Rep a (ZonkAny 2) -> [Char])
    -> (a -> Rep a (ZonkAny 2)) -> a -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Rep a (ZonkAny 2)
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    from
      where
        convert :: String -> String
        convert :: ShowS
    convert = Bool -> Bool -> ShowS
    convert' Bool
    True Bool
    True

        convert' :: Bool   -- ^ Is this the first letter
                 -> Bool   -- ^ Was the previous letter capital
                 -> String -- ^ Remainder of the string
                 -> String
        convert' :: Bool -> Bool -> ShowS
    convert' Bool
    _ Bool
    _ []    = []
        convert' Bool
    _ Bool
    v [Char
    x]
          | Bool
    v Bool -> Bool -> Bool
    && Char -> Bool
    isUpper Char
    x = Char -> Char
    toLower Char
    x Char -> ShowS
    forall a. a -> [a] -> [a]
    : []
          | Char -> Bool
    isUpper Char
    x      = Char
    '_' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Char -> Char
    toLower Char
    x Char -> ShowS
    forall a. a -> [a] -> [a]
    : []
          | Bool
    otherwise      = Char
    x Char -> ShowS
    forall a. a -> [a] -> [a]
    : []
        convert' Bool
    b Bool
    v (Char
    x1:Char
    x2:[Char]
    xs)
          | Bool -> Bool
    not Bool
    b Bool -> Bool -> Bool
    && Char -> Bool
    isUpper Char
    x1 Bool -> Bool -> Bool
    && (Char -> Bool
    isLower Char
    x2 Bool -> Bool -> Bool
    || Bool -> Bool
    not Bool
    v)
          = Char
    '_' Char -> ShowS
    forall a. a -> [a] -> [a]
    : Char -> Char
    toLower Char
    x1 Char -> ShowS
    forall a. a -> [a] -> [a]
    : Bool -> Bool -> ShowS
    convert' Bool
    False (Char -> Bool
    isUpper Char
    x1) (Char
    x2Char -> ShowS
    forall a. a -> [a] -> [a]
    :[Char]
    xs)
          | Bool
    otherwise
          = Char -> Char
    toLower Char
    x1 Char -> ShowS
    forall a. a -> [a] -> [a]
    : Bool -> Bool -> ShowS
    convert' Bool
    False (Char -> Bool
    isUpper Char
    x1) (Char
    x2Char -> ShowS
    forall a. a -> [a] -> [a]
    :[Char]
    xs)

    -- | A default implementation of 'toValues' that leverages 'Generic'. In order
    -- to use this, make sure you derive a 'Generic' instance for your data type and
    -- then define @'toValues' = 'toValuesDefault'@ in its 'Struct' instance.
    toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a]
    toValuesDefault :: forall a. (Generic a, GStruct (Rep a)) => a -> [Value a]
    toValuesDefault a
    x = [Value (Rep a (ZonkAny 1))] -> [Value a]
    forall a b. Coercible a b => a -> b
    coerce ([Value (Rep a (ZonkAny 1))] -> [Value a])
    -> [Value (Rep a (ZonkAny 1))] -> [Value a]
    forall a b. (a -> b) -> a -> b
    $ Rep a (ZonkAny 1) -> [Value (Rep a (ZonkAny 1))]
    forall p. Rep a p -> [Value (Rep a p)]
    forall (f :: * -> *) p. GStruct f => f p -> [Value (f p)]
    gToValues (Rep a (ZonkAny 1) -> [Value (Rep a (ZonkAny 1))])
    -> Rep a (ZonkAny 1) -> [Value (Rep a (ZonkAny 1))]
    forall a b. (a -> b) -> a -> b
    $ a -> Rep a (ZonkAny 1)
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    from a
    x

    -- | A default implementation of 'updateField' that leverages 'Generic'. In
    -- order to use this, make sure you derive a 'Generic' instance for your data
    -- type and then define @'updateField' = 'updateFieldDefault'@ in its 'Struct'
    -- instance.
    updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a
    updateFieldDefault :: forall a t. (Generic a, GStruct (Rep a)) => a -> Value t -> a
    updateFieldDefault a
    a v :: Value t
    v@(Value Type t
    _ Field s t
    field)
        | Bool
    updated   = Rep a (ZonkAny 0) -> a
    forall a x. Generic a => Rep a x -> a
    forall x. Rep a x -> a
    to Rep a (ZonkAny 0)
    a'
        | Bool
    otherwise = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error ([Char] -> a) -> [Char] -> a
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Unexpected field: " [Char] -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Field s t -> [Char]
    forall a. Show a => a -> [Char]
    show Field s t
    field
      where
        (Rep a (ZonkAny 0)
    a', Bool
    updated) = Rep a (ZonkAny 0) -> Value t -> (Rep a (ZonkAny 0), Bool)
    forall p t. Rep a p -> Value t -> (Rep a p, Bool)
    forall (f :: * -> *) p t.
    GStruct f =>
    f p -> Value t -> (f p, Bool)
    gUpdateField (a -> Rep a (ZonkAny 0)
    forall x. a -> Rep a x
    forall a x. Generic a => a -> Rep a x
    from a
    a) Value t
    v

    -- | A default implementation of 'typeOf' that leverages 'Generic'. In order to
    -- use this, make sure you derive a 'Generic' instance for your data type and
    -- then define @'typeOf' = 'typeOfDefault'@ in its 'Typed' instance.
    typeOfDefault ::
      forall a. (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a
    typeOfDefault :: forall a.
    (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) =>
    Type a
    typeOfDefault = a -> Type a
    forall a. (Typed a, Struct a) => a -> Type a
    Struct (a -> Type a) -> a -> Type a
    forall a b. (a -> b) -> a -> b
    $ Rep a () -> a
    forall a x. Generic a => Rep a x -> a
    forall x. Rep a x -> a
    to (Rep a () -> a) -> Rep a () -> a
    forall a b. (a -> b) -> a -> b
    $ forall (f :: * -> *) p. GTypedStruct f => f p
    gStructPlaceholder @(Rep a) @()

    -- ** Generic-based classes (not exported)

    -- | Capture the name of a Haskell data type from its 'Generic' metadata.
    class GDatatype f where
      -- | Returns the name of a Haskell data type. (Note that this differs from
      -- 'typeName', which is expected to return the name of the struct in the
      -- /target/ language).
      gTypeName :: f p -> String

    -- | The only 'GDatatype' instance we need is for 'D1', which describes
    -- 'Datatype' metadata (@d@). We ignore all other metadata (@_f@).
    instance Datatype d => GDatatype (D1 d _f) where
      gTypeName :: forall p. D1 d _f p -> [Char]
    gTypeName = M1 D d _f p -> [Char]
    forall {k} (d :: k) k1 (t :: k -> (k1 -> *) -> k1 -> *)
           (f :: k1 -> *) (a :: k1).
    Datatype d =>
    t d f a -> [Char]
    forall k1 (t :: Meta -> (k1 -> *) -> k1 -> *) (f :: k1 -> *)
           (a :: k1).
    t d f a -> [Char]
    datatypeName

    -- | Perform struct-related operations on 'Generic' representation types.
    class GStruct f where
      -- | Transforms all the struct representation's fields into a list of values.
      gToValues :: f p -> [Value (f p)]

      -- | Update the value of a struct representation's field. This returns two
      -- things:
      --
      -- 1. @f p@: The struct representation, but with the field updated.
      --
      -- 2. 'Bool': This is 'True' if the field was successfully updated and 'False'
      --    otherwise. If this returns 'False', it is the responsibility of the
      --    caller to raise an error.
      gUpdateField :: f p -> Value t -> (f p, Bool)

    -- | 'U1' represents a data constructor with no fields. As such, 'gToValues'
    -- returns an empty list of 'Value's, and 'gUpdateField' does not update
    -- anything.
    instance GStruct U1 where
      gToValues :: forall p. U1 p -> [Value (U1 p)]
    gToValues U1 p
    U1 = []
      gUpdateField :: forall p t. U1 p -> Value t -> (U1 p, Bool)
    gUpdateField U1 p
    u Value t
    _ = (U1 p
    u, Bool
    False)

    -- | 'M1' is only used to store metadata, which the 'GStruct' class does not
    -- make use of. As such, this instance discards the metadata and recurses.
    instance GStruct f => GStruct (M1 _i _c f) where
      gToValues :: forall p. M1 _i _c f p -> [Value (M1 _i _c f p)]
    gToValues (M1 f p
    x) = [Value (f p)] -> [Value (M1 _i _c f p)]
    forall a b. Coercible a b => a -> b
    coerce (f p -> [Value (f p)]
    forall p. f p -> [Value (f p)]
    forall (f :: * -> *) p. GStruct f => f p -> [Value (f p)]
    gToValues f p
    x)
      gUpdateField :: forall p t. M1 _i _c f p -> Value t -> (M1 _i _c f p, Bool)
    gUpdateField (M1 f p
    x) Value t
    v = (f p -> M1 _i _c f p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 f p
    x', Bool
    updated)
        where
          (f p
    x', Bool
    updated) = f p -> Value t -> (f p, Bool)
    forall p t. f p -> Value t -> (f p, Bool)
    forall (f :: * -> *) p t.
    GStruct f =>
    f p -> Value t -> (f p, Bool)
    gUpdateField f p
    x Value t
    v

    -- | @(':*:')@ represents a data constructor with multiple fields.
    instance (GStruct f, GStruct g) => GStruct (f :*: g) where
      -- Recursively compute two lists of Values and append them.
      gToValues :: forall p. (:*:) f g p -> [Value ((:*:) f g p)]
    gToValues (f p
    f :*: g p
    g) = [Value (f p)] -> [Value ((:*:) f g p)]
    forall a b. Coercible a b => a -> b
    coerce (f p -> [Value (f p)]
    forall p. f p -> [Value (f p)]
    forall (f :: * -> *) p. GStruct f => f p -> [Value (f p)]
    gToValues f p
    f) [Value ((:*:) f g p)]
    -> [Value ((:*:) f g p)] -> [Value ((:*:) f g p)]
    forall a. [a] -> [a] -> [a]
    ++ [Value (g p)] -> [Value ((:*:) f g p)]
    forall a b. Coercible a b => a -> b
    coerce (g p -> [Value (g p)]
    forall p. g p -> [Value (g p)]
    forall (f :: * -> *) p. GStruct f => f p -> [Value (f p)]
    gToValues g p
    g)
      -- Recursively attempt to update the field in both branches and combine the
      -- updated branches. We will have successfully updated the field if either
      -- branch was successfully updated.
      gUpdateField :: forall p t. (:*:) f g p -> Value t -> ((:*:) f g p, Bool)
    gUpdateField (f p
    f :*: g p
    g) Value t
    v = (f p
    f' f p -> g p -> (:*:) f g p
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: g p
    g', Bool
    updatedF Bool -> Bool -> Bool
    || Bool
    updatedG)
        where
          (f p
    f', Bool
    updatedF) = f p -> Value t -> (f p, Bool)
    forall p t. f p -> Value t -> (f p, Bool)
    forall (f :: * -> *) p t.
    GStruct f =>
    f p -> Value t -> (f p, Bool)
    gUpdateField f p
    f Value t
    v
          (g p
    g', Bool
    updatedG) = g p -> Value t -> (g p, Bool)
    forall p t. g p -> Value t -> (g p, Bool)
    forall (f :: * -> *) p t.
    GStruct f =>
    f p -> Value t -> (f p, Bool)
    gUpdateField g p
    g Value t
    v

    -- | 'K1' represents a single field in a data constructor. This is the base
    -- case.
    instance (KnownSymbol name, Typed ty, c ~ Field name ty) =>
        GStruct (K1 _i c) where
      -- Now that we have the field, return it in a singleton list.
      gToValues :: forall p. K1 _i c p -> [Value (K1 _i c p)]
    gToValues (K1 c
    field) = [Type ty -> Field name ty -> Value (K1 _i c p)
    forall a (s :: Symbol) t.
    (Typeable t, KnownSymbol s, Show t) =>
    Type t -> Field s t -> Value a
    Value Type ty
    forall a. Typed a => Type a
    typeOf c
    Field name ty
    field]
      -- In order to update the field, we check that the field names and types
      -- match. If they do, return the updated field and declare the update as
      -- successful. Otherwise, return the old field and declare the update as
      -- unsuccessful.
      gUpdateField :: forall p t. K1 _i c p -> Value t -> (K1 _i c p, Bool)
    gUpdateField (K1 c
    oldField) (Value Type t
    newTy (Field s t
    newField :: Field newName newTy)) =
        case (Proxy name -> Proxy s -> Maybe (name :~: s)
    forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
           (proxy2 :: Symbol -> *).
    (KnownSymbol a, KnownSymbol b) =>
    proxy1 a -> proxy2 b -> Maybe (a :~: b)
    sameSymbol Proxy name
    pName Proxy s
    pNewName, Type ty -> Type t -> Maybe (ty :~: t)
    forall a b. Type a -> Type b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Type ty
    ty Type t
    newTy) of
          (Just name :~: s
    Refl, Just ty :~: t
    Refl) -> (c -> K1 _i c p
    forall k i c (p :: k). c -> K1 i c p
    K1 c
    Field s t
    newField, Bool
    True)
          (Maybe (name :~: s), Maybe (ty :~: t))
    _                      -> (c -> K1 _i c p
    forall k i c (p :: k). c -> K1 i c p
    K1 c
    oldField, Bool
    False)
        where
          pName :: Proxy name
    pName    = forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @name
          pNewName :: Proxy s
    pNewName = forall {k} (t :: k). Proxy t
    forall (t :: Symbol). Proxy t
    Proxy @newName
          ty :: Type ty
    ty       = forall a. Typed a => Type a
    typeOf @ty

    -- | Compute a 'Generic' placeholder value to use for a struct type.
    class GTypedStruct f where
      -- | A placeholder value to supply to use in a generic implementation of
      -- 'typeOf' for a struct type.
      gStructPlaceholder :: f p

    -- | 'U1' represents a data constructor with no fields. As such,
    -- 'gStructPlaceholder' simply returns the data constructor with no other
    -- information.
    instance GTypedStruct U1 where
      gStructPlaceholder :: forall p. U1 p
    gStructPlaceholder = U1 p
    forall k (p :: k). U1 p
    U1

    -- | 'M1' is only used to store metadata, which the 'GTypedStruct' class does
    -- not make use of. As such, this instance recursively computes a placeholder
    -- value without inspecting the metadata.
    instance GTypedStruct f => GTypedStruct (M1 _i _c f) where
      gStructPlaceholder :: forall p. M1 _i _c f p
    gStructPlaceholder = f p -> M1 _i _c f p
    forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
    M1 f p
    forall p. f p
    forall (f :: * -> *) p. GTypedStruct f => f p
    gStructPlaceholder

    -- | @(':*:')@ represents a data constructor with multiple fields. As such,
    -- 'gStructPlaceholder' recursively computes placeholders for each field and
    -- combines them into the overall data constructor.
    instance (GTypedStruct f, GTypedStruct g) => GTypedStruct (f :*: g) where
      gStructPlaceholder :: forall p. (:*:) f g p
    gStructPlaceholder = f p
    forall p. f p
    forall (f :: * -> *) p. GTypedStruct f => f p
    gStructPlaceholder f p -> g p -> (:*:) f g p
    forall k (f :: k -> *) (g :: k -> *) (p :: k).
    f p -> g p -> (:*:) f g p
    :*: g p
    forall p. g p
    forall (f :: * -> *) p. GTypedStruct f => f p
    gStructPlaceholder

    -- | 'K1' represents a single field in a data constructor. This is the base
    -- case. This instance computes a placeholder value that works for any field of
    -- any type.
    instance (c ~ Field name ty) => GTypedStruct (K1 _i c) where
      -- We use 'undefined' as the actual value for the 'Field' because Copilot
      -- never inspects the value.
      gStructPlaceholder :: forall p. K1 _i c p
    gStructPlaceholder = c -> K1 _i c p
    forall k i c (p :: k). c -> K1 i c p
    K1 (c -> K1 _i c p) -> c -> K1 _i c p
    forall a b. (a -> b) -> a -> b
    $ ty -> Field name ty
    forall (s :: Symbol) t. t -> Field s t
    Field ty
    forall a. HasCallStack => a
    undefined