-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | Utilities for declaring and documenting entry points.
module Lorentz.Entrypoints.Doc
  ( DEntrypoint (..)
  , pattern DEntrypointDocItem
  , EntrypointKindHasDoc (..)
  , entrypointSection
  , DEntrypointReference (..)
  , EntryArrow (..)
  , PlainEntrypointsKind
  , FlattenedEntrypointsKind
  , FlattenedEntrypointsKindHiding
  , CommonContractBehaviourKind
  , CommonEntrypointsBehaviourKind
  , diEntrypointToMarkdown
  , SomeEntrypointArg (..)
  , DEntrypointArg (..)
  , DType (..)
  , DeriveCtorFieldDoc (..)
  , ParamBuilder (..)
  , ParamBuildingDesc (..)
  , ParamBuildingStep (..)
  , mkPbsWrapIn
  , clarifyParamBuildingSteps
  , emptyDEpArg
  , mkUType
  , mkDEpUType
  , mkDEntrypointArgSimple
  , DocumentEntrypoints
  , documentEntrypoint
  , entryCase
  , entryCase_
  , finalizeParamCallingDoc
  , finalizeParamCallingDoc'
  , areFinalizedParamBuildingSteps
  , entryCaseSimple_
  , entryCaseSimple
  , entryCaseFlattened_
  , entryCaseFlattened
  , entryCaseFlattenedHiding_
  , entryCaseFlattenedHiding
  , RequireFlatParamEps
  , RequireFlatEpDerivation
  ) where

import Control.Lens.Cons (_head)
import Data.Char (toLower)
import Data.Constraint (Dict(..))
import Data.Map qualified as Map
import Data.Singletons (fromSing)
import Data.Text qualified as T
import Data.Vinyl.Core (RMap, rappend)
import Fcf (IsJust, type (@@))
import Fmt (Buildable(..), build, fmt, listF)
import GHC.Generics ((:+:))
import GHC.Generics qualified as G

import Lorentz.ADT
import Lorentz.Annotation
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.Doc
import Lorentz.Entrypoints.Core
import Lorentz.Entrypoints.Helpers
import Lorentz.Entrypoints.Impl
import Morley.Michelson.Printer (printTypedValue)
import Morley.Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)
import Morley.Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue, sing)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Typed.Haskell.Doc
import Morley.Michelson.Typed.Haskell.Instr
import Morley.Michelson.Untyped qualified as Untyped
import Morley.Util.Label (Label)
import Morley.Util.Markdown
import Morley.Util.Type
import Morley.Util.TypeLits
import Morley.Util.TypeTuple
import Morley.Util.Typeable

-- | Gathers information about single entrypoint.
--
-- We assume that entry points might be of different kinds,
-- which is designated by phantom type parameter.
-- For instance, you may want to have several groups of entry points
-- corresponding to various parts of a contract - specifying different @kind@
-- type argument for each of those groups will allow you defining different
-- 'DocItem' instances with appropriate custom descriptions for them.
data DEntrypoint (kind :: Type) = DEntrypoint
  { depName :: Text
  , depSub :: SubDoc
  }

-- | Pattern that checks whether given 'SomeDocItem' hides 'DEntrypoint' inside
-- (of any entrypoint kind).
--
-- In case a specific kind is necessary, use plain @(cast -> Just DEntrypoint{..})@
-- construction instead.
pattern DEntrypointDocItem :: DEntrypoint kind -> SomeDocItem
pattern DEntrypointDocItem dep <- SomeDocItem (castIgnoringPhantom -> Just dep)

-- | Default implementation of 'docItemToMarkdown' for entrypoints.
diEntrypointToMarkdown :: HeaderLevel -> DEntrypoint level -> Markdown
diEntrypointToMarkdown lvl (DEntrypoint name block) =
  mdSeparator <>
  mdHeader lvl (mdTicked . build . over _head toLower $ name) <>
    ( modifyExample block
    $ subDocToMarkdown (nextHeaderLevel lvl)
    $ filterDEntrypointExample block
    )
  where
    filterDEntrypointExample (SubDoc subdoc) =
      SubDoc $ Map.delete (docItemPosition @DEntrypointExample) subdoc

    -- | Modify 'SubDoc' of an entrypoint to replace its example value with the one defined in
    -- 'DEntrypointExample' in an ad-hoc way.
    modifyExample :: SubDoc -> Markdown -> Markdown
    modifyExample (SubDoc sub) subDocMd =
      case (Map.lookup (docItemPosition @DEntrypointExample) sub) of
        Just (DocSection ((DocElem b _ ) :| _)) ->
          mdFindExampleIdAndReplace
            (docItemToMarkdown (HeaderLevel 0) $ b)
            subDocMd
        Nothing -> subDocMd

    mdFindExampleIdAndReplace :: Markdown -> Markdown -> Markdown
    mdFindExampleIdAndReplace replaceTxt inputText =
      build
      $ unlines
      $ (\w ->  case T.isInfixOf ("id=\"" <> (fmt @Text exampleId) <> "\"") w of
        True -> fmt @Text $ "    + " <>
          mdSubsection "Example" (mdAddId exampleId $ mdTicked replaceTxt)
        False -> w
        )
      <$> lines (fmt @Text inputText)
      where
        exampleId = "example-id"

