-- | 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
  ) where

import Data.Singletons (SingI, sing)

import Michelson.Typed.Annotation (Notes(..))
import Michelson.Typed.Sing (Sing(..), fromSingCT, fromSingT, withSomeSingCT)
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 . fst)

mkUType :: Sing x -> Notes x -> Un.Type
mkUType s notes = case (s, notes) of
  (STc ct, NTc tn)              -> Un.Type (Un.Tc (fromSingCT ct)) 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 t, NTOption tn n)   -> Un.Type (Un.TOption (mkUType t n)) tn
  (STList t, NTList tn n)       -> Un.Type (Un.TList (mkUType t n)) tn
  (STSet ct, NTSet tn n)        -> Un.Type (Un.TSet $ mkComp ct n) tn
  (STOperation, NTOperation tn) -> Un.Type Un.TOperation tn
  (STContract t, NTContract tn n) ->
    Un.Type (Un.TContract (mkUType t n)) tn
  (STPair tl tr, NTPair tn fl fr nl nr) ->
    Un.Type (Un.TPair fl fr (mkUType tl nl) (mkUType tr nr)) tn
  (STOr tl tr, NTOr tn fl fr nl nr) ->
    Un.Type (Un.TOr fl fr (mkUType tl nl) (mkUType tr nr)) tn
  (STLambda p q, NTLambda tn np nq) ->
    Un.Type (Un.TLambda (mkUType p np) (mkUType q nq)) tn
  (STMap k v, NTMap tn nk nv) ->
    Un.Type (Un.TMap (mkComp k nk) (mkUType v nv)) tn
  (STBigMap k v, NTBigMap tn nk nv) ->
    Un.Type (Un.TBigMap (mkComp k nk) (mkUType v nv)) tn
 where
  mkComp t a = Un.Comparable (fromSingCT t) a

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

  Un.Tc tc -> withSomeSingCT tc $
    \(_ :: Sing tc) -> cont (sing @('Tc tc), NTc tn)

  Un.TKey ->
    cont (sing @'TKey, NTKey tn)

  Un.TUnit ->
    cont (sing @'TUnit, NTUnit tn)

  Un.TSignature ->
    cont (sing @'TSignature, NTSignature tn)

  Un.TChainId ->
    cont (sing @'TChainId, NTChainId tn)

  Un.TOption internalT -> withUType internalT $
    \(_ :: Sing internalT, notesInternalT :: Notes internalT) ->
      cont (sing @('TOption internalT), NTOption tn notesInternalT)

  Un.TList listT -> withUType listT $
    \(_ :: Sing listT, notesListT :: Notes listT) ->
      cont (sing @('TList listT), NTList tn notesListT)

  Un.TSet (Un.Comparable sCT nsCT) -> withSomeSingCT sCT $
    \(_ :: Sing sCT) -> cont (sing @('TSet sCT), NTSet tn nsCT)

  Un.TOperation ->
    cont (sing @'TOperation, NTOperation tn)

  Un.TContract contractT -> withUType contractT $
    \(_ :: Sing contractT, notesContractT :: Notes contractT) ->
      cont (sing @('TContract contractT), NTContract tn notesContractT)

  Un.TPair la ra lt rt ->
    withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
      withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
        cont (sing @('TPair lt rt), NTPair tn la ra ln rn)

  Un.TOr la ra lt rt ->
    withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
      withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
        cont (sing @('TOr lt rt), NTOr tn la ra ln rn)

  Un.TLambda lt rt ->
    withUType lt $ \(_ :: Sing lt, ln :: Notes lt) ->
      withUType rt $ \(_ :: Sing rt, rn :: Notes rt) ->
        cont (sing @('TLambda lt rt), NTLambda tn ln rn)

  Un.TMap (Un.Comparable keyT notesT) valT ->
    withSomeSingCT keyT $ \(_ :: Sing keyT) ->
      withUType valT $ \(_ :: Sing valT, valN :: Notes valt) ->
        cont (sing @('TMap keyT valT), NTMap tn notesT valN)

  Un.TBigMap (Un.Comparable keyT notesT) valT ->
    withSomeSingCT keyT $ \(_ :: Sing keyT) ->
      withUType valT $ \(_ :: Sing valT, valN :: Notes valt) ->
        cont (sing @('TBigMap keyT valT), NTBigMap tn notesT valN)

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

-- | Transparently represent untyped 'Type' as wrapper over @(Sing t, Notes t)@
-- from typed world.
--
-- 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 :: () => (Typeable t, SingI t) => Sing t -> Notes t -> Un.Type
pattern AsUType sng notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo (sng, notes))
  where AsUType sng notes = mkUType sng notes
{-# COMPLETE AsUType #-}