morley 1.16.4 → 1.17.0

raw patch · 88 files changed

+4827/−6568 lines, 88 filesdep +bimapdep +singletons-basePVP ok

version bump matches the API change (PVP)

Dependencies added: bimap, singletons-base

API changes (from Hackage documentation)

Files

• CHANGES.md +103/−0
• README.md +3/−16
• app/Main.hs +29/−34
• app/REPL.hs +21/−15
• docs/language/morleyInstructions.md +0/−78
• docs/language/morleyLanguage.md +0/−43
• docs/language/morleyLet.md +0/−170
• docs/language/morleyMacros.md +0/−71
• docs/language/morleySyntaxSugar.md +0/−140
• docs/morleyTypechecker.md +1/−3
• morley.cabal +6/−12
• src/Morley/AsRPC.hs +45/−9
• src/Morley/CLI.hs +27/−1
• src/Morley/Micheline/Binary.hs +16/−16
• src/Morley/Micheline/Class.hs +1021/−988
• src/Morley/Micheline/Expression.hs +253/−49
• src/Morley/Micheline/Expression/WithMeta.hs +107/−0
• src/Morley/Michelson/ErrorPos.hs +11/−28
• src/Morley/Michelson/FailPattern.hs +8/−8
• src/Morley/Michelson/Interpret.hs +241/−280
• src/Morley/Michelson/Interpret/Unpack.hs +1/−1
• src/Morley/Michelson/Let.hs +0/−32
• src/Morley/Michelson/Macro.hs +29/−155
• src/Morley/Michelson/Optimizer.hs +2/−11
• src/Morley/Michelson/Parser.hs +34/−81
• src/Morley/Michelson/Parser/Annotations.hs +21/−13
• src/Morley/Michelson/Parser/Common.hs +1/−1
• src/Morley/Michelson/Parser/Error.hs +1/−27
• src/Morley/Michelson/Parser/Ext.hs +0/−76
• src/Morley/Michelson/Parser/Helpers.hs +2/−21
• src/Morley/Michelson/Parser/Instr.hs +215/−221
• src/Morley/Michelson/Parser/Let.hs +0/−127
• src/Morley/Michelson/Parser/Lexer.hs +15/−47
• src/Morley/Michelson/Parser/Macro.hs +52/−98
• src/Morley/Michelson/Parser/Type.hs +102/−205
• src/Morley/Michelson/Parser/Types.hs +2/−53
• src/Morley/Michelson/Parser/Value.hs +26/−72
• src/Morley/Michelson/Preprocess.hs +8/−3
• src/Morley/Michelson/Runtime.hs +66/−71
• src/Morley/Michelson/Runtime/Dummy.hs +7/−1
• src/Morley/Michelson/Runtime/GState.hs +39/−16
• src/Morley/Michelson/Runtime/Import.hs +1/−52
• src/Morley/Michelson/TypeCheck.hs +1/−2
• src/Morley/Michelson/TypeCheck/Error.hs +6/−20
• src/Morley/Michelson/TypeCheck/Ext.hs +11/−58
• src/Morley/Michelson/TypeCheck/Helpers.hs +99/−465
• src/Morley/Michelson/TypeCheck/Instr.hs +398/−454
• src/Morley/Michelson/TypeCheck/TypeCheck.hs +19/−5
• src/Morley/Michelson/TypeCheck/Types.hs +9/−24
• src/Morley/Michelson/TypeCheck/Value.hs +30/−15
• src/Morley/Michelson/Typed.hs +1/−2
• src/Morley/Michelson/Typed/Annotation.hs +150/−96
• src/Morley/Michelson/Typed/Arith.hs +0/−58
• src/Morley/Michelson/Typed/Contract.hs +62/−6
• src/Morley/Michelson/Typed/Convert.hs +150/−435
• src/Morley/Michelson/Typed/Doc.hs +30/−71
• src/Morley/Michelson/Typed/Entrypoints.hs +2/−2
• src/Morley/Michelson/Typed/Extract.hs +3/−0
• src/Morley/Michelson/Typed/Haskell/Doc.hs +6/−0
• src/Morley/Michelson/Typed/Haskell/Instr/Product.hs +1/−1
• src/Morley/Michelson/Typed/Haskell/Value.hs +6/−1
• src/Morley/Michelson/Typed/Instr.hs +384/−345
• src/Morley/Michelson/Typed/OpSize.hs +0/−33
• src/Morley/Michelson/Typed/Operation.hs +8/−5
• src/Morley/Michelson/Typed/Polymorphic.hs +0/−20
• src/Morley/Michelson/Typed/Scope.hs +41/−35
• src/Morley/Michelson/Typed/Sing.hs +11/−1
• src/Morley/Michelson/Typed/T.hs +2/−0
• src/Morley/Michelson/Typed/Util.hs +485/−393
• src/Morley/Michelson/Typed/Value.hs +26/−12
• src/Morley/Michelson/Typed/View.hs +0/−1
• src/Morley/Michelson/Untyped.hs +0/−1
• src/Morley/Michelson/Untyped/Annotation.hs +22/−70
• src/Morley/Michelson/Untyped/Ext.hs +6/−24
• src/Morley/Michelson/Untyped/Instr.hs +7/−4
• src/Morley/Michelson/Untyped/OpSize.hs +0/−306
• src/Morley/Michelson/Untyped/Type.hs +8/−2
• src/Morley/Michelson/Untyped/Value.hs +4/−2
• src/Morley/Tezos/Address.hs +70/−100
• src/Morley/Tezos/Address/Alias.hs +46/−0
• src/Morley/Tezos/Crypto.hs +150/−63
• src/Morley/Util/CustomGeneric.hs +22/−5
• src/Morley/Util/Fcf.hs +2/−2
• src/Morley/Util/Named.hs +1/−26
• src/Morley/Util/Positive.hs +0/−40
• src/Morley/Util/SizedList.hs +17/−10
• src/Morley/Util/TH.hs +8/−6
• src/Morley/Util/Type.hs +7/−2

@@ -1,6 +1,109 @@ <!-- Unreleased: append new entries here -->  +1.17.0+======+* [!1173](https://gitlab.com/morley-framework/morley/-/merge_requests/1173)+  Typechecker fixes+  + Remove unused `TypeCheckPack` typechecker mode+  + Do not throw `error` in the typechecker+  + Set typecheck mode in `typeCheckValue` (don't accept `SELF` inside a pushed+    `lambda`)+  + Hotfix: Give `IsNotInView` in `TypeCheckTest` mode (fix morley repl+    confusingly complaining about views)+* [!1123](https://gitlab.com/morley-framework/morley/-/merge_requests/1123)+  Remove deprecated exports+* [!1161](https://gitlab.com/morley-framework/morley/-/merge_requests/1161)+  Remove support for `AliasHint`+* [!1169](https://gitlab.com/morley-framework/morley/-/merge_requests/1169)+  Support MIN_BLOCK_TIME instruction+  + Add `MIN_BLOCK_TIME` typed and untyped instructions.+  + `MIN_BLOCK_TIME` accepts any number of any annotations, introduce `AnyAnn`+    type for arbitrary annotations.+  + Remove unused `SomeAnn` and `SomeTag`.+  + Add `ceMinBlockTime` to `ContractEnv` and `eeMinBlockTime` to `ExecutorEnv`.+  + Add a corresponding CLI option.+* [!1166](https://gitlab.com/morley-framework/morley/-/merge_requests/1166)+  Support transaction rollup jakarta changes.+  + Refactor address hash parsing/printing.+      * `HashKind` datakind introduced;+      * `KeyHash` and `ContractHash` are replaced by `Hash (a :: HashKind)`,+      * `KeyHashTag` replaced by `HashTag (a :: HashKind)`;+      * `KeyHash`, `KeyHashTag` and `ContractHash` compatibility type synonyms+        introduced,+      * `formatKeyHash`, `mformatKeyHash`, `parseKeyHash`, `parseKeyHashRaw`,+        `keyHashLengthBytes` are renamed to `formatHash`, `mformatHash`,+        `parseHash`, `hashLengthBytes`, respectively,+      * `contractHashLengthBytes`, `formatContractHash`, `parseContractHash` are+        removed (use generic `hashLengthBytes`, `formatHash` and `parseHash`)+      * Use `Hash HashContract` instead of `ContractHash` pattern/constructor.+  + Add typechecking support for `tx_rollup_l2_address` Michelson type.+      * `TxRollupL2Address` type introduced, isomorphic to+        `tx_rollup_l2_address`.+      * `HashBLS` hash kind introduced; `KeyHashL2` convenience type synonym+        introduced.+  + Add parsing/printing for `tz4` addresses.+  + Add typechecking support and parsing/printing for `txr1` addresses.+      * `TransactionRollupAddress` data constructor for `Address` is introduced;+      * `HashKindTxRollup` hash kind and `TxRollupHash` type synonym introduced.+  + NB: emulator support for transaction rollups is not yet implemented.+* [!1167](https://gitlab.com/morley-framework/morley/-/merge_requests/1167)+  Adjust to sapling changes in jakarta+  * Update the type of the `SAPLING_VERIFY_UPDATE` instruction.+  * Reject contracts with the `sapling_transaction_deprecated` type.+  * Support deserializing the `SAPLING_EMPTY_STATE`, `SAPLING_VERIFY_UPDATE`,+    `OPEN_CHEST` instructions.+  * Fix bug in the deserialization of the `sapling_transaction` type.+* [!1158](https://gitlab.com/morley-framework/morley/-/merge_requests/1158)+  Refactor (out) annotation checking support+  + Ignore annotations in the morley typechecker+  + All typed instructions have `AnnINSTR` constructor, accepting a list of+    annotations, and a pattern synonym `INSTR` that ignores annotations.+  + `InstrWithVarAnns`, `InstrWithNotes`, `InstrWithVarNotes`+    pseudo-constructors removed.+  + `(::&+)` pattern synonym removed+  + `AnnConvergeError`, `converge`, `convergeAnns`, `convergeDestrAnns`,+    `deriveSpecialVN`, `deriveSpecialFNs`, `deriveVN`, `deriveNsOr`,+    `deriveNsOption`, `convergeHSTEl`, `convergeHST`, `hstToTs`, `matchHST1`,+    `onTypeCheckInstrAnnErr`, `matchTypes`, `WithAnn` pattern, `orAnn`,+    `unifyAnn`, `unifyPairFieldAnn`, `convergeVarAnns`, `ifAnnUnified`,+    `convAnn`, `starNotesStkEl`, `matchTypes` removed.+  + `SomeAnns` and `instrAnns` utility functions to extract annotations of an+    instruction added.+  + Optimizations will now strip annotations.+* [!1160](https://gitlab.com/morley-framework/morley/-/merge_requests/1160)+  Forbid parameter prefix root annotations+* [!1163](https://gitlab.com/morley-framework/morley/-/merge_requests/1163)+  Prohibit some operations in views+  + New class `IsNotInView`, which is conjured into existence where appropriate.+  + `ContractCode` is now a newtype wrapper instead of type synonym; this is+    required to avoid accidentally pasting contract code in views.+  + New "smart" constructors `mkContractCode` and `mkVLam` which conjure+    `IsNotInView` constraint (`mkLam` is needed because operations forbidden in+    views are allowed in lambdas inside views)+* [!1088](https://gitlab.com/morley-framework/morley/-/merge_requests/1088)+  Add options to specify convenient human-readable contract names for `originate`, `transfer` commands in Morley CLI.+* [!1153](https://gitlab.com/morley-framework/morley/-/merge_requests/1153)+  Remove 'OpSize' modules.+* [!1139](https://gitlab.com/morley-framework/morley/-/merge_requests/1139)+  Various small improvements.+  * Export `eqInstrExt`.+  * Add `ConcreteMeta` pattern synonym.+* [!1114](https://gitlab.com/morley-framework/morley/-/merge_requests/1114)+  Update to ghc-9.0.2+* [!1108](https://gitlab.com/morley-framework/morley/-/merge_requests/1108)+  Remove support for the deprecated morley extensions+* [!1148](https://gitlab.com/morley-framework/morley/-/merge_requests/1148)+  Fix deriveRPC's call to customGeneric' so that field ordering is maintained+* [!1141](https://gitlab.com/morley-framework/morley/-/merge_requests/1141)+  Forbid transfers from empty sender on emulator+  + This brings the emulator into closer correspondence with the network+  + New `ExecutorError` constructor, `EEEmptyImplicitContract`.+* [!1131](https://gitlab.com/morley-framework/morley/-/merge_requests/1131)+  Make `dfsTraverseValue` parameterized by `DfsSettings`+* [!1130](https://gitlab.com/morley-framework/morley/-/merge_requests/1130)+  Fix deriveRPCWithStrategy on data with type variables+ 1.16.4 ====== * [!1135](https://gitlab.com/morley-framework/morley/-/merge_requests/1135)

@@ -3,12 +3,10 @@ [![Hackage](https://img.shields.io/hackage/v/morley.svg)](https://hackage.haskell.org/package/morley)  Morley aims to make writing smart contracts in Michelson pleasant and effective.-It contains 3 major things:+It contains 2 major things:+ 1. An [executable](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-executable) that lets you perform various operations on Michelson smart contracts. 2. A [library](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-library) with core Tezos and Michelson data types, and functions such as Michelson typechecker and interpreter.-3. A superset of the Michelson language that we call the [Morley language](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-language).-It relaxes Michelson parser rules, adds some syntax sugar and simple features.-**deprecated**  ## Morley executable @@ -52,7 +50,6 @@ - `analyze` a contract and print some statistics about it. - `print` a contract in vanilla Michelson format. It can be useful in some cases:-  + You have a smart contract that uses [Morley extensions](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-language) and want to convert it to vanilla Michelson format that can be handled by Tezos reference implementation.   + You have a contract with inconsistent/ugly formatting and want to format it in uniform style.   + You want to print a contract on a single line. - `parse` a contract and return its representation in Haskell types.@@ -70,20 +67,10 @@ - [`Morley.Michelson.TypeCheck`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-TypeCheck.html): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyTypechecker.md). - [`Morley.Michelson.Interpret`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Interpret.html): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyInterpreter.md). - [`Morley.Michelson.Macro`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Macro.html) Types for macros, syntactic sugar, and other extensions that are described in the next chapter.-- [`Morley.Michelson.Parser`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Parser.html) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT.+- [`Morley.Michelson.Parser`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Parser.html) A parser to turn a `.tz` into a Haskell ADT. - [`Morley.Michelson.Runtime`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Runtime.html): A high-level interface to Morley functionality, see [morleyRuntime.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyRuntime.md). - The `Morley.Micheline.*` hierarchy ([`Morley.Micheline.Binary`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Binary.html), [`Morley.Micheline.Class`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Class.html), [`Morley.Micheline.Expression`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Expression.html), [`Morley.Micheline.Json`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Json.html)) contains the representation of Micheline `Expression`s, conversion to/from Michelson values, as well as encoding/decoding to/from JSON and binary format. - The `Morley.Util.*` hierarchy defines various `Morley`-related utilities that are used all over the project.--## Morley language--**NOTE:** Morley-the-language is deprecated and support for it will be removed in not-so-distant future. Features of morley-the-language are done better in `lorentz` and in some cases are superseded by new Michelson revisions.--Morley-the-language is a superset of the Michelson language, which means that each Michelson contract is also a valid Morley contract but not vice versa.-There are several extensions which make it more convenient to write Michelson contracts and test them.-For example, one can write inline assertions in their contracts for testing.-All the details can be found in [the document](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/language/morleyLanguage.md) about these extensions.-A smart contract written in the Morley language can be transpiled to Michelson using the aforementioned `morley print` command.

@@ -1,9 +1,6 @@ -- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA --- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations #-}- module Main   ( main   ) where@@ -24,14 +21,15 @@ import Morley.Michelson.Optimizer (optimize) import Morley.Michelson.Printer (printSomeContract, printUntypedContract) import Morley.Michelson.Runtime-  (TxData(..), originateContract, prepareContract, prepareContractExt, runContract, transfer)+  (TxData(..), originateContract, prepareContract, runContract, transfer) import Morley.Michelson.Runtime.GState (genesisAddress) import Morley.Michelson.TypeCheck (tcVerbose, typeCheckContract, typeCheckingWith) import Morley.Michelson.TypeCheck qualified as TypeCheck import Morley.Michelson.TypeCheck.Types (mapSomeContract)-import Morley.Michelson.Typed (Contract'(..), SomeContract(..))+import Morley.Michelson.Typed (Contract'(..), SomeContract(..), unContractCode) import Morley.Michelson.Untyped qualified as U import Morley.Tezos.Address (Address)+import Morley.Tezos.Address.Alias (AddressOrAlias, Alias) import Morley.Tezos.Core (Mutez, Timestamp(..), tz) import Morley.Tezos.Crypto import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey)@@ -84,6 +82,7 @@   , roVerbose :: Bool   , roNow :: Maybe Timestamp   , roLevel :: Maybe Natural+  , roMinBlockTime :: Maybe Natural   , roMaxSteps :: Word64   , roInitBalance :: Mutez   , roWrite :: Bool@@ -94,6 +93,7 @@   , ooDBPath :: FilePath   , ooTcOptions :: TypeCheck.TypeCheckOptions   , ooOriginator :: Address+  , ooAlias :: Maybe Alias   , ooDelegate :: Maybe KeyHash   , ooStorageValue :: U.Value   , ooBalance :: Mutez@@ -103,17 +103,18 @@ data TransferOptions = TransferOptions   { toDBPath :: FilePath   , toTcOptions :: TypeCheck.TypeCheckOptions-  , toDestination :: Address+  , toDestination :: AddressOrAlias   , toTxData :: TxData   , toNow :: Maybe Timestamp   , toLevel :: Maybe Natural+  , toMinBlockTime :: Maybe Natural   , toMaxSteps :: Word64   , toVerbose :: Bool   , toDryRun :: Bool   } -argParser :: Opt.Parser (Bool, CmdLnArgs)-argParser = ((,) <$> enableExtsOption <*>) . subparser $+argParser :: Opt.Parser CmdLnArgs+argParser = subparser $   printSubCmd <>   typecheckSubCmd <>   emulateSubCmd <>@@ -122,10 +123,6 @@   createChestSubCmd <>   replSubCmd   where-    enableExtsOption = switch $-      long "deprecated-morley-extensions" <>-      help "Enable parsing deprecated Morley extensions"-     typecheckSubCmd =       mkCommandParser "typecheck"         (TypeCheck <$> typeCheckOptions) $@@ -239,6 +236,7 @@         <*> verboseFlag         <*> nowOption         <*> levelOption+        <*> minBlockTimeOption         <*> maxStepsOption         <*> mutezOption (Just defaultBalance)             (#name :! "balance") (#help :! "Initial balance of this contract")@@ -252,6 +250,7 @@         <*> typeCheckOptionsOption         <*> addressOption (Just genesisAddress)             (#name :! "originator") (#help :! "Contract's originator")+        <*> optional (aliasOption "alias")         <*> optional             (keyHashOption Nothing               (#name :! "delegate") (#help :! "Contract's optional delegate")@@ -266,12 +265,14 @@     transferOptions = do       toDBPath <- dbPathOption       toTcOptions <- typeCheckOptionsOption-      toDestination <--        addressOption Nothing-        (#name :! "to") (#help :! "Destination address")+      toDestination <- addressOrAliasOption+        Nothing+        (#name :! "to")+        (#help :! "Address or alias of the transfer's destination")       toTxData <- txDataOption       toNow <- nowOption       toLevel <- levelOption+      toMinBlockTime <- minBlockTimeOption       toMaxSteps <- maxStepsOption       toVerbose <- verboseFlag       toDryRun <- dryRunFlag@@ -289,9 +290,7 @@ ----------------------------------------------------------------------------  main :: IO ()-main = wrapMain $ do-  (exts, cmdLnArgs) <- execParser programInfo-  run exts cmdLnArgs+main = wrapMain $ run =<< execParser programInfo   where     programInfo = info (helper <*> versionOption <*> argParser) $       mconcat@@ -304,16 +303,16 @@     versionOption = infoOption ("morley-" <> showVersion version)       (long "version" <> help "Show version.") -    run :: Bool -> CmdLnArgs -> IO ()-    run exts args = case args of+    run :: CmdLnArgs -> IO ()+    run args = case args of       Print (argF #input -> mInputFile)             (argF #output -> mOutputFile)             (arg #singleLine -> forceSingleLine) -> do-        contract <- prepareContract' mInputFile+        contract <- prepareContract mInputFile         let write = maybe putStrLn Utf8.writeFile mOutputFile         write $ printUntypedContract forceSingleLine contract       Optimize OptimizeOptions{..} -> do-        untypedContract <- prepareContract' optoContractFile+        untypedContract <- prepareContract optoContractFile         checkedContract <-           either throwM pure . typeCheckingWith laxTcOptions $             typeCheckContract untypedContract@@ -321,13 +320,13 @@         let write = maybe putStrLn Utf8.writeFile optoOutput         write $ printSomeContract optoSingleLine optimizedContract       Analyze AnalyzeOptions{..} -> do-        untypedContract <- prepareContract' aoContractFile+        untypedContract <- prepareContract aoContractFile         SomeContract contract <-           either throwM pure . typeCheckingWith laxTcOptions $             typeCheckContract untypedContract-        putTextLn $ pretty $ analyze (cCode contract)+        putTextLn $ pretty $ analyze (unContractCode $ cCode contract)       TypeCheck TypeCheckOptions{..} -> do-        morleyContract <- prepareContract' tcoContractFile+        morleyContract <- prepareContract tcoContractFile         -- At the moment of writing, 'tcStrict' option does not change anything         -- because it affects only values parsing; but this may change         contract <- either throwM pure . typeCheckingWith tcoTcOptions@@ -336,17 +335,18 @@           putStrLn $ printSomeContract False contract         putTextLn "Contract is well-typed"       Run RunOptions {..} -> do-        michelsonContract <- prepareContract' roContractFile-        void $ runContract roNow roLevel roMaxSteps roInitBalance roDBPath roTcOptions roStorageValue michelsonContract roTxData+        michelsonContract <- prepareContract roContractFile+        void $ runContract roNow roLevel roMinBlockTime roMaxSteps roInitBalance roDBPath roTcOptions roStorageValue michelsonContract roTxData           ! #verbose roVerbose           ! #dryRun (not roWrite)       Originate OriginateOptions {..} -> do-        michelsonContract <- prepareContract' ooContractFile+        michelsonContract <- prepareContract ooContractFile         addr <-           originateContract             ooDBPath             ooTcOptions             ooOriginator+            ooAlias             ooDelegate             ooBalance             ooStorageValue@@ -354,7 +354,7 @@             ! #verbose ooVerbose         putTextLn $ "Originated contract " <> pretty addr       Transfer TransferOptions {..} -> do-        transfer toNow toLevel toMaxSteps toDBPath toTcOptions toDestination toTxData+        transfer toNow toLevel toMinBlockTime toMaxSteps toDBPath toTcOptions toDestination toTxData           ! #verbose toVerbose           ! #dryRun toDryRun       REPL -> runRepl@@ -362,11 +362,6 @@         (chest, key) <- createChestAndChestKey ccPayload ccTime         putStrLn $ "Chest: 0x" <> encodeHex (chestBytes chest)         putStrLn $ "Key: 0x" <> encodeHex (chestKeyBytes key)-      where-        -- TODO [#712]: Remove this next major release-        prepareContract'-          | exts = prepareContractExt-          | otherwise = prepareContract   usageDoc :: Maybe Doc

@@ -21,6 +21,7 @@ import Data.ByteString.Base58 qualified as Base58 import Data.ByteString.Lazy qualified as BSL import Data.List (stripPrefix)+import Data.Singletons (fromSing) import Data.Text as T (length, replicate, strip) import Data.Text qualified as T (stripPrefix) import Data.Vinyl (Rec(..))@@ -32,7 +33,7 @@ import Morley.Michelson.Interpret (interpretInstr) import Morley.Michelson.Macro (ParsedOp, expandList) import Morley.Michelson.Parser (errorBundlePretty, ops, parseExpandValue, parseNoEnv, type_)-import Morley.Michelson.Parser.Types (MichelsonSource(..), noLetEnv)+import Morley.Michelson.Parser.Types (MichelsonSource(..)) import Morley.Michelson.Printer (printDoc, printTypedValue) import Morley.Michelson.Printer.Util (buildRenderDoc, doesntNeedParens) import Morley.Michelson.Runtime.Dummy@@ -99,7 +100,7 @@            let pkh = hashKey pk            printResult "Secret Key" (formatSecretKey sk)            printResult "Public Key" (formatPublicKey pk)-           printResult "Public Key hash" (formatKeyHash pkh)+           printResult "Public Key hash" (formatHash pkh)         (stripPrefixNonEmpty ":" -> Just cmd) ->           printErr $ "Unknown command or argument missing in `:"<> (toText cmd) <> "`. Use :help to see a list of commands"         _ -> flip catch (\Interrupt -> putTextLn "Cancelled") $ withInterrupt $ runCode (toText input)@@ -142,6 +143,7 @@   tryParseMichelsonValue @'T.TChainId "Michelson ChainId" parseInput   tryParseMichelsonValue @'T.TTimestamp "Michelson Timestamp" parseInput   tryParseMichelsonValue @'T.TAddress "Michelson Address" parseInput+  tryParseMichelsonValue @'T.TTxRollupL2Address "Michelson Transaction Rollup L2 Address" parseInput   tryParseMichelsonValue @'T.TString "Michelson String" parseInput   tryParseMichelsonValue @'T.TInt "Michelson Int" parseInput   tryParseMichelsonValue @'T.TNat "Michelson Nat" parseInput@@ -165,10 +167,14 @@     Right p -> do       printResult "Secret Key" $ formatSecretKey p     Left _ -> pass-  case parseKeyHash parseInput of+  case parseHash @'HashKindPublicKey parseInput of     Right p -> do-      printResult "KeyHash" $ formatKeyHash p+      printResult "KeyHash" $ formatHash p     Left _ -> pass+  case parseHash @'HashKindL2PublicKey parseInput of+    Right p -> do+      printResult "KeyHash" $ formatHash p+    Left _ -> pass   case Base58.decodeBase58 Base58.bitcoinAlphabet (encodeUtf8 parseInput) of     Just p -> do       printResult "Base58 Encoded Bytes" $ "0x" <> (encodeHex p)@@ -224,7 +230,7 @@  parseInstructions :: Text -> Either Text [ParsedOp] parseInstructions src =-  case parseNoEnv @() ops MSUnspecified src of+  case parseNoEnv ops MSUnspecified src of     Right p -> Right p     Left err -> Left (toText $ errorBundlePretty err) @@ -243,17 +249,17 @@   -> Either Text (T.Dict (T.SingI (t ': xs)), HST (t ': xs)) addValueToHST v hstIn = case T.valueTypeSanity v of   T.Dict -> case T.getWTP @t of-    Right wtpDict -> Right (T.Dict, (T.starNotes @t, wtpDict, U.noAnn) ::&  hstIn)+    Right wtpDict -> Right (T.Dict, (T.sing @t, wtpDict) ::&  hstIn)     Left (T.NotWellTyped t cause) -> let       U.Ty t' tann = T.toUType t       in Left $ "Value of type '" <> (renderT t' (U.fullAnnSet [tann] [] []))                 <> "' is not well typed in the provided Value because it "                 <> pretty cause <> "." -renderType :: T.Notes t -> U.VarAnn -> Text-renderType notes vann = let-  U.Ty t tann = T.mkUType notes-  in renderT t (U.fullAnnSet [tann] [] [vann])+renderType :: T.SingT t -> Text+renderType notes = let+  U.Ty t tann = T.toUType (fromSing notes)+  in renderT t (U.fullAnnSet [tann] [] [])  renderT :: U.T -> U.AnnotationSet -> Text renderT t annSet = toText $ printDoc True $ U.renderType t True doesntNeedParens annSet@@ -285,10 +291,10 @@ -- | Dump stack as a lit of tuples that represent (value, type) pairs. dumpStack :: forall t. Rec T.Value t -> HST t -> Either Text [(Text, Text)] dumpStack RNil _ = Right []-dumpStack ((v :: T.Value a) :& rst) ((notes, _, vann) ::& rHst) = case T.valueTypeSanity v of+dumpStack ((v :: T.Value a) :& rst) ((notes, _) ::& rHst) = case T.valueTypeSanity v of   T.Dict -> case T.checkOpPresence (T.sing @a) of     T.OpAbsent -> case dumpStack rst rHst of-      Right t -> Right ((toText $ printTypedValue True v, renderType notes vann) : t)+      Right t -> Right ((toText $ printTypedValue True v, renderType notes) : t)       Left e -> Left e     T.OpPresent ->  Left "Cannot dump stack with operations" @@ -300,7 +306,7 @@     buildStack :: Either Text SomeStack -> (Text, Text) -> Either Text SomeStack     buildStack (Left err) _ = Left err     buildStack (Right (SomeStack stk hst)) (txVal, txTyp) = case-      (parseExpandValue "stack" txVal, parse (runReaderT type_ noLetEnv) "" txTyp) of+      (parseExpandValue "stack" txVal, parse type_ "" txTyp) of         (Right val, Right typ) ->           case typeCheckingWith tcOptions $ typeCheckParameter mempty typ val of             Right (T.SomeValue tVal) ->@@ -313,7 +319,7 @@  showStack :: forall t. Rec T.Value t -> HST t -> Text showStack RNil _ = "--"-showStack ((v :: T.Value a) :& rst) ((notes, _, vann) ::& rHst)  = case T.valueTypeSanity v of+showStack ((v :: T.Value a) :& rst) ((notes, _) ::& rHst)  = case T.valueTypeSanity v of   T.Dict -> case T.checkOpPresence (T.sing @a) of     T.OpAbsent -> -- print nice if value has no operations       addSuffix (toText $ printTypedValue True v)@@ -322,4 +328,4 @@         (T.VList [], T.STList T.STOperation) -> "{ } :: list operation\n" <> showStack rst rHst         _ -> addSuffix $ "(operations container:" <> pretty v <> ")"   where-    addSuffix val = val <>" :: " <> renderType notes vann <> "\n" <> showStack rst rHst+    addSuffix val = val <>" :: " <> renderType notes <> "\n" <> showStack rst rHst

@@ -1,78 +0,0 @@-<!---SPDX-FileCopyrightText: 2020 Tocqueville Group--SPDX-License-Identifier: LicenseRef-MIT-TQ--->--**NOTE:** Morley extended instructions are _deprecated_. The internal representation still uses instructions described here, as those are used by Lorentz, but parsing contracts using these instructions is deprecated and requires `--deprecated-morley-extensions` flag when invoking `morley`. This flag will be removed in the not-so-distant future.--# Morley Ext Instructions--Morley adds some additional instructions of its own to the existing set of-Michelson instructions. These instructions are not macros and have no effect on-a contract's execution. That is, they cannot write or alter any value on the-stack, but simply provide a mechanism to pass additional-information to Morley's typechecker or runtime.--## `STACKTYPE`--The `STACKTYPE` instruction allows us to assert that the stack has a given type-signature. For example, `STACKTYPE '[]` asserts that the stack is the empty-stack, and tells the typechecker to fail the contract otherwise.--### Stack Type Signature--A stack signature can be either an empty stack, a list of types, or a pattern-match on the head of the stack:--```-Empty stack: '[]-stack of three int: '[int, int, int]-A pattern match on a stack with two int at the top: '[int, int, ...]-```--More formally, a stack signature is like a `cons` list with two distinct-`nil`-like terminators:--```-<stack-sig> := "'[" (<empty-stack> | <rest-of-stack> | <stack-cons>)-<empty-stack> := "]"-<rest-of-stack> := "...]"-<stack-cons> := (<type> | "_" ) (("," (<stack-cons> | <stack-rest)) | <empty-stack>)-```--## PRINT--`PRINT` instructs Morley to print a comment during execution, optionally with-a reference into the stack. For example, `PRINT "hello"` will print `hello`.--Stack references may be written within the print-comment as `%[n]`, replacing-`n` with any natural number, which prints the `n`-th stack element from the-head.--For example, `PRINT "Head is: %[0]"` on `'[1, ...]` will print--```-Head is: int 1-```--## TEST_ASSERT--The `TEST_ASSERT` instruction allows us to declare an inline test assertion, which is-a labeled sequence of instructions that runs on a copy of the current stack.-That is, an assertion has no actual effect on the program but can return the-result of some computation on the stack.--For example, suppose we want to verify that the sum of two numbers is greater-than 10:--```-parameter unit;-storage unit;-code { DROP;-       PUSH int 2;-       PUSH int 10;-       TEST_ASSERT Test1 "%[0] + %[1] > 10" {ADD; PUSH int 10; COMPARE;LT;};-       DROP; DROP; UNIT; NIL operation; PAIR; };--```

@@ -1,43 +0,0 @@-<!---SPDX-FileCopyrightText: 2021 Oxhead Alpha-SPDX-License-Identifier: LicenseRef-MIT-OA--->--**NOTE:** Morley language is _deprecated_. The internal representation still uses some of the extended instructions, as those are used by Lorentz, but parsing contracts using the morley language is deprecated and requires `--deprecated-morley-extensions` flag when invoking `morley`. This flag will be removed in the not-so-distant future.--# Morley Language--The Morley Language is a low-level syntactic sugar over the core Michelson-instructions (core Michelson being the instructions which are actually executed-in the Tezos blockchain, as opposed to the various syntactic conveniences-provided by the OCaml reference client: `tezos-client`).--The general principle is that any syntactically valid core Michelson expression-will also be a valid Morley expression, i.e. Morley is a superset of-Michelson. Any language extensions that break this principle must be explicitly-enabled.--## Syntax Sugar--[See `morleySyntaxSugar.md`](./morleySyntaxSugar.md).--## Instruction and type names--In Michelson, all letters in all instructions must be CAPITAL and all letters in types and type constructors must be lowercase.-In Morley, one can also use lowercase letters in instructions.-For example, `ABS` and `abs` are both valid names of the same instruction.--Types and type constructors can start with a capital letter (like in Haskell).-For example, both `Unit` and `unit` are valid names of the unit type.--## Macros and Type synonyms--[See `morleyMacros.md`](./morleyMacros.md).--## Extended NOP Instructions--[See `morleyInstructions.md`](./morleyInstructions.md).--## Let-block Definitions--[See `morleyLet.md`](./morleyLet.md).

@@ -1,170 +0,0 @@-<!---SPDX-FileCopyrightText: 2020 Tocqueville Group--SPDX-License-Identifier: LicenseRef-MIT-TQ--->--**NOTE:** Morley language is _deprecated_, which includes let-block definitions. Parsing contracts using the morley language is deprecated and requires `--deprecated-morley-extensions` flag when invoking `morley`. This flag will be removed in the not-so-distant future.--# Let-block Definitions--In addition to the built-in macros defined in the Michelson specification,-Morley allows the programmer to define their own custom macros, as well as value-and type synonyms in a new top-level block:--```-let {-  type num = int;-  Three :: int = 3;-  add3 :: '[int] -> '[int] = {push int 3; add;};-  add3 :: '[int] -> '[int] = {push num Three; add;};-  add :: '[int, int] -> '[int] = {sub;};-  stkRest :: '[int, ...] -> '[int, ...] = {push int 3; ADD;};-};--parameter unit;-storage unit;-code { DROP;-       PUSH nat Three;-       drop;-       PUSH num Three;-       push Three;-       add;-       stacktype '[int, ...];-       stkRest;-       DROP;-       UNIT; NIL operation; PAIR; };-```--More formally:--```-let {<let>};--<let> := type <string> = type;-    | <string> :: <type> = <value>;-    | <string> :: <type-sig> = {op};-```--As a concrete example:--```-let {-  type num = int;-  Three :: int = 3;-  add3 :: '[int] -> '[int] = {push int 3; add;};-};-```--There are three distinct types of let:--- Type synonyms-- Constants-- Macros--## Constants--Constants may be pushed directly to the stack like so:--```-let {-  Three :: int = 3;-};-...-code {-  ...-  push Three;-  ...-  }-```--At present, constants are not checked statically, only when pushed.--## Type Synonyms--Type synonyms allow for labeling types. A synonym can be referred to anywhere a-type would be expected:--```-let {-  type num = int;-}-code {-  ...-  push num 3;-  ...-  }-```--This `push num 3` instruction pushes the value 3 with the type `int :num` onto-the stack.--Note that type synonyms with names `Parameter` and `Storage` are prohibited, these-names are used for implicit contracts parameter and storage types.--The interaction between type synonyms and type annotations is that if the-synonym's definition contains no annotation, the name of the synonym will be-used. If the synonym definition does contain a type annotation, the annotation-takes precedence and will be preserved:--```-type color = int;     ~> int :color-type color = int :rgb ~> int :rgb-```--## Let Macros--```-add3 :: '[int] -> '[int] = {push int 3; add;};-```--The first line of the macro declaration is the type signature, which denotes the-stack transformation the macro performs.--Crucially, if both input and output stack types contain a `<rest-of-stack>`-pattern match (syntactically `...]`), then the stack type captured by both-pattern matches must be identical.--For example, the type signature of--```-add3 :: '[int, ...] -> '[int, ...] = {push int 3; add;}-```--would be written using the type notation from the Michelson specification as:--```-add3 :: int : 'S -> int : 'S-```--meaning that the pattern match must be universally quantified over the same-stack-type `'S`.--Furthermore, type signatures can also have universally quantified type-parameters, which must be declared in a `forall`:--For instance, the type of the primitive `SWAP` instruction could be notated as:--```-swap :: forall a b. '[a, b, ...] -> '[b, a, ...]-```--It is important to note that type variables are not checked statically (at-present), but rather concretized in-place during type-checking. That is, the-typechecker replaces any unbound type parameter with the concrete type at that-position in the stack, and checks for consistency with any other instances of-that parameter.--## Non-recursive References--These definitions allow for non-recursive references to other definitions,-so one can define:--```-let {-  foo :: '[unit] -> '[unit, unit] = {unit;};-  bar :: '[unit] -> '[unit] = {foo; drop;};-};-```--A reference must always come after the let it refers to in the block.

@@ -1,71 +0,0 @@-<!---SPDX-FileCopyrightText: 2020 Tocqueville Group--SPDX-License-Identifier: LicenseRef-MIT-TQ--->--**NOTE:** Morley language is _deprecated_, which includes these macros. Parsing contracts using the morley language is deprecated and requires `--deprecated-morley-extensions` flag when invoking `morley`. This flag will be removed in the not-so-distant future.--# Morley Language: Macros and Type synonyms--Morley language supports all macros from the OCaml reference implementation and additionally introduces some extra macros and type synonyms.--## A1 macros--First group of macros implemented in Morley consists of macros proposed in [A1 TZIP](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md).-In order to avoid duplication of documentation we don't copy it here, please refer to the A1 document for more information.--## Macros to work with tuples--Large tuples are desugared as right-balanced trees of `Pair`, thus working with them manually is inconvenient and produces fragile code.-The following macros can be used to work with tuples without caring about their actual Michelson representation.--### ACCESS--This macro retrieves an element of a tuple.-It accepts two arguments - 0-based index of desired element and overall tuple size.-For now `ACCESS` is just a macro, not a full-featured morley instruction, thus programmer has to specify tuple size explicitly.--Example:-```-push (int, bool, string, unit) (1, False, "", ());-access 1 4;-# Now stack contains `False` at the top-```--### SET--Modifies single element of a tuple.-This macro has signature similar to one of `ACCESS`, and accepts two stack arguments - original tuple and new value.--Example:-```-push (int, bool, string, unit) (1, False, "", ());-push bool True;-set 1 4;-# Now stack contains `(1, True, "", ())` at the top-```--### CONSTRUCT--Builds a tuple.-For each position of the tuple you provide a code block which builds an element for that position.--Example:-```-construct-  { push int 1 }-  { sender }-  { unit; some }-# Pushes `(1, <sender address>, some ())` on stack-```--Each code block has access to the stack at the moment of `construct` call and eventually have to push exactly one element to stack. This will also work:-```-push 5-construct-  { dup }-  { push int 3 }-  { dup; push int 3; add }-# Now stack is [(5, 3, 8), 5, ...]-```

@@ -1,140 +0,0 @@-<!---SPDX-FileCopyrightText: 2020 Tocqueville Group--SPDX-License-Identifier: LicenseRef-MIT-TQ--->--**NOTE:** Morley language is _deprecated_, which includes the syntax sugar described here. Parsing contracts using the morley language is deprecated and requires `--deprecated-morley-extensions` flag when invoking `morley`. This flag will be removed in the not-so-distant future.--# Morley Language: Syntax Sugar--## Summary--| type   | Sugar                                   | Desugar                                   |-|--------|-----------------------------------------|-------------------------------------------|-| pair   | `(a ,b)`                                | `(pair a b)`                              |-| pair   | `(a, b) :t %f`                          | `(pair :t %f a b)`                        |-| pair   | `(a,b,c)`                               | `(a,(b,c))`                               |-| pair   | `(a, b, c) :t %f`                       | `(a, (b, c)) :t %f`                       |-| pair   | `(a :ta %fa, b :tb %fb, c :tc %fc)`     | `(a :ta %fa, (b :tb %fb, c :tc %fc))`     |-| or     | `(a \| b)`                              | `(or a b)`                                |-| or     | `(a \| b) :t %f`                        | `(or :t %f a b)`                          |-| or     | `(a \| b \| c)`                         | `(a \| (b \| c))`                         |-| or     | `(a \| b \| c) :t %f`                   | `(a \| (b \| c)) :t %f`                   |-| or     | `(a :ta %fa \| b :tb %fb \| c :tc %fc)` | `(a :ta %fa \| (b :tb %fb \| c :tc %fc))` |-| unit   | `()`                                    | `unit`                                    |-| lambda | `(\ a -> b)`                            | `lambda a b`                              |-| list   | `[a]`                                   | `list a`                                  |-| set    | `{a}`                                   | `set a`                                   |----| Value | Sugar       | Desugar      |-|-------|-------------|--------------|-| Pair  | `(a, b)`    | `(Pair a b)` |-| Pair  | `(a, b, c)` | `(a,(b,c))`  |-| Unit  | `()`        | `Unit`       |--## Pairs--### Type Syntax-`pair` types may be written using Haskell-style tuples:--```-(a, b) ~ (pair a b)-(a, b) :t %f ~ (pair :t %f a b)-```--When tuples are nested, parenthesis may be omitted:--```-(a,b,c) ~ (a,(b,c))-```--Unsugaring will be performed in a way which provides the best average access time.-In essence, the tuple is split so that the left part has less by one-or the same size as the right part, these parts are recursively split-until one element remains, and resulting pieces are merged into an `Pair` tree.--For instance:--```-(a, b, c, d, e) ~ ((a, b), (c, (d, e)))-```--For nested tuples, only the outer pair may be annotated:--```-(a, b, c) :t %f ~ (a, (b, c)) :t %f-```--Inner types may be annotated as usual:--```-(a :ta %fa, b :tb %fb, c :tc %fc) ~ (a :ta %fa, (b :tb %fb, c :tc %fc))-```--### Value Syntax--`Pair` values may also be written with tuples:--```-(a, b) ~ (Pair a b)-(a, b, c) ~ (a,(b,c))-```--## Unions--### Type Syntax--`or` types may be written using the `|` character:--```-(or a b) ~ (a | b)-(or :t %f a b) ~ (a | b) :t %f-```--When bars are nested, parenthesis may be omitted:--```-(a | b | c) ~ (a | (b | c))-```--As for tuples, desugaring large unions produces right-balanced trees of `Or`s.--Annotations follow the same pattern as Tuples:-```-(a | b | c) :t %f ~ (a | (b | c)) :t %f-(a :ta %fa | b :tb %fb | c :tc %fc) ~ (a :ta %fa | (b :tb %fb | c :tc %fc))-```--## Unit--The `unit` type may be written as a `0`-tuple--```-unit ~ ()-```--The `Unit` value may also be written this way:--```-Unit ~ ()-```--## Lambda:--They `lambda` type may be written:--```-(lambda a b) ~ (\ a -> b)-```--## Containers--The `list` and `set` types may be written:--```-(list a) ~ [a]-(set a) ~ {a}-```

@@ -8,9 +8,7 @@ In Morley, we have a typechecker for the core Michelson language, i. e. without macros.  It is located in `Morley.Michelson.TypeCheck` and designed in the following way:-* It takes a core Michelson contract extended with `EXT` instruction-  to support additional instructions described in the-  [`morleyInstructions.md`](language/morleyInstructions.md) document.+* It takes a core Michelson contract. * The contract passed to the typechecker uses [untyped   representation](./michelsonTypes.md). * During typechecking, we verify that instructions are well-typed and

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.16.4+version:        1.17.0 synopsis:       Developer tools for the Michelson Language description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category:       Language@@ -25,11 +25,6 @@     docs/morleyInterpreter.md     docs/morleyRuntime.md     docs/morleyTypechecker.md-    docs/language/morleyInstructions.md-    docs/language/morleyLanguage.md-    docs/language/morleyLet.md-    docs/language/morleyMacros.md-    docs/language/morleySyntaxSugar.md  source-repository head   type: git@@ -44,6 +39,7 @@       Morley.Micheline.Binary.Internal       Morley.Micheline.Class       Morley.Micheline.Expression+      Morley.Micheline.Expression.WithMeta       Morley.Micheline.Json       Morley.Michelson.Analyzer       Morley.Michelson.Doc@@ -53,17 +49,14 @@       Morley.Michelson.Interpret.Pack       Morley.Michelson.Interpret.Unpack       Morley.Michelson.Interpret.Utils-      Morley.Michelson.Let       Morley.Michelson.Macro       Morley.Michelson.Optimizer       Morley.Michelson.Parser       Morley.Michelson.Parser.Annotations       Morley.Michelson.Parser.Common       Morley.Michelson.Parser.Error-      Morley.Michelson.Parser.Ext       Morley.Michelson.Parser.Helpers       Morley.Michelson.Parser.Instr-      Morley.Michelson.Parser.Let       Morley.Michelson.Parser.Lexer       Morley.Michelson.Parser.Macro       Morley.Michelson.Parser.Type@@ -111,7 +104,6 @@       Morley.Michelson.Typed.Haskell.Value       Morley.Michelson.Typed.Instr       Morley.Michelson.Typed.Operation-      Morley.Michelson.Typed.OpSize       Morley.Michelson.Typed.Polymorphic       Morley.Michelson.Typed.Scope       Morley.Michelson.Typed.Sing@@ -127,11 +119,11 @@       Morley.Michelson.Untyped.Entrypoints       Morley.Michelson.Untyped.Ext       Morley.Michelson.Untyped.Instr-      Morley.Michelson.Untyped.OpSize       Morley.Michelson.Untyped.Type       Morley.Michelson.Untyped.Value       Morley.Michelson.Untyped.View       Morley.Tezos.Address+      Morley.Tezos.Address.Alias       Morley.Tezos.Core       Morley.Tezos.Crypto       Morley.Tezos.Crypto.BLS12381@@ -161,7 +153,6 @@       Morley.Util.Named       Morley.Util.Peano       Morley.Util.PeanoNatural-      Morley.Util.Positive       Morley.Util.Sing       Morley.Util.SizedList       Morley.Util.SizedList.Types@@ -237,6 +228,7 @@     , aeson-pretty     , base-noprelude >=4.7 && <5     , base58-bytestring+    , bimap     , binary     , bytestring     , constraints >=0.11@@ -264,6 +256,7 @@     , semigroups >=0.19.1     , show-type     , singletons+    , singletons-base     , syb     , template-haskell     , text@@ -354,6 +347,7 @@     , morley-prelude     , named     , optparse-applicative+    , singletons     , text     , vinyl     , with-utf8

@@ -29,13 +29,16 @@  import Control.Lens.Plated (universe) import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))+import Data.Generics (everything, mkQ) import Data.List qualified as List ((\\))+import Data.Map qualified as Map import Data.Singletons (Sing, withSingI)+import Data.Text qualified as T import GHC.Generics qualified as G import Language.Haskell.TH   (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD),   DerivStrategy(AnyclassStrategy), Info(TyConI), Kind, Loc(loc_module), Name, Q, TyLit(StrTyLit),-  TySynEqn(..), TyVarBndr, Type(..), cxt, instanceD, location, mkName, nameBase, ppr, reify,+  TySynEqn(..), TyVarBndr(..), Type(..), cxt, instanceD, location, mkName, nameBase, ppr, reify,   reifyInstances, standaloneDerivWithStrategyD) import Language.Haskell.TH.ReifyMany (reifyManyTyCons) import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)@@ -47,11 +50,12 @@   HasNoContract, HasNoNestedBigMaps, HasNoOp, IsoValue, Notes(..), OpPresence(..), Operation,   SingI(sing), SingT(..), StorageScope, T(..), ToT, Value, Value'(..), WellTyped,   checkContractTypePresence, checkOpPresence, toVal, withDict)-import Morley.Tezos.Address (Address)+import Morley.Tezos.Address (Address, TxRollupL2Address) import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto import Morley.Util.CustomGeneric-  (GenericStrategy, customGeneric', deriveFullType, haskellBalanced, reifyDataType)+  (GenericStrategy, customGeneric', deriveFullType, haskellBalanced,+  mangleGenericStrategyConstructors, mangleGenericStrategyFields, reifyDataType) import Morley.Util.Named hiding (Name) import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail) @@ -137,6 +141,7 @@   TAsRPC 'TBls12381G2 = 'TBls12381G2   TAsRPC 'TChest = 'TChest   TAsRPC 'TChestKey = 'TChestKey+  TAsRPC 'TTxRollupL2Address = 'TTxRollupL2Address   TAsRPC ('TSaplingState n) = ('TSaplingState n)   TAsRPC ('TSaplingTransaction n) = ('TSaplingTransaction n) @@ -261,6 +266,8 @@   type AsRPC Chest = Chest instance HasRPCRepr ChestKey where   type AsRPC ChestKey = ChestKey+instance HasRPCRepr TxRollupL2Address where+  type AsRPC TxRollupL2Address = TxRollupL2Address  ---------------------------------------------------------------------------- -- MaybeRPC@@ -422,14 +429,21 @@   -- that doesn't use `reify` (it should be easy enough).   repInstance <- reifyRepInstance typeName derivedType   currentModuleName <- loc_module <$> location-  let repTypeRPC = convertRep currentModuleName repInstance+  let repTypeRPC = convertRep currentModuleName repInstance tyVars   typeDecOfRPC <- mkTypeDeclaration typeName decCxt typeNameRPC tyVars mKind constructorsRPC +  -- Slightly modify the deriving strategy so that the field/constructor+  -- reordering function from original strategy acts on input field names in+  -- RPC type after stripping RPC suffix. Fix for #811+  let+    gs' = mangleGenericStrategyFields dropRPCSuffix $+            mangleGenericStrategyConstructors dropRPCSuffix gs+   mconcat <$> sequence     [ pure . one $ typeDecOfRPC     , one <$> mkAsRPCInstance fieldTypes derivedType derivedTypeRPC     , mkIsoValueInstance fieldTypesRPC derivedTypeRPC-    , customGeneric' (Just repTypeRPC) typeNameRPC derivedTypeRPC constructorsRPC gs+    , customGeneric' (Just repTypeRPC) typeNameRPC derivedTypeRPC constructorsRPC gs'     ]    where@@ -440,6 +454,9 @@     convertNameStr :: String -> String     convertNameStr s = s <> "RPC" +    dropRPCSuffix :: Text -> Text+    dropRPCSuffix = fromMaybe (error "Unexpected field/constructor without RPC suffix") . T.stripSuffix "RPC"+     convertName :: Name -> Name     convertName = mkName . convertNameStr . nameBase @@ -469,7 +486,7 @@       InfixC field1 _ field2 -> pure [snd field1, snd field2]       constr -> fail $ "Unsupported constructor for '" <> show typeName <> "': " <> show (ppr constr) -    mkTypeDeclaration :: Name -> Cxt -> Name -> [TyVarBndr] -> Maybe Kind -> [Con] -> Q Dec+    mkTypeDeclaration :: Name -> Cxt -> Name -> [TyVarBndr ()] -> Maybe Kind -> [Con] -> Q Dec     mkTypeDeclaration tyName decCxt typeNameRPC tyVars mKind constructorsRPC = do       typeInfo <- reify tyName       case typeInfo of@@ -485,9 +502,16 @@     -- 1. Inspect its metadata and append @RPC@ to the type/constructor/field names.     -- 2. Convert field types (e.g. @T@ becomes @AsRPC T@).     -- 3. Replace the Rep's module name with the name of the module of where this Q is being spliced.-    convertRep :: String -> TySynEqn -> Type-    convertRep currentModuleName (TySynEqn _tyVars _lhs rhs) = go rhs+    convertRep :: String -> TySynEqn -> [TyVarBndr a] -> Type+    convertRep currentModuleName (TySynEqn _tyVars lhs rhs) tvs = go rhs       where+        varMap = Map.fromList $ zip lhsTvs $ tvs <&> \case+          PlainTV vName _ -> vName+          KindedTV vName _ _ -> vName+        lhsTvs = everything (<>) (mempty `mkQ` (maybe mempty pure . varTName)) lhs+        varTName = \case+          VarT v -> Just v+          _ -> Nothing         go :: Type -> Type         go = \case           -- Rename type name and module name@@ -505,8 +529,11 @@           -- Replace field type @T@ with @AsRPC T@           ConT x `AppT` fieldType             | x == ''G.Rec0-            -> ConT x `AppT` convertFieldType fieldType+            -> ConT x `AppT` (convertFieldType $ replaceVars fieldType)           x `AppT` y -> go x `AppT` go y+          x -> replaceVars x+        replaceVars = \case+          VarT v -> VarT $ fromMaybe v $ Map.lookup v varMap           x -> x      -- | Lookup the generic 'Rep' type instance for the given type.@@ -611,6 +638,7 @@     VBls12381Fr {} -> v     VBls12381G1 {} -> v     VBls12381G2 {} -> v+    VTxRollupL2Address {} -> v  -- | Replaces all bigmap IDs with their corresponding bigmap values. -- This is the inverse of `valueAsRPC`.@@ -629,6 +657,7 @@       (STChainId {}, _) -> pure v       (STChest {}, _) -> pure v       (STChestKey {}, _) -> pure v+      (STTxRollupL2Address {}, _) -> pure v       (STOption sMaybe, VOption vMaybe) ->         withSingI sMaybe $           VOption <$> traverse (go sMaybe) vMaybe@@ -701,6 +730,7 @@     NTBls12381G1 {} -> notes     NTBls12381G2 {} -> notes     NTNever {} -> notes+    NTTxRollupL2Address {} -> notes     NTSaplingState {} -> notes     NTSaplingTransaction {} -> notes @@ -750,6 +780,7 @@       STTimestamp {} -> Dict       STAddress {} -> Dict       STNever {} -> Dict+      STTxRollupL2Address {} -> Dict       STSaplingState _ -> Dict       STSaplingTransaction _ -> Dict @@ -792,6 +823,7 @@   STChest {} -> Dict   STChestKey {} -> Dict   STNever {} -> Dict+  STTxRollupL2Address {} -> Dict   STSaplingState _ -> Dict   STSaplingTransaction _ -> Dict @@ -835,6 +867,7 @@   STBls12381G2 {} -> Dict   STTimestamp {} -> Dict   STAddress {} -> Dict+  STTxRollupL2Address {} -> Dict   STNever {} -> Dict   STSaplingState {} -> Dict   STSaplingTransaction {} -> Dict@@ -877,6 +910,7 @@   STNever {} -> Dict   STSaplingState {} -> Dict   STSaplingTransaction {} -> Dict+  STTxRollupL2Address {} -> Dict  -- | A proof that @AsRPC (Value t)@ does not contain big_maps. rpcHasNoNestedBigMapsEvi@@ -922,6 +956,7 @@   STNever {} -> Dict   STSaplingState {} -> Dict   STSaplingTransaction {} -> Dict+  STTxRollupL2Address {} -> Dict  -- | A proof that if @t@ does not contain any contract values, then neither does @TAsRPC t@. rpcHasNoContractEvi@@ -970,6 +1005,7 @@   STNever {} -> Dict   STSaplingState {} -> Dict   STSaplingTransaction {} -> Dict+  STTxRollupL2Address {} -> Dict  -- | A proof that if @t@ is a valid storage type, then so is @TAsRPC t@. rpcStorageScopeEvi :: forall (t :: T). StorageScope t :- StorageScope (TAsRPC t)

@@ -12,6 +12,7 @@   , contractFileOption   , nowOption   , levelOption+  , minBlockTimeOption   , maxStepsOption   , dbPathOption   , txDataOption@@ -20,6 +21,8 @@   , valueOption   , mutezOption   , addressOption+  , aliasOption+  , addressOrAliasOption   , onelineOption   , entrypointOption   , mTextOption@@ -42,6 +45,7 @@ import Morley.Michelson.Untyped (EpName) import Morley.Michelson.Untyped qualified as U import Morley.Tezos.Address (Address)+import Morley.Tezos.Address.Alias (AddressOrAlias(..), Alias(..)) import Morley.Tezos.Core (Mutez, Timestamp, parseTimestamp, timestampFromSeconds) import Morley.Tezos.Crypto import Morley.Util.CLI@@ -113,6 +117,14 @@   where     parser = Opt.maybeReader (Just . read) +minBlockTimeOption :: Opt.Parser (Maybe Natural)+minBlockTimeOption = optional $ option parser $+  long "min-block-time" <>+  metavar "NATURAL" <>+  help "Minimum time between blocks"+  where+    parser = Opt.maybeReader (Just . read)+ -- | Parser for gas limit on contract execution. maxStepsOption :: Opt.Parser Word64 maxStepsOption = mkCLOptionParser@@ -129,6 +141,20 @@   help "Path to DB with data which is used instead of real blockchain data" <>   Opt.showDefault +aliasOption :: String -> Opt.Parser Alias+aliasOption key = fmap Alias . Opt.strOption $+  long key <>+  metavar "ALIAS" <>+  help "An alias to be associated with the originated contract's address, e.g: 'alice', 'bob'"++-- | Generic parser to read an option of 'AddressOrAlias' type.+addressOrAliasOption+  :: Maybe AddressOrAlias+  -> "name" :! String+  -> "help" :! String+  -> Opt.Parser AddressOrAlias+addressOrAliasOption = mkCLOptionParser+ -- | Parser for transaction parameters. txDataOption :: Opt.Parser TxData txDataOption =@@ -150,7 +176,7 @@         , tdAmount = amount         } --- | Generic parser to read an option of 'KeyHash' type.+-- | Generic parser to read an option of t'KeyHash' type. keyHashOption ::   Maybe KeyHash -> "name" :! String -> "help" :! String -> Opt.Parser KeyHash keyHashOption = mkCLOptionParser

