-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, containing functions to convert @Morley.Michelson.Untyped.Ty@ to
-- @Morley.Michelson.Typed.T.T@ Michelson type representation (type stripped off all
-- annotations) and to @Morley.Michelson.Typed.Annotation.Notes@ value (which contains
-- field and type annotations for a given Michelson type).
--
-- I.e. @Morley.Michelson.Untyped.Ty@ is split to value @t :: T@ and value of type
-- @Notes t@ for which @t@ is a type representation of value @t@.
module Morley.Michelson.Typed.Extract
  ( fromUType
  , mkUType
  , mkUType'
  , toUType
  , withUType

  , pattern AsUType
  , pattern AsUTypeExt
  ) where

import Data.Singletons (Sing, SingI, fromSing)

import Morley.Michelson.Typed.Annotation (Notes(..), notesSing)
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..), toUType)
import qualified Morley.Michelson.Untyped as Un

{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}

fromUType :: Un.Ty -> T
fromUType ut = withUType ut (fromSing . notesSing)

mkUType :: SingI x => Notes x -> Un.Ty
mkUType notes = mkUType' (notesSing notes, notes)

mkUType' :: (Sing x, Notes x) -> Un.Ty
mkUType' = \case
  (STInt, NTInt tn)               -> Un.Ty Un.TInt tn
  (STNat, NTNat tn)               -> Un.Ty Un.TNat tn
  (STString, NTString tn)         -> Un.Ty Un.TString tn
  (STBytes, NTBytes tn)           -> Un.Ty Un.TBytes tn
  (STMutez, NTMutez tn)           -> Un.Ty Un.TMutez tn
  (STBool, NTBool tn)             -> Un.Ty Un.TBool tn
  (STKeyHash, NTKeyHash tn)       -> Un.Ty Un.TKeyHash tn
  (STBls12381Fr, NTBls12381Fr tn) -> Un.Ty Un.TBls12381Fr tn
  (STBls12381G1, NTBls12381G1 tn) -> Un.Ty Un.TBls12381G1 tn
  (STBls12381G2, NTBls12381G2 tn) -> Un.Ty Un.TBls12381G2 tn
  (STTimestamp, NTTimestamp tn)   -> Un.Ty Un.TTimestamp tn
  (STAddress, NTAddress tn)       -> Un.Ty Un.TAddress tn
  (STKey, NTKey tn)               -> Un.Ty Un.TKey tn
  (STUnit, NTUnit tn)             -> Un.Ty Un.TUnit tn
  (STSignature, NTSignature tn)   -> Un.Ty Un.TSignature tn
  (STChainId, NTChainId tn)       -> Un.Ty Un.TChainId tn
  (STOption t, NTOption tn n)     -> Un.Ty (Un.TOption $ mkUType' (t, n)) tn
  (STList t, NTList tn n)         -> Un.Ty (Un.TList $ mkUType' (t, n)) tn
  (STSet t, NTSet tn n)           -> Un.Ty (Un.TSet $ mkUType' (t, n)) tn
  (STOperation, NTOperation tn)   -> Un.Ty Un.TOperation tn
  (STNever, NTNever tn)           -> Un.Ty Un.TNever tn
  (STContract t, NTContract tn n) ->
    Un.Ty (Un.TContract $ mkUType' (t, n)) tn
  (STTicket t, NTTicket tn n) ->
      Un.Ty (Un.TTicket $ mkUType' (t, n)) tn
  (STPair t t', NTPair tn fl fr vl vr nl nr) ->
    Un.Ty
    (Un.TPair fl fr vl vr
    (mkUType' (t, nl))
    (mkUType' (t', nr)))
    tn
  (STOr t t', NTOr tn fl fr nl nr) ->
    Un.Ty
    (Un.TOr fl fr
    (mkUType' (t, nl))
    (mkUType' (t', nr)))
    tn
  (STLambda t t', NTLambda tn np nq) ->
    Un.Ty
    (Un.TLambda
    (mkUType' (t, np))
    (mkUType' (t', nq)))
    tn
  (STMap t t', NTMap tn nk nv) ->
    Un.Ty
    (Un.TMap
    (mkUType' (t, nk))
    (mkUType' (t', nv)))
    tn
  (STBigMap t t', NTBigMap tn nk nv) ->
    Un.Ty
    (Un.TBigMap
    (mkUType' (t, nk))
    (mkUType' (t', nv)))
    tn

-- | Convert 'Un.Ty' to the isomorphic set of information from typed world.
withUType
  :: Un.Ty
  -> (forall t. SingI t => Notes t -> r)
  -> r
withUType (Un.Ty ut tn) cont = case ut of

  Un.TInt ->
    cont (NTInt tn)

  Un.TNat ->
    cont (NTNat tn)

  Un.TString ->
    cont (NTString tn)

  Un.TBytes ->
    cont (NTBytes tn)

  Un.TMutez ->
    cont (NTMutez tn)

  Un.TBool ->
    cont (NTBool tn)

  Un.TKeyHash ->
    cont (NTKeyHash tn)

  Un.TBls12381Fr ->
    cont (NTBls12381Fr tn)

  Un.TBls12381G1 ->
    cont (NTBls12381G1 tn)

  Un.TBls12381G2 ->
    cont (NTBls12381G2 tn)

  Un.TTimestamp ->
    cont (NTTimestamp tn)

  Un.TAddress ->
    cont (NTAddress tn)

  Un.TKey ->
    cont (NTKey tn)

  Un.TUnit ->
    cont (NTUnit tn)

  Un.TSignature ->
    cont (NTSignature tn)

  Un.TChainId ->
    cont (NTChainId tn)

  Un.TNever ->
    cont (NTNever tn)

  Un.TOption internalT -> withUType internalT $
    \(notesInternalT :: Notes internalT) ->
      cont (NTOption tn notesInternalT)

  Un.TList listT -> withUType listT $
    \(notesListT :: Notes listT) ->
      cont (NTList tn notesListT)

  Un.TSet setT -> withUType setT $
    \(notesSetT :: Notes setT) ->
      cont (NTSet tn notesSetT)

  Un.TOperation ->
    cont (NTOperation tn)

  Un.TContract contractT -> withUType contractT $
    \(notesContractT :: Notes contractT) ->
      cont (NTContract tn notesContractT)

  Un.TTicket ticketT -> withUType ticketT $
    \(notesTicketT :: Notes ticketT) ->
      cont (NTTicket tn notesTicketT)

  Un.TPair la ra lv rv lt rt ->
    withUType lt $ \ln ->
      withUType rt $ \rn ->
        cont (NTPair tn la ra lv rv ln rn)

  Un.TOr la ra lt rt ->
    withUType lt $ \ln ->
      withUType rt $ \rn ->
        cont (NTOr tn la ra ln rn)

  Un.TLambda lt rt ->
    withUType lt $ \ln ->
      withUType rt $ \rn ->
        cont (NTLambda tn ln rn)

  Un.TMap keyT valT ->
    withUType keyT $ \keyN ->
      withUType valT $ \valN ->
        cont @('TMap _ _) (NTMap tn keyN valN)

  Un.TBigMap keyT valT ->
    withUType keyT $ \keyN ->
      withUType valT $ \valN ->
        cont @('TBigMap _ _) (NTBigMap tn keyN valN)

-- Helper datatype for 'AsUType'.
data SomeTypedInfo = forall t. SingI t => SomeTypedInfo (Notes t)

-- | Transparently represent untyped 'Un.Ty' as wrapper over @Notes t@
-- from typed world with @SingI t@ constraint.
--
-- As expression this carries logic of 'mkUType', and as pattern it performs
-- 'withUType' but may make code a bit cleaner.
--
-- Note about constraints: pattern signatures usually require two constraints -
-- one they require and another one which they provide. In our case we require
-- nothing (thus first constraint is @()@) and provide some knowledge about @t@.
pattern AsUType :: () => (SingI t) => Notes t -> Un.Ty
pattern AsUType notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo notes)
  where AsUType notes = mkUType notes
{-# COMPLETE AsUType #-}

-- | Similar to 'AsUType', but also gives 'Sing' for given type.
pattern AsUTypeExt :: () => (SingI t) => Sing t -> Notes t -> Un.Ty
pattern AsUTypeExt sng notes <- AsUType notes@(notesSing -> sng)
  where AsUTypeExt _ notes = AsUType notes
{-# COMPLETE AsUTypeExt #-}