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

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

  , pattern AsUType
  , pattern AsUTypeExt
  ) where

import Data.Singletons (Sing, SingI)

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

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

fromUType :: Un.Type -> T
fromUType ut = withUType ut (fromSingT . notesSing)

mkUType :: SingI x => Notes x -> Un.Type
mkUType notes = case (notesSing notes, notes) of
  (STInt, NTInt tn)               -> Un.Type Un.TInt tn
  (STNat, NTNat tn)               -> Un.Type Un.TNat tn
  (STString, NTString tn)         -> Un.Type Un.TString tn
  (STBytes, NTBytes tn)           -> Un.Type Un.TBytes tn
  (STMutez, NTMutez tn)           -> Un.Type Un.TMutez tn
  (STBool, NTBool tn)             -> Un.Type Un.TBool tn
  (STKeyHash, NTKeyHash tn)       -> Un.Type Un.TKeyHash tn
  (STTimestamp, NTTimestamp tn)   -> Un.Type Un.TTimestamp tn
  (STAddress, NTAddress tn)       -> Un.Type Un.TAddress tn
  (STKey, NTKey tn)               -> Un.Type Un.TKey tn
  (STUnit, NTUnit tn)             -> Un.Type Un.TUnit tn
  (STSignature, NTSignature tn)   -> Un.Type Un.TSignature tn
  (STChainId, NTChainId tn)       -> Un.Type Un.TChainId tn
  (STOption _, NTOption tn n)     -> Un.Type (Un.TOption (mkUType n)) tn
  (STList _, NTList tn n)         -> Un.Type (Un.TList (mkUType n)) tn
  (STSet _, NTSet tn n)           -> Un.Type (Un.TSet (mkUType n)) tn
  (STOperation, NTOperation tn)   -> Un.Type Un.TOperation tn
  (STContract _, NTContract tn n) ->
    Un.Type (Un.TContract (mkUType n)) tn
  (STPair _ _, NTPair tn fl fr nl nr) ->
    Un.Type (Un.TPair fl fr (mkUType nl) (mkUType nr)) tn
  (STOr _ _, NTOr tn fl fr nl nr) ->
    Un.Type (Un.TOr fl fr (mkUType nl) (mkUType nr)) tn
  (STLambda _ _, NTLambda tn np nq) ->
    Un.Type (Un.TLambda (mkUType np) (mkUType nq)) tn
  (STMap _ _, NTMap tn nk nv) ->
    Un.Type (Un.TMap (mkUType nk) (mkUType nv)) tn
  (STBigMap _ _, NTBigMap tn nk nv) ->
    Un.Type (Un.TBigMap (mkUType nk) (mkUType nv)) tn

-- | Convert 'Un.Type' to the isomorphic set of information from typed world.
withUType
  :: Un.Type
  -> (forall t. KnownT t => Notes t -> r)
  -> r
withUType (Un.Type 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.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.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.TPair la ra lt rt ->
    withUType lt $ \ln ->
      withUType rt $ \rn ->
        cont (NTPair tn la ra 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. KnownT t => SomeTypedInfo (Notes t)

-- | Transparently represent untyped 'Type' 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 :: () => (KnownT t) => Notes t -> Un.Type
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 :: () => (KnownT t) => Sing t -> Notes t -> Un.Type
pattern AsUTypeExt sng notes <- AsUType notes@(notesSing -> sng)
  where AsUTypeExt _ notes = AsUType notes
{-# COMPLETE AsUTypeExt #-}