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

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)

stackRef
  :: forall (gn :: Nat) st n.
      (n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n)
  => PrintComment st
stackRef = PrintComment . one . Right $ mkStackRef @gn

printComment :: PrintComment (ToTs s) -> s :-> s
printComment = I . Ext . PRINT

testAssert
  :: (Typeable (ToTs out), HasCallStack)
  => Text -> PrintComment (ToTs inp) -> inp :-> Bool & out -> inp :-> inp
testAssert msg comment = \case
  I instr -> I . Ext . TEST_ASSERT $ TestAssert msg comment instr
  FI _ -> error "test assert branch always fails"

stackType :: forall s. s :-> s
stackType = I Nop

_sample1 :: s ~ (a & s') => s :-> s
_sample1 = printComment $ "Head is " <> stackRef @0

_sample2 :: Integer & Natural & s :-> Integer & Natural & s
_sample2 = stackType @(Integer & _)