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

{-# OPTIONS_HADDOCK not-home #-}
{-# LANGUAGE DeriveLift #-}

-- Required due to 'genSingletonsType' producing those.
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Data kinds plus singletons defining possible classifications for instructions.
module Morley.Michelson.Typed.ClassifiedInstr.Internal.Types
  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.Types
  ) where

import Data.Singletons (Sing)
import Language.Haskell.TH.Syntax (Lift)

import Morley.Util.Sing

-- | Number of children instructions a given instruction constructor has.
data NumChildren
  = MayHaveChildren
    -- ^ It is unknown at compile-time whether the instruction has children or
    -- not.
  | HasIndirectChildren
    -- ^ The instruction has children indirectly, as values.
  | NoChildren
    -- ^ The instruction has no children.
  | OneChild
    -- ^ The instruction has one child.
  | TwoChildren
    -- ^ The instruction has two children.
  deriving stock (Show, Enum, Lift)

-- | Whether an instruction always fails. An example of always-failing
-- instruction is @NEVER@.
data FailureType
  = AlwaysFailing
    -- ^ Instruction always fails.
  | FailingNormal
    -- ^ Instruction might fail if inputs are incorrect, but will generally
    -- work.
  deriving stock (Show, Enum, Lift)

data IsMichelson
  = FromMichelson
    -- ^ There is corresponding instruction in the Michelson spec.
  | Additional
    -- ^ "Extended instructions". Don't affect execution on chain, but may
    -- affect execution on the morley emulator.
  | Phantom
    -- ^ Wrappers that don't affect execution.
  | Structural
    -- ^ Michelson structures that are not instructions, e.g. a nested code block.
  deriving stock (Show, Enum, Lift)

-- | Whether an instruction carries Michelson annotations.
data HasAnns
  = DoesNotHaveAnns
  | DoesHaveStandardAnns
    -- ^ "Standard" means that the first constructor argument contains all
    -- annotations as @Anns@ type, which is true for most annotated
    -- instructions. There are a couple exceptions, however.
  | DoesHaveNonStandardAnns
  deriving stock (Show, Enum, Lift)

-- | A product type of all classifications.
data InstrClass = InstrClass NumChildren FailureType IsMichelson HasAnns

concatMapM genSingletonsType
  [''InstrClass,''NumChildren,''FailureType,''IsMichelson,''HasAnns]

class ClassifyInstr k where
  type GetClassified (c :: InstrClass) :: k
  getClassified :: SingInstrClass c -> Sing (GetClassified c :: k)

instance ClassifyInstr NumChildren where
  type GetClassified ('InstrClass a _ _ _) = a
  getClassified (SInstrClass a _ _ _) = a
instance ClassifyInstr FailureType where
  type GetClassified ('InstrClass _ a _ _) = a
  getClassified (SInstrClass _ a _ _) = a
instance ClassifyInstr IsMichelson where
  type GetClassified ('InstrClass _ _ a _) = a
  getClassified (SInstrClass _ _ a _) = a
instance ClassifyInstr HasAnns where
  type GetClassified ('InstrClass _ _ _ a) = a
  getClassified (SInstrClass _ _ _ a) = a