-- 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 :: DecsQ
generateClassifiedInstr = do
  TyConI (DataD Cxt
_ Name
_ [TyVarBndr ()]
_ Maybe Kind
_ [Con]
cons [DerivClause]
_) <- Name -> Q Info
reify ''Instr
  [DataD Cxt
cxt' Name
name [TyVarBndr ()]
tvb Maybe Kind
mk [Con]
_ [DerivClause]
ders] <-
    [d|data ClassifiedInstr :: InstrClass -> [T] -> [T] -> Prelude.Type|]
  let substOne :: Con -> Q Con
      substOne :: Con -> Q Con
substOne = \case
        GadtC [Name
nm] [BangType]
args Kind
res -> [Name] -> [BangType] -> Kind -> Con
GadtC [String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"C_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
nameBase Name
nm] [BangType]
args (Kind -> Con) -> Q Kind -> Q Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [BangType] -> Kind -> Q Kind
forall {a}. Name -> [(a, Kind)] -> Kind -> Q Kind
mangleRes Name
nm [BangType]
args Kind
res
        ForallC [TyVarBndr Specificity]
vars Cxt
cxt'' Con
con -> [TyVarBndr Specificity] -> Cxt -> Con -> Con
ForallC [TyVarBndr Specificity]
vars Cxt
cxt'' (Con -> Con) -> Q Con -> Q Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Con -> Q Con
substOne Con
con
        Con
c -> Text -> Q Con
forall a. HasCallStack => Text -> a
error (Text -> Q Con) -> Text -> Q Con
forall a b. (a -> b) -> a -> b
$ Text
"unsupported " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Doc -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Con -> Doc
forall a. Ppr a => a -> Doc
ppr Con
c)
      mangleRes :: Name -> [(a, Kind)] -> Kind -> Q Kind
mangleRes Name
nm [(a, Kind)]
args = \case
        (ConT Name
cn `AppT` Kind
inp `AppT` Kind
out) | Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== ''Instr ->
          [t|$(Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT (Name -> Q Kind) -> Name -> Q Kind
forall a b. (a -> b) -> a -> b
$ String -> Name
mkName String
"ClassifiedInstr") $Q Kind
cls $(Kind -> Q Kind
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
inp) $(Kind -> Q Kind
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Kind
out)|]
          where cls :: Q Kind
cls = Name -> Cxt -> Q Kind
classifyInstrTH Name
nm ((a, Kind) -> Kind
forall a b. (a, b) -> b
snd ((a, Kind) -> Kind) -> [(a, Kind)] -> Cxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Kind)]
args)
        Kind
t -> Text -> Q Kind
forall a. HasCallStack => Text -> a
error (Text -> Q Kind) -> Text -> Q Kind
forall a b. (a -> b) -> a -> b
$ Text
"unexpected Instr return type " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Doc -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Kind -> Doc
forall a. Ppr a => a -> Doc
ppr Kind
t)

  [Con]
