morley 1.19.1 → 1.19.2

raw patch · 92 files changed

+6796/−5775 lines, 92 filesdep +prettyprinterdep −fmtdep −wl-pprint-textdep ~vinylPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: prettyprinter

Dependencies removed: fmt, wl-pprint-text

Dependency ranges changed: vinyl

API changes (from Hackage documentation)

Files

• CHANGES.md +117/−0
• app/Main.hs +3/−301
• app/REPL.hs +0/−327
• morley.cabal +21/−19
• src/Morley/App/CLI.hs +303/−0
• src/Morley/App/REPL.hs +318/−0
• src/Morley/AsRPC.hs +395/−365
• src/Morley/Micheline/Binary.hs +3/−8
• src/Morley/Micheline/Class.hs +942/−1043
• src/Morley/Micheline/Expression.hs +41/−91
• src/Morley/Micheline/Expression/Internal/MichelinePrimitive.hs +127/−0
• src/Morley/Micheline/Expression/Internal/TH.hs +33/−0
• src/Morley/Michelson/Analyzer.hs +3/−4
• src/Morley/Michelson/Doc.hs +2/−2
• src/Morley/Michelson/ErrorPos.hs +3/−9
• src/Morley/Michelson/Internal/ViewName.hs +3/−3
• src/Morley/Michelson/Interpret.hs +349/−211
• src/Morley/Michelson/Macro.hs +117/−72
• src/Morley/Michelson/Optimizer.hs +3/−631
• src/Morley/Michelson/Optimizer/Internal/Rules.hs +526/−0
• src/Morley/Michelson/Optimizer/Internal/Ruleset.hs +78/−0
• src/Morley/Michelson/Optimizer/Utils.hs +107/−0
• src/Morley/Michelson/Parser.hs +98/−40
• src/Morley/Michelson/Parser/Instr.hs +50/−68
• src/Morley/Michelson/Parser/Macro.hs +110/−47
• src/Morley/Michelson/Parser/Value.hs +38/−42
• src/Morley/Michelson/Printer.hs +5/−7
• src/Morley/Michelson/Printer/Util.hs +52/−29
• src/Morley/Michelson/Runtime.hs +80/−53
• src/Morley/Michelson/Runtime/GState.hs +2/−1
• src/Morley/Michelson/Runtime/TxData.hs +6/−0
• src/Morley/Michelson/TypeCheck/Error.hs +114/−113
• src/Morley/Michelson/TypeCheck/Ext.hs +2/−2
• src/Morley/Michelson/TypeCheck/Helpers.hs +18/−18
• src/Morley/Michelson/TypeCheck/Instr.hs +46/−47
• src/Morley/Michelson/TypeCheck/TypeCheck.hs +6/−6
• src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs +69/−23
• src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs +8/−5
• src/Morley/Michelson/TypeCheck/Types.hs +5/−10
• src/Morley/Michelson/TypeCheck/Value.hs +52/−38
• src/Morley/Michelson/Typed/Annotation.hs +1/−6
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/TH.hs +12/−10
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Types.hs +6/−4
• src/Morley/Michelson/Typed/Contract.hs +1/−25
• src/Morley/Michelson/Typed/Convert.hs +126/−106
• src/Morley/Michelson/Typed/Entrypoints.hs +26/−39
• src/Morley/Michelson/Typed/Existential.hs +1/−1
• src/Morley/Michelson/Typed/Haskell/Doc.hs +16/−12
• src/Morley/Michelson/Typed/Haskell/Value.hs +3/−3
• src/Morley/Michelson/Typed/Instr.hs +12/−6
• src/Morley/Michelson/Typed/Operation.hs +150/−5
• src/Morley/Michelson/Typed/Polymorphic.hs +1/−1
• src/Morley/Michelson/Typed/Scope.hs +134/−1413
• src/Morley/Michelson/Typed/Scope/Internal/CheckScope.hs +102/−0
• src/Morley/Michelson/Typed/Scope/Internal/Comparable.hs +146/−0
• src/Morley/Michelson/Typed/Scope/Internal/Deprecated.hs +299/−0
• src/Morley/Michelson/Typed/Scope/Internal/ForbidT.hs +225/−0
• src/Morley/Michelson/Typed/Scope/Internal/Presence.hs +152/−0
• src/Morley/Michelson/Typed/Scope/Internal/Scopes.hs +244/−0
• src/Morley/Michelson/Typed/Scope/Internal/TH.hs +26/−0
• src/Morley/Michelson/Typed/Scope/Internal/WellTyped.hs +169/−0
• src/Morley/Michelson/Typed/Scope/Internal/WithDeMorganScope.hs +147/−0
• src/Morley/Michelson/Typed/Sing.hs +6/−6
• src/Morley/Michelson/Typed/T.hs +5/−14
• src/Morley/Michelson/Typed/Util.hs +7/−15
• src/Morley/Michelson/Typed/Value.hs +28/−16
• src/Morley/Michelson/Typed/View.hs +9/−4
• src/Morley/Michelson/Untyped/Aliases.hs +2/−2
• src/Morley/Michelson/Untyped/Annotation.hs +4/−10
• src/Morley/Michelson/Untyped/Contract.hs +71/−34
• src/Morley/Michelson/Untyped/Entrypoints.hs +4/−8
• src/Morley/Michelson/Untyped/Ext.hs +47/−17
• src/Morley/Michelson/Untyped/HoistInstr.hs +10/−0
• src/Morley/Michelson/Untyped/Instr.hs +166/−43
• src/Morley/Michelson/Untyped/Type.hs +16/−43
• src/Morley/Michelson/Untyped/Value.hs +62/−48
• src/Morley/Michelson/Untyped/View.hs +8/−3
• src/Morley/Tezos/Address.hs +18/−26
• src/Morley/Tezos/Address/Alias.hs +3/−3
• src/Morley/Tezos/Crypto.hs +1/−2
• src/Morley/Tezos/Crypto/BLS.hs +2/−2
• src/Morley/Tezos/Crypto/BLS12381.hs +7/−12
• src/Morley/Tezos/Crypto/Util.hs +10/−15
• src/Morley/Util/Instances.hs +0/−7
• src/Morley/Util/Interpolate.hs +7/−8
• src/Morley/Util/Interpolate/Internal.hs +3/−15
• src/Morley/Util/Markdown.hs +3/−3
• src/Morley/Util/MismatchError.hs +36/−41
• src/Morley/Util/Peano.hs +2/−15
• src/Morley/Util/PeanoNatural.hs +3/−3
• src/Morley/Util/StubbedProof.hs +1/−0
• src/Morley/Util/Type.hs +1/−94

