AST.hs

-- | Haskell AST
--
-- Abstract Haskell syntax for the specific purposes of hs-bindgen: we only
-- cover the parts of the Haskell syntax that we need. We attempt to do this in
-- such a way that the generated Haskell code is type correct by construction.
--
-- Intended for qualified import:
--
-- > import HsBindgen.Backend.Hs.AST qualified as Hs
module HsBindgen.Backend.Hs.AST (
    -- * Generated Haskell datatypes
    Field(..)
  , Struct(..)
  , EmptyData(..)
  , Newtype(..)
    -- * Variable binding
  , Lambda(..)
  , Apply(..)
  , Ap(..)
    -- * Declarations
  , Decl(..)
  , InstanceDecl(..)
  , DefineInstance(..)
  , DeriveInstance(..)
  , Var(..)
    -- ** Variable declarations
  , MacroValue(..)
    -- ** Deriving instances
  , Strategy(..)
    -- ** Foreign imports
  , ForeignImportDecl(..)
  , FunctionParameter(..)
    -- ** Function declarations
  , FunctionDecl(..)
    -- ** 'HsBindgen.Runtime.Support.FunPtr.Class.ToFunPtr'
  , ToFunPtrInstance(..)
  , ForeignImportWrapper(..)
    -- ** 'HsBindgen.Runtime.Support.FunPtr.Class.FromFunPtr'
  , FromFunPtrInstance(..)
  , ForeignImportDynamic(..)
    -- ** @StaticSize@, @ReadRaw@, @WriteRaw@
  , StaticSizeInstance(..)
  , ReadRawInstance(..)
  , WriteRawInstance(..)
  , ReadRawCField(..)
  , WriteRawCField(..)
    -- ** 'Foreign.Storable.Storable'
  , StorableInstance(..)
  , PeekCField(..)
  , PokeCField(..)
    -- ** 'HsBindgen.Instances.Prim'
  , PrimInstance(..)
  , IndexPrimFieldData(..)
  , IndexByteArrayField(..)
  , IndexOffAddrField(..)
  , ReadPrimFieldsData(..)
  , ReadByteArrayFields(..)
  , ReadOffAddrFields(..)
  , WritePrimFieldsData(..)
  , WriteByteArrayFields(..)
  , WriteOffAddrFields(..)
    -- ** 'HsBindgen.Runtime.HasCField.HasCField'
  , HasCFieldInstance(..)
    -- ** 'HsBindgen.Runtime.HasCBitfield.HasCBitfield'
  , HasCBitfieldInstance(..)
    -- ** 'GHC.Records.HasField'
  , HasFieldInstance(..)
  , HasFieldImpl(..)
    -- ** 'GHC.Records.Compat.HasField'
  , HasFieldCompatInstance(..)
  , HasFieldCompatImpl(..)
    -- ** 'GHC.Records.HasField' for the pointer manipulation API
  , HasFieldPtrInstance(..)
  , HasFieldPtrInstanceVia(..)
    -- ** 'HasFlam'
  , HasFlamInstance(..)
    -- ** 'CEnum'
  , CEnumInstance(..)
  , SequentialCEnumInstance(..)
    -- ** Statements
  , Seq(..)
    -- ** Type synonyms
  , TypSyn (..)
    -- ** Structs
  , StructCon (..)
  , ElimStruct(..)
  , makeElimStruct
    -- ** Pattern Synonyms
  , PatSyn(..)
  , CompletePragma(..)
  ) where

import Data.Type.Nat (SNat, SNatI, snat)
import Data.Type.Nat qualified as Fin
import DeBruijn (Add (..), Ctx, EmptyCtx, Idx (..), Wk (..))

import HsBindgen.Backend.Hs.AST.CompletePragma
import HsBindgen.Backend.Hs.AST.Strategy
import HsBindgen.Backend.Hs.CallConv
import HsBindgen.Backend.Hs.Haddock.Documentation qualified as HsDoc
import HsBindgen.Backend.Hs.Name qualified as Hs
import HsBindgen.Backend.Hs.Origin qualified as Origin
import HsBindgen.Backend.SHs.AST qualified as SHs
import HsBindgen.Backend.UniqueSymbol
import HsBindgen.BindingSpec.Private.V1 qualified as BindingSpec
import HsBindgen.Frontend.Pass.Final
import HsBindgen.Frontend.Pass.TypecheckMacros.IsPass
import HsBindgen.Imports
import HsBindgen.Instances qualified as Inst
import HsBindgen.IR.C qualified as C
import HsBindgen.IR.Hs qualified as Hs
import HsBindgen.Language.Haskell qualified as Hs
import HsBindgen.NameHint
import HsBindgen.Orphans ()

