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

{-# OPTIONS_HADDOCK not-home #-}

-- | Main implementation of the classifier machinery.
module Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl
  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl
  ) where

import Data.Singletons (Sing, SingI(..))

import Morley.Michelson.Typed.ClassifiedInstr.Internal.TH
import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types

-- | Classified instruction. Has the same shape as typed @Instr@, but its type
-- also carries information about the classes of the constructor.
generateClassifiedInstr

{- | Given a well-classified instruction, get a particular classification for
it. The general use pattern is:

@
case 'classifyInstr' i of
  'WCI' instr -> case 'getInstrClass' instr of
    'SMayHaveChildren' -> case instr of
      'C_Ext' _ -> _
      -- ...
    -- ...
@

You should use @withClassifiedInstr@, as it provides a less verbose interface.
-}
getInstrClass
  :: forall t c inp out. (SingI c, ClassifyInstr t)
  => ClassifiedInstr c inp out
  -> Sing (GetClassified c :: t)
getInstrClass _ = getClassified (sing @c)

-- | Existential for 'ClassifiedInstr' hiding the class. Use 'classifyInstr' to
-- get it.
data WellClassifiedInstr inp out =
  forall cls. (SingI cls) =>
  WCI { pickClassifiedInstr :: ClassifiedInstr cls inp out }

-- | Convert typed @Instr@ to 'WellClassifiedInstr'.
generateInstrToWCI ''WellClassifiedInstr