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

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

import Data.Singletons (SingI)

import Morley.Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)
import Morley.Michelson.TypeCheck.Types (HST(..), SomeTcInstr(..), SomeTcInstrOut(..))
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Convert (instrToOps)
import Morley.Michelson.Typed.Instr (Instr, castInstr)
import Morley.Michelson.Typed.View (SomeView'(..), View'(..))
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Instr (InstrAbstract(..))
import Morley.Util.TH (deriveGADTNFData)

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

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

deriving stock instance Show op => Show (TypeCheckedOp op)
deriving stock instance Functor TypeCheckedOp

instance Eq op => Eq (TypeCheckedOp op) where
  WellTypedOp i1 == WellTypedOp i2 = castInstr i1 == Just i2
  IllTypedOp i1 == IllTypedOp i2 = i1 == i2
  _ == _ = False

-- | Represents a non-well-typed operation
data IllTypedInstr op
  = SemiTypedInstr (TypeCheckedInstr op) -- ^ Constructs a partialy typed operation.
  | NonTypedInstr op  -- ^ Constructs a completely untyped operation.
  deriving stock (Show, Eq, Generic, Functor)

deriving anyclass instance (NFData (TypeCheckedOp op), NFData op) => NFData (IllTypedInstr op)

instance RenderDoc op => RenderDoc (TypeCheckedOp op) 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 `SomeTcInstr`
someInstrToOp :: SomeTcInstr inp -> TypeCheckedOp op
someInstrToOp (hst :/ rest) = case hst of
  SNil -> go rest
  (::&){} -> go rest
  where
    go :: SingI inp => SomeTcInstrOut inp -> TypeCheckedOp op
    go (i ::: _) = WellTypedOp i
    go (AnyOutInstr i) = WellTypedOp (i @'[])

-- | Makes a view with well-typed code, taking the untyped and typechecked view.
someViewToOp :: U.View' op -> SomeView st -> U.View' (TypeCheckedOp op)
someViewToOp U.View{..} (SomeView View{..}) = U.View
  { U.viewCode = [WellTypedOp vCode]
  , ..
  }

$(deriveGADTNFData ''TypeCheckedOp)