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

{-# OPTIONS_HADDOCK not-home #-}

-- 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 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 (Int -> NumChildren -> ShowS
[NumChildren] -> ShowS
NumChildren -> String
(Int -> NumChildren -> ShowS)
-> (NumChildren -> String)
-> ([NumChildren] -> ShowS)
-> Show NumChildren
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NumChildren] -> ShowS
$cshowList :: [NumChildren] -> ShowS
show :: NumChildren -> String
$cshow :: NumChildren -> String
showsPrec :: Int -> NumChildren -> ShowS
$cshowsPrec :: Int -> NumChildren -> ShowS
Show, Int -> NumChildren
NumChildren -> Int
NumChildren -> [NumChildren]
NumChildren -> NumChildren
NumChildren -> NumChildren -> [NumChildren]
NumChildren -> NumChildren -> NumChildren -> [NumChildren]
(NumChildren -> NumChildren)
-> (NumChildren -> NumChildren)
-> (Int -> NumChildren)
-> (NumChildren -> Int)
-> (NumChildren -> [NumChildren])
-> (NumChildren -> NumChildren -> [NumChildren])
-> (NumChildren -> NumChildren -> [NumChildren])
-> (NumChildren -> NumChildren -> NumChildren -> [NumChildren])
-> Enum NumChildren
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: NumChildren -> NumChildren -> NumChildren -> [NumChildren]
$cenumFromThenTo :: NumChildren -> NumChildren -> NumChildren -> [NumChildren]
enumFromTo :: NumChildren -> NumChildren -> [NumChildren]
$cenumFromTo :: NumChildren -> NumChildren -> [NumChildren]
enumFromThen :: NumChildren -> NumChildren -> [NumChildren]
$cenumFromThen :: NumChildren -> NumChildren -> [NumChildren]
enumFrom :: NumChildren -> [NumChildren]
$cenumFrom :: NumChildren -> [NumChildren]
fromEnum :: NumChildren -> Int
$cfromEnum :: NumChildren -> Int
toEnum :: Int -> NumChildren
$ctoEnum :: Int -> NumChildren
pred :: NumChildren -> NumChildren
$cpred :: NumChildren -> NumChildren
succ :: NumChildren -> NumChildren
$csucc :: NumChildren -> NumChildren
Enum)

-- | 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 (Int -> FailureType -> ShowS
[FailureType] -> ShowS
FailureType -> String
(Int -> FailureType -> ShowS)
-> (FailureType -> String)
-> ([FailureType] -> ShowS)
-> Show FailureType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FailureType] -> ShowS
$cshowList :: [FailureType] -> ShowS
show :: FailureType -> String
$cshow :: FailureType -> String
showsPrec :: Int -> FailureType -> ShowS
$cshowsPrec :: Int -> FailureType -> ShowS
Show, Int -> FailureType
FailureType -> Int
FailureType -> [FailureType]
FailureType -> FailureType
FailureType -> FailureType -> [FailureType]
FailureType -> FailureType -> FailureType -> [FailureType]
(FailureType -> FailureType)
-> (FailureType -> FailureType)
-> (Int -> FailureType)
-> (FailureType -> Int)
-> (FailureType -> [FailureType])
-> (FailureType -> FailureType -> [FailureType])
-> (FailureType -> FailureType -> [FailureType])
-> (FailureType -> FailureType -> FailureType -> [FailureType])
-> Enum FailureType
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: FailureType -> FailureType -> FailureType -> [FailureType]
$cenumFromThenTo :: FailureType -> FailureType -> FailureType -> [FailureType]
enumFromTo :: FailureType -> FailureType -> [FailureType]
$cenumFromTo :: FailureType -> FailureType -> [FailureType]
enumFromThen :: FailureType -> FailureType -> [FailureType]
$cenumFromThen :: FailureType -> FailureType -> [FailureType]
enumFrom :: FailureType -> [FailureType]
$cenumFrom :: FailureType -> [FailureType]
fromEnum :: FailureType -> Int
$cfromEnum :: FailureType -> Int
toEnum :: Int -> FailureType
$ctoEnum :: Int -> FailureType
pred :: FailureType -> FailureType
$cpred :: FailureType -> FailureType
succ :: FailureType -> FailureType
$csucc :: FailureType -> FailureType
Enum)

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 (Int -> IsMichelson -> ShowS
[IsMichelson] -> ShowS
IsMichelson -> String
(Int -> IsMichelson -> ShowS)
-> (IsMichelson -> String)
-> ([IsMichelson] -> ShowS)
-> Show IsMichelson
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IsMichelson] -> ShowS
$cshowList :: [IsMichelson] -> ShowS
show :: IsMichelson -> String
$cshow :: IsMichelson -> String
showsPrec :: Int -> IsMichelson -> ShowS
$cshowsPrec :: Int -> IsMichelson -> ShowS
Show, Int -> IsMichelson
IsMichelson -> Int
IsMichelson -> [IsMichelson]
IsMichelson -> IsMichelson
IsMichelson -> IsMichelson -> [IsMichelson]
IsMichelson -> IsMichelson -> IsMichelson -> [IsMichelson]
(IsMichelson -> IsMichelson)
-> (IsMichelson -> IsMichelson)
-> (Int -> IsMichelson)
-> (IsMichelson -> Int)
-> (IsMichelson -> [IsMichelson])
-> (IsMichelson -> IsMichelson -> [IsMichelson])
-> (IsMichelson -> IsMichelson -> [IsMichelson])
-> (IsMichelson -> IsMichelson -> IsMichelson -> [IsMichelson])
-> Enum IsMichelson
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: IsMichelson -> IsMichelson -> IsMichelson -> [IsMichelson]
$cenumFromThenTo :: IsMichelson -> IsMichelson -> IsMichelson -> [IsMichelson]
enumFromTo :: IsMichelson -> IsMichelson -> [IsMichelson]
$cenumFromTo :: IsMichelson -> IsMichelson -> [IsMichelson]
enumFromThen :: IsMichelson -> IsMichelson -> [IsMichelson]
$cenumFromThen :: IsMichelson -> IsMichelson -> [IsMichelson]
enumFrom :: IsMichelson -> [IsMichelson]
$cenumFrom :: IsMichelson -> [IsMichelson]
fromEnum :: IsMichelson -> Int
$cfromEnum :: IsMichelson -> Int
toEnum :: Int -> IsMichelson
$ctoEnum :: Int -> IsMichelson
pred :: IsMichelson -> IsMichelson
$cpred :: IsMichelson -> IsMichelson
succ :: IsMichelson -> IsMichelson
$csucc :: IsMichelson -> IsMichelson
Enum)