@@ -1,6 +1,123 @@ <!-- Unreleased: append new entries here -->  +1.19.2+======+* [!1365](https://gitlab.com/morley-framework/morley/-/merge_requests/1365)+  Split optimizer module+  + More utilities for writing rules are now exported from+    `Morley.Michelson.Optimizer.Utils`;+  + Fixed a bug with missing pattern in the `Buildable OptimizationStage`+    instance.+* [!1352](https://gitlab.com/morley-framework/morley/-/merge_requests/1352)+  Clean-up Buildable ExecutorOp implementation+  + Add `Buildable` instances for `OriginationOperation`, `TransferOperation`,+    `SetDelegateOperation`, `EmitOperation`;+  + Rewrite `Buildable ExecutorOp` to delegate to these new instances.+* [!1357](https://gitlab.com/morley-framework/morley/-/merge_requests/1357)+  Better tests for `PACK`+  + Fix an issue when untyping `CREATE_CONTRACT` instruction -- morley would+    always use `Readable` representation for its contents;+  + Fix an issue in typechecking `CREATE_CONTRACT` instruction -- morley+    `SELF` inside `CREATE_CONTRACT` inside lambdas was rejected.+* [!1349](https://gitlab.com/morley-framework/morley/-/merge_requests/1349)+  Improve morley compilation time+  + `Forbid*` constraints are no longer carried as superclasses of `Comparable`.+    Match on `comparableImplies` to bring those into scope. In case of+    impossible patterns, empty `case` with `checkComparability` should do the+    trick.+* [!1351](https://gitlab.com/morley-framework/morley/-/merge_requests/1351)+  Fix and improve `Buildable MichelsonFailureWithStack`+* [!1346](https://gitlab.com/morley-framework/morley/-/merge_requests/1346)+  Use proper datatype for Micheline primitives, refactor some FromExp instances+  + Replace a list of strings with a proper datatype for Micheline primitives+  + Refactor `FromExp` instances to make pattern-matches (more) total and reduce+    redundancy+  + Make `FromExp` exceptions more structured+  + Other minor refactoring+* [!1342](https://gitlab.com/morley-framework/morley/-/merge_requests/1342)+  Replace fmt with prettyprinter+  + Introduce overlappable `Buildable` instance for anything `RenderDoc` to+    avoid proliferation of trivial instances+  + Deprecate `buildRenderDoc` and `buildRenderDocExtended`+  + Replace unnecessary `RenderDoc` instances with `Buildable` (this refers to+    various error types)+  + `printDoc`, `printDocB`, `printDocS` deprecated in favor of+    `printRenderDoc`+  + Redundant `forceSingleLine` parameter to `renderType` removed+  + Obsolete `Prettier` newtype deprecated+  + Improve `NotWellTyped` error formatting+  + Improve formatting for `Buildable ExecutorOp`+* [!1347](https://gitlab.com/morley-framework/morley/-/merge_requests/1347)+  Better errors for missing contract fields+  + Improve efficiency when constructing untyped contract from list of contract+    blocks+  + Rename `UnsafeViewsSet` to `ViewsSet`, as there's nothing inherently unsafe+    about this constructor any more (old name is left as a pattern synonym, but+    deprecated)+* [!1343](https://gitlab.com/morley-framework/morley/-/merge_requests/1343)+  Fix optimizer dipSwapDrop regression+  + Fixed a bug where `DIP n code` would be deoptimized into `DIP (n - 1) {+    SWAP; code }`+  + While at it, `DUP; DUG (m + 1); DROP` is now optimized to `DUG m`+* [!1344](https://gitlab.com/morley-framework/morley/-/merge_requests/1344)+  Typecheck recursive lambda values+* [!1323](https://gitlab.com/morley-framework/morley/-/merge_requests/1323)+  Trace called contracts on error+  + Trace operations in the Morley emulator+* [!1310](https://gitlab.com/morley-framework/morley/-/merge_requests/1310)+  Various parser fixes+  + Make parser stricter wrt braces around code blocks. Now things like `DIP+    DROP` are rejected (as per reference), but `DIP FAIL` are allowed (as `FAIL`+    is a macro)+  + Properly handle braced code blocks in typechecker's verbose error messages+  + Use optimized untyped contract representation in `toExpression`+  + Fix macro expansion rules to match reference; add macro expansion tests+    against reference+* [!1341](https://gitlab.com/morley-framework/morley/-/merge_requests/1341)+  Refactor scope constraints+  + Unified all `check*Presence` functions into `checkTPresence`+  + Unified all `*Absense` (sic) and `check*Presence` into `tAbsence` and+    `tPresence`+  + Unified all `Contains*` type families, plus `IsComparable` into `ContainsT`+  + All now-redundant synonyms are deprecated+  + Deprecate `HasNo*` and `Proper*BetterErrors` in favor of `Forbid*` and+    `*Scope` respectively.+  + Simplify `WithDeMorganScope`+  + Avoid unnecessary singleton traversals using `checkTPresence`, remove where+    possible, use de Morgan laws otherwise.+  + Improve `Forbid*` error messages+  + Improve `*Scope` error messages with the suggestion to add the corresponding+    scope constraint+  + Improve error messages on stuck type families with `Forbid*` and `*Scope`+  + Drop redundant uses of `(:-)` implication in `AsRPC`, use constraints+    explicitly+* [!1293](https://gitlab.com/morley-framework/morley/-/merge_requests/1293)+  Add extensible metadata field to StkEl+* [!1335](https://gitlab.com/morley-framework/morley/-/merge_requests/1335)+  Include morley CLI commands with morley-client+  + Moved morley CLI parser and REPL to library under `Morley.App`+* [!1333](https://gitlab.com/morley-framework/morley/-/merge_requests/1333)+  Improve typechecker error rendering+  + Switched to `prettyprinter` from `wl-pprint-text`+  + Introduced `Morley.Michelson.Printer.Compat` as a thin compatibility layer+* [!1336](https://gitlab.com/morley-framework/morley/-/merge_requests/1336)+  Improve non-recursive `deriveRPC` errors+  + Print human-readable error messages when required `HasRPCRepr` instances are+    missing in non-recursive mode (i.e. `droRecursive=False`)+* [!1340](https://gitlab.com/morley-framework/morley/-/merge_requests/1340)+  Remove deprecated types and functions+  + `haskellRepStripFieldPrefix`+  + `Morley.Michelson.Typed.Contract.mapEntriesOrdered`+  + `Morley.Michelson.Untyped.Contract.mapContractCode`+  + `linearizeRightCombValuePair`+  + `expandList`+  + `(|-)`+  + `MockableConstraint` and `unsafeProvideConstraint`+  + `failUnlessEvi`+  + `failWhenEvi`+  + `ConcatListOfTypesAssociativity` and `listOfTypesConcatAssociativityAxiom`+ 1.19.1 ====== * [!1325](https://gitlab.com/morley-framework/morley/-/merge_requests/1325)

@@ -5,312 +5,14 @@   ( main   ) where -import Data.Default (def)-import Data.Singletons (demote)-import Data.Text.Lazy.IO.Utf8 qualified as Utf8 (writeFile) import Data.Version (showVersion)-import Fmt (pretty, unlinesF)-import Named (paramF) import Options.Applicative-  (execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long, progDesc, short,-  subparser, switch)-import Options.Applicative qualified as Opt+  (execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long, progDesc) import Options.Applicative.Help.Pretty (Doc, linebreak) import Paths_morley (version)-import Text.Hex (encodeHex) -import Morley.CLI-import Morley.Michelson.Analyzer (analyze)-import Morley.Michelson.Interpret (RemainingSteps(..))-import Morley.Michelson.Optimizer (OptimizerConf(..), optimizeVerboseWithConf)-import Morley.Michelson.Printer (printSomeContract, printTypedContract, printUntypedContract)-import Morley.Michelson.Runtime-import Morley.Michelson.Runtime.GState (genesisAddress)-import Morley.Michelson.TypeCheck (tcVerbose, typeCheckContract, typeCheckValue, typeCheckingWith)-import Morley.Michelson.TypeCheck qualified as TypeCheck-import Morley.Michelson.Typed (Contract'(..), SomeContract(..), unContractCode)-import Morley.Michelson.Typed qualified as T-import Morley.Michelson.Typed.Contract (mapContractCodeM)-import Morley.Tezos.Address-import Morley.Tezos.Address.Alias-import Morley.Tezos.Core (Mutez, tz)-import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey)-import Morley.Util.CLI (mkCLOptionParser, mkCommandParser, outputOption)-import Morley.Util.Main (wrapMain)-import Morley.Util.Named-import REPL--data DryRunOrWrite = DryRun | Write--mkCommandParser' :: String -> String -> Opt.Parser a -> Opt.Mod Opt.CommandFields a-mkCommandParser' = flip . mkCommandParser--argParser :: Opt.Parser (IO ())-argParser = subparser $ mconcat-  [ printSubCmd-  , typecheckSubCmd-  , emulateSubCmd-  , optimizeSubCmd-  , analyzeSubCmd-  , createChestSubCmd-  , replSubCmd-  ]------------------------------------------------------------------------------------- Subcommands------------------------------------------------------------------------------------- NB: in case this looks mysterious, in IOCmd functions, outer 'do' is--- Opt.Parser using ApplicativeDo, which then returns an IO action, i.e. inner--- 'do' is 'IO ()'. -- @lierdakil--type IOCmd = Opt.Mod Opt.CommandFields (IO ())--typecheckSubCmd :: IOCmd-typecheckSubCmd = mkCommandParser' "typecheck" "Typecheck passed contract." do-  contractFile <- optional contractFileOption-  tcOptions <- typeCheckOptionsOption-  pure do-    morleyContract <- prepareContract contractFile-    -- 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 tcOptions-      $ typeCheckContract morleyContract-    when (TypeCheck.tcVerbose tcOptions) $-      putStrLn $ printSomeContract False contract-    putTextLn "Contract is well-typed"--printSubCmd :: IOCmd-printSubCmd = mkCommandParser' "print"-  "Parse a Morley contract and print corresponding Michelson \-  \contract that can be parsed by the OCaml reference client: octez-client."-  do-    mInputFile <- optional contractFileOption-    mOutputFile <- outputOption-    forceSingleLine <- onelineOption-    pure do-      contract <- prepareContract mInputFile-      let write = maybe putStrLn Utf8.writeFile mOutputFile-      write $ printUntypedContract forceSingleLine contract--emulateSubCmd :: IOCmd-emulateSubCmd = mkCommandParser' "emulate" "Set of commands to run in an emulated environment." $-  subparser $ mconcat-    [ runSubCmd-    , originateSubCmd-    , transferSubCmd-    , transferTicketSubCmd-    , runViewSubCmd-    ]--runSubCmd :: IOCmd-runSubCmd = mkCommandParser' "run"-  "Run passed contract. It's originated first and then a transaction is sent to it." do-    txData <- txDataOption-    contract <- contractSimpleOriginationDataOption-    cro <- commonRunOptions Write-    pure do-      michelsonContract <- traverse prepareContract contract-      void $ runContract cro michelsonContract txData--runViewSubCmd :: IOCmd-runViewSubCmd = mkCommandParser' "view"-  "Run some view on a contract either supplied directly or identified \-  \by an address. It's originated first if supplied directly." do-    cro <- commonRunOptions Write-    addressOrContract <--      ContractSpecAddressOrAlias <$> addressOrAliasOption Nothing-        ! #name "contract-addr"-        ! #help "Contract address to call view on."-      <|> ContractSpecOrigination <$> contractSimpleOriginationDataOption-    viewName <- mkCLOptionParser Nothing-      ! #name "name"-      ! #help "View name."-    sender <- someAddressOrAliasOption-        (Just $ SAOAKindSpecified $ AddressResolved genesisAddress)-      ! #name "sender"-      ! #help "Sender address."-    viewArg <- TxUntypedParam <$> valueOption Nothing-      ! #name "arg"-      ! #help "View call argument."-    pure do-      contractSpec <- (traverse . traverse) prepareContract addressOrContract-      void $ runView cro contractSpec viewName sender viewArg--replSubCmd :: IOCmd-replSubCmd = mkCommandParser' "repl" "Start a Morley REPL." $ pure runRepl--originateSubCmd :: IOCmd-originateSubCmd = mkCommandParser' "originate" "Originate passed contract. Add it to passed DB." do-  simpleOriginationData <- contractSimpleOriginationDataOption-  dbPath <- dbPathOption-  tcOptions <- typeCheckOptionsOption-  verbose <- verboseFlag-  originator <- addressOption (Just genesisAddress)-    ! #name "originator"-    ! #help "Contract's originator."-  alias <- optional (aliasOption "alias")-  delegate <- optional $ keyHashOption Nothing-    ! #name "delegate"-    ! #help "Contract's optional delegate."-  pure do-    michelsonContract <- traverse prepareContract simpleOriginationData-    addr <--      originateContract-        ! #dbPath dbPath-        ! #tcOpts tcOptions-        ! #originator originator-        ! paramF #alias alias-        ! paramF #delegate delegate-        ! #csod michelsonContract-        ! #verbose verbose-    putTextLn $ "Originated contract " <> pretty addr--transferSubCmd :: IOCmd-transferSubCmd = mkCommandParser' "transfer" "Transfer tokens to given address." do-  destination <- someAddressOrAliasOption Nothing-    ! #name "to"-    ! #help "Address or alias of the transfer's destination."-  txData <- txDataOption-  cro <- commonRunOptions DryRun-  pure $ transfer cro destination txData--transferTicketSubCmd :: IOCmd-transferTicketSubCmd = mkCommandParser' "transfer-ticket" "Transfer ticket to given address." do-  destination <- someAddressOrAliasOption Nothing-    ! #name "to"-    ! #help "Address or alias of the transfer's destination."-  tdSenderAddress :: L1Address <- Constrained <$> addressOption (Just genesisAddress)-    ! #name "sender" ! #help "Sender address"-  ticketer <- mkCLOptionParser @Address Nothing-    ! #name "ticketer" ! #help "Ticketer"-  value <- valueOption Nothing-    ! #name "value" ! #help "Ticket value"-  ty <- mkCLOptionParser Nothing-    ! #name "type" ! #help "Ticket argument type"-  tAmount <- mkCLOptionParser @Natural Nothing-    ! #name "amount" ! #help "Amount of tickets"-  tdAmount <- mutezOption (Just minBound)-    ! #name "mutez" ! #help "Mutez amount additionally sent by a transaction. \-    \Note that on network, as of Mumbai, implicit accounts can't send tickets \-    \and mutez in the same operation, however the Morley emulator allows it."-  tdEntrypoint <- entrypointOption-    ! #name "entrypoint" ! #help "Entrypoint to call"-  cro <- commonRunOptions DryRun-  pure $ T.withUType ty \(_ :: T.Notes t) -> do-    tValue <- either throwM pure . typeCheckingWith (croTCOpts cro) $-      typeCheckValue @t value-    T.Dict <- either (throwM . TypeCheck.UnsupportedTypeForScope (demote @t)) pure $-      T.checkScope @(T.ParameterScope t, T.Comparable t)-    let tdParameter = TxTypedParam $ T.VTicket ticketer tValue tAmount-    transfer cro destination TxData{..}--optimizeSubCmd :: IOCmd-optimizeSubCmd = mkCommandParser' "optimize" "Optimize the contract." do-  contractFile <- optional contractFileOption-  output <- outputOption-  singleLine <- onelineOption-  maxStageIterations <- mkCLOptionParser (Just $ ocMaxIterations def)-    ! #name "max-stage-iterations"-    ! #help "Maximum number of iterations per optimizer stage. \-        \The default is usually adequate, but you want to try raising it \-        \to see if it affects the result."-  verbose <- verboseFlag-  pure do-    untypedContract <- prepareContract contractFile-    SomeContract checkedContract <--      either throwM pure . typeCheckingWith laxTcOptions $-        typeCheckContract untypedContract-    let (logs, optimizedContract) =-          mapContractCodeM (optimizeVerboseWithConf conf) checkedContract-        conf = def { ocMaxIterations = maxStageIterations }-    maybe putStrLn Utf8.writeFile output $ printTypedContract singleLine optimizedContract-    when verbose $ hPutStrLn stderr $ pretty @_ @Text $ unlinesF logs--analyzeSubCmd :: IOCmd-analyzeSubCmd = mkCommandParser' "analyze" "Analyze the contract." do-  contractFile <- optional contractFileOption-  pure do-    untypedContract <- prepareContract contractFile-    SomeContract contract <--      either throwM pure . typeCheckingWith laxTcOptions $-        typeCheckContract untypedContract-    putTextLn $ pretty $ analyze (unContractCode $ cCode contract)--createChestSubCmd :: IOCmd-createChestSubCmd = mkCommandParser' "create_chest" "Create a timelocked chest and key." do-  payload <- payloadOption-  time <- timeOption-  pure do-    (chest, key) <- createChestAndChestKey payload time-    putStrLn $ "Chest: 0x" <> encodeHex (chestBytes chest)-    putStrLn $ "Key: 0x" <> encodeHex (chestKeyBytes key)------------------------------------------------------------------------------------- Parsers-----------------------------------------------------------------------------------verboseFlag :: Opt.Parser Bool-verboseFlag = switch $-  short 'v' <>-  long "verbose" <>-  help "Whether output should be verbose."--typeCheckOptionsOption :: Opt.Parser TypeCheck.TypeCheckOptions-typeCheckOptionsOption = do-  tcVerbose <- verboseFlag-  tcStrict <- fmap not . switch $-    long "typecheck-lax" <>-    help "Whether actions permitted in `octez-client run` but forbidden in \-          \e.g. `octez-client originate` should be allowed here."-  return TypeCheck.TypeCheckOptions{..}--commonRunOptions :: DryRunOrWrite -> Opt.Parser CommonRunOptions-commonRunOptions defaultDryRun = do-  croNow <- nowOption-  croLevel <- fromMaybe (croLevel def) <$> levelOption-  croMinBlockTime <- fromMaybe (croMinBlockTime def) <$> minBlockTimeOption-  croMaxSteps <- RemainingSteps <$> maxStepsOption-  croDBPath <- dbPathOption-  croTCOpts <- typeCheckOptionsOption-  croVerbose <- verboseFlag-  croDryRun <- case defaultDryRun of-    Write -> fmap not . switch $-      long "write" <>-      help "Write updated DB to the DB file."-    DryRun -> switch $-      long "dry-run" <>-      help "Do not write updated DB to the DB file."-  pure CommonRunOptions{..}--contractSimpleOriginationDataOption :: Opt.Parser (ContractSimpleOriginationData (Maybe FilePath))-contractSimpleOriginationDataOption = do-  csodStorage <- valueOption Nothing-    ! #name "storage"-    ! #help "Initial storage of the contract."-  csodContract <- optional contractFileOption-  csodBalance <- mutezOption (Just defaultBalance)-    ! #name "balance"-    ! #help "Initial balance of the contract."-  pure ContractSimpleOriginationData{..}------------------------------------------------------------------------------------- Constants-----------------------------------------------------------------------------------defaultBalance :: Mutez-defaultBalance = [tz|4|]---- | Most permitting options, when we don't care much about typechecking.-laxTcOptions :: TypeCheck.TypeCheckOptions-laxTcOptions = TypeCheck.TypeCheckOptions-  { TypeCheck.tcVerbose = False-  , TypeCheck.tcStrict = False-  }------------------------------------------------------------------------------------- Actual main---------------------------------------------------------------------------------+import Morley.App.CLI+import Morley.Util.Main  main :: IO () main = wrapMain $ join $ execParser programInfo

@@ -1,327 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA-{-|-Implements an REPL that can execute Morley instructions.  REPL starts with an-empty stack. At each instruction entered, the modified stack, or an error is-printed. Multiple instructions separated by semicolons should work as expected.-Available meta commads are:-- ':help', displays this help\n ':stack', prints the current stack- ':loadstack filename', loads the stack from a file- ':dumpstack filename', dumps the stack to a file- ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."--}-module REPL-  ( runRepl-  ) where--import Control.Exception (IOException)-import Control.Monad.Random (randomIO)-import Data.Aeson qualified as Aeson-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(..))-import Fmt (fmt, pretty)-import System.Console.Haskeline-  (InputT, Interrupt(..), defaultSettings, getInputLine, runInputT, withInterrupt)-import Text.Megaparsec (parse)--import Morley.Michelson.Interpret (interpretInstr)-import Morley.Michelson.Macro (ParsedOp, expand)-import Morley.Michelson.Parser (errorBundlePretty, ops, parseExpandValue, parseNoEnv, type_)-import Morley.Michelson.Parser.Types (MichelsonSource(..))-import Morley.Michelson.Printer (printDoc, printTypedValue)-import Morley.Michelson.Printer.Util (buildRenderDoc, doesntNeedParens)-import Morley.Michelson.Runtime.Dummy-import Morley.Michelson.Runtime.Import (readValue)-import Morley.Michelson.TypeCheck-  (SomeTcInstr(..), SomeTcInstrOut(..), TypeCheckOptions(..), runTypeCheckIsolated,-  typeCheckingWith)-import Morley.Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter)-import Morley.Michelson.TypeCheck.Types (HST(..))-import Morley.Michelson.Typed qualified as T-import Morley.Michelson.Untyped qualified as U-import Morley.Tezos.Crypto-import Morley.Util.Sing (castSing)-import Text.Hex (decodeHex, encodeHex)--data SomeStack = forall t. T.SingI t => SomeStack-  { stValues :: (Rec T.Value t)-  , stTypes :: HST t-  }--type ReplM = InputT (StateT SomeStack IO)--runRepl :: IO ()-runRepl = evalStateT (runInputT defaultSettings repl) emptyStack---- | Prints an error message to stderr-printErr :: (MonadIO m) => Text -> m ()-printErr m = liftIO $ hPutStrLn stderr m---- | Read commands or instructions from stdin and executes them.--- If user presses Ctrl-c during execution of an instruction, it will be--- caught and handled here itself. This ensures that REPL does not crash as--- a result of user pressing Ctrl-c in an attempt to end a loop.-repl :: ReplM ()-repl = do-  printHelp-  repl_--repl_ :: ReplM ()-repl_ = do-   minput <- getInputLine "Morley>>> "-   case strStrip <$> minput of-     Nothing -> pass -- Ctrl D-     Just ":quit" -> pass-     Just input -> do-      case input of-        "" -> pass-        ":clear" -> lift $ put emptyStack-        ":stack" -> printStack-        ":help" -> printHelp-        (stripPrefixNonEmpty ":dumpstack" -> Just filename) ->-          dumpStackToFile $ toString $ strip $ toText filename-        (stripPrefixNonEmpty ":loadstack" -> Just filename) ->-          loadStackFromFile $ toString $ strip $ toText filename-        (stripPrefixNonEmpty ":parse" -> Just parseInput) ->-          tryParse $ strip $ toText parseInput-        (stripPrefixNonEmpty ":base58encode" -> Just parseInput) ->-          base58Encode $ strip $ toText parseInput-        (stripPrefix ":genkeys" -> Just mseed) -> do-           seed <- case mseed of-             "" -> show <$> (liftIO (randomIO @Word64))-             seed -> pure seed-           let sk = detSecretKey (encodeUtf8 seed)-           let pk = toPublic sk-           let pkh = hashKey pk-           printResult "Secret Key" (formatSecretKey sk)-           printResult "Public Key" (formatPublicKey pk)-           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)-      repl_-  where-    strStrip = toString . strip . toText-    stripPrefixNonEmpty p i = case stripPrefix p i of-      Just "" -> Nothing-      x -> x--base58Encode :: Text -> ReplM ()-base58Encode inp = case decodeHex $ fromMaybe inp $ (T.stripPrefix "0x" inp) of-  Just b -> do-    printResult "Base58encode" $ decodeUtf8 $ Base58.encodeBase58 Base58.bitcoinAlphabet b-    printResult "Base58encode with checksum" $ encodeBase58Check b-  Nothing -> putTextLn "Can't parse input as hex-encoded bytes"--tryParseMichelsonValue :: forall (t :: T.T). (T.SingI t, T.HasNoOp t) => Text -> Text -> ReplM ()-tryParseMichelsonValue msg parseInput =-  case readValue @t MSStdin parseInput of-    Right s -> printResult msg $ (fmt . buildRenderDoc) s-    Left _ -> pass--underlined :: MonadIO m => Text -> m ()-underlined x = liftIO do-  putTextLn x-  putTextLn $ T.replicate (T.length x) "-"--printResult :: MonadIO m => Text -> Text -> m ()-printResult heading result = do-  underlined heading-  putTextLn result-  putTextLn ""--tryParse :: Text -> ReplM ()-tryParse parseInput = do-  tryParseMichelsonValue @'T.TKey "Michelson Key" parseInput-  tryParseMichelsonValue @'T.TUnit "Michelson Unit" parseInput-  tryParseMichelsonValue @'T.TSignature "Michelson Signature" parseInput-  tryParseMichelsonValue @'T.TChainId "Michelson ChainId" parseInput-  tryParseMichelsonValue @'T.TTimestamp "Michelson Timestamp" parseInput-  tryParseMichelsonValue @'T.TAddress "Michelson Address" parseInput-  tryParseMichelsonValue @'T.TString "Michelson String" parseInput-  tryParseMichelsonValue @'T.TInt "Michelson Int" parseInput-  tryParseMichelsonValue @'T.TNat "Michelson Nat" parseInput-  tryParseMichelsonValue @'T.TBytes "Michelson Bytes" parseInput-  tryParseMichelsonValue @'T.TMutez "Michelson Mutez" parseInput-  tryParseMichelsonValue @'T.TKeyHash "Michelson KeyHash" parseInput-  tryParseMichelsonValue @'T.TBls12381Fr "Michelson Bls12381Fr" parseInput-  tryParseMichelsonValue @'T.TBls12381G1 "Michelson Bls12381G1" parseInput-  tryParseMichelsonValue @'T.TBls12381G2 "Michelson Bls12381G2" parseInput-  tryParseMichelsonValue @'T.TBool "Michelson Bool" parseInput--  case parsePublicKey parseInput of-    Right p -> do-      printResult "Public Key" $ formatPublicKey p-    Left _ -> pass-  case parseSignature parseInput of-    Right p -> do-      printResult "Signature" $ formatSignature p-    Left _ -> pass-  case parseSecretKey parseInput of-    Right p -> do-      printResult "Secret Key" $ formatSecretKey p-    Left _ -> pass-  case parseHash @'HashKindPublicKey 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)-    Nothing -> pass-  case decodeBase58Check parseInput of-    Just p -> do-      printResult "Base58Check Encoded Bytes" $ "0x" <> (encodeHex p)-    Nothing -> pass---- | Try to execute the given input string as a Morley instruction.-runCode :: Text -> ReplM ()-runCode code = do-  case parseInstructions code of-    Left err -> printErr err-    Right [] -> pass-    Right parsedOps -> do-      let expandedOps = expand <$> parsedOps-      lift get >>= \case-        SomeStack {..} -> case castSing stTypes of-          Just hstInp -> case typeCheckingWith tcOptions . runTypeCheckIsolated $-                                typeCheckList expandedOps hstInp of-            Right someInstr -> do-              case someInstr of-                _ :/ (instr ::: hstOut)-> case interpretInstr dummyContractEnv instr stValues of-                  Right recOut -> do-                    lift $ put (SomeStack recOut hstOut)-                    printStack-                  Left michelsonFail -> putTextLn (pretty michelsonFail)-                _ :/ (AnyOutInstr _) -> putTextLn "Encountered a FAILWITH instruction"-            Left err -> printErr $ pretty err-          Nothing -> printErr "Casting stack failed"--printHelp :: ReplM ()-printHelp = putTextLn "REPL starts with an empty stack. At each instruction entered,\-  \ the modified stack, or an error is printed. Multiple instructions separated by semicolons should work\-  \ as expected. Available meta commads are:\n\-  \ ':help', displays this help\n ':stack', prints the current stack\n\-  \ ':parse <input>', tries to parse the given string using known formats\n\-  \ ':base58encode <input>', prints the base58 encoding of a bytestring\n\-  \ ':genkeys <seed>', generates a key pair with hash using the seed string \n\-  \ ':loadstack <filename>', loads the stack from a file\n\-  \ ':dumpstack <filename>', dumps the stack to a file \n\-  \ ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."--printStack :: ReplM ()-printStack = lift get >>= \case-  SomeStack stk hst -> do-    putTextLn "--"-    putTextLn $ showStack stk hst--emptyStack :: SomeStack-emptyStack = SomeStack RNil SNil--parseInstructions :: Text -> Either Text [ParsedOp]-parseInstructions src =-  case parseNoEnv ops MSUnspecified src of-    Right p -> Right p-    Left err -> Left (toText $ errorBundlePretty err)--tcOptions :: TypeCheckOptions-tcOptions = TypeCheckOptions-  { tcVerbose = False-  , tcStrict = False-  }---- helpers--addValueToHST-  :: forall t xs. T.SingI xs-  => T.Value t-  -> HST xs-  -> 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.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.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--dumpStackToFile :: FilePath -> ReplM ()-dumpStackToFile fname =- lift get >>= \case-  SomeStack stk hst -> case dumpStack stk hst of-    Right stkd -> liftIO $ Prelude.catch (BSL.writeFile fname $ Aeson.encode stkd) handler-    Left err -> printErr err-  where-    handler :: IOException -> IO ()-    handler e = printErr $ toText $ displayException e--loadStackFromFile :: FilePath -> ReplM ()-loadStackFromFile fname = do-  mStack <- liftIO $ flip Prelude.catch handler $ do-    stackTxt <- BSL.readFile fname-    case Aeson.decode @[(Text, Text)] stackTxt of-      Just s -> pure $ loadStack s-      Nothing -> pure $ Left "Decoding error when parsing stack data from file"-  case mStack of-    Right stk -> lift $ put stk-    Left err -> printErr err-  where-    handler :: IOException -> IO (Either Text a)-    handler e = pure $ Left $ toText $ displayException e---- | 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, _) ::& 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) : t)-      Left e -> Left e-    T.OpPresent ->  Left "Cannot dump stack with operations"---- | Overwrite the current stack with a stack loaded from a list of tuples--- representing (value/type) pairs.-loadStack :: [(Text, Text)] -> Either Text SomeStack-loadStack = foldl' buildStack (Right emptyStack) . reverse-  where-    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 type_ "" txTyp) of-        (Right val, Right typ) ->-          case typeCheckingWith tcOptions $ typeCheckParameter mempty typ val of-            Right (T.SomeValue tVal) ->-              case addValueToHST tVal hst of-                Right (T.Dict, newHst) -> Right $ SomeStack (tVal :& stk) newHst-                Left err -> Left err-            Left tcError -> Left $ pretty tcError-        (Left err, _) -> Left $ pretty err-        (_, Left err) -> Left $ toText $ errorBundlePretty err--showStack :: forall t. Rec T.Value t -> HST t -> Text-showStack RNil _ = "--"-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)-    _ ->          -- else just call show, and indicate value has operation inside-      case (v, T.sing @a) of-        (T.VList [], T.STList T.STOperation) -> "{ } :: list operation\n" <> showStack rst rHst-        _ -> addSuffix $ "(operations container:" <> pretty v <> ")"-  where-    addSuffix val = val <>" :: " <> renderType notes <> "\n" <> showStack rst rHst

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.19.1+version:        1.19.2 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@@ -32,6 +32,8 @@  library   exposed-modules:+      Morley.App.CLI+      Morley.App.REPL       Morley.AsRPC       Morley.CLI       Morley.Micheline@@ -39,6 +41,8 @@       Morley.Micheline.Binary.Internal       Morley.Micheline.Class       Morley.Micheline.Expression+      Morley.Micheline.Expression.Internal.MichelinePrimitive+      Morley.Micheline.Expression.Internal.TH       Morley.Micheline.Expression.WithMeta       Morley.Micheline.Json       Morley.Michelson.Analyzer@@ -54,6 +58,9 @@       Morley.Michelson.Macro       Morley.Michelson.Optimizer       Morley.Michelson.Optimizer.Internal.Proofs+      Morley.Michelson.Optimizer.Internal.Rules+      Morley.Michelson.Optimizer.Internal.Ruleset+      Morley.Michelson.Optimizer.Utils       Morley.Michelson.Parser       Morley.Michelson.Parser.Annotations       Morley.Michelson.Parser.Common@@ -122,6 +129,15 @@       Morley.Michelson.Typed.Operation       Morley.Michelson.Typed.Polymorphic       Morley.Michelson.Typed.Scope+      Morley.Michelson.Typed.Scope.Internal.CheckScope+      Morley.Michelson.Typed.Scope.Internal.Comparable+      Morley.Michelson.Typed.Scope.Internal.Deprecated+      Morley.Michelson.Typed.Scope.Internal.ForbidT+      Morley.Michelson.Typed.Scope.Internal.Presence+      Morley.Michelson.Typed.Scope.Internal.Scopes+      Morley.Michelson.Typed.Scope.Internal.TH+      Morley.Michelson.Typed.Scope.Internal.WellTyped+      Morley.Michelson.Typed.Scope.Internal.WithDeMorganScope       Morley.Michelson.Typed.Sing       Morley.Michelson.Typed.T       Morley.Michelson.Typed.TypeLevel@@ -134,6 +150,7 @@       Morley.Michelson.Untyped.Contract       Morley.Michelson.Untyped.Entrypoints       Morley.Michelson.Untyped.Ext+      Morley.Michelson.Untyped.HoistInstr       Morley.Michelson.Untyped.Instr       Morley.Michelson.Untyped.Type       Morley.Michelson.Untyped.Value@@ -263,10 +280,10 @@     , dependent-sum-template     , elliptic-curve     , first-class-families >=0.5.0.0-    , fmt >=0.6.3.0     , galois-field     , generic-deriving     , gitrev+    , haskeline     , hex-text     , hsblst     , lens@@ -278,6 +295,7 @@     , optparse-applicative     , pairing     , parser-combinators >=1.0.0+    , prettyprinter     , scientific     , semigroups >=0.19.1     , show-type@@ -298,13 +316,11 @@     , vector     , vinyl >=0.13.1     , with-utf8-    , wl-pprint-text   default-language: Haskell2010  executable morley   main-is: Main.hs   other-modules:-      REPL       Paths_morley   autogen-modules:       Paths_morley@@ -363,22 +379,8 @@       ViewPatterns   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode   build-depends:-      MonadRandom-    , aeson-    , base-noprelude >=4.7 && <5-    , base58-bytestring-    , bytestring-    , data-default-    , fmt-    , haskeline-    , hex-text-    , megaparsec >=7.0.0+      base-noprelude >=4.7 && <5     , morley     , morley-prelude-    , named     , optparse-applicative-    , singletons-    , text-    , vinyl-    , with-utf8   default-language: Haskell2010

