-- 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 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 a view with well-typed code, taking the untyped and typechecked view.
someViewToOp :: U.View' op -> SomeView st -> U.View' (TypeCheckedOp op)
someViewToOp :: forall op (st :: T).
View' op -> SomeView st -> View' (TypeCheckedOp op)
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 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]
  , Ty
ViewName
viewReturn :: Ty
viewArgument :: Ty
viewName :: ViewName
viewReturn :: Ty
viewArgument :: Ty
viewName :: ViewName
..
  }

$(deriveGADTNFData ''TypeCheckedOp)