-- 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 :: 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). Notes t -> Sing t
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 :: forall r. 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)

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

  Un.TSaplingState Natural
n ->
    (\(SomeSing Sing a
s) -> Sing a -> (SingI a => r) -> r
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
s ((SingI a => r) -> r) -> (SingI a => r) -> r
forall a b. (a -> b) -> a -> b
$
      Notes ('TSaplingState a) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Sing a -> Notes ('TSaplingState a)
forall (n :: Peano). TypeAnn -> Sing n -> Notes ('TSaplingState n)
NTSaplingState TypeAnn
tn Sing a
s)
    ) (SomeSing Peano -> r) -> SomeSing Peano -> r
forall a b. (a -> b) -> a -> b
$ Natural -> SomeSing Peano
Peano.someSingNat Natural
n

  Un.TSaplingTransaction Natural
n ->
    (\(SomeSing Sing a
s) -> Sing a -> (SingI a => r) -> r
forall {k} (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
s ((SingI a => r) -> r) -> (SingI a => r) -> r
forall a b. (a -> b) -> a -> b
$
      Notes ('TSaplingTransaction a) -> r
forall (t :: T). SingI t => Notes t -> r
cont (TypeAnn -> Sing a -> Notes ('TSaplingTransaction a)
forall (n :: Peano).
TypeAnn -> Sing n -> Notes ('TSaplingTransaction n)
NTSaplingTransaction TypeAnn
tn Sing a
s)
    ) (SomeSing Peano -> r) -> SomeSing Peano -> r
forall a b. (a -> b) -> a -> b
$ Natural -> SomeSing Peano
Peano.someSingNat Natural
n

  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 (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TOption t1)
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 (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TList t1)
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 (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TSet t1)
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 (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TContract t1)
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 (t1 :: T). TypeAnn -> Notes t1 -> Notes ('TTicket t1)
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) (q :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
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) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
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) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
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 ->
        forall (t :: T). SingI t => Notes t -> r
cont @('TMap _ _) (TypeAnn -> Notes t -> Notes t -> Notes ('TMap t t)
forall (k :: T) (v :: T).
TypeAnn -> Notes k -> Notes v -> Notes ('TMap k v)
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 ->
        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 :: forall (t :: T). SingI t => Notes t -> Ty
$mAsUType :: forall {r}.
Ty
-> (forall {t :: T}. SingI t => Notes t -> r) -> (Void# -> r) -> r
AsUType notes <- ((\Ty
ut -> Ty
-> (forall (t :: T). SingI t => Notes t -> SomeTypedInfo)
-> SomeTypedInfo
forall r. Ty -> (forall (t :: T). SingI t => Notes t -> r) -> r
withUType Ty
ut forall (t :: T). SingI t => Notes t -> SomeTypedInfo
SomeTypedInfo) -> SomeTypedInfo notes)
  where AsUType Notes t
notes = Notes t -> Ty
forall (x :: T). 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 :: forall (t :: T). SingI t => 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 (t :: T). SingI t => Notes t -> Ty
AsUType Notes t
notes
{-# COMPLETE AsUTypeExt #-}