-- 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.Annotation
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 Instr inp out
i1 == :: TypeCheckedOp op -> TypeCheckedOp op -> 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 op
i1 == IllTypedOp IllTypedInstr op
i2 = IllTypedInstr op
i1 IllTypedInstr op -> IllTypedInstr op -> Bool
forall a. Eq a => a -> a -> Bool
== IllTypedInstr op
i2
  TypeCheckedOp op
_ == TypeCheckedOp op
_ = Bool
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 (Int -> IllTypedInstr op -> ShowS
[IllTypedInstr op] -> ShowS
IllTypedInstr op -> String
(Int -> IllTypedInstr op -> ShowS)
-> (IllTypedInstr op -> String)
-> ([IllTypedInstr op] -> ShowS)
-> Show (IllTypedInstr op)
forall op. Show op => Int -> IllTypedInstr op -> ShowS
forall op. Show op => [IllTypedInstr op] -> ShowS
forall op. Show op => IllTypedInstr op -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [IllTypedInstr op] -> ShowS
$cshowList :: forall op. Show op => [IllTypedInstr op] -> ShowS
show :: IllTypedInstr op -> String
$cshow :: forall op. Show op => IllTypedInstr op -> String
showsPrec :: Int -> IllTypedInstr op -> ShowS
$cshowsPrec :: forall op. Show op => Int -> IllTypedInstr op -> ShowS
Show, IllTypedInstr op -> IllTypedInstr op -> Bool
(IllTypedInstr op -> IllTypedInstr op -> Bool)
-> (IllTypedInstr op -> IllTypedInstr op -> Bool)
-> Eq (IllTypedInstr op)
forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IllTypedInstr op -> IllTypedInstr op -> Bool
$c/= :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
== :: IllTypedInstr op -> IllTypedInstr op -> Bool
$c== :: forall op. Eq op => IllTypedInstr op -> IllTypedInstr op -> Bool
Eq, (forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x)
-> (forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op)
-> Generic (IllTypedInstr op)
forall x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall x. IllTypedInstr op -> Rep (IllTypedInstr op) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
$cto :: forall op x. Rep (IllTypedInstr op) x -> IllTypedInstr op
$cfrom :: forall op x. IllTypedInstr op -> Rep (IllTypedInstr op) x
Generic, (forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b)
-> (forall a b. a -> IllTypedInstr b -> IllTypedInstr a)
-> Functor IllTypedInstr
forall a b. a -> IllTypedInstr b -> IllTypedInstr a
forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
$c<$ :: forall a b. a -> IllTypedInstr b -> IllTypedInstr a
fmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
$cfmap :: forall a b. (a -> b) -> IllTypedInstr a -> IllTypedInstr b
Functor)

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

instance RenderDoc op => RenderDoc (TypeCheckedOp op) where
  renderDoc :: RenderContext -> TypeCheckedOp op -> 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 op
instr)) = RenderContext -> TypeCheckedInstr op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn TypeCheckedInstr op
instr
  renderDoc RenderContext
pn (IllTypedOp (NonTypedInstr op
op)) = RenderContext -> op -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
pn op
op

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

-- | Makes takes a typed view and converts it into an untyped one with
-- typechecked code.
someViewToOp :: SomeView st -> U.View' (TypeCheckedOp op)
someViewToOp :: forall (st :: T) op. SomeView st -> View' (TypeCheckedOp op)
someViewToOp (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 op]
U.viewCode = [ViewCode' Instr arg st ret -> TypeCheckedOp op
forall (inp :: [T]) (out :: [T]) op.
(SingI inp, SingI out) =>
Instr inp out -> TypeCheckedOp op
WellTypedOp ViewCode' Instr arg st ret
vCode]
  , viewName :: ViewName
U.viewName = ViewName
vName
  , viewArgument :: Ty
U.viewArgument = Notes arg -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes arg
vArgument
  , viewReturn :: Ty
U.viewReturn = Notes ret -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes ret
vReturn
  }

$(deriveGADTNFData ''TypeCheckedOp)