@@ -0,0 +1,303 @@+-- SPDX-FileCopyrightText: 2021 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++module Morley.App.CLI+  ( argParser+  ) where++import Data.Default (def)+import Data.Singletons (demote)+import Data.Text.Lazy.IO.Utf8 qualified as Utf8 (writeFile)+import Fmt (pretty, prettyText, unlinesF)+import Named (paramF)+import Options.Applicative (help, long, short, subparser, switch)+import Options.Applicative qualified as Opt+import Text.Hex (encodeHex)++import Morley.App.REPL+import Morley.CLI+import Morley.Michelson.Analyzer (analyze)+import Morley.Michelson.Interpret (RemainingSteps(..))+import Morley.Michelson.Optimizer (OptimizerConf(..), optimizeVerboseWithConf)+import Morley.Michelson.Printer (printSomeContract, printTypedContract, printUntypedContract)+import Morley.Michelson.Runtime+import Morley.Michelson.Runtime.GState (genesisAddress)+import Morley.Michelson.TypeCheck (tcVerbose, typeCheckContract, typeCheckValue, typeCheckingWith)+import Morley.Michelson.TypeCheck qualified as TypeCheck+import Morley.Michelson.Typed (Contract'(..), SomeContract(..), unContractCode)+import Morley.Michelson.Typed qualified as T+import Morley.Michelson.Typed.Contract (mapContractCodeM)+import Morley.Tezos.Address+import Morley.Tezos.Address.Alias+import Morley.Tezos.Core (Mutez, tz)+import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey)+import Morley.Util.CLI (mkCLOptionParser, mkCommandParser, outputOption)+import Morley.Util.Named++data DryRunOrWrite = DryRun | Write++mkCommandParser' :: String -> String -> Opt.Parser a -> Opt.Mod Opt.CommandFields a+mkCommandParser' = flip . mkCommandParser++argParser :: Opt.Parser (IO ())+argParser = subparser $ mconcat+  [ printSubCmd+  , typecheckSubCmd+  , emulateSubCmd+  , optimizeSubCmd+  , analyzeSubCmd+  , createChestSubCmd+  , replSubCmd+  ]++--------------------------------------------------------------------------------+-- Subcommands+--------------------------------------------------------------------------------++-- NB: in case this looks mysterious, in IOCmd functions, outer 'do' is+-- Opt.Parser using ApplicativeDo, which then returns an IO action, i.e. inner+-- 'do' is 'IO ()'. -- @lierdakil++type IOCmd = Opt.Mod Opt.CommandFields (IO ())++typecheckSubCmd :: IOCmd+typecheckSubCmd = mkCommandParser' "typecheck" "Typecheck passed contract." do+  contractFile <- optional contractFileOption+  tcOptions <- typeCheckOptionsOption+  pure do+    morleyContract <- prepareContract contractFile+    -- 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 tcOptions+      $ typeCheckContract morleyContract+    when (TypeCheck.tcVerbose tcOptions) $+      putStrLn $ printSomeContract False contract+    putTextLn "Contract is well-typed"++printSubCmd :: IOCmd+printSubCmd = mkCommandParser' "print"+  "Parse a Morley contract and print corresponding Michelson \+  \contract that can be parsed by the OCaml reference client: octez-client."+  do+    mInputFile <- optional contractFileOption+    mOutputFile <- outputOption+    forceSingleLine <- onelineOption+    pure do+      contract <- prepareContract mInputFile+      let write = maybe putStrLn Utf8.writeFile mOutputFile+      write $ printUntypedContract forceSingleLine contract++emulateSubCmd :: IOCmd+emulateSubCmd = mkCommandParser' "emulate" "Set of commands to run in an emulated environment." $+  subparser $ mconcat+    [ runSubCmd+    , originateSubCmd+    , transferSubCmd+    , transferTicketSubCmd+    , runViewSubCmd+    ]++runSubCmd :: IOCmd+runSubCmd = mkCommandParser' "run"+  "Run passed contract. It's originated first and then a transaction is sent to it." do+    txData <- txDataOption+    contract <- contractSimpleOriginationDataOption+    cro <- commonRunOptions Write+    pure do+      michelsonContract <- traverse prepareContract contract+      void $ runContract cro michelsonContract txData++runViewSubCmd :: IOCmd+runViewSubCmd = mkCommandParser' "view"+  "Run some view on a contract either supplied directly or identified \+  \by an address. It's originated first if supplied directly." do+    cro <- commonRunOptions Write+    addressOrContract <-+      ContractSpecAddressOrAlias <$> addressOrAliasOption Nothing+        ! #name "contract-addr"+        ! #help "Contract address to call view on."+      <|> ContractSpecOrigination <$> contractSimpleOriginationDataOption+    viewName <- mkCLOptionParser Nothing+      ! #name "name"+      ! #help "View name."+    sender <- someAddressOrAliasOption+        (Just $ SAOAKindSpecified $ AddressResolved genesisAddress)+      ! #name "sender"+      ! #help "Sender address."+    viewArg <- TxUntypedParam <$> valueOption Nothing+      ! #name "arg"+      ! #help "View call argument."+    pure do+      contractSpec <- (traverse . traverse) prepareContract addressOrContract+      void $ runView cro contractSpec viewName sender viewArg++replSubCmd :: IOCmd+replSubCmd = mkCommandParser' "repl" "Start a Morley REPL." $ pure runRepl++originateSubCmd :: IOCmd+originateSubCmd = mkCommandParser' "originate" "Originate passed contract. Add it to passed DB." do+  simpleOriginationData <- contractSimpleOriginationDataOption+  dbPath <- dbPathOption+  tcOptions <- typeCheckOptionsOption+  verbose <- verboseFlag+  originator <- addressOption (Just genesisAddress)+    ! #name "originator"+    ! #help "Contract's originator."+  alias <- optional (aliasOption "alias")+  delegate <- optional $ keyHashOption Nothing+    ! #name "delegate"+    ! #help "Contract's optional delegate."+  pure do+    michelsonContract <- traverse prepareContract simpleOriginationData+    addr <-+      originateContract+        ! #dbPath dbPath+        ! #tcOpts tcOptions+        ! #originator originator+        ! paramF #alias alias+        ! paramF #delegate delegate+        ! #csod michelsonContract+        ! #verbose verbose+    putTextLn $ "Originated contract " <> pretty addr++transferSubCmd :: IOCmd+transferSubCmd = mkCommandParser' "transfer" "Transfer tokens to given address." do+  destination <- someAddressOrAliasOption Nothing+    ! #name "to"+    ! #help "Address or alias of the transfer's destination."+  txData <- txDataOption+  cro <- commonRunOptions DryRun+  pure $ transfer cro destination txData++transferTicketSubCmd :: IOCmd+transferTicketSubCmd = mkCommandParser' "transfer-ticket" "Transfer ticket to given address." do+  destination <- someAddressOrAliasOption Nothing+    ! #name "to"+    ! #help "Address or alias of the transfer's destination."+  tdSenderAddress :: L1Address <- Constrained <$> addressOption (Just genesisAddress)+    ! #name "sender" ! #help "Sender address"+  ticketer <- mkCLOptionParser @Address Nothing+    ! #name "ticketer" ! #help "Ticketer"+  value <- valueOption Nothing+    ! #name "value" ! #help "Ticket value"+  ty <- mkCLOptionParser Nothing+    ! #name "type" ! #help "Ticket argument type"+  tAmount <- mkCLOptionParser @Natural Nothing+    ! #name "amount" ! #help "Amount of tickets"+  tdAmount <- mutezOption (Just minBound)+    ! #name "mutez" ! #help "Mutez amount additionally sent by a transaction. \+    \Note that on network, as of Mumbai, implicit accounts can't send tickets \+    \and mutez in the same operation, however the Morley emulator allows it."+  tdEntrypoint <- entrypointOption+    ! #name "entrypoint" ! #help "Entrypoint to call"+  cro <- commonRunOptions DryRun+  pure $ T.withUType ty \(_ :: T.Notes t) -> do+    tValue <- either throwM pure . typeCheckingWith (croTCOpts cro) $+      typeCheckValue @t value+    T.Dict <- either (throwM . TypeCheck.UnsupportedTypeForScope (demote @t)) pure $+      T.checkScope @(T.ParameterScope t, T.Comparable t)+    let tdParameter = TxTypedParam $ T.VTicket ticketer tValue tAmount+    transfer cro destination TxData{..}++optimizeSubCmd :: IOCmd+optimizeSubCmd = mkCommandParser' "optimize" "Optimize the contract." do+  contractFile <- optional contractFileOption+  output <- outputOption+  singleLine <- onelineOption+  maxStageIterations <- mkCLOptionParser (Just $ ocMaxIterations def)+    ! #name "max-stage-iterations"+    ! #help "Maximum number of iterations per optimizer stage. \+        \The default is usually adequate, but you want to try raising it \+        \to see if it affects the result."+  verbose <- verboseFlag+  pure do+    untypedContract <- prepareContract contractFile+    SomeContract checkedContract <-+      either throwM pure . typeCheckingWith laxTcOptions $+        typeCheckContract untypedContract+    let (logs, optimizedContract) =+          mapContractCodeM (optimizeVerboseWithConf conf) checkedContract+        conf = def { ocMaxIterations = maxStageIterations }+    maybe putStrLn Utf8.writeFile output $ printTypedContract singleLine optimizedContract+    when verbose $ hPutStrLn stderr $ prettyText $ unlinesF logs++analyzeSubCmd :: IOCmd+analyzeSubCmd = mkCommandParser' "analyze" "Analyze the contract." do+  contractFile <- optional contractFileOption+  pure do+    untypedContract <- prepareContract contractFile+    SomeContract contract <-+      either throwM pure . typeCheckingWith laxTcOptions $+        typeCheckContract untypedContract+    putTextLn $ pretty $ analyze (unContractCode $ cCode contract)++createChestSubCmd :: IOCmd+createChestSubCmd = mkCommandParser' "create_chest" "Create a timelocked chest and key." do+  payload <- payloadOption+  time <- timeOption+  pure do+    (chest, key) <- createChestAndChestKey payload time+    putStrLn $ "Chest: 0x" <> encodeHex (chestBytes chest)+    putStrLn $ "Key: 0x" <> encodeHex (chestKeyBytes key)++--------------------------------------------------------------------------------+-- Parsers+--------------------------------------------------------------------------------++verboseFlag :: Opt.Parser Bool+verboseFlag = switch $+  short 'v' <>+  long "verbose" <>+  help "Whether output should be verbose."++typeCheckOptionsOption :: Opt.Parser TypeCheck.TypeCheckOptions+typeCheckOptionsOption = do+  tcVerbose <- verboseFlag+  tcStrict <- fmap not . switch $+    long "typecheck-lax" <>+    help "Whether actions permitted in `octez-client run` but forbidden in \+          \e.g. `octez-client originate` should be allowed here."+  return TypeCheck.TypeCheckOptions{..}++commonRunOptions :: DryRunOrWrite -> Opt.Parser CommonRunOptions+commonRunOptions defaultDryRun = do+  croNow <- nowOption+  croLevel <- fromMaybe (croLevel def) <$> levelOption+  croMinBlockTime <- fromMaybe (croMinBlockTime def) <$> minBlockTimeOption+  croMaxSteps <- RemainingSteps <$> maxStepsOption+  croDBPath <- dbPathOption+  croTCOpts <- typeCheckOptionsOption+  croVerbose <- verboseFlag+  croDryRun <- case defaultDryRun of+    Write -> fmap not . switch $+      long "write" <>+      help "Write updated DB to the DB file."+    DryRun -> switch $+      long "dry-run" <>+      help "Do not write updated DB to the DB file."+  pure CommonRunOptions{..}++contractSimpleOriginationDataOption :: Opt.Parser (ContractSimpleOriginationData (Maybe FilePath))+contractSimpleOriginationDataOption = do+  csodStorage <- valueOption Nothing+    ! #name "storage"+    ! #help "Initial storage of the contract."+  csodContract <- optional contractFileOption+  csodBalance <- mutezOption (Just defaultBalance)+    ! #name "balance"+    ! #help "Initial balance of the contract."+  pure ContractSimpleOriginationData{..}++--------------------------------------------------------------------------------+-- Constants+--------------------------------------------------------------------------------++defaultBalance :: Mutez+defaultBalance = [tz|4|]++-- | Most permitting options, when we don't care much about typechecking.+laxTcOptions :: TypeCheck.TypeCheckOptions+laxTcOptions = TypeCheck.TypeCheckOptions+  { TypeCheck.tcVerbose = False+  , TypeCheck.tcStrict = False+  }

@@ -0,0 +1,318 @@+-- SPDX-FileCopyrightText: 2021 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA+{-|+Implements an REPL that can execute Morley instructions.  REPL starts with an+empty stack. At each instruction entered, the modified stack, or an error is+printed. Multiple instructions separated by semicolons should work as expected.+Available meta commads are:++ ':help', displays this help\n ':stack', prints the current stack+ ':loadstack filename', loads the stack from a file+ ':dumpstack filename', dumps the stack to a file+ ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."+-}+module Morley.App.REPL+  ( runRepl+  ) where++import Prelude hiding (group)++import Control.Exception (IOException)+import Control.Monad.Random (randomIO)+import Data.Aeson qualified as Aeson+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(..))+import Fmt (Doc, build, pretty)+import Prettyprinter (align, group, line, nest)+import System.Console.Haskeline+  (InputT, Interrupt(..), defaultSettings, getInputLine, runInputT, withInterrupt)+import Text.Megaparsec (parse)++import Morley.Michelson.Interpret (interpretInstr)+import Morley.Michelson.Macro (ParsedOp, expand)+import Morley.Michelson.Parser+  (errorBundlePretty, parseExpandValue, parseNoEnv, rawOpsSequence, type_)+import Morley.Michelson.Parser.Types (MichelsonSource(..))+import Morley.Michelson.Printer.Util (printRenderDoc)+import Morley.Michelson.Runtime.Dummy+import Morley.Michelson.Runtime.Import (readValue)+import Morley.Michelson.TypeCheck+  (SomeTcInstr(..), SomeTcInstrOut(..), TypeCheckOptions(..), runTypeCheckIsolated,+  typeCheckingWith)+import Morley.Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter)+import Morley.Michelson.TypeCheck.Types (HST(..))+import Morley.Michelson.Typed qualified as T+import Morley.Tezos.Crypto+import Morley.Util.Sing (castSing)+import Text.Hex (decodeHex, encodeHex)++data SomeStack = forall t. T.SingI t => SomeStack+  { stValues :: (Rec T.Value t)+  , stTypes :: HST t+  }++type ReplM = InputT (StateT SomeStack IO)++runRepl :: IO ()+runRepl = evalStateT (runInputT defaultSettings repl) emptyStack++-- | Prints an error message to stderr+printErr :: (MonadIO m) => Text -> m ()+printErr m = liftIO $ hPutStrLn stderr m++-- | Read commands or instructions from stdin and executes them.+-- If user presses Ctrl-c during execution of an instruction, it will be+-- caught and handled here itself. This ensures that REPL does not crash as+-- a result of user pressing Ctrl-c in an attempt to end a loop.+repl :: ReplM ()+repl = do+  printHelp+  repl_++repl_ :: ReplM ()+repl_ = do+   minput <- getInputLine "Morley>>> "+   case strStrip <$> minput of+     Nothing -> pass -- Ctrl D+     Just ":quit" -> pass+     Just input -> do+      case input of+        "" -> pass+        ":clear" -> lift $ put emptyStack+        ":stack" -> printStack+        ":help" -> printHelp+        (stripPrefixNonEmpty ":dumpstack" -> Just filename) ->+          dumpStackToFile $ toString $ strip $ toText filename+        (stripPrefixNonEmpty ":loadstack" -> Just filename) ->+          loadStackFromFile $ toString $ strip $ toText filename+        (stripPrefixNonEmpty ":parse" -> Just parseInput) ->+          tryParse $ strip $ toText parseInput+        (stripPrefixNonEmpty ":base58encode" -> Just parseInput) ->+          base58Encode $ strip $ toText parseInput+        (stripPrefix ":genkeys" -> Just mseed) -> do+           seed <- case mseed of+             "" -> show <$> (liftIO (randomIO @Word64))+             seed -> pure seed+           let sk = detSecretKey (encodeUtf8 seed)+           let pk = toPublic sk+           let pkh = hashKey pk+           printResult "Secret Key" (formatSecretKey sk)+           printResult "Public Key" (formatPublicKey pk)+           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)+      repl_+  where+    strStrip = toString . strip . toText+    stripPrefixNonEmpty p i = case stripPrefix p i of+      Just "" -> Nothing+      x -> x++base58Encode :: Text -> ReplM ()+base58Encode inp = case decodeHex $ fromMaybe inp $ (T.stripPrefix "0x" inp) of+  Just b -> do+    printResult "Base58encode" $ decodeUtf8 $ Base58.encodeBase58 Base58.bitcoinAlphabet b+    printResult "Base58encode with checksum" $ encodeBase58Check b+  Nothing -> putTextLn "Can't parse input as hex-encoded bytes"++tryParseMichelsonValue :: forall (t :: T.T). (T.SingI t) => Text -> Text -> ReplM ()+tryParseMichelsonValue msg parseInput =+  case readValue @t MSStdin parseInput of+    Right s -> printResult msg $ pretty s+    Left _ -> pass++underlined :: MonadIO m => Text -> m ()+underlined x = liftIO do+  putTextLn x+  putTextLn $ T.replicate (T.length x) "-"++printResult :: MonadIO m => Text -> Text -> m ()+printResult heading result = do+  underlined heading+  putTextLn result+  putTextLn ""++tryParse :: Text -> ReplM ()+tryParse parseInput = do+  tryParseMichelsonValue @'T.TKey "Michelson Key" parseInput+  tryParseMichelsonValue @'T.TUnit "Michelson Unit" parseInput+  tryParseMichelsonValue @'T.TSignature "Michelson Signature" parseInput+  tryParseMichelsonValue @'T.TChainId "Michelson ChainId" parseInput+  tryParseMichelsonValue @'T.TTimestamp "Michelson Timestamp" parseInput+  tryParseMichelsonValue @'T.TAddress "Michelson Address" parseInput+  tryParseMichelsonValue @'T.TString "Michelson String" parseInput+  tryParseMichelsonValue @'T.TInt "Michelson Int" parseInput+  tryParseMichelsonValue @'T.TNat "Michelson Nat" parseInput+  tryParseMichelsonValue @'T.TBytes "Michelson Bytes" parseInput+  tryParseMichelsonValue @'T.TMutez "Michelson Mutez" parseInput+  tryParseMichelsonValue @'T.TKeyHash "Michelson KeyHash" parseInput+  tryParseMichelsonValue @'T.TBls12381Fr "Michelson Bls12381Fr" parseInput+  tryParseMichelsonValue @'T.TBls12381G1 "Michelson Bls12381G1" parseInput+  tryParseMichelsonValue @'T.TBls12381G2 "Michelson Bls12381G2" parseInput+  tryParseMichelsonValue @'T.TBool "Michelson Bool" parseInput++  case parsePublicKey parseInput of+    Right p -> do+      printResult "Public Key" $ formatPublicKey p+    Left _ -> pass+  case parseSignature parseInput of+    Right p -> do+      printResult "Signature" $ formatSignature p+    Left _ -> pass+  case parseSecretKey parseInput of+    Right p -> do+      printResult "Secret Key" $ formatSecretKey p+    Left _ -> pass+  case parseHash @'HashKindPublicKey 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)+    Nothing -> pass+  case decodeBase58Check parseInput of+    Just p -> do+      printResult "Base58Check Encoded Bytes" $ "0x" <> (encodeHex p)+    Nothing -> pass++-- | Try to execute the given input string as a Morley instruction.+runCode :: Text -> ReplM ()+runCode code = do+  case parseInstructions code of+    Left err -> printErr err+    Right [] -> pass+    Right parsedOps -> do+      let expandedOps = expand <$> parsedOps+      lift get >>= \case+        SomeStack {..} -> case castSing stTypes of+          Just hstInp -> case typeCheckingWith tcOptions . runTypeCheckIsolated $+                                typeCheckList expandedOps hstInp of+            Right someInstr -> do+              case someInstr of+                _ :/ (instr ::: hstOut)-> case interpretInstr dummyContractEnv instr stValues of+                  Right recOut -> do+                    lift $ put (SomeStack recOut hstOut)+                    printStack+                  Left michelsonFail -> putTextLn (pretty michelsonFail)+                _ :/ (AnyOutInstr _) -> putTextLn "Encountered a FAILWITH instruction"+            Left err -> printErr $ pretty err+          Nothing -> printErr "Casting stack failed"++printHelp :: ReplM ()+printHelp = putTextLn "REPL starts with an empty stack. At each instruction entered,\+  \ the modified stack, or an error is printed. Multiple instructions separated by semicolons should work\+  \ as expected. Available meta commads are:\n\+  \ ':help', displays this help\n ':stack', prints the current stack\n\+  \ ':parse <input>', tries to parse the given string using known formats\n\+  \ ':base58encode <input>', prints the base58 encoding of a bytestring\n\+  \ ':genkeys <seed>', generates a key pair with hash using the seed string \n\+  \ ':loadstack <filename>', loads the stack from a file\n\+  \ ':dumpstack <filename>', dumps the stack to a file \n\+  \ ':clear', clears the current stack. Ctrl-D or ':quit' to end REPL."++printStack :: ReplM ()+printStack = lift get >>= \case+  SomeStack stk hst -> do+    putTextLn "--"+    putTextLn $ pretty $ showStack stk hst++emptyStack :: SomeStack+emptyStack = SomeStack RNil SNil++parseInstructions :: Text -> Either Text [ParsedOp]+parseInstructions src =+  case parseNoEnv (rawOpsSequence $ pure ()) MSUnspecified src of+    Right p -> Right p+    Left err -> Left (toText $ errorBundlePretty err)++tcOptions :: TypeCheckOptions+tcOptions = TypeCheckOptions+  { tcVerbose = False+  , tcStrict = False+  }++-- helpers++addValueToHST+  :: forall t xs. T.SingI xs+  => T.Value t+  -> HST xs+  -> 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.sing @t, wtpDict) ::&  hstIn)+    Left e -> Left $ pretty e++dumpStackToFile :: FilePath -> ReplM ()+dumpStackToFile fname =+ lift get >>= \case+  SomeStack stk hst -> case dumpStack stk hst of+    Right stkd -> liftIO $ Prelude.catch (BSL.writeFile fname $ Aeson.encode stkd) handler+    Left err -> printErr err+  where+    handler :: IOException -> IO ()+    handler e = printErr $ toText $ displayException e++loadStackFromFile :: FilePath -> ReplM ()+loadStackFromFile fname = do+  mStack <- liftIO $ flip Prelude.catch handler $ do+    stackTxt <- BSL.readFile fname+    case Aeson.decode @[(Text, Text)] stackTxt of+      Just s -> pure $ loadStack s+      Nothing -> pure $ Left "Decoding error when parsing stack data from file"+  case mStack of+    Right stk -> lift $ put stk+    Left err -> printErr err+  where+    handler :: IOException -> IO (Either Text a)+    handler e = pure $ Left $ toText $ displayException e++-- | Dump stack as a list 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, _) ::& rHst) = case T.valueTypeSanity v of+  T.Dict -> case T.checkTPresence T.SPSOp (T.sing @a) of+    T.TAbsent -> case dumpStack rst rHst of+      Right t -> Right $ (printRenderDoc True v, printRenderDoc True (fromSing notes)) : t+      Left e -> Left e+    T.TPresent ->  Left "Cannot dump stack with operations"++-- | Overwrite the current stack with a stack loaded from a list of tuples+-- representing (value/type) pairs.+loadStack :: [(Text, Text)] -> Either Text SomeStack+loadStack = foldl' buildStack (Right emptyStack) . reverse+  where+    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 type_ "" txTyp) of+        (Right val, Right typ) ->+          case typeCheckingWith tcOptions $ typeCheckParameter mempty typ val of+            Right (T.SomeValue tVal) ->+              case addValueToHST tVal hst of+                Right (T.Dict, newHst) -> Right $ SomeStack (tVal :& stk) newHst+                Left err -> Left err+            Left tcError -> Left $ pretty tcError+        (Left err, _) -> Left $ pretty err+        (_, Left err) -> Left $ toText $ errorBundlePretty err++showStack :: forall t. Rec T.Value t -> HST t -> Doc+showStack RNil _ = "--"+showStack ((v :: T.Value a) :& rst) ((notes, _) ::& rHst)  = case T.valueTypeSanity v of+  T.Dict -> case T.checkTPresence T.SPSOp (T.sing @a) of+    T.TAbsent -> -- print nice if value has no operations+      addSuffix (build v)+    T.TPresent ->          -- else just call show, and indicate value has operation inside+      case (v, T.sing @a) of+        (T.VList [], T.STList T.STOperation) -> "{ } :: list operation\n" <> showStack rst rHst+        _ -> addSuffix $ "(operations container:" <> pretty v <> ")"+  where+    addSuffix val =+      nest 2 (group $ val <> line <> ":: " <> align (pretty notes)) <> line <> showStack rst rHst

