-- | Common implementations of entrypoints.
module Lorentz.EntryPoints.Impl
  ( EpdPlain
  , EpdRecursive
  ) where

import qualified Data.Kind as Kind
import Data.Singletons (SingI (..))
import Data.Singletons.Prelude (Sing (STrue, SFalse))
import Data.Singletons.Prelude.Eq ((%==))
import Data.Type.Bool (If)
import qualified GHC.Generics as G
import Util.TypeLits
import Fcf (Exp, Eval)
import qualified Fcf

import Michelson.Typed
import Michelson.Typed.Haskell.Instr.Sum (IsPrimitiveValue)
import Michelson.Typed.Haskell.Value (GValueType, GenericIsoValue)
import Michelson.Untyped (FieldAnn, noAnn)
import Lorentz.Value
import Util.Type
import Util.Fcf (Over2, type (<|>), TyEqSing)

import Lorentz.EntryPoints.Helpers
import Lorentz.EntryPoints.Core
import Lorentz.TypeAnns

-- | Implementation of 'ParameterHasEntryPoints' which fits for case when
-- your contract exposes multiple entrypoints via having sum type as its
-- parameter.
--
-- In particular, each constructor would produce a homonymous entrypoint with
-- argument type equal to type of constructor field (each constructor should
-- have only one field).
-- Constructor called 'Default' will designate the default entrypoint.
data EpdPlain
instance PlainEntryPointsC 'False cp => EntryPointsDerivation EpdPlain cp where
  type EpdAllEntryPoints EpdPlain cp = PlainAllEntryPointsExt 'False cp
  type EpdLookupEntryPoint EpdPlain cp = PlainLookupEntryPointExt 'False cp
  epdNotes = plainEpdNotesExt @'False @cp
  epdCall = plainEpdCallExt @'False @cp

-- | Similar to 'EpdPlain', but for case of parameter being defined as
-- several nested datatypes.
--
-- In particular, this will traverse sum types recursively, stopping at
-- Michelson primitives (like 'Natural') and constructors with number of
-- fields different from one.
--
-- It does not assign names to intermediate nodes of 'Or' tree, only to the very
-- leaves.
data EpdRecursive
instance PlainEntryPointsC 'True cp => EntryPointsDerivation EpdRecursive cp where
  type EpdAllEntryPoints EpdRecursive cp = PlainAllEntryPointsExt 'True cp
  type EpdLookupEntryPoint EpdRecursive cp = PlainLookupEntryPointExt 'True cp
  epdNotes = plainEpdNotesExt @'True @cp
  epdCall = plainEpdCallExt @'True @cp

type PlainAllEntryPointsExt deep cp = AllEntryPoints deep (BuildEPTree deep cp) cp

type PlainLookupEntryPointExt deep cp = LookupEntryPoint deep (BuildEPTree deep cp) cp

plainEpdNotesExt
  :: forall deep cp.
     (PlainEntryPointsC deep cp, HasCallStack)
  => Notes (ToT cp)
plainEpdNotesExt = mkEntryPointsNotes @deep @(BuildEPTree deep cp) @cp

plainEpdCallExt
  :: forall deep cp name.
     (PlainEntryPointsC deep cp, ParameterScope (ToT cp), KnownSymbol name)
  => Label name
  -> EpConstructionRes (ToT cp) (Eval (LookupEntryPoint deep (BuildEPTree deep cp) cp name))
plainEpdCallExt = mkEpLiftSequence @deep @(BuildEPTree deep cp) @cp

type PlainEntryPointsC deep cp =
  ( GenericIsoValue cp
  , EntryPointsNotes deep (BuildEPTree deep cp) cp
  , RequireSumType cp
  )

-- | Entrypoints tree - skeleton on 'TOr' tree later used to distinguish
-- between constructors-entrypoints and constructors which consolidate
-- a whole pack of entrypoints.
data EPTree
  = EPNode EPTree EPTree
  | EPLeaf

-- | Build 'EPTree' by parameter type.
type BuildEPTree deep a = GBuildEntryPointsTree deep (G.Rep a)

type family GBuildEntryPointsTree (deep :: Bool) (x :: Kind.Type -> Kind.Type)
             :: EPTree where
  GBuildEntryPointsTree deep (G.D1 _ x) =
    GBuildEntryPointsTree deep x
  GBuildEntryPointsTree deep (x G.:+: y) =
    'EPNode (GBuildEntryPointsTree deep x) (GBuildEntryPointsTree deep y)
  GBuildEntryPointsTree 'False (G.C1 _ _) =
    'EPLeaf
  GBuildEntryPointsTree 'True (G.C1 _ x) =
    GBuildEntryPointsTree 'True x
  GBuildEntryPointsTree deep (G.S1 _ x) =
    GBuildEntryPointsTree deep x
  GBuildEntryPointsTree _ G.U1 =
    'EPLeaf
  GBuildEntryPointsTree _ (_ G.:*: _) =
    'EPLeaf
  GBuildEntryPointsTree deep (G.Rec0 a) =
    If (IsPrimitiveValue a)
       'EPLeaf
       (BuildEPTree deep a)

