-- 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 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

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

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 msg :: Text
msg comment :: PrintComment (ToTs inp)
comment = \case
  I instr :: 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 _ -> Text -> inp :-> inp
forall a. HasCallStack => Text -> a
error "test assert branch always fails"

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
$ "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 & _)