-- | 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 (Int -> HasAnns -> ShowS
[HasAnns] -> ShowS
HasAnns -> String
(Int -> HasAnns -> ShowS)
-> (HasAnns -> String) -> ([HasAnns] -> ShowS) -> Show HasAnns
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasAnns] -> ShowS
$cshowList :: [HasAnns] -> ShowS
show :: HasAnns -> String
$cshow :: HasAnns -> String
showsPrec :: Int -> HasAnns -> ShowS
$cshowsPrec :: Int -> HasAnns -> ShowS
Show, Int -> HasAnns
HasAnns -> Int
HasAnns -> [HasAnns]
HasAnns -> HasAnns
HasAnns -> HasAnns -> [HasAnns]
HasAnns -> HasAnns -> HasAnns -> [HasAnns]
(HasAnns -> HasAnns)
-> (HasAnns -> HasAnns)
-> (Int -> HasAnns)
-> (HasAnns -> Int)
-> (HasAnns -> [HasAnns])
-> (HasAnns -> HasAnns -> [HasAnns])
-> (HasAnns -> HasAnns -> [HasAnns])
-> (HasAnns -> HasAnns -> HasAnns -> [HasAnns])
-> Enum HasAnns
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: HasAnns -> HasAnns -> HasAnns -> [HasAnns]
$cenumFromThenTo :: HasAnns -> HasAnns -> HasAnns -> [HasAnns]
enumFromTo :: HasAnns -> HasAnns -> [HasAnns]
$cenumFromTo :: HasAnns -> HasAnns -> [HasAnns]
enumFromThen :: HasAnns -> HasAnns -> [HasAnns]
$cenumFromThen :: HasAnns -> HasAnns -> [HasAnns]
enumFrom :: HasAnns -> [HasAnns]
$cenumFrom :: HasAnns -> [HasAnns]
fromEnum :: HasAnns -> Int
$cfromEnum :: HasAnns -> Int
toEnum :: Int -> HasAnns
$ctoEnum :: Int -> HasAnns
pred :: HasAnns -> HasAnns
$cpred :: HasAnns -> HasAnns
succ :: HasAnns -> HasAnns
$csucc :: HasAnns -> HasAnns
Enum)

-- | 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 :: forall (c :: InstrClass).
SingInstrClass c -> Sing (GetClassified c)
getClassified (SInstrClass Sing n
a Sing n
_ Sing n
_ Sing n
_) = Sing n
Sing (GetClassified c)
a
instance ClassifyInstr FailureType where
  type GetClassified ('InstrClass _ a _ _) = a
  getClassified :: forall (c :: InstrClass).
SingInstrClass c -> Sing (GetClassified c)
getClassified (SInstrClass Sing n
_ Sing n
a Sing n
_ Sing n
_) = Sing n
Sing (GetClassified c)
a
instance ClassifyInstr IsMichelson where
  type GetClassified ('InstrClass _ _ a _) = a
  getClassified :: forall (c :: InstrClass).
SingInstrClass c -> Sing (GetClassified c)
getClassified (SInstrClass Sing n
_ Sing n
_ Sing n
a Sing n
_) = Sing n
Sing (GetClassified c)
a
instance ClassifyInstr HasAnns where
  type GetClassified ('InstrClass _ _ _ a) = a
  getClassified :: forall (c :: InstrClass).
SingInstrClass c -> Sing (GetClassified c)
getClassified (SInstrClass Sing n
_ Sing n
_ Sing n
_ Sing n
a) = Sing n
Sing (GetClassified c)
a