-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- This module provides data types for representing partially typed
-- instructions.
module Michelson.TypeCheck.TypeCheckedOp
  ( TypeCheckedInstr
  , TypeCheckedOp(..)
  , IllTypedInstr(..)
  , someInstrToOp
  ) where

import Data.Typeable (cast)

import Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))
import Michelson.Typed.Convert (instrToOps)
import Michelson.Typed.Instr (Instr)
import Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..))
import Util.TH (deriveGADTNFData)

-- | Represents a root of a partially typed operation tree.
type TypeCheckedInstr = InstrAbstract TypeCheckedOp

-- | Represents nodes of a partially typed operation tree.
data TypeCheckedOp where
  -- | Constructs well-typed node.
  WellTypedOp :: (Typeable inp, Typeable out) => Instr inp out -> TypeCheckedOp
  -- | Constructs ill-typed node which might in turn contain well-typed and
  -- non-typed operations.
  IllTypedOp :: IllTypedInstr -> TypeCheckedOp

instance Eq TypeCheckedOp where
  WellTypedOp i1 :: Instr inp out
i1 == :: TypeCheckedOp -> TypeCheckedOp -> Bool
== WellTypedOp i2 :: Instr inp out
i2 = Instr inp out -> Maybe (Instr inp out)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Instr inp out
i1 Maybe (Instr inp out) -> Maybe (Instr inp out) -> Bool
forall a. Eq a => a -> a -> Bool
== Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i2
  IllTypedOp i1 :: IllTypedInstr
i1 == IllTypedOp i2 :: IllTypedInstr
i2 = IllTypedInstr
i1 IllTypedInstr -> IllTypedInstr -> Bool
forall a. Eq a => a -> a -> Bool
== IllTypedInstr
i2
  _ == _ = Bool
False

-- | Represents a non-well-typed operation
data IllTypedInstr
  = SemiTypedInstr TypeCheckedInstr -- ^ Constructs a partialy typed operation.
  | NonTypedInstr ExpandedOp  -- ^ Constructs a completely untyped operation.
  deriving stock (IllTypedInstr -> IllTypedInstr -> Bool
(IllTypedInstr -> IllTypedInstr -> Bool)
-> (IllTypedInstr -> IllTypedInstr -> Bool) -> Eq IllTypedInstr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IllTypedInstr -> IllTypedInstr -> Bool
$c/= :: IllTypedInstr -> IllTypedInstr -> Bool
== :: IllTypedInstr -> IllTypedInstr -> Bool
$c== :: IllTypedInstr -> IllTypedInstr -> Bool
Eq, (forall x. IllTypedInstr -> Rep IllTypedInstr x)
-> (forall x. Rep IllTypedInstr x -> IllTypedInstr)
-> Generic IllTypedInstr
forall x. Rep IllTypedInstr x -> IllTypedInstr
forall x. IllTypedInstr -> Rep IllTypedInstr x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep IllTypedInstr x -> IllTypedInstr
$cfrom :: forall x. IllTypedInstr -> Rep IllTypedInstr x
Generic)

deriving anyclass instance NFData TypeCheckedOp => NFData IllTypedInstr

instance RenderDoc TypeCheckedOp where
  renderDoc :: RenderContext -> TypeCheckedOp -> Doc
renderDoc _ (WellTypedOp instr :: Instr inp out
instr) = Bool -> [ExpandedOp] -> Doc
forall op. RenderDoc op => Bool -> [op] -> Doc
renderOpsListNoBraces Bool
False (Instr inp out -> [ExpandedOp]
forall (inp :: [T]) (out :: [T]).
HasCallStack =>
Instr inp out -> [ExpandedOp]
instrToOps Instr inp out
instr)
  renderDoc pn :: RenderContext
pn (IllTypedOp (SemiTypedInstr instr :: TypeCheckedInstr
instr)) = RenderContext -> TypeCheckedInstr -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn TypeCheckedInstr
instr
  renderDoc pn :: RenderContext
pn (IllTypedOp (NonTypedInstr op :: ExpandedOp
op)) = RenderContext -> ExpandedOp -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn ExpandedOp
op

-- | Makes a well-typed node out of `SomeInstr`
someInstrToOp :: SomeInstr inp -> TypeCheckedOp
someInstrToOp :: SomeInstr inp -> TypeCheckedOp
someInstrToOp (hst :: HST inp
hst :/ rest :: SomeInstrOut inp
rest) = case HST inp
hst of
  SNil -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]).
Typeable inp =>
SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
  (::&){} -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]).
Typeable inp =>
SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
  where
    go :: forall inp. Typeable inp => SomeInstrOut inp -> TypeCheckedOp
    go :: SomeInstrOut inp -> TypeCheckedOp
go (i :: Instr inp out
i ::: _) = Instr inp out -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(Typeable inp, Typeable out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp Instr inp out
i
    go (AnyOutInstr i :: forall (out :: [T]). Instr inp out
i) = Instr inp '[] -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(Typeable inp, Typeable out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp (Instr inp '[]
forall (out :: [T]). Instr inp out
i @'[])

$(deriveGADTNFData ''TypeCheckedOp)