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

-- | 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
  , toUType
  , withUType

  , pattern AsUType
  , pattern AsUTypeExt
  ) where

import Data.Singletons (Sing, SingI, SomeSing(..), fromSing, withSingI)

import Morley.Michelson.Typed.Annotation (Notes(..), mkUType, notesSing)
import Morley.Michelson.Typed.T (T(..), toUType)
import Morley.Michelson.Untyped qualified as Un
import Morley.Util.Peano qualified as Peano

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

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

-- | 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.TChest ->
    cont (NTChest tn)

  Un.TChestKey ->
    cont (NTChestKey tn)

  Un.TNever ->
    cont (NTNever tn)

  Un.TSaplingState n ->
    (\(SomeSing s) -> withSingI s $
      cont (NTSaplingState tn s)
    ) $ Peano.someSingNat n

  Un.TSaplingTransaction n ->
    (\(SomeSing s) -> withSingI s $
      cont (NTSaplingTransaction tn s)
    ) $ Peano.someSingNat n

  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 #-}