module Lorentz.ViewBase
( ViewTyInfo(..)
, type (?::)
, type (>->)
, ViewsList
, RevealViews
, LookupView
, LookupRevealView
, HasView
, ViewsNames
, ViewName (..)
, ViewInterface (..)
, demoteViewName
, demoteViewTyInfos
, DemoteViewsDescriptor
, demoteViewsDescriptor
, ViewInterfaceMatchError (..)
, checkViewsCoverInterface
) where
import Control.Monad.Except (throwError)
import Data.Map qualified as Map
import Data.Singletons (demote)
import Fmt (Buildable(..), pretty, (+|), (|+))
import Morley.Michelson.Typed
import Morley.Util.MismatchError
import Morley.Util.TypeLits
data ViewTyInfo = ViewTyInfo Symbol Type Type
type family (?::) (name :: Symbol) (tys :: (Type, Type)) where
name ?:: '(arg, ret) = 'ViewTyInfo name arg ret
infix 3 ?::
type arg >-> ret = '(arg, ret)
infix 5 >->
type family RevealViews (desc :: Type) :: [ViewTyInfo]
data ViewsList (vl :: [ViewTyInfo])
type instance RevealViews () = '[]
type instance RevealViews (ViewsList info) = info
type family LookupView (name :: Symbol) (views :: [ViewTyInfo]) :: (Type, Type) where
LookupView name '[] =
TypeError ('Text "View " ':<>: 'ShowType name ':<>: 'Text " is not found")
LookupView name ('ViewTyInfo name arg ret ': _) = '(arg, ret)
LookupView name ('ViewTyInfo _ _ _ ': vs) = LookupView name vs
type LookupRevealView name viewRef = LookupView name (RevealViews viewRef)
type HasView vd name arg ret = (LookupRevealView name vd ~ '(arg, ret))
type family ViewsNames (vs :: [ViewTyInfo]) :: [Symbol] where
ViewsNames '[] = '[]
ViewsNames ('ViewTyInfo name _ _ ': vs) = name ': ViewsNames vs
demoteViewName
:: forall name.
(KnownSymbol name, HasCallStack)
=> ViewName
demoteViewName :: forall (name :: Symbol).
(KnownSymbol name, HasCallStack) =>
ViewName
demoteViewName = Either BadViewNameError ViewName -> ViewName
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either BadViewNameError ViewName -> ViewName)
-> (Text -> Either BadViewNameError ViewName) -> Text -> ViewName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either BadViewNameError ViewName
mkViewName (Text -> ViewName) -> Text -> ViewName
forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @name
data ViewInterface = ViewInterface
{ ViewInterface -> ViewName
viName :: ViewName
, ViewInterface -> T
viArg :: T
, ViewInterface -> T
viRet :: T
}
class DemoteViewTyInfo (vs :: [ViewTyInfo]) where
demoteViewTyInfos' :: Proxy vs -> [ViewInterface]
instance DemoteViewTyInfo '[] where
demoteViewTyInfos' :: Proxy '[] -> [ViewInterface]
demoteViewTyInfos' Proxy '[]
_ = []
instance (KnownSymbol name, IsoValue arg, IsoValue ret, DemoteViewTyInfo vs) =>
DemoteViewTyInfo ('ViewTyInfo name arg ret ': vs) where
demoteViewTyInfos' :: Proxy ('ViewTyInfo name arg ret : vs) -> [ViewInterface]
demoteViewTyInfos' Proxy ('ViewTyInfo name arg ret : vs)
_ =
ViewInterface :: ViewName -> T -> T -> ViewInterface
ViewInterface
{ viName :: ViewName
viName = forall (name :: Symbol).
(KnownSymbol name, HasCallStack) =>
ViewName
demoteViewName @name
, viArg :: T
viArg = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @(ToT arg)
, viRet :: T
viRet = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @(ToT ret)
} ViewInterface -> [ViewInterface] -> [ViewInterface]
forall a. a -> [a] -> [a]
: Proxy vs -> [ViewInterface]
forall (vs :: [ViewTyInfo]).
DemoteViewTyInfo vs =>
Proxy vs -> [ViewInterface]
demoteViewTyInfos' (forall {t :: [ViewTyInfo]}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs)
demoteViewTyInfos
:: forall (vs :: [ViewTyInfo]). DemoteViewTyInfo vs
=> [ViewInterface]
demoteViewTyInfos :: forall (vs :: [ViewTyInfo]). DemoteViewTyInfo vs => [ViewInterface]
demoteViewTyInfos = Proxy vs -> [ViewInterface]
forall (vs :: [ViewTyInfo]).
DemoteViewTyInfo vs =>
Proxy vs -> [ViewInterface]
demoteViewTyInfos' (forall {t :: [ViewTyInfo]}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @vs)
type DemoteViewsDescriptor vd = DemoteViewTyInfo (RevealViews vd)
demoteViewsDescriptor
:: forall (vd :: Type). DemoteViewTyInfo (RevealViews vd)
=> [ViewInterface]
demoteViewsDescriptor :: forall vd. DemoteViewTyInfo (RevealViews vd) => [ViewInterface]
demoteViewsDescriptor = forall (vs :: [ViewTyInfo]). DemoteViewTyInfo vs => [ViewInterface]
demoteViewTyInfos @(RevealViews vd)
data ViewInterfaceMatchError
= VIMViewNotFound ViewName
| VIMViewArgMismatch (MismatchError T)
| VIMViewRetMismatch (MismatchError T)
deriving stock (Int -> ViewInterfaceMatchError -> ShowS
[ViewInterfaceMatchError] -> ShowS
ViewInterfaceMatchError -> String
(Int -> ViewInterfaceMatchError -> ShowS)
-> (ViewInterfaceMatchError -> String)
-> ([ViewInterfaceMatchError] -> ShowS)
-> Show ViewInterfaceMatchError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ViewInterfaceMatchError] -> ShowS
$cshowList :: [ViewInterfaceMatchError] -> ShowS
show :: ViewInterfaceMatchError -> String
$cshow :: ViewInterfaceMatchError -> String
showsPrec :: Int -> ViewInterfaceMatchError -> ShowS
$cshowsPrec :: Int -> ViewInterfaceMatchError -> ShowS
Show, ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool
(ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool)
-> (ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool)
-> Eq ViewInterfaceMatchError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool
$c/= :: ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool
== :: ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool
$c== :: ViewInterfaceMatchError -> ViewInterfaceMatchError -> Bool
Eq)
instance Buildable ViewInterfaceMatchError where
build :: ViewInterfaceMatchError -> Doc
build = \case
VIMViewNotFound ViewName
name ->
Doc
"View not found in the contract " Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| ViewName
name ViewName -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""
VIMViewArgMismatch MismatchError T
merr ->
Doc
"View argument type mismatch.\n" Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| MismatchError T
merr MismatchError T -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""
VIMViewRetMismatch MismatchError T
merr ->
Doc
"View return type mismatch.\n" Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| MismatchError T
merr MismatchError T -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
""
instance Exception ViewInterfaceMatchError where
displayException :: ViewInterfaceMatchError -> String
displayException = ViewInterfaceMatchError -> String
forall a b. (Buildable a, FromDoc b) => a -> b
pretty
checkViewsCoverInterface
:: forall st. [ViewInterface] -> ViewsSet st -> Either ViewInterfaceMatchError ()
checkViewsCoverInterface :: forall (st :: T).
[ViewInterface] -> ViewsSet st -> Either ViewInterfaceMatchError ()
checkViewsCoverInterface [ViewInterface]
interfaces (ViewsList [SomeView' Instr st]
views) =
[ViewInterface]
-> (Element [ViewInterface] -> Either ViewInterfaceMatchError ())
-> Either ViewInterfaceMatchError ()
forall t (m :: * -> *) b.
(Container t, Monad m) =>
t -> (Element t -> m b) -> m ()
forM_ [ViewInterface]
interfaces ((Element [ViewInterface] -> Either ViewInterfaceMatchError ())
-> Either ViewInterfaceMatchError ())
-> (Element [ViewInterface] -> Either ViewInterfaceMatchError ())
-> Either ViewInterfaceMatchError ()
forall a b. (a -> b) -> a -> b
$ \ViewInterface{ViewName
T
viRet :: T
viArg :: T
viName :: ViewName
viRet :: ViewInterface -> T
viArg :: ViewInterface -> T
viName :: ViewInterface -> ViewName
..} -> do
() <- case ViewName
-> Map ViewName (SomeView' Instr st) -> Maybe (SomeView' Instr st)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ViewName
viName Map ViewName (SomeView' Instr st)
viewsMap of
Maybe (SomeView' Instr st)
Nothing -> ViewInterfaceMatchError -> Either ViewInterfaceMatchError ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ViewName -> ViewInterfaceMatchError
VIMViewNotFound ViewName
viName)
Just (SomeView View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg st ret
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
vCode :: ViewCode' Instr arg st ret
vReturn :: Notes ret
vArgument :: Notes arg
vName :: ViewName
..}) -> do
Bool
-> Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notes arg -> T
forall (t :: T). Notes t -> T
notesT Notes arg
vArgument T -> T -> Bool
forall a. Eq a => a -> a -> Bool
== T
viArg) (Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ())
-> Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ()
forall a b. (a -> b) -> a -> b
$
ViewInterfaceMatchError -> Either ViewInterfaceMatchError ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ViewInterfaceMatchError -> Either ViewInterfaceMatchError ())
-> ViewInterfaceMatchError -> Either ViewInterfaceMatchError ()
forall a b. (a -> b) -> a -> b
$ MismatchError T -> ViewInterfaceMatchError
VIMViewArgMismatch MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError
{ meExpected :: T
meExpected = T
viArg, meActual :: T
meActual = Notes arg -> T
forall (t :: T). Notes t -> T
notesT Notes arg
vArgument }
Bool
-> Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notes ret -> T
forall (t :: T). Notes t -> T
notesT Notes ret
vReturn T -> T -> Bool
forall a. Eq a => a -> a -> Bool
== T
viRet) (Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ())
-> Either ViewInterfaceMatchError ()
-> Either ViewInterfaceMatchError ()
forall a b. (a -> b) -> a -> b
$
ViewInterfaceMatchError -> Either ViewInterfaceMatchError ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (ViewInterfaceMatchError -> Either ViewInterfaceMatchError ())
-> ViewInterfaceMatchError -> Either ViewInterfaceMatchError ()
forall a b. (a -> b) -> a -> b
$ MismatchError T -> ViewInterfaceMatchError
VIMViewRetMismatch MkMismatchError :: forall a. a -> a -> MismatchError a
MkMismatchError
{ meExpected :: T
meExpected = T
viRet, meActual :: T
meActual = Notes ret -> T
forall (t :: T). Notes t -> T
notesT Notes ret
vReturn }
Either ViewInterfaceMatchError ()
forall (f :: * -> *). Applicative f => f ()
pass
where
viewsMap :: Map.Map ViewName (SomeView st)
viewsMap :: Map ViewName (SomeView' Instr st)
viewsMap = [(ViewName, SomeView' Instr st)]
-> Map ViewName (SomeView' Instr st)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (ViewName
vName, SomeView' Instr st
v) | v :: SomeView' Instr st
v@(SomeView View{ViewName
Notes arg
Notes ret
ViewCode' Instr arg st ret
vCode :: ViewCode' Instr arg st ret
vReturn :: Notes ret
vArgument :: Notes arg
vName :: ViewName
vReturn :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes ret
vName :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewName
vCode :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> ViewCode' instr arg st ret
vArgument :: forall (instr :: [T] -> [T] -> *) (arg :: T) (st :: T) (ret :: T).
View' instr arg st ret -> Notes arg
..}) <- [SomeView' Instr st]
views ]