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

-- | Module, providing 'T' data type, representing Michelson
-- language types without annotations.
module Morley.Michelson.Typed.T
  ( T (..)
  , toUType
  , buildStack
  ) where

import Data.Data (Data)
import Fmt (Buildable(..), Builder, listF)

import Morley.Michelson.Printer.Util (Prettier(..), RenderDoc(..), buildRenderDocExtended)
import Morley.Michelson.Untyped.Annotation qualified as Un
import Morley.Michelson.Untyped.Type qualified as Un
import Morley.Util.MismatchError
import Morley.Util.Peano qualified as Peano

-- | Michelson language type with annotations stripped off.
data T =
    TKey
  | TUnit
  | TSignature
  | TChainId
  | TOption T
  | TList T
  | TSet T
  | TOperation
  | TContract T
  | TTicket T
  | TPair T T
  | TOr T T
  | TLambda T T
  | TMap T T
  | TBigMap T T
  | TInt
  | TNat
  | TString
  | TBytes
  | TMutez
  | TBool
  | TKeyHash
  | TBls12381Fr
  | TBls12381G1
  | TBls12381G2
  | TTimestamp
  | TAddress
  | TChest
  | TChestKey
  | TSaplingState Peano.Peano
  | TSaplingTransaction Peano.Peano
  | TTxRollupL2Address
  | TNever
  deriving stock (T -> T -> Bool
(T -> T -> Bool) -> (T -> T -> Bool) -> Eq T
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: T -> T -> Bool
$c/= :: T -> T -> Bool
== :: T -> T -> Bool
$c== :: T -> T -> Bool
Eq, Int -> T -> ShowS
[T] -> ShowS
T -> String
(Int -> T -> ShowS) -> (T -> String) -> ([T] -> ShowS) -> Show T
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [T] -> ShowS
$cshowList :: [T] -> ShowS
show :: T -> String
$cshow :: T -> String
showsPrec :: Int -> T -> ShowS
$cshowsPrec :: Int -> T -> ShowS
Show, (forall x. T -> Rep T x) -> (forall x. Rep T x -> T) -> Generic T
forall x. Rep T x -> T
forall x. T -> Rep T x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep T x -> T
$cfrom :: forall x. T -> Rep T x
Generic, Typeable T
Typeable T
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> T -> c T)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c T)
-> (T -> Constr)
-> (T -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c T))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T))
-> ((forall b. Data b => b -> b) -> T -> T)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r)
-> (forall u. (forall d. Data d => d -> u) -> T -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> T -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> T -> m T)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> T -> m T)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> T -> m T)
-> Data T
T -> DataType
T -> Constr
(forall b. Data b => b -> b) -> T -> T
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> T -> u
forall u. (forall d. Data d => d -> u) -> T -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> T -> m T
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c T
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> T -> c T
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c T)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> T -> m T
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> T -> m T
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> T -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> T -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> T -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> T -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
gmapT :: (forall b. Data b => b -> b) -> T -> T
$cgmapT :: (forall b. Data b => b -> b) -> T -> T
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c T)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c T)
dataTypeOf :: T -> DataType
$cdataTypeOf :: T -> DataType
toConstr :: T -> Constr
$ctoConstr :: T -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c T
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c T
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> T -> c T
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> T -> c T
Data)

instance NFData T

-- | Converts from 'T' to 'Un.Ty'.
toUType :: T -> Un.Ty
toUType :: T -> Ty
toUType T
t = T -> TypeAnn -> Ty
Un.Ty (T -> T
convert T
t) TypeAnn
forall {k} (a :: k). Annotation a
Un.noAnn
  where
    convert :: T -> Un.T
    convert :: T -> T
convert T
TInt = T
Un.TInt
    convert T
TNat = T
Un.TNat
    convert T
TString = T
Un.TString
    convert T
TBytes = T
Un.TBytes
    convert T
TMutez = T
Un.TMutez
    convert T
TBool = T
Un.TBool
    convert T
TKeyHash = T
Un.TKeyHash
    convert T
TTimestamp = T
Un.TTimestamp
    convert T
TAddress = T
Un.TAddress
    convert T
TKey = T
Un.TKey
    convert T
TBls12381Fr = T
Un.TBls12381Fr
    convert T
TBls12381G1 = T
Un.TBls12381G1
    convert T
TBls12381G2 = T
Un.TBls12381G2
    convert T
TUnit = T
Un.TUnit
    convert T
TSignature = T
Un.TSignature
    convert T
TChainId = T
Un.TChainId
    convert T
TChest = T
Un.TChest
    convert T
TChestKey = T
Un.TChestKey
    convert T
TTxRollupL2Address = T
Un.TTxRollupL2Address
    convert T