@@ -37,8 +37,8 @@  buildExpr :: Expression -> Bi.Builder buildExpr = \case-  ExpressionSeq xs -> buildWord8 2 <> buildDynamic buildList (DynamicSize xs)-  ExpressionPrim (MichelinePrimAp prim args annots) -> case (args, annots) of+  ExpSeq () xs -> buildWord8 2 <> buildDynamic buildList (DynamicSize xs)+  ExpPrim () (MichelinePrimAp prim args annots) -> case (args, annots) of     ([], []) -> buildWord8 3 <> buildPrim prim     ([], _) -> buildWord8 4 <> buildPrim prim <> buildAnnotationList annots     ([arg1], []) -> buildWord8 5 <> buildPrim prim <> buildExpr arg1@@ -46,9 +46,9 @@     ([arg1, arg2], []) -> buildWord8 7 <> buildPrim prim <> buildExpr arg1 <> buildExpr arg2     ([arg1, arg2], _) -> buildWord8 8 <> buildPrim prim <> buildExpr arg1 <> buildExpr arg2 <> buildAnnotationList annots     _ -> buildWord8 9 <> buildPrim prim <> buildDynamic buildList (DynamicSize args) <> buildAnnotationList annots-  ExpressionString x -> buildWord8 1 <> buildDynamic buildText (DynamicSize x)-  ExpressionInt x -> buildWord8 0 <> buildInteger x-  ExpressionBytes x -> buildWord8 10 <> buildDynamic buildByteString (DynamicSize x)+  ExpString () x -> buildWord8 1 <> buildDynamic buildText (DynamicSize x)+  ExpInt () x -> buildWord8 0 <> buildInteger x+  ExpBytes () x -> buildWord8 10 <> buildDynamic buildByteString (DynamicSize x)  buildList :: [Expression] -> Bi.Builder buildList = foldMap buildExpr@@ -75,17 +75,17 @@  getExpr :: Bi.Get Expression getExpr = Bi.getWord8 >>= \case-  0 -> ExpressionInt <$> getInteger-  1 -> ExpressionString . unDynamicSize <$> (getDynamic getText)-  2 -> ExpressionSeq . unDynamicSize <$> (getDynamic getList)-  3 -> ExpressionPrim . (\pn -> MichelinePrimAp pn [] []) <$> getPrim-  4 -> ExpressionPrim <$> (flip MichelinePrimAp [] <$> getPrim <*> getAnnotationList)-  5 -> ExpressionPrim <$> (MichelinePrimAp <$> getPrim <*> (one <$> getExpr) <*> pure [])-  6 -> ExpressionPrim <$> (MichelinePrimAp <$> getPrim <*> (one <$> getExpr) <*> getAnnotationList)-  7 -> ExpressionPrim <$> ((\n a -> MichelinePrimAp n a []) <$> getPrim <*> replicateM 2 getExpr)-  8 -> ExpressionPrim <$> (MichelinePrimAp <$> getPrim <*> replicateM 2 getExpr <*> getAnnotationList)-  9 -> ExpressionPrim <$> (MichelinePrimAp <$> getPrim <*> (unDynamicSize <$> (getDynamic getList)) <*> getAnnotationList)-  10 -> ExpressionBytes . unDynamicSize <$> (getDynamic getByteString)+  0 -> ExpInt () <$> getInteger+  1 -> ExpString () . unDynamicSize <$> (getDynamic getText)+  2 -> ExpSeq () . unDynamicSize <$> (getDynamic getList)+  3 -> ExpPrim () . (\pn -> MichelinePrimAp pn [] []) <$> getPrim+  4 -> ExpPrim () <$> (flip MichelinePrimAp [] <$> getPrim <*> getAnnotationList)+  5 -> ExpPrim () <$> (MichelinePrimAp <$> getPrim <*> (one <$> getExpr) <*> pure [])+  6 -> ExpPrim () <$> (MichelinePrimAp <$> getPrim <*> (one <$> getExpr) <*> getAnnotationList)+  7 -> ExpPrim () <$> ((\n a -> MichelinePrimAp n a []) <$> getPrim <*> replicateM 2 getExpr)+  8 -> ExpPrim () <$> (MichelinePrimAp <$> getPrim <*> replicateM 2 getExpr <*> getAnnotationList)+  9 -> ExpPrim () <$> (MichelinePrimAp <$> getPrim <*> (unDynamicSize <$> (getDynamic getList)) <*> getAnnotationList)+  10 -> ExpBytes () . unDynamicSize <$> (getDynamic getByteString)   _ -> fail "invalid Micheline expression tag"  getList :: Bi.Get [Expression]

