{-# OPTIONS_GHC -Wno-orphans #-}
module Michelson.Typed.Instr
( Instr (..)
, castInstr
, pattern (:#)
, ExtInstr (..)
, CommentType (..)
, StackRef (..)
, mkStackRef
, PrintComment (..)
, TestAssert (..)
, ContractCode
, Contract (..)
, defaultContract
, mapContractCode
, mapEntriesOrdered
, pattern CAR
, pattern CDR
, pattern LEFT
, pattern PAIR
, pattern RIGHT
, pattern UNPAIR
, ConstraintDUPN
, ConstraintDUPN'
, ConstraintDIPN
, ConstraintDIPN'
, ConstraintDIG
, ConstraintDIG'
, ConstraintDUG
, ConstraintDUG'
, ConstraintPairN
, PairN
, RightComb
, ConstraintUnpairN
, UnpairN
, ConstraintGetN
, GetN
, ConstraintUpdateN
, UpdateN
) where
import Data.Default
import Data.Singletons (Sing)
import Data.Type.Equality ((:~:)(..))
import Data.Vinyl (RMap, Rec(..), RecordToList, ReifyConstraint(..))
import Fmt ((+||), (||+))
import GHC.TypeNats (type (+))
import qualified GHC.TypeNats as GHC (Nat)
import qualified Text.Show
import Michelson.Doc
import Michelson.ErrorPos
import Michelson.Typed.Annotation (Notes(..), starNotes)
import Michelson.Typed.Arith
import Michelson.Typed.Entrypoints
import Michelson.Typed.Polymorphic
import Michelson.Typed.Scope
import Michelson.Typed.T (T(..))
import Michelson.Typed.TypeLevel
(CombedPairLeafCount, CombedPairLeafCountIsAtLeast, CombedPairNodeCount,
CombedPairNodeIndexIsValid, IsPair)
import Michelson.Typed.Value (Comparable, ContractInp, ContractOut, Value'(..))
import Michelson.Untyped
(Annotation(..), EntriesOrder(..), FieldAnn, StackFn, StackTypePattern, TypeAnn, VarAnn, VarAnns,
entriesOrderToInt)
import Util.Peano
import Util.PeanoNatural
import Util.Sing (eqI)
import Util.TH
import Util.Type (If, KnownList, type (++))
import Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)), TypeErrorUnless)
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) =
( 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 :: InstrCallStack -> Instr a b -> Instr a b
InstrWithNotes
:: forall a (topElems :: [T]) (s :: [T]).
( RMap topElems
, RecordToList topElems
, ReifyConstraint Show Notes topElems
, ReifyConstraint NFData Notes topElems
, Each '[ SingI ] topElems
)
=> Proxy s -> Rec Notes topElems
-> Instr a (topElems ++ s) -> Instr a (topElems ++ s)
InstrWithVarNotes :: NonEmpty VarAnn -> Instr a b -> Instr a b
InstrWithVarAnns :: VarAnns -> 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
Fn :: Text -> StackFn -> Instr inp out -> Instr inp out
AnnCAR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': s)
AnnCDR :: VarAnn -> FieldAnn -> Instr ('TPair a b ': s) (b ': s)
DROP :: Instr (a ': s) s
DROPN
:: forall (n :: Peano) s.
(RequireLongerOrSameLength s n, NFData (Sing n))
=> PeanoNatural n -> Instr s (Drop n s)
DUP :: DupableScope a => Instr (a ': s) (a ': a ': s)
DUPN
:: forall (n :: Peano) inp out a. (ConstraintDUPN n inp out a, DupableScope a, NFData (Sing n))
=> 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, NFData (Sing n))
=> PeanoNatural n -> Instr inp out
DUG
:: forall (n :: Peano) inp out a. (ConstraintDUG n inp out a, NFData (Sing n))
=> PeanoNatural n -> Instr inp out
PUSH
:: forall t s . ConstantScope t
=> Value' Instr t -> Instr s (t ': s)
SOME :: Instr (a ': s) ('TOption a ': s)
NONE :: forall a s . SingI a => Instr s ('TOption a ': s)
UNIT :: Instr s ('TUnit ': s)
IF_NONE
:: Instr s s'
-> Instr (a ': s) s'
-> Instr ('TOption a ': s) s'
AnnPAIR :: TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': b ': s) ('TPair a b ': s)
AnnUNPAIR :: VarAnn -> VarAnn -> FieldAnn -> FieldAnn -> Instr ('TPair a b ': s) (a ': b ': s)
PAIRN
:: forall n inp. ConstraintPairN n inp
=> 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 => TypeAnn -> FieldAnn -> FieldAnn -> Instr (a ': s) ('TOr a b ': s)
AnnRIGHT :: SingI a => TypeAnn -> FieldAnn -> FieldAnn -> Instr (b ': s) ('TOr a b ': s)
IF_LEFT
:: Instr (a ': s) s'
-> Instr (b ': s) s'
-> Instr ('TOr a b ': s) s'
NIL :: SingI p => Instr s ('TList p ': s)
CONS :: Instr (a ': 'TList a ': s) ('TList a ': s)
IF_CONS
:: Instr (a ': 'TList a ': s) s'
-> Instr s s'
-> Instr ('TList a ': s) s'
SIZE :: SizeOp c => Instr (c ': s) ('TNat ': s)
EMPTY_SET :: (SingI e, Comparable e) => Instr s ('TSet e ': s)
EMPTY_MAP :: (SingI a, SingI b, Comparable a) => Instr s ('TMap a b ': s)
EMPTY_BIG_MAP :: (SingI a, SingI b, Comparable a, HasNoBigMap b) => Instr s ('TBigMap a b ': s)
MAP :: (MapOp c, SingI b)
=> 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
MEM :: MemOp c => Instr (MemOpKey c ': c ': s) ('TBool ': s)
GET
:: (GetOp c, SingI (GetOpVal c))
=> Instr (GetOpKey c ': c ': s) ('TOption (GetOpVal c) ': s)
GETN
:: forall (ix :: Peano) (pair :: T) (s :: [T]).
ConstraintGetN ix pair
=> PeanoNatural ix
-> Instr (pair : s) (GetN ix pair ': s)
UPDATE
:: UpdOp c
=> Instr (UpdOpKey c ': UpdOpParams c ': c ': s) (c ': s)
UPDATEN
:: forall (ix :: Peano) (val :: T) (pair :: T) (s :: [T]).
ConstraintUpdateN ix pair
=> PeanoNatural ix
-> Instr (val : pair : s) (UpdateN ix val pair ': s)
GET_AND_UPDATE
:: ( GetOp c, UpdOp c, SingI (GetOpVal c)
, UpdOpKey c ~ GetOpKey c
)
=> 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)
LAMBDA :: forall i o s . (SingI i, SingI o)
=> Value' Instr ('TLambda i o) -> Instr s ('TLambda i o ': s)
EXEC :: Instr (t1 ': 'TLambda t1 t2 ': s) (t2 ': s)
APPLY
:: forall a b c s . (ConstantScope a, SingI b)
=> 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', (NFData (Sing n)))
=> PeanoNatural n -> Instr s s' -> Instr inp out
FAILWITH :: (SingI a, ConstantScope a) => Instr (a ': s) t
CAST :: forall a s . SingI a => Instr (a ': s) (a ': s)
RENAME :: Instr (a ': s) (a ': s)
PACK :: PackedValScope a => Instr (a ': s) ('TBytes ': s)
UNPACK :: (UnpackedValScope a, SingI a) => Instr ('TBytes ': s) ('TOption a ': s)
CONCAT :: ConcatOp c => Instr (c ': c ': s) (c ': s)
CONCAT' :: ConcatOp c => Instr ('TList c ': s) (c ': s)
SLICE
:: (SliceOp c, SingI c)
=> Instr ('TNat ': 'TNat ': c ': s) ('TOption c ': s)
ISNAT :: Instr ('TInt ': s) ('TOption ('TNat) ': s)
ADD
:: ArithOp Add n m
=> Instr (n ': m ': s) (ArithRes Add n m ': s)
SUB
:: ArithOp Sub n m
=> Instr (n ': m ': s) (ArithRes Sub n m ': s)
MUL
:: ArithOp Mul n m
=> Instr (n ': m ': s) (ArithRes Mul n m ': s)
EDIV
:: EDivOp n m
=> Instr (n ': m ': s)
(('TOption ('TPair (EDivOpRes n m)
(EModOpRes n m))) ': s)
ABS
:: UnaryArithOp Abs n
=> Instr (n ': s) (UnaryArithRes Abs n ': s)
NEG
:: UnaryArithOp Neg n
=> Instr (n ': s) (UnaryArithRes Neg n ': s)
LSL
:: ArithOp Lsl n m
=> Instr (n ': m ': s) (ArithRes Lsl n m ': s)
LSR
:: ArithOp Lsr n m
=> Instr (n ': m ': s) (ArithRes Lsr n m ': s)
OR
:: ArithOp Or n m
=> Instr (n ': m ': s) (ArithRes Or n m ': s)
AND
:: ArithOp And n m
=> Instr (n ': m ': s) (ArithRes And n m ': s)
XOR
:: ArithOp Xor n m
=> Instr (n ': m ': s) (ArithRes Xor n m ': s)
NOT
:: UnaryArithOp Not n
=> Instr (n ': s) (UnaryArithRes Not n ': s)
COMPARE
:: (Comparable n, SingI n)
=> Instr (n ': n ': s) ('TInt ': s)
EQ
:: UnaryArithOp Eq' n
=> Instr (n ': s) (UnaryArithRes Eq' n ': s)
NEQ
:: UnaryArithOp Neq n
=> Instr (n ': s) (UnaryArithRes Neq n ': s)
LT
:: UnaryArithOp Lt n
=> Instr (n ': s) (UnaryArithRes Lt n ': s)
GT
:: UnaryArithOp Gt n
=> Instr (n ': s) (UnaryArithRes Gt n ': s)
LE
:: UnaryArithOp Le n
=> Instr (n ': s) (UnaryArithRes Le n ': s)
GE
:: UnaryArithOp Ge n
=> Instr (n ': s) (UnaryArithRes Ge n ': s)
INT
:: ToIntArithOp n
=> Instr (n ': s) ('TInt ': s)
SELF
:: forall (arg :: T) s .
(ParameterScope arg)
=> SomeEntrypointCallT arg
-> Instr s ('TContract arg ': s)
CONTRACT
:: (ParameterScope p)
=> Notes p
-> EpName
-> Instr ('TAddress ': s) ('TOption ('TContract p) ': s)
TRANSFER_TOKENS
:: (ParameterScope p) =>
Instr (p ': 'TMutez ': 'TContract p ': s)
('TOperation ': s)
SET_DELEGATE
:: Instr ('TOption 'TKeyHash ': s) ('TOperation ': s)
CREATE_CONTRACT
:: (ParameterScope p, StorageScope g)
=> Contract p g
-> Instr ('TOption 'TKeyHash ':
'TMutez ':
g ': s)
('TOperation ': 'TAddress ': s)
IMPLICIT_ACCOUNT
:: Instr ('TKeyHash ': s) ('TContract 'TUnit ': s)
NOW :: Instr s ('TTimestamp ': s)
AMOUNT :: Instr s ('TMutez ': s)
BALANCE :: Instr s ('TMutez ': s)
VOTING_POWER :: Instr ('TKeyHash ': s) ('TNat ': s)
TOTAL_VOTING_POWER :: Instr s ('TNat ': s)
CHECK_SIGNATURE
:: Instr ('TKey ': 'TSignature ': 'TBytes ': s)
('TBool ': s)
SHA256 :: Instr ('TBytes ': s) ('TBytes ': s)
SHA512 :: Instr ('TBytes ': s) ('TBytes ': s)
BLAKE2B :: Instr ('TBytes ': s) ('TBytes ': s)
SHA3 :: Instr ('TBytes ': s) ('TBytes ': s)
KECCAK :: Instr ('TBytes ': s) ('TBytes ': s)
HASH_KEY :: Instr ('TKey ': s) ('TKeyHash ': s)
PAIRING_CHECK
:: Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) ': s) ('TBool ': s)
SOURCE :: Instr s ('TAddress ': s)
SENDER :: Instr s ('TAddress ': s)
ADDRESS :: Instr ('TContract a ': s) ('TAddress ': s)
CHAIN_ID :: Instr s ('TChainId ': s)
LEVEL :: Instr s ('TNat ': s)
SELF_ADDRESS :: Instr s ('TAddress ': s)
NEVER :: Instr ('TNever ': s) t
TICKET
:: (Comparable a)
=> Instr (a ': 'TNat ': s) ('TTicket a ': s)
READ_TICKET
:: Instr ('TTicket a ': s)
(RightComb ['TAddress, a, 'TNat] ': 'TTicket a ': s)
SPLIT_TICKET
:: Instr ('TTicket a ': 'TPair 'TNat 'TNat ': s)
('TOption ('TPair ('TTicket a) ('TTicket a)) ': s)
JOIN_TICKETS
:: Instr ('TPair ('TTicket a) ('TTicket a) ': s)
('TOption ('TTicket a) ': s)
castInstr
:: forall inp1 out1 inp2 out2.
( SingI inp1
, SingI out1
, SingI inp2
, SingI out2
)
=> Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr :: Instr inp1 out1 -> Maybe (Instr inp2 out2)
castInstr Instr inp1 out1
instr =
case ((SingI inp1, SingI inp2, TestEquality Sing) =>
Maybe (inp1 :~: inp2)
forall k (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @inp1 @inp2, (SingI out1, SingI out2, TestEquality Sing) =>
Maybe (out1 :~: out2)
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:# :: 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]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b 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
pattern CAR :: () => (i ~ ('TPair a b : s), o ~ (a : s)) => Instr i o
pattern $bCAR :: Instr i o
$mCAR :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : s)) =>
r)
-> (Void# -> r)
-> r
CAR = AnnCAR (UnsafeAnnotation "") (UnsafeAnnotation "")
pattern CDR :: () => (i ~ ('TPair a b : s), o ~ (b : s)) => Instr i o
pattern $bCDR :: Instr i o
$mCDR :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
r)
-> (Void# -> r)
-> r
CDR = AnnCDR (UnsafeAnnotation "") (UnsafeAnnotation "")
pattern UNPAIR :: () => (i ~ ('TPair a b : s), o ~ (a : b : s)) => Instr i o
pattern $bUNPAIR :: Instr i o
$mUNPAIR :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
r)
-> (Void# -> r)
-> r
UNPAIR = AnnUNPAIR (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")
pattern PAIR :: () => (i ~ (a ': b ': s), o ~ ('TPair a b ': s)) => Instr i o
pattern $bPAIR :: Instr i o
$mPAIR :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]).
(i ~ (a : b : s), o ~ ('TPair a b : s)) =>
r)
-> (Void# -> r)
-> r
PAIR = AnnPAIR (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")
pattern LEFT :: () => (SingI b, i ~ (a ': s), o ~ ('TOr a b ': s)) => Instr i o
pattern $bLEFT :: Instr i o
$mLEFT :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (b :: T) (a :: T) (s :: [T]).
(SingI b, i ~ (a : s), o ~ ('TOr a b : s)) =>
r)
-> (Void# -> r)
-> r
LEFT = AnnLEFT (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")
pattern RIGHT :: () => (SingI a, i ~ (b ': s), o ~ ('TOr a b ': s)) => Instr i o
pattern $bRIGHT :: Instr i o
$mRIGHT :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]).
(SingI a, i ~ (b : s), o ~ ('TOr a b : s)) =>
r)
-> (Void# -> r)
-> r
RIGHT = AnnRIGHT (UnsafeAnnotation "") (UnsafeAnnotation "") (UnsafeAnnotation "")
data TestAssert (s :: [T]) where
TestAssert
:: (SingI out)
=> Text
-> PrintComment inp
-> Instr inp ('TBool ': out)
-> TestAssert inp
deriving stock instance Show (TestAssert 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)
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 :: Nat). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat1 Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== PeanoNatural idx -> Natural
forall (n :: Nat). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat2
instance Show (StackRef st) where
show :: StackRef st -> String
show (StackRef PeanoNatural idx
snat) = Builder
"StackRef {" Builder -> Builder -> String
forall b. FromBuilder b => Builder -> Builder -> b
+|| PeanoNatural idx -> Natural
forall (n :: Nat). PeanoNatural n -> Natural
fromPeanoNatural PeanoNatural idx
snat Natural -> Builder -> Builder
forall a b. (Show a, FromBuilder b) => a -> Builder -> b
||+ Builder
"}"
mkStackRef
:: forall (gn :: GHC.Nat) st n.
(n ~ ToPeano gn, SingI (ToPeano gn), RequireLongerThan st n)
=> StackRef st
mkStackRef :: StackRef st
mkStackRef = PeanoNatural n -> StackRef st
forall (st :: [T]) (idx :: Nat).
RequireLongerThan st idx =>
PeanoNatural idx -> StackRef st
StackRef (PeanoNatural n -> StackRef st) -> PeanoNatural n -> StackRef st
forall a b. (a -> b) -> a -> b
$ SingI (ToPeano gn) => PeanoNatural (ToPeano gn)
forall (n :: Nat). SingI (ToPeano 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 (b -> PrintComment st -> PrintComment st
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 :: 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
$cp1Monoid :: forall (st :: [T]). Semigroup (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
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)
instance NFData (ExtInstr s)
type ContractCode cp st = Instr (ContractInp cp st) (ContractOut st)
data Contract cp st = (ParameterScope cp, StorageScope st) => Contract
{ Contract cp st -> ContractCode cp st
cCode :: ContractCode cp st
, Contract cp st -> ParamNotes cp
cParamNotes :: ParamNotes cp
, Contract cp st -> Notes st
cStoreNotes :: Notes st
, Contract cp st -> EntriesOrder
cEntriesOrder :: EntriesOrder
}
deriving stock instance Show (Contract cp st)
deriving stock instance Eq (ContractCode cp st) => Eq (Contract cp st)
instance NFData (Contract cp st) where
rnf :: Contract cp st -> ()
rnf (Contract ContractCode cp st
a ParamNotes cp
b Notes st
c EntriesOrder
d) = (ContractCode cp st, ParamNotes cp, Notes st, EntriesOrder) -> ()
forall a. NFData a => a -> ()
rnf (ContractCode cp st
a, ParamNotes cp
b, Notes st
c, EntriesOrder
d)
defaultContract :: (ParameterScope cp, StorageScope st) => ContractCode cp st -> Contract cp st
defaultContract :: ContractCode cp st -> Contract cp st
defaultContract ContractCode cp st
code = Contract :: forall (cp :: T) (st :: T).
(ParameterScope cp, StorageScope st) =>
ContractCode cp st
-> ParamNotes cp -> Notes st -> EntriesOrder -> Contract cp st
Contract
{ cCode :: ContractCode cp st
cCode = ContractCode cp st
code
, cParamNotes :: ParamNotes cp
cParamNotes = ParamNotes cp
forall (t :: T). SingI t => ParamNotes t
starParamNotes
, cStoreNotes :: Notes st
cStoreNotes = Notes st
forall (t :: T). SingI t => Notes t
starNotes
, cEntriesOrder :: EntriesOrder
cEntriesOrder = EntriesOrder
forall a. Default a => a
def
}
mapContractCode
:: (ContractCode cp st -> ContractCode cp st)
-> Contract cp st
-> Contract cp st
mapContractCode :: (ContractCode cp st -> ContractCode cp st)
-> Contract cp st -> Contract cp st
mapContractCode ContractCode cp st -> ContractCode cp st
f Contract cp st
contract = Contract cp st
contract { cCode :: ContractCode cp st
cCode = ContractCode cp st -> ContractCode cp st
f (ContractCode cp st -> ContractCode cp st)
-> ContractCode cp st -> ContractCode cp st
forall a b. (a -> b) -> a -> b
$ Contract cp st -> ContractCode cp st
forall (cp :: T) (st :: T). Contract cp st -> ContractCode cp st
cCode Contract cp st
contract }
mapEntriesOrdered
:: Contract cp st
-> (ParamNotes cp -> a)
-> (Notes st -> a)
-> (ContractCode cp st -> a)
-> [a]
mapEntriesOrdered :: Contract cp st
-> (ParamNotes cp -> a)
-> (Notes st -> a)
-> (ContractCode cp st -> a)
-> [a]
mapEntriesOrdered Contract{EntriesOrder
Notes st
ParamNotes cp
ContractCode cp st
cEntriesOrder :: EntriesOrder
cStoreNotes :: Notes st
cParamNotes :: ParamNotes cp
cCode :: ContractCode cp st
cEntriesOrder :: forall (cp :: T) (st :: T). Contract cp st -> EntriesOrder
cStoreNotes :: forall (cp :: T) (st :: T). Contract cp st -> Notes st
cParamNotes :: forall (cp :: T) (st :: T). Contract cp st -> ParamNotes cp
cCode :: forall (cp :: T) (st :: T). Contract cp st -> ContractCode cp st
..} ParamNotes cp -> a
fParam Notes st -> a
fStorage ContractCode cp st -> a
fCode =
((Int, a) -> a) -> [(Int, a)] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, a) -> a
forall a b. (a, b) -> b
snd
([(Int, a)] -> [a]) -> [(Int, a)] -> [a]
forall a b. (a -> b) -> a -> b
$ ((Int, a) -> Int) -> [(Int, a)] -> [(Int, a)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortWith (Int, a) -> Int
forall a b. (a, b) -> a
fst
[ (Int
paramPos, ParamNotes cp -> a
fParam ParamNotes cp
cParamNotes)
, (Int
storagePos, Notes st -> a
fStorage Notes st
cStoreNotes)
, (Int
codePos, ContractCode cp st -> a
fCode ContractCode cp st
cCode)
]
where
(Int
paramPos, Int
storagePos, Int
codePos) = EntriesOrder -> (Int, Int, Int)
entriesOrderToInt EntriesOrder
cEntriesOrder
$(deriveGADTNFData ''Instr)