TNever = T
Un.TNever
    convert (TSaplingState Peano
n) = Natural -> T
Un.TSaplingState (Peano -> Natural
Peano.toNatural Peano
n)
    convert (TSaplingTransaction Peano
n) = Natural -> T
Un.TSaplingTransaction (Peano -> Natural
Peano.toNatural Peano
n)
    convert (TOption T
a) = Ty -> T
Un.TOption (T -> Ty
toUType T
a)
    convert (TList T
a) = Ty -> T
Un.TList (T -> Ty
toUType T
a)
    convert (TSet T
a) = Ty -> T
Un.TSet (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.unwrapT (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ T -> Ty
toUType T
a) TypeAnn
forall {k} (a :: k). Annotation a
Un.noAnn
    convert (T
TOperation) = T
Un.TOperation
    convert (TContract T
a) = Ty -> T
Un.TContract (T -> Ty
toUType T
a)
    convert (TTicket T
a) = Ty -> T
Un.TTicket (T -> Ty
toUType T
a)
    convert (TPair T
a T
b) =
      FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
Un.TPair FieldAnn
forall {k} (a :: k). Annotation a
Un.noAnn FieldAnn
forall {k} (a :: k). Annotation a
Un.noAnn VarAnn
forall {k} (a :: k). Annotation a
Un.noAnn VarAnn
forall {k} (a :: k). Annotation a
Un.noAnn (T -> Ty
toUType T
a) (T -> Ty
toUType T
b)
    convert (TOr T
a T
b) =
      FieldAnn -> FieldAnn -> Ty -> Ty -> T
Un.TOr FieldAnn
forall {k} (a :: k). Annotation a
Un.noAnn FieldAnn
forall {k} (a :: k). Annotation a
Un.noAnn (T -> Ty
toUType T
a) (T -> Ty
toUType T
b)
    convert (TLambda T
a T
b) =
      Ty -> Ty -> T
Un.TLambda (T -> Ty
toUType T
a) (T -> Ty
toUType T
b)
    convert (TMap T
a T
b) =
      Ty -> Ty -> T
Un.TMap (T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.unwrapT (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ T -> Ty
toUType T
a) TypeAnn
forall {k} (a :: k). Annotation a
Un.noAnn) (T -> Ty
toUType T
b)
    convert (TBigMap T
a T
b) =
      Ty -> Ty -> T
Un.TBigMap (T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.unwrapT (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ T -> Ty
toUType T
a) TypeAnn
forall {k} (a :: k). Annotation a
Un.noAnn) (T -> Ty
toUType T
b)

instance Buildable T where
  build :: T -> Builder
build = Ty -> Builder
forall p. Buildable p => p -> Builder
build (Ty -> Builder) -> (T -> Ty) -> T -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Ty
toUType

instance Buildable (MismatchError T) where
  build :: MismatchError T -> Builder
build = MismatchError T -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended

instance Buildable (MismatchError [T]) where
  build :: MismatchError [T] -> Builder
build = MismatchError [T] -> Builder
forall a. RenderDoc a => a -> Builder
buildRenderDocExtended

instance RenderDoc T where
  renderDoc :: RenderContext -> T -> Doc
renderDoc RenderContext
context = RenderContext -> Ty -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context (Ty -> Doc) -> (T -> Ty) -> T -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Ty
toUType

instance RenderDoc (Prettier T) where
  renderDoc :: RenderContext -> Prettier T -> Doc
renderDoc RenderContext
context = RenderContext -> Prettier Ty -> Doc
forall a. RenderDoc a => RenderContext -> a -> Doc
renderDoc RenderContext
context (Prettier Ty -> Doc)
-> (Prettier T -> Prettier Ty) -> Prettier T -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T -> Ty) -> Prettier T -> Prettier Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T -> Ty
toUType

instance RenderDoc (MismatchError T) where
  renderDoc :: RenderContext -> MismatchError T -> Doc
renderDoc RenderContext
ctx = RenderContext -> MismatchError (Prettier T) -> Doc
forall a. RenderDoc a => RenderContext -> MismatchError a -> Doc
renderDocDiff RenderContext
ctx (MismatchError (Prettier T) -> Doc)
-> (MismatchError T -> MismatchError (Prettier T))
-> MismatchError T
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T -> Prettier T) -> MismatchError T -> MismatchError (Prettier T)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap T -> Prettier T
forall a. a -> Prettier a
Prettier

instance RenderDoc (MismatchError [T]) where
  renderDoc :: RenderContext -> MismatchError [T] -> Doc
renderDoc RenderContext
ctx = RenderContext -> MismatchError [Prettier T] -> Doc
forall a. RenderDoc a => RenderContext -> MismatchError [a] -> Doc
renderDocDiffList RenderContext
ctx (MismatchError [Prettier T] -> Doc)
-> (MismatchError [T] -> MismatchError [Prettier T])
-> MismatchError [T]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([T] -> [Prettier T])
-> MismatchError [T] -> MismatchError [Prettier T]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([T] -> [Prettier T])
 -> MismatchError [T] -> MismatchError [Prettier T])
-> ((T -> Prettier T) -> [T] -> [Prettier T])
-> (T -> Prettier T)
-> MismatchError [T]
-> MismatchError [Prettier T]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T -> Prettier T) -> [T] -> [Prettier T]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) T -> Prettier T
forall a. a -> Prettier a
Prettier

-- | Format type stack in a pretty way.
buildStack :: [T] -> Builder
buildStack :: [T] -> Builder
buildStack = [T] -> Builder
forall (f :: * -> *) a. (Foldable f, Buildable a) => f a -> Builder
listF