-- 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 = unsafe . mkViewName $ symbolValT' @name

-- | Interface of a single view at term-level.
data ViewInterface = ViewInterface
  { viName :: ViewName
  , viArg :: 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' _ = []
instance (KnownSymbol name, IsoValue arg, IsoValue ret, DemoteViewTyInfo vs) =>
         DemoteViewTyInfo ('ViewTyInfo name arg ret ': vs) where
  demoteViewTyInfos' _ =
    ViewInterface
    { viName = demoteViewName @name
    , viArg = demote @(ToT arg)
    , viRet = demote @(ToT ret)
    } : demoteViewTyInfos' (Proxy @vs)

-- | Demote 'ViewTyInfo's to 'ViewInterface's.
demoteViewTyInfos
  :: forall (vs :: [ViewTyInfo]). DemoteViewTyInfo vs
  => [ViewInterface]
demoteViewTyInfos = demoteViewTyInfos' (Proxy @vs)

type DemoteViewsDescriptor vd = DemoteViewTyInfo (RevealViews vd)

-- | Demote views descriptor to 'ViewInterface's.
demoteViewsDescriptor
  :: forall (vd :: Type). DemoteViewTyInfo (RevealViews vd)
  => [ViewInterface]
demoteViewsDescriptor = demoteViewTyInfos @(RevealViews vd)

data ViewInterfaceMatchError
  = VIMViewNotFound ViewName
  | VIMViewArgMismatch (MismatchError T)
  | VIMViewRetMismatch (MismatchError T)
  deriving stock (Show, Eq)

instance Buildable ViewInterfaceMatchError where
  build = \case
    VIMViewNotFound name ->
      "View not found in the contract " +| name |+ ""
    VIMViewArgMismatch merr ->
      "View argument type mismatch.\n" +| merr |+ ""
    VIMViewRetMismatch merr ->
      "View return type mismatch.\n" +| merr |+ ""

instance Exception ViewInterfaceMatchError where
  displayException = 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 interfaces (ViewsList views) =
  forM_ interfaces $ \ViewInterface{..} -> do
    () <- case Map.lookup viName viewsMap of
      Nothing -> throwError (VIMViewNotFound viName)
      Just (SomeView View{..}) -> do
        unless (notesT vArgument == viArg) $
          throwError $ VIMViewArgMismatch MkMismatchError
            { meExpected = viArg, meActual = notesT vArgument }
        unless (notesT vReturn == viRet) $
          throwError $ VIMViewRetMismatch MkMismatchError
            { meExpected = viRet, meActual = notesT vReturn }
    pass
  where
    viewsMap :: Map.Map ViewName (SomeView st)
    viewsMap = Map.fromList [ (vName, v) | v@(SomeView View{..}) <- views ]