-- | Describes location of entrypoints of the given kind.
--
-- All such entrypoints will be placed under the same "entrypoints" section,
-- and this instance defines characteristics of this section.
class Typeable ep => EntrypointKindHasDoc (ep :: Type) where
  -- | Can be used to make a kind equivalent to some other kind;
  -- if changing this, 'entrypointKindPos' and 'entrypointKindSectionName'
  -- will be ignored.
  type EntrypointKindOverride ep
  type EntrypointKindOverride ep = ep

  -- | Implement this when specifying 'EntrypointKindOverride'.
  -- This should never be normally used, but because @MINIMAL@ pragma
  -- can't specify type families, we use this hack.
  --
  -- Default implementation is a bottom (i.e. a runtime error).
  --
  -- If implemented, it should be
  --
  -- > entrypointKindOverrideSpecified = Dict
  entrypointKindOverrideSpecified :: Dict ((EntrypointKindOverride ep == ep) ~ False)
  entrypointKindOverrideSpecified = error "Called entrypointKindOverrideSpecified"

  -- | Position of the respective entrypoints section in the doc.
  -- This shares the same positions space with all other doc items.
  entrypointKindPos :: Natural
  default entrypointKindPos :: EntrypointKindHasDoc (EntrypointKindOverride ep) => Natural
  entrypointKindPos = entrypointKindPos @(EntrypointKindOverride ep)

  -- | Name of the respective entrypoints section.
  entrypointKindSectionName :: Text
  default entrypointKindSectionName :: EntrypointKindHasDoc (EntrypointKindOverride ep) => Text
  entrypointKindSectionName = entrypointKindSectionName @(EntrypointKindOverride ep)

  -- | Description in the respective entrypoints section.
  entrypointKindSectionDescription :: Maybe Markdown
  entrypointKindSectionDescription = Nothing

  {-# MINIMAL entrypointKindOverrideSpecified | (entrypointKindPos, entrypointKindSectionName) #-}

{-# WARNING entrypointKindOverrideSpecified "Normally you should never need to use this function" #-}

instance EntrypointKindHasDoc ep => DocItem (DEntrypoint ep) where
  type DocItemPlacement (DEntrypoint ep) = 'DocItemInlined
  type DocItemReferenced (DEntrypoint ep) = 'True
  docItemRef (DEntrypoint name _) = DocItemRefInlined $
    DocItemId ("entrypoints-" <> (over _head toLower $ name))
  docItemPos = entrypointKindPos @ep
  docItemSectionName = Just $ entrypointKindSectionName @ep
  docItemSectionDescription = entrypointKindSectionDescription @ep
  docItemToMarkdown = diEntrypointToMarkdown
  docItemToToc lvl d@(DEntrypoint name _) =
    mdTocFromRef lvl (build . over _head toLower $ name) d

-- | Mark code as part of entrypoint with given name.
--
-- This is automatically called at most of the appropriate situations, like
-- 'entryCase' calls.
entrypointSection
  :: EntrypointKindHasDoc kind
  => Text -> Proxy kind -> (i :-> o) -> (i :-> o)
entrypointSection name (_ :: Proxy kind) =
  docGroup (DEntrypoint @kind name)

-- | Default value for 'DEntrypoint' type argument.
data PlainEntrypointsKind

instance EntrypointKindHasDoc PlainEntrypointsKind where
  entrypointKindPos = 1000
  entrypointKindSectionName = "Entrypoints"

-- | Special entrypoint kind that flattens one level of recursive entrypoints.
--
-- With 'EpdRecursive', intermediary nodes are hidden from documentation.
--
-- With 'EpdDelegate', intermediary nodes will still be shown.
--
-- Any entrypoints can be omitted from docs by listing those in the type
-- parameter (which is especially helpful with 'EpdDelegate').
--
-- For other entrypoint derivation strategies (e.g. 'EpdPlain'), behaves like
-- 'PlainEntrypointsKind' (with the exception of hiding entrypoints from docs)
--
-- If you have several levels of recursion, each level will need to have this
-- kind.
--
-- Note that list of entrypoints to be hidden is not checked by default. Use
-- 'entryCaseFlattenedHiding' to have a static check that entrypoints to be
-- hidden do indeed exist.
data FlattenedEntrypointsKindHiding (hiddenEntrypoints :: [Symbol])

-- | A convenience type synonym for 'FlattenedEntrypointsKindHiding' not hiding
-- any entrypoitns.
type FlattenedEntrypointsKind = FlattenedEntrypointsKindHiding '[]

instance Typeable heps => EntrypointKindHasDoc (FlattenedEntrypointsKindHiding heps) where
  type EntrypointKindOverride (FlattenedEntrypointsKindHiding heps) = PlainEntrypointsKind
  entrypointKindOverrideSpecified = Dict

-- | Describes the behaviour common for all entrypoints.
--
-- For instance, if your contract runs some checks before calling any
-- entrypoint, you probably want to wrap those checks into
-- @entrypointSection "Prior checks" (Proxy \@CommonContractBehaviourKind)@.
data CommonContractBehaviourKind

instance EntrypointKindHasDoc CommonContractBehaviourKind where
  entrypointKindPos = 1800
  entrypointKindSectionName = "Common for all contract's entrypoints"

-- | Describes the behaviour common for entrypoints of given kind.
--
-- This has very special use cases, like contracts with mix of upgradeable
-- and permanent entrypoints.
data CommonEntrypointsBehaviourKind kind

instance EntrypointKindHasDoc kind =>
         EntrypointKindHasDoc (CommonEntrypointsBehaviourKind kind) where
  entrypointKindPos = entrypointKindPos @kind + 5
  entrypointKindSectionName =
    "Common for " <> entrypointKindSectionName @kind
  entrypointKindSectionDescription = Just $
    let refToBase = docItemSectionRef @(DEntrypoint kind)
                 ?: error "Unexpectedly cannot reference section with entrypoints"
    in "Logic common for all entrypoints in " <> refToBase <> " section."

-- | Inserts a reference to an existing entrypoint.
--
-- This helps to avoid duplication in the generated documentation, in order not
-- to overwhelm the reader.
data DEntrypointReference = DEntrypointReference Text Anchor

instance DocItem DEntrypointReference where
  docItemPos = 13
  docItemSectionName = Nothing
  docItemToMarkdown _ (DEntrypointReference name anchor) =
    "Copies behaviour of " <>
    mdLocalRef (mdTicked $ build name) anchor <>
    " entrypoint."

-- | When describing the way of parameter construction - piece of incremental
-- builder for this description.
newtype ParamBuilder = ParamBuilder
  { unParamBuilder :: Markdown -> Markdown
    -- ^ Argument stands for previously constructed parameter piece, and
    -- returned value - a piece constructed after our step.
  }

-- | Show what given 'ParamBuilder' does on a sample.
pbSample :: ParamBuilder -> Markdown
pbSample (ParamBuilder b) = b "·"

instance Buildable ParamBuilder where
  build = pbSample

instance Eq ParamBuilder where
  (==) = (==) `on` pbSample

data ParamBuildingDesc = ParamBuildingDesc
  { pbdEnglish :: Markdown
    -- ^ Plain english description of this step.
  , pbdHaskell :: ParamBuilder
    -- ^ How to construct parameter in Haskell code.
  , pbdMichelson :: ParamBuilder
    -- ^ How to construct parameter working on raw Michelson.
  } deriving stock (Eq)

-- | Describes a parameter building step.
--
-- This can be wrapping into (Haskell) constructor, or a more complex
-- transformation.
data ParamBuildingStep
    -- | Wraps something into constructor with given name.
    -- Constructor should be the one which corresponds to an entrypoint
    -- defined via field annotation, for more complex cases use 'PbsCustom'.
  = PbsWrapIn Text ParamBuildingDesc
    -- | Directly call an entrypoint marked with a field annotation.
  | PbsCallEntrypoint EpName
    -- | Other action.
  | PbsCustom ParamBuildingDesc
    -- | This entrypoint cannot be called, which is possible when an explicit
    -- default entrypoint is present. This is not a true entrypoint but just some
    -- intermediate node in @or@ tree and neither it nor any of its parents
    -- are marked with a field annotation.
    --
    -- It contains dummy 'ParamBuildingStep's which were assigned before
    -- entrypoints were taken into account.
  | PbsUncallable [ParamBuildingStep]
  deriving stock (Eq)

instance Buildable ParamBuildingStep where
  build = \case
    PbsWrapIn ctor _desc -> "Wrap in `" <> build ctor <> "`"
    PbsCallEntrypoint ep -> "Call entrypoint " <> build ep
    PbsCustom desc -> "Custom: \"" <> pbdEnglish desc <> "\""
    PbsUncallable steps -> "Uncallable; dummy steps: " <> listF steps

-- | Make a 'ParamBuildingStep' that tells about wrapping an argument into
-- a constructor with given name and uses given 'ParamBuilder' as description of
-- Michelson part.
mkPbsWrapIn :: Text -> ParamBuilder -> ParamBuildingStep
mkPbsWrapIn ctorName michDesc =
  PbsWrapIn ctorName ParamBuildingDesc
    { pbdEnglish = "Wrap into " <> mdTicked (build ctorName) <> " constructor."
    , pbdHaskell = ParamBuilder $ \p -> build ctorName <> " (" <> p <> ")"
    , pbdMichelson = michDesc
    }

-- | Entrypoint argument type in typed representation.
data SomeEntrypointArg =
  forall a. (NiceParameter a, TypeHasDoc a) => SomeEntrypointArg (Proxy a)

-- | Describes argument of an entrypoint.
data DEntrypointArg =
  DEntrypointArg
  { epaArg :: Maybe SomeEntrypointArg
    -- ^ Argument of the entrypoint. Pass 'Nothing' if no argument is required.
  , epaBuilding :: [ParamBuildingStep]
    -- ^ Describes a way to lift an entrypoint argument into full parameter
    -- which can be passed to the contract.
    --
    -- Steps are supposed to be applied in the order opposite to one in which
    -- they are given.
    -- E.g. suppose that an entrypoint is called as @Run (Service1 arg)@;
    -- then the first step (actual last) should describe wrapping into @Run@
    -- constructor, and the second step (actual first) should be about wrapping
    -- into @Service1@ constructor.
  }

emptyDEpArg :: DEntrypointArg
emptyDEpArg = DEntrypointArg
  { epaArg = Nothing
  , epaBuilding = []
  }

mkDEpUType :: forall t. HasAnnotation t => Untyped.Ty
mkDEpUType = mkUType (getAnnotation @t FollowEntrypoint)

mkDEntrypointArgSimple :: forall t. (NiceParameter t, TypeHasDoc t) => DEntrypointArg
mkDEntrypointArgSimple = DEntrypointArg
  { epaArg = Just $ SomeEntrypointArg (Proxy @t)
  , epaBuilding = []
  }

-- | Go over contract code and update every occurrence of 'DEntrypointArg'
-- documentation item, modifying param building steps.
modifyParamBuildingSteps
  :: ([ParamBuildingStep] -> [ParamBuildingStep])
  -> (inp :-> out)
  -> (inp :-> out)
modifyParamBuildingSteps f =
  modifyDoc (\di -> Just di{ epaBuilding = f (epaBuilding di) })

-- | Go over contract code and update every occurrence of 'DEntrypointArg'
-- documentation item, adding the given step to its "how to build parameter"
-- description.
clarifyParamBuildingSteps :: ParamBuildingStep -> (inp :-> out) -> (inp :-> out)
clarifyParamBuildingSteps pbs =
  modifyParamBuildingSteps (pbs :)

instance DocItem DEntrypointArg where
  docItemPos = 20
  docItemSectionName = Nothing
  docItemDependencies (DEntrypointArg mdty _) =
    [ SomeDocDefinitionItem (DType $ Proxy @ty)
    | Just (SomeEntrypointArg (_ :: Proxy ty)) <- pure mdty ]
  docItemToMarkdown _ (DEntrypointArg mdty psteps) =
    mconcat . Prelude.map (<> "\n\n") $
      [ mdSubsection "Argument" $
          case mdty of
            Nothing -> "none (pass unit)"
            Just (SomeEntrypointArg (dty :: Proxy ep)) -> mconcat . Prelude.intersperse "\n" $
              [ mempty
              , "  + " <>
                mdSubsection "In Haskell"
                  (typeDocMdReference dty (WithinParens False))
              , "  + " <>
                mdSubsection "In Michelson"
                  (mdTicked $ printDocB False . renderDoc needsParens $
                     T.untypeDemoteT @(T.ToT ep))
              , fromMaybe "" $ sampleTypedValue (sing @(ToT ep)) <&> \sampleVal ->
                "    + " <>
                mdSubsection "Example"
                  (mdAddId "example-id"
                    $ mdTicked
                    $ build $ printTypedValue True sampleVal
                  )
              ],
          mdSpoiler "How to call this entrypoint" $
            "\n0. Construct an argument for the entrypoint.\n" <>
            howToCall
      ]
    where
      howToCall =
        mconcat . Prelude.intersperse "\n" $
        -- Markdown re-enumerates enumerated lists automatically
        Prelude.map ("1. " <>) $
          reverse psteps <&> \case
            PbsWrapIn _ pbd ->
              renderPbDesc pbd
            PbsCallEntrypoint ep -> case ep of
              DefEpName ->
                "Call the contract (default entrypoint) with the constructed \
                \argument."
              _ ->
                "Call contract's " <> mdTicked (build ep) <> " entrypoint \
                \passing the constructed argument."
            PbsCustom pbd ->
              renderPbDesc pbd
            PbsUncallable _ ->
              "Feel sad: this entrypoint *cannot* be called and is enlisted \
              \here only to describe the parameter structure."
              -- We could hide such entrypoints, but then in case of incorrect
              -- use of 'entryCase's or a bug in documentation, understanding
              -- what's going on would be hard

      renderPbDesc ParamBuildingDesc{..} =
        mconcat . Prelude.intersperse "\n" $
        [ pbdEnglish
        , "    + " <>
          mdSubsection "In Haskell" (mdTicked $ pbSample pbdHaskell)
        , "    + " <>
          mdSubsection "In Michelson" (mdTicked $ pbSample pbdMichelson)
        ]

-- | Pick a type documentation from 'CtorField'.
class (KnownSymbol con) => DeriveCtorFieldDoc con (cf :: CtorField) where
  deriveCtorFieldDoc :: DEntrypointArg

instance
    (KnownSymbol con)
  =>
    DeriveCtorFieldDoc con 'NoFields
  where
  deriveCtorFieldDoc = emptyDEpArg

instance
    (NiceParameter ty, TypeHasDoc ty, KnownValue ty, KnownSymbol con)
  =>
    DeriveCtorFieldDoc con ('OneField ty)
  where
  deriveCtorFieldDoc = mkDEntrypointArgSimple @ty

-- | Add necessary documentation to entry points.
documentEntrypoints
  :: forall a kind inp out.
     DocumentEntrypoints kind a
  => Rec (CaseClauseL inp out) (CaseClauses a)
  -> Rec (CaseClauseL inp out) (CaseClauses a)
documentEntrypoints =
  gDocumentEntrypoints @(BuildEPTree' a) @kind @(G.Rep a) $
    ParamBuilder id

-- | Constraint for 'documentEntrypoints'.
type DocumentEntrypoints kind a =
  (Generic a, GDocumentEntrypoints (BuildEPTree' a) kind (G.Rep a))

type BuildEPTree' a = BuildEPTree (GetParameterEpDerivation a) a

-- | Traverse entry points and add parameter building step (which describes
-- necessity to wrap parameter into some constructor of the given datatype)
-- to all parameters described within given code.
class GDocumentEntrypoints (ept :: EPTree) (kind :: Type) (x :: Type -> Type) where
  -- | Add corresponding parameter building step.
  --
  -- First argument is accumulator for Michelson description of the building step.
  gDocumentEntrypoints
    :: ParamBuilder
    -> Rec (CaseClauseL inp out) (GCaseClauses x)
    -> Rec (CaseClauseL inp out) (GCaseClauses x)

instance GDocumentEntrypoints ept kind x => GDocumentEntrypoints ept kind (G.D1 i x) where
  gDocumentEntrypoints = gDocumentEntrypoints @ept @kind @x

instance ( GDocumentEntrypoints eptl kind x, GDocumentEntrypoints eptr kind y
         , RSplit (GCaseClauses x) (GCaseClauses y)
         ) =>
         GDocumentEntrypoints ('EPNode eptl eptr) kind (x :+: y) where
  gDocumentEntrypoints (ParamBuilder michDesc) clauses =
    let (lclauses, rclauses) = rsplit @CaseClauseParam @(GCaseClauses x) clauses
    in gDocumentEntrypoints @eptl @kind @x
         (ParamBuilder $ \a -> michDesc $ "Left (" <> a <> ")")
         lclauses
       `rappend`
       gDocumentEntrypoints @eptr @kind @y
         (ParamBuilder $ \a -> michDesc $ "Right (" <> a <> ")")
         rclauses

instance {-# OVERLAPPABLE #-}
         ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
         , KnownSymbol ctor
         , DocItem (DEntrypoint (EntrypointKindOverride kind))
         , DeriveCtorFieldDoc ctor cf
         ) =>
         GDocumentEntrypoints ept kind (G.C1 ('G.MetaCons ctor _1 _2) x) where
  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
    let entrypointName = toText $ symbolVal (Proxy @ctor)
        psteps = mkPbsWrapIn entrypointName michDesc
        addDoc instr =
          clarifyParamBuildingSteps psteps $
          docGroup (DEntrypoint @(EntrypointKindOverride kind) entrypointName) $
          doc (deriveCtorFieldDoc @ctor @cf) # instr
    in CaseClauseL (addDoc clause) :& RNil

instance ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
         , KnownSymbol ctor
         ) =>
         GDocumentEntrypoints ('EPNode a b) (FlattenedEntrypointsKindHiding _heps)
            (G.C1 ('G.MetaCons ctor _1 _2) x) where
  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
    let entrypointName = toText $ symbolVal (Proxy @ctor)
        psteps = mkPbsWrapIn entrypointName michDesc
    in CaseClauseL (clarifyParamBuildingSteps psteps clause) :& RNil

instance {-# OVERLAPPABLE #-}
         ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
         , KnownSymbol ctor
         , DeriveCtorFieldDoc ctor cf
         , T.SingI heps
         ) =>
         GDocumentEntrypoints ept (FlattenedEntrypointsKindHiding heps)
            (G.C1 ('G.MetaCons ctor _1 _2) x) where
  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
    let epName = toText $ symbolVal (Proxy @ctor)
        psteps = mkPbsWrapIn epName michDesc
        hiddenEps = fromSing $ T.sing @heps
        epDoc instr
          | epName `elem` hiddenEps = instr
          | otherwise =
              docGroup (DEntrypoint @PlainEntrypointsKind epName)
                (doc (deriveCtorFieldDoc @ctor @cf))
              # instr
        addDoc instr =
          clarifyParamBuildingSteps psteps $
            epDoc instr
    in CaseClauseL (addDoc clause) :& RNil

-- | Like 'case_', to be used for pattern-matching on a parameter
-- or its part.
--
-- Modifies documentation accordingly. Including description of
-- entrypoints' arguments, thus for them you will need to supply
-- 'TypeHasDoc' instance.
entryCase_
  :: forall dt entrypointKind out inp.
     ( InstrCaseC dt
     , RMap (CaseClauses dt)
     , DocumentEntrypoints entrypointKind dt
     )
  => Proxy entrypointKind
  -> Rec (CaseClauseL inp out) (CaseClauses dt)
  -> dt : inp :-> out
entryCase_ _ = case_ . documentEntrypoints @dt @entrypointKind

-- | Version of 'entryCase_' for tuples.
entryCase
  :: forall dt entrypointKind out inp clauses.
     ( CaseTC dt out inp clauses
     , DocumentEntrypoints entrypointKind dt
     )
  => Proxy entrypointKind -> IsoRecTuple clauses -> dt : inp :-> out
entryCase p = entryCase_ p . recFromTuple

-- | Wrapper for documenting single entrypoint which parameter
-- isn't going to be unwrapped from some datatype.
--
-- @entryCase@ unwraps a datatype, however, sometimes we want to
-- have entrypoint parameter to be not wrapped into some datatype.
documentEntrypoint
  :: forall kind epName param s out.
     ( KnownSymbol epName
     , DocItem (DEntrypoint kind)
     , NiceParameter param
     , TypeHasDoc param
     )
  => param : s :-> out -> param : s :-> out
documentEntrypoint instr =
  let entrypointName = toText $ symbolVal (Proxy @epName) in
    docGroup (DEntrypoint @kind entrypointName) $
    doc (mkDEntrypointArgSimple @param) # instr

-- | Provides arror for convenient entrypoint documentation
class EntryArrow kind name body where
  -- | Lift entrypoint implementation.
  --
  -- Entrypoint names should go with "e" prefix.
  (#->) :: (Label name, Proxy kind) -> body -> body

instance ( name ~ ("e" `AppendSymbol` epName)
         , body ~ (param : s :-> out)
         , KnownSymbol epName
         , DocItem (DEntrypoint kind)
         , NiceParameter param
         , TypeHasDoc param
         , KnownValue param
         ) => EntryArrow kind name body where
  (#->) _ = documentEntrypoint @kind @epName

-- | Modify param building steps with respect to entrypoints that given
-- parameter declares.
--
-- Each contract with entrypoints should eventually call this function,
-- otherwise, in case if contract uses built-in entrypoints feature,
-- the resulting parameter building steps in the generated documentation
-- will not consider entrypoints and thus may be incorrect.
--
-- Calling this twice over the same code is also prohibited.
--
-- This method is for internal use, if you want to apply it to a contract
-- manually, use 'finalizeParamCallingDoc'.
finalizeParamCallingDoc'
  :: forall cp inp out.
     (NiceParameterFull cp, HasCallStack)
  => Proxy cp -> (inp :-> out) -> (inp :-> out)
finalizeParamCallingDoc' _ = modifyParamBuildingSteps modifySteps
  where
    epDescs :: [Some1 EpCallingDesc]
    epDescs =
      -- Reversing the list because if element @e1@ of this list is prefix of
      -- another element @e2@, we want @e2@ to appear eariler than @e1@ to
      -- match against it first. But without reverse exactly the opposite
      -- holds due to [order of entrypoints children] property.
      reverse $ pepDescsWithDef @cp

    modifySteps :: [ParamBuildingStep] -> [ParamBuildingStep]
    modifySteps pbs
      | areFinalizedParamBuildingSteps pbs =
          error "Applying finalization second time"
      | otherwise =
          fromMaybe [PbsUncallable pbs] . listToMaybe . catMaybes $
          epDescs <&> \epDesc -> tryShortcut epDesc pbs

    -- Further we check whether given 'EpCallingStep's form prefix of
    -- 'ParamBuildingStep's; if so, we can apply only part of building
    -- steps and then call the entrypoint directly

    match :: [EpCallingStep] -> [ParamBuildingStep] -> Bool
    match cSteps pbSteps =
      and $ zip cSteps (prolong pbSteps) <&> \case
        (EpsWrapIn ctor, Just (PbsWrapIn ctor2 _)) | ctor == ctor2 -> True
        _ -> False
      where
        prolong :: [a] -> [Maybe a]
        prolong l = map Just l ++ repeat Nothing

    tryShortcut
      :: Some1 EpCallingDesc
      -> [ParamBuildingStep]
      -> Maybe [ParamBuildingStep]
    tryShortcut (Some1 EpCallingDesc{ epcdSteps = cSteps, epcdEntrypoint = ep })
                pbSteps
      | match cSteps pbSteps =
          let truncated = drop (length cSteps) pbSteps
              callEpStep = PbsCallEntrypoint ep
          in Just $ callEpStep : truncated
      | otherwise = Nothing

-- | Version of 'finalizeParamCallingDoc\'' more convenient for manual call in
-- a contract.
finalizeParamCallingDoc
  :: forall cp inp out.
     (NiceParameterFull cp, RequireSumType cp, HasCallStack)
  => (cp : inp :-> out) -> (cp : inp :-> out)
finalizeParamCallingDoc = finalizeParamCallingDoc' (Proxy @cp)
  where
    -- We do not actually need it, requiring this constraint only to avoid
    -- misapplication of our function.
    _needSumType :: Dict (RequireSumType cp)
    _needSumType = Dict

-- | Whether 'finalizeParamCallingDoc' has already been applied to these steps.
areFinalizedParamBuildingSteps :: [ParamBuildingStep] -> Bool
areFinalizedParamBuildingSteps =
  -- Currently, 'finalizeParamCallingDoc' puts either 'PbsCallEntrypoint' or
  -- 'PbsUncallable' to list, and only it, and we rely on this behaviour here.
  -- If something changes so that these heuristics do not work, we can always
  -- insert special markers which would tell us whether finalization has been
  -- applied.
  let
    hasFinalizationTraces = \case
      PbsWrapIn{} -> False
      PbsCallEntrypoint{} -> True
      PbsCustom{} -> False
      PbsUncallable{} -> True
  in any hasFinalizationTraces

-- | Version of 'entryCase_' for contracts with flat parameter.
entryCaseSimple_
  :: forall cp out inp.
     ( InstrCaseC cp
     , RMap (CaseClauses cp)
     , DocumentEntrypoints PlainEntrypointsKind cp
     , RequireFlatParamEps cp
     )
  => Rec (CaseClauseL inp out) (CaseClauses cp)
  -> cp : inp :-> out
entryCaseSimple_ =
  entryCase_ (Proxy @PlainEntrypointsKind)
  where
    _reqFlat = Dict @(RequireFlatEpDerivation cp (GetParameterEpDerivation cp))

-- | Version of 'entryCase' for contracts with flat parameter.
entryCaseSimple
  :: forall cp out inp clauses.
     ( CaseTC cp out inp clauses
     , DocumentEntrypoints PlainEntrypointsKind cp
     , RequireFlatParamEps cp
     )
  => IsoRecTuple clauses -> cp : inp :-> out
entryCaseSimple = entryCaseSimple_ . recFromTuple

-- | Version of 'entryCase_' for contracts with recursive parameter that needs
-- to be flattened. Use it with 'EpdRecursive' when you don't need intermediary
-- nodes in autodoc.
entryCaseFlattened_
  :: forall cp out inp.
     ( InstrCaseC cp
     , RMap (CaseClauses cp)
     , DocumentEntrypoints FlattenedEntrypointsKind cp
     )
  => Rec (CaseClauseL inp out) (CaseClauses cp)
  -> cp : inp :-> out
entryCaseFlattened_ =
  entryCase_ (Proxy @FlattenedEntrypointsKind)

-- | Version of 'entryCase' for contracts with recursive parameter that needs
-- to be flattened. Use it with 'EpdRecursive' when you don't need intermediary
-- nodes in autodoc.
entryCaseFlattened
  :: forall cp out inp clauses.
     ( CaseTC cp out inp clauses
     , DocumentEntrypoints FlattenedEntrypointsKind cp
     )
  => IsoRecTuple clauses -> cp : inp :-> out
entryCaseFlattened = entryCaseFlattened_ . recFromTuple

-- | Version of 'entryCase_' for contracts with recursive delegate parameter that needs
-- to be flattened. Use it with 'EpdDelegate' when you don't need hierarchical
-- entrypoints in autodoc. You can also hide particular entrypoints with the
-- type parameter. Consider using 'entryCaseFlattened_' if you don't want
-- to hide any entrypoints.
entryCaseFlattenedHiding_
  :: forall heps cp out inp.
     ( InstrCaseC cp
     , RMap (CaseClauses cp)
     , DocumentEntrypoints (FlattenedEntrypointsKindHiding heps) cp
     , HasEntrypoints (ParameterEntrypointsDerivation cp) cp heps
     )
  => Rec (CaseClauseL inp out) (CaseClauses cp)
  -> cp : inp :-> out
entryCaseFlattenedHiding_ =
  entryCase_ (Proxy @(FlattenedEntrypointsKindHiding heps))
  where
    _reqHasEps = Dict @(HasEntrypoints (ParameterEntrypointsDerivation cp) cp heps)

-- | Version of 'entryCase' for contracts with recursive delegate parameter that needs
-- to be flattened. Use it with 'EpdDelegate' when you don't need hierarchical
-- entrypoints in autodoc. You can also hide particular entrypoints with the
-- first type parameter. Consider using 'entryCaseFlattened' if you don't want
-- to hide any entrypoints.
--
-- @
--  entryCaseFlattenedHiding @'["Ep1", "Ep2"] ...
-- @
entryCaseFlattenedHiding
  :: forall heps cp out inp clauses.
     ( CaseTC cp out inp clauses
     , DocumentEntrypoints (FlattenedEntrypointsKindHiding heps) cp
     , HasEntrypoints (ParameterEntrypointsDerivation cp) cp heps
     )
  => IsoRecTuple clauses -> cp : inp :-> out
entryCaseFlattenedHiding = entryCaseFlattenedHiding_ @heps . recFromTuple

type family RequireFlatParamEps cp :: Constraint where
  RequireFlatParamEps cp =
    ( NiceParameterFull cp
    , RequireFlatEpDerivation cp (GetParameterEpDerivation cp)
    , RequireSumType cp
    )

-- Checking this is not strictly necessary, but let's try it
type family RequireFlatEpDerivation cp deriv :: Constraint where
  RequireFlatEpDerivation _ EpdNone = ()
  RequireFlatEpDerivation _ EpdPlain = ()
  RequireFlatEpDerivation cp deriv = TypeError
    ( 'Text "Parameter is not flat" ':$$:
      'Text "For parameter `" ':<>: 'ShowType cp ':<>: 'Text "`" ':$$:
      'Text "With entrypoints derivation way `" ':<>: 'ShowType deriv ':<>: 'Text "`"
    )

type family HasEntrypoints mode cp syms :: Constraint where
  HasEntrypoints mode cp (x ': xs) =
    FailUnlessElse (IsJust @@ (EpdLookupEntrypoint mode cp @@ x))
       ('Text "Parameter type " ':<>: 'ShowType cp
        ':<>: 'Text " does not contain entrypoint " ':<>: 'ShowType x)
       (HasEntrypoints mode cp xs)
  HasEntrypoints _ _ '[] = ()

---------------------------
-- Helper
---------------------------

-- | Surrouned a markdown text in a span tag with given id.
mdAddId :: Markdown -> Markdown -> Markdown
mdAddId idTxt txt = "<span id=\"" <> idTxt <> "\">" <> txt <> "</span>"