@@ -5,991 +5,1024 @@ -- Micheline representation. module Morley.Micheline.Class   ( ToExpression (..)-  , FromExpressionError (..)-  , FromExpression (..)-  ) where--import Control.Lens ((<>~))-import Data.Bits (toIntegralSized)-import Data.Default (def)-import Data.Singletons (SingI(..), demote)-import Fmt (Buildable(..), indentF, pretty, unlinesF)--import Morley.Micheline.Expression-  (Annotation(..), Expression(..), MichelinePrimAp(..), _ExpressionPrim, isAnnotationField,-  isAnnotationType, isAnnotationVariable, mkAnns, mpaAnnotsL, toAnnSet)-import Morley.Michelson.Text (mkMText, unMText)-import Morley.Michelson.TypeCheck-  (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith)-import Morley.Michelson.TypeCheck.Instr (typeCheckValue)-import Morley.Michelson.Typed-  (Contract, HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType, rfAnyInstr,-  toUType)-import Morley.Michelson.Typed.Convert (convertContract, instrToOpsOptimized, untypeValueOptimized)-import Morley.Michelson.Untyped qualified as Untyped-import Morley.Michelson.Untyped.Annotation-  (AnnotationSet(..), FieldAnn, FieldTag, RootAnn, TypeAnn, TypeTag, VarAnn, VarTag, annsCount,-  emptyAnnSet, firstAnn, noAnn, secondAnn)-import Morley.Michelson.Untyped.Contract (ContractBlock(..), orderContractBlock)-import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..))-import Morley.Michelson.Untyped.Type (Ty(..))-import Morley.Michelson.Untyped.View---- | Type class that provides an ability to convert--- something to Micheline Expression.-class ToExpression a where-  toExpression :: a -> Expression--instance (HasNoOp t) => ToExpression (Value t) where-  toExpression = toExpression . untypeValueOptimized--instance ToExpression Untyped.Value where-  toExpression = \case-    Untyped.ValueInt v -> ExpressionInt v-    Untyped.ValueString s -> ExpressionString $ unMText s-    Untyped.ValueBytes (Untyped.InternalByteString bs) -> ExpressionBytes bs-    Untyped.ValueUnit -> PrimExpr "Unit" [] []-    Untyped.ValueTrue -> PrimExpr "True" [] []-    Untyped.ValueFalse -> PrimExpr "False" [] []-    Untyped.ValuePair l r ->-      PrimExpr "Pair" [toExpression l, toExpression r] []-    Untyped.ValueLeft v -> PrimExpr "Left" [toExpression v] []-    Untyped.ValueRight v -> PrimExpr "Right" [toExpression v] []-    Untyped.ValueSome v -> PrimExpr "Some" [toExpression v] []-    Untyped.ValueNone -> PrimExpr "None" [] []-    Untyped.ValueNil -> ExpressionSeq []-    Untyped.ValueSeq vs -> toExpression vs-    Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts-    Untyped.ValueLambda ops -> toExpression ops-    where-      eltToExpr :: Untyped.Elt ExpandedOp -> Expression-      eltToExpr (Untyped.Elt l r) = PrimExpr "Elt"-        [toExpression l, toExpression r] []---instance ToExpression (Instr inp out) where-  toExpression = toExpression . instrToOpsOptimized--instance ToExpression T where-  toExpression = toExpression . toUType--instance ToExpression (Notes t) where-  toExpression = toExpression . mkUType--instance ToExpression Untyped.T where-  toExpression = \case-    Untyped.TKey -> PrimExpr "key" [] []-    Untyped.TUnit -> PrimExpr "unit" [] []-    Untyped.TSignature -> PrimExpr "signature" [] []-    Untyped.TChainId -> PrimExpr "chain_id" [] []-    Untyped.TOption arg -> PrimExpr "option" [toExpression arg] []-    Untyped.TList arg -> PrimExpr "list" [toExpression arg] []-    Untyped.TSet arg -> PrimExpr "set" [toExpression arg] []-    Untyped.TOperation -> PrimExpr "operation" [] []-    Untyped.TContract arg -> PrimExpr "contract" [toExpression arg] []-    Untyped.TTicket arg -> PrimExpr "ticket" [toExpression arg] []-    t@Untyped.TPair{} -> PrimExpr "pair"-      (rightCombedPairToList (Ty t noAnn) (noAnn, noAnn)) []-    Untyped.TOr fa1 fa2 l r ->-      let exprL = addTrimmedAnns (toExpression l) [] [fa1] []-          exprR = addTrimmedAnns (toExpression r) [] [fa2] []-      in PrimExpr "or" [exprL, exprR] []-    Untyped.TLambda inp out ->-      PrimExpr "lambda" [toExpression inp, toExpression out] []-    Untyped.TMap k v ->-      PrimExpr "map" [toExpression k, toExpression v] []-    Untyped.TBigMap k v ->-      PrimExpr "big_map" [toExpression k, toExpression v] []-    Untyped.TInt -> PrimExpr "int" [] []-    Untyped.TNat -> PrimExpr "nat" [] []-    Untyped.TString -> PrimExpr "string" [] []-    Untyped.TBytes -> PrimExpr "bytes" [] []-    Untyped.TMutez -> PrimExpr "mutez" [] []-    Untyped.TBool -> PrimExpr "bool" [] []-    Untyped.TKeyHash -> PrimExpr "key_hash" [] []-    Untyped.TBls12381Fr -> PrimExpr "bls12_381_fr" [] []-    Untyped.TBls12381G1 -> PrimExpr "bls12_381_g1" [] []-    Untyped.TBls12381G2 -> PrimExpr "bls12_381_g2" [] []-    Untyped.TTimestamp -> PrimExpr "timestamp" [] []-    Untyped.TAddress -> PrimExpr "address" [] []-    Untyped.TChest -> PrimExpr "chest" [] []-    Untyped.TChestKey -> PrimExpr "chest_key" [] []-    Untyped.TNever -> PrimExpr "never" [] []-    Untyped.TSaplingState n -> PrimExpr "sapling_state" [naturalToExpr n] []-    Untyped.TSaplingTransaction n -> PrimExpr "sapling_transaction" [naturalToExpr n] []--    where-      addAnns :: Expression -> [Annotation] -> Expression-      addAnns e anns =-        e & _ExpressionPrim . mpaAnnotsL <>~ anns--      rightCombedPairToList :: Ty -> (FieldAnn, VarAnn) -> [Expression]-      rightCombedPairToList ty (fa, va) = case (ty, fa) of-        (Ty (Untyped.TPair fa1 fa2 va1 va2 l r) (Untyped.Annotation ""), Untyped.Annotation "") ->-          let annsL = mkAnns [] [fa1] [va1]-              exprL = toExpression l `addAnns` annsL-          in exprL : (rightCombedPairToList r (fa2, va2))-        _ ->-          let anns = mkAnns [] [fa] [va]-          in one $ toExpression ty `addAnns` anns--instance ToExpression Ty where-  toExpression (Ty t ta) = addTrimmedAnns (toExpression t) [ta] [] []--instance (ToExpression a) => ToExpression [a] where-  toExpression xs = ExpressionSeq $ toExpression <$> xs--instance (ToExpression a) => ToExpression (NonEmpty a) where-  toExpression = toExpression . toList--instance ToExpression Expression where-  toExpression = id--instance ToExpression ExpandedOp where-  toExpression = \case-    PrimEx instr   -> toExpression instr-    SeqEx s        -> ExpressionSeq $ toExpression <$> s-    WithSrcEx _ op -> toExpression op--instance ToExpression ViewName where-  toExpression (ViewName s) = ExpressionString s--instance ToExpression ExpandedInstr where-  toExpression = \case-    PUSH va ty v -> PrimExpr "PUSH" [toExpression ty, toExpression v] $-      mkAnns [] [] [va]-    DROP -> PrimExpr "DROP" [] []-    DROPN n -> PrimExpr "DROP" [wordToExpr n] []-    DUP va -> PrimExpr "DUP" [] $ mkAnns [] [] [va]-    DUPN va n -> PrimExpr "DUP" [wordToExpr n] $ mkAnns [] [] [va]-    SWAP -> PrimExpr "SWAP" [] []-    DIG n -> PrimExpr "DIG" [wordToExpr n] []-    DUG n -> PrimExpr "DUG" [wordToExpr n] []-    SOME ta va ->-      PrimExpr "SOME" [] $ mkAnns [ta] [] [va]-    NONE ta va ty -> PrimExpr "NONE" [toExpression ty] $ mkAnns [ta] [] [va]-    UNIT ta va -> PrimExpr "UNIT" [] $ mkAnns [ta] [] [va]-    IF_NONE ops1 ops2 ->-      PrimExpr "IF_NONE" [toExpression ops1, toExpression ops2] []-    PAIR ta va fa1 fa2 -> PrimExpr "PAIR" [] $ mkAnns [ta] [fa1, fa2] [va]-    UNPAIR va1 va2 fa1 fa2 -> PrimExpr "UNPAIR" [] $-      mkAnns [] [fa1, fa2] [va1, va2]-    PAIRN va n -> PrimExpr "PAIR" [wordToExpr n] $ mkAnns [] [] [va]-    UNPAIRN n -> PrimExpr "UNPAIR" [wordToExpr n] []-    CAR va fa -> PrimExpr "CAR" [] $ mkAnns [] [fa] [va]-    CDR va fa -> PrimExpr "CDR" [] $ mkAnns [] [fa] [va]-    LEFT ta va fa1 fa2 ty -> PrimExpr "LEFT" [toExpression ty] $-      mkAnns [ta] [fa1, fa2] [va]-    RIGHT ta va fa1 fa2 ty -> PrimExpr "RIGHT" [toExpression ty] $-      mkAnns [ta] [fa1, fa2] [va]-    IF_LEFT ops1 ops2 ->-      PrimExpr "IF_LEFT" [toExpression ops1, toExpression ops2] []-    NIL ta va ty -> PrimExpr "NIL" [toExpression ty] $-      mkAnns [ta] [] [va]-    CONS va -> PrimExpr "CONS" [] $ mkAnns [] [] [va]-    IF_CONS ops1 ops2 ->-      PrimExpr "IF_CONS" [toExpression ops1, toExpression ops2] []-    SIZE va -> PrimExpr "SIZE" [] $ mkAnns [] [] [va]-    EMPTY_SET ta va ty -> PrimExpr "EMPTY_SET" [toExpression ty] $-      mkAnns [ta] [] [va]-    EMPTY_MAP ta va kty vty ->-      PrimExpr "EMPTY_MAP" [toExpression kty, toExpression vty] $-      mkAnns [ta] [] [va]-    EMPTY_BIG_MAP ta va kty vty ->-      PrimExpr "EMPTY_BIG_MAP" [toExpression kty, toExpression vty] $-      mkAnns [ta] [] [va]-    MAP va ops -> PrimExpr "MAP" [toExpression ops] $ mkAnns [] [] [va]-    ITER ops -> PrimExpr "ITER" [toExpression ops] []-    MEM va -> PrimExpr "MEM" [] $ mkAnns [] [] [va]-    GET va -> PrimExpr "GET" [] $ mkAnns [] [] [va]-    GETN va n -> PrimExpr "GET" [wordToExpr n] $ mkAnns [] [] [va]-    UPDATE va -> PrimExpr "UPDATE" [] $ mkAnns [] [] [va]-    UPDATEN va n -> PrimExpr "UPDATE" [wordToExpr n] $ mkAnns [] [] [va]-    GET_AND_UPDATE va -> PrimExpr "GET_AND_UPDATE" [] $ mkAnns [] [] [va]-    IF ops1 ops2 ->-      PrimExpr "IF" [toExpression ops1, toExpression ops2] []-    LOOP ops -> PrimExpr "LOOP" [toExpression ops] []-    LOOP_LEFT ops -> PrimExpr "LOOP_LEFT" [toExpression ops] []-    LAMBDA va tyin tyout ops ->-      PrimExpr "LAMBDA" [ toExpression tyin-                            , toExpression tyout-                            , toExpression ops-                            ] $ mkAnns [] [] [va]-    EXEC va -> PrimExpr "EXEC" [] $ mkAnns [] [] [va]-    APPLY va -> PrimExpr "APPLY" [] $ mkAnns [] [] [va]-    DIP ops -> PrimExpr "DIP" [toExpression ops] []-    DIPN n ops -> PrimExpr "DIP" [wordToExpr n, toExpression ops] []-    FAILWITH -> PrimExpr "FAILWITH" [] []-    CAST va ty -> PrimExpr "CAST" [toExpression ty] $ mkAnns [] [] [va]-    RENAME va -> PrimExpr "RENAME" [] $ mkAnns [] [] [va]-    PACK va -> PrimExpr "PACK" [] $ mkAnns [] [] [va]-    UNPACK ta va ty -> PrimExpr "UNPACK" [toExpression ty] $-      mkAnns [ta] [] [va]-    CONCAT va -> PrimExpr "CONCAT" [] $ mkAnns [] [] [va]-    SLICE va -> PrimExpr "SLICE" [] $ mkAnns [] [] [va]-    ISNAT va -> PrimExpr "ISNAT" [] $ mkAnns [] [] [va]-    ADD va -> PrimExpr "ADD" [] $ mkAnns [] [] [va]-    SUB va -> PrimExpr "SUB" [] $ mkAnns [] [] [va]-    SUB_MUTEZ va -> PrimExpr "SUB_MUTEZ" [] $ mkAnns [] [] [va]-    MUL va -> PrimExpr "MUL" [] $ mkAnns [] [] [va]-    EDIV va -> PrimExpr "EDIV" [] $ mkAnns [] [] [va]-    ABS va -> PrimExpr "ABS" [] $ mkAnns [] [] [va]-    NEG va -> PrimExpr "NEG" [] $ mkAnns [] [] [va]-    LSL va -> PrimExpr "LSL" [] $ mkAnns [] [] [va]-    LSR va -> PrimExpr "LSR" [] $ mkAnns [] [] [va]-    OR va -> PrimExpr "OR" [] $ mkAnns [] [] [va]-    AND va -> PrimExpr "AND" [] $ mkAnns [] [] [va]-    XOR va -> PrimExpr "XOR" [] $ mkAnns [] [] [va]-    NOT va -> PrimExpr "NOT" [] $ mkAnns [] [] [va]-    COMPARE va -> PrimExpr "COMPARE" [] $ mkAnns [] [] [va]-    Untyped.EQ va -> PrimExpr "EQ" [] $ mkAnns [] [] [va]-    NEQ va -> PrimExpr "NEQ" [] $ mkAnns [] [] [va]-    Untyped.LT va -> PrimExpr "LT" [] $ mkAnns [] [] [va]-    Untyped.GT va -> PrimExpr "GT" [] $ mkAnns [] [] [va]-    LE va -> PrimExpr "LE" [] $ mkAnns [] [] [va]-    GE va -> PrimExpr "GE" [] $ mkAnns [] [] [va]-    INT va -> PrimExpr "INT" [] $ mkAnns [] [] [va]-    VIEW va n t -> PrimExpr "VIEW" [toExpression n, toExpression t] $-      mkAnns [] [] [va]-    SELF va fa -> PrimExpr "SELF" [] $ mkAnns [] [fa] [va]-    CONTRACT va fa ty -> PrimExpr "CONTRACT" [toExpression ty] $-      mkAnns [] [fa] [va]-    TRANSFER_TOKENS va -> PrimExpr "TRANSFER_TOKENS" [] $ mkAnns [] [] [va]-    SET_DELEGATE va -> PrimExpr "SET_DELEGATE" [] $ mkAnns [] [] [va]-    CREATE_CONTRACT va1 va2 c ->-      PrimExpr "CREATE_CONTRACT" [toExpression c] $-      mkAnns [] [] [va1, va2]-    IMPLICIT_ACCOUNT va -> PrimExpr "IMPLICIT_ACCOUNT" [] $-      mkAnns [] [] [va]-    NOW va -> PrimExpr "NOW" [] $ mkAnns [] [] [va]-    AMOUNT va -> PrimExpr "AMOUNT" [] $ mkAnns [] [] [va]-    BALANCE va -> PrimExpr "BALANCE" [] $ mkAnns [] [] [va]-    VOTING_POWER va -> PrimExpr "VOTING_POWER" [] $ mkAnns [] [] [va]-    TOTAL_VOTING_POWER va -> PrimExpr "TOTAL_VOTING_POWER" [] $-      mkAnns [] [] [va]-    CHECK_SIGNATURE va -> PrimExpr "CHECK_SIGNATURE" [] $ mkAnns [] [] [va]-    SHA256 va -> PrimExpr "SHA256" [] $ mkAnns [] [] [va]-    SHA512 va -> PrimExpr "SHA512" [] $ mkAnns [] [] [va]-    BLAKE2B va -> PrimExpr "BLAKE2B" [] $ mkAnns [] [] [va]-    SHA3 va -> PrimExpr "SHA3" [] $ mkAnns [] [] [va]-    KECCAK va -> PrimExpr "KECCAK" [] $ mkAnns [] [] [va]-    HASH_KEY va -> PrimExpr "HASH_KEY" [] $ mkAnns [] [] [va]-    PAIRING_CHECK va -> PrimExpr "PAIRING_CHECK" [] $ mkAnns [] [] [va]-    SOURCE va -> PrimExpr "SOURCE" [] $ mkAnns [] [] [va]-    SENDER va -> PrimExpr "SENDER" [] $ mkAnns [] [] [va]-    ADDRESS va -> PrimExpr "ADDRESS" [] $ mkAnns [] [] [va]-    CHAIN_ID va -> PrimExpr "CHAIN_ID" [] $ mkAnns [] [] [va]-    LEVEL va -> PrimExpr "LEVEL" [] $ mkAnns [] [] [va]-    SELF_ADDRESS va -> PrimExpr "SELF_ADDRESS" [] $ mkAnns [] [] [va]-    TICKET va -> PrimExpr "TICKET" [] $ mkAnns [] [] [va]-    READ_TICKET va -> PrimExpr "READ_TICKET" [] $ mkAnns [] [] [va]-    SPLIT_TICKET va -> PrimExpr "SPLIT_TICKET" [] $ mkAnns [] [] [va]-    JOIN_TICKETS va -> PrimExpr "JOIN_TICKETS" [] $ mkAnns [] [] [va]-    OPEN_CHEST va -> PrimExpr "OPEN_CHEST" [] $ mkAnns [] [] [va]-    NEVER -> PrimExpr "NEVER" [] []-    EXT _ -> ExpressionSeq []-    SAPLING_EMPTY_STATE va n -> PrimExpr "SAPLING_EMPTY_STATE" [naturalToExpr n] $ mkAnns [] [] [va]-    SAPLING_VERIFY_UPDATE va -> PrimExpr "SAPLING_VERIFY_UPDATE" [] $ mkAnns [] [] [va]--instance ToExpression Untyped.Contract where-  toExpression contract-    = ExpressionSeq $ Untyped.mapEntriesOrdered contract-          (\(Untyped.ParameterType ty rootAnn) -> PrimExpr "parameter"-            [insertRootAnn (toExpression ty) rootAnn] [])-          (\storage -> PrimExpr "storage" [toExpression storage] [])-          (\code -> PrimExpr "code" [toExpression code] [])-          (\Untyped.View{..} -> PrimExpr "view"-            [toExpression viewName, toExpression viewArgument, toExpression viewReturn, toExpression viewCode] []-          )--instance ToExpression (Contract cp st) where-  toExpression = toExpression . convertContract---- | Errors that can happen when we convert an 'Expression' to our--- data type.-data FromExpressionError = FromExpressionError Expression Text-  deriving stock (Show, Eq)--instance Buildable FromExpressionError where-  build (FromExpressionError expr err) =-    unlinesF-      [ "Failed to convert expression:"-      , indentF 2 $ build expr-      , ""-      , "Error:"-      , indentF 2 $ build err-      ]--instance Exception FromExpressionError where-  displayException = pretty---- | Type class that provides the ability to convert--- something from a Micheline Expression.-class FromExpression a where-  fromExpression :: Expression -> Either FromExpressionError a--instance (SingI t) => FromExpression (Value t) where-  fromExpression expr =-    case fromExpression @Untyped.Value expr of-    Right uv -> case typeCheck uv of-      Left tcErr -> Left $ FromExpressionError expr $-        pretty $ unlinesF-          [ "Failed to typecheck expression as a value of type:"-          , indentF 2 $ build $ demote @t-          , ""-          , "Typechecker error:"-          , indentF 2 $ build tcErr-          ]-      Right tv -> Right tv-    Left e -> Left e-    where-      typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $-        (runTypeCheck $ TypeCheckValue (uv, demote @t)) $-        usingReaderT def $-        typeCheckValue uv--instance FromExpression Untyped.Value where-  fromExpression e = case e of-    ExpressionInt v -> pure $ Untyped.ValueInt v-    ExpressionString s -> first (FromExpressionError e)-      (Untyped.ValueString <$> mkMText s)-    ExpressionBytes bs -> pure $ Untyped.ValueBytes $ Untyped.InternalByteString bs-    PrimExpr "Unit" [] [] -> pure Untyped.ValueUnit-    PrimExpr "True" [] [] -> pure Untyped.ValueTrue-    PrimExpr "False" [] [] -> pure Untyped.ValueFalse-    PrimExpr "Pair" [l, r] [] -> do-      l' <- fromExpression l-      r' <- fromExpression r-      pure $ Untyped.ValuePair l' r'-    PrimExpr "Pair" args [] ->-      case (nonEmpty args) >>= forbidSingletonList of-        Nothing -> Left $ FromExpressionError e-          "Expected a pair with at least 2 arguments"-        Just args' -> fromExpression $ seqToPairExpr args' "Pair"-    PrimExpr "Left" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.ValueLeft arg'-    PrimExpr "Right" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.ValueRight arg'-    PrimExpr "Some" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.ValueSome arg'-    PrimExpr "None" [] [] -> pure Untyped.ValueNone-    ExpressionSeq [] -> pure Untyped.ValueNil-    ExpressionSeq (h : t) ->-      case fromExpression @Untyped.ExpandedOp h of-      Right op -> do-        ops <- traverse (fromExpression @Untyped.ExpandedOp) t-        pure . Untyped.ValueLambda $ op :| ops-      Left _ -> case exprToElt h of-        Right elt -> do-          elts <- traverse exprToElt t-          pure . Untyped.ValueMap $ elt :| elts-        Left _ -> case fromExpression h of-          Left (FromExpressionError err _) -> Left $ FromExpressionError err-            "Value, instruction or 'Elt' expression expected"-          Right h' -> do-            t' <- traverse fromExpression t-            pure . Untyped.ValueSeq $ h' :| t'-    _ -> Left $ FromExpressionError e "Expected a value"-    where-      exprToElt :: Expression -> Either FromExpressionError (Untyped.Elt ExpandedOp)-      exprToElt ex = case ex of-        PrimExpr "Elt" [l, r] [] -> do-          l' <- fromExpression l-          r' <- fromExpression r-          pure $ Untyped.Elt l' r'-        PrimExpr "Elt" _ [] -> Left $ FromExpressionError ex-          "Expected 'Elt' expression with exactly 2 elements"-        PrimExpr "Elt" _ _ -> Left $ FromExpressionError ex-          "Expected 'Elt' expression without annotations"-        _ -> Left $ FromExpressionError ex "Expected 'Elt' expression"--instance (FromExpression a) => FromExpression [a] where-  fromExpression = \case-    ExpressionSeq exprs -> traverse fromExpression exprs-    e -> Left $ FromExpressionError e "'ExpressionSeq' expected"--instance FromExpression ExpandedOp where-  fromExpression = \case-    ExpressionSeq s -> SeqEx <$> traverse fromExpression s-    e               -> PrimEx <$> fromExpression e--instance FromExpression ExpandedInstr where-  fromExpression e = let annSet = getAnnSet e in case e of-    PrimExpr "DROP" [n] [] -> do-      n' <- intExprToWord n-      pure $ DROPN n'-    PrimExpr "DROP" [] _ -> pure $ DROP-    PrimExpr "DUP" [n] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      let va = firstAnn @VarTag annSet-      n' <- intExprToWord n-      pure $ DUPN va n'-    PrimExpr "DUP" [] _ ->-      let va = firstAnn @VarTag annSet-      in checkAnnsCount e annSet (0, 0, 1) $> DUP va-    PrimExpr "SWAP" [] [] -> pure $ SWAP-    PrimExpr "DIG" [n] [] -> do-      n' <- intExprToWord n-      pure $ DIG $ n'-    PrimExpr "DUG" [n] [] -> do-      n' <- intExprToWord n-      pure $ DUG n'-    PrimExpr "PUSH" [t, v] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      let va = firstAnn @VarTag annSet-      t' <- fromExpression @Ty t-      v' <- fromExpression @Untyped.Value v-      pure $ PUSH va t' v'-    PrimExpr "SOME" [] _ ->-      let ta = firstAnn @TypeTag annSet-          va = firstAnn @VarTag annSet-      in checkAnnsCount e annSet (1, 0, 1) $> SOME ta va-    PrimExpr "NONE" [t] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      let ta = firstAnn @TypeTag annSet-      let va = firstAnn @VarTag annSet-      t' <- fromExpression @Ty t-      pure $ NONE ta va t'-    PrimExpr "UNIT" [] _ ->-      let ta = firstAnn @TypeTag annSet-          va = firstAnn @VarTag annSet-      in checkAnnsCount e annSet (1, 0, 1) $> UNIT ta va-    PrimExpr "IF_NONE" [ops1, ops2] [] -> do-      ops1' <- fromExpression @([ExpandedOp]) ops1-      ops2' <- fromExpression @([ExpandedOp]) ops2-      pure $ IF_NONE ops1' ops2'-    PrimExpr "PAIR" [] _ ->-      let ta = firstAnn @TypeTag annSet-          va = firstAnn @VarTag annSet-          fa1 = firstAnn @FieldTag annSet-          fa2 = secondAnn @FieldTag annSet-      in (checkAnnsCount e annSet (1, 2, 1)) $> PAIR ta va fa1 fa2-    PrimExpr "UNPAIR" [] _ ->-      let va1 = firstAnn @VarTag annSet-          va2 = secondAnn @VarTag annSet-          fa1 = firstAnn @FieldTag annSet-          fa2 = secondAnn @FieldTag annSet-      in checkAnnsCount e annSet (0, 2, 2) $> UNPAIR va1 va2 fa1 fa2-    PrimExpr "PAIR" [n] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      n' <- intExprToWord n-      let va = firstAnn @VarTag annSet-      pure $ PAIRN va n'-    PrimExpr "UNPAIR" [n] [] -> do-      n' <- intExprToWord n-      pure $ UNPAIRN n'-    PrimExpr "CAR" [] _ ->-      let va = firstAnn @VarTag annSet-          fa = firstAnn @FieldTag annSet-      in checkAnnsCount e annSet (0, 1, 1) $> CAR va fa-    PrimExpr "CDR" [] _ ->-      let va = firstAnn @VarTag annSet-          fa = firstAnn @FieldTag annSet-      in checkAnnsCount e annSet (0, 1, 1) $> CDR va fa-    PrimExpr "LEFT" [t] _ -> do-      checkAnnsCount e annSet (1, 2, 1)-      t' <- fromExpression @Ty t-      let ta = firstAnn @TypeTag annSet-      let va = firstAnn @VarTag annSet-      let fa1 = firstAnn @FieldTag annSet-      let fa2 = secondAnn @FieldTag annSet-      pure $ LEFT ta va fa1 fa2 t'-    PrimExpr "RIGHT" [t] _ -> do-      checkAnnsCount e annSet (1, 2, 1)-      t' <- fromExpression @Ty t-      let ta = firstAnn @TypeTag annSet-      let va = firstAnn @VarTag annSet-      let fa1 = firstAnn @FieldTag annSet-      let fa2 = secondAnn @FieldTag annSet-      pure $ RIGHT ta va fa1 fa2 t'-    PrimExpr "IF_LEFT" [ops1, ops2] [] -> do-      ops1' <- fromExpression @([ExpandedOp]) ops1-      ops2' <- fromExpression @([ExpandedOp]) ops2-      pure $ IF_LEFT ops1' ops2'-    PrimExpr "NIL" [t] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      t' <- fromExpression @Ty t-      let va = firstAnn @VarTag annSet-      let ta = firstAnn @TypeTag annSet-      pure $ NIL ta va t'-    PrimExpr "CONS" [] anns -> mkInstrWithVarAnn CONS anns-    PrimExpr "IF_CONS" [ops1, ops2] [] -> do-      ops1' <- fromExpression @([ExpandedOp]) ops1-      ops2' <- fromExpression @([ExpandedOp]) ops2-      pure $ IF_CONS ops1' ops2'-    PrimExpr "SIZE" [] anns -> mkInstrWithVarAnn SIZE anns-    PrimExpr "EMPTY_SET" [t] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      t' <- fromExpression @Ty t-      let va = firstAnn @VarTag annSet-      let ta = firstAnn @TypeTag annSet-      pure $ EMPTY_SET ta va t'-    PrimExpr "EMPTY_MAP" [kt, vt] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      kt' <- fromExpression @Ty kt-      vt' <- fromExpression @Ty vt-      let va = firstAnn @VarTag annSet-      let ta = firstAnn @TypeTag annSet-      pure $ EMPTY_MAP ta va kt' vt'-    PrimExpr "EMPTY_BIG_MAP" [kt, vt] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      kt' <- fromExpression @Ty kt-      vt' <- fromExpression @Ty vt-      let va = firstAnn @VarTag annSet-      let ta = firstAnn @TypeTag annSet-      pure $ EMPTY_BIG_MAP ta va kt' vt'-    PrimExpr "MAP" [ops] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      ops' <- fromExpression @([ExpandedOp]) ops-      let va = firstAnn @VarTag annSet-      pure $ MAP va ops'-    PrimExpr "ITER" [ops] [] -> do-      ops' <- fromExpression @([ExpandedOp]) ops-      pure $ ITER ops'-    PrimExpr "MEM" [] anns -> mkInstrWithVarAnn MEM anns-    PrimExpr "GET" [] anns -> mkInstrWithVarAnn GET anns-    PrimExpr "GET" [n] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      n' <- intExprToWord n-      let va = firstAnn @VarTag annSet-      pure $ GETN va n'-    PrimExpr "UPDATE" [] anns -> mkInstrWithVarAnn UPDATE anns-    PrimExpr "UPDATE" [n] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      n' <- intExprToWord n-      let va = firstAnn @VarTag annSet-      pure $ UPDATEN va n'-    PrimExpr "GET_AND_UPDATE" [] anns ->-      mkInstrWithVarAnn GET_AND_UPDATE anns-    PrimExpr "IF" [ops1, ops2] [] -> do-      ops1' <- fromExpression @([ExpandedOp]) ops1-      ops2' <- fromExpression @([ExpandedOp]) ops2-      pure $ IF ops1' ops2'-    PrimExpr "LOOP" [ops] [] -> do-      ops' <- fromExpression @([ExpandedOp]) ops-      pure $ LOOP ops'-    PrimExpr "LOOP_LEFT" [ops] [] -> do-      ops' <- fromExpression @([ExpandedOp]) ops-      pure $ LOOP_LEFT ops'-    PrimExpr "LAMBDA" [inp, out, ops] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      inp' <- fromExpression @Ty inp-      out' <- fromExpression @Ty out-      ops' <- fromExpression @([ExpandedOp]) ops-      let va = firstAnn @VarTag annSet-      pure $ LAMBDA va inp' out' ops'-    PrimExpr "EXEC" [] anns -> mkInstrWithVarAnn EXEC anns-    PrimExpr "APPLY" [] anns -> mkInstrWithVarAnn APPLY anns-    PrimExpr "DIP" [ops] [] -> do-      ops' <- fromExpression @([ExpandedOp]) ops-      pure $ DIP ops'-    PrimExpr "DIP" [n, ops] [] -> do-      n' <- intExprToWord n-      ops' <- fromExpression @([ExpandedOp]) ops-      pure $ DIPN n' ops'-    PrimExpr "FAILWITH" [] [] -> pure FAILWITH-    PrimExpr "CAST" [t] _ -> do-      checkAnnsCount e annSet (0, 0, 1)-      t' <- fromExpression @Ty t-      let va = firstAnn @VarTag annSet-      pure $ CAST va t'-    PrimExpr "RENAME" [] anns -> mkInstrWithVarAnn RENAME anns-    PrimExpr "PACK" [] anns -> mkInstrWithVarAnn PACK anns-    PrimExpr "UNPACK" [t] _ -> do-      checkAnnsCount e annSet (1, 0, 1)-      t' <- fromExpression @Ty t-      let ta = firstAnn @TypeTag annSet-      let va = firstAnn @VarTag annSet-      pure $ UNPACK ta va t'-    PrimExpr "CONCAT" [] anns -> mkInstrWithVarAnn CONCAT anns-    PrimExpr "SLICE" [] anns -> mkInstrWithVarAnn SLICE anns-    PrimExpr "ISNAT" [] anns -> mkInstrWithVarAnn ISNAT anns-    PrimExpr "ADD" [] anns -> mkInstrWithVarAnn ADD anns-    PrimExpr "SUB" [] anns -> mkInstrWithVarAnn SUB anns-    PrimExpr "SUB_MUTEZ" [] anns -> mkInstrWithVarAnn SUB_MUTEZ anns-    PrimExpr "MUL" [] anns -> mkInstrWithVarAnn MUL anns-    PrimExpr "EDIV" [] anns -> mkInstrWithVarAnn EDIV anns-    PrimExpr "ABS" [] anns -> mkInstrWithVarAnn ABS anns-    PrimExpr "NEG" [] anns -> mkInstrWithVarAnn NEG anns-    PrimExpr "LSL" [] anns -> mkInstrWithVarAnn LSL anns-    PrimExpr "LSR" [] anns -> mkInstrWithVarAnn LSR anns-    PrimExpr "OR" [] anns -> mkInstrWithVarAnn OR anns-    PrimExpr "AND" [] anns -> mkInstrWithVarAnn AND anns-    PrimExpr "XOR" [] anns -> mkInstrWithVarAnn XOR anns-    PrimExpr "NOT" [] anns -> mkInstrWithVarAnn NOT anns-    PrimExpr "COMPARE" [] anns -> mkInstrWithVarAnn COMPARE anns-    PrimExpr "EQ" [] anns -> mkInstrWithVarAnn Untyped.EQ anns-    PrimExpr "NEQ" [] anns -> mkInstrWithVarAnn NEQ anns-    PrimExpr "LT" [] anns -> mkInstrWithVarAnn Untyped.LT anns-    PrimExpr "GT" [] anns -> mkInstrWithVarAnn Untyped.GT anns-    PrimExpr "LE" [] anns -> mkInstrWithVarAnn LE anns-    PrimExpr "GE" [] anns -> mkInstrWithVarAnn GE anns-    PrimExpr "INT" [] anns -> mkInstrWithVarAnn INT anns-    PrimExpr "VIEW" [name, t] _ -> do-      let va = firstAnn @VarTag annSet-      name' <- fromExpression @ViewName name-      t' <- fromExpression @Ty t-      checkAnnsCount e annSet (0, 0, 1) $> VIEW va name' t'-    PrimExpr "SELF" [] _ ->-      let fa = firstAnn @FieldTag annSet-          va = firstAnn @VarTag annSet-      in checkAnnsCount e annSet (0, 1, 1) $> SELF va fa-    PrimExpr "CONTRACT" [t] _ -> do-      checkAnnsCount e annSet (0, 1, 1)-      t' <- fromExpression @Ty t-      let va = firstAnn @VarTag annSet-      let fa = firstAnn @FieldTag annSet-      pure $ CONTRACT va fa t'-    PrimExpr "TRANSFER_TOKENS" [] anns ->-      mkInstrWithVarAnn TRANSFER_TOKENS anns-    PrimExpr "SET_DELEGATE" [] anns ->-      mkInstrWithVarAnn SET_DELEGATE anns-    PrimExpr "CREATE_CONTRACT" [c] _ -> do-      checkAnnsCount e annSet (0, 0, 2)-      c' <- fromExpression @Untyped.Contract c-      let va1 = firstAnn @VarTag annSet-      let va2 = secondAnn @VarTag annSet-      pure $ CREATE_CONTRACT va1 va2 c'-    PrimExpr "IMPLICIT_ACCOUNT" [] anns ->-      mkInstrWithVarAnn IMPLICIT_ACCOUNT anns-    PrimExpr "NOW" [] anns -> mkInstrWithVarAnn NOW anns-    PrimExpr "AMOUNT" [] anns -> mkInstrWithVarAnn AMOUNT anns-    PrimExpr "BALANCE" [] anns -> mkInstrWithVarAnn BALANCE anns-    PrimExpr "VOTING_POWER" [] anns ->-      mkInstrWithVarAnn VOTING_POWER anns-    PrimExpr "TOTAL_VOTING_POWER" [] anns ->-      mkInstrWithVarAnn TOTAL_VOTING_POWER anns-    PrimExpr "CHECK_SIGNATURE" [] anns ->-      mkInstrWithVarAnn CHECK_SIGNATURE anns-    PrimExpr "SHA256" [] anns -> mkInstrWithVarAnn SHA256 anns-    PrimExpr "SHA512" [] anns -> mkInstrWithVarAnn SHA512 anns-    PrimExpr "BLAKE2B" [] anns -> mkInstrWithVarAnn BLAKE2B anns-    PrimExpr "SHA3" [] anns -> mkInstrWithVarAnn SHA3 anns-    PrimExpr "KECCAK" [] anns -> mkInstrWithVarAnn KECCAK anns-    PrimExpr "HASH_KEY" [] anns -> mkInstrWithVarAnn HASH_KEY anns-    PrimExpr "PAIRING_CHECK" [] anns ->-      mkInstrWithVarAnn PAIRING_CHECK anns-    PrimExpr "SOURCE" [] anns -> mkInstrWithVarAnn SOURCE anns-    PrimExpr "SENDER" [] anns -> mkInstrWithVarAnn SENDER anns-    PrimExpr "ADDRESS" [] anns -> mkInstrWithVarAnn ADDRESS anns-    PrimExpr "CHAIN_ID" [] anns -> mkInstrWithVarAnn CHAIN_ID anns-    PrimExpr "LEVEL" [] anns -> mkInstrWithVarAnn LEVEL anns-    PrimExpr "SELF_ADDRESS" [] anns ->-      mkInstrWithVarAnn SELF_ADDRESS anns-    PrimExpr "NEVER" [] [] -> pure NEVER-    PrimExpr "TICKET" [] anns -> mkInstrWithVarAnn TICKET anns-    PrimExpr "READ_TICKET" [] anns ->-      mkInstrWithVarAnn READ_TICKET anns-    PrimExpr "SPLIT_TICKET" [] anns ->-      mkInstrWithVarAnn SPLIT_TICKET anns-    PrimExpr "JOIN_TICKETS" [] anns ->-      mkInstrWithVarAnn JOIN_TICKETS anns-    _ -> Left $ FromExpressionError e "Expected an instruction"--    where-      mkInstrWithVarAnn-        :: (VarAnn -> ExpandedInstr)-        -> [Annotation]-        -> Either FromExpressionError ExpandedInstr-      mkInstrWithVarAnn ctor anns =-        let annSet = toAnnSet anns-            va = firstAnn @VarTag annSet-        in checkAnnsCount e annSet (0, 0, 1) $> ctor va--      getAnnSet :: Expression -> AnnotationSet-      getAnnSet = \case-        PrimExpr _ _ anns -> toAnnSet anns-        _                 -> emptyAnnSet--instance FromExpression Untyped.Contract where-  fromExpression blocks = case blocks of-    ExpressionSeq bs -> do-      bs' <- mapM exprToCB bs-      maybeToRight (FromExpressionError blocks "Something's wrong with top-level contract blocks")-        (orderContractBlock bs')-    expr -> Left $ FromExpressionError expr "Failed to parse contract, expected sequence"-    where-      exprToCB-        :: Expression-        -> Either FromExpressionError (ContractBlock ExpandedOp)-      exprToCB e = case e of-        PrimExpr "parameter" args anns -> mkCbParam e args anns-        PrimExpr "storage"   args anns -> mkCBStorage e args anns-        PrimExpr "code"      args anns -> mkCBCode e args anns-        PrimExpr "view"      args anns -> mkCBView e args anns-        _                              ->-          Left $ FromExpressionError e "Unexpected primitive at contract top-level"--      mkCbParam-        :: Expression-        -> [Expression]-        -> [Annotation]-        -> Either FromExpressionError (ContractBlock ExpandedOp)-      mkCbParam e args anns = case (args, anns) of-        ([p], []) -> do-          let annSet = toAnnSet (p ^. _ExpressionPrim . mpaAnnotsL)-          let rootAnn = firstAnn @FieldTag annSet-          unless (secondAnn @FieldTag annSet == noAnn) $-            Left $ FromExpressionError p-              "Expected parameter with at most 1 root annotation"-          p' <- fromExpression @Ty-            (p & _ExpressionPrim . mpaAnnotsL %~ filter (not . isAnnotationField))-          pure $ CBParam $ Untyped.ParameterType p' rootAnn-        _ -> Left $ FromExpressionError e-          "Expected 'parameter' block without annotations and exactly 1 argument"--      mkCBStorage-        :: Expression-        -> [Expression]-        -> [Annotation]-        -> Either FromExpressionError (ContractBlock ExpandedOp)-      mkCBStorage e args anns = case (args, anns) of-        ([s], []) -> do-          s' <- fromExpression @Ty s-          pure $ CBStorage s'-        _ -> Left $ FromExpressionError e-               "Expected 'storage' block without annotations and exactly 1 argument"--      mkCBCode-        :: Expression-        -> [Expression]-        -> [Annotation]-        -> Either FromExpressionError (ContractBlock ExpandedOp)-      mkCBCode e args anns = case (args, anns) of-        ([ops], []) -> do-          ops' <- fromExpression @([ExpandedOp]) ops-          pure $ CBCode ops'-        _ -> Left $ FromExpressionError e-               "Expected 'code' block without annotations"--      mkCBView-        :: Expression-        -> [Expression]-        -> [Annotation]-        -> Either FromExpressionError (ContractBlock ExpandedOp)-      mkCBView e args anns = case (args, anns) of-        ([name, arg, ret, ops], []) -> do-          name' <- fromExpression name-          arg' <- fromExpression arg-          ret' <- fromExpression ret-          ops' <- fromExpression @[ExpandedOp] ops-          pure $ CBView $ Untyped.View name' arg' ret' ops'-        (_, _ : _) ->-          Left $ FromExpressionError e-               "Expected 'view' block without annotations"-        (_, []) ->-          Left $ FromExpressionError e-               "Invalid 'view' block, expected 4 expressions in it"--instance FromExpression Untyped.T where-  fromExpression e = case e of-    PrimExpr "key" [] [] -> pure Untyped.TKey-    PrimExpr "unit" [] [] -> pure Untyped.TUnit-    PrimExpr "signature" [] [] -> pure Untyped.TSignature-    PrimExpr "chain_id" [] [] -> pure Untyped.TChainId-    PrimExpr "option" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.TOption arg'-    PrimExpr "list" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.TList arg'-    PrimExpr "set" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.TSet arg'-    PrimExpr "operation" [] [] -> pure Untyped.TOperation-    PrimExpr "contract" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.TContract arg'-    PrimExpr "ticket" [arg] [] -> do-      arg' <- fromExpression arg-      pure $ Untyped.TTicket arg'-    PrimExpr "or" [arg1, arg2] [] -> do-      let as1 = toAnnSet $ arg1 ^. _ExpressionPrim . mpaAnnotsL-      let as2 = toAnnSet $ arg2 ^. _ExpressionPrim . mpaAnnotsL-      checkAnnsCount e as1 (1, 1, 0)-      checkAnnsCount e as2 (1, 1, 0)-      let fa1 = firstAnn @FieldTag as1-      let fa2 = firstAnn @FieldTag as2-      l <- fromExpression $ removeAnns arg1 isAnnotationField-      r <- fromExpression $ removeAnns arg2 isAnnotationField-      pure $ Untyped.TOr fa1 fa2 l r-    PrimExpr "pair" [arg1, arg2] [] -> do-      let as1 = toAnnSet $ arg1 ^. _ExpressionPrim . mpaAnnotsL-      let as2 = toAnnSet $ arg2 ^. _ExpressionPrim . mpaAnnotsL-      checkAnnsCount e as1 (1, 1, 1)-      checkAnnsCount e as2 (1, 1, 1)-      let fa1 = firstAnn @FieldTag as1-      let fa2 = firstAnn @FieldTag as2-      let va1 = firstAnn @VarTag as1-      let va2 = firstAnn @VarTag as2-      l <- fromExpression $ removeAnns arg1-        (isAnnotationField || isAnnotationVariable)-      r <- fromExpression $ removeAnns arg2-        (isAnnotationField || isAnnotationVariable)-      pure $ Untyped.TPair fa1 fa2 va1 va2 l r-    PrimExpr "pair" args [] ->-      case (nonEmpty args) >>= forbidSingletonList of-        Nothing -> Left $ FromExpressionError e-          "Expected a pair with at least 2 arguments"-        Just args' -> fromExpression $ seqToPairExpr args' "pair"-    PrimExpr "lambda" args [] -> mkDoubleParamType Untyped.TLambda args e-      "Expected a lambda with input and output types"-    PrimExpr "map" args [] -> mkDoubleParamType Untyped.TMap args e-      "Expected a map with key and value types"-    PrimExpr "big_map" args [] -> mkDoubleParamType Untyped.TBigMap args e-      "Expected a big_map with key and value types"-    PrimExpr "int" [] [] -> pure Untyped.TInt-    PrimExpr "nat" [] [] -> pure Untyped.TNat-    PrimExpr "string" [] [] -> pure Untyped.TString-    PrimExpr "bytes" [] [] -> pure Untyped.TBytes-    PrimExpr "mutez" [] [] -> pure Untyped.TMutez-    PrimExpr "bool" [] [] -> pure Untyped.TBool-    PrimExpr "key_hash" [] [] -> pure Untyped.TKeyHash-    PrimExpr "bls12_381_fr" [] [] -> pure Untyped.TBls12381Fr-    PrimExpr "bls12_381_g1" [] [] -> pure Untyped.TBls12381G1-    PrimExpr "bls12_381_g2" [] [] -> pure Untyped.TBls12381G2-    PrimExpr "timestamp" [] [] -> pure Untyped.TTimestamp-    PrimExpr "address" [] [] -> pure Untyped.TAddress-    PrimExpr "chest" [] [] -> pure Untyped.TChest-    PrimExpr "chest_key" [] [] -> pure Untyped.TChestKey-    PrimExpr "never" [] [] -> pure Untyped.TNever-    PrimExpr "sapling_state" [n] [] -> do-      n' <- natExprToNatural n-      pure $ Untyped.TSaplingState n'-    PrimExpr "sapling_transaction" [n] [] -> do-      n' <- natExprToNatural n-      pure $ Untyped.TSaplingState n'-    _ -> Left $ FromExpressionError e "Expected a type"-    where-      mkDoubleParamType-        :: (Ty -> Ty -> Untyped.T)-        -> [Expression]-        -> Expression-        -> Text-        -> Either FromExpressionError Untyped.T-      mkDoubleParamType ctor args expr msg = do-        case args of-          [arg1, arg2] -> do-            arg1' <- fromExpression arg1-            arg2' <- fromExpression arg2-            pure $ ctor arg1' arg2'-          _ -> Left $ FromExpressionError expr msg--      removeAnns :: Expression -> (Annotation -> Bool) -> Expression-      removeAnns expr p =-        expr & _ExpressionPrim . mpaAnnotsL %~ filter (not . p)--instance FromExpression Ty where-  fromExpression e = case e of-    PrimExpr primName args anns -> do-      let annSet = toAnnSet anns-      let ta = firstAnn @TypeTag annSet-      when (secondAnn @TypeTag annSet /= noAnn) $-        Left $ FromExpressionError e-          "Expected expression with at most 1 type annotation"-      t <- fromExpression @Untyped.T $ PrimExpr primName args $ filter-        (not . isAnnotationType) anns-      pure $ Ty t ta-    _ -> Left $ FromExpressionError e "Expected a type"--instance FromExpression T where-  fromExpression =-    second fromUType . fromExpression @Untyped.Ty---- Note: we should generalize this to work for any instruction,--- not just lambdas (i.e. instructions with one input and one output).-instance (SingI inp, SingI out) => FromExpression (Instr '[inp] '[out]) where-  fromExpression expr =-    fromExpression @(Value ('TLambda inp out)) expr <&> \case-      VLam instr -> rfAnyInstr instr--instance FromExpression ViewName where-  fromExpression e = case e of-    ExpressionString s ->-      first (FromExpressionError e . pretty) $ mkViewName s-    _ -> Left $ FromExpressionError e "Expected view name"--------------------------------------------------------------------------------- Helpers--------------------------------------------------------------------------------- | Converts a sequence of expression to the right combed pair.-seqToPairExpr :: NonEmpty Expression -> Text -> Expression-seqToPairExpr e name = foldr1 (\x xs -> PrimExpr name [x, xs] []) e---- | Adds annotations to the expression, after removing empty annotations--- at the end of each list.-addTrimmedAnns-  :: Expression-  -> [TypeAnn]-  -> [FieldAnn]-  -> [VarAnn]-  -> Expression-addTrimmedAnns e tas fas vas =-  e & _ExpressionPrim . mpaAnnotsL <>~ mkAnns tas fas vas---- | Inserts the root annotation into the contract parameter.-insertRootAnn :: HasCallStack => Expression -> RootAnn -> Expression-insertRootAnn expr rootAnn = case expr of-  ExpressionPrim p-    -- The order of annotations is important iff there are-    -- multiple annotations of the same kind or there are-    -- other kinds of annotations in the list.-    -- Prepending root field annotation is okay because-    -- there can not be more than one root annotation.-    | rootAnn /= noAnn -> ExpressionPrim p-      { mpaAnnots = AnnotationField rootAnn : mpaAnnots p-      }-    | otherwise -> expr-  -- Currently this error can't happen because parameter type-  -- must be a Micheline primitive. If it ever changes, we-  -- would like to notice it ASAP and update this place.-  _ -> error $ "parameter is not a primitive: " <> pretty expr---- | Checks for a given expression that the number of annotations--- of each type in it doesn't exceed the specified threshold.-checkAnnsCount-  :: Expression-  -> AnnotationSet-  -> (Int, Int, Int)-  -> Either FromExpressionError ()-checkAnnsCount e annSet maxCount@(maxTas, maxFas, maxVas) =-  let actualCount@(tasCnt, fasCnt, vasCnt) = annsCount annSet-  in unless (actualCount <= maxCount) $-    Left $ FromExpressionError e $ pretty $ unlinesF-      [ "Expected at most"-      , indentF 2 $ build maxTas <> " type annotations,"-      , indentF 2 $ build maxFas <> " field annotations,"-      , indentF 2 $ build maxVas <> " variable annotations"-      , "but found:"-      , indentF 2 $ build tasCnt <> " type annotations,"-      , indentF 2 $ build fasCnt <> " field annotations,"-      , indentF 2 $ build vasCnt <> " variable annotations."-      ]--forbidSingletonList :: NonEmpty a -> Maybe (NonEmpty a)-forbidSingletonList = \case-  _ :| [] -> Nothing-  x       -> Just x--wordToExpr :: Word -> Expression-wordToExpr = toExpression @(Value 'TInt) . VInt . fromIntegral @Word @Integer--intExprToWord :: Expression -> Either FromExpressionError Word-intExprToWord n = do-  v <- fromExpression @(Value 'TInt) n-  case v of-    VInt n' -> maybeToRight (FromExpressionError n "Value is out of bounds")-      (toIntegralSized @Integer @Word n')--naturalToExpr :: Natural -> Expression-naturalToExpr = toExpression @(Value 'TNat) . VNat--natExprToNatural :: Expression -> Either FromExpressionError Natural-natExprToNatural n = do-  v <- fromExpression @(Value 'TNat) n-  case v of-    VNat n' -> Right n'+  , FromExpError (..)+  , FromExpressionError+  , FromExp (..)+  , FromExpression+  , fromExpression+  ) where++import Control.Lens ((<>~))+import Data.Bits (Bits)+import Data.Default (def)+import Data.Singletons (SingI(..), demote)+import Fmt (Buildable(..), indentF, pretty, unlinesF)++import Morley.Micheline.Expression+import Morley.Michelson.Text (mkMText, unMText)+import Morley.Michelson.TypeCheck+  (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith)+import Morley.Michelson.TypeCheck.Instr (typeCheckValue)+import Morley.Michelson.Typed+  (Contract, HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType, rfAnyInstr,+  toUType)+import Morley.Michelson.Typed.Convert (convertContract, instrToOpsOptimized, untypeValueOptimized)+import Morley.Michelson.Untyped qualified as Untyped+import Morley.Michelson.Untyped.Annotation+  (AnnotationSet(..), FieldAnn, FieldTag, RootAnn, TypeAnn, TypeTag, VarAnn, VarTag, annsCount,+  emptyAnnSet, firstAnn, noAnn, secondAnn)+import Morley.Michelson.Untyped.Contract (ContractBlock(..), orderContractBlock)+import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..))+import Morley.Michelson.Untyped.Type (Ty(..))+import Morley.Michelson.Untyped.View++-- ToExpression+----------------------------------------------------------------------------++-- | Type class that provides an ability to convert+-- something to Micheline Expression.+class ToExpression a where+  toExpression :: a -> Expression++instance (HasNoOp t) => ToExpression (Value t) where+  toExpression = toExpression . untypeValueOptimized++instance ToExpression Untyped.Value where+  toExpression = \case+    Untyped.ValueInt v -> expressionInt v+    Untyped.ValueString s -> expressionString $ unMText s+    Untyped.ValueBytes (Untyped.InternalByteString bs) -> expressionBytes bs+    Untyped.ValueUnit -> expressionPrim' "Unit" [] []+    Untyped.ValueTrue -> expressionPrim' "True" [] []+    Untyped.ValueFalse -> expressionPrim' "False" [] []+    Untyped.ValuePair l r ->+      expressionPrim' "Pair" [toExpression l, toExpression r] []+    Untyped.ValueLeft v -> expressionPrim' "Left" [toExpression v] []+    Untyped.ValueRight v -> expressionPrim' "Right" [toExpression v] []+    Untyped.ValueSome v -> expressionPrim' "Some" [toExpression v] []+    Untyped.ValueNone -> expressionPrim' "None" [] []+    Untyped.ValueNil -> expressionSeq []+    Untyped.ValueSeq vs -> toExpression vs+    Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts+    Untyped.ValueLambda ops -> toExpression ops+    where+      eltToExpr :: Untyped.Elt ExpandedOp -> Expression+      eltToExpr (Untyped.Elt l r) = expressionPrim' "Elt"+        [toExpression l, toExpression r] []+++instance ToExpression (Instr inp out) where+  toExpression = toExpression . instrToOpsOptimized++instance ToExpression T where+  toExpression = toExpression . toUType++instance ToExpression (Notes t) where+  toExpression = toExpression . mkUType++instance ToExpression Untyped.T where+  toExpression = \case+    Untyped.TKey -> expressionPrim' "key" [] []+    Untyped.TUnit -> expressionPrim' "unit" [] []+    Untyped.TSignature -> expressionPrim' "signature" [] []+    Untyped.TChainId -> expressionPrim' "chain_id" [] []+    Untyped.TOption arg -> expressionPrim' "option" [toExpression arg] []+    Untyped.TList arg -> expressionPrim' "list" [toExpression arg] []+    Untyped.TSet arg -> expressionPrim' "set" [toExpression arg] []+    Untyped.TOperation -> expressionPrim' "operation" [] []+    Untyped.TContract arg -> expressionPrim' "contract" [toExpression arg] []+    Untyped.TTicket arg -> expressionPrim' "ticket" [toExpression arg] []+    t@Untyped.TPair{} -> expressionPrim' "pair"+      (rightCombedPairToList (Ty t noAnn) (noAnn, noAnn)) []+    Untyped.TOr fa1 fa2 l r ->+      let exprL = addTrimmedAnns (toExpression l) [] [fa1] []+          exprR = addTrimmedAnns (toExpression r) [] [fa2] []+      in expressionPrim' "or" [exprL, exprR] []+    Untyped.TLambda inp out ->+      expressionPrim' "lambda" [toExpression inp, toExpression out] []+    Untyped.TMap k v ->+      expressionPrim' "map" [toExpression k, toExpression v] []+    Untyped.TBigMap k v ->+      expressionPrim' "big_map" [toExpression k, toExpression v] []+    Untyped.TInt -> expressionPrim' "int" [] []+    Untyped.TNat -> expressionPrim' "nat" [] []+    Untyped.TString -> expressionPrim' "string" [] []+    Untyped.TBytes -> expressionPrim' "bytes" [] []+    Untyped.TMutez -> expressionPrim' "mutez" [] []+    Untyped.TBool -> expressionPrim' "bool" [] []+    Untyped.TKeyHash -> expressionPrim' "key_hash" [] []+    Untyped.TBls12381Fr -> expressionPrim' "bls12_381_fr" [] []+    Untyped.TBls12381G1 -> expressionPrim' "bls12_381_g1" [] []+    Untyped.TBls12381G2 -> expressionPrim' "bls12_381_g2" [] []+    Untyped.TTimestamp -> expressionPrim' "timestamp" [] []+    Untyped.TAddress -> expressionPrim' "address" [] []+    Untyped.TChest -> expressionPrim' "chest" [] []+    Untyped.TChestKey -> expressionPrim' "chest_key" [] []+    Untyped.TTxRollupL2Address -> expressionPrim' "tx_rollup_l2_address" [] []+    Untyped.TNever -> expressionPrim' "never" [] []+    Untyped.TSaplingState n -> expressionPrim' "sapling_state" [integralToExpr n] []+    Untyped.TSaplingTransaction n -> expressionPrim' "sapling_transaction" [integralToExpr n] []++    where+      addAnns :: Expression -> [Annotation] -> Expression+      addAnns e anns =+        e & _ExpressionPrim . mpaAnnotsL <>~ anns++      rightCombedPairToList :: Ty -> (FieldAnn, VarAnn) -> [Expression]+      rightCombedPairToList ty (fa, va) = case (ty, fa) of+        (Ty (Untyped.TPair fa1 fa2 va1 va2 l r) (Untyped.Annotation ""), Untyped.Annotation "") ->+          let annsL = mkAnns [] [fa1] [va1]+              exprL = toExpression l `addAnns` annsL+          in exprL : (rightCombedPairToList r (fa2, va2))+        _ ->+          let anns = mkAnns [] [fa] [va]+          in one $ toExpression ty `addAnns` anns++instance ToExpression Ty where+  toExpression (Ty t ta) = addTrimmedAnns (toExpression t) [ta] [] []++instance (ToExpression a) => ToExpression [a] where+  toExpression xs = expressionSeq $ toExpression <$> xs++instance (ToExpression a) => ToExpression (NonEmpty a) where+  toExpression = toExpression . toList++instance ToExpression Expression where+  toExpression = id++instance ToExpression ExpandedOp where+  toExpression = \case+    PrimEx instr   -> toExpression instr+    SeqEx s        -> expressionSeq $ toExpression <$> s+    WithSrcEx _ op -> toExpression op++instance ToExpression ViewName where+  toExpression (ViewName s) = expressionString s++instance ToExpression ExpandedInstr where+  toExpression = \case+    PUSH va ty v -> expressionPrim' "PUSH" [toExpression ty, toExpression v] $+      mkAnns [] [] [va]+    DROP -> expressionPrim' "DROP" [] []+    DROPN n -> expressionPrim' "DROP" [integralToExpr n] []+    DUP va -> expressionPrim' "DUP" [] $ mkAnns [] [] [va]+    DUPN va n -> expressionPrim' "DUP" [integralToExpr n] $ mkAnns [] [] [va]+    SWAP -> expressionPrim' "SWAP" [] []+    DIG n -> expressionPrim' "DIG" [integralToExpr n] []+    DUG n -> expressionPrim' "DUG" [integralToExpr n] []+    SOME ta va ->+      expressionPrim' "SOME" [] $ mkAnns [ta] [] [va]+    NONE ta va ty -> expressionPrim' "NONE" [toExpression ty] $ mkAnns [ta] [] [va]+    UNIT ta va -> expressionPrim' "UNIT" [] $ mkAnns [ta] [] [va]+    IF_NONE ops1 ops2 ->+      expressionPrim' "IF_NONE" [toExpression ops1, toExpression ops2] []+    PAIR ta va fa1 fa2 -> expressionPrim' "PAIR" [] $ mkAnns [ta] [fa1, fa2] [va]+    UNPAIR va1 va2 fa1 fa2 -> expressionPrim' "UNPAIR" [] $+      mkAnns [] [fa1, fa2] [va1, va2]+    PAIRN va n -> expressionPrim' "PAIR" [integralToExpr n] $ mkAnns [] [] [va]+    UNPAIRN n -> expressionPrim' "UNPAIR" [integralToExpr n] []+    CAR va fa -> expressionPrim' "CAR" [] $ mkAnns [] [fa] [va]+    CDR va fa -> expressionPrim' "CDR" [] $ mkAnns [] [fa] [va]+    LEFT ta va fa1 fa2 ty -> expressionPrim' "LEFT" [toExpression ty] $+      mkAnns [ta] [fa1, fa2] [va]+    RIGHT ta va fa1 fa2 ty -> expressionPrim' "RIGHT" [toExpression ty] $+      mkAnns [ta] [fa1, fa2] [va]+    IF_LEFT ops1 ops2 ->+      expressionPrim' "IF_LEFT" [toExpression ops1, toExpression ops2] []+    NIL ta va ty -> expressionPrim' "NIL" [toExpression ty] $+      mkAnns [ta] [] [va]+    CONS va -> expressionPrim' "CONS" [] $ mkAnns [] [] [va]+    IF_CONS ops1 ops2 ->+      expressionPrim' "IF_CONS" [toExpression ops1, toExpression ops2] []+    SIZE va -> expressionPrim' "SIZE" [] $ mkAnns [] [] [va]+    EMPTY_SET ta va ty -> expressionPrim' "EMPTY_SET" [toExpression ty] $+      mkAnns [ta] [] [va]+    EMPTY_MAP ta va kty vty ->+      expressionPrim' "EMPTY_MAP" [toExpression kty, toExpression vty] $+      mkAnns [ta] [] [va]+    EMPTY_BIG_MAP ta va kty vty ->+      expressionPrim' "EMPTY_BIG_MAP" [toExpression kty, toExpression vty] $+      mkAnns [ta] [] [va]+    MAP va ops -> expressionPrim' "MAP" [toExpression ops] $ mkAnns [] [] [va]+    ITER ops -> expressionPrim' "ITER" [toExpression ops] []+    MEM va -> expressionPrim' "MEM" [] $ mkAnns [] [] [va]+    GET va -> expressionPrim' "GET" [] $ mkAnns [] [] [va]+    GETN va n -> expressionPrim' "GET" [integralToExpr n] $ mkAnns [] [] [va]+    UPDATE va -> expressionPrim' "UPDATE" [] $ mkAnns [] [] [va]+    UPDATEN va n -> expressionPrim' "UPDATE" [integralToExpr n] $ mkAnns [] [] [va]+    GET_AND_UPDATE va -> expressionPrim' "GET_AND_UPDATE" [] $ mkAnns [] [] [va]+    IF ops1 ops2 ->+      expressionPrim' "IF" [toExpression ops1, toExpression ops2] []+    LOOP ops -> expressionPrim' "LOOP" [toExpression ops] []+    LOOP_LEFT ops -> expressionPrim' "LOOP_LEFT" [toExpression ops] []+    LAMBDA va tyin tyout ops ->+      expressionPrim' "LAMBDA" [ toExpression tyin+                            , toExpression tyout+                            , toExpression ops+                            ] $ mkAnns [] [] [va]+    EXEC va -> expressionPrim' "EXEC" [] $ mkAnns [] [] [va]+    APPLY va -> expressionPrim' "APPLY" [] $ mkAnns [] [] [va]+    DIP ops -> expressionPrim' "DIP" [toExpression ops] []+    DIPN n ops -> expressionPrim' "DIP" [integralToExpr n, toExpression ops] []+    FAILWITH -> expressionPrim' "FAILWITH" [] []+    CAST va ty -> expressionPrim' "CAST" [toExpression ty] $ mkAnns [] [] [va]+    RENAME va -> expressionPrim' "RENAME" [] $ mkAnns [] [] [va]+    PACK va -> expressionPrim' "PACK" [] $ mkAnns [] [] [va]+    UNPACK ta va ty -> expressionPrim' "UNPACK" [toExpression ty] $+      mkAnns [ta] [] [va]+    CONCAT va -> expressionPrim' "CONCAT" [] $ mkAnns [] [] [va]+    SLICE va -> expressionPrim' "SLICE" [] $ mkAnns [] [] [va]+    ISNAT va -> expressionPrim' "ISNAT" [] $ mkAnns [] [] [va]+    ADD va -> expressionPrim' "ADD" [] $ mkAnns [] [] [va]+    SUB va -> expressionPrim' "SUB" [] $ mkAnns [] [] [va]+    SUB_MUTEZ va -> expressionPrim' "SUB_MUTEZ" [] $ mkAnns [] [] [va]+    MUL va -> expressionPrim' "MUL" [] $ mkAnns [] [] [va]+    EDIV va -> expressionPrim' "EDIV" [] $ mkAnns [] [] [va]+    ABS va -> expressionPrim' "ABS" [] $ mkAnns [] [] [va]+    NEG va -> expressionPrim' "NEG" [] $ mkAnns [] [] [va]+    LSL va -> expressionPrim' "LSL" [] $ mkAnns [] [] [va]+    LSR va -> expressionPrim' "LSR" [] $ mkAnns [] [] [va]+    OR va -> expressionPrim' "OR" [] $ mkAnns [] [] [va]+    AND va -> expressionPrim' "AND" [] $ mkAnns [] [] [va]+    XOR va -> expressionPrim' "XOR" [] $ mkAnns [] [] [va]+    NOT va -> expressionPrim' "NOT" [] $ mkAnns [] [] [va]+    COMPARE va -> expressionPrim' "COMPARE" [] $ mkAnns [] [] [va]+    Untyped.EQ va -> expressionPrim' "EQ" [] $ mkAnns [] [] [va]+    NEQ va -> expressionPrim' "NEQ" [] $ mkAnns [] [] [va]+    Untyped.LT va -> expressionPrim' "LT" [] $ mkAnns [] [] [va]+    Untyped.GT va -> expressionPrim' "GT" [] $ mkAnns [] [] [va]+    LE va -> expressionPrim' "LE" [] $ mkAnns [] [] [va]+    GE va -> expressionPrim' "GE" [] $ mkAnns [] [] [va]+    INT va -> expressionPrim' "INT" [] $ mkAnns [] [] [va]+    VIEW va n t -> expressionPrim' "VIEW" [toExpression n, toExpression t] $+      mkAnns [] [] [va]+    SELF va fa -> expressionPrim' "SELF" [] $ mkAnns [] [fa] [va]+    CONTRACT va fa ty -> expressionPrim' "CONTRACT" [toExpression ty] $+      mkAnns [] [fa] [va]+    TRANSFER_TOKENS va -> expressionPrim' "TRANSFER_TOKENS" [] $ mkAnns [] [] [va]+    SET_DELEGATE va -> expressionPrim' "SET_DELEGATE" [] $ mkAnns [] [] [va]+    CREATE_CONTRACT va1 va2 c ->+      expressionPrim' "CREATE_CONTRACT" [toExpression c] $+      mkAnns [] [] [va1, va2]+    IMPLICIT_ACCOUNT va -> expressionPrim' "IMPLICIT_ACCOUNT" [] $+      mkAnns [] [] [va]+    NOW va -> expressionPrim' "NOW" [] $ mkAnns [] [] [va]+    AMOUNT va -> expressionPrim' "AMOUNT" [] $ mkAnns [] [] [va]+    BALANCE va -> expressionPrim' "BALANCE" [] $ mkAnns [] [] [va]+    VOTING_POWER va -> expressionPrim' "VOTING_POWER" [] $ mkAnns [] [] [va]+    TOTAL_VOTING_POWER va -> expressionPrim' "TOTAL_VOTING_POWER" [] $+      mkAnns [] [] [va]+    CHECK_SIGNATURE va -> expressionPrim' "CHECK_SIGNATURE" [] $ mkAnns [] [] [va]+    SHA256 va -> expressionPrim' "SHA256" [] $ mkAnns [] [] [va]+    SHA512 va -> expressionPrim' "SHA512" [] $ mkAnns [] [] [va]+    BLAKE2B va -> expressionPrim' "BLAKE2B" [] $ mkAnns [] [] [va]+    SHA3 va -> expressionPrim' "SHA3" [] $ mkAnns [] [] [va]+    KECCAK va -> expressionPrim' "KECCAK" [] $ mkAnns [] [] [va]+    HASH_KEY va -> expressionPrim' "HASH_KEY" [] $ mkAnns [] [] [va]+    PAIRING_CHECK va -> expressionPrim' "PAIRING_CHECK" [] $ mkAnns [] [] [va]+    SOURCE va -> expressionPrim' "SOURCE" [] $ mkAnns [] [] [va]+    SENDER va -> expressionPrim' "SENDER" [] $ mkAnns [] [] [va]+    ADDRESS va -> expressionPrim' "ADDRESS" [] $ mkAnns [] [] [va]+    CHAIN_ID va -> expressionPrim' "CHAIN_ID" [] $ mkAnns [] [] [va]+    LEVEL va -> expressionPrim' "LEVEL" [] $ mkAnns [] [] [va]+    SELF_ADDRESS va -> expressionPrim' "SELF_ADDRESS" [] $ mkAnns [] [] [va]+    TICKET va -> expressionPrim' "TICKET" [] $ mkAnns [] [] [va]+    READ_TICKET va -> expressionPrim' "READ_TICKET" [] $ mkAnns [] [] [va]+    SPLIT_TICKET va -> expressionPrim' "SPLIT_TICKET" [] $ mkAnns [] [] [va]+    JOIN_TICKETS va -> expressionPrim' "JOIN_TICKETS" [] $ mkAnns [] [] [va]+    OPEN_CHEST va -> expressionPrim' "OPEN_CHEST" [] $ mkAnns [] [] [va]+    NEVER -> expressionPrim' "NEVER" [] []+    EXT _ -> expressionSeq []+    SAPLING_EMPTY_STATE va n -> expressionPrim' "SAPLING_EMPTY_STATE" [integralToExpr n] $ mkAnns [] [] [va]+    SAPLING_VERIFY_UPDATE va -> expressionPrim' "SAPLING_VERIFY_UPDATE" [] $ mkAnns [] [] [va]+    MIN_BLOCK_TIME va -> expressionPrim' "MIN_BLOCK_TIME" [] $ mkAnnsFromAny va++instance ToExpression Untyped.Contract where+  toExpression contract+    = expressionSeq $ Untyped.mapEntriesOrdered contract+          (\(Untyped.ParameterType ty rootAnn) -> expressionPrim' "parameter"+            [insertRootAnn (toExpression ty) rootAnn] [])+          (\storage -> expressionPrim' "storage" [toExpression storage] [])+          (\code -> expressionPrim' "code" [toExpression code] [])+          (\Untyped.View{..} -> expressionPrim' "view"+            [toExpression viewName, toExpression viewArgument, toExpression viewReturn, toExpression viewCode] []+          )++instance ToExpression (Contract cp st) where+  toExpression = toExpression . convertContract++-- FromExpression+----------------------------------------------------------------------------++-- | Errors that can happen when we convert an 'Exp' to our+-- data type.+data FromExpError x = FromExpError (Exp x) Text++deriving stock instance Show (Exp x) => Show (FromExpError x)+deriving stock instance Eq (Exp x) => Eq (FromExpError x)++-- | Error in case of vanilla expression.+type FromExpressionError = FromExpError RegularExp++instance Buildable FromExpressionError where+  build (FromExpError expr err) =+    unlinesF+      [ "Failed to convert expression:"+      , indentF 2 $ build expr+      , ""+      , "Error:"+      , indentF 2 $ build err+      ]++instance Exception FromExpressionError where+  displayException = pretty++-- | Type class that provides the ability to convert+-- something from a Micheline Expression.+class FromExp x a where+  fromExp :: Exp x -> Either (FromExpError x) a++type FromExpression = FromExp RegularExp++-- | Parse vanilla expression to something.+fromExpression+  :: FromExp RegularExp a+  => Expression -> Either FromExpressionError a+fromExpression = fromExp++instance (FromExp x Untyped.Value, SingI t) => FromExp x (Value t) where+  fromExp expr =+    case fromExp @_ @Untyped.Value expr of+    Right uv -> case typeCheck uv of+      Left tcErr -> Left $ FromExpError expr $+        pretty $ unlinesF+          [ "Failed to typecheck expression as a value of type:"+          , indentF 2 $ build $ demote @t+          , ""+          , "Typechecker error:"+          , indentF 2 $ build tcErr+          ]+      Right tv -> Right tv+    Left e -> Left e+    where+      typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $+        (runTypeCheck $ TypeCheckValue (uv, demote @t)) $+        usingReaderT def $+        typeCheckValue uv++instance FromExp x op => FromExp x (Untyped.Value' op) where+  fromExp e = case e of+    ExpInt _ v -> pure $ Untyped.ValueInt v+    ExpString _ s -> first (FromExpError e)+      (Untyped.ValueString <$> mkMText s)+    ExpBytes _ bs -> pure $ Untyped.ValueBytes $ Untyped.InternalByteString bs+    ExpPrim' _ "Unit" [] [] -> pure Untyped.ValueUnit+    ExpPrim' _ "True" [] [] -> pure Untyped.ValueTrue+    ExpPrim' _ "False" [] [] -> pure Untyped.ValueFalse+    ExpPrim' _ "Pair" args [] ->+      case nonEmpty args >>= forbidSingletonList of+        Nothing -> Left $ FromExpError e+          "Expected a pair with at least 2 arguments"+        Just args' -> do+          tys <- mapM fromExp args'+          return $ foldr1 Untyped.ValuePair tys+    ExpPrim' _ "Left" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.ValueLeft arg'+    ExpPrim' _ "Right" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.ValueRight arg'+    ExpPrim' _ "Some" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.ValueSome arg'+    ExpPrim' _ "None" [] [] -> pure Untyped.ValueNone+    ExpSeq _ [] -> pure Untyped.ValueNil+    ExpSeq _ (h : t) ->+      case fromExp @x @op h of+      Right op -> do+        ops <- traverse (fromExp @x @op) t+        pure . Untyped.ValueLambda $ op :| ops+      Left _ -> case exprToElt h of+        Right elt -> do+          elts <- traverse exprToElt t+          pure . Untyped.ValueMap $ elt :| elts+        Left _ -> case fromExp h of+          Left (FromExpError err _) -> Left $ FromExpError err+            "Value, instruction or 'Elt' expression expected"+          Right h' -> do+            t' <- traverse fromExp t+            pure . Untyped.ValueSeq $ h' :| t'+    _ -> Left $ FromExpError e "Expected a value"+    where+      exprToElt :: Exp x -> Either (FromExpError x) (Untyped.Elt op)+      exprToElt ex = case ex of+        ExpPrim' _ "Elt" [l, r] [] -> do+          l' <- fromExp l+          r' <- fromExp r+          pure $ Untyped.Elt l' r'+        ExpPrim' _ "Elt" _ [] -> Left $ FromExpError ex+          "Expected 'Elt' expression with exactly 2 elements"+        ExpPrim' _ "Elt" _ _ -> Left $ FromExpError ex+          "Expected 'Elt' expression without annotations"+        _ -> Left $ FromExpError ex "Expected 'Elt' expression"++instance FromExp x a => FromExp x [a] where+  fromExp = \case+    ExpSeq _ exprs -> traverse fromExp exprs+    e -> Left $ FromExpError e "'ExpressionSeq' expected"++instance FromExp RegularExp ExpandedOp where+  fromExp = \case+    ExpSeq _ s -> SeqEx <$> traverse fromExp s+    e          -> PrimEx <$> fromExp e++instance FromExp x op =>+         FromExp x (InstrAbstract op) where+  fromExp e = let annSet = getAnnSet e in case e of+    ExpPrim' _ "DROP" [n] [] -> do+      n' <- integralFromExpr n+      pure $ DROPN n'+    ExpPrim' _ "DROP" [] _ -> pure $ DROP+    ExpPrim' _ "DUP" [n] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      let va = firstAnn @VarTag annSet+      n' <- integralFromExpr n+      pure $ DUPN va n'+    ExpPrim' _ "DUP" [] _ ->+      let va = firstAnn @VarTag annSet+      in checkAnnsCount e annSet (0, 0, 1) $> DUP va+    ExpPrim' _ "SWAP" [] [] -> pure $ SWAP+    ExpPrim' _ "DIG" [n] [] -> do+      n' <- integralFromExpr n+      pure $ DIG $ n'+    ExpPrim' _ "DUG" [n] [] -> do+      n' <- integralFromExpr n+      pure $ DUG n'+    ExpPrim' _ "PUSH" [t, v] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      let va = firstAnn @VarTag annSet+      t' <- fromExp @x @Ty t+      v' <- fromExp @x @(Untyped.Value' op) v+      pure $ PUSH va t' v'+    ExpPrim' _ "SOME" [] _ ->+      let ta = firstAnn @TypeTag annSet+          va = firstAnn @VarTag annSet+      in checkAnnsCount e annSet (1, 0, 1) $> SOME ta va+    ExpPrim' _ "NONE" [t] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      let ta = firstAnn @TypeTag annSet+      let va = firstAnn @VarTag annSet+      t' <- fromExp @x @Ty t+      pure $ NONE ta va t'+    ExpPrim' _ "UNIT" [] _ ->+      let ta = firstAnn @TypeTag annSet+          va = firstAnn @VarTag annSet+      in checkAnnsCount e annSet (1, 0, 1) $> UNIT ta va+    ExpPrim' _ "IF_NONE" [ops1, ops2] [] -> do+      ops1' <- fromExp @x @[op] ops1+      ops2' <- fromExp @x @[op] ops2+      pure $ IF_NONE ops1' ops2'+    ExpPrim' _ "PAIR" [] _ ->+      let ta = firstAnn @TypeTag annSet+          va = firstAnn @VarTag annSet+          fa1 = firstAnn @FieldTag annSet+          fa2 = secondAnn @FieldTag annSet+      in (checkAnnsCount e annSet (1, 2, 1)) $> PAIR ta va fa1 fa2+    ExpPrim' _ "UNPAIR" [] _ ->+      let va1 = firstAnn @VarTag annSet+          va2 = secondAnn @VarTag annSet+          fa1 = firstAnn @FieldTag annSet+          fa2 = secondAnn @FieldTag annSet+      in checkAnnsCount e annSet (0, 2, 2) $> UNPAIR va1 va2 fa1 fa2+    ExpPrim' _ "PAIR" [n] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      n' <- integralFromExpr n+      let va = firstAnn @VarTag annSet+      pure $ PAIRN va n'+    ExpPrim' _ "UNPAIR" [n] [] -> do+      n' <- integralFromExpr n+      pure $ UNPAIRN n'+    ExpPrim' _ "CAR" [] _ ->+      let va = firstAnn @VarTag annSet+          fa = firstAnn @FieldTag annSet+      in checkAnnsCount e annSet (0, 1, 1) $> CAR va fa+    ExpPrim' _ "CDR" [] _ ->+      let va = firstAnn @VarTag annSet+          fa = firstAnn @FieldTag annSet+      in checkAnnsCount e annSet (0, 1, 1) $> CDR va fa+    ExpPrim' _ "LEFT" [t] _ -> do+      checkAnnsCount e annSet (1, 2, 1)+      t' <- fromExp @x @Ty t+      let ta = firstAnn @TypeTag annSet+      let va = firstAnn @VarTag annSet+      let fa1 = firstAnn @FieldTag annSet+      let fa2 = secondAnn @FieldTag annSet+      pure $ LEFT ta va fa1 fa2 t'+    ExpPrim' _ "RIGHT" [t] _ -> do+      checkAnnsCount e annSet (1, 2, 1)+      t' <- fromExp @x @Ty t+      let ta = firstAnn @TypeTag annSet+      let va = firstAnn @VarTag annSet+      let fa1 = firstAnn @FieldTag annSet+      let fa2 = secondAnn @FieldTag annSet+      pure $ RIGHT ta va fa1 fa2 t'+    ExpPrim' _ "IF_LEFT" [ops1, ops2] [] -> do+      ops1' <- fromExp @x @[op] ops1+      ops2' <- fromExp @x @[op] ops2+      pure $ IF_LEFT ops1' ops2'+    ExpPrim' _ "NIL" [t] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      t' <- fromExp @x @Ty t+      let va = firstAnn @VarTag annSet+      let ta = firstAnn @TypeTag annSet+      pure $ NIL ta va t'+    ExpPrim' _ "CONS" [] anns -> mkInstrWithVarAnn CONS anns+    ExpPrim' _ "IF_CONS" [ops1, ops2] [] -> do+      ops1' <- fromExp @x @[op] ops1+      ops2' <- fromExp @x @[op] ops2+      pure $ IF_CONS ops1' ops2'+    ExpPrim' _ "SIZE" [] anns -> mkInstrWithVarAnn SIZE anns+    ExpPrim' _ "EMPTY_SET" [t] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      t' <- fromExp @x @Ty t+      let va = firstAnn @VarTag annSet+      let ta = firstAnn @TypeTag annSet+      pure $ EMPTY_SET ta va t'+    ExpPrim' _ "EMPTY_MAP" [kt, vt] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      kt' <- fromExp @x @Ty kt+      vt' <- fromExp @x @Ty vt+      let va = firstAnn @VarTag annSet+      let ta = firstAnn @TypeTag annSet+      pure $ EMPTY_MAP ta va kt' vt'+    ExpPrim' _ "EMPTY_BIG_MAP" [kt, vt] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      kt' <- fromExp @x @Ty kt+      vt' <- fromExp @x @Ty vt+      let va = firstAnn @VarTag annSet+      let ta = firstAnn @TypeTag annSet+      pure $ EMPTY_BIG_MAP ta va kt' vt'+    ExpPrim' _ "MAP" [ops] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      ops' <- fromExp @x @[op] ops+      let va = firstAnn @VarTag annSet+      pure $ MAP va ops'+    ExpPrim' _ "ITER" [ops] [] -> do+      ops' <- fromExp @x @[op] ops+      pure $ ITER ops'+    ExpPrim' _ "MEM" [] anns -> mkInstrWithVarAnn MEM anns+    ExpPrim' _ "GET" [] anns -> mkInstrWithVarAnn GET anns+    ExpPrim' _ "GET" [n] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      n' <- integralFromExpr n+      let va = firstAnn @VarTag annSet+      pure $ GETN va n'+    ExpPrim' _ "UPDATE" [] anns -> mkInstrWithVarAnn UPDATE anns+    ExpPrim' _ "UPDATE" [n] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      n' <- integralFromExpr n+      let va = firstAnn @VarTag annSet+      pure $ UPDATEN va n'+    ExpPrim' _ "GET_AND_UPDATE" [] anns ->+      mkInstrWithVarAnn GET_AND_UPDATE anns+    ExpPrim' _ "IF" [ops1, ops2] [] -> do+      ops1' <- fromExp @x @[op] ops1+      ops2' <- fromExp @x @[op] ops2+      pure $ IF ops1' ops2'+    ExpPrim' _ "LOOP" [ops] [] -> do+      ops' <- fromExp @x @[op] ops+      pure $ LOOP ops'+    ExpPrim' _ "LOOP_LEFT" [ops] [] -> do+      ops' <- fromExp @x @[op] ops+      pure $ LOOP_LEFT ops'+    ExpPrim' _ "LAMBDA" [inp, out, ops] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      inp' <- fromExp @x @Ty inp+      out' <- fromExp @x @Ty out+      ops' <- fromExp @x @[op] ops+      let va = firstAnn @VarTag annSet+      pure $ LAMBDA va inp' out' ops'+    ExpPrim' _ "EXEC" [] anns -> mkInstrWithVarAnn EXEC anns+    ExpPrim' _ "APPLY" [] anns -> mkInstrWithVarAnn APPLY anns+    ExpPrim' _ "DIP" [ops] [] -> do+      ops' <- fromExp @x @[op] ops+      pure $ DIP ops'+    ExpPrim' _ "DIP" [n, ops] [] -> do+      n' <- integralFromExpr n+      ops' <- fromExp @x @[op] ops+      pure $ DIPN n' ops'+    ExpPrim' _ "FAILWITH" [] [] -> pure FAILWITH+    ExpPrim' _ "CAST" [t] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      t' <- fromExp @x @Ty t+      let va = firstAnn @VarTag annSet+      pure $ CAST va t'+    ExpPrim' _ "RENAME" [] anns -> mkInstrWithVarAnn RENAME anns+    ExpPrim' _ "PACK" [] anns -> mkInstrWithVarAnn PACK anns+    ExpPrim' _ "UNPACK" [t] _ -> do+      checkAnnsCount e annSet (1, 0, 1)+      t' <- fromExp @x @Ty t+      let ta = firstAnn @TypeTag annSet+      let va = firstAnn @VarTag annSet+      pure $ UNPACK ta va t'+    ExpPrim' _ "CONCAT" [] anns -> mkInstrWithVarAnn CONCAT anns+    ExpPrim' _ "SLICE" [] anns -> mkInstrWithVarAnn SLICE anns+    ExpPrim' _ "ISNAT" [] anns -> mkInstrWithVarAnn ISNAT anns+    ExpPrim' _ "ADD" [] anns -> mkInstrWithVarAnn ADD anns+    ExpPrim' _ "SUB" [] anns -> mkInstrWithVarAnn SUB anns+    ExpPrim' _ "SUB_MUTEZ" [] anns -> mkInstrWithVarAnn SUB_MUTEZ anns+    ExpPrim' _ "MUL" [] anns -> mkInstrWithVarAnn MUL anns+    ExpPrim' _ "EDIV" [] anns -> mkInstrWithVarAnn EDIV anns+    ExpPrim' _ "ABS" [] anns -> mkInstrWithVarAnn ABS anns+    ExpPrim' _ "NEG" [] anns -> mkInstrWithVarAnn NEG anns+    ExpPrim' _ "LSL" [] anns -> mkInstrWithVarAnn LSL anns+    ExpPrim' _ "LSR" [] anns -> mkInstrWithVarAnn LSR anns+    ExpPrim' _ "OR" [] anns -> mkInstrWithVarAnn OR anns+    ExpPrim' _ "AND" [] anns -> mkInstrWithVarAnn AND anns+    ExpPrim' _ "XOR" [] anns -> mkInstrWithVarAnn XOR anns+    ExpPrim' _ "NOT" [] anns -> mkInstrWithVarAnn NOT anns+    ExpPrim' _ "COMPARE" [] anns -> mkInstrWithVarAnn COMPARE anns+    ExpPrim' _ "EQ" [] anns -> mkInstrWithVarAnn Untyped.EQ anns+    ExpPrim' _ "NEQ" [] anns -> mkInstrWithVarAnn NEQ anns+    ExpPrim' _ "LT" [] anns -> mkInstrWithVarAnn Untyped.LT anns+    ExpPrim' _ "GT" [] anns -> mkInstrWithVarAnn Untyped.GT anns+    ExpPrim' _ "LE" [] anns -> mkInstrWithVarAnn LE anns+    ExpPrim' _ "GE" [] anns -> mkInstrWithVarAnn GE anns+    ExpPrim' _ "INT" [] anns -> mkInstrWithVarAnn INT anns+    ExpPrim' _ "VIEW" [name, t] _ -> do+      let va = firstAnn @VarTag annSet+      name' <- fromExp @x @ViewName name+      t' <- fromExp @x @Ty t+      checkAnnsCount e annSet (0, 0, 1) $> VIEW va name' t'+    ExpPrim' _ "SELF" [] _ ->+      let fa = firstAnn @FieldTag annSet+          va = firstAnn @VarTag annSet+      in checkAnnsCount e annSet (0, 1, 1) $> SELF va fa+    ExpPrim' _ "CONTRACT" [t] _ -> do+      checkAnnsCount e annSet (0, 1, 1)+      t' <- fromExp @x @Ty t+      let va = firstAnn @VarTag annSet+      let fa = firstAnn @FieldTag annSet+      pure $ CONTRACT va fa t'+    ExpPrim' _ "TRANSFER_TOKENS" [] anns ->+      mkInstrWithVarAnn TRANSFER_TOKENS anns+    ExpPrim' _ "SET_DELEGATE" [] anns ->+      mkInstrWithVarAnn SET_DELEGATE anns+    ExpPrim' _ "CREATE_CONTRACT" [c] _ -> do+      checkAnnsCount e annSet (0, 0, 2)+      c' <- fromExp @x @(Untyped.Contract' op) c+      let va1 = firstAnn @VarTag annSet+      let va2 = secondAnn @VarTag annSet+      pure $ CREATE_CONTRACT va1 va2 c'+    ExpPrim' _ "IMPLICIT_ACCOUNT" [] anns ->+      mkInstrWithVarAnn IMPLICIT_ACCOUNT anns+    ExpPrim' _ "NOW" [] anns -> mkInstrWithVarAnn NOW anns+    ExpPrim' _ "AMOUNT" [] anns -> mkInstrWithVarAnn AMOUNT anns+    ExpPrim' _ "BALANCE" [] anns -> mkInstrWithVarAnn BALANCE anns+    ExpPrim' _ "VOTING_POWER" [] anns ->+      mkInstrWithVarAnn VOTING_POWER anns+    ExpPrim' _ "TOTAL_VOTING_POWER" [] anns ->+      mkInstrWithVarAnn TOTAL_VOTING_POWER anns+    ExpPrim' _ "CHECK_SIGNATURE" [] anns ->+      mkInstrWithVarAnn CHECK_SIGNATURE anns+    ExpPrim' _ "SHA256" [] anns -> mkInstrWithVarAnn SHA256 anns+    ExpPrim' _ "SHA512" [] anns -> mkInstrWithVarAnn SHA512 anns+    ExpPrim' _ "BLAKE2B" [] anns -> mkInstrWithVarAnn BLAKE2B anns+    ExpPrim' _ "SHA3" [] anns -> mkInstrWithVarAnn SHA3 anns+    ExpPrim' _ "KECCAK" [] anns -> mkInstrWithVarAnn KECCAK anns+    ExpPrim' _ "HASH_KEY" [] anns -> mkInstrWithVarAnn HASH_KEY anns+    ExpPrim' _ "PAIRING_CHECK" [] anns ->+      mkInstrWithVarAnn PAIRING_CHECK anns+    ExpPrim' _ "SOURCE" [] anns -> mkInstrWithVarAnn SOURCE anns+    ExpPrim' _ "SENDER" [] anns -> mkInstrWithVarAnn SENDER anns+    ExpPrim' _ "ADDRESS" [] anns -> mkInstrWithVarAnn ADDRESS anns+    ExpPrim' _ "CHAIN_ID" [] anns -> mkInstrWithVarAnn CHAIN_ID anns+    ExpPrim' _ "LEVEL" [] anns -> mkInstrWithVarAnn LEVEL anns+    ExpPrim' _ "SELF_ADDRESS" [] anns ->+      mkInstrWithVarAnn SELF_ADDRESS anns+    ExpPrim' _ "NEVER" [] [] -> pure NEVER+    ExpPrim' _ "TICKET" [] anns -> mkInstrWithVarAnn TICKET anns+    ExpPrim' _ "READ_TICKET" [] anns ->+      mkInstrWithVarAnn READ_TICKET anns+    ExpPrim' _ "SPLIT_TICKET" [] anns ->+      mkInstrWithVarAnn SPLIT_TICKET anns+    ExpPrim' _ "JOIN_TICKETS" [] anns ->+      mkInstrWithVarAnn JOIN_TICKETS anns+    ExpPrim' _ "OPEN_CHEST" [] anns ->+      mkInstrWithVarAnn OPEN_CHEST anns+    ExpPrim' _ "SAPLING_EMPTY_STATE" [n] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      n' <- integralFromExpr n+      let va = firstAnn @VarTag annSet+      pure $ SAPLING_EMPTY_STATE va n'+    ExpPrim' _ "SAPLING_VERIFY_UPDATE" [] anns ->+      mkInstrWithVarAnn SAPLING_VERIFY_UPDATE anns+    ExpPrim' _ "MIN_BLOCK_TIME" [] anns -> pure $ mkInstrWithAnyAnns MIN_BLOCK_TIME anns+    _ -> Left $ FromExpError e "Expected an instruction"++    where+      mkInstrWithVarAnn+        :: (VarAnn -> InstrAbstract op)+        -> [Annotation]+        -> Either (FromExpError x) (InstrAbstract op)+      mkInstrWithVarAnn ctor anns =+        let annSet = toAnnSet anns+            va = firstAnn @VarTag annSet+        in checkAnnsCount e annSet (0, 0, 1) $> ctor va++      mkInstrWithAnyAnns+        :: ([Untyped.AnyAnn] -> InstrAbstract op)+        -> [Annotation]+        -> InstrAbstract op+      mkInstrWithAnyAnns ctor anns = ctor $ anns <&> \case+        AnnotationType x -> Untyped.AnyAnnType x+        AnnotationField x -> Untyped.AnyAnnField x+        AnnotationVariable x -> Untyped.AnyAnnVar x++      getAnnSet :: Exp d -> AnnotationSet+      getAnnSet = \case+        ExpPrim' _ _ _ anns -> toAnnSet anns+        _                   -> emptyAnnSet++instance (FromExp x op) => FromExp x (Untyped.Contract' op) where+  fromExp blocks = case blocks of+    ExpSeq _ bs -> do+      bs' <- mapM exprToCB bs+      maybeToRight (FromExpError blocks "Something's wrong with top-level contract blocks")+        (orderContractBlock bs')+    expr -> Left $ FromExpError expr "Failed to parse contract, expected sequence"+    where+      exprToCB+        :: Exp x+        -> Either (FromExpError x) (ContractBlock op)+      exprToCB e = case e of+        ExpPrim' _ "parameter" args anns -> mkCbParam e args anns+        ExpPrim' _ "storage"   args anns -> mkCBStorage e args anns+        ExpPrim' _ "code"      args anns -> mkCBCode e args anns+        ExpPrim' _ "view"      args anns -> mkCBView e args anns+        _                              ->+          Left $ FromExpError e "Unexpected primitive at contract top-level"++      mkCbParam+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCbParam e args anns = case (args, anns) of+        ([p], []) -> do+          let annSet = toAnnSet (p ^. _ExpPrim . _2 . mpaAnnotsL)+          let rootAnn = firstAnn @FieldTag annSet+          unless (secondAnn @FieldTag annSet == noAnn) $+            Left $ FromExpError p+              "Expected parameter with at most 1 root annotation"+          p' <- fromExp @x @Ty+            (p & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . isAnnotationField))+          pure $ CBParam $ Untyped.ParameterType p' rootAnn+        _ -> Left $ FromExpError e+          "Expected 'parameter' block without annotations and exactly 1 argument"++      mkCBStorage+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBStorage e args anns = case (args, anns) of+        ([s], []) -> do+          s' <- fromExp @x @Ty s+          pure $ CBStorage s'+        _ -> Left $ FromExpError e+               "Expected 'storage' block without annotations and exactly 1 argument"++      mkCBCode+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBCode e args anns = case (args, anns) of+        ([ops], []) -> do+          ops' <- fromExp @x @[op] ops+          pure $ CBCode ops'+        _ -> Left $ FromExpError e+               "Expected 'code' block without annotations"++      mkCBView+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBView e args anns = case (args, anns) of+        ([name, arg, ret, ops], []) -> do+          name' <- fromExp name+          arg' <- fromExp arg+          ret' <- fromExp ret+          ops' <- fromExp @x @[op] ops+          pure $ CBView $ Untyped.View name' arg' ret' ops'+        (_, _ : _) ->+          Left $ FromExpError e+               "Expected 'view' block without annotations"+        (_, []) ->+          Left $ FromExpError e+               "Invalid 'view' block, expected 4 expressions in it"++instance FromExp x Untyped.T where+  fromExp e = case e of+    ExpPrim' _ "key" [] [] -> pure Untyped.TKey+    ExpPrim' _ "unit" [] [] -> pure Untyped.TUnit+    ExpPrim' _ "signature" [] [] -> pure Untyped.TSignature+    ExpPrim' _ "chain_id" [] [] -> pure Untyped.TChainId+    ExpPrim' _ "option" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.TOption arg'+    ExpPrim' _ "list" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.TList arg'+    ExpPrim' _ "set" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.TSet arg'+    ExpPrim' _ "operation" [] [] -> pure Untyped.TOperation+    ExpPrim' _ "contract" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.TContract arg'+    ExpPrim' _ "ticket" [arg] [] -> do+      arg' <- fromExp arg+      pure $ Untyped.TTicket arg'+    ExpPrim' _ "or" [arg1, arg2] [] -> do+      let as1 = toAnnSet $ arg1 ^. _ExpPrim . _2 . mpaAnnotsL+      let as2 = toAnnSet $ arg2 ^. _ExpPrim . _2 . mpaAnnotsL+      checkAnnsCount e as1 (1, 1, 0)+      checkAnnsCount e as2 (1, 1, 0)+      let fa1 = firstAnn @FieldTag as1+      let fa2 = firstAnn @FieldTag as2+      l <- fromExp $ removeAnns arg1 isAnnotationField+      r <- fromExp $ removeAnns arg2 isAnnotationField+      pure $ Untyped.TOr fa1 fa2 l r+    ExpPrim' _ "pair" args [] -> do+      args2 <- case nonEmpty args >>= forbidSingletonList of+        Nothing -> Left $ FromExpError e+          "Expected a pair with at least 2 arguments"+        Just as -> pure as+      -- Check and extract annotations info+      tyInfos <- forM args2 \arg -> do+        let as = toAnnSet $ arg ^. _ExpPrim . _2 . mpaAnnotsL+        checkAnnsCount e as (1, 1, 1)+        let fa = firstAnn @FieldTag as+        let va = firstAnn @VarTag as+        ty <- fromExp $ removeAnns arg+          (isAnnotationField || isAnnotationVariable)+        return (ty, fa, va)+      -- Make a right-comb pairs tree+      let combiner (ty1, fa1, va1) (ty2, fa2, va2) =+            ( Ty (Untyped.TPair fa1 fa2 va1 va2 ty1 ty2) noAnn+            , noAnn+            , noAnn+            )+      let (Ty tRes _, _, _) = foldr1 combiner tyInfos+      return tRes+    ExpPrim' _ "lambda" args [] -> mkDoubleParamType Untyped.TLambda args e+      "Expected a lambda with input and output types"+    ExpPrim' _ "map" args [] -> mkDoubleParamType Untyped.TMap args e+      "Expected a map with key and value types"+    ExpPrim' _ "big_map" args [] -> mkDoubleParamType Untyped.TBigMap args e+      "Expected a big_map with key and value types"+    ExpPrim' _ "int" [] [] -> pure Untyped.TInt+    ExpPrim' _ "nat" [] [] -> pure Untyped.TNat+    ExpPrim' _ "string" [] [] -> pure Untyped.TString+    ExpPrim' _ "bytes" [] [] -> pure Untyped.TBytes+    ExpPrim' _ "mutez" [] [] -> pure Untyped.TMutez+    ExpPrim' _ "bool" [] [] -> pure Untyped.TBool+    ExpPrim' _ "key_hash" [] [] -> pure Untyped.TKeyHash+    ExpPrim' _ "bls12_381_fr" [] [] -> pure Untyped.TBls12381Fr+    ExpPrim' _ "bls12_381_g1" [] [] -> pure Untyped.TBls12381G1+    ExpPrim' _ "bls12_381_g2" [] [] -> pure Untyped.TBls12381G2+    ExpPrim' _ "timestamp" [] [] -> pure Untyped.TTimestamp+    ExpPrim' _ "address" [] [] -> pure Untyped.TAddress+    ExpPrim' _ "chest" [] [] -> pure Untyped.TChest+    ExpPrim' _ "chest_key" [] [] -> pure Untyped.TChestKey+    ExpPrim' _ "tx_rollup_l2_address" [] [] -> pure Untyped.TTxRollupL2Address+    ExpPrim' _ "never" [] [] -> pure Untyped.TNever+    ExpPrim' _ "sapling_state" [n] [] -> do+      n' <- integralFromExpr n+      pure $ Untyped.TSaplingState n'+    ExpPrim' _ "sapling_transaction" [n] [] -> do+      n' <- integralFromExpr n+      pure $ Untyped.TSaplingTransaction n'+    ExpPrim' _ "sapling_transaction_deprecated" _ _ -> do+      Left $ FromExpError e "Use of deprecated type: sapling_transaction_deprecated"+    _ -> Left $ FromExpError e "Expected a type"+    where+      mkDoubleParamType+        :: (Ty -> Ty -> Untyped.T)+        -> [Exp x]+        -> Exp x+        -> Text+        -> Either (FromExpError x) Untyped.T+      mkDoubleParamType ctor args expr msg = do+        case args of+          [arg1, arg2] -> do+            arg1' <- fromExp arg1+            arg2' <- fromExp arg2+            pure $ ctor arg1' arg2'+          _ -> Left $ FromExpError expr msg++      removeAnns :: Exp x -> (Annotation -> Bool) -> Exp x+      removeAnns expr p =+        expr & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . p)++instance FromExp x Ty where+  fromExp e = case e of+    ExpPrim' ex primName args anns -> do+      let annSet = toAnnSet anns+      let ta = firstAnn @TypeTag annSet+      when (secondAnn @TypeTag annSet /= noAnn) $+        Left $ FromExpError e+          "Expected expression with at most 1 type annotation"+      t <- fromExp @x @Untyped.T $ ExpPrim' ex primName args $ filter+        (not . isAnnotationType) anns+      pure $ Ty t ta+    _ -> Left $ FromExpError e "Expected a type"++instance FromExp x T where+  fromExp =+    second fromUType . fromExp @x @Untyped.Ty++-- Note: we should generalize this to work for any instruction,+-- not just lambdas (i.e. instructions with one input and one output).+instance (SingI inp, SingI out) => FromExp RegularExp (Instr '[inp] '[out]) where+  fromExp expr =+    fromExpression @(Value ('TLambda inp out)) expr <&> \case+      VLam instr -> rfAnyInstr instr++instance FromExp x ViewName where+  fromExp e = case e of+    ExpString _ s ->+      first (FromExpError e . pretty) $ mkViewName s+    _ -> Left $ FromExpError e "Expected view name"++----------------------------------------------------------------------------+-- Helpers+----------------------------------------------------------------------------++-- | Adds annotations to the expression, after removing empty annotations+-- at the end of each list.+addTrimmedAnns+  :: Exp x+  -> [TypeAnn]+  -> [FieldAnn]+  -> [VarAnn]+  -> Exp x+addTrimmedAnns e tas fas vas =+  e & _ExpPrim . _2 . mpaAnnotsL <>~ mkAnns tas fas vas++-- | Inserts the root annotation into the contract parameter.+insertRootAnn :: HasCallStack => Expression -> RootAnn -> Expression+insertRootAnn expr rootAnn = case expr of+  ExpPrim () p+    -- The order of annotations is important iff there are+    -- multiple annotations of the same kind or there are+    -- other kinds of annotations in the list.+    -- Prepending root field annotation is okay because+    -- there can not be more than one root annotation.+    | rootAnn /= noAnn -> expressionPrim p+      { mpaAnnots = AnnotationField rootAnn : mpaAnnots p+      }+    | otherwise -> expr+  -- Currently this error can't happen because parameter type+  -- must be a Micheline primitive. If it ever changes, we+  -- would like to notice it ASAP and update this place.+  _ -> error $ "parameter is not a primitive: " <> pretty expr++-- | Checks for a given expression that the number of annotations+-- of each type in it doesn't exceed the specified threshold.+checkAnnsCount+  :: Exp x+  -> AnnotationSet+  -> (Int, Int, Int)+  -> Either (FromExpError x) ()+checkAnnsCount e annSet maxCount@(maxTas, maxFas, maxVas) =+  let actualCount@(tasCnt, fasCnt, vasCnt) = annsCount annSet+  in unless (actualCount <= maxCount) $+    Left $ FromExpError e $ pretty $ unlinesF+      [ "Expected at most"+      , indentF 2 $ build maxTas <> " type annotations,"+      , indentF 2 $ build maxFas <> " field annotations,"+      , indentF 2 $ build maxVas <> " variable annotations"+      , "but found:"+      , indentF 2 $ build tasCnt <> " type annotations,"+      , indentF 2 $ build fasCnt <> " field annotations,"+      , indentF 2 $ build vasCnt <> " variable annotations."+      ]++forbidSingletonList :: NonEmpty a -> Maybe (NonEmpty a)+forbidSingletonList = \case+  _ :| [] -> Nothing+  x       -> Just x++integralToExpr :: Integral i => i -> Expression+integralToExpr = expressionInt . toInteger++integralFromExpr :: (Integral i, Bits i) => Exp x -> Either (FromExpError x) i+integralFromExpr e = case e of+  ExpInt _ v ->+    maybeToRight (FromExpError e "Value is out of bounds")+      (fromIntegralMaybe @Integer v)+  _ -> Left $ FromExpError e "Expected a number here"

