-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

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

-- | Type-level information about a view.
data ViewTyInfo = ViewTyInfo Symbol Type Type

-- | Neat constructor for 'ViewTyInfo'.
--
-- type View = "view" ?:: Integer >-> Natural
type family (?::) (name :: Symbol) (tys :: (Type, Type)) where
  name ?:: '(arg, ret) = 'ViewTyInfo name arg ret
infix 3 ?::

type arg >-> ret = '(arg, ret)
infix 5 >->

-- | Get a list of views by a descriptor object.
--
-- The problem this type family solves:
-- it is unpleasant to carry around a list of views because it may be large,
-- and if we merely hide this list under a type alias, error messages will still
-- mention the type alias expanded.
-- We want e.g. @Contract Parameter Storage Views@ to be carried as-is.
-- @Parameter@ and @Storage@ are usually datatypes and they are fine, while
-- for @Views@ to be not automatically expanded we have to take special care.
--
-- You can still provide the list of 'ViewTyInfo's to this type family using
-- t'ViewsList', but generally prefer creating a dedicated datatype that would
-- expand to a views list.
type family RevealViews (desc :: Type) :: [ViewTyInfo]

-- | A views descriptor that directly carries the full list of views.
data ViewsList (vl :: [ViewTyInfo])

type instance RevealViews () = '[]
type instance RevealViews (ViewsList info) = info

-- | Find a view in a contract by name.
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

-- | Reveal views and find a view there.
type LookupRevealView name viewRef = LookupView name (RevealViews viewRef)

-- | Constraint indicating that presence of the view with the specified
-- parameters is implied by the views descriptor.
type HasView vd name arg ret = (LookupRevealView name vd ~ '(arg, ret))

-- | Map views to get their names.
type family ViewsNames (vs :: [ViewTyInfo]) :: [Symbol] where
  ViewsNames '[] = '[]
  ViewsNames ('ViewTyInfo name _ _ ': vs) = name ': ViewsNames vs

-- | Demote view name from type level to term level.
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

-- | Interface of a single view at term-level.
data ViewInterface = ViewInterface
  { ViewInterface -> ViewName
viName :: ViewName
  , ViewInterface -> T
viArg :: T
  , ViewInterface -> T
viRet :: T
  }

-- | Helper typeclass to demote 'ViewTyInfo's to 'ViewInterface's.
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)

-- | Demote 'ViewTyInfo's to 'ViewInterface's.
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)

-- | Demote views descriptor to 'ViewInterface's.
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 -> Builder
build = \case
    VIMViewNotFound ViewName
name ->
      Builder
"View not found in the contract " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| ViewName
name ViewName -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    VIMViewArgMismatch MismatchError T
merr ->
      Builder
"View argument type mismatch.\n" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| MismatchError T
merr MismatchError T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""
    VIMViewRetMismatch MismatchError T
merr ->
      Builder
"View return type mismatch.\n" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| MismatchError T
merr MismatchError T -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""

instance Exception ViewInterfaceMatchError where
  displayException :: ViewInterfaceMatchError -> String
displayException = ViewInterfaceMatchError -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty

-- | Check that the given set of views covers the given view interfaces.
-- Extra views in the set, that do not appear in the interface, are fine.
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{T
ViewName
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{Notes arg
Notes ret
ViewCode' Instr arg st ret
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
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{Notes arg
Notes ret
ViewCode' Instr arg st ret
ViewName
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 ]