-- 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 :: Type -> T
fromUType ut :: Type
ut = Type -> (forall (t :: T). KnownT t => Notes t -> T) -> T
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
ut (SingT t -> T
forall (a :: T). Sing a -> T
fromSingT (SingT t -> T) -> (Notes t -> SingT t) -> Notes t -> T
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notes t -> SingT t
forall (t :: T). SingI t => Notes t -> Sing t
notesSing)

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

  Un.TInt ->
    Notes 'TInt -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TInt
NTInt TypeAnn
tn)

  Un.TNat ->
    Notes 'TNat -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TNat
NTNat TypeAnn
tn)

  Un.TString ->
    Notes 'TString -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TString
NTString TypeAnn
tn)

  Un.TBytes ->
    Notes 'TBytes -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TBytes
NTBytes TypeAnn
tn)

  Un.TMutez ->
    Notes 'TMutez -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TMutez
NTMutez TypeAnn
tn)

  Un.TBool ->
    Notes 'TBool -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TBool
NTBool TypeAnn
tn)

  Un.TKeyHash ->
    Notes 'TKeyHash -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TKeyHash
NTKeyHash TypeAnn
tn)

  Un.TTimestamp ->
    Notes 'TTimestamp -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TTimestamp
NTTimestamp TypeAnn
tn)

  Un.TAddress ->
    Notes 'TAddress -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TAddress
NTAddress TypeAnn
tn)

  Un.TKey ->
    Notes 'TKey -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TKey
NTKey TypeAnn
tn)

  Un.TUnit ->
    Notes 'TUnit -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TUnit
NTUnit TypeAnn
tn)

  Un.TSignature ->
    Notes 'TSignature -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TSignature
NTSignature TypeAnn
tn)

  Un.TChainId ->
    Notes 'TChainId -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TChainId
NTChainId TypeAnn
tn)

  Un.TOption internalT :: Type
internalT -> Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
internalT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesInternalT :: Notes internalT) ->
      Notes ('TOption t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TOption t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TOption t)
NTOption TypeAnn
tn Notes t
notesInternalT)

  Un.TList listT :: Type
listT -> Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
listT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesListT :: Notes listT) ->
      Notes ('TList t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TList t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TList t)
NTList TypeAnn
tn Notes t
notesListT)

  Un.TSet setT :: Type
setT -> Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
setT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesSetT :: Notes setT) ->
      Notes ('TSet t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TSet t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TSet t)
NTSet TypeAnn
tn Notes t
notesSetT)

  Un.TOperation ->
    Notes 'TOperation -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes 'TOperation
NTOperation TypeAnn
tn)

  Un.TContract contractT :: Type
contractT -> Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
contractT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesContractT :: Notes contractT) ->
      Notes ('TContract t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TContract t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TContract t)
NTContract TypeAnn
tn Notes t
notesContractT)

  Un.TPair la :: FieldAnn
la ra :: FieldAnn
ra lt :: Type
lt rt :: Type
rt ->
    Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
lt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \ln :: Notes t
ln ->
      Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
rt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \rn :: Notes t
rn ->
        Notes ('TPair t t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes t -> Notes ('TPair t t)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TPair p p)
NTPair TypeAnn
tn FieldAnn
la FieldAnn
ra Notes t
ln Notes t
rn)

  Un.TOr la :: FieldAnn
la ra :: FieldAnn
ra lt :: Type
lt rt :: Type
rt ->
    Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
lt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \ln :: Notes t
ln ->
      Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
rt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \rn :: Notes t
rn ->
        Notes ('TOr t t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes t -> Notes ('TOr t t)
forall (p :: T) (p :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes p -> Notes ('TOr p p)
NTOr TypeAnn
tn FieldAnn
la FieldAnn
ra Notes t
ln Notes t
rn)

  Un.TLambda lt :: Type
lt rt :: Type
rt ->
    Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
lt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \ln :: Notes t
ln ->
      Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
rt ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \rn :: Notes t
rn ->
        Notes ('TLambda t t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes t -> Notes ('TLambda t t)
forall (p :: T) (k :: T).
TypeAnn -> Notes p -> Notes k -> Notes ('TLambda p k)
NTLambda TypeAnn
tn Notes t
ln Notes t
rn)

  Un.TMap keyT :: Type
keyT valT :: Type
valT ->
    Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
keyT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \keyN :: Notes t
keyN ->
      Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
valT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \valN :: Notes t
valN ->
        Notes ('TMap t t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont @('TMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TMap t t)
forall (k :: T) (k :: T).
TypeAnn -> Notes k -> Notes k -> Notes ('TMap k k)
NTMap TypeAnn
tn Notes t
keyN Notes t
valN)

  Un.TBigMap keyT :: Type
keyT valT :: Type
valT ->
    Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
keyT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \keyN :: Notes t
keyN ->
      Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall r. Type -> (forall (t :: T). KnownT t => Notes t -> r) -> r
withUType Type
valT ((forall (t :: T). KnownT t => Notes t -> r) -> r)
-> (forall (t :: T). KnownT t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \valN :: Notes t
valN ->
        Notes ('TBigMap t t) -> r
forall (t :: T). KnownT t => Notes t -> r
cont @('TBigMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TBigMap t t)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TBigMap k v)
NTBigMap TypeAnn
tn Notes t
keyN Notes t
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 $bAsUType :: Notes t -> Type
$mAsUType :: forall r.
Type
-> (forall (t :: T). KnownT t => Notes t -> r) -> (Void# -> r) -> r
AsUType notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo notes)
  where AsUType notes :: Notes t
notes = Notes t -> Type
forall (x :: T). SingI x => Notes x -> Type
mkUType Notes t
notes
{-# COMPLETE AsUType #-}

-- | Similar to 'AsUType', but also gives 'Sing' for given type.
pattern AsUTypeExt :: () => (KnownT t) => Sing t -> Notes t -> Un.Type
pattern $bAsUTypeExt :: Sing t -> Notes t -> Type
$mAsUTypeExt :: forall r.
Type
-> (forall (t :: T). KnownT t => Sing t -> Notes t -> r)
-> (Void# -> r)
-> r
AsUTypeExt sng notes <- AsUType notes@(notesSing -> sng)
  where AsUTypeExt _ notes :: Notes t
notes = Notes t -> Type
forall (t :: T). KnownT t => Notes t -> Type
AsUType Notes t
notes
{-# COMPLETE AsUTypeExt #-}