@@ -26,29 +26,26 @@ import Prelude qualified  import Control.Lens.Plated (universe)-import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))+import Data.Constraint ((\\)) import Data.Default (Default(..))-import Data.Generics (everything, mkQ)+import Data.Generics (everything, everywhere, mkQ, mkT) import Data.List qualified as List ((\\)) import Data.Map qualified as Map import Data.Singletons (Sing, withSingI) import Data.Text qualified as T+import Data.Type.Equality ((:~:)(Refl)) 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(..), conT, cxt, instanceD, location, lookupTypeName, mkName,-  nameBase, normalB, ppr, reify, reifyInstances, standaloneDerivWithStrategyD, valD, varE, varP)+  (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD), Info(TyConI), Kind,+  Loc(loc_module), Name, Q, TyLit(StrTyLit), TySynEqn(..), TyVarBndr(..), Type(..), conT, cxt,+  instanceD, location, lookupTypeName, mkName, nameBase, normalB, ppr, reify, reifyInstances, valD,+  varE, varP) import Language.Haskell.TH qualified as TH import Language.Haskell.TH.ReifyMany (reifyManyTyCons)-import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)+import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames, unAppsT, unSigT)  import Morley.Michelson.Text (MText) import Morley.Michelson.Typed-  (BigMap, BigMapId, ContractPresence(ContractAbsent), ContractRef, EpAddress, HasNoBigMap,-  HasNoContract, HasNoNestedBigMaps, HasNoOp, IsoValue, Notes(..), OpPresence(..), Operation,-  SingI(sing), SingT(..), StorageScope, T(..), ToT, Value, Value'(..), WellTyped,-  checkContractTypePresence, checkOpPresence, withDict) import Morley.Tezos.Address (Address) import Morley.Tezos.Core (ChainId, Mutez, Timestamp) import Morley.Tezos.Crypto@@ -57,14 +54,25 @@   mangleGenericStrategyConstructors, mangleGenericStrategyFields, reifyDataType) import Morley.Util.Interpolate (itu) import Morley.Util.Named hiding (Name)+import Morley.Util.StubbedProof (stubProof) import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail)  {-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-} --- $setup--- >>> import Morley.Michelson.Typed--- >>> import Morley.Michelson.Text (MText)+{- $setup+>>> import Morley.Michelson.Typed+>>> import Morley.Michelson.Text (MText)+>>> import Data.Default (def)+>>> :{+-- mock definitions for doctests, mirroring those in Lorentz.+data FollowEntrypointFlag = FollowEntrypoint | NotFollowEntrypoint+class HasAnnotation a where+  getAnnotation :: FollowEntrypointFlag -> Notes (ToT a)+  annOptions :: ()+:}+-} + ---------------------------------------------------------------------------- -- TAsRPC ----------------------------------------------------------------------------@@ -300,38 +308,58 @@ {- | Derive an RPC representation for a type, as well as instances for 'Generic', 'IsoValue', 'HasRPCRepr' and optionally @HasAnnotation@. -> data ExampleStorage a b = ExampleStorage->   { esField1 :: Integer->   , esField2 :: [BigMap Integer MText]->   , esField3 :: a->   }->   deriving stock Generic->   deriving anyclass IsoValue->-> deriveRPC "ExampleStorage"+>>> :{+data ExampleStorage a b = ExampleStorage+  { esField1 :: Integer+  , esField2 :: [BigMap Integer MText]+  , esField3 :: a+  }+  deriving stock Generic+  deriving anyclass IsoValue+--+deriveRPC "ExampleStorage"+:}  Will generate: -> data ExampleStorageRPC a b = ExampleStorageRPC->   { esField1RPC :: AsRPC Integer->   , esField2RPC :: AsRPC [BigMap Integer MText]->   , esField3RPC :: AsRPC a->   }->-> instance HasRPCRepr a => HasRPCRepr (ExampleStorage a b) where->   type AsRPC (ExampleStorage a b) = ExampleStorageRPC a b-> deriving anyclass instance (IsoValue (AsRPC a), IsoValue (AsRPC b)) => IsoValue (ExampleStorageRPC a b)-> instance Generic (ExampleStorageRPC a b) where->   ...+>>> :i ExampleStorageRPC+...+data ExampleStorageRPC a b+  = ExampleStorageRPC {esField1RPC :: !(AsRPC Integer),+                       esField2RPC :: !(AsRPC [BigMap Integer MText]),+                       esField3RPC :: !(AsRPC a)}+...+instance forall a k (b :: k).+         IsoValue (AsRPC a) =>+         IsoValue (ExampleStorageRPC a b)+...+instance forall a k (b :: k). Generic (ExampleStorageRPC a b)+... -When 'droHasAnnotation' is @True@, it will also generate a @HasAnnotation@ (from-@Lorentz@) instance like:+>>> :i HasRPCRepr+...+instance forall a k (b :: k).+         HasRPCRepr a =>+         HasRPCRepr (ExampleStorage a b)+... -> instance With [HasAnnotation, HasRPCRepr] ExampleStorage->   => HasAnnotation ExampleStorageRPC where->   getAnnotation = notesAsRPC . getAnnotation @ExampleStorage->   annOptions = annOptions @ExampleStorage+>>> :i AsRPC+...+type instance forall k a (b :: k). AsRPC (ExampleStorage a b)+  = ExampleStorageRPC a b+... ++When 'droHasAnnotation' is @True@ (the default), it will also generate a+@HasAnnotation@ (from @Lorentz@) instance like:++>>> :i HasAnnotation+...+instance forall a k (b :: k).+         With '[HasAnnotation, HasRPCRepr] (ExampleStorage a b) =>+         HasAnnotation (ExampleStorageRPC a b)+...+ Note that if the type doesn't contain type variables or only contains phantom type variables, 'HasRPCRepr' constraint is omitted, as it would be redundant. @@ -339,16 +367,26 @@  Void types will generate a type synonym instead, e.g. -> data MyVoidType->   deriving stock Generic->   deriving anyclass IsoValue+>>> :{+data MyVoidType+  deriving stock Generic+  deriving anyclass IsoValue+--+deriveRPC "MyVoidType"+:}  will produce -> instance HasRPCRepr MyVoidType where->   type AsRPC MyVoidType = MyVoidTypeRPC-> type MyVoidTypeRPC = MyVoidType+>>> :i AsRPC+...+type instance AsRPC MyVoidType = MyVoidTypeRPC+... +>>> :i MyVoidTypeRPC+...+type MyVoidTypeRPC = MyVoidType+...+ When 'droRecursive' is @True@, recursively enumerate @data@, @newtype@ and @type@ declarations, and derive an RPC representation for each type that doesn't yet have one. This will however silently skip over void types that do not have@@ -360,17 +398,69 @@ types somewhere. The algorithm isn't smart enough to figure out those don't need RPC representation and will try to derive it anyway. -In this example, this will generate an RPC representation for @A@ and @B@, but-not for @C@ (because we explicitly said we don't want one) or @D@ (because it-already has one).+>>> :{+data B = B deriving (Generic, IsoValue)+data C = C deriving (Generic, IsoValue)+data D = D deriving (Generic, IsoValue)+data E a = E deriving (Generic, IsoValue)+--+instance HasRPCRepr D where type AsRPC D = ()+--+data A = A B (E C) D deriving (Generic, IsoValue)+deriveRPCWithOptions "A" def{droRecursive=True, droRecursiveSkipTypes=["C"]}+:} -> data B = B-> data C = C-> data D = D-> deriveRPC "D"->-> data A = A B C D-> deriveRPCWithOptions "A" def{droRecursive=True, droRecursiveSkipTypes=["C"]}+In this example, this will generate an RPC representation for @A@ and @B@,++>>> :i ARPC+...+data ARPC = ...+...+>>> :i BRPC+...+data BRPC = ...+...++but not for @C@ (because we explicitly said we don't want one) or @D@ (because+it already has one).++>>> :i CRPC+...+... Not in scope: ...+...+>>> :i DRPC+...+... Not in scope: ...+...++When using with @droRecursive = False@, if some types do not have 'HasRPCRepr',+'IsoValue' or 'Generic' instances, but need to, an error will be raised:++>>> :{+data B = B deriving (Generic, IsoValue)+data A = A B deriving (Generic, IsoValue)+--+deriveRPCWithOptions "A" def{droRecursive = False}+:}+...+... error:+... Type ... must implement 'HasRPCRepr'.++>>> :{+data B = B deriving (Generic, IsoValue)+data A = A B deriving (Generic, IsoValue)+--+deriveRPCWithOptions "B" def{droRecursive = False}+deriveRPCWithOptions "A" def{droRecursive = False}+:}++>>> :i AsRPC+...+type instance AsRPC B = BRPC ...+type instance AsRPC A = ARPC ...+...++This check isn't very smart, so it might miss some corner cases. -} deriveRPCWithOptions :: String -> DeriveRPCOptions -> Q [Dec] deriveRPCWithOptions typeStr opts@DeriveRPCOptions{droRecursive}@@ -448,10 +538,9 @@         , pure $ TySynD typeNameRPC [] $ ConT typeName         ]   else do-    -- TODO [#722]: use `reifyInstances` to check that 'AsRPC' exists for `fieldType`-    -- Print user-friendly error msg if it doesn't.     constructorsRPC <- traverse convertConstructor constructors     fieldTypes <- getFieldTypes constructors+    forM_ fieldTypes checkInstanceForFieldTy     fieldTypesRPC <- getFieldTypes constructorsRPC      -- Note: we can't use `makeRep0Inline` to derive a `Rep` instance for `derivedTypeRPC`@@ -484,6 +573,37 @@       ]    where+    checkInstanceForFieldTy fieldTy =+      reifyInstances ''HasRPCRepr [fieldTy] >>= \case+        [] | droRecursive -> pass+           | otherwise+           -> fail $ "Type '" <> show (ppr fieldTy) <> "' must implement 'HasRPCRepr'."+        [TH.InstanceD _ cs (ConT n' `AppT` ty) _] | n' == ''HasRPCRepr -> do+          let tyMap = Map.fromList $ filter isVarMapping $+                zip (unSigT <$> unAppsT ty) (unSigT <$> unAppsT fieldTy)+              isVarMapping = \case+                (VarT{}, _) -> True+                _ -> False+              instantiatedConstraints =+                map (everywhere (mkT substVar)) . concatMap getHasRPCReprTys $+                  everywhere (mkT unSigT) cs+              getHasRPCReprTys = \case+                ConT n `AppT` x | n == ''HasRPCRepr -> [x]+                ConT n `AppT` (PromotedConsT `AppT` ConT n2 `AppT` PromotedNilT) `AppT` xs+                  | n == ''Each, n2 == ''HasRPCRepr -> flip unfoldr xs \case+                      PromotedNilT -> Nothing+                      PromotedConsT `AppT` x `AppT` xs' -> Just (x, xs')+                      _ -> Nothing+                _ -> [] -- we could error here and above, but for safety we don't+              substVar = \case+                v@VarT{} | Just s <- Map.lookup v tyMap -> s+                x -> x+          forM_ instantiatedConstraints checkInstanceForFieldTy+        [d] -> fail $ "Unexpected instance for " <> show (ppr fieldTy) <> ": " <> show (ppr d)+        -- most likely fieldTy is a tyvar, if not, GHC will complain about+        -- duplicate instances anyway+        (_:_:_) -> pass+     -- Given the field type @FieldType a b@, returns @AsRPC (FieldType a b)@.     convertFieldType :: Type -> Type     convertFieldType tp = ConT ''AsRPC `AppT` tp@@ -583,13 +703,13 @@      -- Given the type @Foo a b = Foo (Bar a)@, generate an 'IsoValue' instance like:     ---    -- > deriving anyclass instance IsoValue (AsRPC (Bar a)) => IsoValue (FooRPC a b)+    -- > instance IsoValue (AsRPC (Bar a)) => IsoValue (FooRPC a b)     --     -- Note that if a type variable @t@ is a phantom type variable, then no @IsoValue (AsRPC t)@     -- constraint is generated for it.     mkIsoValueInstance :: [Type] -> Type -> Q [Dec]     mkIsoValueInstance fieldTypes tp =-      one <$> standaloneDerivWithStrategyD (Just AnyclassStrategy) constraints [t|IsoValue $(pure tp)|]+      one <$> instanceD constraints [t|IsoValue $(pure tp)|] []       where         constraints :: Q Cxt         constraints =@@ -676,52 +796,45 @@ -- -- Throws an error if it finds a big_map without an ID. valueAsRPC :: HasCallStack => Value t -> Value (TAsRPC t)-valueAsRPC v =-  case v of-    VKey {} -> v-    VUnit {} -> v-    VSignature {} -> v-    VChainId {} -> v-    VChest {} -> v-    VChestKey {} -> v-    VOption (vMaybe :: Maybe (Value elem)) ->-      withDict (rpcSingIEvi @elem) $-        VOption $ valueAsRPC <$> vMaybe-    VList (vList :: [Value elem]) ->-      withDict (rpcSingIEvi @elem) $-        VList $ valueAsRPC <$> vList-    VSet {} -> v-    VOp {} -> v-    VContract {} -> v-    VTicket {} -> v-    VPair (x, y) -> VPair (valueAsRPC x, valueAsRPC y)-    VOr (vEither :: Either (Value l) (Value r)) ->-      withDict (rpcSingIEvi @l *** rpcSingIEvi @r) $-        case vEither of-          Right r -> VOr (Right (valueAsRPC r))-          Left l -> VOr (Left (valueAsRPC l))-    VLam {} -> v-    VMap (vMap :: Map (Value k) (Value v)) ->-      withDict (rpcSingIEvi @v) $-        VMap $ valueAsRPC <$> vMap-    VBigMap (Just bmId) _ -> VNat bmId-    VBigMap Nothing _ ->-      error $ unlines-        [ "Expected all big_maps to have an ID, but at least one big_map didn't."-        , "This is most likely a bug."-        ]-    VInt {} -> v-    VNat {} -> v-    VString {} -> v-    VBytes {} -> v-    VMutez {} -> v-    VBool {} -> v-    VKeyHash {} -> v-    VTimestamp {} -> v-    VAddress {} -> v-    VBls12381Fr {} -> v-    VBls12381G1 {} -> v-    VBls12381G2 {} -> v+valueAsRPC v = case v of+  VKey {} -> v+  VUnit {} -> v+  VSignature {} -> v+  VChainId {} -> v+  VChest {} -> v+  VChestKey {} -> v+  VOption (vMaybe :: Maybe (Value elem)) ->+    VOption (valueAsRPC <$> vMaybe) \\ rpcSingIEvi @elem+  VList (vList :: [Value elem]) ->+    VList (valueAsRPC <$> vList) \\ rpcSingIEvi @elem+  VSet {} -> v+  VOp {} -> v+  VContract {} -> v+  VTicket {} -> v+  VPair (x, y) -> VPair (valueAsRPC x, valueAsRPC y)+  VOr (vEither :: Either (Value l) (Value r)) ->+    VOr (bimap valueAsRPC valueAsRPC vEither) \\ rpcSingIEvi @l \\ rpcSingIEvi @r+  VLam {} -> v+  VMap (vMap :: Map (Value k) (Value v)) ->+    VMap (valueAsRPC <$> vMap) \\ rpcSingIEvi @v+  VBigMap (Just bmId) _ -> VNat bmId+  VBigMap Nothing _ ->+    error $ unlines+      [ "Expected all big_maps to have an ID, but at least one big_map didn't."+      , "This is most likely a bug."+      ]+  VInt {} -> v+  VNat {} -> v+  VString {} -> v+  VBytes {} -> v+  VMutez {} -> v+  VBool {} -> v+  VKeyHash {} -> v+  VTimestamp {} -> v+  VAddress {} -> v+  VBls12381Fr {} -> v+  VBls12381G1 {} -> v+  VBls12381G2 {} -> v  -- | Replaces all bigmap IDs with their corresponding bigmap values. -- This is the inverse of `valueAsRPC`.@@ -778,42 +891,41 @@  -- | Replace all @big_map@ annotations in a value with @nat@ annotations. notesAsRPC :: Notes t -> Notes (TAsRPC t)-notesAsRPC notes =-  case notes of-    NTKey {} -> notes-    NTUnit {} -> notes-    NTSignature {} -> notes-    NTChainId {} -> notes-    NTChest {} -> notes-    NTChestKey {} -> notes-    NTOption typeAnn elemNotes -> NTOption typeAnn $ notesAsRPC elemNotes-    NTList typeAnn elemNotes -> NTList typeAnn $ notesAsRPC elemNotes-    NTSet {} -> notes-    NTOperation {} -> notes-    NTContract {} -> notes-    NTTicket {} -> notes-    NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 notes1 notes2 ->-      NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 (notesAsRPC notes1) (notesAsRPC notes2)-    NTOr typeAnn fieldAnn1 fieldAnn2 notes1 notes2 ->-      NTOr typeAnn fieldAnn1 fieldAnn2 (notesAsRPC notes1) (notesAsRPC notes2)-    NTLambda {} -> notes-    NTMap typeAnn keyAnns valueNotes -> NTMap typeAnn keyAnns (notesAsRPC valueNotes)-    NTBigMap typeAnn _ _ -> NTNat typeAnn-    NTInt {} -> notes-    NTNat {} -> notes-    NTString {} -> notes-    NTBytes {} -> notes-    NTMutez {} -> notes-    NTBool {} -> notes-    NTKeyHash {} -> notes-    NTTimestamp {} -> notes-    NTAddress {} -> notes-    NTBls12381Fr {} -> notes-    NTBls12381G1 {} -> notes-    NTBls12381G2 {} -> notes-    NTNever {} -> notes-    NTSaplingState {} -> notes-    NTSaplingTransaction {} -> notes+notesAsRPC notes = case notes of+  NTKey {} -> notes+  NTUnit {} -> notes+  NTSignature {} -> notes+  NTChainId {} -> notes+  NTChest {} -> notes+  NTChestKey {} -> notes+  NTOption typeAnn elemNotes -> NTOption typeAnn $ notesAsRPC elemNotes+  NTList typeAnn elemNotes -> NTList typeAnn $ notesAsRPC elemNotes+  NTSet {} -> notes+  NTOperation {} -> notes+  NTContract {} -> notes+  NTTicket {} -> notes+  NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 notes1 notes2 ->+    NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 (notesAsRPC notes1) (notesAsRPC notes2)+  NTOr typeAnn fieldAnn1 fieldAnn2 notes1 notes2 ->+    NTOr typeAnn fieldAnn1 fieldAnn2 (notesAsRPC notes1) (notesAsRPC notes2)+  NTLambda {} -> notes+  NTMap typeAnn keyAnns valueNotes -> NTMap typeAnn keyAnns (notesAsRPC valueNotes)+  NTBigMap typeAnn _ _ -> NTNat typeAnn+  NTInt {} -> notes+  NTNat {} -> notes+  NTString {} -> notes+  NTBytes {} -> notes+  NTMutez {} -> notes+  NTBool {} -> notes+  NTKeyHash {} -> notes+  NTTimestamp {} -> notes+  NTAddress {} -> notes+  NTBls12381Fr {} -> notes+  NTBls12381G1 {} -> notes+  NTBls12381G2 {} -> notes+  NTNever {} -> notes+  NTSaplingState {} -> notes+  NTSaplingTransaction {} -> notes  ---------------------------------------------------------------------------- -- Entailments@@ -821,58 +933,50 @@  -- | A proof that if a singleton exists for @t@, -- then so it does for @TAsRPC t@.-rpcSingIEvi :: forall (t :: T). SingI t :- SingI (TAsRPC t)-rpcSingIEvi =-  Sub $-    case sing @t of-      STKey -> Dict-      STUnit {} -> Dict-      STSignature {} -> Dict-      STChainId {} -> Dict-      STChest {} -> Dict-      STChestKey {} -> Dict-      STOption (s :: Sing elem) -> withSingI s $ Dict \\ rpcSingIEvi @elem-      STList (s :: Sing elem) -> withSingI s $  Dict \\ rpcSingIEvi @elem-      STSet (s :: Sing elem) -> withSingI s $ Dict \\ rpcSingIEvi @elem-      STOperation {} -> Dict-      STContract {} -> Dict-      STTicket {} -> Dict-      STPair (sa :: Sing a) (sb :: Sing b) ->-        withSingI sa $ withSingI sb $-          Dict \\ rpcSingIEvi @a \\ rpcSingIEvi @b-      STOr (sl :: Sing l) (sr :: Sing r) ->-        withSingI sl $ withSingI sr $-          Dict \\ rpcSingIEvi @l \\ rpcSingIEvi @r-      STLambda {} -> Dict-      STMap (sk :: Sing k) (sv :: Sing v) ->-        withSingI sk $ withSingI sv $-          Dict \\ rpcSingIEvi @k \\ rpcSingIEvi @v-      STBigMap {} -> Dict-      STInt {} -> Dict-      STNat {} -> Dict-      STString {} -> Dict-      STBytes {} -> Dict-      STMutez {} -> Dict-      STBool {} -> Dict-      STKeyHash {} -> Dict-      STBls12381Fr {} -> Dict-      STBls12381G1 {} -> Dict-      STBls12381G2 {} -> Dict-      STTimestamp {} -> Dict-      STAddress {} -> Dict-      STNever {} -> Dict-      STSaplingState _ -> Dict-      STSaplingTransaction _ -> Dict+rpcSingIEvi :: forall t. SingI t => Dict (SingI (TAsRPC t))+rpcSingIEvi = withSingI (rpcSing $ sing @t) Dict +rpcSing :: Sing t -> Sing (TAsRPC t)+rpcSing st = case st of+  STKey -> st+  STUnit {} -> st+  STSignature {} -> st+  STChainId {} -> st+  STChest {} -> st+  STChestKey {} -> st+  STOption s -> STOption $ rpcSing s+  STList s ->  STList $ rpcSing s+  STSet{} -> st+  STOperation {} -> st+  STContract {} -> st+  STTicket {} -> st+  STPair sa sb -> STPair (rpcSing sa) (rpcSing sb)+  STOr sl sr -> STOr (rpcSing sl) (rpcSing sr)+  STLambda {} -> st+  STMap sk sv -> STMap sk (rpcSing sv)+  STBigMap {} -> STNat+  STInt {} -> st+  STNat {} -> st+  STString {} -> st+  STBytes {} -> st+  STMutez {} -> st+  STBool {} -> st+  STKeyHash {} -> st+  STBls12381Fr {} -> st+  STBls12381G1 {} -> st+  STBls12381G2 {} -> st+  STTimestamp {} -> st+  STAddress {} -> st+  STNever {} -> st+  STSaplingState _ -> st+  STSaplingTransaction _ -> st+ -- | A proof that if @t@ is well-typed, then @TAsRPC t@ is also well-typed.-rpcWellTypedEvi :: forall (t :: T). WellTyped t => WellTyped t :- WellTyped (TAsRPC t)-rpcWellTypedEvi = rpcWellTypedEvi' sing+rpcWellTypedEvi :: forall t. WellTyped t => Dict (WellTyped (TAsRPC t))+rpcWellTypedEvi = rpcWellTypedEvi' $ sing @t -rpcWellTypedEvi'-  :: WellTyped t-  => Sing t-  -> WellTyped t :- WellTyped (TAsRPC t)-rpcWellTypedEvi' sng = Sub $ case sng of+rpcWellTypedEvi' :: WellTyped t => Sing t -> Dict (WellTyped (TAsRPC t))+rpcWellTypedEvi' sng = case sng of   STKey -> Dict   STUnit {} -> Dict   STSignature {} -> Dict@@ -907,187 +1011,113 @@   STSaplingTransaction _ -> Dict  -- | A proof that if @t@ does not contain any operations, then neither does @TAsRPC t@.-rpcHasNoOpEvi :: forall (t :: T). (SingI t, HasNoOp t) => HasNoOp t :- HasNoOp (TAsRPC t)-rpcHasNoOpEvi = rpcHasNoOpEvi' sing--rpcHasNoOpEvi'-  :: HasNoOp t-  => Sing t-  -> HasNoOp t :- HasNoOp (TAsRPC t)-rpcHasNoOpEvi' sng = Sub $ case sng of-  STKey -> Dict-  STUnit {} -> Dict-  STSignature {} -> Dict-  STChainId {} -> Dict-  STChest {} -> Dict-  STChestKey {} -> Dict-  STOption s -> Dict \\ rpcHasNoOpEvi' s-  STList s -> Dict \\ rpcHasNoOpEvi' s-  STSet s -> Dict \\ rpcHasNoOpEvi' s-  STContract {} -> Dict-  STTicket {} -> Dict-  STPair sa sb -> case checkOpPresence sa of-    OpAbsent -> Dict \\ rpcHasNoOpEvi' sa \\ rpcHasNoOpEvi' sb-  STOr sl sr -> case checkOpPresence sl of-    OpAbsent -> Dict \\ rpcHasNoOpEvi' sl \\ rpcHasNoOpEvi' sr-  STLambda {} -> Dict-  STMap _ sv -> case checkOpPresence sv of-    OpAbsent -> Dict \\ rpcHasNoOpEvi' sv-  STBigMap {} -> Dict-  STInt {} -> Dict-  STNat {} -> Dict-  STString {} -> Dict-  STBytes {} -> Dict-  STMutez {} -> Dict-  STBool {} -> Dict-  STKeyHash {} -> Dict-  STBls12381Fr {} -> Dict-  STBls12381G1 {} -> Dict-  STBls12381G2 {} -> Dict-  STTimestamp {} -> Dict-  STAddress {} -> Dict-  STNever {} -> Dict-  STSaplingState {} -> Dict-  STSaplingTransaction {} -> Dict+rpcHasNoOpEvi :: forall (t :: T). (SingI t, ForbidOp t) => Dict (ForbidOp (TAsRPC t))+rpcHasNoOpEvi = Dict \\ rpcHasNoTEvi @t SPSOp  -- | A proof that @AsRPC (Value t)@ does not contain big_maps.-rpcHasNoBigMapEvi :: forall (t :: T). SingI t => Dict (HasNoBigMap (TAsRPC t))-rpcHasNoBigMapEvi = rpcHasNoBigMapEvi' (sing @t)--rpcHasNoBigMapEvi' :: Sing t -> Dict (HasNoBigMap (TAsRPC t))-rpcHasNoBigMapEvi' = \case-  STKey -> Dict-  STUnit {} -> Dict-  STSignature {} -> Dict-  STChainId {} -> Dict-  STChest {} -> Dict-  STChestKey {} -> Dict-  STOption s -> Dict \\ rpcHasNoBigMapEvi' s-  STList s -> Dict \\ rpcHasNoBigMapEvi' s-  STSet s -> Dict \\ rpcHasNoBigMapEvi' s-  STOperation {} -> Dict-  STContract {} -> Dict-  STTicket {} -> Dict-  STPair sa sb -> Dict \\ rpcHasNoBigMapEvi' sa \\ rpcHasNoBigMapEvi' sb-  STOr sl sr -> Dict \\ rpcHasNoBigMapEvi' sl \\ rpcHasNoBigMapEvi' sr-  STLambda {} -> Dict-  STMap sk sv -> Dict \\ rpcHasNoBigMapEvi' sk \\ rpcHasNoBigMapEvi' sv-  STBigMap {} -> Dict-  STInt {} -> Dict-  STNat {} -> Dict-  STString {} -> Dict-  STBytes {} -> Dict-  STMutez {} -> Dict-  STBool {} -> Dict-  STKeyHash {} -> Dict-  STBls12381Fr {} -> Dict-  STBls12381G1 {} -> Dict-  STBls12381G2 {} -> Dict-  STTimestamp {} -> Dict-  STAddress {} -> Dict-  STNever {} -> Dict-  STSaplingState {} -> Dict-  STSaplingTransaction {} -> Dict+rpcHasNoBigMapEvi :: forall (t :: T). (SingI t, ForbidBigMap t) => Dict (ForbidBigMap (TAsRPC t))+rpcHasNoBigMapEvi = Dict \\ rpcHasNoTEvi @t SPSBigMap --- | A proof that @AsRPC (Value t)@ does not contain big_maps.+-- | A proof that @AsRPC (Value t)@ does not contain nested big_maps. rpcHasNoNestedBigMapsEvi-  :: forall (t :: T).-     SingI t-  => Dict (HasNoNestedBigMaps (TAsRPC t))-rpcHasNoNestedBigMapsEvi = rpcHasNoNestedBigMapsEvi' (sing @t)+  :: forall (t :: T). (SingI t, ForbidNestedBigMaps t) => Dict (ForbidNestedBigMaps (TAsRPC t))+rpcHasNoNestedBigMapsEvi = Dict \\ rpcHasNoTEvi @t SPSNestedBigMaps -rpcHasNoNestedBigMapsEvi' :: Sing t -> Dict (HasNoNestedBigMaps (TAsRPC t))-rpcHasNoNestedBigMapsEvi' = \case-  STKey -> Dict-  STUnit {} -> Dict-  STSignature {} -> Dict-  STChainId {} -> Dict-  STChest {} -> Dict-  STChestKey {} -> Dict-  STOption s -> Dict \\ rpcHasNoNestedBigMapsEvi' s-  STList s -> Dict \\ rpcHasNoNestedBigMapsEvi' s-  STSet s -> Dict \\ rpcHasNoNestedBigMapsEvi' s-  STOperation {} -> Dict-  STContract {} -> Dict-  STTicket {} -> Dict-  STPair sa sb ->-    Dict \\ rpcHasNoNestedBigMapsEvi' sa \\ rpcHasNoNestedBigMapsEvi' sb-  STOr sl sr ->-    Dict \\ rpcHasNoNestedBigMapsEvi' sl \\ rpcHasNoNestedBigMapsEvi' sr-  STLambda {} -> Dict-  STMap sk sv ->-    Dict \\ rpcHasNoNestedBigMapsEvi' sk \\ rpcHasNoNestedBigMapsEvi' sv-  STBigMap {} -> Dict-  STInt {} -> Dict-  STNat {} -> Dict-  STString {} -> Dict-  STBytes {} -> Dict-  STMutez {} -> Dict-  STBool {} -> Dict-  STKeyHash {} -> Dict-  STBls12381Fr {} -> Dict-  STBls12381G1 {} -> Dict-  STBls12381G2 {} -> Dict-  STTimestamp {} -> Dict-  STAddress {} -> Dict-  STNever {} -> Dict-  STSaplingState {} -> Dict-  STSaplingTransaction {} -> Dict+-- | A proof that @AsRPC (Value t)@ does not contain some type defined by a predicate.+rpcHasNoTEvi+  :: forall (t :: T) p.+     (SingI t, ContainsT p t ~ 'False)+  => Sing p -> (ContainsT p (TAsRPC t) :~: 'False)+rpcHasNoTEvi sp = rpcHasNoTEvi' sp (sing @t) +rpcHasNoTEvi'+  :: forall t p. (ContainsT p t ~ 'False)+  => Sing p -> Sing t -> ContainsT p (TAsRPC t) :~: 'False+rpcHasNoTEvi' ps ts = stubProof case ts of+  STKey -> Refl+  STUnit {} -> Refl+  STSignature {} -> Refl+  STChainId {} -> Refl+  STChest {} -> Refl+  STChestKey {} -> Refl+  STOption s -> Refl \\ go s+  STList s -> case ps of+    SPSOp -> Refl \\ go s+    SPSContract -> Refl \\ go s+    SPSTicket -> Refl \\ go s+    SPSBigMap -> Refl \\ go s+    SPSNestedBigMaps -> Refl \\ go s+    SPSSaplingState -> Refl \\ go s+  STSet _ -> case ps of+    SPSOp -> Refl+    SPSContract -> Refl+    SPSTicket -> Refl+    SPSBigMap -> Refl+    SPSNestedBigMaps -> Refl+    SPSSaplingState -> Refl+  STOperation {} -> case ps of+    SPSContract -> Refl+    SPSTicket -> Refl+    SPSBigMap -> Refl+    SPSNestedBigMaps -> Refl+    SPSSaplingState -> Refl+  STContract {} -> case ps of+    SPSOp -> Refl+    SPSTicket -> Refl+    SPSBigMap -> Refl+    SPSNestedBigMaps -> Refl+    SPSSaplingState -> Refl+  STTicket _ -> case ps of+    SPSOp -> Refl+    SPSContract -> Refl+    SPSBigMap -> Refl+    SPSNestedBigMaps -> Refl+    SPSSaplingState -> Refl+  STPair sa sb -> deMorganForbidT ps sa sb $ Refl \\ go sa \\ go sb+  STOr sl sr -> deMorganForbidT ps sl sr $ Refl \\ go sl \\ go sr+  STLambda {} -> Refl+  STMap sk sv -> case ps of+    SPSOp -> deMorganForbidT ps sk sv $ Refl \\ go sv+    SPSContract -> deMorganForbidT ps sk sv $ Refl \\ go sv+    SPSTicket -> deMorganForbidT ps sk sv $ Refl \\ go sv+    SPSBigMap -> deMorganForbidT ps sk sv $ Refl \\ go sv+    SPSNestedBigMaps -> deMorganForbidT ps sk sv $ Refl \\ go sv+    SPSSaplingState -> deMorganForbidT ps sk sv $ Refl \\ go sv+  STBigMap {} -> Refl+  STInt {} -> Refl+  STNat {} -> Refl+  STString {} -> Refl+  STBytes {} -> Refl+  STMutez {} -> Refl+  STBool {} -> Refl+  STKeyHash {} -> Refl+  STBls12381Fr {} -> Refl+  STBls12381G1 {} -> Refl+  STBls12381G2 {} -> Refl+  STTimestamp {} -> Refl+  STAddress {} -> Refl+  STNever {} -> Refl+  STSaplingState {} -> case ps of+    SPSOp -> Refl+    SPSTicket -> Refl+    SPSContract -> Refl+    SPSBigMap -> Refl+    SPSNestedBigMaps -> Refl+  STSaplingTransaction {} -> Refl+  where+    go :: (ContainsT p t' ~ 'False) => Sing t' -> ContainsT p (TAsRPC t') :~: 'False+    go = rpcHasNoTEvi' ps+ -- | A proof that if @t@ does not contain any contract values, then neither does @TAsRPC t@. rpcHasNoContractEvi-  :: forall (t :: T).-     (SingI t, HasNoContract t)-  => HasNoContract t :- HasNoContract (TAsRPC t)-rpcHasNoContractEvi = rpcHasNoContractEvi' sing--rpcHasNoContractEvi'-  :: HasNoContract t-  => Sing t-  -> HasNoContract t :- HasNoContract (TAsRPC t)-rpcHasNoContractEvi' sng = Sub $ case sng of-  STKey -> Dict-  STUnit {} -> Dict-  STSignature {} -> Dict-  STChainId {} -> Dict-  STChest {} -> Dict-  STChestKey {} -> Dict-  STOption s -> Dict \\ rpcHasNoContractEvi' s-  STList s -> Dict \\ rpcHasNoContractEvi' s-  STSet _ -> Dict-  STOperation {} -> Dict-  STTicket {} -> Dict-  STPair sa sb -> case checkContractTypePresence sa of-    ContractAbsent ->-      Dict \\ rpcHasNoContractEvi' sa \\ rpcHasNoContractEvi' sb-  STOr sl sr -> case checkContractTypePresence sl of-    ContractAbsent ->-      Dict \\ rpcHasNoContractEvi' sl \\ rpcHasNoContractEvi' sr-  STLambda {} -> Dict-  STMap _ sv -> Dict \\ rpcHasNoContractEvi' sv-  STBigMap {} -> Dict-  STInt {} -> Dict-  STNat {} -> Dict-  STString {} -> Dict-  STBytes {} -> Dict-  STMutez {} -> Dict-  STBool {} -> Dict-  STKeyHash {} -> Dict-  STBls12381Fr {} -> Dict-  STBls12381G1 {} -> Dict-  STBls12381G2 {} -> Dict-  STTimestamp {} -> Dict-  STAddress {} -> Dict-  STNever {} -> Dict-  STSaplingState {} -> Dict-  STSaplingTransaction {} -> Dict+  :: forall (t :: T). (SingI t, ForbidContract t) => Dict (ForbidContract (TAsRPC t))+rpcHasNoContractEvi = Dict \\ rpcHasNoTEvi @t SPSContract  -- | A proof that if @t@ is a valid storage type, then so is @TAsRPC t@.-rpcStorageScopeEvi :: forall (t :: T). StorageScope t :- StorageScope (TAsRPC t)-rpcStorageScopeEvi =-  Sub $ Dict-    \\ rpcSingIEvi @t-    \\ rpcHasNoOpEvi @t-    \\ rpcHasNoNestedBigMapsEvi @t-    \\ rpcHasNoContractEvi @t-    \\ rpcWellTypedEvi @t+rpcStorageScopeEvi :: forall (t :: T). StorageScope t => Dict (StorageScope (TAsRPC t))+rpcStorageScopeEvi = Dict+  \\ rpcSingIEvi @t+  \\ rpcHasNoOpEvi @t+  \\ rpcHasNoNestedBigMapsEvi @t+  \\ rpcHasNoContractEvi @t+  \\ rpcWellTypedEvi @t

