{-# OPTIONS_GHC -fno-warn-orphans #-}
module Michelson.Typed.Convert
( convertContract
, convertFullContract
, instrToOps
, untypeValue
) where
import qualified Data.Map as Map
import Data.Singletons (SingI(sing), demote)
import Fmt (Buildable(..), pretty)
import Michelson.Text
import Michelson.Typed.Annotation (Notes(..))
import Michelson.Typed.CValue
import Michelson.Typed.EntryPoints
import Michelson.Typed.Extract (mkUType, toUType)
import Michelson.Typed.Instr as Instr
import Michelson.Typed.Scope
import Michelson.Typed.Sing (Sing(..))
import Michelson.Typed.T (CT(..), T(..))
import Michelson.Typed.Value
import qualified Michelson.Untyped as U
import Tezos.Core (mformatChainId, unMutez)
import Tezos.Crypto (mformatKeyHash, mformatPublicKey, mformatSignature)
import Util.Peano
import Util.Typeable
convertContract
:: forall param store . (SingI param, SingI store)
=> Contract param store -> U.Contract
convertContract contract =
U.Contract
{ para = untypeDemoteT @param
, stor = untypeDemoteT @store
, code = instrToOps contract
}
addCtNote :: U.TypeAnn -> U.Comparable -> U.Comparable
addCtNote ta (U.Comparable ct _) = U.Comparable ct ta
convertFullContract
:: forall param store . (SingI param, SingI store)
=> FullContract param store -> U.Contract
convertFullContract fc =
let c = convertContract (fcCode fc)
in c { U.para = mkUType sing (fcParamNotes fc)
, U.stor = mkUType sing (fcStoreNotes fc) }
untypeValue ::
forall t . (SingI t, HasNoOp t)
=> Value' Instr t
-> U.Value
untypeValue val = case (val, sing @t) of
(VC cVal, _) ->
untypeCValue cVal
(VKey b, _) ->
U.ValueString $ mformatPublicKey b
(VUnit, _) ->
U.ValueUnit
(VSignature b, _) ->
U.ValueString $ mformatSignature b
(VChainId b, _) ->
U.ValueString $ mformatChainId b
(VOption (Just x), STOption _) ->
U.ValueSome (untypeValue x)
(VOption Nothing, STOption _) ->
U.ValueNone
(VList l, STList _) ->
vList U.ValueSeq $ map untypeValue l
(VSet s, _) ->
vList U.ValueSeq $ map untypeCValue $ toList s
(VContract addr sepc, _) ->
U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)
(VPair (l, r), STPair lt _) ->
case checkOpPresence lt of
OpAbsent -> U.ValuePair (untypeValue l) (untypeValue r)
(VOr (Left x), STOr lt _) ->
case checkOpPresence lt of
OpAbsent -> U.ValueLeft (untypeValue x)
(VOr (Right x), STOr lt _) ->
case checkOpPresence lt of
OpAbsent -> U.ValueRight (untypeValue x)
(VLam (rfAnyInstr -> ops :: Instr '[inp] '[out]), _) ->
vList U.ValueLambda $ instrToOps ops
(VMap m, STMap _ vt) ->
case checkOpPresence vt of
OpAbsent ->
vList U.ValueMap $ Map.toList m <&> \(k, v) ->
U.Elt (untypeCValue k) (untypeValue v)
(VBigMap m, STBigMap _ vt) ->
case checkOpPresence vt of
OpAbsent ->
vList U.ValueMap $ Map.toList m <&> \(k, v) ->
U.Elt (untypeCValue k) (untypeValue v)
where
vList ctor = maybe U.ValueNil ctor . nonEmpty
untypeDemoteT :: forall (t :: T). SingI t => U.Type
untypeDemoteT = toUType $ demote @t
untypeCValue :: CValue t -> U.Value
untypeCValue cVal = case cVal of
CvInt i -> U.ValueInt i
CvNat i -> U.ValueInt $ toInteger i
CvString s -> U.ValueString s
CvBytes b -> U.ValueBytes $ U.InternalByteString b
CvMutez m -> U.ValueInt $ toInteger $ unMutez m
CvBool True -> U.ValueTrue
CvBool False -> U.ValueFalse
CvKeyHash h -> U.ValueString $ mformatKeyHash h
CvTimestamp t -> U.ValueString $ mkMTextUnsafe $ pretty t
CvAddress a -> U.ValueString $ mformatEpAddress a
instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOps = \case
Nop -> []
Seq i1 i2 -> instrToOps i1 <> instrToOps i2
Nested sq -> one $ U.SeqEx $ instrToOps sq
DocGroup _ sq -> instrToOps sq
Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
FrameInstr _ i -> instrToOps i
InstrWithNotes n i -> case i of
Nop -> instrToOps i
Seq _ _ -> instrToOps i
Nested _ -> instrToOps i
DocGroup _ _ -> instrToOps i
Ext _ -> instrToOps i
InstrWithNotes _ _ -> instrToOps i
InstrWithVarNotes _ _ -> instrToOps i
_ -> [U.PrimEx $ handleInstrAnnotate i n]
InstrWithVarNotes n i -> case i of
Nop -> instrToOps i
Seq _ _ -> instrToOps i
Nested _ -> instrToOps i
DocGroup _ _ -> instrToOps i
Ext _ -> instrToOps i
InstrWithNotes _ _ -> instrToOps i
InstrWithVarNotes _ _ -> instrToOps i
_ -> [U.PrimEx $ handleInstrVarNotes i n]
i -> [U.PrimEx $ handleInstr i]
where
handleInstrAnnotate
:: forall inp' out' . HasCallStack
=> Instr inp' out' -> PackedNotes out' -> U.ExpandedInstr
handleInstrAnnotate ins' (PackedNotes notes' sing') = let
x = handleInstr ins' in addInstrNote x sing' notes'
where
addInstrNote
:: HasCallStack
=> U.ExpandedInstr -> Sing t -> Notes t -> U.ExpandedInstr
addInstrNote ins s nte = case (s, ins, nte) of
(_, U.PUSH va _ v, _) -> U.PUSH va (mkUType s nte) v
(_, U.SOME _ va, NTOption ta _) -> U.SOME ta va
(STOption sp, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType sp nt)
(_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va
(_, U.PAIR _ va _ _, NTPair ta f1 f2 _ _) -> U.PAIR ta va f1 f2
(_, U.CAR va f1, _) -> U.CAR va f1
(_, U.CDR va f1, _) -> U.CDR va f1
(STOr _ sq, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) ->
U.LEFT ta va f1 f2 (mkUType sq n2)
(STOr sp _, U.RIGHT _ va _ _ _, NTOr ta f1 f2 n1 _) ->
U.RIGHT ta va f1 f2 (mkUType sp n1)
(STList sp, U.NIL _ va _, NTList ta n) -> U.NIL ta va (mkUType sp n)
(_, U.EMPTY_SET _ va ct, NTSet ta1 ta2) ->
U.EMPTY_SET ta1 va (addCtNote ta2 ct)
(STMap _ sq, U.EMPTY_MAP _ va ct _, NTMap ta1 ta2 n) ->
U.EMPTY_MAP ta1 va (addCtNote ta2 ct) (mkUType sq n)
(STBigMap _ sq, U.EMPTY_BIG_MAP _ va ct _, NTBigMap ta1 ta2 n) ->
U.EMPTY_BIG_MAP ta1 va (addCtNote ta2 ct) (mkUType sq n)
(STLambda sp sq, U.LAMBDA va _ _ ops, NTLambda _ n1 n2) ->
U.LAMBDA va (mkUType sp n1) (mkUType sq n2) ops
(_, U.CAST va _, n) -> U.CAST va (mkUType s n)
(STOption sp, U.UNPACK _ va _, NTOption ta nt) -> U.UNPACK ta va (mkUType sp nt)
(STOption (STContract sp), U.CONTRACT va fa _, NTOption _ (NTContract _ nt)) ->
U.CONTRACT va fa (mkUType sp nt)
(_, U.CONTRACT va fa t, NTOption _ _) -> U.CONTRACT va fa t
(_, a@(U.APPLY {}), _) -> a
(_, a@(U.CHAIN_ID {}), _) -> a
(_, a@(U.EXT _), _) -> a
(_, a@(U.DROP), _) -> a
(_, a@(U.DROPN _), _) -> a
(_, a@(U.DUP _), _) -> a
(_, a@(U.SWAP), _) -> a
(_, a@(U.DIG {}), _) -> a
(_, a@(U.DUG {}), _) -> a
(_, a@(U.IF_NONE _ _), _) -> a
(_, a@(U.CONS _), _) -> a
(_, a@(U.IF_LEFT _ _), _) -> a
(_, a@(U.IF_CONS _ _), _) -> a
(_, a@(U.SIZE _), _) -> a
(_, a@(U.MAP _ _), _) -> a
(_, a@(U.ITER _), _) -> a
(_, a@(U.MEM _), _) -> a
(_, a@(U.GET _), _) -> a
(_, a@(U.UPDATE _), _) -> a
(_, a@(U.IF _ _), _) -> a
(_, a@(U.LOOP _), _) -> a
(_, a@(U.LOOP_LEFT _), _) -> a
(_, a@(U.EXEC _), _) -> a
(_, a@(U.DIP _), _) -> a
(_, a@(U.DIPN {}), _) -> a
(_, a@(U.FAILWITH), _) -> a
(_, a@(U.RENAME _), _) -> a
(_, a@(U.PACK _), _) -> a
(_, a@(U.CONCAT _), _) -> a
(_, a@(U.SLICE _), _) -> a
(_, a@(U.ISNAT _), _) -> a
(_, a@(U.ADD _), _) -> a
(_, a@(U.SUB _), _) -> a
(_, a@(U.MUL _), _) -> a
(_, a@(U.EDIV _), _) -> a
(_, a@(U.ABS _), _) -> a
(_, a@(U.NEG _), _) -> a
(_, a@(U.LSL _), _) -> a
(_, a@(U.LSR _), _) -> a
(_, a@(U.OR _), _) -> a
(_, a@(U.AND _), _) -> a
(_, a@(U.XOR _), _) -> a
(_, a@(U.NOT _), _) -> a
(_, a@(U.COMPARE _), _) -> a
(_, a@(U.EQ _), _) -> a
(_, a@(U.NEQ _), _) -> a
(_, a@(U.LT _), _) -> a
(_, a@(U.GT _), _) -> a
(_, a@(U.LE _), _) -> a
(_, a@(U.GE _), _) -> a
(_, a@(U.INT _), _) -> a
(_, a@(U.SELF _ _), _) -> a
(_, a@(U.TRANSFER_TOKENS _), _) -> a
(_, a@(U.SET_DELEGATE _), _) -> a
(_, a@(U.CREATE_CONTRACT {}), _) -> a
(_, a@(U.IMPLICIT_ACCOUNT _), _) -> a
(_, a@(U.NOW _), _) -> a
(_, a@(U.AMOUNT _), _) -> a
(_, a@(U.BALANCE _), _) -> a
(_, a@(U.CHECK_SIGNATURE _), _) -> a
(_, a@(U.SHA256 _), _) -> a
(_, a@(U.SHA512 _), _) -> a
(_, a@(U.BLAKE2B _), _) -> a
(_, a@(U.HASH_KEY _), _) -> a
(_, a@(U.STEPS_TO_QUOTA _), _) -> a
(_, a@(U.SOURCE _), _) -> a
(_, a@(U.SENDER _), _) -> a
(_, a@(U.ADDRESS _), _) -> a
(_, b, c) -> error $ "addInstrNote: Unexpected instruction/annotation combination: " <> show (b, c)
handleInstrVarNotes :: forall inp' out' . HasCallStack
=> Instr inp' out' -> NonEmpty U.VarAnn -> U.ExpandedInstr
handleInstrVarNotes ins' varAnns =
let x = handleInstr ins' in addVarNotes x varAnns
where
addVarNotes
:: HasCallStack
=> U.ExpandedInstr -> NonEmpty U.VarAnn -> U.ExpandedInstr
addVarNotes ins varNotes = case varNotes of
va1 :| [va2] -> case ins of
U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va1 va2 c
_ -> error $
"addVarNotes: Cannot add two var annotations to instr: " <> show ins
va :| [] -> case ins of
U.DUP _ -> U.DUP va
U.PUSH _ t v -> U.PUSH va t v
U.SOME ta _ -> U.SOME ta va
U.NONE ta _ t -> U.NONE ta va t
U.UNIT ta _ -> U.UNIT ta va
U.PAIR ta _ fa1 fa2 -> U.PAIR ta va fa1 fa2
U.CAR _ fa -> U.CAR va fa
U.CDR _ fa -> U.CDR va fa
U.LEFT ta _ fa1 fa2 t -> U.LEFT ta va fa1 fa2 t
U.RIGHT ta _ fa1 fa2 t -> U.RIGHT ta va fa1 fa2 t
U.NIL ta _ t -> U.NIL ta va t
U.CONS _ -> U.CONS va
U.SIZE _ -> U.SIZE va
U.EMPTY_SET ta _ c -> U.EMPTY_SET ta va c
U.EMPTY_MAP ta _ c t -> U.EMPTY_MAP ta va c t
U.EMPTY_BIG_MAP ta _ c t -> U.EMPTY_BIG_MAP ta va c t
U.MAP _ ops -> U.MAP va ops
U.MEM _ -> U.MEM va
U.GET _ -> U.GET va
U.UPDATE _ -> U.UPDATE va
U.LAMBDA _ t1 t2 ops -> U.LAMBDA va t1 t2 ops
U.EXEC _ -> U.EXEC va
U.APPLY _ -> U.APPLY va
U.CAST _ t -> U.CAST va t
U.RENAME _ -> U.RENAME va
U.PACK _ -> U.PACK va
U.UNPACK ta _ t -> U.UNPACK ta va t
U.CONCAT _ -> U.CONCAT va
U.SLICE _ -> U.SLICE va
U.ISNAT _ -> U.ISNAT va
U.ADD _ -> U.ADD va
U.SUB _ -> U.MUL va
U.MUL _ -> U.MUL va
U.EDIV _ -> U.EDIV va
U.ABS _ -> U.ABS va
U.NEG _ -> U.NEG va
U.LSL _ -> U.LSL va
U.LSR _ -> U.LSR va
U.OR _ -> U.OR va
U.AND _ -> U.AND va
U.XOR _ -> U.XOR va
U.NOT _ -> U.NOT va
U.COMPARE _ -> U.COMPARE va
U.EQ _ -> U.EQ va
U.NEQ _ -> U.NEQ va
U.LT _ -> U.GT va
U.GT _ -> U.GT va
U.LE _ -> U.GE va
U.INT _ -> U.INT va
U.SELF _ fa -> U.SELF va fa
U.CONTRACT _ fa t -> U.CONTRACT va fa t
U.TRANSFER_TOKENS _ -> U.TRANSFER_TOKENS va
U.SET_DELEGATE _ -> U.SET_DELEGATE va
U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va U.noAnn c
U.IMPLICIT_ACCOUNT _ -> U.IMPLICIT_ACCOUNT va
U.NOW _ -> U.NOW va
U.AMOUNT _ -> U.AMOUNT va
U.BALANCE _ -> U.BALANCE va
U.CHECK_SIGNATURE _ -> U.CHECK_SIGNATURE va
U.SHA256 _ -> U.SHA512 va
U.BLAKE2B _ -> U.BLAKE2B va
U.HASH_KEY _ -> U.HASH_KEY va
U.STEPS_TO_QUOTA _ -> U.STEPS_TO_QUOTA va
U.SOURCE _ -> U.SOURCE va
U.SENDER _ -> U.SENDER va
U.ADDRESS _ -> U.ADDRESS va
U.CHAIN_ID _ -> U.CHAIN_ID va
_ -> error $
"addVarNotes: Cannot add single var annotation to instr: " <> (show ins)
_ -> error $
"addVarNotes: Trying to add more than two var annotations to instr: " <> (show ins)
handleInstr :: Instr inp out -> U.ExpandedInstr
handleInstr = \case
(InstrWithNotes _ _) -> error "impossible"
(InstrWithVarNotes _ _) -> error "impossible"
(FrameInstr _ _) -> error "impossible"
(Seq _ _) -> error "impossible"
Nop -> error "impossible"
(Ext _) -> error "impossible"
(Nested _) -> error "impossible"
DocGroup{} -> error "impossible"
DROP -> U.DROP
(DROPN s) -> U.DROPN (fromIntegral $ peanoValSing s)
DUP -> U.DUP U.noAnn
SWAP -> U.SWAP
(DIG s) -> U.DIG (fromIntegral $ peanoValSing s)
(DUG s) -> U.DUG (fromIntegral $ peanoValSing s)
i@(PUSH val) | _ :: Instr inp1 (t ': s) <- i ->
let value = untypeValue val
in U.PUSH U.noAnn (untypeDemoteT @t) value
i@NONE | _ :: Instr inp1 ('TOption a ': inp1) <- i ->
U.NONE U.noAnn U.noAnn (untypeDemoteT @a)
SOME -> U.SOME U.noAnn U.noAnn
UNIT -> U.UNIT U.noAnn U.noAnn
(IF_NONE i1 i2) -> U.IF_NONE (instrToOps i1) (instrToOps i2)
PAIR -> U.PAIR U.noAnn U.noAnn U.noAnn U.noAnn
(AnnCAR fn) -> U.CAR U.noAnn fn
(AnnCDR fn) -> U.CDR U.noAnn fn
i@LEFT | _ :: Instr (a ': s) ('TOr a b ': s) <- i ->
U.LEFT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @b)
i@RIGHT | _ :: Instr (b ': s) ('TOr a b ': s) <- i ->
U.RIGHT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @a)
(IF_LEFT i1 i2) -> U.IF_LEFT (instrToOps i1) (instrToOps i2)
i@NIL | _ :: Instr s ('TList p ': s) <- i ->
U.NIL U.noAnn U.noAnn (untypeDemoteT @p)
CONS -> U.CONS U.noAnn
(IF_CONS i1 i2) -> U.IF_CONS (instrToOps i1) (instrToOps i2)
SIZE -> U.SIZE U.noAnn
i@EMPTY_SET | _ :: Instr s ('TSet e ': s) <- i ->
U.EMPTY_SET U.noAnn U.noAnn (U.Comparable (demote @e) U.noAnn)
i@EMPTY_MAP | _ :: Instr s ('TMap a b ': s) <- i ->
U.EMPTY_MAP U.noAnn U.noAnn (U.Comparable (demote @a) U.noAnn)
(untypeDemoteT @b)
i@EMPTY_BIG_MAP | _ :: Instr s ('TBigMap a b ': s) <- i ->
U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Comparable (demote @a) U.noAnn)
(untypeDemoteT @b)
(MAP op) -> U.MAP U.noAnn $ instrToOps op
(ITER op) -> U.ITER $ instrToOps op
MEM -> U.MEM U.noAnn
GET -> U.GET U.noAnn
UPDATE -> U.UPDATE U.noAnn
(IF op1 op2) -> U.IF (instrToOps op1) (instrToOps op2)
(LOOP op) -> U.LOOP (instrToOps op)
(LOOP_LEFT op) -> U.LOOP_LEFT (instrToOps op)
i@(LAMBDA {}) | LAMBDA (VLam l) :: Instr s ('TLambda i o ': s) <- i ->
U.LAMBDA U.noAnn (untypeDemoteT @i) (untypeDemoteT @o) (instrToOps $ rfAnyInstr l)
EXEC -> U.EXEC U.noAnn
APPLY -> U.APPLY U.noAnn
(DIP op) -> U.DIP (instrToOps op)
(DIPN s op) ->
U.DIPN (fromIntegral $ peanoValSing s) (instrToOps op)
FAILWITH -> U.FAILWITH
i@CAST | _ :: Instr (a ': s) (a ': s) <- i ->
U.CAST U.noAnn (untypeDemoteT @a)
RENAME -> U.RENAME U.noAnn
PACK -> U.PACK U.noAnn
i@UNPACK
| _ :: Instr ('Tc 'CBytes ': s) ('TOption a ': s) <- i ->
U.UNPACK U.noAnn U.noAnn (untypeDemoteT @a)
CONCAT -> U.CONCAT U.noAnn
CONCAT' -> U.CONCAT U.noAnn
SLICE -> U.SLICE U.noAnn
ISNAT -> U.ISNAT U.noAnn
ADD -> U.ADD U.noAnn
SUB -> U.SUB U.noAnn
MUL -> U.MUL U.noAnn
EDIV -> U.EDIV U.noAnn
ABS -> U.ABS U.noAnn
NEG -> U.NEG U.noAnn
LSL -> U.LSL U.noAnn
LSR -> U.LSR U.noAnn
OR -> U.OR U.noAnn
AND -> U.AND U.noAnn
XOR -> U.XOR U.noAnn
NOT -> U.NOT U.noAnn
COMPARE -> U.COMPARE U.noAnn
Instr.EQ -> U.EQ U.noAnn
NEQ -> U.NEQ U.noAnn
Instr.LT -> U.LT U.noAnn
Instr.GT -> U.GT U.noAnn
LE -> U.LE U.noAnn
GE -> U.GE U.noAnn
INT -> U.INT U.noAnn
SELF sepc ->
U.SELF U.noAnn (epNameToRefAnn $ sepcName sepc)
i@(CONTRACT nt epName)
| _ :: Instr ('Tc 'CAddress ': s) ('TOption ('TContract p) ': s) <- i ->
let fa = epNameToRefAnn epName
in U.CONTRACT U.noAnn fa (mkUType (sing @p) nt)
TRANSFER_TOKENS -> U.TRANSFER_TOKENS U.noAnn
SET_DELEGATE -> U.SET_DELEGATE U.noAnn
i@(CREATE_CONTRACT fullContract)
| _ :: Instr
( 'TOption ('Tc 'CKeyHash)
': 'Tc 'CMutez
': g
': s)
('TOperation ': 'Tc 'CAddress ': s) <- i ->
U.CREATE_CONTRACT U.noAnn U.noAnn (convertFullContract fullContract)
IMPLICIT_ACCOUNT -> U.IMPLICIT_ACCOUNT U.noAnn
NOW -> U.NOW U.noAnn
AMOUNT -> U.AMOUNT U.noAnn
BALANCE -> U.BALANCE U.noAnn
CHECK_SIGNATURE -> U.CHECK_SIGNATURE U.noAnn
SHA256 -> U.SHA256 U.noAnn
SHA512 -> U.SHA512 U.noAnn
BLAKE2B -> U.BLAKE2B U.noAnn
HASH_KEY -> U.HASH_KEY U.noAnn
STEPS_TO_QUOTA -> U.STEPS_TO_QUOTA U.noAnn
SOURCE -> U.SOURCE U.noAnn
SENDER -> U.SENDER U.noAnn
ADDRESS -> U.ADDRESS U.noAnn
CHAIN_ID -> U.CHAIN_ID U.noAnn
untypeStackRef :: StackRef s -> U.StackRef
untypeStackRef (StackRef n) = U.StackRef (peanoVal n)
untypePrintComment :: PrintComment s -> U.PrintComment
untypePrintComment (PrintComment pc) = U.PrintComment $ map (second untypeStackRef) pc
extInstrToOps :: ExtInstr s -> [U.ExtInstrAbstract U.ExpandedOp]
extInstrToOps = \case
PRINT pc -> one $ U.UPRINT (untypePrintComment pc)
TEST_ASSERT (TestAssert nm pc i) ->
one $ U.UTEST_ASSERT $
U.TestAssert nm (untypePrintComment pc) (instrToOps i)
DOC_ITEM{} -> []
instance Eq (Instr inp out) where
i1 == i2 = instrToOps i1 == instrToOps i2
instance Typeable s => Eq (TestAssert s) where
TestAssert name1 pattern1 instr1
==
TestAssert name2 pattern2 instr2
= and
[ name1 == name2
, pattern1 `eqParam1` pattern2
, instr1 `eqParam2` instr2
]
instance (SingI t, HasNoOp t) => Buildable (Value' Instr t) where
build = build . untypeValue