cons'' <- (Con -> Q Con) -> [Con] -> Q [Con]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Con -> Q Con
substOne [Con]
cons
  pure [Cxt
-> Name
-> [TyVarBndr ()]
-> Maybe Kind
-> [Con]
-> [DerivClause]
-> Dec
DataD Cxt
cxt' Name
name [TyVarBndr ()]
tvb Maybe Kind
mk [Con]
cons'' [DerivClause]
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 :: forall a. (Enum a, Lift a) => a -> Q Kind
promote = a -> Q Exp
forall t (m :: * -> *). (Lift t, Quote m) => t -> m Exp
forall (m :: * -> *). Quote m => a -> m Exp
lift (a -> Q Exp) -> (Exp -> Q Kind) -> a -> Q Kind
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case
  ConE Name
nm -> Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
promotedT Name
nm
  Exp
_ -> Text -> Q Kind
forall a. HasCallStack => Text -> a
error Text
"impossible because it's a enum"
  where Dict (Enum a)
_ = forall (a :: Constraint). a => Dict a
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 :: Name -> Cxt -> Q Kind
classifyInstrTH Name
nm Cxt
args = [t|'InstrClass $Q Kind
numc $Q Kind
ft $Q Kind
mich $Q Kind
anns|]
  where
    numc :: Q Kind
numc = NumChildren -> Q Kind
forall a. (Enum a, Lift a) => a -> Q Kind
promote (NumChildren -> Q Kind) -> NumChildren -> Q Kind
forall a b. (a -> b) -> a -> b
$ Cxt -> NumChildren
numChildren Cxt
args
    ft :: Q Kind
ft   = FailureType -> Q Kind
forall a. (Enum a, Lift a) => a -> Q Kind
promote (FailureType -> Q Kind) -> FailureType -> Q Kind
forall a b. (a -> b) -> a -> b
$ InstrEnum -> FailureType
isAlwaysFailing InstrEnum
someEnum
    mich :: Q Kind
mich = IsMichelson -> Q Kind
forall a. (Enum a, Lift a) => a -> Q Kind
promote (IsMichelson -> Q Kind) -> IsMichelson -> Q Kind
forall a b. (a -> b) -> a -> b
$ InstrEnum -> IsMichelson
isMichelson InstrEnum
someEnum
    anns :: Q Kind
anns = HasAnns -> Q Kind
forall a. (Enum a, Lift a) => a -> Q Kind
promote (HasAnns -> Q Kind) -> HasAnns -> Q Kind
forall a b. (a -> b) -> a -> b
$ InstrEnum -> HasAnns
hasAnns InstrEnum
someEnum
    someEnum :: InstrEnum
someEnum = Name -> InstrEnum
fromName Name
nm

-- | Generate the function converting from 'Instr' to @WellClassifiedInstr@ existential.
generateInstrToWCI :: Name -> DecsQ
generateInstrToWCI :: Name -> DecsQ
generateInstrToWCI Name
wellClassifiedInstrName = do
  TyConI (DataD Cxt
_ Name
_ [TyVarBndr ()]
_ Maybe Kind
_ [Con]
cons [DerivClause]
_) <- Name -> Q Info
reify ''Instr
  let expr :: Q Exp
expr = [Q Match] -> Q Exp
forall (m :: * -> *). Quote m => [m Match] -> m Exp
lamCaseE ([Q Match] -> Q Exp) -> [Q Match] -> Q Exp
forall a b. (a -> b) -> a -> b
$ Con -> Q Match
go (Con -> Q Match) -> [Con] -> [Q Match]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Con]
cons
      go :: Con -> Q Match
go = \case
        GadtC [Name
nm] [BangType]
args Kind
_ -> do
          [Name]
names <- (BangType -> Q Name) -> [BangType] -> Q [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\BangType
_ -> String -> Q Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"x") [BangType]
args
          let pat :: Q Pat
pat = Name -> [Q Pat] -> Q Pat
forall (m :: * -> *). Quote m => Name -> [m Pat] -> m Pat
conP Name
nm [Q Pat]
varsP
              varsP :: [Q Pat]
varsP = Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
varP (Name -> Q Pat) -> [Name] -> [Q Pat]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
names
              varsE :: [Q Exp]
varsE = Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
varE (Name -> Q Exp) -> [Name] -> [Q Exp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Name]
names
              con :: Q Exp
con = (Q Exp -> Element [Q Exp] -> Q Exp) -> Q Exp -> [Q Exp] -> Q Exp
forall t b. Container t => (b -> Element t -> b) -> b -> t -> b
forall b. (b -> Element [Q Exp] -> b) -> b -> [Q Exp] -> b
foldl' Q Exp -> Q Exp -> Q Exp
Q Exp -> Element [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => m Exp -> m Exp -> m Exp
appE (Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
conE (Name -> Q Exp) -> Name -> Q Exp
forall a b. (a -> b) -> a -> b
$ String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"C_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Name -> String
nameBase Name
nm) [Q Exp]
varsE
          Q Pat -> Q Body -> [Q Dec] -> Q Match
forall (m :: * -> *).
Quote m =>
m Pat -> m Body -> [m Dec] -> m Match
match Q Pat
pat (Q Exp -> Q Body
forall (m :: * -> *). Quote m => m Exp -> m Body
normalB [|WCI $ $Q Exp
con|]) []
        ForallC [TyVarBndr Specificity]
_ Cxt
_ Con
con -> Con -> Q Match
go Con
con
        Con
c -> Text -> Q Match
forall a. HasCallStack => Text -> a
error (Text -> Q Match) -> Text -> Q Match
forall a b. (a -> b) -> a -> b
$ Text
"unsupported " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Doc -> Text
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Con -> Doc
forall a. Ppr a => a -> Doc
ppr Con
c)
      wellClassifiedInstr :: Q Kind
wellClassifiedInstr = Name -> Q Kind
forall (m :: * -> *). Quote m => Name -> m Kind
conT Name
wellClassifiedInstrName
  [d|
    classifyInstr :: Instr inp out -> $Q Kind
wellClassifiedInstr inp out
    classifyInstr = $Q Exp
expr
    |]