@@ -16,7 +16,6 @@ import Data.Binary.Get qualified as Bi import Data.ByteString qualified as BS import Data.ByteString.Lazy qualified as LBS-import Data.Sequence qualified as Seq import Unsafe qualified (fromIntegral)  import Morley.Micheline.Binary.Internal@@ -54,9 +53,7 @@ buildList = foldMap buildExpr  buildPrim :: MichelinePrimitive -> Bi.Builder-buildPrim (MichelinePrimitive p) = case Seq.elemIndexL p michelsonPrimitive of-  Nothing -> error $ "unknown Michelson/Micheline primitive: " <> p-  Just ix -> buildWord8 (Unsafe.fromIntegral @Int @Word8 ix)+buildPrim = buildWord8 . Unsafe.fromIntegral @Int @Word8 . fromEnum  buildAnnotationList :: [Annotation] -> Bi.Builder buildAnnotationList listAnn = buildDynamic buildText (DynamicSize $ unwords . fmap annotToText $ listAnn)@@ -92,10 +89,8 @@ getList = many getExpr  getPrim :: Bi.Get MichelinePrimitive-getPrim =-  Bi.getWord8 >>= \ix -> case Seq.lookup (fromIntegral ix) michelsonPrimitive of-    Nothing -> fail "unknown Michelson/Micheline opcode"-    Just str -> pure $ MichelinePrimitive str+getPrim = maybe (fail "unknown Michelson/Micheline opcode") pure . toEnumSafe . fromIntegral+  =<< Bi.getWord8  getAnnotationList :: Bi.Get [Annotation] getAnnotationList = mapM annotFromText . words . unDynamicSize =<< (getDynamic getText)

