module Morley.Michelson.Typed.Instr
( Instr (..
, CAR
, CDR
, DUP
, DUPN
, PUSH
, SOME
, NONE
, UNIT
, PAIR
, UNPAIR
, PAIRN
, LEFT
, RIGHT
, NIL
, CONS
, SIZE
, EMPTY_SET
, EMPTY_MAP
, EMPTY_BIG_MAP
, MAP
, MEM
, GET
, GETN
, UPDATE
, UPDATEN
, GET_AND_UPDATE
, LAMBDA
, LAMBDA_REC
, EXEC
, APPLY
, CAST
, RENAME
, PACK
, UNPACK
, CONCAT
, CONCAT'
, SLICE
, ISNAT
, ADD
, SUB
, SUB_MUTEZ
, MUL
, EDIV
, ABS
, NEG
, LSL
, LSR
, OR
, AND
, XOR
, NOT
, COMPARE
, EQ
, NEQ
, LT
, GT
, LE
, GE
, INT
, VIEW
, SELF
, CONTRACT
, TRANSFER_TOKENS
, SET_DELEGATE
, CREATE_CONTRACT
, IMPLICIT_ACCOUNT
, NOW
, AMOUNT
, BALANCE
, VOTING_POWER
, TOTAL_VOTING_POWER
, CHECK_SIGNATURE
, SHA256
, SHA512
, BLAKE2B
, SHA3
, KECCAK
, HASH_KEY
, PAIRING_CHECK
, SOURCE
, SENDER
, ADDRESS
, CHAIN_ID
, LEVEL
, SELF_ADDRESS
, TICKET
, TICKET_DEPRECATED
, READ_TICKET
, SPLIT_TICKET
, JOIN_TICKETS
, OPEN_CHEST
, SAPLING_EMPTY_STATE
, SAPLING_VERIFY_UPDATE
, MIN_BLOCK_TIME
, EMIT
, BYTES
, NAT
)
, castInstr
, pattern (:#)
, ExtInstr (..)
, CommentType (..)
, StackRef (..)
, mkStackRef
, PrintComment (..)
, TestAssert (..)
, SomeMeta (..)
, pattern ConcreteMeta
, frameInstr
) where
import Prelude hiding (EQ, GT, LT)
import Data.Constraint ((\\))
import Data.Default (def)
import Data.List (stripPrefix)
import Data.Singletons (Sing)
import Data.Type.Equality ((:~:)(..))
import Data.Typeable (cast)
import Fmt (Buildable(..), (+|), (|+))
import GHC.TypeNats (Nat)
import Language.Haskell.TH
import Text.Show qualified as T
import Morley.Michelson.Doc
import Morley.Michelson.ErrorPos
import Morley.Michelson.Typed.Annotation (AnnVar, Anns, Notes(..))
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Instr.Constraints
import Morley.Michelson.Typed.Instr.Internal.Proofs
import Morley.Michelson.Typed.Polymorphic
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value (RemFail(..), Value'(..))
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped (AnyAnn, FieldAnn, StackTypePattern, TypeAnn, VarAnn)
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Sing (eqI)
import Morley.Util.TH
import Morley.Util.Type (type (++))
{-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-}
infixr 8 `Seq`
data Instr (inp :: [T]) (out :: [T]) where
WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b
Meta :: SomeMeta -> Instr a b -> Instr a b
Seq :: Instr a b -> Instr b c -> Instr a c
Nop :: Instr s s
Ext :: ExtInstr s -> Instr s s
Nested :: Instr inp out -> Instr inp out
DocGroup :: DocGrouping -> Instr inp out -> Instr inp out
AnnCAR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': s)
AnnCDR :: Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b ': s) (b ': s)
DROP :: Instr (a ': s) s
DROPN
:: forall (n :: Peano) s.
(RequireLongerOrSameLength s n)
=> PeanoNatural n -> Instr s (Drop n s)
AnnDUP :: DupableScope a => AnnVar -> Instr (a ': s) (a ': a ': s)
AnnDUPN
:: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a)
=> AnnVar -> PeanoNatural n -> Instr inp out
SWAP :: Instr (a ': b ': s) (b ': a ': s)
DIG
:: forall (n :: Peano) inp out a. (ConstraintDIG n inp out a)
=> PeanoNatural n -> Instr inp out
DUG
:: forall (n :: Peano) inp out a. (ConstraintDUG n inp out a)
=> PeanoNatural n -> Instr inp out
AnnPUSH
:: forall t s . ConstantScope t
=> Anns '[VarAnn, Notes t] -> Value' Instr t -> Instr s (t ': s)
AnnSOME :: Anns '[TypeAnn, VarAnn] -> Instr (a ': s) ('TOption a ': s)
AnnNONE :: forall a s . SingI a => Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a ': s)
AnnUNIT :: Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit ': s)
IF_NONE
:: Instr s s'
-> Instr (a ': s) s'
-> Instr ('TOption a ': s) s'
AnnPAIR :: Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn] -> Instr (a ': b ': s) ('TPair a b ': s)
AnnUNPAIR :: Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn] -> Instr ('TPair a b ': s) (a ': b ': s)
AnnPAIRN
:: forall n inp. ConstraintPairN n inp
=> AnnVar -> PeanoNatural n -> Instr inp (PairN n inp)
UNPAIRN
:: forall (n :: Peano) (pair :: T) (s :: [T]).
ConstraintUnpairN n pair
=> PeanoNatural n
-> Instr (pair : s) (UnpairN n pair ++ s)
AnnLEFT :: SingI b => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b] -> Instr (a ': s) ('TOr a b ': s)
AnnRIGHT :: SingI a => Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a] -> Instr (b ': s) ('TOr a b ': s)
IF_LEFT
:: Instr (a ': s) s'
-> Instr (b ': s) s'
-> Instr ('TOr a b ': s) s'
AnnNIL :: SingI p => Anns '[TypeAnn, VarAnn, Notes p] -> Instr s ('TList p ': s)
AnnCONS :: AnnVar -> Instr (a ': 'TList a ': s) ('TList a ': s)
IF_CONS
:: Instr (a ': 'TList a ': s) s'
-> Instr s s'
-> Instr ('TList a ': s) s'
AnnSIZE :: SizeOp c => AnnVar -> Instr (c ': s) ('TNat ': s)
AnnEMPTY_SET
:: Comparable e
=> Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
AnnEMPTY_MAP
:: (SingI b, Comparable a)
=> Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
AnnEMPTY_BIG_MAP
:: (SingI b, Comparable a, ForbidBigMap b)
=> Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TBigMap a b ': s)
AnnMAP :: (MapOp c, SingI b)
=> AnnVar
-> Instr (MapOpInp c ': s) (b ': s)
-> Instr (c ': s) (MapOpRes c b ': s)
ITER :: IterOp c => Instr (IterOpEl c ': s) s -> Instr (c ': s) s
AnnMEM :: MemOp c => AnnVar -> Instr (MemOpKey c ': c ': s) ('TBool ': s)
AnnGET
:: (GetOp c, SingI (GetOpVal c))
=> AnnVar -> Instr (GetOpKey c ': c ': s) ('TOption (GetOpVal c) ': s)
AnnGETN
:: forall (ix :: Peano) (pair :: T) (s :: [T]).
ConstraintGetN ix pair
=> AnnVar
-> PeanoNatural ix
-> Instr (pair : s) (GetN ix pair ': s)
AnnUPDATE
:: UpdOp c
=> AnnVar
-> Instr (UpdOpKey c ': UpdOpParams c ': c ': s) (c ': s)
AnnUPDATEN
:: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]).
ConstraintUpdateN ix pair
=> AnnVar
-> PeanoNatural ix
-> Instr (val : pair : s) (UpdateN ix val pair ': s)
AnnGET_AND_UPDATE
:: ( GetOp c, UpdOp c, SingI (GetOpVal c)
, UpdOpKey c ~ GetOpKey c
)
=> AnnVar
-> Instr (UpdOpKey c ': UpdOpParams c ': c ': s) ('TOption (GetOpVal c) : c ': s)
IF :: Instr s s'
-> Instr s s'
-> Instr ('TBool ': s) s'
LOOP :: Instr s ('TBool ': s)
-> Instr ('TBool ': s) s
LOOP_LEFT
:: Instr (a ': s) ('TOr a b ': s)
-> Instr ('TOr a b ': s) (b ': s)
AnnLAMBDA
:: forall i o s . (SingI i, SingI o)
=> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o]
-> Instr s ('TLambda i o ': s)
AnnLAMBDA_REC
:: forall i o s . (SingI i, SingI o)
=> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o ': s)
AnnEXEC :: AnnVar -> Instr (t1 ': 'TLambda t1 t2 ': s) (t2 ': s)
AnnAPPLY
:: forall a b c s . (ConstantScope a, SingI b)
=> AnnVar -> Instr (a ': 'TLambda ('TPair a b) c ': s) ('TLambda b c ': s)
DIP :: Instr a c -> Instr (b ': a) (b ': c)
DIPN
:: forall (n :: Peano) inp out s s'. (ConstraintDIPN n inp out s s')
=> PeanoNatural n -> Instr s s' -> Instr inp out
FAILWITH :: (SingI a, ConstantScope a) => Instr (a ': s) t
AnnCAST :: forall a s . SingI a => Anns '[VarAnn, Notes a] -> Instr (a ': s) (a ': s)
AnnRENAME :: AnnVar -> Instr (a ': s) (a ': s)
AnnPACK :: PackedValScope a => AnnVar -> Instr (a ': s) ('TBytes ': s)
AnnUNPACK
:: (UnpackedValScope a, SingI a)
=> Anns '[TypeAnn, VarAnn, Notes a]
-> Instr ('TBytes ': s) ('TOption a ': s)
AnnCONCAT :: ConcatOp c => AnnVar -> Instr (c ': c ': s) (c ': s)
AnnCONCAT' :: ConcatOp c => AnnVar -> Instr ('TList c ': s) (c ': s)
AnnSLICE
:: (SliceOp c, SingI c)
=> AnnVar
-> Instr ('TNat ': 'TNat ': c ': s) ('TOption c ': s)
AnnISNAT :: AnnVar -> Instr ('TInt ': s) ('TOption ('TNat) ': s)
AnnADD
:: ArithOp Add n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Add n m ': s)
AnnSUB
:: ArithOp Sub n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Sub n m ': s)
AnnSUB_MUTEZ :: AnnVar -> Instr ('TMutez ': 'TMutez ': s) ('TOption 'TMutez ': s)
AnnMUL
:: ArithOp Mul n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Mul n m ': s)
AnnEDIV
:: ArithOp EDiv n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes EDiv n m ': s)
AnnABS
:: UnaryArithOp Abs n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Abs n ': s)
AnnNEG
:: UnaryArithOp Neg n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Neg n ': s)
AnnLSL
:: ArithOp Lsl n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Lsl n m ': s)
AnnLSR
:: ArithOp Lsr n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Lsr n m ': s)
AnnOR
:: ArithOp Or n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Or n m ': s)
AnnAND
:: ArithOp And n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes And n m ': s)
AnnXOR
:: ArithOp Xor n m
=> AnnVar
-> Instr (n ': m ': s) (ArithRes Xor n m ': s)
AnnNOT
:: (SingI n, UnaryArithOp Not n)
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Not n ': s)
AnnCOMPARE
:: Comparable n
=> AnnVar
-> Instr (n ': n ': s) ('TInt ': s)
AnnEQ
:: UnaryArithOp Eq' n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Eq' n ': s)
AnnNEQ
:: UnaryArithOp Neq n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Neq n ': s)
AnnLT
:: UnaryArithOp Lt n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Lt n ': s)
AnnGT
:: UnaryArithOp Gt n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Gt n ': s)
AnnLE
:: UnaryArithOp Le n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Le n ': s)
AnnGE
:: UnaryArithOp Ge n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Ge n ': s)
AnnINT
:: ToIntArithOp n
=> AnnVar
-> Instr (n ': s) ('TInt ': s)
AnnBYTES
:: ToBytesArithOp n
=> AnnVar
-> Instr (n ': s) ('TBytes ': s)
AnnNAT
:: AnnVar
-> Instr ('TBytes ': s) ('TNat ': s)
AnnVIEW
:: (SingI arg, ViewableScope ret)
=> Anns '[VarAnn, Notes ret]
-> ViewName
-> Instr (arg ': 'TAddress ': s) ('TOption ret ': s)
AnnSELF
:: forall (arg :: T) s .
(ParameterScope arg, IsNotInView)
=> AnnVar
-> SomeEntrypointCallT arg
-> Instr s ('TContract arg ': s)
AnnCONTRACT
:: (ParameterScope p)
=> Anns '[VarAnn, Notes p]
-> EpName
-> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
AnnTRANSFER_TOKENS
:: (ParameterScope p, IsNotInView)
=> AnnVar
-> Instr (p ': 'TMutez ': 'TContract p ': s) ('TOperation ': s)
AnnSET_DELEGATE
:: IsNotInView
=> AnnVar
-> Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)
AnnCREATE_CONTRACT
:: (ParameterScope p, StorageScope g, IsNotInView)
=> Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr ('TOption 'TKeyHash ':
'TMutez ':
g ': s)
('TOperation ': 'TAddress ': s)
AnnIMPLICIT_ACCOUNT
:: AnnVar
-> Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
AnnNOW :: AnnVar -> Instr s ('TTimestamp ': s)
AnnAMOUNT :: AnnVar -> Instr s ('TMutez ': s)
AnnBALANCE :: AnnVar -> Instr s ('TMutez ': s)
AnnVOTING_POWER :: AnnVar -> Instr ('TKeyHash ': s) ('TNat ': s)
AnnTOTAL_VOTING_POWER :: AnnVar -> Instr s ('TNat ': s)
AnnCHECK_SIGNATURE
:: AnnVar
-> Instr ('TKey ': 'TSignature ': 'TBytes ': s) ('TBool ': s)
AnnSHA256 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
AnnSHA512 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
AnnBLAKE2B :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
AnnSHA3 :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
AnnKECCAK :: AnnVar -> Instr ('TBytes ': s) ('TBytes ': s)
AnnHASH_KEY :: AnnVar -> Instr ('TKey ': s) ('TKeyHash ': s)
AnnPAIRING_CHECK
:: AnnVar
-> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
AnnSOURCE :: AnnVar -> Instr s ('TAddress ': s)
AnnSENDER :: AnnVar -> Instr s ('TAddress ': s)
AnnADDRESS :: AnnVar -> Instr ('TContract a ': s) ('TAddress ': s)
AnnCHAIN_ID :: AnnVar -> Instr s ('TChainId ': s)
AnnLEVEL :: AnnVar -> Instr s ('TNat ': s)
AnnSELF_ADDRESS :: AnnVar -> Instr s ('TAddress ': s)
NEVER :: Instr ('TNever ': s) t
AnnTICKET_DEPRECATED
:: Comparable a
=> AnnVar
-> Instr (a ': 'TNat ': s) ('TTicket a ': s)
AnnTICKET
:: Comparable a
=> AnnVar
-> Instr (a ': 'TNat ': s) ('TOption ('TTicket a) ': s)
AnnREAD_TICKET
:: AnnVar
-> Instr ('TTicket a ': s) (RightComb ['TAddress, a, 'TNat] ': 'TTicket a ': s)
AnnSPLIT_TICKET
:: AnnVar
-> Instr ('TTicket a ': 'TPair 'TNat 'TNat ': s)
('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
AnnJOIN_TICKETS
:: AnnVar
-> Instr ('TPair ('TTicket a) ('TTicket a) ': s)
('TOption ('TTicket a) ': s)
AnnOPEN_CHEST
:: AnnVar
-> Instr ('TChestKey ': 'TChest ': 'TNat ': s)
('TOr 'TBytes 'TBool ': s)
AnnSAPLING_EMPTY_STATE
:: AnnVar
-> Sing n
-> Instr s
('TSaplingState n ': s)
AnnSAPLING_VERIFY_UPDATE
:: AnnVar
-> Instr ('TSaplingTransaction n : 'TSaplingState n ': s)
('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s)
AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s)
AnnEMIT
:: PackedValScope t
=> AnnVar
-> FieldAnn
-> Maybe (Notes t)
-> Instr (t ': s) ('TOperation : s)
castInstr
:: forall inp1 out1 inp2 out2.
( SingI inp1
, SingI out1
, SingI inp2
, SingI out2
)
=> Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr :: forall (inp1 :: [T]) (out1 :: [T]) (inp2 :: [T]) (out2 :: [T]).
(SingI inp1, SingI out1, SingI inp2, SingI out2) =>
Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr Instr inp1 out1
instr =
case (forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @inp1 @inp2, forall (a :: [T]) (b :: [T]).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @out1 @out2) of
(Just inp1 :~: inp2
Refl, Just out1 :~: out2
Refl) -> Instr inp2 out2 -> Maybe (Instr inp2 out2)
forall a. a -> Maybe a
Just Instr inp1 out1
Instr inp2 out2
instr
(Maybe (inp1 :~: inp2)
_,Maybe (out1 :~: out2)
_) -> Maybe (Instr inp2 out2)
forall a. Maybe a
Nothing
pattern (:#) :: Instr a b -> Instr b c -> Instr a c
pattern a $m:# :: forall {r} {a :: [T]} {c :: [T]}.
Instr a c
-> (forall {b :: [T]}. Instr a b -> Instr b c -> r)
-> ((# #) -> r)
-> r
$b:# :: forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# b = Seq a b
infixr 8 :#
deriving stock instance Show (Instr inp out)
instance Semigroup (Instr s s) where
<> :: Instr s s -> Instr s s -> Instr s s
(<>) = Instr s s -> Instr s s -> Instr s s
forall (a :: [T]) (a :: [T]) (c :: [T]).
Instr a a -> Instr a c -> Instr a c
Seq
instance Monoid (Instr s s) where
mempty :: Instr s s
mempty = Instr s s
forall (s :: [T]). Instr s s
Nop
data TestAssert (s :: [T]) where
TestAssert
:: Text
-> PrintComment inp
-> Instr inp ('TBool ': out)
-> TestAssert inp
deriving stock instance Show (TestAssert s)
data StackRef (st :: [T]) where
StackRef
:: RequireLongerThan st idx
=> PeanoNatural idx -> StackRef st
instance NFData (StackRef st) where
rnf :: StackRef st -> ()
rnf (StackRef PeanoNatural idx
s) = PeanoNatural idx -> ()
forall a. NFData a => a -> ()
rnf PeanoNatural idx
s
instance Eq (StackRef st) where
StackRef PeanoNatural idx
snat1 == :: StackRef st -> StackRef st -> Bool
== StackRef PeanoNatural idx
snat2 = PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat1 Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat2
instance Show (StackRef st) where
showsPrec :: Int -> StackRef st -> ShowS
showsPrec Int
d (StackRef PeanoNatural idx
snat) = Bool -> ShowS -> ShowS
T.showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
app_prec) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
T.showString String
"StackRef " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Bool -> ShowS -> ShowS
T.showParen Bool
True (String -> ShowS
T.showString String
"toPeanoNatural' @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> ShowS
forall a. Show a => a -> ShowS
T.shows (PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat))
where
app_prec :: Int
app_prec = Int
10
instance Buildable (StackRef st) where
build :: StackRef st -> Doc
build (StackRef PeanoNatural idx
snat) = Doc
"StackRef {" Doc -> Doc -> Doc
forall b. FromDoc b => Doc -> Doc -> b
+| PeanoNatural idx -> Nat
forall (n :: Peano). PeanoNatural n -> Nat
fromPeanoNatural PeanoNatural idx
snat Nat -> Doc -> Doc
forall a b. (Buildable a, FromDoc b) => a -> Doc -> b
|+ Doc
"}"
mkStackRef
:: forall (gn :: Nat) st n.
(n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n)
=> StackRef st
mkStackRef :: forall (gn :: Nat) (st :: [T]) (n :: Peano).
(n ~ ToPeano gn, SingIPeano gn, RequireLongerThan st n) =>
StackRef st
mkStackRef = PeanoNatural (ToPeano gn) -> StackRef st
forall (st :: [T]) (a :: Peano).
RequireLongerThan st a =>
PeanoNatural a -> StackRef st
StackRef (PeanoNatural (ToPeano gn) -> StackRef st)
-> PeanoNatural (ToPeano gn) -> StackRef st
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)
toPeanoNatural' @gn
newtype (st :: [T]) =
{ :: [Either Text (StackRef st)]
} deriving stock (PrintComment st -> PrintComment st -> Bool
(PrintComment st -> PrintComment st -> Bool)
-> (PrintComment st -> PrintComment st -> Bool)
-> Eq (PrintComment st)
forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
== :: PrintComment st -> PrintComment st -> Bool
$c/= :: forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
/= :: PrintComment st -> PrintComment st -> Bool
Eq, Int -> PrintComment st -> ShowS
[PrintComment st] -> ShowS
PrintComment st -> String
(Int -> PrintComment st -> ShowS)
-> (PrintComment st -> String)
-> ([PrintComment st] -> ShowS)
-> Show (PrintComment st)
forall (st :: [T]). Int -> PrintComment st -> ShowS
forall (st :: [T]). [PrintComment st] -> ShowS
forall (st :: [T]). PrintComment st -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (st :: [T]). Int -> PrintComment st -> ShowS
showsPrec :: Int -> PrintComment st -> ShowS
$cshow :: forall (st :: [T]). PrintComment st -> String
show :: PrintComment st -> String
$cshowList :: forall (st :: [T]). [PrintComment st] -> ShowS
showList :: [PrintComment st] -> ShowS
Show, (forall x. PrintComment st -> Rep (PrintComment st) x)
-> (forall x. Rep (PrintComment st) x -> PrintComment st)
-> Generic (PrintComment st)
forall (st :: [T]) x. Rep (PrintComment st) x -> PrintComment st
forall (st :: [T]) x. PrintComment st -> Rep (PrintComment st) x
forall x. Rep (PrintComment st) x -> PrintComment st
forall x. PrintComment st -> Rep (PrintComment st) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (st :: [T]) x. PrintComment st -> Rep (PrintComment st) x
from :: forall x. PrintComment st -> Rep (PrintComment st) x
$cto :: forall (st :: [T]) x. Rep (PrintComment st) x -> PrintComment st
to :: forall x. Rep (PrintComment st) x -> PrintComment st
Generic)
deriving newtype (NonEmpty (PrintComment st) -> PrintComment st
PrintComment st -> PrintComment st -> PrintComment st
(PrintComment st -> PrintComment st -> PrintComment st)
-> (NonEmpty (PrintComment st) -> PrintComment st)
-> (forall b.
Integral b =>
b -> PrintComment st -> PrintComment st)
-> Semigroup (PrintComment st)
forall (st :: [T]). NonEmpty (PrintComment st) -> PrintComment st
forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
forall (st :: [T]) b.
Integral b =>
b -> PrintComment st -> PrintComment st
forall b. Integral b => b -> PrintComment st -> PrintComment st
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
<> :: PrintComment st -> PrintComment st -> PrintComment st
$csconcat :: forall (st :: [T]). NonEmpty (PrintComment st) -> PrintComment st
sconcat :: NonEmpty (PrintComment st) -> PrintComment st
$cstimes :: forall (st :: [T]) b.
Integral b =>
b -> PrintComment st -> PrintComment st
stimes :: forall b. Integral b => b -> PrintComment st -> PrintComment st
Semigroup, Semigroup (PrintComment st)
PrintComment st
Semigroup (PrintComment st)
-> PrintComment st
-> (PrintComment st -> PrintComment st -> PrintComment st)
-> ([PrintComment st] -> PrintComment st)
-> Monoid (PrintComment st)
[PrintComment st] -> PrintComment st
PrintComment st -> PrintComment st -> PrintComment st
forall (st :: [T]). Semigroup (PrintComment st)
forall (st :: [T]). PrintComment st
forall (st :: [T]). [PrintComment st] -> PrintComment st
forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: forall (st :: [T]). PrintComment st
mempty :: PrintComment st
$cmappend :: forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
mappend :: PrintComment st -> PrintComment st -> PrintComment st
$cmconcat :: forall (st :: [T]). [PrintComment st] -> PrintComment st
mconcat :: [PrintComment st] -> PrintComment st
Monoid)
instance NFData (PrintComment st)
instance IsString (PrintComment st) where
fromString :: String -> PrintComment st
fromString = [Either Text (StackRef st)] -> PrintComment st
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
PrintComment ([Either Text (StackRef st)] -> PrintComment st)
-> (String -> [Either Text (StackRef st)])
-> String
-> PrintComment st
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Text (StackRef st) -> [Either Text (StackRef st)]
OneItem [Either Text (StackRef st)] -> [Either Text (StackRef st)]
forall x. One x => OneItem x -> x
one (Either Text (StackRef st) -> [Either Text (StackRef st)])
-> (String -> Either Text (StackRef st))
-> String
-> [Either Text (StackRef st)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text (StackRef st)
forall a b. a -> Either a b
Left (Text -> Either Text (StackRef st))
-> (String -> Text) -> String -> Either Text (StackRef st)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString
data
= FunctionStarts Text
| FunctionEnds Text
| StatementStarts Text
| StatementEnds Text
| Text
| (Maybe [T])
deriving stock (Int -> CommentType -> ShowS
[CommentType] -> ShowS
CommentType -> String
(Int -> CommentType -> ShowS)
-> (CommentType -> String)
-> ([CommentType] -> ShowS)
-> Show CommentType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CommentType -> ShowS
showsPrec :: Int -> CommentType -> ShowS
$cshow :: CommentType -> String
show :: CommentType -> String
$cshowList :: [CommentType] -> ShowS
showList :: [CommentType] -> ShowS
Show, (forall x. CommentType -> Rep CommentType x)
-> (forall x. Rep CommentType x -> CommentType)
-> Generic CommentType
forall x. Rep CommentType x -> CommentType
forall x. CommentType -> Rep CommentType x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CommentType -> Rep CommentType x
from :: forall x. CommentType -> Rep CommentType x
$cto :: forall x. Rep CommentType x -> CommentType
to :: forall x. Rep CommentType x -> CommentType
Generic)
instance NFData CommentType
instance IsString CommentType where
fromString :: String -> CommentType
fromString = Text -> CommentType
JustComment (Text -> CommentType) -> (String -> Text) -> String -> CommentType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString
data ExtInstr s
= TEST_ASSERT (TestAssert s)
| PRINT (PrintComment s)
| DOC_ITEM SomeDocItem
| CommentType
| STACKTYPE StackTypePattern
deriving stock (Int -> ExtInstr s -> ShowS
[ExtInstr s] -> ShowS
ExtInstr s -> String
(Int -> ExtInstr s -> ShowS)
-> (ExtInstr s -> String)
-> ([ExtInstr s] -> ShowS)
-> Show (ExtInstr s)
forall (s :: [T]). Int -> ExtInstr s -> ShowS
forall (s :: [T]). [ExtInstr s] -> ShowS
forall (s :: [T]). ExtInstr s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (s :: [T]). Int -> ExtInstr s -> ShowS
showsPrec :: Int -> ExtInstr s -> ShowS
$cshow :: forall (s :: [T]). ExtInstr s -> String
show :: ExtInstr s -> String
$cshowList :: forall (s :: [T]). [ExtInstr s] -> ShowS
showList :: [ExtInstr s] -> ShowS
Show, (forall x. ExtInstr s -> Rep (ExtInstr s) x)
-> (forall x. Rep (ExtInstr s) x -> ExtInstr s)
-> Generic (ExtInstr s)
forall (s :: [T]) x. Rep (ExtInstr s) x -> ExtInstr s
forall (s :: [T]) x. ExtInstr s -> Rep (ExtInstr s) x
forall x. Rep (ExtInstr s) x -> ExtInstr s
forall x. ExtInstr s -> Rep (ExtInstr s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (s :: [T]) x. ExtInstr s -> Rep (ExtInstr s) x
from :: forall x. ExtInstr s -> Rep (ExtInstr s) x
$cto :: forall (s :: [T]) x. Rep (ExtInstr s) x -> ExtInstr s
to :: forall x. Rep (ExtInstr s) x -> ExtInstr s
Generic)
data SomeMeta where
SomeMeta
:: forall meta
. With [NFData, Show, Typeable] meta
=> meta
-> SomeMeta
instance NFData SomeMeta where
rnf :: SomeMeta -> ()
rnf (SomeMeta meta
meta) = meta -> ()
forall a. NFData a => a -> ()
rnf meta
meta
deriving stock instance Show SomeMeta
pattern ConcreteMeta :: Typeable meta => meta -> Instr i o -> Instr i o
pattern $mConcreteMeta :: forall {r} {meta} {i :: [T]} {o :: [T]}.
Typeable meta =>
Instr i o -> (meta -> Instr i o -> r) -> ((# #) -> r) -> r
ConcreteMeta meta instr <- Meta (SomeMeta (cast -> Just meta)) instr
pattern LAMBDA
:: forall s r . ()
=> forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s))
=> (IsNotInView => RemFail Instr '[i] '[o])
-> Instr s r
pattern $mLAMBDA :: forall {r} {s :: [T]} {r :: [T]}.
Instr s r
-> (forall {i :: T} {o :: T}.
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i] '[o]) -> r)
-> ((# #) -> r)
-> r
$bLAMBDA :: forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i] '[o]) -> Instr s r
LAMBDA code <- AnnLAMBDA _ code
where LAMBDA IsNotInView => RemFail Instr '[i] '[o]
code = Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a] '[b] -> Instr s ('TLambda a b : s)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
forall a. Default a => a
def (RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s))
-> RemFail Instr '[i] '[o] -> Instr s ('TLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[i] '[o]) -> RemFail Instr '[i] '[o]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail Instr '[i] '[o]
IsNotInView => RemFail Instr '[i] '[o]
code
pattern LAMBDA_REC
:: forall s r . ()
=> forall i o. (SingI i, SingI o, r ~ ('TLambda i o ': s))
=> (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o])
-> Instr s r
pattern $mLAMBDA_REC :: forall {r} {s :: [T]} {r :: [T]}.
Instr s r
-> (forall {i :: T} {o :: T}.
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> r)
-> ((# #) -> r)
-> r
$bLAMBDA_REC :: forall (s :: [T]) (r :: [T]) (i :: T) (o :: T).
(SingI i, SingI o, r ~ ('TLambda i o : s)) =>
(IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]) -> Instr s r
LAMBDA_REC code <- AnnLAMBDA_REC _ code
where LAMBDA_REC IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]
code = Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o : s)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a, 'TLambda a b] '[b]
-> Instr s ('TLambda a b : s)
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
forall a. Default a => a
def (RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o : s))
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr s ('TLambda i o : s)
forall a b. (a -> b) -> a -> b
$ (IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o])
-> RemFail Instr '[i, 'TLambda i o] '[o]
forall r. (IsNotInView => r) -> r
giveNotInView RemFail Instr '[i, 'TLambda i o] '[o]
IsNotInView => RemFail Instr '[i, 'TLambda i o] '[o]
code
frameInstr :: forall s a b. Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr :: forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr = \case
Seq Instr a b
i1 Instr b b
i2 -> Instr (a ++ s) (b ++ s)
-> Instr (b ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (a :: [T]) (c :: [T]).
Instr a a -> Instr a c -> Instr a c
Seq (Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1) (Instr b b -> Instr (b ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr b b
i2)
WithLoc ErrorSrcPos
loc Instr a b
instr -> ErrorSrcPos -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]). ErrorSrcPos -> Instr a b -> Instr a b
WithLoc ErrorSrcPos
loc (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
instr
Meta SomeMeta
m Instr a b
instr -> SomeMeta -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (a :: [T]) (b :: [T]). SomeMeta -> Instr a b -> Instr a b
Meta SomeMeta
m (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
instr
Nested Instr a b
i1 -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
Nested (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1
DocGroup DocGrouping
dg Instr a b
i1 -> DocGrouping -> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall (inp :: [T]) (out :: [T]).
DocGrouping -> Instr inp out -> Instr inp out
DocGroup DocGrouping
dg (Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s))
-> Instr (a ++ s) (b ++ s) -> Instr (a ++ s) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr a b -> Instr (a ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a b
i1
IF_NONE Instr s b
i1 Instr (a : s) b
i2 -> Instr (s ++ s) (b ++ s)
-> Instr (a : (s ++ s)) (b ++ s)
-> Instr ('TOption a : (s ++ s)) (b ++ s)
forall (a :: [T]) (s' :: [T]) (b :: T).
Instr a s' -> Instr (b : a) s' -> Instr ('TOption b : a) s'
IF_NONE (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i1) (Instr (a : s) b -> Instr ((a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) b
i2)
IF_LEFT Instr (a : s) b
i1 Instr (b : s) b
i2 -> Instr (a : (s ++ s)) (b ++ s)
-> Instr (b : (s ++ s)) (b ++ s)
-> Instr ('TOr a b : (s ++ s)) (b ++ s)
forall (a :: T) (b :: [T]) (s' :: [T]) (s :: T).
Instr (a : b) s' -> Instr (s : b) s' -> Instr ('TOr a s : b) s'
IF_LEFT (Instr (a : s) b -> Instr ((a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) b
i1) (Instr (b : s) b -> Instr ((b : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (b : s) b
i2)
IF_CONS Instr (a : 'TList a : s) b
i1 Instr s b
i2 -> Instr (a : 'TList a : (s ++ s)) (b ++ s)
-> Instr (s ++ s) (b ++ s) -> Instr ('TList a : (s ++ s)) (b ++ s)
forall (a :: T) (b :: [T]) (s' :: [T]).
Instr (a : 'TList a : b) s'
-> Instr b s' -> Instr ('TList a : b) s'
IF_CONS (Instr (a : 'TList a : s) b
-> Instr ((a : 'TList a : s) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : 'TList a : s) b
i1) (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i2)
IF Instr s b
i1 Instr s b
i2 -> Instr (s ++ s) (b ++ s)
-> Instr (s ++ s) (b ++ s) -> Instr ('TBool : (s ++ s)) (b ++ s)
forall (a :: [T]) (s' :: [T]).
Instr a s' -> Instr a s' -> Instr ('TBool : a) s'
IF (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i1) (Instr s b -> Instr (s ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s b
i2)
AnnMAP AnnVar
ann Instr (MapOpInp c : s) (b : s)
i1 -> AnnVar
-> Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
-> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(MapOp a, SingI b) =>
AnnVar
-> Instr (MapOpInp a : s) (b : s)
-> Instr (a : s) (MapOpRes a b : s)
AnnMAP AnnVar
ann (Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
-> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s)))
-> Instr (MapOpInp c : (s ++ s)) (b : (s ++ s))
-> Instr (c : (s ++ s)) (MapOpRes c b : (s ++ s))
forall a b. (a -> b) -> a -> b
$ Instr (MapOpInp c : s) (b : s)
-> Instr ((MapOpInp c : s) ++ s) ((b : s) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (MapOpInp c : s) (b : s)
i1
ITER Instr (IterOpEl c : b) b
i1 -> Instr (IterOpEl c : (b ++ s)) (b ++ s)
-> Instr (c : (b ++ s)) (b ++ s)
forall (a :: T) (s :: [T]).
IterOp a =>
Instr (IterOpEl a : s) s -> Instr (a : s) s
ITER (Instr (IterOpEl c : (b ++ s)) (b ++ s)
-> Instr (c : (b ++ s)) (b ++ s))
-> Instr (IterOpEl c : (b ++ s)) (b ++ s)
-> Instr (c : (b ++ s)) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr (IterOpEl c : b) b -> Instr ((IterOpEl c : b) ++ s) (b ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (IterOpEl c : b) b
i1
LOOP Instr b ('TBool : b)
i1 -> Instr (b ++ s) ('TBool : (b ++ s))
-> Instr ('TBool : (b ++ s)) (b ++ s)
forall (s :: [T]). Instr s ('TBool : s) -> Instr ('TBool : s) s
LOOP (Instr (b ++ s) ('TBool : (b ++ s))
-> Instr ('TBool : (b ++ s)) (b ++ s))
-> Instr (b ++ s) ('TBool : (b ++ s))
-> Instr ('TBool : (b ++ s)) (b ++ s)
forall a b. (a -> b) -> a -> b
$ Instr b ('TBool : b) -> Instr (b ++ s) (('TBool : b) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr b ('TBool : b)
i1
LOOP_LEFT Instr (a : s) ('TOr a b : s)
i1 -> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
-> Instr ('TOr a b : (s ++ s)) (b : (s ++ s))
forall (a :: T) (b :: [T]) (s :: T).
Instr (a : b) ('TOr a s : b) -> Instr ('TOr a s : b) (s : b)
LOOP_LEFT (Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
-> Instr ('TOr a b : (s ++ s)) (b : (s ++ s)))
-> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
-> Instr ('TOr a b : (s ++ s)) (b : (s ++ s))
forall a b. (a -> b) -> a -> b
$ Instr (a : s) ('TOr a b : s)
-> Instr ((a : s) ++ s) (('TOr a b : s) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr (a : s) ('TOr a b : s)
i1
DIP Instr a c
i1 -> Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s))
forall (a :: [T]) (b :: [T]) (s :: T).
Instr a b -> Instr (s : a) (s : b)
DIP (Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s)))
-> Instr (a ++ s) (c ++ s) -> Instr (b : (a ++ s)) (b : (c ++ s))
forall a b. (a -> b) -> a -> b
$ Instr a c -> Instr (a ++ s) (c ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a c
i1
DIPN PeanoNatural n
n (Instr s s'
i1 :: Instr s1 s1') -> PeanoNatural n
-> Instr (Drop n (a ++ s)) (Drop n (b ++ s))
-> Instr (a ++ s) (b ++ s)
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: [T])
(s :: [T]).
ConstraintDIPN a inp out b s =>
PeanoNatural a -> Instr b s -> Instr inp out
DIPN PeanoNatural n
n (Instr s s' -> Instr (s ++ s) (s' ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr s s'
i1) ((RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s' ++ s)) ~ (b ++ s),
(s ++ s) ~ Drop n (a ++ s), (s' ++ s) ~ Drop n (b ++ s)) =>
Instr (a ++ s) (b ++ s))
-> Dict
(RequireLongerOrSameLength (a ++ s) n,
(LazyTake n (a ++ s) ++ (s ++ s)) ~ (a ++ s),
(LazyTake n (a ++ s) ++ (s' ++ s)) ~ (b ++ s),
(s ++ s) ~ Drop n (a ++ s), (s' ++ s) ~ Drop n (b ++ s))
-> Instr (a ++ s) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (s1 :: [T]) (s1' :: [T])
(n :: Peano).
ConstraintDIPN n a b s1 s1' =>
PeanoNatural n
-> Dict (ConstraintDIPN n (a ++ s) (b ++ s) (s1 ++ s) (s1' ++ s))
dipNExtensionThm @s @a @b @s1 @s1' PeanoNatural n
n
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v -> Anns '[VarAnn, Notes t]
-> Value' Instr t -> Instr (a ++ s) (t : (a ++ s))
forall (a :: T) (s :: [T]).
ConstantScope a =>
Anns '[VarAnn, Notes a] -> Value' Instr a -> Instr s (a : s)
AnnPUSH Anns '[VarAnn, Notes t]
ann Value' Instr t
v
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
lam -> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i] '[o]
-> Instr (a ++ s) ('TLambda i o : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a] '[b] -> Instr s ('TLambda a b : s)
AnnLAMBDA Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i] '[o]
lam
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
lam -> Anns '[VarAnn, Notes i, Notes o]
-> RemFail Instr '[i, 'TLambda i o] '[o]
-> Instr (a ++ s) ('TLambda i o : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b) =>
Anns '[VarAnn, Notes a, Notes b]
-> RemFail Instr '[a, 'TLambda a b] '[b]
-> Instr s ('TLambda a b : s)
AnnLAMBDA_REC Anns '[VarAnn, Notes i, Notes o]
ann RemFail Instr '[i, 'TLambda i o] '[o]
lam
AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract -> Anns '[VarAnn, VarAnn]
-> Contract' Instr p g
-> Instr
('TOption 'TKeyHash : 'TMutez : g : (s ++ s))
('TOperation : 'TAddress : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(ParameterScope a, StorageScope b, IsNotInView) =>
Anns '[VarAnn, VarAnn]
-> Contract' Instr a b
-> Instr
('TOption 'TKeyHash : 'TMutez : b : s)
('TOperation : 'TAddress : s)
AnnCREATE_CONTRACT Anns '[VarAnn, VarAnn]
ann Contract' Instr p g
contract
Instr a b
Nop -> Instr (a ++ s) (a ++ s)
Instr (a ++ s) (b ++ s)
forall (s :: [T]). Instr s s
Nop
Ext (TEST_ASSERT (TestAssert Text
t PrintComment a
c Instr a ('TBool : out)
i)) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s))
-> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall a b. (a -> b) -> a -> b
$ TestAssert (a ++ s) -> ExtInstr (a ++ s)
forall (s :: [T]). TestAssert s -> ExtInstr s
TEST_ASSERT (TestAssert (a ++ s) -> ExtInstr (a ++ s))
-> TestAssert (a ++ s) -> ExtInstr (a ++ s)
forall a b. (a -> b) -> a -> b
$ Text
-> PrintComment (a ++ s)
-> Instr (a ++ s) ('TBool : (out ++ s))
-> TestAssert (a ++ s)
forall (inp :: [T]) (a :: [T]).
Text
-> PrintComment inp -> Instr inp ('TBool : a) -> TestAssert inp
TestAssert Text
t (PrintComment a -> PrintComment (a ++ s)
comment PrintComment a
c) (Instr a ('TBool : out) -> Instr (a ++ s) (('TBool : out) ++ s)
forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go Instr a ('TBool : out)
i)
Ext (PRINT PrintComment a
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s))
-> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall a b. (a -> b) -> a -> b
$ PrintComment (a ++ s) -> ExtInstr (a ++ s)
forall (s :: [T]). PrintComment s -> ExtInstr s
PRINT (PrintComment (a ++ s) -> ExtInstr (a ++ s))
-> PrintComment (a ++ s) -> ExtInstr (a ++ s)
forall a b. (a -> b) -> a -> b
$ PrintComment a -> PrintComment (a ++ s)
comment PrintComment a
x
Ext (DOC_ITEM SomeDocItem
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (SomeDocItem -> ExtInstr (a ++ s)
forall (s :: [T]). SomeDocItem -> ExtInstr s
DOC_ITEM SomeDocItem
x)
Ext (COMMENT_ITEM CommentType
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (CommentType -> ExtInstr (a ++ s)
forall (s :: [T]). CommentType -> ExtInstr s
COMMENT_ITEM CommentType
x)
Ext (STACKTYPE StackTypePattern
x) -> ExtInstr (a ++ s) -> Instr (a ++ s) (a ++ s)
forall (s :: [T]). ExtInstr s -> Instr s s
Ext (StackTypePattern -> ExtInstr (a ++ s)
forall (s :: [T]). StackTypePattern -> ExtInstr s
STACKTYPE StackTypePattern
x)
AnnCAR Anns '[VarAnn, FieldAnn]
anns -> Anns '[VarAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b : s) (a : s)
AnnCAR Anns '[VarAnn, FieldAnn]
anns
AnnCDR Anns '[VarAnn, FieldAnn]
anns -> Anns '[VarAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, FieldAnn] -> Instr ('TPair a b : s) (b : s)
AnnCDR Anns '[VarAnn, FieldAnn]
anns
Instr a b
DROP -> Instr (a : (b ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: T) (s :: [T]). Instr (a : s) s
DROP
DROPN PeanoNatural n
n -> PeanoNatural n -> Instr (a ++ s) (Drop n (a ++ s))
forall (a :: Peano) (s :: [T]).
RequireLongerOrSameLength s a =>
PeanoNatural a -> Instr s (Drop a s)
DROPN PeanoNatural n
n ((Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True) =>
Instr (a ++ s) (b ++ s))
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
-> Instr (a ++ s) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
forall {k} (s :: [k]) (a :: [k]) (b :: [k]) (n :: Peano).
(Drop n a ~ b, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
(Drop n (a ++ s) ~ (b ++ s),
IsLongerOrSameLength (a ++ s) n ~ 'True)
dropNExtensionThm @s @a PeanoNatural n
n
AnnDUP AnnVar
anns -> AnnVar -> Instr (a : (s ++ s)) (a : a : (s ++ s))
forall (a :: T) (b :: [T]).
DupableScope a =>
AnnVar -> Instr (a : b) (a : a : b)
AnnDUP AnnVar
anns
AnnDUPN AnnVar
anns PeanoNatural n
n -> AnnVar -> PeanoNatural n -> Instr (a ++ s) (a : (a ++ s))
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
(ConstraintDUPN a inp out b, DupableScope b) =>
AnnVar -> PeanoNatural a -> Instr inp out
AnnDUPN AnnVar
anns PeanoNatural n
n ((RequireLongerOrSameLength (a ++ s) n, 'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s) ++ (a : Drop n (a ++ s))),
(a : (a ++ s)) ~ (a : (a ++ s))) =>
Instr (a ++ s) (a : (a ++ s)))
-> Dict
(RequireLongerOrSameLength (a ++ s) n, 'True ~ 'True,
(a ++ s)
~ (LazyTake (Decrement n) (a ++ s) ++ (a : Drop n (a ++ s))),
(a : (a ++ s)) ~ (a : (a ++ s)))
-> Instr (a ++ s) (a : (a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T).
ConstraintDUPN n a b x =>
PeanoNatural n -> Dict (ConstraintDUPN n (a ++ s) (b ++ s) x)
dupNExtensionThm @s @a @b PeanoNatural n
n
Instr a b
SWAP -> Instr (a : b : (s ++ s)) (b : a : (s ++ s))
Instr (a ++ s) (b ++ s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
DIG PeanoNatural n
n -> PeanoNatural n
-> Instr
(a ++ s) (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s)))
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
ConstraintDIG a inp out b =>
PeanoNatural a -> Instr inp out
DIG PeanoNatural n
n ((RequireLongerThan (a ++ s) n,
(a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
~ (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s)
~ (LazyTake n ((LazyTake n a ++ Drop ('S n) a) ++ s)
++ (a : Drop n ((LazyTake n a ++ Drop ('S n) a) ++ s)))) =>
Instr (a ++ s) (a : ((LazyTake n a ++ Drop ('S n) a) ++ s)))
-> Dict
(RequireLongerThan (a ++ s) n,
(a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
~ (a : (LazyTake n (a ++ s) ++ Drop ('S n) (a ++ s))),
(a ++ s)
~ (LazyTake n ((LazyTake n a ++ Drop ('S n) a) ++ s)
++ (a : Drop n ((LazyTake n a ++ Drop ('S n) a) ++ s))))
-> Instr (a ++ s) (a : ((LazyTake n a ++ Drop ('S n) a) ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
(n :: Peano).
(b ~ (x : r), ConstraintDIG n a b x) =>
PeanoNatural n -> Dict (ConstraintDIG n (a ++ s) (b ++ s) x)
digNExtensionThm @s @a @b PeanoNatural n
n
DUG PeanoNatural n
n -> PeanoNatural n
-> Instr
(a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))) (b ++ s)
forall (a :: Peano) (inp :: [T]) (out :: [T]) (b :: T).
ConstraintDUG a inp out b =>
PeanoNatural a -> Instr inp out
DUG PeanoNatural n
n ((RequireLongerThan (b ++ s) n,
(a : ((LazyTake n b ++ Drop ('S n) b) ++ s))
~ (a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s)
~ (LazyTake n ((LazyTake n b ++ Drop ('S n) b) ++ s)
++ (a : Drop n ((LazyTake n b ++ Drop ('S n) b) ++ s)))) =>
Instr (a : ((LazyTake n b ++ Drop ('S n) b) ++ s)) (b ++ s))
-> Dict
(RequireLongerThan (b ++ s) n,
(a : ((LazyTake n b ++ Drop ('S n) b) ++ s))
~ (a : (LazyTake n (b ++ s) ++ Drop ('S n) (b ++ s))),
(b ++ s)
~ (LazyTake n ((LazyTake n b ++ Drop ('S n) b) ++ s)
++ (a : Drop n ((LazyTake n b ++ Drop ('S n) b) ++ s))))
-> Instr (a : ((LazyTake n b ++ Drop ('S n) b) ++ s)) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (x :: T) (r :: [T])
(n :: Peano).
(a ~ (x : r), ConstraintDUG n a b x) =>
PeanoNatural n -> Dict (ConstraintDUG n (a ++ s) (b ++ s) x)
dugNExtensionThm @s @a @b PeanoNatural n
n
AnnSOME Anns '[TypeAnn, VarAnn]
anns -> Anns '[TypeAnn, VarAnn]
-> Instr (a : (s ++ s)) ('TOption a : (s ++ s))
forall (a :: T) (b :: [T]).
Anns '[TypeAnn, VarAnn] -> Instr (a : b) ('TOption a : b)
AnnSOME Anns '[TypeAnn, VarAnn]
anns
AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
anns -> Anns '[TypeAnn, VarAnn, Notes a]
-> Instr (a ++ s) ('TOption a : (a ++ s))
forall (a :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TOption a : s)
AnnNONE Anns '[TypeAnn, VarAnn, Notes a]
anns
AnnUNIT Anns '[TypeAnn, VarAnn]
anns -> Anns '[TypeAnn, VarAnn] -> Instr (a ++ s) ('TUnit : (a ++ s))
forall (s :: [T]). Anns '[TypeAnn, VarAnn] -> Instr s ('TUnit : s)
AnnUNIT Anns '[TypeAnn, VarAnn]
anns
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : (s ++ s)) ('TPair a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr (a : b : s) ('TPair a b : s)
AnnPAIR Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn]
anns
AnnUNPAIR Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns -> Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr ('TPair a b : (s ++ s)) (a : b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
-> Instr ('TPair a b : s) (a : b : s)
AnnUNPAIR Anns '[VarAnn, VarAnn, FieldAnn, FieldAnn]
anns
AnnPAIRN AnnVar
anns PeanoNatural n
n -> AnnVar -> PeanoNatural n -> Instr (a ++ s) (PairN n (a ++ s))
forall (a :: Peano) (inp :: [T]).
ConstraintPairN a inp =>
AnnVar -> PeanoNatural a -> Instr inp (PairN a inp)
AnnPAIRN AnnVar
anns PeanoNatural n
n (((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s)) =>
Instr (a ++ s) (RightComb (LazyTake n a) : (Drop n a ++ s)))
-> Dict
((RequireLongerOrSameLength (a ++ s) n,
(() :: Constraint, 'True ~ 'True)),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
-> Instr (a ++ s) (RightComb (LazyTake n a) : (Drop n a ++ s))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (n :: Peano).
((n >= ToPeano 2) ~ 'True, IsLongerOrSameLength a n ~ 'True) =>
PeanoNatural n
-> Dict
(ConstraintPairN n (a ++ s),
RightComb (LazyTake n (a ++ s)) ~ RightComb (LazyTake n a),
Drop n (a ++ s) ~ (Drop n a ++ s))
pairNExtensionThm @s @a PeanoNatural n
n
UNPAIRN PeanoNatural n
n -> PeanoNatural n
-> Instr (pair : (s ++ s)) (UnpairN n pair ++ (s ++ s))
forall (a :: Peano) (b :: T) (s :: [T]).
ConstraintUnpairN a b =>
PeanoNatural a -> Instr (b : s) (UnpairN a b ++ s)
UNPAIRN PeanoNatural n
n ((((() :: Constraint, 'True ~ 'True),
(() :: Constraint, 'True ~ 'True)),
(UnpairN n pair ++ (s ++ s)) ~ (b ++ s)) =>
Instr (pair : (s ++ s)) (b ++ s))
-> Dict
(((() :: Constraint, 'True ~ 'True),
(() :: Constraint, 'True ~ 'True)),
(UnpairN n pair ++ (s ++ s)) ~ (b ++ s))
-> Instr (pair : (s ++ s)) (b ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (s :: [T]) (a :: [T]) (b :: [T]) (n :: Peano) (x :: T)
(r :: [T]).
(a ~ (x : r), CombedPairLeafCountIsAtLeast n x ~ 'True,
(n >= ToPeano 2) ~ 'True, (UnpairN n x ++ r) ~ b) =>
PeanoNatural n
-> Dict
(ConstraintUnpairN n x, (UnpairN n x ++ (r ++ s)) ~ (b ++ s))
unpairNExtensionThm @s @a PeanoNatural n
n
AnnLEFT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
-> Instr (a : (s ++ s)) ('TOr a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : s) ('TOr b a : s)
AnnLEFT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes b]
anns
AnnRIGHT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns -> Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : (s ++ s)) ('TOr a b : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
-> Instr (b : s) ('TOr a b : s)
AnnRIGHT Anns '[TypeAnn, VarAnn, FieldAnn, FieldAnn, Notes a]
anns
AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
anns -> Anns '[TypeAnn, VarAnn, Notes p]
-> Instr (a ++ s) ('TList p : (a ++ s))
forall (a :: T) (s :: [T]).
SingI a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TList a : s)
AnnNIL Anns '[TypeAnn, VarAnn, Notes p]
anns
AnnCONS AnnVar
anns -> AnnVar -> Instr (a : 'TList a : (s ++ s)) ('TList a : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar -> Instr (a : 'TList a : b) ('TList a : b)
AnnCONS AnnVar
anns
AnnSIZE AnnVar
anns -> AnnVar -> Instr (c : (s ++ s)) ('TNat : (s ++ s))
forall (a :: T) (b :: [T]).
SizeOp a =>
AnnVar -> Instr (a : b) ('TNat : b)
AnnSIZE AnnVar
anns
AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
anns -> Anns '[TypeAnn, VarAnn, Notes e]
-> Instr (a ++ s) ('TSet e : (a ++ s))
forall (a :: T) (s :: [T]).
Comparable a =>
Anns '[TypeAnn, VarAnn, Notes a] -> Instr s ('TSet a : s)
AnnEMPTY_SET Anns '[TypeAnn, VarAnn, Notes e]
anns
AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns -> Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> Instr (a ++ s) ('TMap a b : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, Comparable b) =>
Anns '[TypeAnn, VarAnn, Notes b, Notes a]
-> Instr s ('TMap b a : s)
AnnEMPTY_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns -> Anns '[TypeAnn, VarAnn, Notes a, Notes b]
-> Instr (a ++ s) ('TBigMap a b : (a ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, Comparable b, ForbidBigMap a) =>
Anns '[TypeAnn, VarAnn, Notes b, Notes a]
-> Instr s ('TBigMap b a : s)
AnnEMPTY_BIG_MAP Anns '[TypeAnn, VarAnn, Notes a, Notes b]
anns
AnnMEM AnnVar
anns -> AnnVar -> Instr (MemOpKey c : c : (s ++ s)) ('TBool : (s ++ s))
forall (a :: T) (b :: [T]).
MemOp a =>
AnnVar -> Instr (MemOpKey a : a : b) ('TBool : b)
AnnMEM AnnVar
anns
AnnGET AnnVar
anns -> AnnVar
-> Instr
(GetOpKey c : c : (s ++ s)) ('TOption (GetOpVal c) : (s ++ s))
forall (a :: T) (b :: [T]).
(GetOp a, SingI (GetOpVal a)) =>
AnnVar -> Instr (GetOpKey a : a : b) ('TOption (GetOpVal a) : b)
AnnGET AnnVar
anns
AnnGETN AnnVar
anns PeanoNatural ix
n -> AnnVar
-> PeanoNatural ix
-> Instr (pair : (s ++ s)) (GetN ix pair : (s ++ s))
forall (a :: Peano) (b :: T) (s :: [T]).
ConstraintGetN a b =>
AnnVar -> PeanoNatural a -> Instr (b : s) (GetN a b : s)
AnnGETN AnnVar
anns PeanoNatural ix
n
AnnUPDATE AnnVar
anns -> AnnVar
-> Instr (UpdOpKey c : UpdOpParams c : c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
UpdOp a =>
AnnVar -> Instr (UpdOpKey a : UpdOpParams a : a : b) (a : b)
AnnUPDATE AnnVar
anns
AnnUPDATEN AnnVar
anns PeanoNatural ix
n -> AnnVar
-> PeanoNatural ix
-> Instr (val : pair : (s ++ s)) (UpdateN ix val pair : (s ++ s))
forall (a :: Peano) (b :: T) (s :: T) (s :: [T]).
ConstraintUpdateN a s =>
AnnVar -> PeanoNatural a -> Instr (b : s : s) (UpdateN a b s : s)
AnnUPDATEN AnnVar
anns PeanoNatural ix
n
AnnGET_AND_UPDATE AnnVar
anns -> AnnVar
-> Instr
(UpdOpKey c : UpdOpParams c : c : (s ++ s))
('TOption (GetOpVal c) : c : (s ++ s))
forall (a :: T) (b :: [T]).
(GetOp a, UpdOp a, SingI (GetOpVal a), UpdOpKey a ~ GetOpKey a) =>
AnnVar
-> Instr
(UpdOpKey a : UpdOpParams a : a : b)
('TOption (GetOpVal a) : a : b)
AnnGET_AND_UPDATE AnnVar
anns
AnnEXEC AnnVar
anns -> AnnVar -> Instr (t1 : 'TLambda t1 t2 : (s ++ s)) (t2 : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
AnnVar -> Instr (a : 'TLambda a b : s) (b : s)
AnnEXEC AnnVar
anns
AnnAPPLY AnnVar
anns -> AnnVar
-> Instr
(a : 'TLambda ('TPair a b) c : (s ++ s)) ('TLambda b c : (s ++ s))
forall (a :: T) (b :: T) (s :: T) (s :: [T]).
(ConstantScope a, SingI b) =>
AnnVar
-> Instr (a : 'TLambda ('TPair a b) s : s) ('TLambda b s : s)
AnnAPPLY AnnVar
anns
Instr a b
FAILWITH -> Instr (a : (s ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: T) (b :: [T]) (t :: [T]).
(SingI a, ConstantScope a) =>
Instr (a : b) t
FAILWITH
AnnCAST Anns '[VarAnn, Notes a]
anns -> Anns '[VarAnn, Notes a] -> Instr (a : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: [T]).
SingI a =>
Anns '[VarAnn, Notes a] -> Instr (a : b) (a : b)
AnnCAST Anns '[VarAnn, Notes a]
anns
AnnRENAME AnnVar
anns -> AnnVar -> Instr (a : (s ++ s)) (a : (s ++ s))
forall (a :: T) (b :: [T]). AnnVar -> Instr (a : b) (a : b)
AnnRENAME AnnVar
anns
AnnPACK AnnVar
anns -> AnnVar -> Instr (a : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: T) (b :: [T]).
PackedValScope a =>
AnnVar -> Instr (a : b) ('TBytes : b)
AnnPACK AnnVar
anns
AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
anns -> Anns '[TypeAnn, VarAnn, Notes a]
-> Instr ('TBytes : (s ++ s)) ('TOption a : (s ++ s))
forall (a :: T) (b :: [T]).
(UnpackedValScope a, SingI a) =>
Anns '[TypeAnn, VarAnn, Notes a]
-> Instr ('TBytes : b) ('TOption a : b)
AnnUNPACK Anns '[TypeAnn, VarAnn, Notes a]
anns
AnnCONCAT AnnVar
anns -> AnnVar -> Instr (c : c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
ConcatOp a =>
AnnVar -> Instr (a : a : b) (a : b)
AnnCONCAT AnnVar
anns
AnnCONCAT' AnnVar
anns -> AnnVar -> Instr ('TList c : (s ++ s)) (c : (s ++ s))
forall (a :: T) (b :: [T]).
ConcatOp a =>
AnnVar -> Instr ('TList a : b) (a : b)
AnnCONCAT' AnnVar
anns
AnnSLICE AnnVar
anns -> AnnVar
-> Instr ('TNat : 'TNat : c : (s ++ s)) ('TOption c : (s ++ s))
forall (a :: T) (b :: [T]).
(SliceOp a, SingI a) =>
AnnVar -> Instr ('TNat : 'TNat : a : b) ('TOption a : b)
AnnSLICE AnnVar
anns
AnnISNAT AnnVar
anns -> AnnVar -> Instr ('TInt : (s ++ s)) ('TOption 'TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TInt : a) ('TOption 'TNat : a)
AnnISNAT AnnVar
anns
AnnADD AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Add n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Add a b =>
AnnVar -> Instr (a : b : s) (ArithRes Add a b : s)
AnnADD AnnVar
anns
AnnSUB AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Sub n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Sub a b =>
AnnVar -> Instr (a : b : s) (ArithRes Sub a b : s)
AnnSUB AnnVar
anns
AnnSUB_MUTEZ AnnVar
anns -> AnnVar
-> Instr
('TMutez : 'TMutez : (s ++ s)) ('TOption 'TMutez : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TMutez : 'TMutez : a) ('TOption 'TMutez : a)
AnnSUB_MUTEZ AnnVar
anns
AnnMUL AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Mul n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Mul a b =>
AnnVar -> Instr (a : b : s) (ArithRes Mul a b : s)
AnnMUL AnnVar
anns
AnnEDIV AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes EDiv n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp EDiv a b =>
AnnVar -> Instr (a : b : s) (ArithRes EDiv a b : s)
AnnEDIV AnnVar
anns
AnnABS AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Abs n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Abs a =>
AnnVar -> Instr (a : b) (UnaryArithRes Abs a : b)
AnnABS AnnVar
anns
AnnNEG AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Neg n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Neg a =>
AnnVar -> Instr (a : b) (UnaryArithRes Neg a : b)
AnnNEG AnnVar
anns
AnnLSL AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Lsl n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Lsl a b =>
AnnVar -> Instr (a : b : s) (ArithRes Lsl a b : s)
AnnLSL AnnVar
anns
AnnLSR AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Lsr n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Lsr a b =>
AnnVar -> Instr (a : b : s) (ArithRes Lsr a b : s)
AnnLSR AnnVar
anns
AnnOR AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Or n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Or a b =>
AnnVar -> Instr (a : b : s) (ArithRes Or a b : s)
AnnOR AnnVar
anns
AnnAND AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes And n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp And a b =>
AnnVar -> Instr (a : b : s) (ArithRes And a b : s)
AnnAND AnnVar
anns
AnnXOR AnnVar
anns -> AnnVar -> Instr (n : m : (s ++ s)) (ArithRes Xor n m : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
ArithOp Xor a b =>
AnnVar -> Instr (a : b : s) (ArithRes Xor a b : s)
AnnXOR AnnVar
anns
AnnNOT AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Not n : (s ++ s))
forall (a :: T) (b :: [T]).
(SingI a, UnaryArithOp Not a) =>
AnnVar -> Instr (a : b) (UnaryArithRes Not a : b)
AnnNOT AnnVar
anns
AnnCOMPARE AnnVar
anns -> AnnVar -> Instr (n : n : (s ++ s)) ('TInt : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : a : b) ('TInt : b)
AnnCOMPARE AnnVar
anns
AnnEQ AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Eq' n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Eq' a =>
AnnVar -> Instr (a : b) (UnaryArithRes Eq' a : b)
AnnEQ AnnVar
anns
AnnNEQ AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Neq n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Neq a =>
AnnVar -> Instr (a : b) (UnaryArithRes Neq a : b)
AnnNEQ AnnVar
anns
AnnLT AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Lt n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Lt a =>
AnnVar -> Instr (a : b) (UnaryArithRes Lt a : b)
AnnLT AnnVar
anns
AnnGT AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Gt n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Gt a =>
AnnVar -> Instr (a : b) (UnaryArithRes Gt a : b)
AnnGT AnnVar
anns
AnnLE AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Le n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Le a =>
AnnVar -> Instr (a : b) (UnaryArithRes Le a : b)
AnnLE AnnVar
anns
AnnGE AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) (UnaryArithRes Ge n : (s ++ s))
forall (a :: T) (b :: [T]).
UnaryArithOp Ge a =>
AnnVar -> Instr (a : b) (UnaryArithRes Ge a : b)
AnnGE AnnVar
anns
AnnINT AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) ('TInt : (s ++ s))
forall (a :: T) (b :: [T]).
ToIntArithOp a =>
AnnVar -> Instr (a : b) ('TInt : b)
AnnINT AnnVar
anns
AnnVIEW Anns '[VarAnn, Notes ret]
anns ViewName
n -> Anns '[VarAnn, Notes ret]
-> ViewName
-> Instr (arg : 'TAddress : (s ++ s)) ('TOption ret : (s ++ s))
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, ViewableScope b) =>
Anns '[VarAnn, Notes b]
-> ViewName -> Instr (a : 'TAddress : s) ('TOption b : s)
AnnVIEW Anns '[VarAnn, Notes ret]
anns ViewName
n
AnnSELF AnnVar
anns SomeEntrypointCallT arg
ep -> AnnVar
-> SomeEntrypointCallT arg
-> Instr (a ++ s) ('TContract arg : (a ++ s))
forall (a :: T) (s :: [T]).
(ParameterScope a, IsNotInView) =>
AnnVar -> SomeEntrypointCallT a -> Instr s ('TContract a : s)
AnnSELF AnnVar
anns SomeEntrypointCallT arg
ep
AnnCONTRACT Anns '[VarAnn, Notes p]
anns EpName
c -> Anns '[VarAnn, Notes p]
-> EpName
-> Instr
('TAddress : (s ++ s)) ('TOption ('TContract p) : (s ++ s))
forall (a :: T) (b :: [T]).
ParameterScope a =>
Anns '[VarAnn, Notes a]
-> EpName -> Instr ('TAddress : b) ('TOption ('TContract a) : b)
AnnCONTRACT Anns '[VarAnn, Notes p]
anns EpName
c
AnnTRANSFER_TOKENS AnnVar
anns -> AnnVar
-> Instr
(p : 'TMutez : 'TContract p : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: T) (b :: [T]).
(ParameterScope a, IsNotInView) =>
AnnVar -> Instr (a : 'TMutez : 'TContract a : b) ('TOperation : b)
AnnTRANSFER_TOKENS AnnVar
anns
AnnSET_DELEGATE AnnVar
anns -> AnnVar
-> Instr ('TOption 'TKeyHash : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: [T]).
IsNotInView =>
AnnVar -> Instr ('TOption 'TKeyHash : a) ('TOperation : a)
AnnSET_DELEGATE AnnVar
anns
AnnIMPLICIT_ACCOUNT AnnVar
anns -> AnnVar
-> Instr ('TKeyHash : (s ++ s)) ('TContract 'TUnit : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TKeyHash : a) ('TContract 'TUnit : a)
AnnIMPLICIT_ACCOUNT AnnVar
anns
AnnNOW AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TTimestamp : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TTimestamp : s)
AnnNOW AnnVar
anns
AnnAMOUNT AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TMutez : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TMutez : s)
AnnAMOUNT AnnVar
anns
AnnBALANCE AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TMutez : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TMutez : s)
AnnBALANCE AnnVar
anns
AnnVOTING_POWER AnnVar
anns -> AnnVar -> Instr ('TKeyHash : (s ++ s)) ('TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TKeyHash : a) ('TNat : a)
AnnVOTING_POWER AnnVar
anns
AnnTOTAL_VOTING_POWER AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TNat : s)
AnnTOTAL_VOTING_POWER AnnVar
anns
AnnCHECK_SIGNATURE AnnVar
anns -> AnnVar
-> Instr
('TKey : 'TSignature : 'TBytes : (s ++ s)) ('TBool : (s ++ s))
forall (a :: [T]).
AnnVar -> Instr ('TKey : 'TSignature : 'TBytes : a) ('TBool : a)
AnnCHECK_SIGNATURE AnnVar
anns
AnnSHA256 AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA256 AnnVar
anns
AnnSHA512 AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA512 AnnVar
anns
AnnBLAKE2B AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnBLAKE2B AnnVar
anns
AnnSHA3 AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnSHA3 AnnVar
anns
AnnKECCAK AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TBytes : a)
AnnKECCAK AnnVar
anns
AnnHASH_KEY AnnVar
anns -> AnnVar -> Instr ('TKey : (s ++ s)) ('TKeyHash : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TKey : a) ('TKeyHash : a)
AnnHASH_KEY AnnVar
anns
AnnPAIRING_CHECK AnnVar
anns -> AnnVar
-> Instr
('TList ('TPair 'TBls12381G1 'TBls12381G2) : (s ++ s))
('TBool : (s ++ s))
forall (a :: [T]).
AnnVar
-> Instr
('TList ('TPair 'TBls12381G1 'TBls12381G2) : a) ('TBool : a)
AnnPAIRING_CHECK AnnVar
anns
AnnSOURCE AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSOURCE AnnVar
anns
AnnSENDER AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSENDER AnnVar
anns
AnnADDRESS AnnVar
anns -> AnnVar -> Instr ('TContract a : (s ++ s)) ('TAddress : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar -> Instr ('TContract a : b) ('TAddress : b)
AnnADDRESS AnnVar
anns
AnnCHAIN_ID AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TChainId : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TChainId : s)
AnnCHAIN_ID AnnVar
anns
AnnLEVEL AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TNat : s)
AnnLEVEL AnnVar
anns
AnnSELF_ADDRESS AnnVar
anns -> AnnVar -> Instr (a ++ s) ('TAddress : (a ++ s))
forall (s :: [T]). AnnVar -> Instr s ('TAddress : s)
AnnSELF_ADDRESS AnnVar
anns
Instr a b
NEVER -> Instr ('TNever : (s ++ s)) (b ++ s)
Instr (a ++ s) (b ++ s)
forall (a :: [T]) (t :: [T]). Instr ('TNever : a) t
NEVER
AnnTICKET AnnVar
anns -> AnnVar
-> Instr (a : 'TNat : (s ++ s)) ('TOption ('TTicket a) : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : 'TNat : b) ('TOption ('TTicket a) : b)
AnnTICKET AnnVar
anns
AnnTICKET_DEPRECATED AnnVar
anns -> AnnVar -> Instr (a : 'TNat : (s ++ s)) ('TTicket a : (s ++ s))
forall (a :: T) (b :: [T]).
Comparable a =>
AnnVar -> Instr (a : 'TNat : b) ('TTicket a : b)
AnnTICKET_DEPRECATED AnnVar
anns
AnnREAD_TICKET AnnVar
anns -> AnnVar
-> Instr
('TTicket a : (s ++ s))
(RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
('TTicket a : b)
(RightComb '[ 'TAddress, a, 'TNat] : 'TTicket a : b)
AnnREAD_TICKET AnnVar
anns
AnnSPLIT_TICKET AnnVar
anns -> AnnVar
-> Instr
('TTicket a : 'TPair 'TNat 'TNat : (s ++ s))
('TOption ('TPair ('TTicket a) ('TTicket a)) : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
('TTicket a : 'TPair 'TNat 'TNat : b)
('TOption ('TPair ('TTicket a) ('TTicket a)) : b)
AnnSPLIT_TICKET AnnVar
anns
AnnJOIN_TICKETS AnnVar
anns -> AnnVar
-> Instr
('TPair ('TTicket a) ('TTicket a) : (s ++ s))
('TOption ('TTicket a) : (s ++ s))
forall (a :: T) (b :: [T]).
AnnVar
-> Instr
('TPair ('TTicket a) ('TTicket a) : b) ('TOption ('TTicket a) : b)
AnnJOIN_TICKETS AnnVar
anns
AnnOPEN_CHEST AnnVar
anns -> AnnVar
-> Instr
('TChestKey : 'TChest : 'TNat : (s ++ s))
('TOr 'TBytes 'TBool : (s ++ s))
forall (a :: [T]).
AnnVar
-> Instr
('TChestKey : 'TChest : 'TNat : a) ('TOr 'TBytes 'TBool : a)
AnnOPEN_CHEST AnnVar
anns
AnnSAPLING_EMPTY_STATE AnnVar
anns Sing n
n -> AnnVar -> Sing n -> Instr (a ++ s) ('TSaplingState n : (a ++ s))
forall (a :: Peano) (s :: [T]).
AnnVar -> Sing a -> Instr s ('TSaplingState a : s)
AnnSAPLING_EMPTY_STATE AnnVar
anns Sing n
n
AnnSAPLING_VERIFY_UPDATE AnnVar
anns -> AnnVar
-> Instr
('TSaplingTransaction n : 'TSaplingState n : (s ++ s))
('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n)))
: (s ++ s))
forall (a :: Peano) (b :: [T]).
AnnVar
-> Instr
('TSaplingTransaction a : 'TSaplingState a : b)
('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState a))) : b)
AnnSAPLING_VERIFY_UPDATE AnnVar
anns
AnnMIN_BLOCK_TIME [AnyAnn]
anns -> [AnyAnn] -> Instr (a ++ s) ('TNat : (a ++ s))
forall (s :: [T]). [AnyAnn] -> Instr s ('TNat : s)
AnnMIN_BLOCK_TIME [AnyAnn]
anns
AnnEMIT AnnVar
anns FieldAnn
tag Maybe (Notes t)
ty -> AnnVar
-> FieldAnn
-> Maybe (Notes t)
-> Instr (t : (s ++ s)) ('TOperation : (s ++ s))
forall (a :: T) (b :: [T]).
PackedValScope a =>
AnnVar
-> FieldAnn -> Maybe (Notes a) -> Instr (a : b) ('TOperation : b)
AnnEMIT AnnVar
anns FieldAnn
tag Maybe (Notes t)
ty
AnnBYTES AnnVar
anns -> AnnVar -> Instr (n : (s ++ s)) ('TBytes : (s ++ s))
forall (a :: T) (b :: [T]).
ToBytesArithOp a =>
AnnVar -> Instr (a : b) ('TBytes : b)
AnnBYTES AnnVar
anns
AnnNAT AnnVar
anns -> AnnVar -> Instr ('TBytes : (s ++ s)) ('TNat : (s ++ s))
forall (a :: [T]). AnnVar -> Instr ('TBytes : a) ('TNat : a)
AnnNAT AnnVar
anns
where
go :: forall a' b'. Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go :: forall (a' :: [T]) (b' :: [T]).
Instr a' b' -> Instr (a' ++ s) (b' ++ s)
go = forall (s :: [T]) (a :: [T]) (b :: [T]).
Instr a b -> Instr (a ++ s) (b ++ s)
frameInstr @s
comment :: PrintComment a -> PrintComment (a ++ s)
comment :: PrintComment a -> PrintComment (a ++ s)
comment (PrintComment [Either Text (StackRef a)]
c) = [Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s)
forall (st :: [T]). [Either Text (StackRef st)] -> PrintComment st
PrintComment ([Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s))
-> [Either Text (StackRef (a ++ s))] -> PrintComment (a ++ s)
forall a b. (a -> b) -> a -> b
$ [Either Text (StackRef a)]
c [Either Text (StackRef a)]
-> (Either Text (StackRef a) -> Either Text (StackRef (a ++ s)))
-> [Either Text (StackRef (a ++ s))]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
Left Text
t -> Text -> Either Text (StackRef (a ++ s))
forall a b. a -> Either a b
Left Text
t
Right (StackRef PeanoNatural idx
n) -> StackRef (a ++ s) -> Either Text (StackRef (a ++ s))
forall a b. b -> Either a b
Right (StackRef (a ++ s) -> Either Text (StackRef (a ++ s)))
-> StackRef (a ++ s) -> Either Text (StackRef (a ++ s))
forall a b. (a -> b) -> a -> b
$ forall (st :: [T]) (a :: Peano).
RequireLongerThan st a =>
PeanoNatural a -> StackRef st
StackRef @(a ++ s) PeanoNatural idx
n
((IsLongerThan (a ++ s) idx ~ 'True) => StackRef (a ++ s))
-> (IsLongerThan (a ++ s) idx :~: 'True) -> StackRef (a ++ s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (a :: [T]) (s :: [T]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
forall {k} (a :: [k]) (s :: [k]) (n :: Peano).
(IsLongerThan a n ~ 'True) =>
PeanoNatural n -> IsLongerThan (a ++ s) n :~: 'True
isLongerThanExtThm @a @s PeanoNatural idx
n
deriveGADTNFData ''Instr
instance NFData (ExtInstr s)
instance NFData (TestAssert s) where
rnf :: TestAssert s -> ()
rnf (TestAssert Text
a PrintComment s
b Instr s ('TBool : out)
c) = (Text, PrintComment s, Instr s ('TBool : out)) -> ()
forall a. NFData a => a -> ()
rnf (Text
a, PrintComment s
b, Instr s ('TBool : out)
c)