{-# OPTIONS_GHC -Wno-orphans #-}
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
, 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
, READ_TICKET
, SPLIT_TICKET
, JOIN_TICKETS
, OPEN_CHEST
, SAPLING_EMPTY_STATE
, SAPLING_VERIFY_UPDATE
, MIN_BLOCK_TIME
)
, castInstr
, pattern (:#)
, ExtInstr (..)
, CommentType (..)
, StackRef (..)
, mkStackRef
, PrintComment (..)
, TestAssert (..)
, SomeMeta (..)
, pattern ConcreteMeta
, ConstraintDUPN
, ConstraintDUPN'
, ConstraintDIPN
, ConstraintDIPN'
, ConstraintDIG
, ConstraintDIG'
, ConstraintDUG
, ConstraintDUG'
, ConstraintPairN
, PairN
, RightComb
, ConstraintUnpairN
, UnpairN
, ConstraintGetN
, GetN
, ConstraintUpdateN
, UpdateN
) where
import Prelude hiding (EQ, GT, LT)
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, type (+))
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.Polymorphic
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.TypeLevel
(CombedPairLeafCount, CombedPairLeafCountIsAtLeast, CombedPairNodeCount,
CombedPairNodeIndexIsValid, IsPair)
import Morley.Michelson.Typed.Value (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 (If, KnownList, type (++))
import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)), TypeErrorUnless)
{-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-}
type ConstraintDUPN' kind (n :: Peano) (inp :: [kind]) (out :: [kind]) (a :: kind) =
( RequireLongerOrSameLength inp n, n > 'Z ~ 'True
, inp ~ (Take (Decrement n) inp ++ (a ': Drop n inp))
, out ~ (a ': inp)
)
type ConstraintDUPN n inp out a = ConstraintDUPN' T n inp out a
type ConstraintDIPN' kind (n :: Peano) (inp :: [kind])
(out :: [kind]) (s :: [kind]) (s' :: [kind]) =
( RequireLongerOrSameLength inp n
, ((Take n inp) ++ s) ~ inp
, ((Take n inp) ++ s') ~ out
)
type ConstraintDIPN n inp out s s' = ConstraintDIPN' T n inp out s s'
type ConstraintDIG' kind (n :: Peano) (inp :: [kind])
(out :: [kind]) (a :: kind) =
( KnownList inp
, RequireLongerThan inp n
, inp ~ (Take n inp ++ (a ': Drop ('S n) inp))
, out ~ (a ': Take n inp ++ Drop ('S n) inp)
)
type ConstraintDIG n inp out a = ConstraintDIG' T n inp out a
type ConstraintDUG' kind (n :: Peano) (inp :: [kind])
(out :: [kind]) (a :: kind) =
( RequireLongerThan out n
, inp ~ (a ': Drop ('S 'Z) inp)
, out ~ (Take n (Drop ('S 'Z) inp) ++ (a ': Drop ('S n) inp))
)
type ConstraintDUG n inp out a = ConstraintDUG' T n inp out a
type ConstraintPairN (n :: Peano) (inp :: [T]) =
( RequireLongerOrSameLength inp n
, TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")
)
type PairN (n :: Peano) (s :: [T]) = (RightComb (Take n s) ': Drop n s)
type family RightComb (s :: [T]) :: T where
RightComb '[ x, y ] = 'TPair x y
RightComb (x ': xs) = 'TPair x (RightComb xs)
type ConstraintUnpairN (n :: Peano) (pair :: T) =
( TypeErrorUnless (n >= ToPeano 2)
('Text "'UNPAIR n' expects n ≥ 2")
, TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair)
(If (IsPair pair)
('Text "'UNPAIR "
':<>: 'ShowType (FromPeano n)
':<>: 'Text "' expects a right-combed pair with at least "
':<>: 'ShowType (FromPeano n)
':<>: 'Text " elements at the top of the stack,"
':$$: 'Text "but the pair only contains "
':<>: 'ShowType (FromPeano (CombedPairLeafCount pair))
':<>: 'Text " elements.")
('Text "Expected a pair at the top of the stack, but found: "
':<>: 'ShowType pair
)
)
)
type family UnpairN (n :: Peano) (s :: T) :: [T] where
UnpairN ('S ('S 'Z)) ('TPair x y) = [x, y]
UnpairN ('S n) ('TPair x y) = x : UnpairN n y
type ConstraintGetN (ix :: Peano) (pair :: T) =
( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)
(If (IsPair pair)
('Text "'GET "
':<>: 'ShowType (FromPeano ix)
':<>: 'Text "' expects a right-combed pair with at least "
':<>: 'ShowType (FromPeano ix + 1)
':<>: 'Text " nodes at the top of the stack,"
':$$: 'Text "but the pair only contains "
':<>: 'ShowType (FromPeano (CombedPairNodeCount pair))
':<>: 'Text " nodes.")
('Text "Expected a pair at the top of the stack, but found: "
':<>: 'ShowType pair
)
)
)
type family GetN (ix :: Peano) (pair :: T) :: T where
GetN 'Z val = val
GetN ('S 'Z) ('TPair left _) = left
GetN ('S ('S n)) ('TPair _ right) = GetN n right
type ConstraintUpdateN (ix :: Peano) (pair :: T) =
( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)
(If (IsPair pair)
('Text "'UPDATE "
':<>: 'ShowType (FromPeano ix)
':<>: 'Text "' expects the 2nd element of the stack to be a right-combed pair with at least "
':<>: 'ShowType (FromPeano ix + 1)
':<>: 'Text " nodes,"
':$$: 'Text "but the pair only contains "
':<>: 'ShowType (FromPeano (CombedPairNodeCount pair))
':<>: 'Text " nodes.")
('Text "Expected the 2nd element of the stack to be a pair, but found: "
':<>: 'ShowType pair
)
)
)
type family UpdateN (ix :: Peano) (val :: T) (pair :: T) :: T where
UpdateN 'Z val _ = val
UpdateN ('S 'Z) val ('TPair _ right) = 'TPair val right
UpdateN ('S ('S n)) val ('TPair left right) = 'TPair left (UpdateN n val right)
data Instr (inp :: [T]) (out :: [T]) where
WithLoc :: ErrorSrcPos -> Instr a b -> Instr a b
Meta :: SomeMeta -> Instr a b -> Instr a b
FrameInstr
:: forall a b s.
(KnownList a, KnownList b)
=> Proxy s -> Instr a b -> Instr (a ++ s) (b ++ s)
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 :: (SingI e, Comparable e) => Anns '[TypeAnn, VarAnn, Notes e] -> Instr s ('TSet e ': s)
AnnEMPTY_MAP :: (SingI a, SingI b, Comparable a) => Anns '[TypeAnn, VarAnn, Notes a, Notes b] -> Instr s ('TMap a b ': s)
AnnEMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap 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]
-> Value' Instr ('TLambda i 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
:: UnaryArithOp Not n
=> AnnVar
-> Instr (n ': s) (UnaryArithRes Not n ': s)
AnnCOMPARE
:: (Comparable n, SingI 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)
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
:: (Comparable a)
=> AnnVar
-> Instr (a ': 'TNat ': s) ('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)
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 inp1 out1 -> Maybe (Instr inp1 out1)
forall a. a -> Maybe a
Just Instr inp1 out1
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 $b:# :: forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
$m:# :: forall {r} {a :: [T]} {c :: [T]}.
Instr a c
-> (forall {b :: [T]}. Instr a b -> Instr b c -> r)
-> (Void# -> r)
-> r
:# 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 -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== PeanoNatural idx -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
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
. Natural -> ShowS
forall a. Show a => a -> ShowS
T.shows (PeanoNatural idx -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat))
where
app_prec :: Int
app_prec = Int
10
instance Buildable (StackRef st) where
build :: StackRef st -> Builder
build (StackRef PeanoNatural idx
snat) = Builder
"StackRef {" Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| PeanoNatural idx -> Natural
forall (n :: Peano). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat Natural -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
"}"
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 n -> StackRef st
forall (st :: [T]) (a :: Peano).
RequireLongerThan st a =>
PeanoNatural a -> StackRef st
StackRef (PeanoNatural n -> StackRef st) -> PeanoNatural n -> 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
/= :: PrintComment st -> PrintComment st -> Bool
$c/= :: forall (st :: [T]). PrintComment st -> PrintComment st -> Bool
== :: PrintComment st -> PrintComment st -> Bool
$c== :: forall (st :: [T]). 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
showList :: [PrintComment st] -> ShowS
$cshowList :: forall (st :: [T]). [PrintComment st] -> ShowS
show :: PrintComment st -> String
$cshow :: forall (st :: [T]). PrintComment st -> String
showsPrec :: Int -> PrintComment st -> ShowS
$cshowsPrec :: forall (st :: [T]). Int -> 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
$cto :: forall (st :: [T]) x. Rep (PrintComment st) x -> PrintComment st
$cfrom :: forall (st :: [T]) x. PrintComment st -> Rep (PrintComment st) x
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
stimes :: forall b. Integral b => b -> PrintComment st -> PrintComment st
$cstimes :: forall (st :: [T]) b.
Integral b =>
b -> PrintComment st -> PrintComment st
sconcat :: NonEmpty (PrintComment st) -> PrintComment st
$csconcat :: forall (st :: [T]). NonEmpty (PrintComment st) -> PrintComment st
<> :: PrintComment st -> PrintComment st -> PrintComment st
$c<> :: forall (st :: [T]).
PrintComment st -> 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
mconcat :: [PrintComment st] -> PrintComment st
$cmconcat :: forall (st :: [T]). [PrintComment st] -> PrintComment st
mappend :: PrintComment st -> PrintComment st -> PrintComment st
$cmappend :: forall (st :: [T]).
PrintComment st -> PrintComment st -> PrintComment st
mempty :: PrintComment st
$cmempty :: forall (st :: [T]). 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)]
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
showList :: [CommentType] -> ShowS
$cshowList :: [CommentType] -> ShowS
show :: CommentType -> String
$cshow :: CommentType -> String
showsPrec :: Int -> CommentType -> ShowS
$cshowsPrec :: Int -> 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
$cto :: forall x. Rep CommentType x -> CommentType
$cfrom :: forall x. CommentType -> Rep CommentType x
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
showList :: [ExtInstr s] -> ShowS
$cshowList :: forall (s :: [T]). [ExtInstr s] -> ShowS
show :: ExtInstr s -> String
$cshow :: forall (s :: [T]). ExtInstr s -> String
showsPrec :: Int -> ExtInstr s -> ShowS
$cshowsPrec :: forall (s :: [T]). Int -> 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
$cto :: forall (s :: [T]) x. Rep (ExtInstr s) x -> ExtInstr s
$cfrom :: forall (s :: [T]) x. ExtInstr s -> Rep (ExtInstr s) x
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) -> (Void# -> r) -> r
ConcreteMeta meta instr <- Meta (SomeMeta (cast -> Just meta)) instr
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)
$