@@ -14,1046 +14,945 @@  import Control.Lens ((<>~)) import Data.Bits (Bits)-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 (TypeCheckOptions(..), typeCheckingWith)-import Morley.Michelson.TypeCheck.Instr (typeCheckValue)-import Morley.Michelson.Typed-  (Contract, HasNoOp, Instr, LambdaCode'(..), 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-    Untyped.ValueLamRec ops -> expressionPrim' "Lambda_rec" [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 t) []-    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.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 :: Untyped.T -> [Expression]-      rightCombedPairToList t =-        let go ty (fa, va)-              | Ty (Untyped.TPair faL faR vaL vaR l r) ta <- ty-              , ta == noAnn, fa == noAnn, va == noAnn-              = toExpression l `addAnns` mkAnns [] [faL] [vaL] : go r (faR, vaR)-              | otherwise-              = one $ toExpression ty `addAnns` mkAnns [] [fa] [va]-        in go (Ty t noAnn) (noAnn, noAnn)--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---- Note: On adding new expressions here, you must also add the symmetric (reading) case--- to FromExp x (InstrAbstract op) as well.-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]-    LAMBDA_REC va tyin tyout ops ->-      expressionPrim' "LAMBDA_REC" [ 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]-    NAT va -> expressionPrim' "NAT" [] $ mkAnns [] [] [va]-    BYTES va -> expressionPrim' "BYTES" [] $ 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]-    TICKET_DEPRECATED va -> expressionPrim' "TICKET_DEPRECATED" [] $ 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-    EMIT va tag ty -> expressionPrim' "EMIT" (toExpression <$> maybeToList ty) $ mkAnns [] [tag] [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) $-        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-    ExpPrim' _ "Lambda_rec" [args] [] -> fmap Untyped.ValueLamRec $-      fromExp args >>= maybeToRight (FromExpError e "Expected at least one instruction") . nonEmpty-    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---- Note: On adding new expressions here, you must also add the symmetric (writing) case--- to ToExpression as well.-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' _ "LAMBDA_REC" [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_REC 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' _ "NAT" [] anns -> mkInstrWithVarAnn NAT anns-    ExpPrim' _ "BYTES" [] anns -> mkInstrWithVarAnn BYTES 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_DEPRECATED" [] anns ->-      mkInstrWithVarAnn TICKET_DEPRECATED anns-    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-    ExpPrim' _ "EMIT" mty _ -> do-      checkAnnsCount e annSet (0, 1, 1)-      let tag = firstAnn @FieldTag annSet-          va = firstAnn @VarTag annSet-      ty' <- maybe (pure Nothing) (fmap Just . fromExp @x @Ty) $ listToMaybe mty-      pure $ EMIT va tag ty'-    _ -> 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" [] [] ->-      Left $ FromExpError e "Transaction rollups are not supported"-    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 (LambdaCode instr) -> pure $ rfAnyInstr instr-      VLam LambdaCodeRec{} -> Left $ FromExpError expr-        "Expected block of code, found Lambda_rec"--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"+import Data.Singletons (SingI(..), demote, fromSing)+import Fmt (Buildable(..), fillSepF, indentF, nameF, pretty, punctuateF, unlinesF, (++|), (|++))++import Morley.Micheline.Expression+import Morley.Michelson.Text (mkMText, unMText)+import Morley.Michelson.TypeCheck (TcError, TypeCheckOptions(..), typeCheckingWith)+import Morley.Michelson.TypeCheck.Instr (typeCheckValue)+import Morley.Michelson.Typed+  (Contract, ForbidOp, Instr, LambdaCode'(..), Notes(..), T(..), Value, Value'(..), fromUType,+  mkUType, rfAnyInstr, toUType)+import Morley.Michelson.Typed.Convert+  (convertContractOptimized, instrToOpsOptimized, untypeValueOptimized)+import Morley.Michelson.Untyped qualified as Untyped+import Morley.Michelson.Untyped.Annotation+  (AnnotationSet(..), FieldAnn, FieldTag, RootAnn, TypeAnn, TypeTag, VarAnn, VarTag, annsCount,+  firstAnn, noAnn, secondAnn)+import Morley.Michelson.Untyped.Contract (ContractBlock(..), ContractBlockError, orderContractBlock)+import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..))+import Morley.Michelson.Untyped.Type (Ty(..))+import Morley.Michelson.Untyped.View+import Morley.Util.MismatchError++-- ToExpression+----------------------------------------------------------------------------++-- | Type class that provides an ability to convert+-- something to Micheline Expression.+class ToExpression a where+  toExpression :: a -> Expression++instance ForbidOp 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' Prim_Unit [] []+    Untyped.ValueTrue -> expressionPrim' Prim_True [] []+    Untyped.ValueFalse -> expressionPrim' Prim_False [] []+    Untyped.ValuePair l r ->+      expressionPrim' Prim_Pair [toExpression l, toExpression r] []+    Untyped.ValueLeft v -> expressionPrim' Prim_Left [toExpression v] []+    Untyped.ValueRight v -> expressionPrim' Prim_Right [toExpression v] []+    Untyped.ValueSome v -> expressionPrim' Prim_Some [toExpression v] []+    Untyped.ValueNone -> expressionPrim' Prim_None [] []+    Untyped.ValueNil -> expressionSeq []+    Untyped.ValueSeq vs -> toExpression vs+    Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts+    Untyped.ValueLambda ops -> toExpression ops+    Untyped.ValueLamRec ops -> expressionPrim' Prim_Lambda_rec [toExpression ops] []+    where+      eltToExpr :: Untyped.Elt [] ExpandedOp -> Expression+      eltToExpr (Untyped.Elt l r) = expressionPrim' Prim_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' Prim_key [] []+    Untyped.TUnit -> expressionPrim' Prim_unit [] []+    Untyped.TSignature -> expressionPrim' Prim_signature [] []+    Untyped.TChainId -> expressionPrim' Prim_chain_id [] []+    Untyped.TOption arg -> expressionPrim' Prim_option [toExpression arg] []+    Untyped.TList arg -> expressionPrim' Prim_list [toExpression arg] []+    Untyped.TSet arg -> expressionPrim' Prim_set [toExpression arg] []+    Untyped.TOperation -> expressionPrim' Prim_operation [] []+    Untyped.TContract arg -> expressionPrim' Prim_contract [toExpression arg] []+    Untyped.TTicket arg -> expressionPrim' Prim_ticket [toExpression arg] []+    t@Untyped.TPair{} -> expressionPrim' Prim_pair (rightCombedPairToList t) []+    Untyped.TOr fa1 fa2 l r ->+      let exprL = addTrimmedAnns (toExpression l) [] [fa1] []+          exprR = addTrimmedAnns (toExpression r) [] [fa2] []+      in expressionPrim' Prim_or [exprL, exprR] []+    Untyped.TLambda inp out ->+      expressionPrim' Prim_lambda [toExpression inp, toExpression out] []+    Untyped.TMap k v ->+      expressionPrim' Prim_map [toExpression k, toExpression v] []+    Untyped.TBigMap k v ->+      expressionPrim' Prim_big_map [toExpression k, toExpression v] []+    Untyped.TInt -> expressionPrim' Prim_int [] []+    Untyped.TNat -> expressionPrim' Prim_nat [] []+    Untyped.TString -> expressionPrim' Prim_string [] []+    Untyped.TBytes -> expressionPrim' Prim_bytes [] []+    Untyped.TMutez -> expressionPrim' Prim_mutez [] []+    Untyped.TBool -> expressionPrim' Prim_bool [] []+    Untyped.TKeyHash -> expressionPrim' Prim_key_hash [] []+    Untyped.TBls12381Fr -> expressionPrim' Prim_bls12_381_fr [] []+    Untyped.TBls12381G1 -> expressionPrim' Prim_bls12_381_g1 [] []+    Untyped.TBls12381G2 -> expressionPrim' Prim_bls12_381_g2 [] []+    Untyped.TTimestamp -> expressionPrim' Prim_timestamp [] []+    Untyped.TAddress -> expressionPrim' Prim_address [] []+    Untyped.TChest -> expressionPrim' Prim_chest [] []+    Untyped.TChestKey -> expressionPrim' Prim_chest_key [] []+    Untyped.TNever -> expressionPrim' Prim_never [] []+    Untyped.TSaplingState n -> expressionPrim' Prim_sapling_state [integralToExpr n] []+    Untyped.TSaplingTransaction n -> expressionPrim' Prim_sapling_transaction [integralToExpr n] []++    where+      addAnns :: Expression -> [Annotation] -> Expression+      addAnns e anns =+        e & _ExpressionPrim . mpaAnnotsL <>~ anns++      rightCombedPairToList :: Untyped.T -> [Expression]+      rightCombedPairToList t =+        let go ty (fa, va)+              | Ty (Untyped.TPair faL faR vaL vaR l r) ta <- ty+              , ta == noAnn, fa == noAnn, va == noAnn+              = toExpression l `addAnns` mkAnns [] [faL] [vaL] : go r (faR, vaR)+              | otherwise+              = one $ toExpression ty `addAnns` mkAnns [] [fa] [va]+        in go (Ty t noAnn) (noAnn, noAnn)++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++-- Note: On adding new expressions here, you must also add the symmetric (reading) case+-- to FromExp x (InstrAbstract [] op) as well.+instance ToExpression ExpandedInstr where+  toExpression = \case+    PUSH va ty v -> expressionPrim' Prim_PUSH [toExpression ty, toExpression v] $+      mkAnns [] [] [va]+    DROP -> expressionPrim' Prim_DROP [] []+    DROPN n -> expressionPrim' Prim_DROP [integralToExpr n] []+    DUP va -> expressionPrim' Prim_DUP [] $ mkAnns [] [] [va]+    DUPN va n -> expressionPrim' Prim_DUP [integralToExpr n] $ mkAnns [] [] [va]+    SWAP -> expressionPrim' Prim_SWAP [] []+    DIG n -> expressionPrim' Prim_DIG [integralToExpr n] []+    DUG n -> expressionPrim' Prim_DUG [integralToExpr n] []+    SOME ta va ->+      expressionPrim' Prim_SOME [] $ mkAnns [ta] [] [va]+    NONE ta va ty -> expressionPrim' Prim_NONE [toExpression ty] $ mkAnns [ta] [] [va]+    UNIT ta va -> expressionPrim' Prim_UNIT [] $ mkAnns [ta] [] [va]+    IF_NONE ops1 ops2 ->+      expressionPrim' Prim_IF_NONE [toExpression ops1, toExpression ops2] []+    PAIR ta va fa1 fa2 -> expressionPrim' Prim_PAIR [] $ mkAnns [ta] [fa1, fa2] [va]+    UNPAIR va1 va2 fa1 fa2 -> expressionPrim' Prim_UNPAIR [] $+      mkAnns [] [fa1, fa2] [va1, va2]+    PAIRN va n -> expressionPrim' Prim_PAIR [integralToExpr n] $ mkAnns [] [] [va]+    UNPAIRN n -> expressionPrim' Prim_UNPAIR [integralToExpr n] []+    CAR va fa -> expressionPrim' Prim_CAR [] $ mkAnns [] [fa] [va]+    CDR va fa -> expressionPrim' Prim_CDR [] $ mkAnns [] [fa] [va]+    LEFT ta va fa1 fa2 ty -> expressionPrim' Prim_LEFT [toExpression ty] $+      mkAnns [ta] [fa1, fa2] [va]+    RIGHT ta va fa1 fa2 ty -> expressionPrim' Prim_RIGHT [toExpression ty] $+      mkAnns [ta] [fa1, fa2] [va]+    IF_LEFT ops1 ops2 ->+      expressionPrim' Prim_IF_LEFT [toExpression ops1, toExpression ops2] []+    NIL ta va ty -> expressionPrim' Prim_NIL [toExpression ty] $+      mkAnns [ta] [] [va]+    CONS va -> expressionPrim' Prim_CONS [] $ mkAnns [] [] [va]+    IF_CONS ops1 ops2 ->+      expressionPrim' Prim_IF_CONS [toExpression ops1, toExpression ops2] []+    SIZE va -> expressionPrim' Prim_SIZE [] $ mkAnns [] [] [va]+    EMPTY_SET ta va ty -> expressionPrim' Prim_EMPTY_SET [toExpression ty] $+      mkAnns [ta] [] [va]+    EMPTY_MAP ta va kty vty ->+      expressionPrim' Prim_EMPTY_MAP [toExpression kty, toExpression vty] $+      mkAnns [ta] [] [va]+    EMPTY_BIG_MAP ta va kty vty ->+      expressionPrim' Prim_EMPTY_BIG_MAP [toExpression kty, toExpression vty] $+      mkAnns [ta] [] [va]+    MAP va ops -> expressionPrim' Prim_MAP [toExpression ops] $ mkAnns [] [] [va]+    ITER ops -> expressionPrim' Prim_ITER [toExpression ops] []+    MEM va -> expressionPrim' Prim_MEM [] $ mkAnns [] [] [va]+    GET va -> expressionPrim' Prim_GET [] $ mkAnns [] [] [va]+    GETN va n -> expressionPrim' Prim_GET [integralToExpr n] $ mkAnns [] [] [va]+    UPDATE va -> expressionPrim' Prim_UPDATE [] $ mkAnns [] [] [va]+    UPDATEN va n -> expressionPrim' Prim_UPDATE [integralToExpr n] $ mkAnns [] [] [va]+    GET_AND_UPDATE va -> expressionPrim' Prim_GET_AND_UPDATE [] $ mkAnns [] [] [va]+    IF ops1 ops2 ->+      expressionPrim' Prim_IF [toExpression ops1, toExpression ops2] []+    LOOP ops -> expressionPrim' Prim_LOOP [toExpression ops] []+    LOOP_LEFT ops -> expressionPrim' Prim_LOOP_LEFT [toExpression ops] []+    LAMBDA va tyin tyout ops ->+      expressionPrim' Prim_LAMBDA [ toExpression tyin+                            , toExpression tyout+                            , toExpression ops+                            ] $ mkAnns [] [] [va]+    LAMBDA_REC va tyin tyout ops ->+      expressionPrim' Prim_LAMBDA_REC [ toExpression tyin+                            , toExpression tyout+                            , toExpression ops+                            ] $ mkAnns [] [] [va]+    EXEC va -> expressionPrim' Prim_EXEC [] $ mkAnns [] [] [va]+    APPLY va -> expressionPrim' Prim_APPLY [] $ mkAnns [] [] [va]+    DIP ops -> expressionPrim' Prim_DIP [toExpression ops] []+    DIPN n ops -> expressionPrim' Prim_DIP [integralToExpr n, toExpression ops] []+    FAILWITH -> expressionPrim' Prim_FAILWITH [] []+    CAST va ty -> expressionPrim' Prim_CAST [toExpression ty] $ mkAnns [] [] [va]+    RENAME va -> expressionPrim' Prim_RENAME [] $ mkAnns [] [] [va]+    PACK va -> expressionPrim' Prim_PACK [] $ mkAnns [] [] [va]+    UNPACK ta va ty -> expressionPrim' Prim_UNPACK [toExpression ty] $+      mkAnns [ta] [] [va]+    CONCAT va -> expressionPrim' Prim_CONCAT [] $ mkAnns [] [] [va]+    SLICE va -> expressionPrim' Prim_SLICE [] $ mkAnns [] [] [va]+    ISNAT va -> expressionPrim' Prim_ISNAT [] $ mkAnns [] [] [va]+    ADD va -> expressionPrim' Prim_ADD [] $ mkAnns [] [] [va]+    SUB va -> expressionPrim' Prim_SUB [] $ mkAnns [] [] [va]+    SUB_MUTEZ va -> expressionPrim' Prim_SUB_MUTEZ [] $ mkAnns [] [] [va]+    MUL va -> expressionPrim' Prim_MUL [] $ mkAnns [] [] [va]+    EDIV va -> expressionPrim' Prim_EDIV [] $ mkAnns [] [] [va]+    ABS va -> expressionPrim' Prim_ABS [] $ mkAnns [] [] [va]+    NEG va -> expressionPrim' Prim_NEG [] $ mkAnns [] [] [va]+    LSL va -> expressionPrim' Prim_LSL [] $ mkAnns [] [] [va]+    LSR va -> expressionPrim' Prim_LSR [] $ mkAnns [] [] [va]+    OR va -> expressionPrim' Prim_OR [] $ mkAnns [] [] [va]+    AND va -> expressionPrim' Prim_AND [] $ mkAnns [] [] [va]+    XOR va -> expressionPrim' Prim_XOR [] $ mkAnns [] [] [va]+    NOT va -> expressionPrim' Prim_NOT [] $ mkAnns [] [] [va]+    COMPARE va -> expressionPrim' Prim_COMPARE [] $ mkAnns [] [] [va]+    Untyped.EQ va -> expressionPrim' Prim_EQ [] $ mkAnns [] [] [va]+    NEQ va -> expressionPrim' Prim_NEQ [] $ mkAnns [] [] [va]+    Untyped.LT va -> expressionPrim' Prim_LT [] $ mkAnns [] [] [va]+    Untyped.GT va -> expressionPrim' Prim_GT [] $ mkAnns [] [] [va]+    LE va -> expressionPrim' Prim_LE [] $ mkAnns [] [] [va]+    GE va -> expressionPrim' Prim_GE [] $ mkAnns [] [] [va]+    INT va -> expressionPrim' Prim_INT [] $ mkAnns [] [] [va]+    NAT va -> expressionPrim' Prim_NAT [] $ mkAnns [] [] [va]+    BYTES va -> expressionPrim' Prim_BYTES [] $ mkAnns [] [] [va]+    VIEW va n t -> expressionPrim' Prim_VIEW [toExpression n, toExpression t] $+      mkAnns [] [] [va]+    SELF va fa -> expressionPrim' Prim_SELF [] $ mkAnns [] [fa] [va]+    CONTRACT va fa ty -> expressionPrim' Prim_CONTRACT [toExpression ty] $+      mkAnns [] [fa] [va]+    TRANSFER_TOKENS va -> expressionPrim' Prim_TRANSFER_TOKENS [] $ mkAnns [] [] [va]+    SET_DELEGATE va -> expressionPrim' Prim_SET_DELEGATE [] $ mkAnns [] [] [va]+    CREATE_CONTRACT va1 va2 c ->+      expressionPrim' Prim_CREATE_CONTRACT [toExpression c] $+      mkAnns [] [] [va1, va2]+    IMPLICIT_ACCOUNT va -> expressionPrim' Prim_IMPLICIT_ACCOUNT [] $+      mkAnns [] [] [va]+    NOW va -> expressionPrim' Prim_NOW [] $ mkAnns [] [] [va]+    AMOUNT va -> expressionPrim' Prim_AMOUNT [] $ mkAnns [] [] [va]+    BALANCE va -> expressionPrim' Prim_BALANCE [] $ mkAnns [] [] [va]+    VOTING_POWER va -> expressionPrim' Prim_VOTING_POWER [] $ mkAnns [] [] [va]+    TOTAL_VOTING_POWER va -> expressionPrim' Prim_TOTAL_VOTING_POWER [] $+      mkAnns [] [] [va]+    CHECK_SIGNATURE va -> expressionPrim' Prim_CHECK_SIGNATURE [] $ mkAnns [] [] [va]+    SHA256 va -> expressionPrim' Prim_SHA256 [] $ mkAnns [] [] [va]+    SHA512 va -> expressionPrim' Prim_SHA512 [] $ mkAnns [] [] [va]+    BLAKE2B va -> expressionPrim' Prim_BLAKE2B [] $ mkAnns [] [] [va]+    SHA3 va -> expressionPrim' Prim_SHA3 [] $ mkAnns [] [] [va]+    KECCAK va -> expressionPrim' Prim_KECCAK [] $ mkAnns [] [] [va]+    HASH_KEY va -> expressionPrim' Prim_HASH_KEY [] $ mkAnns [] [] [va]+    PAIRING_CHECK va -> expressionPrim' Prim_PAIRING_CHECK [] $ mkAnns [] [] [va]+    SOURCE va -> expressionPrim' Prim_SOURCE [] $ mkAnns [] [] [va]+    SENDER va -> expressionPrim' Prim_SENDER [] $ mkAnns [] [] [va]+    ADDRESS va -> expressionPrim' Prim_ADDRESS [] $ mkAnns [] [] [va]+    CHAIN_ID va -> expressionPrim' Prim_CHAIN_ID [] $ mkAnns [] [] [va]+    LEVEL va -> expressionPrim' Prim_LEVEL [] $ mkAnns [] [] [va]+    SELF_ADDRESS va -> expressionPrim' Prim_SELF_ADDRESS [] $ mkAnns [] [] [va]+    TICKET va -> expressionPrim' Prim_TICKET [] $ mkAnns [] [] [va]+    TICKET_DEPRECATED va -> expressionPrim' Prim_TICKET_DEPRECATED [] $ mkAnns [] [] [va]+    READ_TICKET va -> expressionPrim' Prim_READ_TICKET [] $ mkAnns [] [] [va]+    SPLIT_TICKET va -> expressionPrim' Prim_SPLIT_TICKET [] $ mkAnns [] [] [va]+    JOIN_TICKETS va -> expressionPrim' Prim_JOIN_TICKETS [] $ mkAnns [] [] [va]+    OPEN_CHEST va -> expressionPrim' Prim_OPEN_CHEST [] $ mkAnns [] [] [va]+    NEVER -> expressionPrim' Prim_NEVER [] []+    EXT _ -> expressionSeq []+    SAPLING_EMPTY_STATE va n -> expressionPrim' Prim_SAPLING_EMPTY_STATE [integralToExpr n] $ mkAnns [] [] [va]+    SAPLING_VERIFY_UPDATE va -> expressionPrim' Prim_SAPLING_VERIFY_UPDATE [] $ mkAnns [] [] [va]+    MIN_BLOCK_TIME va -> expressionPrim' Prim_MIN_BLOCK_TIME [] $ mkAnnsFromAny va+    EMIT va tag ty -> expressionPrim' Prim_EMIT (toExpression <$> maybeToList ty) $ mkAnns [] [tag] [va]++instance ToExpression Untyped.Contract where+  toExpression contract+    = expressionSeq $ Untyped.mapEntriesOrdered contract+          (\(Untyped.ParameterType ty rootAnn) -> expressionPrim' Prim_parameter+            [insertRootAnn (toExpression ty) rootAnn] [])+          (\storage -> expressionPrim' Prim_storage [toExpression storage] [])+          (\code -> expressionPrim' Prim_code [toExpression code] [])+          (\Untyped.View{..} -> expressionPrim' Prim_view+            [toExpression viewName, toExpression viewArgument, toExpression viewReturn, toExpression viewCode] []+          )++instance ToExpression (Contract cp st) where+  toExpression = toExpression . convertContractOptimized++-- FromExpression+----------------------------------------------------------------------------++-- | Errors that can happen when we convert an 'Exp' to our+-- data type.+data FromExpError x = FromExpError (Exp x) FromExpErrorReason++deriving stock instance Show (Exp x) => Show (FromExpError x)+deriving stock instance Eq (Exp x) => Eq (FromExpError x)++data FromExpErrorReason+  = FEERMTextDecodingFailure Text+  | FEERTcError T TcError+  | FEERNotEnoughArguments Word Int+  | FEERUnexpectedPrim (Maybe MichelinePrimitive) MichelinePrimitive+  | FEERUnexpectedPrimClass MichelinePrimitiveTag MichelinePrimitiveTag+  | FEERArgumentCountMismatch (NonEmpty Word) Int+  | FEERUnexpectedAnnotations+  | FEERExpectedPrim (NonEmpty MichelinePrimitiveTag)+  | FEERExpectedSeq+  | FEERUnsupported+  | FEERDeprecated+  | FEERTooManyAnns (Maybe Int, Maybe Int, Maybe Int) (Int, Int, Int)+  | FEEROutOfBounds+  | FEERExpectedNumber+  | FEERExpectedString+  | FEERViewNameError BadViewNameError+  | FEERBadContractBlocks (NonEmpty ContractBlockError)+  deriving stock (Show, Eq)++instance Buildable FromExpErrorReason where+  build = \case+    FEERMTextDecodingFailure msg -> nameF "Text decoding failure" $ build msg+    FEERTcError ty err -> unlinesF+      [ nameF "Failed to typecheck expression as a value of type" $ build ty+      , mempty+      , nameF "Typechecker error" $ build err+      ]+    FEERNotEnoughArguments minArgs numArgs ->+      "Expected at least" ++| minArgs |++ "arguments, but got" ++| numArgs |++ ""+    FEERUnexpectedPrim expected got ->+      nameF "Unexpected primitive" $ case expected of+        Nothing -> build got+        Just e -> build MkMismatchError { meExpected = e, meActual = got }+    FEERUnexpectedPrimClass expected got ->+      nameF "Unexpected primitive class" $ build $ MkMismatchError+        { meExpected = expected, meActual = got }+    FEERArgumentCountMismatch expected got ->+      fillSepF+        $ "Expected exactly"+        : punctuateF "," " or" expected <>+        [ "arguments, but got"+        , build got+        ]+    FEERUnexpectedAnnotations -> "Unexpected annotations"+    FEERExpectedPrim prims -> fillSepF+      $ "Expected primitive"+      : punctuateF "," " or" prims+    FEERExpectedSeq -> "Expected sequence"+    FEERTooManyAnns (maxTas, maxFas, maxVas) (tasCnt, fasCnt, vasCnt) -> unlinesF+      [ nameF "Expected at most" $ unlinesF $ catMaybes+          [ (<> " type annotations")    . build <$> maxTas+          , (<> " field annotations")   . build <$> maxFas+          , (<> " variable annotations") . build <$> maxVas+          ]+      , nameF "but found" $ unlinesF $ catMaybes+          [ (<> " type annotations")     . build <$> (maxTas $> tasCnt)+          , (<> " field annotations")    . build <$> (maxFas $> fasCnt)+          , (<> " variable annotations") . build <$> (maxVas $> vasCnt)+          ]+      ]+    FEEROutOfBounds -> "Value is out of bounds"+    FEERBadContractBlocks cbes -> unlinesF $ build <$> cbes+    FEERUnsupported -> "Unsupported"+    FEERDeprecated -> "Deprecated primitive"+    FEERExpectedNumber -> "Expected number"+    FEERExpectedString -> "Expected string"+    FEERViewNameError err -> nameF "View name error" $ build err++-- | 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 $ FEERTcError (demote @t) tcErr+      Right tv -> Right tv+    Left e -> Left e+    where+      typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $+        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 . FEERMTextDecodingFailure)+        (Untyped.ValueString <$> mkMText s)+    ExpBytes _ bs -> pure $ Untyped.ValueBytes $ Untyped.InternalByteString bs+    ExpPrim _ (MichelinePrimAp prim args _) -> withClassifiedPrim prim \case+      SMPTValue -> \case+        C_Prim_Unit -> withArgs Untyped.ValueUnit+        C_Prim_True -> withArgs Untyped.ValueTrue+        C_Prim_False -> withArgs Untyped.ValueFalse+        C_Prim_Pair ->+          case nonEmpty args >>= forbidSingletonList of+            Nothing -> Left $ FromExpError e $ FEERNotEnoughArguments 2 (length args)+            Just args' -> do+              tys <- mapM fromExp args'+              return $ foldr1 Untyped.ValuePair tys+        C_Prim_Left -> withArgs Untyped.ValueLeft+        C_Prim_Right -> withArgs Untyped.ValueRight+        C_Prim_Some -> withArgs Untyped.ValueSome+        C_Prim_None -> withArgs Untyped.ValueNone+        C_Prim_Lambda_rec -> withArgs Untyped.ValueLamRec+        C_Prim_Elt -> Left $ FromExpError e $ FEERUnexpectedPrim Nothing Prim_Elt+      s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTValue (fromSing s)+      where+        withArgs :: WithArgsRec x a r => a -> Either (FromExpError x) r+        withArgs = withArgsRec e args+    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 $+            FEERExpectedPrim (MPTValue :| [MPTInstr])+          Right h' -> do+            t' <- traverse fromExp t+            pure . Untyped.ValueSeq $ h' :| t'+    ExpX _ -> Left $ FromExpError e $ FEERExpectedPrim (one MPTValue)+    where+      exprToElt :: Exp x -> Either (FromExpError x) (Untyped.Elt [] op)+      exprToElt ex = case ex of+        ExpPrim' _ Prim_Elt [l, r] [] -> do+          l' <- fromExp l+          r' <- fromExp r+          pure $ Untyped.Elt l' r'+        ExpPrim' _ Prim_Elt args' [] -> Left $ FromExpError ex $+          FEERArgumentCountMismatch (one 2) (length args')+        ExpPrim' _ Prim_Elt _ _ -> Left $ FromExpError ex FEERUnexpectedAnnotations+        ExpPrim' _ prim _ _ -> Left $ FromExpError ex $ FEERUnexpectedPrim (Just Prim_Elt) prim+        _ -> Left $ FromExpError ex $ FEERExpectedPrim $ one MPTValue++instance FromExp x a => FromExp x [a] where+  fromExp = \case+    ExpSeq _ exprs -> traverse fromExp exprs+    e -> Left $ FromExpError e FEERExpectedSeq++instance FromExp RegularExp ExpandedOp where+  fromExp = \case+    ExpSeq _ s -> SeqEx <$> traverse fromExp s+    e          -> PrimEx <$> fromExp e++instance FromExp x Word where+  fromExp = integralFromExpr++instance FromExp x Natural where+  fromExp = integralFromExpr++-- | Used to improve type inference with 'WithArgsRec'.+type family EndResult a where+  EndResult (_ -> b) = EndResult b+  EndResult b = b++-- | Recursive typeclass that unpacks a list of constructor arguments and+-- applies a function to them.+class (EndResult a ~ r, CountArgs a r) => WithArgsRec x a r where+  -- | Given the 'Exp' itself (used for error reporting), its arguments, and a+  -- function constructing the result form the arguments, produce the result or+  -- an error if the argument count is mismatched.+  withArgsRec' :: FromExpError x -> [Exp x] -> a -> Either (FromExpError x) r++instance (FromExp x a, WithArgsRec x b r) => WithArgsRec x (a -> b) r where+  withArgsRec' ee (e:es) f = fromExp @x e >>= withArgsRec' ee es . f+  withArgsRec' ee [] _ = Left ee++instance (EndResult r ~ r) => WithArgsRec x r r where+  withArgsRec' _ [] x = pure x+  withArgsRec' ee _ _ = Left ee++class CountArgs a r where countArgs :: Word+instance CountArgs r r where countArgs = 0+instance CountArgs b r => CountArgs (a -> b) r where countArgs = succ $ countArgs @b @r++withArgsRec+  :: forall x a r. WithArgsRec x a r+  => Exp x -> [Exp x] -> a -> Either (FromExpError x) r+withArgsRec e args = withArgsRec'+  (FromExpError e $ FEERArgumentCountMismatch (one $ countArgs @a @r) (length args))+  args++-- Note: On adding new expressions here, you must also add the symmetric (writing) case+-- to ToExpression as well.+instance FromExp x op =>+         FromExp x (InstrAbstract [] op) where+  fromExp e@(ExpPrim' _ prim args anns) = withClassifiedPrim prim \case+    SMPTInstr -> \case+      C_Prim_DROP -> nilAnns *> case args of+        [] -> pure DROP+        [n] -> DROPN <$> integralFromExpr n+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_DUP -> annsCnt (0, 0, 1) *> case args of+        [n] -> DUPN va <$> integralFromExpr n+        [] -> pure $ DUP va+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_SWAP -> withArgsAnns nil SWAP+      C_Prim_DIG -> withArgsAnns nil DIG+      C_Prim_DUG -> withArgsAnns nil DUG+      C_Prim_PUSH -> withArgsAnns (0, 0, 1) $ PUSH va+      C_Prim_SOME -> withArgsAnns (1, 0, 1) $ SOME ta va+      C_Prim_NONE -> withArgsAnns (1, 0, 1) $ NONE ta va+      C_Prim_UNIT -> withArgsAnns (1, 0, 1) $ UNIT ta va+      C_Prim_IF_NONE -> withArgsAnns nil IF_NONE+      C_Prim_PAIR -> case args of+        [] -> annsCnt (1, 2, 1) $> PAIR ta va fa1 fa2+        [n] -> annsCnt (0, 0, 1) $> PAIRN va <*> integralFromExpr n+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_UNPAIR -> case args of+        [] -> annsCnt (0, 2, 2) $> UNPAIR va1 va2 fa1 fa2+        [n] -> nilAnns $> UNPAIRN <*> integralFromExpr n+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_CAR -> withArgsAnns (0, 1, 1) $ CAR va fa+      C_Prim_CDR -> withArgsAnns (0, 1, 1) $ CDR va fa+      C_Prim_LEFT -> withArgsAnns (1, 2, 1) $ LEFT ta va fa1 fa2+      C_Prim_RIGHT -> withArgsAnns (1, 2, 1) $ RIGHT ta va fa1 fa2+      C_Prim_IF_LEFT -> withArgsAnns nil IF_LEFT+      C_Prim_NIL -> withArgsAnns (1, 0, 1) $ NIL ta va+      C_Prim_CONS -> mkInstrWithVarAnn CONS+      C_Prim_IF_CONS -> withArgsAnns nil IF_CONS+      C_Prim_SIZE -> mkInstrWithVarAnn SIZE+      C_Prim_EMPTY_SET -> withArgsAnns (1, 0, 1) $ EMPTY_SET ta va+      C_Prim_EMPTY_MAP -> withArgsAnns (1, 0, 1) $ EMPTY_MAP ta va+      C_Prim_EMPTY_BIG_MAP -> withArgsAnns (1, 0, 1) $ EMPTY_BIG_MAP ta va+      C_Prim_MAP -> withArgsAnns (0, 0, 1) $ MAP va+      C_Prim_ITER -> withArgsAnns nil ITER+      C_Prim_MEM -> mkInstrWithVarAnn MEM+      C_Prim_GET -> case args of+        [] -> mkInstrWithVarAnn GET+        [n] -> annsCnt (0, 0, 1) $> GETN va <*> integralFromExpr n+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_UPDATE -> case args of+        [] -> mkInstrWithVarAnn UPDATE+        [n] -> annsCnt (0, 0, 1) $> UPDATEN va <*> integralFromExpr n+        _ -> invalidNumArgs $ 0 :| [1]+      C_Prim_GET_AND_UPDATE -> mkInstrWithVarAnn GET_AND_UPDATE+      C_Prim_IF -> withArgsAnns nil IF+      C_Prim_LOOP -> withArgsAnns nil LOOP+      C_Prim_LOOP_LEFT -> withArgsAnns nil LOOP_LEFT+      C_Prim_LAMBDA -> withArgsAnns (0, 0, 1) $ LAMBDA va+      C_Prim_LAMBDA_REC -> withArgsAnns (0, 0, 1) $ LAMBDA_REC va+      C_Prim_EXEC -> mkInstrWithVarAnn EXEC+      C_Prim_APPLY -> mkInstrWithVarAnn APPLY+      C_Prim_DIP -> nilAnns *> case args of+        [ops] -> DIP <$> fromExp ops+        [n, ops] -> DIPN <$> fromExp n <*> fromExp ops+        _ -> invalidNumArgs $ 1 :| [2]+      C_Prim_FAILWITH -> withArgsAnns nil FAILWITH+      C_Prim_CAST -> withArgsAnns (0, 0, 1) $ CAST va+      C_Prim_RENAME -> mkInstrWithVarAnn RENAME+      C_Prim_PACK -> mkInstrWithVarAnn PACK+      C_Prim_UNPACK -> withArgsAnns (1, 0, 1) $ UNPACK ta va+      C_Prim_CONCAT -> mkInstrWithVarAnn CONCAT+      C_Prim_SLICE -> mkInstrWithVarAnn SLICE+      C_Prim_ISNAT -> mkInstrWithVarAnn ISNAT+      C_Prim_ADD -> mkInstrWithVarAnn ADD+      C_Prim_SUB -> mkInstrWithVarAnn SUB+      C_Prim_SUB_MUTEZ -> mkInstrWithVarAnn SUB_MUTEZ+      C_Prim_MUL -> mkInstrWithVarAnn MUL+      C_Prim_EDIV -> mkInstrWithVarAnn EDIV+      C_Prim_ABS -> mkInstrWithVarAnn ABS+      C_Prim_NEG -> mkInstrWithVarAnn NEG+      C_Prim_LSL -> mkInstrWithVarAnn LSL+      C_Prim_LSR -> mkInstrWithVarAnn LSR+      C_Prim_OR -> mkInstrWithVarAnn OR+      C_Prim_AND -> mkInstrWithVarAnn AND+      C_Prim_XOR -> mkInstrWithVarAnn XOR+      C_Prim_NOT -> mkInstrWithVarAnn NOT+      C_Prim_COMPARE -> mkInstrWithVarAnn COMPARE+      C_Prim_EQ -> mkInstrWithVarAnn Untyped.EQ+      C_Prim_NEQ -> mkInstrWithVarAnn NEQ+      C_Prim_LT -> mkInstrWithVarAnn Untyped.LT+      C_Prim_GT -> mkInstrWithVarAnn Untyped.GT+      C_Prim_LE -> mkInstrWithVarAnn LE+      C_Prim_GE -> mkInstrWithVarAnn GE+      C_Prim_INT -> mkInstrWithVarAnn INT+      C_Prim_NAT -> mkInstrWithVarAnn NAT+      C_Prim_BYTES -> mkInstrWithVarAnn BYTES+      C_Prim_VIEW -> withArgsAnns (0, 0, 1) $ VIEW va+      C_Prim_SELF -> withArgsAnns (0, 1, 1) $ SELF va fa+      C_Prim_CONTRACT -> withArgsAnns (0, 1, 1) $ CONTRACT va fa+      C_Prim_TRANSFER_TOKENS -> mkInstrWithVarAnn TRANSFER_TOKENS+      C_Prim_SET_DELEGATE -> mkInstrWithVarAnn SET_DELEGATE+      C_Prim_CREATE_CONTRACT -> withArgsAnns (0, 0, 2) $ CREATE_CONTRACT va1 va2+      C_Prim_IMPLICIT_ACCOUNT -> mkInstrWithVarAnn IMPLICIT_ACCOUNT+      C_Prim_NOW -> mkInstrWithVarAnn NOW+      C_Prim_AMOUNT -> mkInstrWithVarAnn AMOUNT+      C_Prim_BALANCE -> mkInstrWithVarAnn BALANCE+      C_Prim_VOTING_POWER -> mkInstrWithVarAnn VOTING_POWER+      C_Prim_TOTAL_VOTING_POWER -> mkInstrWithVarAnn TOTAL_VOTING_POWER+      C_Prim_CHECK_SIGNATURE -> mkInstrWithVarAnn CHECK_SIGNATURE+      C_Prim_SHA256 -> mkInstrWithVarAnn SHA256+      C_Prim_SHA512 -> mkInstrWithVarAnn SHA512+      C_Prim_BLAKE2B -> mkInstrWithVarAnn BLAKE2B+      C_Prim_SHA3 -> mkInstrWithVarAnn SHA3+      C_Prim_KECCAK -> mkInstrWithVarAnn KECCAK+      C_Prim_HASH_KEY -> mkInstrWithVarAnn HASH_KEY+      C_Prim_PAIRING_CHECK -> mkInstrWithVarAnn PAIRING_CHECK+      C_Prim_SOURCE -> mkInstrWithVarAnn SOURCE+      C_Prim_SENDER -> mkInstrWithVarAnn SENDER+      C_Prim_ADDRESS -> mkInstrWithVarAnn ADDRESS+      C_Prim_CHAIN_ID -> mkInstrWithVarAnn CHAIN_ID+      C_Prim_LEVEL -> mkInstrWithVarAnn LEVEL+      C_Prim_SELF_ADDRESS -> mkInstrWithVarAnn SELF_ADDRESS+      C_Prim_NEVER -> withArgsAnns nil NEVER+      C_Prim_TICKET_DEPRECATED -> mkInstrWithVarAnn TICKET_DEPRECATED+      C_Prim_TICKET -> mkInstrWithVarAnn TICKET+      C_Prim_READ_TICKET -> mkInstrWithVarAnn READ_TICKET+      C_Prim_SPLIT_TICKET -> mkInstrWithVarAnn SPLIT_TICKET+      C_Prim_JOIN_TICKETS -> mkInstrWithVarAnn JOIN_TICKETS+      C_Prim_OPEN_CHEST -> mkInstrWithVarAnn OPEN_CHEST+      C_Prim_SAPLING_EMPTY_STATE -> withArgsAnns (0, 0, 1) $ SAPLING_EMPTY_STATE va+      C_Prim_SAPLING_VERIFY_UPDATE -> mkInstrWithVarAnn SAPLING_VERIFY_UPDATE+      C_Prim_MIN_BLOCK_TIME -> withArgsRec e args $ mkInstrWithAnyAnns MIN_BLOCK_TIME+      C_Prim_EMIT -> annsCnt (0, 1, 1) $> EMIT va fa <*> case args of+        [] -> pure Nothing+        [ty] -> Just <$> fromExp ty+        _ -> invalidNumArgs (0 :| [1])+    s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTInstr (fromSing s)++    where+      annSet = toAnnSet anns+      va = firstAnn @VarTag annSet+      ta = firstAnn @TypeTag annSet+      fa = firstAnn @FieldTag annSet+      fa1 = fa+      fa2 = secondAnn @FieldTag annSet+      va1 = va+      va2 = secondAnn @VarTag annSet++      withArgsAnns+        :: WithArgsRec x a (InstrAbstract [] op)+        => (Int, Int, Int) -> a -> Either (FromExpError x) (InstrAbstract [] op)+      withArgsAnns n f = annsCnt n *> withArgsRec e args f++      invalidNumArgs :: NonEmpty Word -> Either (FromExpError x) b+      invalidNumArgs expected = Left $ FromExpError e $+        FEERArgumentCountMismatch expected (length args)++      annsCnt = checkAnnsCount e annSet++      nil = (0, 0, 0)++      nilAnns = annsCnt nil++      mkInstrWithVarAnn+        :: WithArgsRec x a (InstrAbstract [] op)+        => (Untyped.Annotation VarTag -> a)+        -> Either (FromExpError x) (InstrAbstract [] op)+      mkInstrWithVarAnn ctor = withArgsAnns (0, 0, 1) $ ctor va++      mkInstrWithAnyAnns :: ([Untyped.AnyAnn] -> t) -> t+      mkInstrWithAnyAnns ctor = ctor $ anns <&> \case+        AnnotationType x -> Untyped.AnyAnnType x+        AnnotationField x -> Untyped.AnyAnnField x+        AnnotationVariable x -> Untyped.AnyAnnVar x++  fromExp e = Left $ FromExpError e $ FEERExpectedPrim (one MPTInstr)++instance (FromExp x op) => FromExp x (Untyped.Contract' op) where+  fromExp blocks = case blocks of+    ExpSeq _ bs -> do+      bs' <- mapM exprToCB bs+      first (FromExpError blocks . FEERBadContractBlocks) $ orderContractBlock bs'+    expr -> Left $ FromExpError expr FEERExpectedSeq+    where+      exprToCB+        :: Exp x+        -> Either (FromExpError x) (ContractBlock op)+      exprToCB e@(ExpPrim' _ prim args anns) = withClassifiedPrim prim \case+        SMPTKeyword -> \case+          C_Prim_parameter -> mkCbParam e args anns+          C_Prim_storage   -> mkCBStorage e args anns+          C_Prim_code      -> mkCBCode e args anns+          C_Prim_view      -> mkCBView e args anns+        s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTKeyword (fromSing s)+      exprToCB e = Left $ FromExpError e $ FEERExpectedPrim $ one MPTKeyword++      mkCbParam+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCbParam e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *> case args of+        [p] -> do+          let annSet = toAnnSet (p ^. _ExpPrim . _2 . mpaAnnotsL)+              annCnt = annsCount annSet+          let rootAnn = firstAnn @FieldTag annSet+          unless (secondAnn @FieldTag annSet == noAnn) $+            Left $ FromExpError p $ FEERTooManyAnns (Nothing, Just 1, Nothing) annCnt+          p' <- fromExp @x @Ty+            (p & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . isAnnotationField))+          pure $ CBParam $ Untyped.ParameterType p' rootAnn+        _ -> Left $ FromExpError e $ FEERArgumentCountMismatch (one 1) (length args)++      mkCBStorage+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBStorage e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>+        withArgsRec e args CBStorage++      mkCBCode+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBCode e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>+        withArgsRec e args CBCode++      mkCBView+        :: Exp x+        -> [Exp x]+        -> [Annotation]+        -> Either (FromExpError x) (ContractBlock op)+      mkCBView e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>+        withArgsRec e args (CBView ... Untyped.View)++instance FromExp x Untyped.T where+  fromExp e@(ExpPrim' _ prim args anns) = assertNoAnns *> withClassifiedPrim prim \case+    SMPTType -> \case+      C_Prim_key -> withArgs Untyped.TKey+      C_Prim_unit -> withArgs Untyped.TUnit+      C_Prim_signature -> withArgs Untyped.TSignature+      C_Prim_chain_id -> withArgs Untyped.TChainId+      C_Prim_option -> withArgs Untyped.TOption+      C_Prim_list -> withArgs Untyped.TList+      C_Prim_set -> withArgs Untyped.TSet+      C_Prim_operation -> withArgs Untyped.TOperation+      C_Prim_contract -> withArgs Untyped.TContract+      C_Prim_ticket -> withArgs Untyped.TTicket+      C_Prim_or+        | [arg1, arg2] <- args -> 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+        | otherwise -> Left $ FromExpError e $+            FEERArgumentCountMismatch (one 2) (length args)+      C_Prim_pair -> do+        args2 <- case nonEmpty args >>= forbidSingletonList of+          Nothing -> Left $ FromExpError e $ FEERNotEnoughArguments 2 (length args)+          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+      C_Prim_lambda -> withArgs Untyped.TLambda+      C_Prim_map -> withArgs Untyped.TMap+      C_Prim_big_map -> withArgs Untyped.TBigMap+      C_Prim_int -> withArgs Untyped.TInt+      C_Prim_nat -> withArgs Untyped.TNat+      C_Prim_string -> withArgs Untyped.TString+      C_Prim_bytes -> withArgs Untyped.TBytes+      C_Prim_mutez -> withArgs Untyped.TMutez+      C_Prim_bool -> withArgs Untyped.TBool+      C_Prim_key_hash -> withArgs Untyped.TKeyHash+      C_Prim_bls12_381_fr -> withArgs Untyped.TBls12381Fr+      C_Prim_bls12_381_g1 -> withArgs Untyped.TBls12381G1+      C_Prim_bls12_381_g2 -> withArgs Untyped.TBls12381G2+      C_Prim_timestamp -> withArgs Untyped.TTimestamp+      C_Prim_address -> withArgs Untyped.TAddress+      C_Prim_chest -> withArgs Untyped.TChest+      C_Prim_chest_key -> withArgs Untyped.TChestKey+      C_Prim_tx_rollup_l2_address ->+        Left $ FromExpError e FEERUnsupported+      C_Prim_never -> withArgs Untyped.TNever+      C_Prim_sapling_state -> withArgs Untyped.TSaplingState+      C_Prim_sapling_transaction -> withArgs Untyped.TSaplingTransaction+      C_Prim_sapling_transaction_deprecated ->+        Left $ FromExpError e FEERDeprecated+    s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTType (fromSing s)+    where+      assertNoAnns = unless (null anns) $ Left $ FromExpError e FEERUnexpectedAnnotations+      withArgs :: WithArgsRec x a Untyped.T => a -> Either (FromExpError x) Untyped.T+      withArgs = withArgsRec e args++      removeAnns :: Exp x -> (Annotation -> Bool) -> Exp x+      removeAnns expr p =+        expr & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . p)+  fromExp e = Left $ FromExpError e $ FEERExpectedPrim $ one MPTType++instance FromExp x Ty where+  fromExp e = case e of+    ExpPrim' ex primName args anns -> do+      let annSet = toAnnSet anns+          annCnt = annsCount annSet+      let ta = firstAnn @TypeTag annSet+      when (secondAnn @TypeTag annSet /= noAnn) $+        Left $ FromExpError e $ FEERTooManyAnns (Just 1, Nothing, Nothing) annCnt+      t <- fromExp @x @Untyped.T $ ExpPrim' ex primName args $ filter+        (not . isAnnotationType) anns+      pure $ Ty t ta+    _ -> Left $ FromExpError e $ FEERExpectedPrim (one MPTType)++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 (LambdaCode instr) -> pure $ rfAnyInstr instr+      VLam LambdaCodeRec{} -> Left $ FromExpError expr $+        FEERUnexpectedPrim Nothing Prim_Lambda_rec++instance FromExp x ViewName where+  fromExp e = case e of+    ExpString _ s ->+      first (FromExpError e . FEERViewNameError) $ mkViewName s+    _ -> Left $ FromExpError e FEERExpectedString++----------------------------------------------------------------------------+-- 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) = do+  let actualCount = annsCount annSet+  unless (actualCount <= maxCount) $+    Left $ FromExpError e $ FEERTooManyAnns (Just maxTas, Just maxFas, Just maxVas) actualCount++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 FEEROutOfBounds)+      (fromIntegralMaybe @Integer v)+  _ -> Left $ FromExpError e FEERExpectedNumber