-- 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 :: Ty -> T
fromUType Ty
ut = Ty -> (forall (t :: T). SingI t => Notes t -> T) -> T
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ut (SingT t -> T
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing (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.Ty
mkUType :: Notes x -> Ty
mkUType Notes x
notes = (Sing x, Notes x) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Notes x -> Sing x
forall (t :: T). SingI t => Notes t -> Sing t
notesSing Notes x
notes, Notes x
notes)

mkUType' :: (Sing x, Notes x) -> Un.Ty
mkUType' :: (Sing x, Notes x) -> Ty
mkUType' = \case
  (Sing x
STInt, NTInt TypeAnn
tn)               -> T -> TypeAnn -> Ty
Un.Ty T
Un.TInt TypeAnn
tn
  (Sing x
STNat, NTNat TypeAnn
tn)               -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNat TypeAnn
tn
  (Sing x
STString, NTString TypeAnn
tn)         -> T -> TypeAnn -> Ty
Un.Ty T
Un.TString TypeAnn
tn
  (Sing x
STBytes, NTBytes TypeAnn
tn)           -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBytes TypeAnn
tn
  (Sing x
STMutez, NTMutez TypeAnn
tn)           -> T -> TypeAnn -> Ty
Un.Ty T
Un.TMutez TypeAnn
tn
  (Sing x
STBool, NTBool TypeAnn
tn)             -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBool TypeAnn
tn
  (Sing x
STKeyHash, NTKeyHash TypeAnn
tn)       -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKeyHash TypeAnn
tn
  (Sing x
STBls12381Fr, NTBls12381Fr TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381Fr TypeAnn
tn
  (Sing x
STBls12381G1, NTBls12381G1 TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G1 TypeAnn
tn
  (Sing x
STBls12381G2, NTBls12381G2 TypeAnn
tn) -> T -> TypeAnn -> Ty
Un.Ty T
Un.TBls12381G2 TypeAnn
tn
  (Sing x
STTimestamp, NTTimestamp TypeAnn
tn)   -> T -> TypeAnn -> Ty
Un.Ty T
Un.TTimestamp TypeAnn
tn
  (Sing x
STAddress, NTAddress TypeAnn
tn)       -> T -> TypeAnn -> Ty
Un.Ty T
Un.TAddress TypeAnn
tn
  (Sing x
STKey, NTKey TypeAnn
tn)               -> T -> TypeAnn -> Ty
Un.Ty T
Un.TKey TypeAnn
tn
  (Sing x
STUnit, NTUnit TypeAnn
tn)             -> T -> TypeAnn -> Ty
Un.Ty T
Un.TUnit TypeAnn
tn
  (Sing x
STSignature, NTSignature TypeAnn
tn)   -> T -> TypeAnn -> Ty
Un.Ty T
Un.TSignature TypeAnn
tn
  (Sing x
STChainId, NTChainId TypeAnn
tn)       -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChainId TypeAnn
tn
  (STOption t, NTOption TypeAnn
tn Notes t
n)     -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TOption (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
  (STList t, NTList TypeAnn
tn Notes t
n)         -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TList (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
  (STSet t, NTSet TypeAnn
tn Notes t
n)           -> T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TSet (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
  (Sing x
STOperation, NTOperation TypeAnn
tn)   -> T -> TypeAnn -> Ty
Un.Ty T
Un.TOperation TypeAnn
tn
  (Sing x
STChest, NTChest TypeAnn
tn)           -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChest TypeAnn
tn
  (Sing x
STChestKey, NTChestKey TypeAnn
tn)     -> T -> TypeAnn -> Ty
Un.Ty T
Un.TChestKey TypeAnn
tn
  (Sing x
STNever, NTNever TypeAnn
tn)           -> T -> TypeAnn -> Ty
Un.Ty T
Un.TNever TypeAnn
tn
  (STContract t, NTContract TypeAnn
tn Notes t
n) ->
    T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TContract (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
  (STTicket t, NTTicket TypeAnn
tn Notes t
n) ->
      T -> TypeAnn -> Ty
Un.Ty (Ty -> T
Un.TTicket (Ty -> T) -> Ty -> T
forall a b. (a -> b) -> a -> b
$ (Sing t, Notes t) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing t
t, Notes t
n)) TypeAnn
tn
  (STPair t t', NTPair TypeAnn
tn FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr Notes p
nl Notes q
nr) ->
    T -> TypeAnn -> Ty
Un.Ty
    (FieldAnn -> FieldAnn -> VarAnn -> VarAnn -> Ty -> Ty -> T
Un.TPair FieldAnn
fl FieldAnn
fr VarAnn
vl VarAnn
vr
    ((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
nl))
    ((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nr)))
    TypeAnn
tn
  (STOr t t', NTOr TypeAnn
tn FieldAnn
fl FieldAnn
fr Notes p
nl Notes q
nr) ->
    T -> TypeAnn -> Ty
Un.Ty
    (FieldAnn -> FieldAnn -> Ty -> Ty -> T
Un.TOr FieldAnn
fl FieldAnn
fr
    ((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
nl))
    ((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nr)))
    TypeAnn
tn
  (STLambda t t', NTLambda TypeAnn
tn Notes p
np Notes q
nq) ->
    T -> TypeAnn -> Ty
Un.Ty
    (Ty -> Ty -> T
Un.TLambda
    ((Sing p, Notes p) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing p
t, Notes p
np))
    ((Sing q, Notes q) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing q
t', Notes q
nq)))
    TypeAnn
tn
  (STMap t t', NTMap TypeAnn
tn Notes k
nk Notes v
nv) ->
    T -> TypeAnn -> Ty
Un.Ty
    (Ty -> Ty -> T
Un.TMap
    ((Sing k, Notes k) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing k
t, Notes k
nk))
    ((Sing v, Notes v) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing v
t', Notes v
nv)))
    TypeAnn
tn
  (STBigMap t t', NTBigMap TypeAnn
tn Notes k
nk Notes v
nv) ->
    T -> TypeAnn -> Ty
Un.Ty
    (Ty -> Ty -> T
Un.TBigMap
    ((Sing k, Notes k) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing k
t, Notes k
nk))
    ((Sing v, Notes v) -> Ty
forall (x :: T). (Sing x, Notes x) -> Ty
mkUType' (Sing n
Sing v
t', Notes v
nv)))
    TypeAnn
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 :: Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType (Un.Ty T
ut TypeAnn
tn) forall (t :: T). SingI t => Notes t -> r
cont = case T
ut of

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

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

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

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

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

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

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

  T