@@ -8,11 +8,30 @@ -- | Module that defines Expression type, its related types -- and its JSON instance. module Morley.Micheline.Expression-  ( Expression(.., PrimExpr)+  ( Exp+    ( ..+    , ExpPrim'+    )+  , expressionInt+  , expressionString+  , expressionBytes+  , expressionSeq+  , expressionPrim+  , expressionPrim'+  , RegularExp+  , Expression   , MichelinePrimAp(..)   , MichelinePrimitive(..)   , michelsonPrimitive+  , ExpExtensionDescriptorKind+  , ExpExtensionDescriptor (..) +  , ExpExtrasConstrained+  , ExpAllExtrasConstrainted+  , ExpExtras (..)+  , mkUniformExpExtras+  , hoistExpExtras+   , Annotation (..)   , annotToText   , annotFromText@@ -22,8 +41,14 @@   , isNoAnn   , mkAnns   , toAnnSet+  , mkAnnsFromAny    -- * Prisms+  , _ExpInt+  , _ExpString+  , _ExpBytes+  , _ExpSeq+  , _ExpPrim   , _ExpressionInt   , _ExpressionString   , _ExpressionBytes@@ -39,16 +64,16 @@   , mpaAnnotsL   ) where -import Control.Lens (Plated)+import Control.Lens (Iso', Plated, Prism', iso, prism') import Control.Lens.TH (makeLensesWith, makePrisms)  import Data.Aeson   (FromJSON, ToJSON, object, parseJSON, toEncoding, toJSON, withObject, withText, (.!=), (.:),   (.:?), (.=)) import Data.Aeson.Encoding.Internal qualified as Aeson+import Data.Aeson.KeyMap qualified as KeyMap import Data.Aeson.Types qualified as Aeson import Data.Data (Data)-import Data.HashMap.Strict qualified as HashMap import Data.Sequence qualified as Seq import Data.Text qualified as T (uncons) import Fmt (Buildable(..), pretty, (+|), (|+))@@ -64,7 +89,7 @@ import Morley.Util.Lens (postfixLFields)  newtype MichelinePrimitive = MichelinePrimitive Text-  deriving newtype (Eq, Ord, ToJSON, FromJSON)+  deriving newtype (Eq, Ord, IsString, ToJSON, FromJSON)   deriving stock (Show, Data, Lift)  michelsonPrimitive :: Seq Text@@ -105,39 +130,161 @@   "string", "bytes", "mutez", "timestamp", "unit", "operation", "address", "SLICE",   "DIG", "DUG", "EMPTY_BIG_MAP", "APPLY", "chain_id", "CHAIN_ID", "LEVEL", "SELF_ADDRESS",   "never", "NEVER", "UNPAIR", "VOTING_POWER", "TOTAL_VOTING_POWER", "KECCAK", "SHA3", "PAIRING_CHECK",-  "bls12_381_g1", "bls12_381_g2", "bls12_381_fr", "sapling_state", "sapling_transaction", "SAPLING_EMPTY_STATE", "SAPLING_VERIFY_UPDATE", "ticket",+  "bls12_381_g1", "bls12_381_g2", "bls12_381_fr", "sapling_state", "sapling_transaction_deprecated", "SAPLING_EMPTY_STATE", "SAPLING_VERIFY_UPDATE", "ticket",   "TICKET", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE", "chest", "chest_key", "OPEN_CHEST",-  "VIEW", "view", "constant", "SUB_MUTEZ"+  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction"   ] --- | Type for Micheline Expression-data Expression-  = ExpressionInt Integer-    -- ^ Micheline represents both nats and ints using the same decimal format.-    -- The Haskell Integer type spans all possible values that the final-    -- (Michelson) type could end up being, and then some, so we use-    -- (StringEncode Integer) to represent all integral values here for easy-    -- JSON encoding compatibility.-  | ExpressionString Text-  | ExpressionBytes ByteString-  | ExpressionSeq [Expression]-  | ExpressionPrim MichelinePrimAp-  deriving stock (Eq, Show, Data, Lift)+-- | Type for Micheline Expression with extension points.+--+-- Following the Trees-that-Grow approach, this type provides the core set+-- of constructors used by Tezos accompanied with additional data (@XExp*@).+-- Plus additional constructors provided by @XExp@.+--+-- The type argument @x@ will be called /extension descriptor/ and it must have+-- @ExpExtensionDescriptor@ instance.+data Exp x+  = ExpInt (XExpInt x) Integer+  | ExpString (XExpString x) Text+  | ExpBytes (XExpBytes x) ByteString+  | ExpSeq (XExpSeq x) [Exp x]+  | ExpPrim (XExpPrim x) (MichelinePrimAp x)+  | ExpX (XExp x) -pattern PrimExpr :: Text -> [Expression] -> [Annotation] -> Expression-pattern PrimExpr primName args anns =-  ExpressionPrim (MichelinePrimAp (MichelinePrimitive primName) args anns)+pattern ExpPrim' :: XExpPrim x -> MichelinePrimitive -> [Exp x] -> [Annotation] -> Exp x+pattern ExpPrim' x primAp exprs anns = ExpPrim x (MichelinePrimAp primAp exprs anns) -instance Plated Expression+deriving stock instance ExpAllExtrasConstrainted Eq x => Eq (Exp x)+deriving stock instance ExpAllExtrasConstrainted Show x => Show (Exp x)+deriving stock instance (ExpAllExtrasConstrainted Data x, Typeable x) => Data (Exp x)+deriving stock instance ExpAllExtrasConstrainted Lift x => Lift (Exp x) +-- | Kind of extension descriptors.+--+-- We use a dedicated open type for this, not just @Type@, to notice earlier+-- when type arguments are mis-placed.+type ExpExtensionDescriptorKind = ExpExtensionTag -> Type+data ExpExtensionTag++-- | Defines details of extension descriptor.+class ExpExtensionDescriptor (x :: ExpExtensionDescriptorKind) where++  -- | Additional data in 'ExpInt' constructor.+  type XExpInt x :: Type+  type XExpInt _ = ()++  -- | Additional data in 'ExpString' constructor.+  type XExpString x :: Type+  type XExpString _ = ()++  -- | Additional data in 'ExpBytes' constructor.+  type XExpBytes x :: Type+  type XExpBytes _ = ()++  -- | Additional data in 'ExpSeq' constructor.+  type XExpSeq x :: Type+  type XExpSeq _ = ()++  -- | Additional data in 'ExpPrim' constructor.+  type XExpPrim x :: Type+  type XExpPrim _ = ()++  -- | Additional constructors.+  type XExp x :: Type+  type XExp _ = Void++-- | Constraint all the extra fields provided by this extension.+type ExpExtrasConstrained c x =+  Each '[c]+  [XExpInt x, XExpString x, XExpBytes x, XExpSeq x, XExpPrim x]++-- | Constraint all the extra fields and the constructor provided by+-- this extension.+type ExpAllExtrasConstrainted c x = (ExpExtrasConstrained c x, c (XExp x))++-- | A helper type that carries something for all extra fields.+--+-- Fields are carried in the given functor @f@ so that one could provide+-- a generator, parser or something else.+--+-- Extra constructor is not included here as it may need special treatment,+-- you have to carry it separately.+data ExpExtras f x = ExpExtras+  { eeInt :: f (XExpInt x)+  , eeString :: f (XExpString x)+  , eeBytes :: f (XExpBytes x)+  , eeSeq :: f (XExpSeq x)+  , eePrim :: f (XExpPrim x)+  }++-- | Fill 'ExpExtras' with the same data, assuming all types of extras are+-- the same.+mkUniformExpExtras+  :: ( extra ~ XExpInt x+     , extra ~ XExpString x+     , extra ~ XExpBytes x+     , extra ~ XExpSeq x+     , extra ~ XExpPrim x+     )+  => f extra -> ExpExtras f x+mkUniformExpExtras x = ExpExtras x x x x x++-- | Change the functor used in 'ExpExtras'.+hoistExpExtras+  :: (forall extra. f1 extra -> f2 extra)+  -> ExpExtras f1 x -> ExpExtras f2 x+hoistExpExtras f ExpExtras{..} = ExpExtras+  { eeInt = f eeInt+  , eeString = f eeString+  , eeBytes = f eeBytes+  , eeSeq = f eeSeq+  , eePrim = f eePrim+  }++-- | Extension descriptor for plain expressions without additional data.+data RegularExp :: ExpExtensionDescriptorKind+instance ExpExtensionDescriptor RegularExp++-- | Simple expression without any extras.+type Expression = Exp RegularExp++expressionInt :: Integer -> Expression+expressionInt a = ExpInt () a++expressionString :: Text -> Expression+expressionString a = ExpString () a++expressionBytes :: ByteString -> Expression+expressionBytes a = ExpBytes () a++expressionSeq :: [Expression] -> Expression+expressionSeq a = ExpSeq () a++expressionPrim :: MichelinePrimAp RegularExp -> Expression+expressionPrim a = ExpPrim () a++expressionPrim' :: Text -> [Expression] -> [Annotation] -> Expression+expressionPrim' primName args anns =+  ExpPrim () (MichelinePrimAp (MichelinePrimitive primName) args anns)++-- | Default instance that uses @uniplate@ as implementation.+--+-- If it tries to find expressions for polymorphic types too agressively+-- (requiring 'Data' where you don't what that), feel free to define an+-- overlapping manual instance.+instance ( Typeable x+         , ExpAllExtrasConstrainted Data x+         , ExpAllExtrasConstrainted Typeable x)+         => Plated (Exp x)+ instance Buildable Expression where   build = \case-    ExpressionInt i -> build $ i-    ExpressionString s -> build s-    ExpressionBytes b ->+    ExpInt () i -> build i+    ExpString () s -> build s+    ExpBytes () b ->       build $ encodeBase58Check b-    ExpressionSeq s -> "(" +| buildList build s |+ ")"-    ExpressionPrim (MichelinePrimAp (MichelinePrimitive text) s annots) ->+    ExpSeq () s -> "(" +| buildList build s |+ ")"+    ExpPrim () (MichelinePrimAp (MichelinePrimitive text) s annots) ->       text <> " " |+ "(" +|       buildList build s +| ") " +|       buildList (build . annotToText) annots@@ -150,19 +297,24 @@   | AnnotationField FieldAnn   deriving stock (Eq, Show, Data, Lift) -data MichelinePrimAp = MichelinePrimAp+data MichelinePrimAp x = MichelinePrimAp   { mpaPrim :: MichelinePrimitive-  , mpaArgs :: [Expression]+  , mpaArgs :: [Exp x]   , mpaAnnots :: [Annotation]-  } deriving stock (Eq, Show, Data, Lift)+  } -instance FromJSON MichelinePrimAp where+deriving stock instance Eq (Exp x) => Eq (MichelinePrimAp x)+deriving stock instance Show (Exp x) => Show (MichelinePrimAp x)+deriving stock instance (Data (Exp x), Typeable x) => Data (MichelinePrimAp x)+deriving stock instance Lift (Exp x) => Lift (MichelinePrimAp x)++instance FromJSON (Exp x) => FromJSON (MichelinePrimAp x) where   parseJSON = withObject "Prim" $ \v -> MichelinePrimAp     <$> v .: "prim"     <*> v .:? "args" .!= []     <*> v .:? "annots" .!= [] -instance ToJSON MichelinePrimAp where+instance ToJSON (Exp x) => ToJSON (MichelinePrimAp x) where   toJSON MichelinePrimAp {..} = object $ catMaybes     [ Just ("prim" .= mpaPrim)     , if null mpaArgs then Nothing else Just ("args" .= mpaArgs)@@ -198,6 +350,12 @@      (AnnotationField <$> asFields minAnnSet) <>      (AnnotationVariable <$> asVars minAnnSet) +mkAnnsFromAny :: [U.AnyAnn] -> [Annotation]+mkAnnsFromAny xs = xs <&> \case+  U.AnyAnnType x -> AnnotationType x+  U.AnyAnnField x -> AnnotationField x+  U.AnyAnnVar x -> AnnotationVariable x+ isAnnotationField :: Annotation -> Bool isAnnotationField = \case   AnnotationField _ -> True@@ -234,25 +392,71 @@   toEncoding = toEncoding . annotToText  instance FromJSON Expression where-  parseJSON v = ExpressionSeq <$> parseJSON v-            <|> ExpressionPrim <$> parseJSON v-            <|> ExpressionString <$> withObject "ExpressionString" (.: "string") v-            <|> ExpressionInt . unStringEncode <$> withObject "ExpressionInt" (.: "int") v-            <|> ExpressionBytes . unHexJSONByteString <$> withObject "ExpressionBytes" (.: "bytes") v+  parseJSON v = ExpSeq () <$> parseJSON v+            <|> ExpPrim () <$> parseJSON v+            <|> ExpString () <$> withObject "ExpressionString" (.: "string") v+            <|> ExpInt () . unStringEncode <$> withObject "ExpressionInt" (.: "int") v+            <|> ExpBytes () . unHexJSONByteString <$> withObject "ExpressionBytes" (.: "bytes") v  instance ToJSON Expression where-  toJSON (ExpressionSeq xs) = toJSON xs-  toJSON (ExpressionPrim xs) = toJSON xs-  toJSON (ExpressionString x) = Aeson.Object (HashMap.singleton "string" $ toJSON x)-  toJSON (ExpressionInt x) = Aeson.Object (HashMap.singleton "int" $ toJSON $ StringEncode x)-  toJSON (ExpressionBytes x) = Aeson.Object (HashMap.singleton "bytes" $ toJSON $ HexJSONByteString x)+  toJSON (ExpSeq () xs) = toJSON xs+  toJSON (ExpPrim () xs) = toJSON xs+  toJSON (ExpString () x) = Aeson.Object (KeyMap.singleton "string" $ toJSON x)+  toJSON (ExpInt () x) = Aeson.Object (KeyMap.singleton "int" $ toJSON $ StringEncode x)+  toJSON (ExpBytes () x) = Aeson.Object (KeyMap.singleton "bytes" $ toJSON $ HexJSONByteString x) -  toEncoding (ExpressionSeq xs) = toEncoding xs-  toEncoding (ExpressionPrim xs) = toEncoding xs-  toEncoding (ExpressionString x) = Aeson.pairs (Aeson.pair "string" (toEncoding x))-  toEncoding (ExpressionInt x) = Aeson.pairs (Aeson.pair "int" (toEncoding $ StringEncode x))-  toEncoding (ExpressionBytes x) = Aeson.pairs (Aeson.pair "bytes" (toEncoding $ HexJSONByteString x))+  toEncoding (ExpSeq () xs) = toEncoding xs+  toEncoding (ExpPrim () xs) = toEncoding xs+  toEncoding (ExpString () x) = Aeson.pairs (Aeson.pair "string" (toEncoding x))+  toEncoding (ExpInt () x) = Aeson.pairs (Aeson.pair "int" (toEncoding $ StringEncode x))+  toEncoding (ExpBytes () x) = Aeson.pairs (Aeson.pair "bytes" (toEncoding $ HexJSONByteString x)) -makePrisms ''Expression+--------------------------------------------------------------------------------+-- Optics+--------------------------------------------------------------------------------++_ExpInt :: Prism' (Exp d) (XExpInt d, Integer)+_ExpInt = prism' (uncurry ExpInt) \case+  ExpInt x a -> Just (x, a)+  _ -> Nothing++_ExpString :: Prism' (Exp d) (XExpString d, Text)+_ExpString = prism' (uncurry ExpString) \case+  ExpString x a -> Just (x, a)+  _ -> Nothing++_ExpBytes :: Prism' (Exp d) (XExpBytes d, ByteString)+_ExpBytes = prism' (uncurry ExpBytes) \case+  ExpBytes x a -> Just (x, a)+  _ -> Nothing++_ExpSeq :: Prism' (Exp d) (XExpSeq d, [Exp d])+_ExpSeq = prism' (uncurry ExpSeq) \case+  ExpSeq x a -> Just (x, a)+  _ -> Nothing++_ExpPrim :: Prism' (Exp d) (XExpPrim d, MichelinePrimAp d)+_ExpPrim = prism' (uncurry ExpPrim) \case+  ExpPrim x a -> Just (x, a)+  _ -> Nothing++neglecting :: Iso' ((), a) a+neglecting = iso snd pure++_ExpressionInt :: Prism' Expression Integer+_ExpressionInt = _ExpInt . neglecting++_ExpressionString :: Prism' Expression Text+_ExpressionString = _ExpString . neglecting++_ExpressionBytes :: Prism' Expression ByteString+_ExpressionBytes = _ExpBytes . neglecting++_ExpressionSeq :: Prism' Expression [Expression]+_ExpressionSeq = _ExpSeq . neglecting++_ExpressionPrim :: Prism' Expression (MichelinePrimAp RegularExp)+_ExpressionPrim = _ExpPrim . neglecting+ makePrisms ''Annotation makeLensesWith postfixLFields ''MichelinePrimAp

@@ -0,0 +1,107 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- | Expression that carries the same extra data for all 'Exp' constructors.+module Morley.Micheline.Expression.WithMeta+  ( -- * General case+    expAllExtraL++    -- * Custom extra field, no extra constructors+  , WithMeta+  , ExpressionWithMeta+  , expMetaL+  , expAnnotate+  , expAllMetaL++    -- * Utilities+  , IsEq+  ) where++import Control.Lens qualified as L++import Morley.Micheline.Expression+import Morley.Util.Type (IsEq)++--------------------------------------------------------------------------------+-- General case+--------------------------------------------------------------------------------++-- | Traversal that visits all the extra fields ('XExpInt' and others)+-- in DFS order assuming they are the same for every constructor.+--+-- It is generic enough to work not only with 'ExpressionWithMeta', but+-- with any 'Exp' that has all the extra fields of the same type;+-- hence, this traversal is applicable to 'Expression' too.+--+-- This also supports additional constructors. Use 'L.devoid' if you have none.+--+-- Moreover, when used as setter, it can change the type of meta.+expAllExtraL+  :: forall x2 x1 meta2 meta1.+     ( ExpExtrasConstrained (IsEq meta1) x1+     , ExpExtrasConstrained (IsEq meta2) x2+     )+  => Traversal (XExp x1) (XExp x2) meta1 meta2+  -> Traversal (Exp x1) (Exp x2) meta1 meta2+expAllExtraL ctorL = go+  where+    go f = \case+      ExpInt x a -> ExpInt <$> f x <*> pure a+      ExpString x a -> ExpString <$> f x <*> pure a+      ExpBytes x a -> ExpBytes <$> f x <*> pure a+      ExpSeq x a -> ExpSeq <$> f x <*> traverse (go f) a+      ExpPrim x a ->+        ExpPrim <$> f x <*> L.traverseOf (mpaArgsL . L.traversed) (go f) a+      ExpX x -> ExpX <$> ctorL f x++--------------------------------------------------------------------------------+-- Custom extra field, no extra constructors+--------------------------------------------------------------------------------++-- | Expression that has the same type of metadata attached to each of+-- its constructors.+data WithMeta (meta :: Type) :: ExpExtensionDescriptorKind+instance ExpExtensionDescriptor (WithMeta m) where+  type XExpInt (WithMeta m) = m+  type XExpString (WithMeta m) = m+  type XExpBytes (WithMeta m) = m+  type XExpSeq (WithMeta m) = m+  type XExpPrim (WithMeta m) = m++-- | Alias for expression with given meta.+type ExpressionWithMeta meta = Exp (WithMeta meta)++{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}++-- | Lens for getting immediate meta of the node.+expMetaL :: Lens' (Exp (WithMeta meta)) meta+expMetaL f = \case+  ExpInt x a ->+    f x <&> \x' -> ExpInt x' a+  ExpString x a ->+    f x <&> \x' -> ExpString x' a+  ExpBytes x a ->+    f x <&> \x' -> ExpBytes x' a+  ExpSeq x a ->+    f x <&> \x' -> ExpSeq x' a+  ExpPrim x a ->+    f x <&> \x' -> ExpPrim x' a++-- | Traversal that visits all the metas in DFS order.+-- This is a specialization of 'expAllExtraL'.+--+-- This is pretty similar to 'expMetaL', but picks meta of all the+-- transitive children.+--+-- When used as setter, it can change the type of meta.+expAllMetaL+  :: forall x2 x1 meta2 meta1.+     ( ExpExtrasConstrained (IsEq meta1) x1+     , ExpExtrasConstrained (IsEq meta2) x2+     )+  => Traversal (ExpressionWithMeta meta1) (ExpressionWithMeta meta2) meta1 meta2+expAllMetaL = expAllExtraL L.devoid++-- | Lift plain 'Expression' to 'ExpressionWithMeta'.+expAnnotate :: Expression -> ExpressionWithMeta ()+expAnnotate = expAllExtraL L.devoid %~ id

@@ -6,9 +6,7 @@   , Pos (..)   , SrcPos (..)   , srcPos-  , InstrCallStack (..)-  , LetCallStack-  , LetName (..)+  , ErrorSrcPos (..)   ) where  import Unsafe qualified (fromIntegral)@@ -16,10 +14,9 @@ import Data.Aeson.TH (deriveJSON) import Data.Data (Data(..)) import Data.Default (Default(..))-import Data.Text qualified as T import Fmt (Buildable(..)) import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended, renderAnyBuildable)-import Text.PrettyPrint.Leijen.Text (list, (<+>))+import Text.PrettyPrint.Leijen.Text ((<+>))  import Morley.Util.Aeson @@ -47,40 +44,26 @@ srcPos :: Word -> Word -> SrcPos srcPos x y = SrcPos (Pos x) (Pos y) -newtype LetName = LetName T.Text-  deriving stock (Eq, Ord, Show, Data, Generic)-  deriving newtype Buildable--instance NFData LetName--type LetCallStack = [LetName]-data InstrCallStack = InstrCallStack-  { icsCallStack :: LetCallStack-  , icsSrcPos    :: SrcPos+newtype ErrorSrcPos = ErrorSrcPos+  { unErrorSrcPos :: SrcPos   } deriving stock (Eq, Ord, Show, Generic, Data)+    deriving newtype (Default)+    deriving anyclass (NFData) -instance RenderDoc InstrCallStack where-  renderDoc _ InstrCallStack{icsCallStack, icsSrcPos = SrcPos (Pos row) (Pos col)} =+instance RenderDoc ErrorSrcPos where+  renderDoc _ ErrorSrcPos{unErrorSrcPos = SrcPos (Pos row) (Pos col)} =     "Error occurred on line" <+> (renderAnyBuildable (row + 1)) <+> "char" <+> (renderAnyBuildable (col + 1))-    <> case icsCallStack of-         [] -> "."-         _ -> " inside these let defenitions:" <+> (list $ fmap renderAnyBuildable icsCallStack) <> "."+    <> "." -instance Buildable InstrCallStack where+instance Buildable ErrorSrcPos where   build = buildRenderDocExtended -instance NFData InstrCallStack- instance Default Pos where   def = Pos 0  instance Default SrcPos where   def = SrcPos def def -instance Default InstrCallStack where-  def = InstrCallStack def def- deriveJSON morleyAesonOptions ''Pos deriveJSON morleyAesonOptions ''SrcPos-deriveJSON morleyAesonOptions ''LetName-deriveJSON morleyAesonOptions ''InstrCallStack+deriveJSON morleyAesonOptions ''ErrorSrcPos

@@ -56,8 +56,8 @@         PUSH v -> isTypicalErrorConstant v         Seq _ (PUSH v) -> isTypicalErrorConstant v -        Seq (PUSH v) PAIR -> FailWithStackValue <$> isStringValue v-        Seq (Seq _ (PUSH v)) PAIR -> FailWithStackValue <$> isStringValue v+        Seq (PUSH v) PAIR{} -> FailWithStackValue <$> isStringValue v+        Seq (Seq _ (PUSH v)) PAIR{} -> FailWithStackValue <$> isStringValue v          _ -> Nothing @@ -92,24 +92,24 @@             -- It is quite hard to move the body of these very similar             -- cases into a separate function because involved types             -- are quite sophisticated.-            Seq (PUSH v) PAIR+            Seq (AnnPUSH ann@(Anns2' s _) v) (AnnPAIR ann')               | _ :: Value a <- v               , _ :: Instr (b ': s) ('TPair a b ': s) <- i1 ->                 case sing @('TPair a b) of                   STPair l r -> withSingI l $ withSingI r $ case isStringValue v of                     Just (f -> SomeConstant v') ->-                      PUSH v' `Seq` PAIR `Seq` FAILWITH+                      AnnPUSH (Anns2' s starNotes) v' `Seq` AnnPAIR ann' `Seq` FAILWITH                     Nothing ->-                      PUSH v `Seq` PAIR `Seq` FAILWITH-            Seq (Seq i0 (PUSH v)) PAIR+                      AnnPUSH ann v `Seq` AnnPAIR ann' `Seq` FAILWITH+            Seq (Seq i0 (AnnPUSH ann@(Anns2' s _) v)) (AnnPAIR ann')               | _ :: Value a <- v               , _ :: Instr s0 ('TPair a b ': s) <- i1 ->                 case sing @('TPair a b) of                   STPair l r -> withSingI l $ withSingI r $ Seq i0 $ case isStringValue v of                     Just (f -> SomeConstant v') ->-                      PUSH v' `Seq` PAIR `Seq` FAILWITH+                      AnnPUSH (Anns2' s starNotes) v' `Seq` AnnPAIR ann' `Seq` FAILWITH                     Nothing ->-                      PUSH v `Seq` PAIR `Seq` FAILWITH+                      AnnPUSH ann v `Seq` AnnPAIR ann' `Seq` FAILWITH              _ -> Seq i1 FAILWITH 

@@ -1,9 +1,6 @@ -- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA --- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations #-}- -- | Module, containing function to interpret Michelson -- instructions against given context and input stack. module Morley.Michelson.Interpret@@ -29,7 +26,6 @@   , EvalM   , InterpreterStateMonad (..)   , StkEl (..)-  , starNotesStkEl   , InstrRunner   , runInstr   , runInstrNoGas@@ -60,18 +56,17 @@ import Fmt (Buildable(build), blockListF, pretty, prettyLn, (+|), (|+)) import Unsafe qualified (fromIntegral) -import Morley.Michelson.ErrorPos (InstrCallStack(..))+import Morley.Michelson.ErrorPos (ErrorSrcPos(..)) import Morley.Michelson.Interpret.Pack (packValue') import Morley.Michelson.Interpret.Unpack (UnpackError, unpackValue') import Morley.Michelson.Runtime.GState-import Morley.Michelson.TypeCheck (matchTypes)+import Morley.Michelson.TypeCheck (eqType) import Morley.Michelson.Typed hiding (Branch(..)) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Operation   (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)-import Morley.Michelson.Untyped qualified as U-import Morley.Michelson.Untyped.Annotation (annQ) import Morley.Tezos.Address (Address(..), GlobalCounter(..))+import Morley.Tezos.Address.Alias (Alias) import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez) import Morley.Tezos.Crypto   (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,@@ -126,21 +121,15 @@  makePrisms ''MorleyLogs -data StkEl t = StkEl+newtype StkEl t = StkEl   { seValue :: Value t-  , seVarAnn :: U.VarAnn-  , seNotes :: Notes t   } deriving stock (Eq, Show)  makeLensesFor   [ ("seValue", "seValueL")-  , ("seVarAnn", "seVarAnnL")   ]   ''StkEl -starNotesStkEl :: forall t. Value t -> StkEl t-starNotesStkEl v = StkEl v U.noAnn $ withValueTypeSanity v $ starNotes @t- -- | Environment for contract execution. data ContractEnv = ContractEnv   { ceNow :: Timestamp@@ -168,8 +157,10 @@   -- correct contract address computation in @CREATE_CONTRACT@ instruction.   , ceLevel :: Natural   -- ^ Number of blocks before the given one in the chain-  , ceInstrCallStack :: InstrCallStack+  , ceErrorSrcPos :: ErrorSrcPos   -- ^ Current source position information+  , ceMinBlockTime :: Natural+  -- ^ Minimum time between blocks   }  -- | Represents @[FAILED]@ state of a Michelson program. Contains@@ -209,10 +200,10 @@       MichelsonUnsupported instr ->         build instr <> " instruction is not supported." --- | Carries a 'MichelsonFailed' error and the 'InstrCallStack' at which it was raised+-- | Carries a 'MichelsonFailed' error and the 'ErrorSrcPos' at which it was raised data MichelsonFailureWithStack = MichelsonFailureWithStack   { mfwsFailed :: MichelsonFailed-  , mfwsInstrCallStack :: InstrCallStack+  , mfwsErrorSrcPos :: ErrorSrcPos   } deriving stock (Show, Generic, Eq)  instance Buildable MichelsonFailureWithStack where@@ -262,7 +253,7 @@ -- | Helper function to convert a record of @Value@ to @StkEl@. These will be -- created with @starNotes@. mapToStkEl :: Rec T.Value inp -> Rec StkEl inp-mapToStkEl = rmap starNotesStkEl+mapToStkEl = rmap StkEl  -- | Helper function to convert a record of @StkEl@ to @Value@. Any present -- notes will be discarded.@@ -280,24 +271,20 @@   -> ContractReturn st interpret' Contract{..} epc param initSt env ist = first (fmap fromFinalStack) $   runEvalOp-    (runInstr cCode $ mkInitStack (liftCallArg epc param) cParamNotes initSt cStoreNotes)+    (runInstr (unContractCode cCode) $ mkInitStack (liftCallArg epc param) initSt)     env     ist  mkInitStack   :: T.Value param-  -> T.ParamNotes param   -> T.Value st-  -> T.Notes st   -> Rec StkEl (ContractInp param st)-mkInitStack param T.UnsafeParamNotes{..} st stNotes = StkEl+mkInitStack param st = StkEl   (T.VPair (param, st))-  U.noAnn-  (T.NTPair U.noAnn (U.convAnn pnRootAnn) U.noAnn [annQ|parameter|] [annQ|storage|] pnNotes stNotes)     :& RNil  fromFinalStack :: Rec StkEl (ContractOut st) -> ([T.Operation], T.Value st)-fromFinalStack (StkEl (T.VPair (T.VList ops, st)) _ _ :& RNil) =+fromFinalStack (StkEl (T.VPair (T.VList ops, st)) :& RNil) =   (map (\(T.VOp op) -> op) ops, st)  interpret@@ -316,7 +303,7 @@ initInterpreterState globalCounter bmCounter env =   InterpreterState (ceMaxSteps env) globalCounter bmCounter --- | Interpret an instruction in vacuum, putting no extra contraints on+-- | Interpret an instruction in vacuum, putting no extra constraints on -- its execution. -- -- Mostly for testing purposes.@@ -327,7 +314,7 @@   -> Either MichelsonFailureWithStack (Rec T.Value out) interpretInstr = fmap mapToValue ... interpretInstrAnnotated --- | Interpret an instruction in vacuum, putting no extra contraints on+-- | Interpret an instruction in vacuum, putting no extra constraints on -- its execution while preserving its annotations. -- -- Mostly for testing purposes.@@ -410,20 +397,16 @@   -> m (Rec StkEl out)  throwMichelson :: EvalM m => MichelsonFailed -> m a-throwMichelson mf = asks ceInstrCallStack >>= throwError . MichelsonFailureWithStack mf+throwMichelson mf = asks ceErrorSrcPos >>= throwError . MichelsonFailureWithStack mf  -- | Function to change amount of remaining steps stored in State monad. runInstr :: EvalM m => InstrRunner m runInstr i@(Seq _i1 _i2) r = runInstrImpl runInstr i r runInstr i@(WithLoc _ _) r = runInstrImpl runInstr i r runInstr i@(Meta _ _i1) r = runInstrImpl runInstr i r-runInstr i@(InstrWithNotes _ _ _i1) r = runInstrImpl runInstr i r-runInstr i@(InstrWithVarNotes _ _i1) r = runInstrImpl runInstr i r-runInstr i@(InstrWithVarAnns _ _i1) r = runInstrImpl runInstr i r runInstr i@Nop r = runInstrImpl runInstr i r runInstr i@(Nested _) r = runInstrImpl runInstr i r runInstr i@(DocGroup _ _i1) r = runInstrImpl runInstr i r-runInstr i@(Fn _ _ _i1) r = runInstrImpl runInstr i r runInstr i r = do   rs <- isRemainingSteps <$> getInterpreterState   if rs == 0@@ -438,25 +421,8 @@ -- | Function to interpret Michelson instruction(s) against given stack. runInstrImpl :: forall m. EvalM m => InstrRunner m -> InstrRunner m runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'-runInstrImpl runner (WithLoc ics i) r = local (\env -> env{ceInstrCallStack = ics}) $ runner i r+runInstrImpl runner (WithLoc ics i) r = local (\env -> env{ceErrorSrcPos = ics}) $ runner i r runInstrImpl runner (Meta _ i) r = runner i r-runInstrImpl runner (InstrWithNotes (_ :: Proxy rest) notes instr) inp = do-  out <- runner instr inp-  let zipRec :: Rec Notes topElems -> Rec StkEl (topElems ++ rest) -> Rec StkEl (topElems ++ rest)-      zipRec RNil stkElems = stkElems-      zipRec (stkElemNotes :& xs) (stkElem :& ys) =-        stkElem { seNotes = stkElemNotes } :& zipRec xs ys-  pure $ zipRec notes out-runInstrImpl runner (InstrWithVarNotes _vns i) inp = runner i inp-runInstrImpl runner (InstrWithVarAnns vns i) inp = do-  runner i inp <&> \case-    StkEl v1 _ n1 :& StkEl v2 vn2 n2 :& r -> case vns of-      U.OneVarAnn vn      -> StkEl v1 vn n1 :& StkEl v2 vn2 n2 :& r-      U.TwoVarAnns vn vn' -> StkEl v1 vn n1 :& StkEl v2 vn' n2 :& r-    StkEl v _ n :& r -> case vns of-      U.OneVarAnn vn   -> StkEl v vn n :& r-      U.TwoVarAnns _ _ -> error "Input stack is exhausted but there is still a variable annotation."-    RNil -> error "Input stack is exhausted but there is still variables annotations." runInstrImpl runner (FrameInstr (_ :: Proxy s) i) r = do   let (inp, end) = rsplit @_ @_ @s r   out <- runInstrImpl runner i inp@@ -465,7 +431,6 @@ runInstrImpl runner (Ext nop) r = r <$ interpretExt runner (SomeItStack nop r) runInstrImpl runner (Nested sq) r = runner sq r runInstrImpl runner (DocGroup _ sq) r = runInstrImpl runner sq r-runInstrImpl runner (Fn _ _ i) r = runner i r runInstrImpl _ DROP (_ :& r) = pure $ r runInstrImpl runner (DROPN n) stack =   case n of@@ -479,19 +444,18 @@       -- This recursion is implementation detail of `DROPN`.       -- The same reasoning applies to other instructions parameterized       -- by a natural number like 'DIPN'.-runInstrImpl _ DUP (stkEl :& r) = do+runInstrImpl _ AnnDUP{} (stkEl :& r) = do   -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).   duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl   pure $ duplicateStkEl :& stkEl :& r-runInstrImpl _ (DUPN s) stack = go s stack+runInstrImpl _ (AnnDUPN _ s) stack = go s stack   where     go :: forall (n :: Peano) inp out a. ConstraintDUPN n inp out a        => PeanoNatural n -> Rec StkEl inp -> m (Rec StkEl out)     go (Succ Zero) stk@(stkEl :& _) = do         -- If we're duplicating a big_map, or a value containing big_map(s), we need to generate new big_map ID(s).         duplicateStkEl <- traverseOf seValueL assignBigMapIds' stkEl-        -- Discard variable annotations. This is consistent with tezos-client.-        pure $ (duplicateStkEl & seVarAnnL .~ U.noAnn) :& stk+        pure $ duplicateStkEl :& stk     go (Succ n@(Succ _)) (b :& r) =       go n r <&> \case         (a :& resTail) -> a :& b :& resTail@@ -513,102 +477,91 @@        => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out     go Zero stack = stack     go (Succ n') (a :& b :& r) = b :& go n' (a :& r)-runInstrImpl _ SOME ((seValue -> a) :& r) =+runInstrImpl _ AnnSOME{} ((seValue -> a) :& r) =   withValueTypeSanity a $-    pure $ starNotesStkEl (VOption (Just a)) :& r-runInstrImpl _ (PUSH v) r = pure $ starNotesStkEl v :& r-runInstrImpl _ NONE r = pure $ starNotesStkEl (VOption Nothing) :& r-runInstrImpl _ UNIT r = pure $ starNotesStkEl VUnit :& r-runInstrImpl runner (IF_NONE _bNone bJust) (StkEl (VOption (Just a)) vn (NTOption _ n) :& r) =-  runner bJust (StkEl a vn n :& r)-runInstrImpl runner (IF_NONE bNone _bJust) (StkEl (VOption Nothing) _ _ :& r) =+    pure $ StkEl (VOption (Just a)) :& r+runInstrImpl _ (AnnPUSH _ v) r = pure $ StkEl v :& r+runInstrImpl _ AnnNONE{} r = pure $ StkEl (VOption Nothing) :& r+runInstrImpl _ AnnUNIT{} r = pure $ StkEl VUnit :& r+runInstrImpl runner (IF_NONE _bNone bJust) (StkEl (VOption (Just a)) :& r) =+  runner bJust (StkEl a :& r)+runInstrImpl runner (IF_NONE bNone _bJust) (StkEl (VOption Nothing) :& r) =   runner bNone r runInstrImpl _ NEVER inp = case inp of {}-runInstrImpl _ (AnnPAIR{}) ((StkEl a _ _) :& (StkEl b _ _) :& r) =-  pure $ starNotesStkEl (VPair (a, b)) :& r-runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b)) _ _) :& r) =-  pure $ starNotesStkEl a :& starNotesStkEl b :& r-runInstrImpl _ (PAIRN s) stack = pure $ go s stack+runInstrImpl _ (AnnPAIR{}) ((StkEl a) :& (StkEl b) :& r) =+  pure $ StkEl (VPair (a, b)) :& r+runInstrImpl _ (AnnUNPAIR{}) ((StkEl (VPair (a, b))) :& r) =+  pure $ StkEl a :& StkEl b :& r+runInstrImpl _ (AnnPAIRN _ s) stack = pure $ go s stack   where     go :: forall n inp. ConstraintPairN n inp => PeanoNatural n -> Rec StkEl inp -> Rec StkEl (PairN n inp)-    go (Succ (Succ Zero)) (StkEl a _ _ :& StkEl b _ _ :& r) =+    go (Succ (Succ Zero)) (StkEl a :& StkEl b :& r) =       -- if n=2-      starNotesStkEl (VPair (a, b)) :& r-    go (Succ n@(Succ (Succ _))) (StkEl a _ _ :& r@(_ :& _ :& _)) =+      StkEl (VPair (a, b)) :& r+    go (Succ n@(Succ (Succ _))) (StkEl a :& r@(_ :& _ :& _)) =       -- if n>2       case go n r of-        StkEl combed _ _ :& r' ->-            starNotesStkEl (VPair (a, combed)) :& r'-runInstrImpl _ (UNPAIRN s) (StkEl pair0 _ pairNotes0 :& r) = do-  pure $ go s pair0 pairNotes0 <+> r+        StkEl combed :& r' ->+            StkEl (VPair (a, combed)) :& r'+runInstrImpl _ (UNPAIRN s) (StkEl pair0 :& r) = do+  pure $ go s pair0 <+> r   where     go       :: forall n pair. ConstraintUnpairN n pair-      => PeanoNatural n -> Value pair -> Notes pair+      => PeanoNatural n -> Value pair       -> Rec StkEl (UnpairN n pair)-    go n pair pairNotes =-      case (n, pair, pairNotes) of+    go n pair =+      case (n, pair) of         -- if n=2-        (Succ (Succ Zero), VPair (a, b), NTPair _ aFieldAnn bFieldAnn _ _ aNotes bNotes) ->-          -- @UNPAIR n@ converts field annotations into var annotations.-          ---          -- > /* [ @pair pair (int %aa) (int %bb) (int %cc) (int %dd) ] */ ;-          -- > UNPAIR 3-          -- > /* [ @aa int : @bb int : pair (int %cc) (int %dd) ] */ ;-          ---          -- Nested var annotations will be discarded.-          ---          -- > /* [ pair (int @c) (int @a) (int @b) ] */ ;-          -- UNPAIR 3-          -- /* [ int : int : int ] */ ;-          StkEl a (U.convAnn @U.FieldTag @U.VarTag aFieldAnn) aNotes-            :& StkEl b (U.convAnn @U.FieldTag @U.VarTag bFieldAnn) bNotes+        (Succ (Succ Zero), VPair (a, b)) ->+          StkEl a+            :& StkEl b             :& RNil         -- if n>2-        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _)), NTPair _ aFieldAnn _ _ _ aNotes bNotes) ->-          StkEl a (U.convAnn @U.FieldTag @U.VarTag aFieldAnn) aNotes-            :& go n' b bNotes-runInstrImpl _ (AnnCAR _ _) (StkEl (VPair (a, _b)) _ _ :& r) = pure $ starNotesStkEl a :& r-runInstrImpl _ (AnnCDR _ _) (StkEl (VPair (_a, b)) _ _ :& r) = pure $ starNotesStkEl b :& r-runInstrImpl _ (AnnLEFT nt nf1 nf2) ((StkEl a _ na) :& r) =+        (Succ n'@(Succ (Succ _)), VPair (a, b@(VPair _))) ->+          StkEl a+            :& go n' b+runInstrImpl _ AnnCAR{} (StkEl (VPair (a, _b)) :& r) = pure $ StkEl a :& r+runInstrImpl _ AnnCDR{} (StkEl (VPair (_a, b)) :& r) = pure $ StkEl b :& r+runInstrImpl _ AnnLEFT{} ((StkEl a) :& r) =   withValueTypeSanity a $-    pure $ StkEl (VOr $ Left a) U.noAnn (NTOr nt nf1 nf2 na starNotes) :& r-runInstrImpl _ (AnnRIGHT nt nf1 nf2) ((StkEl b _ nb) :& r) =+    pure $ StkEl (VOr $ Left a) :& r+runInstrImpl _ AnnRIGHT{} ((StkEl b) :& r) =   withValueTypeSanity b $-    pure $ StkEl (VOr $ Right b) U.noAnn (NTOr nt nf1 nf2 starNotes nb) :& r-runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) vn (NTOr _ _ _ nl _) :& r) =-  runner bLeft (StkEl a vn nl :& r)-runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) vn (NTOr _ _ _ _ nr) :& r) =-  runner bRight (StkEl a vn nr :& r)-runInstrImpl _ NIL r = pure $ starNotesStkEl (VList []) :& r-runInstrImpl _ CONS (a :& StkEl (VList l) _ _ :& r) = pure $ starNotesStkEl (VList (seValue a : l)) :& r-runInstrImpl runner (IF_CONS _ bNil) (StkEl (VList []) _ _ :& r) = runner bNil r-runInstrImpl runner (IF_CONS bCons _) (StkEl (VList (lh : lr)) vn ntl@(NTList _ nhd) :& r) =-  runner bCons (StkEl lh vn nhd :& StkEl (VList lr) vn ntl :& r)-runInstrImpl _ SIZE (a :& r) = pure $ starNotesStkEl (VNat $ Unsafe.fromIntegral @Int @Natural $ evalSize $ seValue a) :& r-runInstrImpl _ EMPTY_SET r = pure $ starNotesStkEl (VSet Set.empty) :& r-runInstrImpl _ EMPTY_MAP r = pure $ starNotesStkEl (VMap Map.empty) :& r-runInstrImpl _ EMPTY_BIG_MAP r = do+    pure $ StkEl (VOr $ Right b) :& r+runInstrImpl runner (IF_LEFT bLeft _) (StkEl (VOr (Left a)) :& r) =+  runner bLeft (StkEl a :& r)+runInstrImpl runner (IF_LEFT _ bRight) (StkEl (VOr (Right a)) :& r) =+  runner bRight (StkEl a :& r)+runInstrImpl _ AnnNIL{} r = pure $ StkEl (VList []) :& r+runInstrImpl _ AnnCONS{} (a :& StkEl (VList l) :& r) = pure $ StkEl (VList (seValue a : l)) :& r+runInstrImpl runner (IF_CONS _ bNil) (StkEl (VList []) :& r) = runner bNil r+runInstrImpl runner (IF_CONS bCons _) (StkEl (VList (lh : lr)) :& r) =+  runner bCons (StkEl lh :& StkEl (VList lr) :& r)+runInstrImpl _ AnnSIZE{} (a :& r) = pure $ StkEl (VNat $ Unsafe.fromIntegral @Int @Natural $ evalSize $ seValue a) :& r+runInstrImpl _ AnnEMPTY_SET{} r = pure $ StkEl (VSet Set.empty) :& r+runInstrImpl _ AnnEMPTY_MAP{} r = pure $ StkEl (VMap Map.empty) :& r+runInstrImpl _ AnnEMPTY_BIG_MAP{} r = do   bigMap <- assignBigMapIds' $ VBigMap Nothing Map.empty-  pure $ starNotesStkEl bigMap :& r-runInstrImpl runner (MAP (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl a vn n :& r) = do+  pure $ StkEl bigMap :& r+runInstrImpl runner (AnnMAP _ (code :: Instr (MapOpInp c ': s) (b ': s))) (StkEl a :& r) = do   -- Evaluation must preserve all stack modifications that @MAP@'s does.   (newStack, newList) <- foldlM (\(curStack, curList) (val :: StkEl (MapOpInp c)) -> do     res <- runner code (val :& curStack)     case res of       ((seValue -> nextVal :: T.Value b) :& nextStack) -> pure (nextStack, nextVal : curList))-    (r, []) ((\el -> StkEl el vn (mapOpNotes n)) <$> mapOpToList @c a)-  pure $ starNotesStkEl (mapOpFromList a (reverse newList)) :& newStack-runInstrImpl runner (ITER (code :: Instr (IterOpEl c ': s) s)) (StkEl a vn n :& r) =+    (r, []) ((\el -> StkEl el) <$> mapOpToList @c a)+  pure $ StkEl (mapOpFromList a (reverse newList)) :& newStack+runInstrImpl runner (ITER (code :: Instr (IterOpEl c ': s) s)) (StkEl a :& r) =   case iterOpDetachOne @c a of     (Just x, xs) -> do-      res <- runner code (StkEl x vn (iterOpNotes n) :& r)-      runner (ITER code) (StkEl xs vn n :& res)+      res <- runner code (StkEl x :& r)+      runner (ITER code) (StkEl xs :& res)     (Nothing, _) -> pure r-runInstrImpl _ MEM (a :& b :& r) = pure $ starNotesStkEl (VBool (evalMem (seValue a) (seValue b))) :& r-runInstrImpl _ GET (a :& b :& r) = pure $ starNotesStkEl (VOption (evalGet (seValue a) (seValue b))) :& r-runInstrImpl _ (GETN s) (StkEl pair _ _ :& r) = do-  pure $ starNotesStkEl (go s pair) :& r+runInstrImpl _ AnnMEM{} (a :& b :& r) = pure $ StkEl (VBool (evalMem (seValue a) (seValue b))) :& r+runInstrImpl _ AnnGET{} (a :& b :& r) = pure $ StkEl (VOption (evalGet (seValue a) (seValue b))) :& r+runInstrImpl _ (AnnGETN _ s) (StkEl pair :& r) = do+  pure $ StkEl (go s pair) :& r   where     go       :: forall ix a. ConstraintGetN ix a@@ -617,10 +570,10 @@     go Zero            a                   = a     go (Succ Zero)      (VPair (left, _))  = left     go (Succ (Succ n')) (VPair (_, right)) = go n' right-runInstrImpl _ UPDATE (a :& b :& StkEl c _ _ :& r) =-  pure $ starNotesStkEl (evalUpd (seValue a) (seValue b) c) :& r-runInstrImpl _ (UPDATEN s) (StkEl (val :: Value val) _ _  :& StkEl pair _ _ :& r) = do-  pure $ starNotesStkEl (go s pair) :& r+runInstrImpl _ AnnUPDATE{} (a :& b :& StkEl c :& r) =+  pure $ StkEl (evalUpd (seValue a) (seValue b) c) :& r+runInstrImpl _ (AnnUPDATEN _ s) (StkEl (val :: Value val) :& StkEl pair :& r) = do+  pure $ StkEl (go s pair) :& r   where     go       :: forall ix pair. ConstraintUpdateN ix pair@@ -628,27 +581,27 @@     go Zero             _                      = val     go (Succ Zero)      (VPair (_, right))     = VPair (val, right)     go (Succ (Succ n')) (VPair (left, right))  = VPair (left, go n' right)-runInstrImpl _ GET_AND_UPDATE (StkEl key _ _ :& StkEl valMb _ _ :& StkEl collection _ _ :& r) =+runInstrImpl _ AnnGET_AND_UPDATE{} (StkEl key :& StkEl valMb :& StkEl collection :& r) =   pure $-    starNotesStkEl (VOption (evalGet key collection))-    :& starNotesStkEl (evalUpd key valMb collection)+    StkEl (VOption (evalGet key collection))+    :& StkEl (evalUpd key valMb collection)     :& r-runInstrImpl runner (IF bTrue _) (StkEl (VBool True) _ _ :& r) = runner bTrue r-runInstrImpl runner (IF _ bFalse) (StkEl (VBool False) _ _ :& r) = runner bFalse r-runInstrImpl _ (LOOP _) (StkEl (VBool False) _ _ :& r) = pure $ r-runInstrImpl runner (LOOP ops) (StkEl (VBool True) _ _ :& r) = do+runInstrImpl runner (IF bTrue _) (StkEl (VBool True) :& r) = runner bTrue r+runInstrImpl runner (IF _ bFalse) (StkEl (VBool False) :& r) = runner bFalse r+runInstrImpl _ (LOOP _) (StkEl (VBool False) :& r) = pure $ r+runInstrImpl runner (LOOP ops) (StkEl (VBool True) :& r) = do   res <- runner ops r   runner (LOOP ops) res-runInstrImpl _ (LOOP_LEFT _) (StkEl (VOr (Right a)) _ _ :& r) = pure $ starNotesStkEl a :& r-runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) vn (NTOr _ _ _ nl _) :& r) = do-  res <- runner ops (StkEl a vn nl :& r)+runInstrImpl _ (LOOP_LEFT _) (StkEl (VOr (Right a)) :& r) = pure $ StkEl a :& r+runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) :& r) = do+  res <- runner ops (StkEl a :& r)   runner (LOOP_LEFT ops) res-runInstrImpl _ (LAMBDA lam) r = pure $ starNotesStkEl lam :& r-runInstrImpl runner EXEC (a :& StkEl (VLam (T.rfAnyInstr -> lBody)) _ _ :& r) = do+runInstrImpl _ (AnnLAMBDA _ lam) r = pure $ StkEl lam :& r+runInstrImpl runner AnnEXEC{} (a :& StkEl (VLam (T.rfAnyInstr -> lBody)) :& r) = do   res <- runner lBody (a :& RNil)   pure $ res <+> r-runInstrImpl _ APPLY (StkEl (a :: T.Value a) _ _ :& StkEl (VLam lBody) _ _ :& r) = do-  pure $ starNotesStkEl (VLam (T.rfMapAnyInstr doApply lBody)) :& r+runInstrImpl _ AnnAPPLY{} (StkEl (a :: T.Value a) :& StkEl (VLam lBody) :& r) = do+  pure $ StkEl (VLam (T.rfMapAnyInstr doApply lBody)) :& r   where     doApply :: Instr ('TPair a i ': s) o -> Instr (i ': s) o     doApply b = PUSH a `Seq` PAIR `Seq` Nested b@@ -661,53 +614,53 @@     Succ s' -> case stack of       (a :& r) -> (a :&) <$> runInstrImpl runner (DIPN s' i) r runInstrImpl _ FAILWITH (a :& _) = throwMichelson $ MichelsonFailedWith (seValue a)-runInstrImpl _ CAST (StkEl a _ _ :& r) = pure $ starNotesStkEl a :& r-runInstrImpl _ RENAME (StkEl a _ _ :& r) = pure $ starNotesStkEl a :& r-runInstrImpl _ PACK ((seValue -> a) :& r) = pure $ starNotesStkEl (VBytes $ packValue' a) :& r-runInstrImpl _ UNPACK (StkEl (VBytes a) _ _ :& r) =-  pure $ starNotesStkEl (VOption . rightToMaybe $ runUnpack a) :& r-runInstrImpl _ CONCAT (a :& b :& r) = pure $ starNotesStkEl (evalConcat (seValue a) (seValue b)) :& r-runInstrImpl _ CONCAT' (StkEl (VList a) _ _ :& r) = pure $ starNotesStkEl (evalConcat' a) :& r-runInstrImpl _ SLICE (StkEl (VNat o) _ _ :& StkEl (VNat l) _ _ :& StkEl s _ _ :& r) =-  pure $ starNotesStkEl (VOption (evalSlice o l s)) :& r-runInstrImpl _ ISNAT (StkEl (VInt i) _ _ :& r) =+runInstrImpl _ AnnCAST{} s = pure s+runInstrImpl _ AnnRENAME{} s = pure s+runInstrImpl _ AnnPACK{} ((seValue -> a) :& r) = pure $ StkEl (VBytes $ packValue' a) :& r+runInstrImpl _ AnnUNPACK{} (StkEl (VBytes a) :& r) =+  pure $ StkEl (VOption . rightToMaybe $ runUnpack a) :& r+runInstrImpl _ AnnCONCAT{} (a :& b :& r) = pure $ StkEl (evalConcat (seValue a) (seValue b)) :& r+runInstrImpl _ AnnCONCAT'{} (StkEl (VList a) :& r) = pure $ StkEl (evalConcat' a) :& r+runInstrImpl _ AnnSLICE{} (StkEl (VNat o) :& StkEl (VNat l) :& StkEl s :& r) =+  pure $ StkEl (VOption (evalSlice o l s)) :& r+runInstrImpl _ AnnISNAT{} (StkEl (VInt i) :& r) =   if i < 0-  then pure $ starNotesStkEl (VOption Nothing) :& r-  else pure $ starNotesStkEl (VOption (Just (VNat $ fromInteger i))) :& r-runInstrImpl _ ADD (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Add) l r-runInstrImpl _ SUB (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Sub) l r-runInstrImpl _ SUB_MUTEZ (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @SubMutez) l r-runInstrImpl _ MUL (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Mul) l r-runInstrImpl _ EDIV (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @EDiv) l r-runInstrImpl _ ABS ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Abs) a) :& rest-runInstrImpl _ NEG ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Neg) a) :& rest-runInstrImpl _ LSL (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsl) x s-runInstrImpl _ LSR (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsr) x s-runInstrImpl _ OR (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Or) l r-runInstrImpl _ AND (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @And) l r-runInstrImpl _ XOR (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Xor) l r-runInstrImpl _ NOT ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Not) a) :& rest-runInstrImpl _ COMPARE ((seValue -> l) :& (seValue -> r) :& rest) =-  pure $ starNotesStkEl (T.VInt (compareOp l r)) :& rest-runInstrImpl _ EQ ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Eq') a) :& rest-runInstrImpl _ NEQ ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Neq) a) :& rest-runInstrImpl _ LT ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Lt) a) :& rest-runInstrImpl _ GT ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Gt) a) :& rest-runInstrImpl _ LE ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Le) a) :& rest-runInstrImpl _ GE ((seValue -> a) :& rest) =-  pure $ starNotesStkEl (evalUnaryArithOp (Proxy @Ge) a) :& rest-runInstrImpl _ INT (StkEl a _ _ :& r) =-  pure $ starNotesStkEl (evalToIntOp a) :& r-runInstrImpl runner (VIEW name (_ :: Notes ret))-                    (StkEl (arg :: Value arg) _ _ :& StkEl (VAddress epAddr) addrVa _ :& r) = do+  then pure $ StkEl (VOption Nothing) :& r+  else pure $ StkEl (VOption (Just (VNat $ fromInteger i))) :& r+runInstrImpl _ AnnADD{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Add) l r+runInstrImpl _ AnnSUB{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Sub) l r+runInstrImpl _ AnnSUB_MUTEZ{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @SubMutez) l r+runInstrImpl _ AnnMUL{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Mul) l r+runInstrImpl _ AnnEDIV{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @EDiv) l r+runInstrImpl _ AnnABS{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Abs) a) :& rest+runInstrImpl _ AnnNEG{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Neg) a) :& rest+runInstrImpl _ AnnLSL{} (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsl) x s+runInstrImpl _ AnnLSR{} (x :& s :& rest) = (:& rest) <$> runArithOp (Proxy @Lsr) x s+runInstrImpl _ AnnOR{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Or) l r+runInstrImpl _ AnnAND{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @And) l r+runInstrImpl _ AnnXOR{} (l :& r :& rest) = (:& rest) <$> runArithOp (Proxy @Xor) l r+runInstrImpl _ AnnNOT{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Not) a) :& rest+runInstrImpl _ AnnCOMPARE{} ((seValue -> l) :& (seValue -> r) :& rest) =+  pure $ StkEl (T.VInt (compareOp l r)) :& rest+runInstrImpl _ AnnEQ{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Eq') a) :& rest+runInstrImpl _ AnnNEQ{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Neq) a) :& rest+runInstrImpl _ AnnLT{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Lt) a) :& rest+runInstrImpl _ AnnGT{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Gt) a) :& rest+runInstrImpl _ AnnLE{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Le) a) :& rest+runInstrImpl _ AnnGE{} ((seValue -> a) :& rest) =+  pure $ StkEl (evalUnaryArithOp (Proxy @Ge) a) :& rest+runInstrImpl _ AnnINT{} (StkEl a :& r) =+  pure $ StkEl (evalToIntOp a) :& r+runInstrImpl runner (AnnVIEW (Anns2' _ (_ :: Notes ret)) name)+                    (StkEl (arg :: Value arg) :& StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask   res :: Value ('TOption ret) <- VOption <$> runMaybeT do     let EpAddress addr _ = epAddr@@ -723,11 +676,10 @@     resSt <- lift $       local (mkViewEnv addr viewedContractState) $         runInstrImpl runner vCode $-          starNotesStkEl (VPair (arg, viewedContractStorage)) :& RNil-    let StkEl res _ _ :& RNil = resSt+          StkEl (VPair (arg, viewedContractStorage)) :& RNil+    let StkEl res :& RNil = resSt     return res-  let newAnn = addrVa <> [annQ|contract|]  -- TODO [#704]: ¯\_(ツ)_/¯-  pure (StkEl res newAnn starNotes :& r)+  pure (StkEl res :& r)   where     mkViewEnv :: Address -> ContractState -> ContractEnv -> ContractEnv     mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv@@ -738,15 +690,15 @@       , ceAmount = zeroMutez       , ceContracts       , ceNow, ceMaxSteps, ceVotingPowers, ceChainId, ceOperationHash, ceLevel-      , ceInstrCallStack+      , ceErrorSrcPos, ceMinBlockTime       } -runInstrImpl _ (SELF sepc :: Instr inp out) r = do+runInstrImpl _ (AnnSELF _ sepc :: Instr inp out) r = do   ContractEnv{..} <- ask   case Proxy @out of     (_ :: Proxy ('TContract cp ': s)) -> do-      pure $ starNotesStkEl (VContract ceSelf sepc) :& r-runInstrImpl _ (CONTRACT (nt :: T.Notes a) instrEpName) (StkEl (VAddress epAddr) _ _ :& r) = do+      pure $ StkEl (VContract ceSelf sepc) :& r+runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: T.Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask   let T.EpAddress addr addrEpName = epAddr   let mepName =@@ -756,41 +708,44 @@           (en, DefEpName) -> Just en           _ -> Nothing -  let withNotes v = StkEl v U.noAnn (NTOption U.noAnn $ NTContract U.noAnn nt) :& r-  pure $ withNotes $ case mepName of-    Nothing -> VOption Nothing+  let withNotes v = StkEl v :& r+  withNotes <$> case mepName of+    Nothing -> pure $ VOption Nothing     Just epName ->       case addr of-        KeyAddress{} -> castContract addr epName T.tyImplicitAccountParam-        ContractAddress{} ->+        KeyAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam+        ContractAddress{} -> pure $           case Map.lookup addr ceContracts of             Just (ASSimple _) -> error "Broken addresses map"             Just (ASContract ContractState{..}) ->               castContract addr epName (cParamNotes csContract)             Nothing -> VOption Nothing+        TransactionRollupAddress{} ->+          -- TODO [#838]: support transaction rollups on the emulator+          throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"   where   castContract     :: forall p. T.ParameterScope p     => Address -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))   castContract addr epName param = VOption $ do     -- As we are within Maybe monad, pattern-match failure results in Nothing-    MkEntrypointCallRes na epc <- T.mkEntrypointCall epName param-    Right (Refl, _) <- pure $ matchTypes nt na+    MkEntrypointCallRes (_ :: Notes a') epc <- T.mkEntrypointCall epName param+    Right Refl <- pure $ eqType @a @a'     return $ VContract addr (T.SomeEpc epc) -runInstrImpl _ TRANSFER_TOKENS-  (StkEl p _ _ :& StkEl (VMutez mutez) _ _ :& StkEl contract _ _ :& r) = do+runInstrImpl _ AnnTRANSFER_TOKENS{}+  (StkEl p :& StkEl (VMutez mutez) :& StkEl contract :& r) = do     incrementCounter     globalCounter <- isGlobalCounter <$> getInterpreterState-    pure $ starNotesStkEl (VOp (OpTransferTokens $ TransferTokens p mutez contract globalCounter)) :& r-runInstrImpl _ SET_DELEGATE (StkEl (VOption mbKeyHash) _ _ :& r) = do+    pure $ StkEl (VOp (OpTransferTokens $ TransferTokens p mutez contract globalCounter)) :& r+runInstrImpl _ AnnSET_DELEGATE{} (StkEl (VOption mbKeyHash) :& r) = do   incrementCounter   globalCounter <- isGlobalCounter <$> getInterpreterState   case mbKeyHash of-    Just (VKeyHash k) -> pure $ starNotesStkEl (VOp (OpSetDelegate $ SetDelegate (Just k) globalCounter)) :& r-    Nothing -> pure $ starNotesStkEl (VOp (OpSetDelegate $ SetDelegate Nothing globalCounter)) :& r-runInstrImpl _ (CREATE_CONTRACT contract)-  (StkEl (VOption mbKeyHash) _ _ :& StkEl (VMutez m) _ _ :& StkEl g _ _ :& r) = do+    Just (VKeyHash k) -> pure $ StkEl (VOp (OpSetDelegate $ SetDelegate (Just k) globalCounter)) :& r+    Nothing -> pure $ StkEl (VOp (OpSetDelegate $ SetDelegate Nothing globalCounter)) :& r+runInstrImpl _ (AnnCREATE_CONTRACT _ contract)+  (StkEl (VOption mbKeyHash) :& StkEl (VMutez m) :& StkEl g :& r) = do   originator <- ceSelf <$> ask   opHash <- ceOperationHash <$> ask   incrementCounter@@ -800,101 +755,104 @@           Just hash -> mkContractAddress hash globalCounter           Nothing ->             mkContractAddress-              (mkOriginationOperationHash (createOrigOp originator mbKeyHash m contract g globalCounter))+              (mkOriginationOperationHash (createOrigOp originator Nothing mbKeyHash m contract g globalCounter))               -- If opHash is Nothing it means that interpreter is running in some kind of test               -- context, therefore we generate dummy contract address with its own origination               -- operation.               globalCounter   let resEpAddr = EpAddress resAddr DefEpName   let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g contract globalCounter-  pure $ starNotesStkEl (VOp (OpCreateContract resOp))-      :& starNotesStkEl (VAddress resEpAddr)+  pure $ StkEl (VOp (OpCreateContract resOp))+      :& StkEl (VAddress resEpAddr)       :& r-runInstrImpl _ IMPLICIT_ACCOUNT (StkEl (VKeyHash k) _ _ :& r) =-  pure $ (starNotesStkEl (VContract (KeyAddress k) sepcPrimitive)) :& r-runInstrImpl _ NOW r = do+runInstrImpl _ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash k) :& r) =+  pure $ (StkEl (VContract (KeyAddress k) sepcPrimitive)) :& r+runInstrImpl _ AnnNOW{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VTimestamp ceNow) :& r-runInstrImpl _ AMOUNT r = do+  pure $ StkEl (VTimestamp ceNow) :& r+runInstrImpl _ AnnAMOUNT{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VMutez ceAmount) :& r-runInstrImpl _ BALANCE r = do+  pure $ StkEl (VMutez ceAmount) :& r+runInstrImpl _ AnnBALANCE{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VMutez ceBalance) :& r-runInstrImpl _ VOTING_POWER (StkEl (VKeyHash k) _ _ :& r) = do+  pure $ StkEl (VMutez ceBalance) :& r+runInstrImpl _ AnnVOTING_POWER{} (StkEl (VKeyHash k) :& r) = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VNat $ vpPick k ceVotingPowers) :& r-runInstrImpl _ TOTAL_VOTING_POWER r = do+  pure $ StkEl (VNat $ vpPick k ceVotingPowers) :& r+runInstrImpl _ AnnTOTAL_VOTING_POWER{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VNat $ vpTotal ceVotingPowers) :& r-runInstrImpl _ CHECK_SIGNATURE-  (StkEl (VKey k) _ _ :& StkEl (VSignature v) _ _ :& StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBool $ checkSignature k v b) :& r-runInstrImpl _ SHA256 (StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBytes $ sha256 b) :& r-runInstrImpl _ SHA512 (StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBytes $ sha512 b) :& r-runInstrImpl _ BLAKE2B (StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBytes $ blake2b b) :& r-runInstrImpl _ SHA3 (StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBytes $ sha3 b) :& r-runInstrImpl _ KECCAK (StkEl (VBytes b) _ _ :& r) =-  pure $ starNotesStkEl (VBytes $ keccak b) :& r-runInstrImpl _ HASH_KEY (StkEl (VKey k) _ _ :& r) =-  pure $ starNotesStkEl (VKeyHash $ hashKey k) :& r-runInstrImpl _ PAIRING_CHECK (StkEl (VList pairs) _ _ :& r) = do+  pure $ StkEl (VNat $ vpTotal ceVotingPowers) :& r+runInstrImpl _ AnnCHECK_SIGNATURE{}+  (StkEl (VKey k) :& StkEl (VSignature v) :& StkEl (VBytes b) :& r) =+  pure $ StkEl (VBool $ checkSignature k v b) :& r+runInstrImpl _ AnnSHA256{} (StkEl (VBytes b) :& r) =+  pure $ StkEl (VBytes $ sha256 b) :& r+runInstrImpl _ AnnSHA512{} (StkEl (VBytes b) :& r) =+  pure $ StkEl (VBytes $ sha512 b) :& r+runInstrImpl _ AnnBLAKE2B{} (StkEl (VBytes b) :& r) =+  pure $ StkEl (VBytes $ blake2b b) :& r+runInstrImpl _ AnnSHA3{} (StkEl (VBytes b) :& r) =+  pure $ StkEl (VBytes $ sha3 b) :& r+runInstrImpl _ AnnKECCAK{} (StkEl (VBytes b) :& r) =+  pure $ StkEl (VBytes $ keccak b) :& r+runInstrImpl _ AnnHASH_KEY{} (StkEl (VKey k) :& r) =+  pure $ StkEl (VKeyHash $ hashKey k) :& r+runInstrImpl _ AnnPAIRING_CHECK{} (StkEl (VList pairs) :& r) = do   let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]-  pure $ starNotesStkEl (VBool $ checkPairing pairs') :& r-runInstrImpl _ SOURCE r = do+  pure $ StkEl (VBool $ checkPairing pairs') :& r+runInstrImpl _ AnnSOURCE{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VAddress $ EpAddress ceSource DefEpName) :& r-runInstrImpl _ SENDER r = do+  pure $ StkEl (VAddress $ EpAddress ceSource DefEpName) :& r+runInstrImpl _ AnnSENDER{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VAddress $ EpAddress ceSender DefEpName) :& r-runInstrImpl _ ADDRESS (StkEl (VContract a sepc) _ _ :& r) =-  pure $ starNotesStkEl (VAddress $ EpAddress a (sepcName sepc)) :& r-runInstrImpl _ CHAIN_ID r = do+  pure $ StkEl (VAddress $ EpAddress ceSender DefEpName) :& r+runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =+  pure $ StkEl (VAddress $ EpAddress a (sepcName sepc)) :& r+runInstrImpl _ AnnCHAIN_ID{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VChainId ceChainId) :& r-runInstrImpl _ LEVEL r = do+  pure $ StkEl (VChainId ceChainId) :& r+runInstrImpl _ AnnLEVEL{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VNat ceLevel) :& r-runInstrImpl _ SELF_ADDRESS r = do+  pure $ StkEl (VNat ceLevel) :& r+runInstrImpl _ AnnSELF_ADDRESS{} r = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VAddress $ EpAddress ceSelf DefEpName) :& r-runInstrImpl _ TICKET (StkEl dat _ _ :& StkEl (VNat am) _ _ :& r) = do+  pure $ StkEl (VAddress $ EpAddress ceSelf DefEpName) :& r+runInstrImpl _ AnnTICKET{} (StkEl dat :& StkEl (VNat am) :& r) = do   ContractEnv{..} <- ask-  pure $ starNotesStkEl (VTicket ceSelf dat am) :& r-runInstrImpl _ READ_TICKET (te@(StkEl (VTicket addr dat am) _ _) :& r) = do+  pure $ StkEl (VTicket ceSelf dat am) :& r+runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do   pure $-    starNotesStkEl+    StkEl       (VPair (VAddress (EpAddress addr DefEpName), (VPair (dat, VNat am))))     :& te :& r-runInstrImpl _ SPLIT_TICKET-    (StkEl tv@(VTicket addr dat am) _ _ :&-     StkEl (VPair (VNat am1, VNat am2)) _ _ :& r) = do+runInstrImpl _ AnnSPLIT_TICKET{}+    (StkEl tv@(VTicket addr dat am) :&+     StkEl (VPair (VNat am1, VNat am2)) :& r) = do   let result = withValueTypeSanity tv $ VOption do         guard (am1 + am2 == am)         return $ VPair (VTicket addr dat am1, VTicket addr dat am2)-  pure $ starNotesStkEl result :& r-runInstrImpl _ JOIN_TICKETS-  (StkEl (VPair (tv1@(VTicket addr1 dat1 am1), VTicket addr2 dat2 am2)) _ _ :& r) = do+  pure $ StkEl result :& r+runInstrImpl _ AnnJOIN_TICKETS{}+  (StkEl (VPair (tv1@(VTicket addr1 dat1 am1), VTicket addr2 dat2 am2)) :& r) = do   let result = withValueTypeSanity tv1 $ VOption do         guard (addr1 == addr2)         guard (dat1 == dat2)         return $ VTicket addr1 dat1 (am1 + am2)-  pure $ starNotesStkEl result :& r-runInstrImpl _ OPEN_CHEST-  (StkEl (VChestKey ck) _ _ :& StkEl (VChest c) _ _ :& StkEl (VNat nat) _ _ :& r) = do+  pure $ StkEl result :& r+runInstrImpl _ AnnOPEN_CHEST{}+  (StkEl (VChestKey ck) :& StkEl (VChest c) :& StkEl (VNat nat) :& r) = do   let result = case mkTLTime nat of         Right time -> case openChest c ck time of           Correct bytes -> VOr (Left (VBytes bytes))           BogusOpening  -> VOr (Right (VBool True))           BogusCipher   -> VOr (Right (VBool False))         Left _ -> VOr (Right (VBool True))-  pure $ starNotesStkEl result :& r-runInstrImpl _ (SAPLING_EMPTY_STATE _) _ = throwMichelson $ MichelsonUnsupported "SAPLING_EMPTY_STATE"-runInstrImpl _ SAPLING_VERIFY_UPDATE _ = throwMichelson $ MichelsonUnsupported "SAPLING_VERIFY_UPDATE"+  pure $ StkEl result :& r+runInstrImpl _ AnnSAPLING_EMPTY_STATE{} _ = throwMichelson $ MichelsonUnsupported "SAPLING_EMPTY_STATE"+runInstrImpl _ AnnSAPLING_VERIFY_UPDATE{} _ = throwMichelson $ MichelsonUnsupported "SAPLING_VERIFY_UPDATE"+runInstrImpl _ AnnMIN_BLOCK_TIME{} r = do+  ContractEnv{..} <- ask+  pure $ StkEl (VNat ceMinBlockTime) :& r  -- | Evaluates an arithmetic operation and either fails or proceeds. runArithOp@@ -905,7 +863,7 @@   -> monad (StkEl (ArithRes aop n m)) runArithOp op l r = case evalOp op (seValue l) (seValue r) of   Left  err -> throwMichelson $ MichelsonArithError err-  Right res -> pure $ starNotesStkEl res+  Right res -> pure $ StkEl res  -- | Unpacks given raw data into a typed value. runUnpack@@ -921,13 +879,14 @@ createOrigOp   :: (ParameterScope param, StorageScope store)   => Address+  -> Maybe Alias   -> Maybe (T.Value 'T.TKeyHash)   -> Mutez   -> Contract param store   -> Value' Instr store   -> GlobalCounter   -> OriginationOperation-createOrigOp originator mbDelegate bal contract storage counter =+createOrigOp originator mbAlias mbDelegate bal contract storage counter =   OriginationOperation     { ooOriginator = originator     , ooDelegate = unwrapMbKeyHash mbDelegate@@ -935,6 +894,7 @@     , ooStorage = storage     , ooContract = contract     , ooCounter = counter+    , ooAlias = mbAlias     }  unwrapMbKeyHash :: Maybe (T.Value 'T.TKeyHash) -> Maybe KeyHash@@ -991,11 +951,12 @@   -- Otherwise, assign IDs only to bigmaps that don't have one yet.   -> Value t -> m (Value t) assignBigMapIds overwriteExistingId =-  dfsTraverseValue \case-    VBigMap existingId vBigMap | overwriteExistingId || isNothing existingId -> do-      bigMapId <- bigMapCounter <<+= 1-      pure $ VBigMap (Just bigMapId) vBigMap-    v -> pure v+  dfsTraverseValue def{ dsValueStep = \case+      VBigMap existingId vBigMap | overwriteExistingId || isNothing existingId -> do+        bigMapId <- bigMapCounter <<+= 1+        pure $ VBigMap (Just bigMapId) vBigMap+      v -> pure v+    }  incrementCounter :: (InterpreterStateMonad m) => m () incrementCounter = modifyInterpreterState $ \iState ->

@@ -28,7 +28,7 @@ import Fmt (pretty)  import Morley.Micheline.Binary (eitherDecodeExpression)-import Morley.Micheline.Class (FromExpression(..))+import Morley.Micheline.Class (FromExpression, fromExpression) import Morley.Michelson.Typed (UnpackedValScope) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Untyped

@@ -1,32 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA--module Morley.Michelson.Let-  ( LetType (..)-  , LetValue (..)-  ) where--import Data.Aeson.TH (deriveJSON)-import Data.Text qualified as T--import Morley.Michelson.Macro (ParsedOp)-import Morley.Michelson.Untyped (Ty, Value')-import Morley.Util.Aeson---- | A programmer-defined constant-data LetValue = LetValue-  { lvName :: T.Text-  , lvSig :: Ty-  , lvVal :: (Value' ParsedOp)-  } deriving stock (Eq, Show)--{-# DEPRECATED LetValue, LetType "Let macros are deprecated" #-}---- | A programmer-defined type-synonym-data LetType = LetType-  { ltName :: T.Text-  , ltSig :: Ty-  } deriving stock (Eq, Show)--deriveJSON morleyAesonOptions ''LetValue-deriveJSON morleyAesonOptions ''LetType

@@ -1,9 +1,6 @@ -- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA --- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations #-}- module Morley.Michelson.Macro   (   -- * Macros types@@ -11,7 +8,6 @@   , PairStruct (..)   , UnpairStruct (..)   , Macro (..)-  , LetMacro (..)    -- * Morley Parsed value types   , ParsedValue@@ -41,29 +37,13 @@  import Data.Aeson.TH (deriveJSON) import Data.Data (Data(..))-import Data.Text qualified as T import Fmt (Buildable(build), GenericBuildable(..), (+|), (|+))  import Morley.Michelson.ErrorPos import Morley.Michelson.Printer (RenderDoc(..)) import Morley.Michelson.Untyped import Morley.Util.Aeson-import Morley.Util.Generic-import Morley.Util.Positive --- | A programmer-defined macro-data LetMacro = LetMacro-  { lmName :: T.Text-  , lmSig :: StackFn-  , lmExpr :: [ParsedOp]-  }-  deriving stock (Eq, Show, Data, Generic)-  deriving Buildable via GenericBuildable LetMacro--{-# DEPRECATED LetMacro "Let macros are deprecated" #-}--instance NFData LetMacro- data PairStruct   = F FieldAnn   | P PairStruct PairStruct@@ -93,18 +73,16 @@ data ParsedOp   = Prim ParsedInstr SrcPos -- ^ Primitive Michelson instruction   | Mac Macro        SrcPos -- ^ Built-in Michelson macro defined by the specification-  | LMac LetMacro    SrcPos -- ^ User-defined macro with instructions to be inlined   | Seq [ParsedOp]   SrcPos -- ^ A sequence of instructions   deriving stock (Eq, Show, Data, Generic)  instance RenderDoc ParsedOp where-  renderDoc pn parsedOp = renderDoc pn $ expand [] parsedOp+  renderDoc pn parsedOp = renderDoc pn $ expand parsedOp  instance Buildable ParsedOp where   build = \case     Prim parseInstr _ -> "<Prim: "+|parseInstr|+">"     Mac macro _       -> "<Mac: "+|macro|+">"-    LMac letMacro _   -> "<LMac: "+|letMacro|+">"     Seq parsedOps _   -> "<Seq: "+|parsedOps|+">"  instance NFData ParsedOp@@ -119,21 +97,9 @@  type ParsedValue = Value' ParsedOp -{-# DEPRECATED-  CASE, TAG, ACCESS, SET, CONSTRUCT, VIEW_, VOID-  "Morley-specific macros are deprecated" #-}- -- | Built-in Michelson Macros defined by the specification data Macro-  = CASE (NonEmpty [ParsedOp])-  | TAG Natural (NonEmpty Ty)-  | ACCESS Natural Positive-  | SET Natural Positive-  | CONSTRUCT (NonEmpty [ParsedOp])-    -- A1/TZIP4 VIEW, exists for historical reasons-  | VIEW_ [ParsedOp]-  | VOID [ParsedOp]-  | CMP ParsedInstr VarAnn+  = CMP ParsedInstr VarAnn   | IFX ParsedInstr [ParsedOp] [ParsedOp]   | IFCMP ParsedInstr VarAnn [ParsedOp] [ParsedOp]   | FAIL@@ -159,13 +125,6 @@  instance Buildable Macro where   build = \case-    TAG idx ty -> "<TAG: #"+|idx|+" from "+|toList ty|+""-    CASE parsedInstrs -> "<CASE: "+|toList parsedInstrs|+">"-    ACCESS idx size -> "<ACCESS: #"+|idx|+"/"+|size|+""-    SET idx size -> "<SET: #"+|idx|+"/"+|size|+""-    CONSTRUCT parsedInstrs -> "<CONSTRUCT: "+|toList parsedInstrs|+">"-    VIEW_ code -> "<VIEW_: "+|code|+">"-    VOID code -> "<VOID: "+|code|+">"     CMP parsedInstr carAnn -> "<CMP: "+|parsedInstr|+", "+|carAnn|+">"     IFX parsedInstr parsedOps1 parsedOps2 -> "<IFX: "+|parsedInstr|+", "+|parsedOps1|+", "+|parsedOps2|+">"     IFCMP parsedInstr varAnn parsedOps1 parsedOps2 -> "<IFCMP: "+|parsedInstr|+", "+|varAnn|+", "+|parsedOps1|+", "+|parsedOps2|+">"@@ -192,7 +151,7 @@ instance NFData Macro  expandList :: [ParsedOp] -> [ExpandedOp]-expandList = fmap (expand [])+expandList = fmap expand  expandView :: View' ParsedOp -> View expandView v = v{ viewCode = expandList (viewCode v) }@@ -218,13 +177,13 @@   ValueLambda opList ->     maybe ValueNil ValueLambda $     nonEmpty (expandList $ toList opList)-  x -> fmap (expand []) x+  x -> fmap expand x  expandElt :: Elt ParsedOp -> Elt ExpandedOp expandElt (Elt l r) = Elt (expandValue l) (expandValue r) -expand :: LetCallStack -> ParsedOp -> ExpandedOp-expand cs = let ics pos = InstrCallStack cs pos in \case+expand :: ParsedOp -> ExpandedOp+expand = let ics pos = ErrorSrcPos pos in \case   -- We handle this case specially, because it's essentially just PAIR.   -- It's needed because we have a hack in parser: we parse PAIR as PAPAIR.   -- We need to do something better eventually.@@ -236,55 +195,25 @@   -- As the above comment says, we need to do something better eventually   -- (e. g. to avoid `error` usage inside `expandMacro`).   (Mac (DIIP n ops) pos) ->-    WithSrcEx (ics pos) $ PrimEx (DIPN n (expand cs <$> ops))+    WithSrcEx (ics pos) $ PrimEx (DIPN n (expand <$> ops))   -- Similarly to above, DUUP is now always represented as a single instruction.   (Mac (DUUP n v) pos) ->     WithSrcEx (ics pos) $ PrimEx $ DUPN v n   (Mac m pos) -> WithSrcEx (ics pos) $ SeqEx $ expandMacro (ics pos) m-  (Prim i pos) -> WithSrcEx (ics pos) $ PrimEx $ expand cs <$> i-  (Seq s pos) -> WithSrcEx (ics pos) $ SeqEx $ expand cs <$> s-  (LMac l pos) -> expandLetMac l-    where-      expandLetMac :: LetMacro -> ExpandedOp-      expandLetMac LetMacro {..} =-        let newCS = LetName lmName : cs in-        let ics' = InstrCallStack newCS pos in-        WithSrcEx ics' $ PrimEx . EXT . FN lmName lmSig $ expand newCS <$> lmExpr+  (Prim i pos) -> WithSrcEx (ics pos) $ PrimEx $ expand <$> i+  (Seq s pos) -> WithSrcEx (ics pos) $ SeqEx $ expand <$> s -expandMacro :: InstrCallStack -> Macro -> [ExpandedOp]-expandMacro p@InstrCallStack{icsCallStack=cs,icsSrcPos=macroPos} = \case-  VIEW_ a            -> [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn)-                        , PrimEx (DIP $ oprimEx $ DUPN noAnn 2)-                        , PrimEx $ PAIR noAnn noAnn noAnn noAnn ] ++-                        (expand cs <$> a) ++-                        [ PrimEx (DIP [PrimEx $ AMOUNT noAnn])-                        , PrimEx $ TRANSFER_TOKENS noAnn-                        , PrimEx $ NIL noAnn noAnn (Ty TOperation noAnn)-                        , PrimEx $ SWAP-                        , PrimEx $ CONS noAnn-                        , PrimEx $ PAIR noAnn noAnn noAnn noAnn-                        ]-  VOID a             -> [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn)-                        , PrimEx SWAP-                        , PrimEx $ DIP $ expand cs <$> a-                        , PrimEx SWAP-                        , PrimEx $ EXEC noAnn-                        , PrimEx FAILWITH-                        ]-  CASE ops           -> expandCase (map (expand cs) <$> ops)-  TAG idx uty        -> expandTag idx uty-  ACCESS idx size    -> expandAccess idx size-  SET idx size       -> expandSet idx size-  CONSTRUCT ops      -> expandConstruct (map (expand cs) <$> ops)+expandMacro :: ErrorSrcPos -> Macro -> [ExpandedOp]+expandMacro p@ErrorSrcPos{unErrorSrcPos=macroPos} = \case   CMP i v            -> [PrimEx (COMPARE v), xo i]   IFX i bt bf        -> [xo i, PrimEx $ IF (xp bt) (xp bf)]-  IFCMP i v bt bf    -> PrimEx <$> [COMPARE v, expand cs <$> i, IF (xp bt) (xp bf)]+  IFCMP i v bt bf    -> PrimEx <$> [COMPARE v, expand <$> i, IF (xp bt) (xp bf)]   IF_SOME bt bf      -> [PrimEx (IF_NONE (xp bf) (xp bt))]   IF_RIGHT bt bf     -> [PrimEx (IF_LEFT (xp bf) (xp bt))]   FAIL               -> PrimEx <$> [UNIT noAnn noAnn, FAILWITH]   ASSERT             -> oprimEx $ IF [] (expandMacro p FAIL)-  ASSERTX i          -> [expand cs $ mac $ IFX i [] [mac FAIL]]-  ASSERT_CMP i       -> [expand cs $ mac $ IFCMP i noAnn [] [mac FAIL]]+  ASSERTX i          -> [expand $ mac $ IFX i [] [mac FAIL]]+  ASSERT_CMP i       -> [expand $ mac $ IFCMP i noAnn [] [mac FAIL]]   ASSERT_NONE        -> oprimEx $ IF_NONE [] (expandMacro p FAIL)   ASSERT_SOME        -> oprimEx $ IF_NONE (expandMacro p FAIL) []   ASSERT_LEFT        -> oprimEx $ IF_LEFT [] (expandMacro p FAIL)@@ -303,14 +232,14 @@   where     mac = flip Mac macroPos     oprimEx = one . PrimEx-    xo = PrimEx . fmap (expand cs)-    xp = fmap (expand cs)+    xo = PrimEx . fmap expand+    xp = fmap expand  -- | The macro expansion rules below were taken from: https://tezos.gitlab.io/active/michelson.html#syntactic-conveniences -- -- The correctness of type-annotation expansion is currently untested, as these -- expansions are not explicitly documented in the Michelson Specification.-expandPapair :: InstrCallStack -> PairStruct -> TypeAnn -> VarAnn -> [ExpandedOp]+expandPapair :: ErrorSrcPos -> PairStruct -> TypeAnn -> VarAnn -> [ExpandedOp] expandPapair ics ps t v = case ps of   P (F a) (F b) -> [PrimEx $ PAIR t v a b] @@ -332,7 +261,7 @@   F _           -> []  -- | The macro expansion rules below were taken from: https://tezos.gitlab.io/active/michelson.html#syntactic-conveniences-expandUnpapair :: InstrCallStack -> UnpairStruct -> [ExpandedOp]+expandUnpapair :: ErrorSrcPos -> UnpairStruct -> [ExpandedOp] expandUnpapair ics = \case   UP UF UF ->     [ PrimEx (UNPAIR noAnn noAnn noAnn noAnn) ]@@ -359,7 +288,7 @@   -- but if it accidentally happened let's just do nothing.   UF -> [] -expandCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp]+expandCadr :: ErrorSrcPos -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp] expandCadr ics cs v f = case cs of   []    -> []   [A]  -> [PrimEx $ CAR v f]@@ -376,7 +305,7 @@ pairNoAnn :: VarAnn -> InstrAbstract op pairNoAnn v = PAIR noAnn v [annQ|@|] [annQ|@|] -expandSetCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp]+expandSetCadr :: ErrorSrcPos -> [CadrStruct] -> VarAnn -> FieldAnn -> [ExpandedOp] expandSetCadr ics cs v f = PrimEx <$> case cs of   []    -> []   [A]   -> [DUP noAnn, CAR noAnn f, DROP,@@ -388,71 +317,14 @@   A:css -> [DUP noAnn, DIP (PrimEx carNoAnn : expandMacro ics (SET_CADR css noAnn f)), cdrNoAnn, SWAP, pairNoAnn v]   D:css -> [DUP noAnn, DIP (PrimEx cdrNoAnn : expandMacro ics (SET_CADR css noAnn f)), carNoAnn, pairNoAnn v] -expandMapCadr :: InstrCallStack -> [CadrStruct] -> VarAnn -> FieldAnn -> [ParsedOp] -> [ExpandedOp]-expandMapCadr ics@InstrCallStack{icsCallStack=cls} cs v f ops = case cs of+expandMapCadr :: ErrorSrcPos -> [CadrStruct] -> VarAnn -> FieldAnn -> [ParsedOp] -> [ExpandedOp]+expandMapCadr ics cs v f ops = case cs of   []    -> []-  [A]   -> PrimEx <$> [DUP noAnn, cdrNoAnn, DIP [PrimEx $ CAR noAnn f, SeqEx (expand cls <$> ops)], SWAP, PAIR noAnn v f [annQ|@|]]-  [D]   -> concat [PrimEx <$> [DUP noAnn, CDR noAnn f], [SeqEx (expand cls <$> ops)], PrimEx <$> [SWAP, carNoAnn, PAIR noAnn v [annQ|@|] f]]+  [A]   -> PrimEx <$> [DUP noAnn, cdrNoAnn, DIP [PrimEx $ CAR noAnn f, SeqEx (expand <$> ops)], SWAP, PAIR noAnn v f [annQ|@|]]+  [D]   -> concat [PrimEx <$> [DUP noAnn, CDR noAnn f], [SeqEx (expand <$> ops)], PrimEx <$> [SWAP, carNoAnn, PAIR noAnn v [annQ|@|] f]]   A:css -> PrimEx <$> [DUP noAnn, DIP (PrimEx carNoAnn : expandMacro ics (MAP_CADR css noAnn f ops)), cdrNoAnn, SWAP, pairNoAnn v]   D:css -> PrimEx <$> [DUP noAnn, DIP (PrimEx cdrNoAnn : expandMacro ics (MAP_CADR css noAnn f ops)), carNoAnn, pairNoAnn v] -expandCase :: NonEmpty [ExpandedOp] -> [ExpandedOp]-expandCase = mkGenericTree (\_ l r -> one . PrimEx $ IF_LEFT l r)--expandTag :: Natural -> NonEmpty Ty -> [ExpandedOp]-expandTag idx unionTy =-  reverse . fst $ mkGenericTree merge (([], ) <$> unionTy)-  where-    merge i (li, lt) (ri, rt) =-      let ty = Ty (TOr noAnn noAnn lt rt) noAnn-      in if idx < i-          then (PrimEx (LEFT noAnn noAnn noAnn noAnn rt) : li, ty)-          else (PrimEx (RIGHT noAnn noAnn noAnn noAnn lt) : ri, ty)--expandAccess :: Natural -> Positive -> [ExpandedOp]-expandAccess idx size =-  mkGenericTree merge (replicateNE size [])-  where-    merge i li ri =-      if idx < i-        then PrimEx (CAR noAnn noAnn) : li-        else PrimEx (CDR noAnn noAnn) : ri--expandSet :: Natural -> Positive -> [ExpandedOp]-expandSet idx size =-  PrimEx <$>-  appEndo (mkGenericTree merge (replicateNE size base)) []-  where-    base = pre $ DIP [PrimEx DROP]-    merge i li ri = mconcat $-      if idx < i-        then [ pre $ DIP-                 (map PrimEx [DUP n, DIP [PrimEx $ CDR n n], CAR n n])-             , li-             , pre $ PAIR n n n n-             ]-        else [ pre $ DIP-                 (map PrimEx [DUP n, DIP [PrimEx $ CAR n n], CDR n n])-             , ri-             , pre $ SWAP-             , pre $ PAIR n n n n-             ]-    pre e = Endo (e :)-    n = noAnn--expandConstruct :: NonEmpty [ExpandedOp] -> [ExpandedOp]-expandConstruct ctors =-  appEndo (mkGenericTree merge $ map toBase ctors) []-  where-    toBase ops = Endo (ops ++)-    merge _ li ri =-      mconcat-        [ li-        , pre . PrimEx $ DIP (appEndo ri [])-        , pre . PrimEx $ PAIR noAnn noAnn noAnn noAnn-        ]-    pre e = Endo (e :)- mapPairLeaves :: [FieldAnn] -> PairStruct -> PairStruct mapPairLeaves fs p = evalState (pairLeavesST p) fs @@ -469,9 +341,11 @@       getLeaf (a:as) = (a, as)       getLeaf _      = (noAnn, []) -deriveJSON morleyAesonOptions ''ParsedOp-deriveJSON morleyAesonOptions ''LetMacro deriveJSON morleyAesonOptions ''PairStruct deriveJSON morleyAesonOptions ''UnpairStruct deriveJSON morleyAesonOptions ''CadrStruct-deriveJSON morleyAesonOptions ''Macro++$(mconcat+  [ deriveJSON morleyAesonOptions ''Macro+  , deriveJSON morleyAesonOptions ''ParsedOp+  ])

@@ -7,9 +7,6 @@ {-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -Wno-overlapping-patterns #-} --- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations #-}- -- | Optimizer for typed instructions. -- -- It's quite experimental and incomplete.@@ -122,7 +119,6 @@   flattenSeqLHS     `orSimpleRule` removeNesting     `orSimpleRule` removeExtStackType-    `orSimpleRule` flattenFn     `orSimpleRule` dipDrop2swapDrop     `orSimpleRule` ifNopNop2Drop     `orSimpleRule` nopIsNeutralForSeq@@ -164,11 +160,6 @@   Ext (STACKTYPE{}) -> Just Nop   _                 -> Nothing -flattenFn :: Rule-flattenFn = Rule $ \case-  Fn _ _ i -> Just i-  _        -> Nothing- dipDrop2swapDrop :: Rule dipDrop2swapDrop = Rule $ \case   DIP DROP -> Just $ SWAP :# DROP@@ -564,7 +555,7 @@   LE               :# DROP :# c -> Just $ DROP :# c   GE               :# DROP :# c -> Just $ DROP :# c   INT              :# DROP :# c -> Just $ DROP :# c-  CONTRACT _ _     :# DROP :# c -> Just $ DROP :# c+  CONTRACT _       :# DROP :# c -> Just $ DROP :# c   SET_DELEGATE     :# DROP :# c -> Just $ DROP :# c   IMPLICIT_ACCOUNT :# DROP :# c -> Just $ DROP :# c   VOTING_POWER     :# DROP :# c -> Just $ DROP :# c@@ -601,7 +592,7 @@   LE               :# DROP      -> Just DROP   GE               :# DROP      -> Just DROP   INT              :# DROP      -> Just DROP-  CONTRACT _ _     :# DROP      -> Just DROP+  CONTRACT _       :# DROP      -> Just DROP   SET_DELEGATE     :# DROP      -> Just DROP   IMPLICIT_ACCOUNT :# DROP      -> Just DROP   VOTING_POWER     :# DROP      -> Just DROP

@@ -1,16 +1,12 @@ -- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA --- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations -Wno-redundant-constraints #-}- module Morley.Michelson.Parser   ( -- * Main parser type     Parser    -- * Parsers   , program-  , programExt   , value    -- * Errors@@ -30,13 +26,11 @@   , codeEntry   , ops   , type_-  , letInner-  , letType   , stringLiteral   , bytesLiteral   , intLiteral   , parsedOp-  , printComment+  , cbParameterBare    -- * Quoters   , utypeQ@@ -49,24 +43,20 @@  import Prelude hiding (try) -import Data.Default (Default(..)) import Fmt (pretty, (+|), (|+)) import Language.Haskell.TH qualified as TH import Language.Haskell.TH.Quote qualified as TH import Language.Haskell.TH.Syntax qualified as TH import Text.Megaparsec-  (Parsec, choice, customFailure, eitherP, eof, errorBundlePretty, getSourcePos, hidden, lookAhead,-  parse, sepEndBy, try)+  (Parsec, choice, eitherP, eof, errorBundlePretty, getSourcePos, hidden, lookAhead, parse,+  sepEndBy, try) import Text.Megaparsec.Pos (SourcePos(..), unPos)  import Morley.Michelson.ErrorPos (SrcPos(..), mkPos) import Morley.Michelson.Macro (Macro(..), ParsedInstr, ParsedOp(..), ParsedValue, expandValue)-import Morley.Michelson.Parser.Annotations (noteF) import Morley.Michelson.Parser.Common import Morley.Michelson.Parser.Error-import Morley.Michelson.Parser.Ext import Morley.Michelson.Parser.Instr-import Morley.Michelson.Parser.Let import Morley.Michelson.Parser.Lexer import Morley.Michelson.Parser.Macro import Morley.Michelson.Parser.Type@@ -81,13 +71,12 @@ ----------------------------------------------------------------------------  -- | Parse with empty environment-parseNoEnv ::-     Default le-  => Parser' le a+parseNoEnv+  :: Parser a   -> MichelsonSource   -> Text   -> Either (ParseErrorBundle Text CustomParserException) a-parseNoEnv p src = parse (runReaderT p def <* eof) (pretty src)+parseNoEnv p src = parse (p <* eof) (pretty src)  ------------------------------------------------------------------------------- -- Parsers@@ -98,42 +87,24 @@  -- | Michelson contract program :: Parsec CustomParserException Text (Contract' ParsedOp)-program = runReaderT (programInner @()) def <* eof--programInner-  :: forall env. (Default env)-  => Parser env (Contract' ParsedOp)-programInner = do-  mSpace-  env <- fromMaybe def <$> (optional (letBlock parsedOp))-  local (const env) contract+program = programInner <* eof --- TODO [#712]: Remove this next major release--- | Michelson contract with let definitions-programExt :: Parsec CustomParserException Text (Contract' ParsedOp)-programExt = runReaderT (programInner @LetEnv) def <* eof+programInner :: Parser (Contract' ParsedOp)+programInner = mSpace *> contract -cbParameter :: Parser le ParameterType+cbParameter :: Parser ParameterType cbParameter = symbol1 "parameter" *> cbParameterBare -cbParameterBare :: Parser le ParameterType-cbParameterBare = do-  prefixRootAnn <- optional noteF-  (inTypeRootAnn, t) <- field-  rootAnn <- case (prefixRootAnn, inTypeRootAnn) of-    (Just a, b) | a == noAnn && b == noAnn -> pure noAnn-    (Just a, b) | b == noAnn -> pure a-    (Nothing, b) -> pure b-    (Just _, _) -> customFailure MultiRootAnnotationException-  pure $ ParameterType t rootAnn+cbParameterBare :: Parser ParameterType+cbParameterBare = uncurry ParameterType . swap <$> field -cbStorage :: Parser le Ty+cbStorage :: Parser Ty cbStorage = symbol1 "storage" *> type_ -cbCode :: Parser le [ParsedOp]+cbCode :: Parser [ParsedOp] cbCode = symbol "code" *> codeEntry -cbView :: Parser le (View' ParsedOp)+cbView :: Parser (View' ParsedOp) cbView = do   symbol "view"   viewName <- viewName_@@ -142,7 +113,7 @@   viewCode <- ops   return View{..} -contractBlock :: Parser le (ContractBlock ParsedOp)+contractBlock :: Parser (ContractBlock ParsedOp) contractBlock = choice   [ (CBParam <$> cbParameter)   , (CBStorage <$> cbStorage)@@ -151,7 +122,7 @@   ]  -- | This ensures that the error message will point to the correct line.-ensureNotDuplicate :: [ContractBlock ParsedOp] -> ContractBlock ParsedOp -> Parser le ()+ensureNotDuplicate :: [ContractBlock ParsedOp] -> ContractBlock ParsedOp -> Parser () ensureNotDuplicate blocks result =   let     failDuplicateField a = fail $ "Duplicate contract field: " +| a |+ ""@@ -165,7 +136,7 @@       (_, []) -> pure ()  -- | Michelson contract-contract :: Parser le (Contract' ParsedOp)+contract :: Parser (Contract' ParsedOp) contract = do   mSpace   result <- braces contractTuple <|> contractTuple@@ -186,7 +157,7 @@ -- Value ------------------ -value :: Parser le ParsedValue+value :: Parser ParsedValue value = value' parsedOp  -- | Parse untyped value from text which comes from something that is@@ -202,7 +173,7 @@ -- expecting value -- <BLANKLINE> parseValue :: MichelsonSource -> Text -> Either ParserException ParsedValue-parseValue = first ParserException ... (parseNoEnv @()) value+parseValue = first ParserException ... parseNoEnv value  -- | Like 'parseValue', but also expands macros. parseExpandValue :: MichelsonSource -> Text -> Either ParserException U.Value@@ -211,7 +182,7 @@ -- Primitive instruction ------------------ -prim :: Parser le ParsedInstr+prim :: Parser ParsedInstr prim = primInstr contract parsedOp  -- Parsed operations (primitive instructions, macros, extras, etc.)@@ -220,14 +191,14 @@ -- | Parses code block after "code" keyword of a contract. -- -- This function is part of the module API, its semantics should not change.-codeEntry :: Parser le [ParsedOp]+codeEntry :: Parser [ParsedOp] codeEntry = bracewrappedOps -bracewrappedOps :: Parser le [ParsedOp]+bracewrappedOps :: Parser [ParsedOp] bracewrappedOps = lookAhead (symbol "{") *> ops  -- |--- >>> parseNoEnv @() parsedOp "" "{a}" & either (putStrLn . displayException . ParserException) (const $ pure ())+-- >>> parseNoEnv parsedOp "" "{a}" & either (putStrLn . displayException . ParserException) (const $ pure ()) -- 1:2: --   | -- 1 | {a}@@ -235,35 +206,17 @@ -- unexpected 'a' -- expecting '{', '}', macro, or primitive instruction -- <BLANKLINE>--- >>> :m + Morley.Michelson.Parser.Types--- >>> parseNoEnv @LetEnv parsedOp "" "{a}" & either (putStrLn . displayException . ParserException) (const $ pure ())--- ...--- 1:2:---   |--- 1 | {a}---   |  ^--- unexpected 'a'--- expecting '{', '}', macro, morley instruction, or primitive instruction--- <BLANKLINE>-parsedOp :: Parser le ParsedOp+parsedOp :: Parser ParsedOp parsedOp = do   pos <- getSrcPos   choice-    [ withLetEnv $ flip Prim pos <$> (EXT <$> extInstr ops)-    , withLetEnv $ lmacWithPos-    , flip Prim pos <$> prim+    [ flip Prim pos <$> prim     , flip Mac pos <$> macro parsedOp     , primOrMac     , flip Seq pos <$> bracewrappedOps     ]-  where-    lmacWithPos :: Parser' LetEnv ParsedOp-    lmacWithPos = do-      act <- mkLetMac <$> asks letMacros-      srcPos <- getSrcPos-      flip LMac srcPos <$> act -getSrcPos :: Parser le SrcPos+getSrcPos :: Parser SrcPos getSrcPos = do   sp <- getSourcePos   let l = unPos $ sourceLine sp@@ -271,17 +224,17 @@   -- reindexing starting from 0   pure . unsafe $ SrcPos <$> (mkPos $ l - 1) <*> (mkPos $ c - 1) -primWithPos :: Parser le ParsedInstr -> Parser le ParsedOp+primWithPos :: Parser ParsedInstr -> Parser ParsedOp primWithPos act = do   srcPos <- getSrcPos   flip Prim srcPos <$> act -macWithPos :: Parser le Macro -> Parser le ParsedOp+macWithPos :: Parser Macro -> Parser ParsedOp macWithPos act = do   srcPos <- getSrcPos   flip Mac srcPos <$> act -ops :: Parser le [ParsedOp]+ops :: Parser [ParsedOp] ops = ops' parsedOp  -------------------------------------------------------------------------------@@ -289,10 +242,10 @@ -- These are needed for better error messages ------------------------------------------------------------------------------- -ifOrIfX :: Parser le ParsedOp+ifOrIfX :: Parser ParsedOp ifOrIfX = do   pos <- getSrcPos-  symbol' "IF"+  symbol "IF"   a <- eitherP cmpOp ops   case a of     Left cmp -> flip Mac pos <$> (IFX cmp <$> ops <*> ops)@@ -300,7 +253,7 @@  -- Some of the operations and macros have the same prefixes in their names -- So this case should be handled separately-primOrMac :: Parser le ParsedOp+primOrMac :: Parser ParsedOp primOrMac = hidden    $  (macWithPos (ifCmpMac parsedOp) <|> ifOrIfX)   <|> (macWithPos (mapCadrMac parsedOp) <|> primWithPos (mapOp parsedOp))@@ -312,7 +265,7 @@ -- Safe construction of Haskell values ------------------------------------------------------------------------------- -parserToQuasiQuoter :: Parser () (TH.Q TH.Exp) -> TH.QuasiQuoter+parserToQuasiQuoter :: Parser (TH.Q TH.Exp) -> TH.QuasiQuoter parserToQuasiQuoter parser = TH.QuasiQuoter   { TH.quoteExp = \s ->       case parseNoEnv (mSpace *> parser) "quasi-quoter" (toText s) of

@@ -3,6 +3,7 @@  module Morley.Michelson.Parser.Annotations   ( note+  , anyNote   , noteF   , noteV   , noteDef@@ -32,7 +33,7 @@ import Morley.Util.Default  -- | General T/V/F Annotation parser, including Special Annotations-note :: forall tag le. KnownAnnTag tag => Parser le (Annotation tag)+note :: forall tag. KnownAnnTag tag => Parser (Annotation tag) note = lexeme $ string (annPrefix @tag) >> (specialNote <|> note' <|> emptyNote)   where     -- TODO [#48]: these are special annotations and should not always be accepted@@ -45,22 +46,29 @@       b <- takeWhileP Nothing isValidAnnBodyChar       return . unsafe . mkAnnotation $ T.cons a b -noteV :: Parser le VarAnn+-- | Parse arbitrary annotation.+anyNote :: Parser AnyAnn+anyNote =+      AnyAnnType <$> note @TypeTag+  <|> AnyAnnField <$> note @FieldTag+  <|> AnyAnnVar <$> note @VarTag++noteV :: Parser VarAnn noteV = note -noteDef :: KnownAnnTag tag => Parser le (Annotation tag)+noteDef :: KnownAnnTag tag => Parser (Annotation tag) noteDef = parseDef note -noteF :: Parser le FieldAnn+noteF :: Parser FieldAnn noteF = note -noteV2Def :: Parser le (VarAnn, VarAnn)+noteV2Def :: Parser (VarAnn, VarAnn) noteV2Def = permute2Def note note -notesTVF :: Parser le (TypeAnn, VarAnn, FieldAnn)+notesTVF :: Parser (TypeAnn, VarAnn, FieldAnn) notesTVF = permute3Def note note note -notesTVF2Def :: Parser le (TypeAnn, VarAnn, (FieldAnn, FieldAnn))+notesTVF2Def :: Parser (TypeAnn, VarAnn, (FieldAnn, FieldAnn)) notesTVF2Def = permute3Def note note (permute2Def note note)  -- | Parse 0/1/2 var anns and 0/1/2 field anns.@@ -75,21 +83,21 @@ -- * "@c @d %a %b" is valid -- * "@c %a %b @d" is not valid, because the two var anns are not "grouped" together. -- * "%a @c @d %b" is not valid, because the two fields anns are not "grouped" together.-notesVVFF :: Parser le ((VarAnn, VarAnn), (FieldAnn, FieldAnn))+notesVVFF :: Parser ((VarAnn, VarAnn), (FieldAnn, FieldAnn)) notesVVFF = permute2Def (liftA2 (,) note noteDef) (liftA2 (,) note noteDef) -notesVF :: Parser le (VarAnn, FieldAnn)+notesVF :: Parser (VarAnn, FieldAnn) notesVF = permute2Def note note -notesTV :: Parser le (TypeAnn, VarAnn)+notesTV :: Parser (TypeAnn, VarAnn) notesTV = permute2Def note note -notesTF :: Parser le (TypeAnn, FieldAnn)+notesTF :: Parser (TypeAnn, FieldAnn) notesTF = permute2Def note note  fieldType :: Default a-          => Parser le a-          -> Parser le (a, TypeAnn)+          => Parser a+          -> Parser (a, TypeAnn) fieldType fp = runPermutation $   (,) <$> toPermutationWithDefault  def     fp       <*> toPermutationWithDefault noAnn note

@@ -13,7 +13,7 @@ import Morley.Michelson.Parser.Types import Morley.Michelson.Untyped -viewName_ :: Parser le ViewName+viewName_ :: Parser ViewName viewName_ = lexeme do   string "\""   str <- manyTill anySingle (string "\"")

@@ -11,33 +11,19 @@   ) where  import Data.Data (Data(..))-import Fmt (Buildable(build), pretty, (+|), (|+))+import Fmt (Buildable(build), pretty) import Text.Megaparsec (ParseErrorBundle, ShowErrorComponent(..), errorBundlePretty)  import Morley.Michelson.Untyped.View import Morley.Util.Instances ()-import Morley.Util.Positive  data CustomParserException   = StringLiteralException StringLiteralParserException   | ViewNameException BadViewNameError   | OddNumberBytesException-  | WrongTagArgs Natural Positive-  | WrongAccessArgs Natural Positive-  | WrongSetArgs Natural Positive   | ExcessFieldAnnotation-  | MultiRootAnnotationException-  | DeprecatedException   deriving stock (Eq, Data, Ord, Show, Generic) -{-# DEPRECATED-    WrongTagArgs-  , WrongAccessArgs-  , WrongSetArgs--  "Exceptions specific to deprecated Morley language extensions"-  #-}- instance NFData CustomParserException  instance ShowErrorComponent CustomParserException where@@ -45,18 +31,6 @@   showErrorComponent (ViewNameException e) = pretty e   showErrorComponent OddNumberBytesException = "odd number bytes"   showErrorComponent ExcessFieldAnnotation = "excess field annotation"-  showErrorComponent MultiRootAnnotationException = "unexpected multiple root annotations"-  showErrorComponent DeprecatedException = "deprecated syntax, use --deprecated-morley-extensions \-    \command-line argument to silence this error"-  showErrorComponent (WrongTagArgs idx size) =-    "TAG: too large index: " +| idx |+ " \-           \exceedes union size " +| size |+ ""-  showErrorComponent (WrongAccessArgs idx size) =-    "ACCESS: too large index: " +| idx |+ " \-           \exceedes tuple size " +| size |+ ""-  showErrorComponent (WrongSetArgs idx size) =-    "SET: too large index: " +| idx |+ " \-           \exceedes tuple size " +| size |+ ""  data StringLiteralParserException   = InvalidEscapeSequence Char

@@ -1,76 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA---- TODO [#712]: Remove this next major release-{-# OPTIONS_GHC -Wno-deprecations #-}---- | Parsing logic for extra instructions (Morley extensions)--module Morley.Michelson.Parser.Ext-  ( extInstr-  , stackType--  -- * For tests-  , printComment-  ) where--import Prelude hiding (try)--import Text.Megaparsec (choice, label, satisfy, try)-import Text.Megaparsec.Char (alphaNumChar, string)-import Text.Megaparsec.Char.Lexer qualified as L--import Morley.Michelson.Macro (ParsedOp(..), ParsedUExtInstr)-import Morley.Michelson.Parser.Lexer-import Morley.Michelson.Parser.Type-import Morley.Michelson.Parser.Types (LetEnv, Parser')-import Morley.Michelson.Untyped qualified as U--extInstr :: Parser' LetEnv [ParsedOp] -> Parser' LetEnv ParsedUExtInstr-extInstr opsParser = do-  label "morley instruction" $ choice [stackOp, testAssertOp opsParser, printOp]--stackOp :: Parser' LetEnv ParsedUExtInstr-stackOp = word' "STACKTYPE" U.STACKTYPE <*> stackType--testAssertOp :: Parser' LetEnv [ParsedOp] -> Parser' LetEnv ParsedUExtInstr-testAssertOp opsParser =-  word' "TEST_ASSERT" U.UTEST_ASSERT <*> testAssert opsParser--printOp :: Parser' LetEnv ParsedUExtInstr-printOp = word' "PRINT" U.UPRINT <*> printComment--testAssert :: Parser' LetEnv [ParsedOp] -> Parser' LetEnv (U.TestAssert ParsedOp)-testAssert opsParser = do-  n <- lexeme (toText <$> some alphaNumChar)-  c <- printComment-  o <- opsParser-  return $ U.TestAssert n c o--printComment :: Parser' LetEnv U.PrintComment-printComment = do-  string "\""-  let validChar = toText <$> some (satisfy (\x -> x /= '%' && x /= '"'))-  c <- many (Right <$> stackRef <|> Left <$> validChar)-  symbol "\""-  return $ U.PrintComment c--stackRef :: Parser' LetEnv U.StackRef-stackRef = do-  string "%"-  n <- brackets' L.decimal-  return $ U.StackRef n--stackType :: Parser' LetEnv U.StackTypePattern-stackType = do-  symbol "'[" >> (emptyStk <|> stkCons <|> stkRest)-  where-    emptyStk = try $ symbol "]" $> U.StkEmpty-    stkRest = try $ symbol "..." >> symbol "]" $> U.StkRest-    stkCons = try $ do-      t <- tyVar-      s <- (symbol "," >> stkCons <|> stkRest) <|> emptyStk-      return $ U.StkCons t s--tyVar :: Parser' LetEnv U.TyVar-tyVar = (U.TyCon <$> type_) <|> (U.VarID <$> varID)