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

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

import Data.Singletons (SingI)

import Morley.Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Morley.Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))
import Morley.Michelson.Typed.Convert (instrToOps)
import Morley.Michelson.Typed.Instr (Instr, castInstr)
import Morley.Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..))
import Morley.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 i1 == WellTypedOp i2 = castInstr i1 == Just i2
  IllTypedOp i1 == IllTypedOp i2 = i1 == i2
  _ == _ = 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 (Eq, Generic)

deriving anyclass instance NFData TypeCheckedOp => NFData IllTypedInstr

instance RenderDoc TypeCheckedOp where
  renderDoc _ (WellTypedOp instr) = renderOpsListNoBraces False (instrToOps instr)
  renderDoc pn (IllTypedOp (SemiTypedInstr instr)) = renderDoc pn instr
  renderDoc pn (IllTypedOp (NonTypedInstr op)) = renderDoc pn op

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

$(deriveGADTNFData ''TypeCheckedOp)