-- 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(..), Doc, listF)

import Morley.Michelson.Printer.Util (RenderDoc(..))
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
  | TNever
  deriving stock (T -> T -> Bool
(T -> T -> Bool) -> (T -> T -> Bool) -> Eq T
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: T -> T -> Bool
== :: T -> T -> Bool
$c/= :: T -> T -> Bool
/= :: 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
$cshowsPrec :: Int -> T -> ShowS
showsPrec :: Int -> T -> ShowS
$cshow :: T -> String
show :: T -> String
$cshowList :: [T] -> ShowS
showList :: [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
$cfrom :: forall x. T -> Rep T x
from :: forall x. T -> Rep T x
$cto :: forall x. Rep T x -> T
to :: forall x. Rep T x -> T
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 -> Constr
T -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> T -> c T
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> T -> c T
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c T
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c T
$ctoConstr :: T -> Constr
toConstr :: T -> Constr
$cdataTypeOf :: T -> DataType
dataTypeOf :: T -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c T)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c T)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c T)
$cgmapT :: (forall b. Data b => b -> b) -> T -> T
gmapT :: (forall b. Data b => b -> b) -> T -> T
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> T -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> T -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> T -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> T -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> T -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m T
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> T -> m 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
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 -> Doc
build = Ty -> Doc
forall a. Buildable a => a -> Doc
build (Ty -> Doc) -> (T -> Ty) -> T -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. T -> Ty
toUType

instance Buildable (MismatchError T) where
  build :: MismatchError T -> Doc
build = MismatchError T -> Doc
forall a. Buildable a => MismatchError a -> Doc
buildDocDiff

instance Buildable (MismatchError [T]) where
  build :: MismatchError [T] -> Doc
build = MismatchError [T] -> Doc
forall a. Buildable a => MismatchError [a] -> Doc
buildDocDiffList

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

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