{-------------------------------------------------------------------------------
  Information about generated code
-------------------------------------------------------------------------------}

data Field = Field{
      name    :: Hs.Name Hs.NsVar
    , typ     :: Hs.Type
    , origin  :: Origin.Field
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

-- | Struct
--
-- TODO <https://github.com/well-typed/hs-bindgen/issues/1757>
-- For enums we generate /both/ a newtype /and/ a struct, and then define
-- instances only for the struct. We should get rid of this nasty hack.
data Struct = Struct{
      name      :: Hs.Name Hs.NsTypeConstr
    , constr    :: Hs.Name Hs.NsConstr
    , fields    :: [Field]
    , origin    :: Maybe (Origin.Decl Origin.Struct)
    , instances :: Set Inst.TypeClass
    , comment   :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data EmptyData = EmptyData{
      name      :: Hs.Name Hs.NsTypeConstr
    , origin    :: Origin.Decl Origin.EmptyData
    , instances :: Set Inst.TypeClass
    , comment   :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data Newtype = Newtype{
      name      :: Hs.Name Hs.NsTypeConstr
    , constr    :: Hs.Name Hs.NsConstr
    , ffiType   :: Maybe BindingSpec.HsFFIType
    , field     :: Field
    , origin    :: Origin.Decl Origin.Newtype
    , instances :: Set Inst.TypeClass
    , comment   :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data ForeignImportDecl = ForeignImportDecl{
      name       :: Hs.TermName
    , parameters :: [FunctionParameter Hs.FFIType]
    , result     :: Hs.FFIResType
    , origName   :: C.DeclName
    , callConv   :: CallConv
    , origin     :: Origin.ForeignImport
    , comment    :: Maybe HsDoc.Comment
    , safety     :: SHs.Safety
    }
  deriving stock (Generic, Show)

data FunctionParameter t = FunctionParameter{
      typ     :: t
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data FunctionDecl = FunctionDecl{
      name       :: Hs.TermName
    , parameters :: [FunctionParameter Hs.Type]
    , result     :: Hs.Type
    , body       :: SHs.ClosedExpr
    , origin     :: Origin.ForeignImport
    , pragmas    :: [SHs.Pragma]
    , comment    :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data UnionGetter = UnionGetter{
      name    :: Hs.Name Hs.NsVar
    , typ     :: Hs.Type
    , constr  :: Hs.Name Hs.NsTypeConstr
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data UnionSetter = UnionSetter{
      name    :: Hs.Name Hs.NsVar
    , typ     :: Hs.Type
    , constr  :: Hs.Name Hs.NsTypeConstr
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data DeriveInstance = DeriveInstance{
      strategy :: Strategy Hs.Type
    , clss     :: Inst.TypeClass
    , name     :: Hs.Name Hs.NsTypeConstr
    , comment  :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

data Var = Var{
      name    :: Hs.TermName
    , typ     :: SHs.ClosedType
    , expr    :: SHs.ClosedExpr
    , pragmas :: [SHs.Pragma]
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Show, Generic)

{-------------------------------------------------------------------------------
  Variable binding
-------------------------------------------------------------------------------}

-- | Lambda abstraction
type Lambda :: (Ctx -> Star) -> (Ctx -> Star)
data Lambda t ctx = Lambda
    NameHint  -- ^ name suggestion
    (t (S ctx)) -- ^ body

deriving instance Show (t (S ctx)) => Show (Lambda t ctx)

-- | Direct application (non-applicative)
--
-- Unlike t'Ap' which uses applicative composition (<*>), DirectApply directly
-- applies a constructor to a list of expressions.
--
data Apply pure xs ctx = Apply (pure ctx) [xs ctx]
  deriving stock (Generic, Show)

-- | Applicative structure
data Ap pure xs ctx = Ap (pure ctx) [xs ctx]
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  Declarations
-------------------------------------------------------------------------------}

-- | Top-level declaration
type Decl :: Star -> Star
data Decl l where
    DeclTypSyn               :: TypSyn               -> Decl l
    DeclData                 :: Struct               -> Decl l
    DeclEmpty                :: EmptyData            -> Decl l
    DeclNewtype              :: Newtype              -> Decl l
    DeclPatSyn               :: PatSyn               -> Decl l
    DeclCompletePragma       :: CompletePragma       -> Decl l
    DeclDefineInstance       :: DefineInstance       -> Decl l
    DeclDeriveInstance       :: DeriveInstance       -> Decl l
    DeclForeignImport        :: ForeignImportDecl    -> Decl l
    DeclForeignImportDynamic :: ForeignImportDynamic -> Decl l
    DeclForeignImportWrapper :: ForeignImportWrapper -> Decl l
    DeclFunction             :: FunctionDecl         -> Decl l
    DeclMacroValue           :: MacroValue l         -> Decl l
    DeclVar                  :: Var                  -> Decl l
deriving stock instance Show (Decl l)

data DefineInstance = DefineInstance{
      instanceDecl :: InstanceDecl
    , comment      :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

-- | Class instance declaration (with code that /we/ generate)
type InstanceDecl :: Star
data InstanceDecl where
    -- | 'StaticSize' only needs the type's name (its methods use proxies), so
    -- it accepts a bare name rather than a 'Struct'.  This lets field-less empty
    -- data types (the @emptydata@ representation) carry a 'StaticSize' instance.
    InstanceStaticSize      :: Hs.Name Hs.NsTypeConstr -> StaticSizeInstance -> InstanceDecl
    InstanceReadRaw         :: Struct -> ReadRawInstance -> InstanceDecl
    InstanceWriteRaw        :: Struct -> WriteRawInstance -> InstanceDecl
    InstanceStorable        :: Struct -> StorableInstance -> InstanceDecl
    InstanceHasCField       :: HasCFieldInstance -> InstanceDecl
    InstanceHasCBitfield    :: HasCBitfieldInstance -> InstanceDecl
    InstanceHasField        :: HasFieldInstance -> InstanceDecl
    InstanceHasFieldCompat  :: HasFieldCompatInstance -> InstanceDecl
    InstanceHasFieldPtr     :: HasFieldPtrInstance -> InstanceDecl
    InstanceHasFlam         :: Struct -> HasFlamInstance -> InstanceDecl
    -- | The 'Struct' wraps the C enum's underlying integer field. Invariant:
    -- exactly one field. Established at 'HsBindgen.Backend.Hs.Translation'
    -- where these instances are built from a 'Newtype' carrying a single field.
    InstanceCEnum           :: Struct -> CEnumInstance -> InstanceDecl
    InstanceSequentialCEnum :: Struct -> SequentialCEnumInstance -> InstanceDecl
    InstanceCEnumShow       :: Struct -> InstanceDecl
    InstanceCEnumRead       :: Struct -> InstanceDecl
    InstanceToFunPtr        :: ToFunPtrInstance -> InstanceDecl
    InstanceFromFunPtr      :: FromFunPtrInstance -> InstanceDecl

deriving instance Show InstanceDecl

-- | Macro expression
type MacroValue :: Star -> Star
data MacroValue l = MacroValue {
    -- | Name of variable/function.
      name    :: Hs.Name Hs.NsVar
    -- | Type of variable/function.
    , expr    :: TypecheckedMacroValue l Final
    -- | RHS of variable/function.
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  Pattern Synonyms
-------------------------------------------------------------------------------}

-- | Pattern synonyms
--
-- Supports pattern synonyms of the following forms:
--
-- @
-- pattern P :: T
-- pattern P = C e
-- @
--
-- and
--
-- @
-- pattern P :: T
-- pattern P = e
-- @
--
data PatSyn = PatSyn{
      name    :: Hs.Name Hs.NsConstr
    , typ     :: Hs.Type
    , constr  :: Maybe (Hs.Name Hs.NsConstr)
    , value   :: Integer
    , origin  :: Origin.PatSyn
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'ToFunPtr'
-------------------------------------------------------------------------------}

-- | 'HsBindgen.Runtime.Support.FunPtr.Class.ToFunPtr' instance
data ToFunPtrInstance = ToFunPtrInstance{
      typ  :: Hs.Type
    , body :: UniqueSymbol
    }
  deriving stock (Generic, Show)

-- | A dynamic wrapper
--
-- For example, assuming @name = "foo"@ and @funType = ft@
--
-- > foreign import ccall "wrapper" foo :: ft -> IO (FunPtr ft)
--
-- <https://www.haskell.org/onlinereport/haskell2010/haskellch8.html#x15-1620008.5.1>
data ForeignImportWrapper = ForeignImportWrapper {
      name    :: UniqueSymbol
    , funType :: Hs.FFIFunType
    , origin  :: Origin.ForeignImport
    , comment :: Maybe HsDoc.Comment
    }
    deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'FromFunPtr'
-------------------------------------------------------------------------------}

-- | 'HsBindgen.Runtime.Support.FunPtr.Class.FromFunPtr' instance
data FromFunPtrInstance = FromFunPtrInstance{
      typ  :: Hs.Type
    , body :: UniqueSymbol
    }
  deriving stock (Generic, Show)

-- | A dynamic import
--
-- For example, assuming @name = "foo"@ and @funType = ft@
--
-- > foreign import ccall "dynamic" foo :: FunPtr ft -> ft
--
-- <https://www.haskell.org/onlinereport/haskell2010/haskellch8.html#x15-1620008.5.1>
data ForeignImportDynamic = ForeignImportDynamic {
      name    :: UniqueSymbol
    , funType :: Hs.FFIFunType
    , origin  :: Origin.ForeignImport
    , comment :: Maybe HsDoc.Comment
    }
    deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  @StaticSize@, @ReadRaw@, @WriteRaw@
-------------------------------------------------------------------------------}

-- | 'HsBindgen.Runtime.Marshal.StaticSize' instance
--
-- Currently this models storable instances for structs /only/.
data StaticSizeInstance = StaticSizeInstance{
      staticSizeOf    :: Int
    , staticAlignment :: Int
    }
  deriving stock (Generic, Show)

-- | 'HsBindgen.Runtime.Marshal.ReadRaw' instance
--
-- Currently this models storable instances for structs /only/.
data ReadRawInstance = ReadRawInstance{
      readRaw :: Lambda (Ap StructCon ReadRawCField) EmptyCtx
    }
  deriving stock (Generic, Show)

-- | 'HsBindgen.Runtime.Marshal.WriteRaw' instance
--
-- Currently this models storable instances for structs /only/.
data WriteRawInstance = WriteRawInstance{
      writeRaw :: Lambda (Lambda (ElimStruct (Seq WriteRawCField))) EmptyCtx
    }
  deriving stock (Generic, Show)

-- | A call to 'HsBindgen.Runtime.HasCField.readRawCField', 'HsBindgen.Runtime.HasCBitfield.readRawCBitfield', or 'HsBindgen.Runtime.HasCField.readRawByteOff'
type ReadRawCField :: Ctx -> Star
data ReadRawCField ctx =
    ReadRawCField Hs.Type (Idx ctx)
  | ReadRawCBitfield Hs.Type (Idx ctx)
  | ReadRawByteOff (Idx ctx) Int
  deriving stock (Generic, Show)

-- | A call to 'HsBindgen.Runtime.HasCField.writeRawCField', 'HsBindgen.Runtime.HasCBitfield.writeRawCBitfield', or 'HsBindgen.Runtime.HasCField.writeRawByteOff'
type WriteRawCField :: Ctx -> Star
data WriteRawCField ctx =
    WriteRawCField Hs.Type (Idx ctx) (Idx ctx)
  | WriteRawCBitfield Hs.Type (Idx ctx) (Idx ctx)
  | WriteRawByteOff (Idx ctx) Int (Idx ctx)
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'Storable'
-------------------------------------------------------------------------------}

-- | 'Foreign.Storable.Storable' instance
--
-- Currently this models storable instances for structs /only/.
--
-- <https://hackage.haskell.org/package/base/docs/Foreign-Storable.html#t:Storable>
data StorableInstance = StorableInstance{
      sizeOf    :: Int
    , alignment :: Int
    , peek      :: Lambda (Ap StructCon PeekCField) EmptyCtx
    , poke      :: Lambda (Lambda (ElimStruct (Seq PokeCField))) EmptyCtx
    }
  deriving stock (Generic, Show)

-- | A call to 'HsBindgen.Runtime.HasCField.peekCField', 'HsBindgen.Runtime.HasCBitfield.peekCBitfield', or 'Foreign.Storable.peekByteOff'.
type PeekCField :: Ctx -> Star
data PeekCField ctx =
    PeekCField Hs.Type (Idx ctx)
  | PeekCBitfield Hs.Type (Idx ctx)
  | PeekByteOff (Idx ctx) Int
  deriving stock (Generic, Show)

-- | A call to 'HsBindgen.Runtime.HasCField.pokeCField', 'HsBindgen.Runtime.HasCBitfield.pokeCBitfield', or 'Foreign.Storable.pokeByteOff'.
type PokeCField :: Ctx -> Star
data PokeCField ctx =
    PokeCField Hs.Type (Idx ctx) (Idx ctx)
  | PokeCBitfield Hs.Type (Idx ctx) (Idx ctx)
  | PokeByteOff (Idx ctx) Int (Idx ctx)
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'Prim'
-------------------------------------------------------------------------------}

-- | Prim instance for a struct
--
-- Generates explicit implementations of all Prim methods for structs
-- where all fields are Prim instances.
--
-- Unlike Storable which uses byte offsets and pointer operations, Prim uses
-- element indices and direct primitive operations. The key difference:
--
-- * Storable: @peekByteOff ptr byteOffset@
-- * Prim: @indexByteArray# arr# (numFields# *# i# +# fieldPos#)@
--
-- <https://hackage.haskell.org/package/primitive/docs/Data-Primitive-Types.html#t:Prim>
data PrimInstance = PrimInstance{
      -- | Total size in bytes
      sizeOf :: Int

      -- | Alignment requirement
    , alignment :: Int

      -- | @indexByteArray# :: ByteArray# -> Int# -> a@
      --
      -- Takes array and element index, returns struct by indexing each field
      -- Body: StructCon with direct field calls (no applicative)
    , indexByteArray :: Lambda (Lambda (Apply StructCon IndexByteArrayField)) EmptyCtx

      -- | @readByteArray# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, a #)@
      --
      -- Takes array, element index, and state; returns new state and struct
    , readByteArray :: Lambda (Lambda (Lambda ReadByteArrayFields)) EmptyCtx

      -- | @writeByteArray# :: MutableByteArray# s -> Int# -> a -> State# s -> State# s@
      --
      -- Takes array, element index, struct value, and state; returns new state
    , writeByteArray :: Lambda (Lambda (Lambda (Lambda (ElimStruct WriteByteArrayFields)))) EmptyCtx

      -- | @indexOffAddr# :: Addr# -> Int# -> a@
      --
      -- Takes address and element index, returns struct by indexing each field
      -- Body: StructCon with direct field calls (no applicative)
    , indexOffAddr :: Lambda (Lambda (Apply StructCon IndexOffAddrField)) EmptyCtx

      -- | readOffAddr# :: Addr# -> Int# -> State# s -> (# State# s, a #)
      --
      -- Takes address, element index, and state; returns new state and struct

    , readOffAddr :: Lambda (Lambda (Lambda ReadOffAddrFields)) EmptyCtx

      -- | writeOffAddr# :: Addr# -> Int# -> a -> State# s -> State# s
      --
      -- Takes address, element index, struct value, and state; returns new state
    , writeOffAddr :: Lambda (Lambda (Lambda (Lambda (ElimStruct WriteOffAddrFields)))) EmptyCtx
    }
  deriving stock (Generic, Show)

-- | Common field metadata for indexing operations
type IndexPrimFieldData :: Ctx -> Star
data IndexPrimFieldData ctx = IndexPrimFieldData{
      typ       :: Hs.Type -- ^ Field type
    , arg1      :: Idx ctx -- ^ First argument variable
    , arg2      :: Idx ctx -- ^ Second argument variable
    , pos       :: Int     -- ^ Field position (0-based)
    , numFields :: Int     -- ^ Total number of fields
    }
  deriving stock (Generic, Show)

-- | Index a field from ByteArray# using indexByteArray#
--
-- For a struct with n fields at element index i, field f is at position: n*i + f
-- Example: @indexByteArray# arr# (3# *# i# +# 1#)@ for field 1 of a 3-field struct
--
type IndexByteArrayField :: Ctx -> Star
data IndexByteArrayField ctx = IndexByteArrayField{
      metadata :: IndexPrimFieldData ctx
    }
  deriving stock (Generic, Show)

-- | Index a field from Addr# using indexOffAddr#
--
-- For a struct with n fields at element index i, field f is at position: n*i + f
-- Example: @indexOffAddr# addr# (3# *# i# +# 1#)@ for field 1 of a 3-field struct
type IndexOffAddrField :: Ctx -> Star
data IndexOffAddrField ctx = IndexOffAddrField{
      metadata :: IndexPrimFieldData ctx
    }
  deriving stock (Generic, Show)

-- | Common field metadata for read operations
type ReadPrimFieldsData :: Ctx -> Star
data ReadPrimFieldsData ctx = ReadPrimFieldsData{
      fields    :: [(Hs.Type, Int)] -- ^ Fields: (type, position)
    , arg1      :: Idx ctx         -- ^ First argument variable
    , arg2      :: Idx ctx         -- ^ Second argument variable
    , arg3      :: Idx ctx         -- ^ Third argument variable
    , numFields :: Int             -- ^ Total number of fields
    }
  deriving stock (Generic, Show)

-- | Read fields from MutableByteArray# with state threading
--
-- Generates nested case expressions to thread State# through multiple reads:
--
-- > case readByteArray# arr# (n# *# i# +# 0#) s0 of
-- >   (# s1, x #) -> case readByteArray# arr# (n# *# i# +# 1#) s1 of
-- >     (# s2, y #) -> (# s2, Struct x y #)
--
type ReadByteArrayFields :: Ctx -> Star
data ReadByteArrayFields ctx = ReadByteArrayFields{
      metadata :: ReadPrimFieldsData ctx
    }
  deriving stock (Generic, Show)

-- | Read fields from Addr# with state threading
--
-- Generates nested case expressions to thread State# through multiple reads:
--
-- > case readOffAddr# addr# (n# *# i# +# 0#) s0 of
-- >   (# s1, x #) -> case readOffAddr# addr# (n# *# i# +# 1#) s1 of
-- >     (# s2, y #) -> (# s2, Struct x y #)
--
type ReadOffAddrFields :: Ctx -> Star
data ReadOffAddrFields ctx = ReadOffAddrFields{
      metadata :: ReadPrimFieldsData ctx
    }
  deriving stock (Generic, Show)

-- | Common field metadata for write operations
data WritePrimFieldsData ctx = WritePrimFieldsData{
      fields    :: [(Hs.Type, Int, Idx ctx)] -- ^ Fields: (type, position, value variable)
    , arg1      :: Idx ctx                   -- ^ First argument variable
    , arg2      :: Idx ctx                   -- ^ Second argument variable
    , arg3      :: Idx ctx                   -- ^ Third argument variable
    , numFields :: Int                       -- ^ Total number of fields
    }
  deriving stock (Generic, Show)

-- | Write fields to MutableByteArray# with state threading
--
-- Generates sequential writes that thread State# through:
--
-- > case writeByteArray# arr# (n# *# i# +# 0#) x s0 of
-- >   s1 -> writeByteArray# arr# (n# *# i# +# 1#) y s1
--
type WriteByteArrayFields :: Ctx -> Star
data WriteByteArrayFields ctx = WriteByteArrayFields {
      metadata :: WritePrimFieldsData ctx
    }
  deriving stock (Generic, Show)

-- | Write fields to Addr# with state threading
--
-- Generates sequential writes that thread State# through:
--
-- > case writeOffAddr# addr# (n# *# i# +# 0#) x s0 of
-- >   s1 -> writeOffAddr# addr# (n# *# i# +# 1#) y s1
--
type WriteOffAddrFields :: Ctx -> Star
data WriteOffAddrFields ctx = WriteOffAddrFields {
      metadata :: WritePrimFieldsData ctx
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'HasCField'
-------------------------------------------------------------------------------}

-- | 'HsBindgen.Runtime.HasCField.HasCField' instance
data HasCFieldInstance = HasCFieldInstance {
      -- | The haskell type of the parent C object
      parentType :: Hs.Type

      -- | The name of the field
    , fieldName :: Hs.Name Hs.NsVar

      -- | The haskell type of the field
    , cFieldType :: Hs.Type

      -- | The offset (in number of bytes) of the field wrt the parent object
    , fieldOffset :: Int
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'HasCBitfield'
-------------------------------------------------------------------------------}

-- | 'HsBindgen.Runtime.HasCBitfield.HasCBitfield' instance
data HasCBitfieldInstance = HasCBitfieldInstance {
      -- | The haskell type of the parent C object
      parentType :: Hs.Type

      -- | The name of the bit-field
    , fieldName :: Hs.Name Hs.NsVar

      -- | The haskell type of the bit-field
    , cBitfieldType :: Hs.Type

      -- | The offset (in number of bit) of the bit-field wrt the parent object
    , bitOffset :: Int

      -- | The width (in number of bits) of the bit-field.
    , bitWidth :: Int
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'GHC.Records.HasField'
-------------------------------------------------------------------------------}

-- | 'GHC.Records.HasField' instance
data HasFieldInstance = HasFieldInstance {
      -- | The Haskell type of the parent C object
      parentType :: Hs.Type

      -- | The name of the field
    , fieldName :: Hs.Name Hs.NsVar

      -- | The haskell type of the field
    , fieldType :: Hs.Type

      -- | Implementation of member functions
    , impl :: HasFieldImpl
    }
  deriving stock (Generic, Show)

-- | 'GHC.Records.HasField.getField' implementation
data HasFieldImpl =
    -- | union fields
    HasFieldImplUnion
    -- | union bit-fields
  | HasFieldImplUnionBits {
        bitOffset :: Int
      , bitWidth :: Int
      }
    -- | indirect fields
  | HasFieldImplIndirect {
        -- | The name of the field to go from the current top-level struct/union
        -- to an anonyous struct/union
        nameTopToAnon :: Hs.Name Hs.NsVar
        -- | The name of the field to go from the anonymous struct/union to the
        -- target field (the one we are accessing indirectly)
      , nameAnonToTarget :: Hs.Name Hs.NsVar
      }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'GHC.Records.Compat.HasField'
-------------------------------------------------------------------------------}

-- | 'GHC.Records.Compat.HasField' instance
data HasFieldCompatInstance = HasFieldCompatInstance {
      -- | The Haskell type of the parent C object
      parentType :: Hs.Type

      -- | The name of the field
    , fieldName :: Hs.Name Hs.NsVar

      -- | The haskell type of the field
    , fieldType :: Hs.Type

      -- | Implementation of member functions
    , impl :: HasFieldCompatImpl
    }
  deriving stock (Generic, Show)

-- | 'GHC.Records.Compat.HasField.hasField' implementation
data HasFieldCompatImpl =
    -- | structs, typedefs, enums, and macro types
    HasFieldCompatImplRecord {
        constr :: Hs.Name Hs.NsConstr
        -- | Fields that are unchanged
      , otherFields :: [Hs.Name Hs.NsVar]
      }
    -- | union fields
  | HasFieldCompatImplUnion
    -- | union bit-fields
  | HasFieldCompatImplUnionBits {
        bitOffset :: Int
      , bitWidth :: Int
      }
    -- | Indirect fields
  | HasFieldCompatImplIndirect {
        -- | The name of the field to go from the current top-level struct/union
        -- to an anonyous struct/union
        nameTopToAnon :: Hs.Name Hs.NsVar
        -- | The name of the field to go from the anonymous struct/union to the
        -- target field (the one we are accessing indirectly)
      , nameAnonToTarget :: Hs.Name Hs.NsVar
      }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'GHC.Records.HasField' for the pointer manipulation API
-------------------------------------------------------------------------------}

-- | 'GHC.Records.HasField' instance for the pointer manipulation API
data HasFieldPtrInstance = HasFieldPtrInstance {
      -- | The Haskell type of the parent C object
      parentType :: Hs.Type

      -- | The name of the field
    , fieldName :: Hs.Name Hs.NsVar

      -- | The haskell type of the field
    , fieldType :: Hs.Type

      -- | Implement the instance via a 'HsBindgen.Runtime.HasCField.HasCField'
      -- or 'HsBindgen.Runtime.HasCBitfield.HasCBitfield' instance.
    , deriveVia :: HasFieldPtrInstanceVia
    }
  deriving stock (Generic, Show)

-- | See the @deriveVia@ field of 'HasFieldPtrInstance'.
data HasFieldPtrInstanceVia = ViaHasCField | ViaHasCBitfield
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  'HasFlam'
-------------------------------------------------------------------------------}

data HasFlamInstance = HasFlamInstance {
      typ    :: Hs.Type
    , offset :: Int
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  CEnum
-------------------------------------------------------------------------------}

data CEnumInstance = CEnumInstance {
      fieldType    :: Hs.Type
    , valueNames   :: Map Integer (NonEmpty String)
    , isSequential :: Bool
    }
  deriving stock (Generic, Show)

data SequentialCEnumInstance = SequentialCEnumInstance {
      minName :: Hs.Name Hs.NsConstr
    , maxName :: Hs.Name Hs.NsConstr
    }
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  Statements
-------------------------------------------------------------------------------}

-- | Simple sequential composition (no bindings)
newtype Seq t ctx = Seq [t ctx]
  deriving stock (Generic, Show)

{-------------------------------------------------------------------------------
  Type synonyms
-------------------------------------------------------------------------------}

-- | Type synonyms
--
-- At the moment, we do not support type variables.
data TypSyn = TypSyn{
      name    :: Hs.Name Hs.NsTypeConstr
    , typ     :: Hs.Type
      -- TODO <https://github.com/well-typed/hs-bindgen/issues/1448>
      -- Temporary: origin will be gone.
    , origin  :: Origin.Decl Origin.EmptyData
    , comment :: Maybe HsDoc.Comment
    }
  deriving stock (Generic, Show)


{-------------------------------------------------------------------------------
  Structs
-------------------------------------------------------------------------------}

type StructCon :: Ctx -> Star
data StructCon ctx where
    StructCon :: Struct -> StructCon ctx

deriving instance Show (StructCon ctx)

-- | Case split for a struct
type ElimStruct :: (Ctx -> Star) -> (Ctx -> Star)
data ElimStruct t ctx where
    ElimStruct ::
         Idx ctx
      -> Hs.Name Hs.NsConstr
      -> Vec n NameHint
      -> Add n ctx ctx'
      -> t ctx'
      -> ElimStruct t ctx

deriving instance (forall ctx'. Show (t ctx')) => Show (ElimStruct t ctx)

-- | Create 'HsBindgen.Backend.Hs.AST.ElimStruct' using kind-of HOAS interface.
makeElimStruct :: forall n ctx t.
     SNatI n
  => Idx ctx
  -> Hs.Name Hs.NsConstr
  -> Vec n NameHint
  -> (forall ctx'. Wk ctx ctx' -> Vec n (Idx ctx') -> t ctx')
  -> ElimStruct t ctx
makeElimStruct s constr hints kont = makeElimStruct' (snat :: SNat n) $ \add wk xs ->
    ElimStruct s constr hints add (kont wk xs)

-- TODO <https://github.com/well-typed/hs-bindgen/issues/1757>
-- - Use Data.Type.Nat.induction instead of explicit recursion.
-- - Verify that we bind fields in right order.
makeElimStruct' :: forall m ctx t.
     SNat m
  -> ( forall ctx'.
            Add m ctx ctx'
         -> Wk ctx ctx'
         -> Vec m (Idx ctx')
         -> ElimStruct t ctx
     )
  -> ElimStruct t ctx
makeElimStruct' Fin.SZ      kont = kont AZ IdWk VNil
makeElimStruct' (Fin.SS' n) kont = makeElimStruct' n $ \add wk xs ->
    kont (AS add) (SkipWk wk) (IZ ::: fmap IS xs)