-- | Traverses sum type and constructs 'Notes' which report
-- constructor names via field annotations.
type EntryPointsNotes deep ep a = (Generic a, GEntryPointsNotes deep ep (G.Rep a))

-- | Makes up notes with proper field annotations for given parameter.
mkEntryPointsNotes
  :: forall deep ep a.
      (EntryPointsNotes deep ep a, GenericIsoValue a, HasCallStack)
  => Notes (ToT a)
mkEntryPointsNotes = fst $ gMkEntryPointsNotes @deep @ep @(G.Rep a)

-- | Makes up a way to lift entrypoint argument to full parameter.
mkEpLiftSequence
  :: forall deep ep a name.
      ( EntryPointsNotes deep ep a, ParameterScope (ToT a)
      , GenericIsoValue a, KnownSymbol name
      )
  => Label name
  -> EpConstructionRes (ToT a) (Eval (LookupEntryPoint deep ep a name))
mkEpLiftSequence = gMkEpLiftSequence @deep @ep @(G.Rep a)

-- | Fetches information about all entrypoints - leaves of 'Or' tree.
type AllEntryPoints deep ep a = GAllEntryPoints deep ep (G.Rep a)

-- | Fetches information about all entrypoints - leaves of 'Or' tree.
type LookupEntryPoint deep ep a = GLookupEntryPoint deep ep (G.Rep a)

-- | Generic traversal for 'EntryPointsNotes'.
class GEntryPointsNotes (deep :: Bool) (ep :: EPTree) (x :: Kind.Type -> Kind.Type) where
  type GAllEntryPoints deep ep x :: [(Symbol, Kind.Type)]
  type GLookupEntryPoint deep ep x :: Symbol -> Exp (Maybe Kind.Type)

  {- | Returns:
    1. Notes corresponding to this level;
    2. Field annotation for this level (and which should be used one level above).
  -}
  gMkEntryPointsNotes :: HasCallStack => (Notes (GValueType x), FieldAnn)

  gMkEpLiftSequence
    :: (KnownSymbol name, ParameterScope (GValueType x))
    => Label name
    -> EpConstructionRes (GValueType x) (Eval (GLookupEntryPoint deep ep x name))

instance GEntryPointsNotes deep ep x => GEntryPointsNotes deep ep (G.D1 i x) where
  type GAllEntryPoints deep ep (G.D1 i x) = GAllEntryPoints deep ep x
  type GLookupEntryPoint deep ep (G.D1 i x) = GLookupEntryPoint deep ep x
  gMkEntryPointsNotes = gMkEntryPointsNotes @deep @ep @x
  gMkEpLiftSequence = gMkEpLiftSequence @deep @ep @x

instance (GEntryPointsNotes deep epx x, GEntryPointsNotes deep epy y) =>
         GEntryPointsNotes deep ('EPNode epx epy) (x G.:+: y) where
  type GAllEntryPoints deep ('EPNode epx epy) (x G.:+: y) =
    GAllEntryPoints deep epx x ++ GAllEntryPoints deep epy y
  type GLookupEntryPoint deep ('EPNode epx epy) (x G.:+: y) =
    Over2 (<|>) (GLookupEntryPoint deep epx x) (GLookupEntryPoint deep epy y)
  gMkEntryPointsNotes =
    let (xnotes, xann) = gMkEntryPointsNotes @deep @epx @x
        (ynotes, yann) = gMkEntryPointsNotes @deep @epy @y
    in (NTOr noAnn xann yann xnotes ynotes, noAnn)
  gMkEpLiftSequence label =
    case sing @(GValueType (x G.:+: y)) of
      STOr sl _ -> case (checkOpPresence sl, checkNestedBigMapsPresence sl) of
        (OpAbsent, NestedBigMapsAbsent) ->
          case gMkEpLiftSequence @deep @epx @x label of
            EpConstructed liftSeq -> EpConstructed (EplWrapLeft liftSeq)
            EpConstructionFailed ->
              case gMkEpLiftSequence @deep @epy @y label of
                EpConstructed liftSeq -> EpConstructed (EplWrapRight liftSeq)
                EpConstructionFailed -> EpConstructionFailed

instance ( GHasTypeAnn x, KnownSymbol ctor
         , ToT (GExtractField x) ~ GValueType x
         ) =>
         GEntryPointsNotes 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) where
  type GAllEntryPoints 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) =
    '[ '(ctor, GExtractField x) ]
  type GLookupEntryPoint 'False ep (G.C1 ('G.MetaCons ctor _1 _2) x) =
    JustOnEq ctor (GExtractField x)
  gMkEntryPointsNotes =
    (gGetTypeAnn @x, ctorNameToAnn @ctor)
  gMkEpLiftSequence (_ :: Label name) =
    case sing @ctor %== sing @name of
      STrue -> EpConstructed EplArgHere
      SFalse -> EpConstructionFailed

