-- 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.Singletons (SingI)

import Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))
import Michelson.Typed.Convert (instrToOps)
import Michelson.Typed.Instr (Instr, castInstr)
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 :: (SingI inp, SingI 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 Instr inp out
i1 == :: TypeCheckedOp -> TypeCheckedOp -> Bool
== WellTypedOp Instr inp out
i2 = Instr inp out -> Maybe (Instr inp out)
forall (inp1 :: [T]) (out1 :: [T]) (inp2 :: [T]) (out2 :: [T]).
(SingI inp1, SingI out1, SingI inp2, SingI out2) =>
Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr 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 IllTypedInstr
i1 == IllTypedOp IllTypedInstr
i2 = IllTypedInstr
i1 IllTypedInstr -> IllTypedInstr -> Bool
forall a. Eq a => a -> a -> Bool
== IllTypedInstr
i2
  TypeCheckedOp
_ == TypeCheckedOp
_ = 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 RenderContext
_ (WellTypedOp 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 RenderContext
pn (IllTypedOp (SemiTypedInstr TypeCheckedInstr
instr)) = RenderContext -> TypeCheckedInstr -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn TypeCheckedInstr
instr
  renderDoc RenderContext
pn (IllTypedOp (NonTypedInstr 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 inp
hst :/ SomeInstrOut inp
rest) = case HST inp
hst of
  HST inp
SNil -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]). SingI inp => SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
  (::&){} -> SomeInstrOut inp -> TypeCheckedOp
forall (inp :: [T]). SingI inp => SomeInstrOut inp -> TypeCheckedOp
go SomeInstrOut inp
rest
  where
    go :: forall inp. SingI inp => SomeInstrOut inp -> TypeCheckedOp
    go :: SomeInstrOut inp -> TypeCheckedOp
go (Instr inp out
i ::: HST out
_) = Instr inp out -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp Instr inp out
i
    go (AnyOutInstr forall (out :: [T]). Instr inp out
i) = Instr inp '[] -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp (Instr inp '[]
forall (out :: [T]). Instr inp out
i @'[])

$(deriveGADTNFData ''TypeCheckedOp)