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

{-# OPTIONS_HADDOCK not-home #-}

-- | TH code for generating classification boilerplate.
module Morley.Michelson.Typed.ClassifiedInstr.Internal.TH
  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.TH
  ) where

import Prelude hiding (Type, lift)
import Prelude qualified

import Data.Constraint (Dict(..))
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (Lift(..))

import Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.HasAnns
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsAlwaysFailing
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsMichelson
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.NumChildren
import Morley.Michelson.Typed.ClassifiedInstr.Internal.InstrEnum
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types
import Morley.Michelson.Typed.Instr (Instr)
import Morley.Michelson.Typed.T

{-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-}

-- | Generate @ClassifiedInstr@ from @Instr@.
generateClassifiedInstr :: DecsQ
generateClassifiedInstr = do
  TyConI (DataD _ _ _ _ cons _) <- reify ''Instr
  [DataD cxt' name tvb mk _ ders] <-
    [d|data ClassifiedInstr :: InstrClass -> [T] -> [T] -> Prelude.Type|]
  let substOne :: Con -> Q Con
      substOne = \case
        GadtC [nm] args res -> GadtC [mkName $ "C_" <> nameBase nm] args <$> mangleRes nm args res
        ForallC vars cxt'' con -> ForallC vars cxt'' <$> substOne con
        c -> error $ "unsupported " <> show (ppr c)
      mangleRes nm args = \case
        (ConT cn `AppT` inp `AppT` out) | cn == ''Instr ->
          [t|$(conT $ mkName "ClassifiedInstr") $cls $(pure inp) $(pure out)|]
          where cls = classifyInstrTH nm (snd <$> args)
        t -> error $ "unexpected Instr return type " <> show (ppr t)

  cons'' <- mapM substOne cons
  pure [DataD cxt' name tvb mk cons'' ders]

-- | Convert a 'Enum' constructor to a TemplateHaskell type quote with the
-- corresponding promoted datakind constructor.
promote :: forall a. (Enum a, Lift a) => a -> TypeQ
promote = lift >=> \case
  ConE nm -> promotedT nm
  _ -> error "impossible because it's a enum"
  where _ = Dict @(Enum a) -- silence redundant constraint warning

-- | Based on instruction constructor name and types of its arguments, generate
-- its classification.
classifyInstrTH :: Name -> [Type] -> TypeQ
classifyInstrTH nm args = [t|'InstrClass $numc $ft $mich $anns|]
  where
    numc = promote $ numChildren args
    ft   = promote $ isAlwaysFailing someEnum
    mich = promote $ isMichelson someEnum
    anns = promote $ hasAnns someEnum
    someEnum = fromName nm

-- | Generate the function converting from 'Instr' to @WellClassifiedInstr@ existential.
generateInstrToWCI :: Name -> DecsQ
generateInstrToWCI wellClassifiedInstrName = do
  TyConI (DataD _ _ _ _ cons _) <- reify ''Instr
  let expr = lamCaseE $ go <$> cons
      go = \case
        GadtC [nm] args _ -> do
          names <- mapM (\_ -> newName "x") args
          let pat = conP nm varsP
              varsP = varP <$> names
              varsE = varE <$> names
              con = foldl' appE (conE $ mkName $ "C_" <> nameBase nm) varsE
          match pat (normalB [|WCI $ $con|]) []
        ForallC _ _ con -> go con
        c -> error $ "unsupported " <> show (ppr c)
      wellClassifiedInstr = conT wellClassifiedInstrName
  [d|
    classifyInstr :: Instr inp out -> $wellClassifiedInstr inp out
    classifyInstr = $expr
    |]