-- 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 :: forall t (c :: InstrClass) (inp :: [T]) (out :: [T]).
(SingI c, ClassifyInstr t) =>
ClassifiedInstr c inp out -> Sing (GetClassified c)
getInstrClass ClassifiedInstr c inp out
_ = SingInstrClass c -> Sing (GetClassified c)
forall k (c :: InstrClass).
ClassifyInstr k =>
SingInstrClass c -> Sing (GetClassified c)
getClassified (forall {k} (a :: k). SingI a => Sing a
forall (a :: InstrClass). SingI a => Sing a
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