instance ( GHasTypeAnn x, KnownSymbol ctor
         , ToT (GExtractField x) ~ GValueType x
         ) =>
         GEntryPointsNotes 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) where
  type GAllEntryPoints 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
    '[ '(ctor, GExtractField x) ]
  type GLookupEntryPoint 'True 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
    JustOnEq ctor (GExtractField x)
  gMkEntryPointsNotes =
    (gGetTypeAnn @x, ctorNameToAnn @ctor)
  gMkEpLiftSequence (_ :: Label name) =
    case sing @ctor %== sing @name of
      STrue -> EpConstructed EplArgHere
      SFalse -> EpConstructionFailed

instance (ep ~ 'EPNode epx epy, GEntryPointsNotes 'True ep x) =>
         GEntryPointsNotes 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) where
  type GAllEntryPoints 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
    GAllEntryPoints 'True ('EPNode epx epy) x
  type GLookupEntryPoint 'True ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
    GLookupEntryPoint 'True ('EPNode epx epy) x
  gMkEntryPointsNotes = gMkEntryPointsNotes @'True @ep @x
  gMkEpLiftSequence = gMkEpLiftSequence @'True @ep @x

instance GEntryPointsNotes deep ep x => GEntryPointsNotes deep ep (G.S1 i x) where
  type GAllEntryPoints deep ep (G.S1 i x) = GAllEntryPoints deep ep x
  type GLookupEntryPoint deep ep (G.S1 i x) = GLookupEntryPoint deep ep x
  gMkEntryPointsNotes = gMkEntryPointsNotes @deep @ep @x
  gMkEpLiftSequence = gMkEpLiftSequence @deep @ep @x

instance (EntryPointsNotes deep ep a, GenericIsoValue a) =>
         GEntryPointsNotes deep ep (G.Rec0 a) where
  type GAllEntryPoints deep ep (G.Rec0 a) = AllEntryPoints deep ep a
  type GLookupEntryPoint deep ep (G.Rec0 a) = LookupEntryPoint deep ep a
  gMkEntryPointsNotes = (mkEntryPointsNotes @deep @ep @a, noAnn)
  gMkEpLiftSequence = mkEpLiftSequence @deep @ep @a

instance GEntryPointsNotes deep 'EPLeaf G.U1 where
  type GAllEntryPoints deep 'EPLeaf G.U1 = '[]
  type GLookupEntryPoint deep 'EPLeaf G.U1 = Fcf.ConstFn 'Nothing
  gMkEntryPointsNotes = (starNotes, noAnn)
  gMkEpLiftSequence _ = EpConstructionFailed

instance Each [Typeable, SingI] [GValueType x, GValueType y] =>
         GEntryPointsNotes deep 'EPLeaf (x G.:*: y) where
  type GAllEntryPoints deep 'EPLeaf (x G.:*: y) = '[]
  type GLookupEntryPoint deep 'EPLeaf (x G.:*: y) = Fcf.ConstFn 'Nothing
  gMkEntryPointsNotes = (starNotes, noAnn)
  gMkEpLiftSequence _ = EpConstructionFailed

-- Return 'Just' iff given entries of type @k1@ are equal.
type family JustOnEq (a :: k1) (b :: k2) :: k1 -> Exp (Maybe k2) where
  JustOnEq a b =
    Fcf.Flip Fcf.Guarded
      '[ TyEqSing a 'Fcf.:= Fcf.Pure ('Just b)
       , Fcf.Otherwise 'Fcf.:= Fcf.Pure 'Nothing
       ]

-- Get field type under 'G.C1'.
type family GExtractField (x :: Kind.Type -> Kind.Type) where
  GExtractField (G.S1 _ x) = GExtractField x
  GExtractField (G.Rec0 a) = a
  GExtractField G.U1 = ()