Un.TBls12381Fr ->
    Notes 'TBls12381Fr -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381Fr
NTBls12381Fr TypeAnn
tn)

  T
Un.TBls12381G1 ->
    Notes 'TBls12381G1 -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381G1
NTBls12381G1 TypeAnn
tn)

  T
Un.TBls12381G2 ->
    Notes 'TBls12381G2 -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TBls12381G2
NTBls12381G2 TypeAnn
tn)

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

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

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

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

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

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

  T
Un.TChest ->
    Notes 'TChest -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TChest
NTChest TypeAnn
tn)

  T
Un.TChestKey ->
    Notes 'TChestKey -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TChestKey
NTChestKey TypeAnn
tn)

  T
Un.TNever ->
    Notes 'TNever -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes 'TNever
NTNever TypeAnn
tn)

  Un.TOption Ty
internalT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
internalT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesInternalT :: Notes internalT) ->
      Notes ('TOption t) -> r
forall (t :: T). SingI 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 Ty
listT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
listT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesListT :: Notes listT) ->
      Notes ('TList t) -> r
forall (t :: T). SingI 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 Ty
setT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
setT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesSetT :: Notes setT) ->
      Notes ('TSet t) -> r
forall (t :: T). SingI 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)

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

  Un.TContract Ty
contractT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
contractT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesContractT :: Notes contractT) ->
      Notes ('TContract t) -> r
forall (t :: T). SingI 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.TTicket Ty
ticketT -> Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ticketT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$
    \(Notes t
notesTicketT :: Notes ticketT) ->
      Notes ('TTicket t) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Notes t -> Notes ('TTicket t)
forall (t :: T). TypeAnn -> Notes t -> Notes ('TTicket t)
NTTicket TypeAnn
tn Notes t
notesTicketT)

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

  Un.TOr FieldAnn
la FieldAnn
ra Ty
lt Ty
rt ->
    Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
lt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
ln ->
      Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
rt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
rn ->
        Notes ('TOr t t) -> r
forall (t :: T). SingI 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 Ty
lt Ty
rt ->
    Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
lt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
ln ->
      Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
rt ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
rn ->
        Notes ('TLambda t t) -> r
forall (t :: T). SingI 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 Ty
keyT Ty
valT ->
    Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
keyT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
keyN ->
      Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
valT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
valN ->
        Notes ('TMap t t) -> r
forall (t :: T). SingI 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 Ty
keyT Ty
valT ->
    Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
keyT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
keyN ->
      Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
valT ((forall (t :: T). SingI t => Notes t -> r) -> r)
-> (forall (t :: T). SingI t => Notes t -> r) -> r
forall a b. (a -> b) -> a -> b
$ \Notes t
valN ->
        Notes ('TBigMap t t) -> r
forall (t :: T). SingI 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. 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 $bAsUType :: Notes t -> Ty
$mAsUType :: forall r.
Ty
-> (forall (t :: T). SingI t => Notes t -> r) -> (Void# -> r) -> r
AsUType notes <- ((\ut -> withUType ut SomeTypedInfo) -> SomeTypedInfo notes)
  where AsUType Notes t
notes = Notes t -> Ty
forall (x :: T). SingI x => Notes x -> Ty
mkUType Notes t
notes
{-# COMPLETE AsUType #-}

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