{-# 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 (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(..), fromSingCT)
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 instr = case instr of
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
_ -> [U.PrimEx $ handleInstrAnnotate 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)
handleInstr :: Instr inp out -> U.ExpandedInstr
handleInstr (InstrWithNotes _ _) = error "impossible"
handleInstr (FrameInstr _ _) = error "impossible"
handleInstr (Seq _ _) = error "impossible"
handleInstr Nop = error "impossible"
handleInstr (Ext _) = error "impossible"
handleInstr (Nested _) = error "impossible"
handleInstr DocGroup{} = error "impossible"
handleInstr DROP = U.DROP
handleInstr (DROPN s) = U.DROPN (fromIntegral $ peanoValSing s)
handleInstr DUP = U.DUP U.noAnn
handleInstr SWAP = U.SWAP
handleInstr (DIG s) = U.DIG (fromIntegral $ peanoValSing s)
handleInstr (DUG s) = U.DUG (fromIntegral $ peanoValSing s)
handleInstr i@(PUSH val) | _ :: Instr inp1 (t ': s) <- i =
let value = untypeValue val
in U.PUSH U.noAnn (untypeDemoteT @t) value
handleInstr i@NONE | _ :: Instr inp1 ('TOption a ': inp1) <- i =
U.NONE U.noAnn U.noAnn (untypeDemoteT @a)
handleInstr SOME = U.SOME U.noAnn U.noAnn
handleInstr UNIT = U.UNIT U.noAnn U.noAnn
handleInstr (IF_NONE i1 i2) = U.IF_NONE (instrToOps i1) (instrToOps i2)
handleInstr PAIR = U.PAIR U.noAnn U.noAnn U.noAnn U.noAnn
handleInstr (AnnCAR fn) = U.CAR U.noAnn fn
handleInstr (AnnCDR fn) = U.CDR U.noAnn fn
handleInstr i@LEFT | _ :: Instr (a ': s) ('TOr a b ': s) <- i =
U.LEFT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @b)
handleInstr i@RIGHT | _ :: Instr (b ': s) ('TOr a b ': s) <- i =
U.RIGHT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @a)
handleInstr (IF_LEFT i1 i2) = U.IF_LEFT (instrToOps i1) (instrToOps i2)
handleInstr i@NIL | _ :: Instr s ('TList p ': s) <- i =
U.NIL U.noAnn U.noAnn (untypeDemoteT @p)
handleInstr CONS = U.CONS U.noAnn
handleInstr (IF_CONS i1 i2) = U.IF_CONS (instrToOps i1) (instrToOps i2)
handleInstr SIZE = U.SIZE U.noAnn
handleInstr i@EMPTY_SET | _ :: Instr s ('TSet e ': s) <- i =
U.EMPTY_SET U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @e)) U.noAnn)
handleInstr i@EMPTY_MAP | _ :: Instr s ('TMap a b ': s) <- i =
U.EMPTY_MAP U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @a)) U.noAnn)
(untypeDemoteT @b)
handleInstr i@EMPTY_BIG_MAP | _ :: Instr s ('TBigMap a b ': s) <- i =
U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @a)) U.noAnn)
(untypeDemoteT @b)
handleInstr (MAP op) = U.MAP U.noAnn $ instrToOps op
handleInstr (ITER op) = U.ITER $ instrToOps op
handleInstr MEM = U.MEM U.noAnn
handleInstr GET = U.GET U.noAnn
handleInstr UPDATE = U.UPDATE U.noAnn
handleInstr (IF op1 op2) = U.IF (instrToOps op1) (instrToOps op2)
handleInstr (LOOP op) = U.LOOP (instrToOps op)
handleInstr (LOOP_LEFT op) = U.LOOP_LEFT (instrToOps op)
handleInstr i@(LAMBDA {}) | LAMBDA (VLam l) :: Instr s ('TLambda i o ': s) <- i =
U.LAMBDA U.noAnn (untypeDemoteT @i) (untypeDemoteT @o) (instrToOps $ rfAnyInstr l)
handleInstr EXEC = U.EXEC U.noAnn
handleInstr APPLY = U.APPLY U.noAnn
handleInstr (DIP op) = U.DIP (instrToOps op)
handleInstr (DIPN s op) =
U.DIPN (fromIntegral $ peanoValSing s) (instrToOps op)
handleInstr FAILWITH = U.FAILWITH
handleInstr i@CAST | _ :: Instr (a ': s) (a ': s) <- i =
U.CAST U.noAnn (untypeDemoteT @a)
handleInstr RENAME = U.RENAME U.noAnn
handleInstr PACK = U.PACK U.noAnn
handleInstr i@UNPACK
| _ :: Instr ('Tc 'CBytes ': s) ('TOption a ': s) <- i =
U.UNPACK U.noAnn U.noAnn (untypeDemoteT @a)
handleInstr CONCAT = U.CONCAT U.noAnn
handleInstr CONCAT' = U.CONCAT U.noAnn
handleInstr SLICE = U.SLICE U.noAnn
handleInstr ISNAT = U.ISNAT U.noAnn
handleInstr ADD = U.ADD U.noAnn
handleInstr SUB = U.SUB U.noAnn
handleInstr MUL = U.MUL U.noAnn
handleInstr EDIV = U.EDIV U.noAnn
handleInstr ABS = U.ABS U.noAnn
handleInstr NEG = U.NEG U.noAnn
handleInstr LSL = U.LSL U.noAnn
handleInstr LSR = U.LSR U.noAnn
handleInstr OR = U.OR U.noAnn
handleInstr AND = U.AND U.noAnn
handleInstr XOR = U.XOR U.noAnn
handleInstr NOT = U.NOT U.noAnn
handleInstr COMPARE = U.COMPARE U.noAnn
handleInstr Instr.EQ = U.EQ U.noAnn
handleInstr NEQ = U.NEQ U.noAnn
handleInstr Instr.LT = U.LT U.noAnn
handleInstr Instr.GT = U.GT U.noAnn
handleInstr LE = U.LE U.noAnn
handleInstr GE = U.GE U.noAnn
handleInstr INT = U.INT U.noAnn
handleInstr (SELF sepc) =
U.SELF U.noAnn (epNameToRefAnn $ sepcName sepc)
handleInstr 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)
handleInstr TRANSFER_TOKENS = U.TRANSFER_TOKENS U.noAnn
handleInstr SET_DELEGATE = U.SET_DELEGATE U.noAnn
handleInstr 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)
handleInstr IMPLICIT_ACCOUNT = U.IMPLICIT_ACCOUNT U.noAnn
handleInstr NOW = U.NOW U.noAnn
handleInstr AMOUNT = U.AMOUNT U.noAnn
handleInstr BALANCE = U.BALANCE U.noAnn
handleInstr CHECK_SIGNATURE = U.CHECK_SIGNATURE U.noAnn
handleInstr SHA256 = U.SHA256 U.noAnn
handleInstr SHA512 = U.SHA512 U.noAnn
handleInstr BLAKE2B = U.BLAKE2B U.noAnn
handleInstr HASH_KEY = U.HASH_KEY U.noAnn
handleInstr STEPS_TO_QUOTA = U.STEPS_TO_QUOTA U.noAnn
handleInstr SOURCE = U.SOURCE U.noAnn
handleInstr SENDER = U.SENDER U.noAnn
handleInstr ADDRESS = U.ADDRESS U.noAnn
handleInstr 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
]