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

{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | Lorentz wrappers over instructions from Morley extension.
module Lorentz.Ext
  ( stackRef
  , printComment
  , testAssert
  , stackType
  ) where

import Data.Singletons (SingI)
import GHC.TypeNats (Nat)

import Lorentz.Base
import Michelson.Typed.Haskell
import Michelson.Typed.Instr
import Util.Peano hiding (Nat)

-- | Include a value at given position on stack into comment produced
-- by 'printComment'.
--
-- >>> stackRef @0
-- <includes the top of the stack>
stackRef
  :: forall (gn :: Nat) st n.
      (n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n)
  => PrintComment st
stackRef :: PrintComment st
stackRef = [Either Text (StackRef st)] -> PrintComment st
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
PrintComment ([Either Text (StackRef st)] -> PrintComment st)
-> (StackRef st -> [Either Text (StackRef st)])
-> StackRef st
-> PrintComment st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (StackRef st) -> [Either Text (StackRef st)]
forall x. One x => OneItem x -> x
one (Either Text (StackRef st) -> [Either Text (StackRef st)])
-> (StackRef st -> Either Text (StackRef st))
-> StackRef st
-> [Either Text (StackRef st)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackRef st -> Either Text (StackRef st)
forall a b. b -> Either a b
Right (StackRef st -> PrintComment st) -> StackRef st -> PrintComment st
forall a b. (a -> b) -> a -> b
$ forall (st :: [T]) (n :: Peano).
(n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n) =>
StackRef st
forall (gn :: Nat) (st :: [T]) (n :: Peano).
(n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n) =>
StackRef st
mkStackRef @gn

-- | Print a comment. It will be visible in tests.
--
-- >>> printComment "Hello world!"
-- >>> printComment $ "On top of the stack I see " <> stackRef @0
printComment :: PrintComment (ToTs s) -> s :-> s
printComment :: PrintComment (ToTs s) -> s :-> s
printComment = Instr (ToTs s) (ToTs s) -> s :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs s) (ToTs s) -> s :-> s)
-> (PrintComment (ToTs s) -> Instr (ToTs s) (ToTs s))
-> PrintComment (ToTs s)
-> s :-> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr (ToTs s) -> Instr (ToTs s) (ToTs s)
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr (ToTs s) -> Instr (ToTs s) (ToTs s))
-> (PrintComment (ToTs s) -> ExtInstr (ToTs s))
-> PrintComment (ToTs s)
-> Instr (ToTs s) (ToTs s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrintComment (ToTs s) -> ExtInstr (ToTs s)
forall (s :: [T]). PrintComment s -> ExtInstr s
PRINT

-- | Test an invariant, fail if it does not hold.
--
-- This won't be included into production contract and is executed only in tests.
testAssert
  :: (Typeable (ToTs out), HasCallStack)
  => Text -> PrintComment (ToTs inp) -> inp :-> Bool : out -> inp :-> inp
testAssert :: Text
-> PrintComment (ToTs inp) -> (inp :-> (Bool : out)) -> inp :-> inp
testAssert Text
msg PrintComment (ToTs inp)
comment = \case
  I Instr (ToTs inp) (ToTs (Bool : out))
instr -> Instr (ToTs inp) (ToTs inp) -> inp :-> inp
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I (Instr (ToTs inp) (ToTs inp) -> inp :-> inp)
-> (TestAssert (ToTs inp) -> Instr (ToTs inp) (ToTs inp))
-> TestAssert (ToTs inp)
-> inp :-> inp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtInstr (ToTs inp) -> Instr (ToTs inp) (ToTs inp)
forall (inp :: [T]). ExtInstr inp -> Instr inp inp
Ext (ExtInstr (ToTs inp) -> Instr (ToTs inp) (ToTs inp))
-> (TestAssert (ToTs inp) -> ExtInstr (ToTs inp))
-> TestAssert (ToTs inp)
-> Instr (ToTs inp) (ToTs inp)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestAssert (ToTs inp) -> ExtInstr (ToTs inp)
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert (ToTs inp) -> inp :-> inp)
-> TestAssert (ToTs inp) -> inp :-> inp
forall a b. (a -> b) -> a -> b
$ Text
-> PrintComment (ToTs inp)
-> Instr (ToTs inp) ('TBool : ToTs out)
-> TestAssert (ToTs inp)
forall (out :: [T]) (s :: [T]).
Typeable out =>
Text -> PrintComment s -> Instr s ('TBool : out) -> TestAssert s
TestAssert Text
msg PrintComment (ToTs inp)
comment Instr (ToTs inp) ('TBool : ToTs out)
Instr (ToTs inp) (ToTs (Bool : out))
instr
  FI forall (out' :: [T]). Instr (ToTs inp) out'
_ -> Text -> inp :-> inp
forall a. HasCallStack => Text -> a
error Text
"test assert branch always fails"

-- | Fix the current type of the stack to be given one.
--
-- >>> stackType @'[Natural]
-- >>> stackType @(Integer : Natural : s)
-- >>> stackType @'["balance" :! Integer, "toSpend" :! Integer, BigMap Address Integer]
--
-- Note that you can omit arbitrary parts of the type.
--
-- >>> stackType @'["balance" :! Integer, "toSpend" :! _, BigMap _ _]
stackType :: forall s. s :-> s
stackType :: s :-> s
stackType = Instr (ToTs s) (ToTs s) -> s :-> s
forall (inp :: [*]) (out :: [*]).
Instr (ToTs inp) (ToTs out) -> inp :-> out
I Instr (ToTs s) (ToTs s)
forall (inp :: [T]). Instr inp inp
Nop

_sample1 :: s ~ (a : s') => s :-> s
_sample1 :: s :-> s
_sample1 = PrintComment (ToTs s) -> s :-> s
forall (s :: [*]). PrintComment (ToTs s) -> s :-> s
printComment (PrintComment (ToTs s) -> s :-> s)
-> PrintComment (ToTs s) -> s :-> s
forall a b. (a -> b) -> a -> b
$ PrintComment (ToT a : ToTs s')
"Head is " PrintComment (ToT a : ToTs s')
-> PrintComment (ToT a : ToTs s') -> PrintComment (ToT a : ToTs s')
forall a. Semigroup a => a -> a -> a
<> forall (st :: [T]) (n :: Peano).
(n ~ ToPeano 0, SingI n, KnownPeano n, RequireLongerThan st n) =>
PrintComment st
forall (gn :: Nat) (st :: [T]) (n :: Peano).
(n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n) =>
PrintComment st
stackRef @0

_sample2 :: Integer : Natural : s :-> Integer : Natural : s
_sample2 :: (Integer : Natural : s) :-> (Integer : Natural : s)
_sample2 = (Integer : Natural : s) :-> (Integer : Natural : s)
forall (s :: [*]). s :-> s
stackType @(Integer : _)