-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# OPTIONS_GHC -Wno-orphans #-}

-- | Support for uninhabited type.
--
-- Currently they are not supported my Michelson, so we provide
-- a sort of replacement.
--
-- This module should be removed once the proposal is implemented:
-- https://gitlab.com/tezos/tezos/issues/662
module Lorentz.Empty
  ( Empty
  , absurd_
  ) where

import Fmt (Buildable(..))

import Lorentz.Annotation (HasAnnotation)
import Lorentz.Base
import Lorentz.Doc
import Lorentz.Errors
import Lorentz.Value
import Michelson.Typed.Haskell.Doc

-- | Replacement for uninhabited type.
newtype Empty = Empty ()
  deriving stock (forall x. Empty -> Rep Empty x)
-> (forall x. Rep Empty x -> Empty) -> Generic Empty
forall x. Rep Empty x -> Empty
forall x. Empty -> Rep Empty x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Empty x -> Empty
$cfrom :: forall x. Empty -> Rep Empty x
Generic
  deriving anyclass (WellTypedToT Empty
WellTypedToT Empty =>
(Empty -> Value (ToT Empty))
-> (Value (ToT Empty) -> Empty) -> IsoValue Empty
Value (ToT Empty) -> Empty
Empty -> Value (ToT Empty)
forall a.
WellTypedToT a =>
(a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT Empty) -> Empty
$cfromVal :: Value (ToT Empty) -> Empty
toVal :: Empty -> Value (ToT Empty)
$ctoVal :: Empty -> Value (ToT Empty)
$cp1IsoValue :: WellTypedToT Empty
IsoValue, FollowEntrypointFlag -> Notes (ToT Empty)
(FollowEntrypointFlag -> Notes (ToT Empty)) -> HasAnnotation Empty
forall a.
(FollowEntrypointFlag -> Notes (ToT a)) -> HasAnnotation a
getAnnotation :: FollowEntrypointFlag -> Notes (ToT Empty)
$cgetAnnotation :: FollowEntrypointFlag -> Notes (ToT Empty)
HasAnnotation)

instance TypeHasDoc Empty where
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    "Type which should never be constructed.\n\n\
    \If appears as part of entrypoint argument, this means that the entrypoint \
    \should never be called."

-- | Someone constructed 'Empty' type.
type instance ErrorArg "emptySupplied" = ()

instance Buildable (CustomError "emptySupplied") where
  build :: CustomError "emptySupplied" -> Markdown
build (CustomError _ ()) =
    "'Empty' value was passed to the contract."

instance CustomErrorHasDoc "emptySupplied" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    "Value of type " Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Proxy Empty -> WithinParens -> Markdown
forall a. TypeHasDoc a => Proxy a -> WithinParens -> Markdown
typeDocMdReference (Proxy Empty
forall k (t :: k). Proxy t
Proxy @Empty) (Bool -> WithinParens
WithinParens Bool
False)
    Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> " has been supplied."

-- | Witness of that this code is unreachable.
absurd_ :: Empty : s :-> s'
absurd_ :: (Empty : s) :-> s'
absurd_ =
  Label "emptySupplied" -> (Empty : s) :-> s'
forall (tag :: Symbol) (s :: [*]) (any :: [*])
       (notVoidErrorMsg :: ErrorMessage).
(RequireNoArgError tag notVoidErrorMsg, CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustom_ IsLabel "emptySupplied" (Label "emptySupplied")
Label "emptySupplied"
#emptySupplied ((Empty : s) :-> s') -> (s' :-> s') -> (Empty : s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  DDescription -> s' :-> s'
forall di (s :: [*]). DocItem di => di -> s :-> s
doc (Markdown -> DDescription
DDescription "Should never be called")