{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE DerivingVia             #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE OverloadedLabels        #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE TypeApplications        #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Plutus.Contract.Schema(
      Handlers(..)
    , handlerName
    , handlerArgument
    , Event(..)
    , eventName
    , initialise
    , Input
    , Output
    , EmptySchema
    ) where

import Data.Aeson (FromJSON, ToJSON (toJSON), Value)
import Data.Row as Row
import Data.Row.Internal
import Data.Row.Variants qualified as Variants
import Prettyprinter

import Data.Row.Extras

import GHC.TypeLits

{- Note [Contract Schema]

Every contract has a schema that describes the data types used by the contract
to interact with the outside world. Conceptually the schema is a map of symbols
to pairs of types. Each entry in this map stands for a named request-response
pair.

For example, the 'WriteTx' interaction is defined as

  type WriteTx = "tx" .== ((), [LedgerTxConstraints])

Meaning that the output produced by the contract (2nd element) is a list of
unbalanced transactions, and the input the contract expects as a result (1st
element) is the unit value, telling it that the transactions have been
submitted.

In practice the schema is a type of the 'Data.Row.Row' kind.

-}

type EmptySchema = Row.Empty

newtype Event s = Event { Event s -> Var (Input s)
unEvent :: Var (Input s) }

eventName :: Forall (Input s) Unconstrained1 => Event s -> String
eventName :: Event s -> String
eventName (Event Var (Input s)
v) = (String, ()) -> String
forall a b. (a, b) -> a
fst ((String, ()) -> String) -> (String, ()) -> String
forall a b. (a -> b) -> a -> b
$ (forall a. Unconstrained1 a => a -> ())
-> Var (Input s) -> (String, ())
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
Variants.eraseWithLabels @Unconstrained1 (() -> a -> ()
forall a b. a -> b -> a
const ()) Var (Input s)
v

deriving newtype instance Forall (Input s) Show => Show (Event s)
deriving newtype instance Forall (Input s) Eq => Eq (Event s)

instance (Forall (Input s) Pretty) => Pretty (Event s) where
  pretty :: Event s -> Doc ann
pretty (Event Var (Input s)
e) =
    let (Doc ann
lbl, Doc ann
vl) = (forall a. Pretty a => a -> Doc ann)
-> Var (Input s) -> (Doc ann, Doc ann)
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
Variants.eraseWithLabels @Pretty forall a. Pretty a => a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Var (Input s)
e in
    Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
hang Int
1 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [Doc ann
lbl Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
colon, Doc ann
vl])

deriving via JsonVar (Input s) instance (AllUniqueLabels (Input s), Forall (Input s) FromJSON) => FromJSON (Event s)

deriving via JsonVar (Input s) instance (Forall (Input s) ToJSON) => ToJSON (Event s)

newtype Handlers s = Handlers { Handlers s -> Var (Output s)
unHandlers :: Var (Output s) }

handlerName :: Forall (Output s) Unconstrained1 => Handlers s -> String
handlerName :: Handlers s -> String
handlerName (Handlers Var (Output s)
v) = (String, ()) -> String
forall a b. (a, b) -> a
fst ((String, ()) -> String) -> (String, ()) -> String
forall a b. (a -> b) -> a -> b
$ (forall a. Unconstrained1 a => a -> ())
-> Var (Output s) -> (String, ())
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
Variants.eraseWithLabels @Unconstrained1 (() -> a -> ()
forall a b. a -> b -> a
const ()) Var (Output s)
v

handlerArgument :: Forall (Output s) ToJSON => Handlers s -> Value
handlerArgument :: Handlers s -> Value
handlerArgument (Handlers Var (Output s)
v) = (forall a. ToJSON a => a -> Value) -> Var (Output s) -> Value
forall (c :: * -> Constraint) (ρ :: Row *) b.
Forall ρ c =>
(forall a. c a => a -> b) -> Var ρ -> b
Variants.erase @ToJSON forall a. ToJSON a => a -> Value
toJSON Var (Output s)
v

deriving via (JsonVar (Output s)) instance Forall (Output s) ToJSON => ToJSON (Handlers s)
deriving via (JsonVar (Output s)) instance (AllUniqueLabels (Output s), Forall (Output s) FromJSON) => FromJSON (Handlers s)

deriving newtype instance Forall (Output s) Show => Show (Handlers s)
deriving newtype instance Forall (Output s) Eq   => Eq (Handlers s)

instance (Forall (Output s) Pretty) => Pretty (Handlers s) where
  pretty :: Handlers s -> Doc ann
pretty (Handlers Var (Output s)
s) =
    let (Doc ann
lbl, Doc ann
vl) = (forall a. Pretty a => a -> Doc ann)
-> Var (Output s) -> (Doc ann, Doc ann)
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
Variants.eraseWithLabels @Pretty forall a. Pretty a => a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Var (Output s)
s in
    Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
hang Int
1 (Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep [Doc ann
lbl Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
forall ann. Doc ann
colon, Doc ann
vl])

initialise ::
  forall (s :: Row *) l a.
  ( KnownSymbol l
  , AllUniqueLabels (Output s)
  , HasType l a (Output s)
  )
  => a
  -> Handlers s
initialise :: a -> Handlers s
initialise a
a =
  Var (Output s) -> Handlers s
forall (s :: Row *). Var (Output s) -> Handlers s
Handlers (Label l -> (Output s .! l) -> Var (Output s)
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
Variants.IsJust @l @(Output s) (Label l
forall (s :: Symbol). Label s
Label @l) a
Output s .! l
a)

--  | Given a schema 's', 'Input s' is the 'Row' type of the inputs that
--    contracts with this schema accept. See [Contract Schema]
type family Input (r :: Row *) where
  Input ('R r) = 'R (InputR r)

type family InputR (r :: [LT *]) where
  InputR '[] = '[]
  InputR (l ':-> (t1, _) ': r) =
    l ':-> t1 ': InputR r
  InputR (l ':-> t ': _) =
    TypeError ('Text "Input requires all types to be tuples."
                :$$: 'Text "For one, the field labelled " :<>: ShowType l :<>: 'Text " has type " :<>: ShowType t)

--  | Given a schema 's', 'Output s' is the 'Row' type of the outputs that
--    contracts with this schema produce. See [Contract Schema]
type family Output (r :: Row *) where
  Output ('R r) = 'R (OutputR r)

type family OutputR (r :: [LT *]) where
  OutputR '[] = '[]
  OutputR (l ':-> (_, t2) ': r) =
    l ':-> t2 ': OutputR r
  OutputR (l ':-> t ': _) =
    TypeError ('Text "Output requires all types to be tuples."
                :$$: 'Text "For one, the field labelled " :<>: ShowType l :<>: 'Text " has type " :<>: ShowType t)