-- 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(..), SomeInstr(..), SomeInstrOut(..))
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 (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

deriving stock instance Show 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 (Int -> IllTypedInstr -> ShowS
[IllTypedInstr] -> ShowS
IllTypedInstr -> String
(Int -> IllTypedInstr -> ShowS)
-> (IllTypedInstr -> String)
-> ([IllTypedInstr] -> ShowS)
-> Show IllTypedInstr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IllTypedInstr] -> ShowS
$cshowList :: [IllTypedInstr] -> ShowS
show :: IllTypedInstr -> String
$cshow :: IllTypedInstr -> String
showsPrec :: Int -> IllTypedInstr -> ShowS
$cshowsPrec :: Int -> IllTypedInstr -> ShowS
Show, 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 :: forall (inp :: [T]). 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 :: forall (inp :: [T]). SingI inp => 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 (forall (out :: [T]). Instr inp out
i @'[])

-- | Makes a view with well-typed code, taking the untyped and typechecked view.
someViewToOp :: U.View' op -> SomeView st -> U.View' TypeCheckedOp
someViewToOp :: forall op (st :: T). View' op -> SomeView st -> View' TypeCheckedOp
someViewToOp U.View{[op]
Ty
ViewName
viewCode :: forall op. View' op -> [op]
viewReturn :: forall op. View' op -> Ty
viewArgument :: forall op. View' op -> Ty
viewName :: forall op. View' op -> ViewName
viewCode :: [op]
viewReturn :: Ty
viewArgument :: Ty
viewName :: ViewName
..} (SomeView View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg st ret
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vCode :: ViewCode' Instr arg st ret
vReturn :: Notes ret
vArgument :: Notes arg
vName :: ViewName
..}) = View :: forall op. ViewName -> Ty -> Ty -> [op] -> View' op
U.View
  { viewCode :: [TypeCheckedOp]
U.viewCode = [ViewCode' Instr arg st ret -> TypeCheckedOp
forall (inp :: [T]) (out :: [T]).
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp
WellTypedOp ViewCode' Instr arg st ret
vCode]
  , Ty
ViewName
viewReturn :: Ty
viewArgument :: Ty
viewName :: ViewName
viewReturn :: Ty
viewArgument :: Ty
viewName :: ViewName
..
  }

$(deriveGADTNFData ''TypeCheckedOp)