{-# LANGUAGE RankNTypes #-}

module Plutarch.Extra.Record (
  mkRecord,
  mkRecordConstr,
  (.=),
  (.&),
  RecordMorphism,
  FieldName,
) where

import Control.Category (Category (id, (.)))
import Data.Coerce (coerce)
import Data.Kind (Type)
import GHC.OverloadedLabels (IsLabel (fromLabel))
import GHC.TypeLits (Symbol)
import Plutarch (PlutusType, S, Term, pcon, (#))
import Plutarch.Builtin (PAsData)
import Plutarch.DataRepr (PDataRecord, PLabeledType ((:=)), pdcons, pdnil)
import Prelude (($))

{- | Like 'Data.Proxy.Proxy' but local to this module.

 @since 1.3.0
-}
data FieldName (sym :: Symbol) = FieldName

{- | The use of two different 'Symbol's here allows unification to happen,
     ensuring 'FieldName' has a fully inferred 'Symbol'.

     For example, @'mkRecord' (#foo .= 'pconstantData' (42 :: 'Integer'))@ gets
     the correct type. Namely, @'Term' s ('PDataRecord' '["foo" ':= 'PInteger'])@.

     @since 1.3.0
-}
instance
  forall (sym :: Symbol) (sym' :: Symbol).
  (sym ~ sym') =>
  IsLabel sym (FieldName sym)
  where
  fromLabel :: FieldName sym
fromLabel = forall (sym :: Symbol). FieldName sym
FieldName

{- | Turn a constant 'RecordMorphism' into a fully built 'PDataRecord'.

 @since 1.3.0
-}
mkRecord :: forall (r :: [PLabeledType]) (s :: S). RecordMorphism s '[] r -> Term s (PDataRecord r)
mkRecord :: forall (r :: [PLabeledType]) (s :: S).
RecordMorphism s '[] r -> Term s (PDataRecord r)
mkRecord RecordMorphism s '[] r
f = forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
RecordMorphism s as bs
-> Term s (PDataRecord as) -> Term s (PDataRecord bs)
runRecordMorphism RecordMorphism s '[] r
f forall (s :: S). Term s (PDataRecord '[])
pdnil

{- | 'mkRecord' but for known data-types.

This allows you to dynamically construct a record type constructor.

=== Example:
@
'mkRecordConstr'
  'PScriptContext'
  ( #txInfo '.=' '(Your PTxInfo)'
      '.&' #purpose '.=' '(Your PScriptPurpose)'
  )
@
Is the same as

@
'pconstant' ('ScriptContext' '(Your TxInfo)' '(Your ScriptPurpose)')
@

@since 1.3.0
-}
mkRecordConstr ::
  forall (r :: [PLabeledType]) (s :: S) (pt :: S -> Type).
  PlutusType pt =>
  -- | The constructor. This is just the Haskell-level constructor for the type.
  --   For 'Plutarch.Api.V2.Maybe.PMaybeData', this would
  --   be 'Plutarch.Api.V2.Maybe.PDJust', or 'Plutarch.Api.V2.Maybe.PNothing'.
  (forall s'. Term s' (PDataRecord r) -> pt s') ->
  -- | The morphism that builds the record.
  RecordMorphism s '[] r ->
  Term s pt
mkRecordConstr :: forall (r :: [PLabeledType]) (s :: S) (pt :: S -> Type).
PlutusType pt =>
(forall (s' :: S). Term s' (PDataRecord r) -> pt s')
-> RecordMorphism s '[] r -> Term s pt
mkRecordConstr forall (s' :: S). Term s' (PDataRecord r) -> pt s'
ctr = forall (a :: S -> Type) (s :: S). PlutusType a => a s -> Term s a
pcon forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (s' :: S). Term s' (PDataRecord r) -> pt s'
ctr forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: [PLabeledType]) (s :: S).
RecordMorphism s '[] r -> Term s (PDataRecord r)
mkRecord

{- | A morphism from one 'PDataRecord' to another, representing some sort of consing of data.

 @since 1.3.0
-}
newtype RecordMorphism (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType])
  = RecordMorphism (Term s (PDataRecord as) -> Term s (PDataRecord bs))

-- | @since 3.8.0
runRecordMorphism ::
  forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
  RecordMorphism s as bs ->
  Term s (PDataRecord as) ->
  Term s (PDataRecord bs)
runRecordMorphism :: forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
RecordMorphism s as bs
-> Term s (PDataRecord as) -> Term s (PDataRecord bs)
runRecordMorphism (RecordMorphism Term s (PDataRecord as) -> Term s (PDataRecord bs)
f) = Term s (PDataRecord as) -> Term s (PDataRecord bs)
f

-- | @since 1.3.0
instance Category (RecordMorphism s) where
  id :: forall (a :: [PLabeledType]). RecordMorphism s a a
id = forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
(Term s (PDataRecord as) -> Term s (PDataRecord bs))
-> RecordMorphism s as bs
RecordMorphism forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id
  RecordMorphism s b c
f . :: forall (b :: [PLabeledType]) (c :: [PLabeledType])
       (a :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
. RecordMorphism s a b
g = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
RecordMorphism s as bs
-> Term s (PDataRecord as) -> Term s (PDataRecord bs)
runRecordMorphism RecordMorphism s b c
f forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
RecordMorphism s as bs
-> Term s (PDataRecord as) -> Term s (PDataRecord bs)
runRecordMorphism RecordMorphism s a b
g

infix 7 .=

{- | Cons a labeled type as a 'RecordMorphism'.

 @since 3.1.0
-}
(.=) ::
  forall (sym :: Symbol) (a :: S -> Type) (as :: [PLabeledType]) (s :: S).
  -- | The field name. You can use @-XOverloadedLabels@ to enable the syntax:
  --   @#hello ~ 'FieldName' "hello"@
  FieldName sym ->
  -- | The value at that field. This must be 'PAsData', because the underlying
  --   type is @'PlutusCore.Data.Constr' 'Integer' ['PlutusCore.Data.Data']@.
  Term s (PAsData a) ->
  RecordMorphism s as ((sym ':= a) ': as)
FieldName sym
_ .= :: forall (sym :: Symbol) (a :: S -> Type) (as :: [PLabeledType])
       (s :: S).
FieldName sym
-> Term s (PAsData a) -> RecordMorphism s as ((sym ':= a) : as)
.= Term s (PAsData a)
x = forall (s :: S) (as :: [PLabeledType]) (bs :: [PLabeledType]).
(Term s (PDataRecord as) -> Term s (PDataRecord bs))
-> RecordMorphism s as bs
RecordMorphism forall a b. (a -> b) -> a -> b
$ \Term s (PDataRecord as)
rest -> forall (label :: Symbol) (a :: S -> Type) (l :: [PLabeledType])
       (s :: S).
Term
  s
  (PAsData a
   :--> (PDataRecord l :--> PDataRecord ((label ':= a) : l)))
pdcons forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PAsData a)
x forall (s :: S) (a :: S -> Type) (b :: S -> Type).
HasCallStack =>
Term s (a :--> b) -> Term s a -> Term s b
# Term s (PDataRecord as)
rest

infixr 6 .&

{- | Compose two 'RecordMorphism's.

 @since 1.3.0
-}
(.&) ::
  forall
    (s :: S)
    (a :: [PLabeledType])
    (b :: [PLabeledType])
    (c :: [PLabeledType]).
  RecordMorphism s b c ->
  RecordMorphism s a b ->
  RecordMorphism s a c
.& :: forall (s :: S) (a :: [PLabeledType]) (b :: [PLabeledType])
       (c :: [PLabeledType]).
RecordMorphism s b c
-> RecordMorphism s a b -> RecordMorphism s a c
(.&) = forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
(.)