lorentz 0.7.1 → 0.8.0

raw patch · 26 files changed

+1276/−316 lines, 26 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGES.md +32/−0
• README.md +6/−9
• lorentz.cabal +7/−3
• src/Lorentz.hs +3/−0
• src/Lorentz/ADT.hs +17/−16
• src/Lorentz/Annotation.hs +2/−0
• src/Lorentz/Base.hs +5/−19
• src/Lorentz/Bytes.hs +216/−0
• src/Lorentz/Coercions.hs +14/−1
• src/Lorentz/ContractRegistry.hs +48/−22
• src/Lorentz/Default.hs +50/−0
• src/Lorentz/Doc.hs +34/−2
• src/Lorentz/Entrypoints/Doc.hs +93/−20
• src/Lorentz/Errors.hs +5/−0
• src/Lorentz/Ext.hs +28/−4
• src/Lorentz/Extensible.hs +5/−5
• src/Lorentz/Instr.hs +114/−90
• src/Lorentz/Iso.hs +67/−0
• src/Lorentz/Macro.hs +110/−63
• src/Lorentz/Pack.hs +23/−6
• src/Lorentz/ReferencedByName.hs +11/−4
• src/Lorentz/Run/Simple.hs +89/−0
• src/Lorentz/StoreClass.hs +232/−31
• src/Lorentz/UParam.hs +4/−4
• src/Lorentz/Value.hs +16/−2
• src/Lorentz/Zip.hs +45/−15

@@ -1,3 +1,35 @@+0.8.0+=====+* [!671](https://gitlab.com/morley-framework/morley/-/merge_requests/671)+  + Add `TypeHasDoc` instances for `TAddress` and `FutureContract`.+  + Add a generic `instance DocItem (DEntrypoint ep)`.+    In case of getting overlapping instances, you have to implement `EntrypointKindHasDoc` instead.+  + Some error messages in doc tests are improved.+  + Some bugfixes for anchors.+  + Cases with contract logic residing outside of entrypoints are now better handled.+* [!665](https://gitlab.com/morley-framework/morley/-/merge_requests/665)+  Improve `StorageContains` to work for polymorphic case (when field is marked with `Identity`).+* [!679](https://gitlab.com/morley-framework/morley/-/merge_requests/679)+  Add `dupLNamed`.+* [!672](https://gitlab.com/morley-framework/morley/-/merge_requests/672)+  + Add `Packed`, `TSignature` and `Hash` types.+  + `pack` and `unpack` now work with `Packed` instead of `ByteString` (for the sake of better type-safety).+    Either use `Packed` type, or `packRaw`/`unpackRaw` instructions.+  + `checkSignature` now works with `Packed` and `TSignature`.+  + `blake2b` and other hashing instructions now work with `Hash`.+  + If necessary, coersions can be used to switch between the mentioned types and raw `ByteString`.+* [!667](https://gitlab.com/morley-framework/morley/-/merge_requests/667)+  + Modify representation of extended lambdas+    (arbitrary code used as lambdas is now packed into right-hand combs, not left-hand ones).+  + Add `applicate` macro.+* [!630](https://gitlab.com/morley-framework/morley/-/merge_requests/630)+  Use `:` in all library instructions instead of `&`.+* [!652](https://gitlab.com/morley-framework/morley/-/merge_requests/652)+  Update the `ContractRegistry` to be able to not require contract name for+  all its commands when there is only one contract.+* [!640](https://gitlab.com/morley-framework/morley/-/merge_requests/640)+  Change `StoreSubmapOps` to contain no optional methods.+ 0.7.1 ===== * [!653](https://gitlab.com/morley-framework/morley/-/merge_requests/653)

@@ -37,11 +37,8 @@ (inp :: [Kind.Type]) :-> (out :: [Kind.Type]) ``` -In order to list types on the stack, we will use `&` operator:-```haskell-(a :: Kind.Type) & (b :: [Kind.Type]) = a ': b-```-For example, `Natural & Integer & Bool & '[]`.+In order to list types on the stack, we will use `:` operator.+For example, `Natural : Integer : Bool : '[]`.  Such design provides a nice code decomposition ability. @@ -66,7 +63,7 @@   deriving stock Generic   deriving anyclass IsoValue -showTrafficLight :: TrafficLight & s :-> MText & s+showTrafficLight :: TrafficLight : s :-> MText : s showTrafficLight = caseT   ( #cRed /-> push [mt|Red|]   , #cYellow /-> push [mt|Yellow|]@@ -76,13 +73,13 @@ * `RebindableSyntax` for Lorentz instructions, including `do` notation and `if` operator  ```haskell-sumIsGt10 :: Integer & Integer & s :-> Bool & s+sumIsGt10 :: Integer : Integer : s :-> Bool : s sumIsGt10 = do   add   dip $ push @Integer 10   gt -foo :: Integer & s :-> Integer & s+foo :: Integer : s :-> Integer : s foo = do   dup   sumIsGt10@@ -100,7 +97,7 @@   } deriving stock Generic     deriving anyclass IsoValue -getFullName :: UserInfo & s :-> MText & s+getFullName :: UserInfo : s :-> MText : s getFullName = do   getField #firstName   dip $ toField #secondName

@@ -1,11 +1,11 @@-cabal-version: 2.2+cabal-version: 2.0  -- This file has been generated from package.yaml by hpack version 0.34.2. -- -- see: https://github.com/sol/hpack  name:           lorentz-version:        0.7.1+version:        0.8.0 synopsis:       EDSL for the Michelson Language description:    Lorentz is a powerful meta-programming tool which allows one to write Michelson contracts directly in Haskell. It has the same instructions as Michelson, but operates on Haskell values and allows one to use Haskell features. category:       Language@@ -33,12 +33,14 @@       Lorentz.Annotation       Lorentz.Arith       Lorentz.Base+      Lorentz.Bytes       Lorentz.Coercions       Lorentz.Common       Lorentz.Constraints       Lorentz.Constraints.Derivative       Lorentz.Constraints.Scopes       Lorentz.ContractRegistry+      Lorentz.Default       Lorentz.Doc       Lorentz.Empty       Lorentz.Entrypoints@@ -55,6 +57,7 @@       Lorentz.Ext       Lorentz.Extensible       Lorentz.Instr+      Lorentz.Iso       Lorentz.Macro       Lorentz.OpSize       Lorentz.Pack@@ -65,6 +68,7 @@       Lorentz.Referenced       Lorentz.ReferencedByName       Lorentz.Run+      Lorentz.Run.Simple       Lorentz.StoreClass       Lorentz.UParam       Lorentz.Util.TH@@ -77,7 +81,7 @@       Paths_lorentz   hs-source-dirs:       src-  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns+  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses 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   build-depends:       aeson-pretty

@@ -10,6 +10,7 @@ import Lorentz.Annotation as Exports import Lorentz.Arith as Exports import Lorentz.Base as Exports+import Lorentz.Bytes as Exports import Lorentz.Coercions as Exports import Lorentz.Common as Exports import Lorentz.Constraints as Exports@@ -22,6 +23,7 @@ import Lorentz.Errors.Numeric as Exports import Lorentz.Ext as Exports import Lorentz.Instr as Exports+import Lorentz.Iso as Exports import Lorentz.Macro as Exports import Lorentz.OpSize as Exports import Lorentz.Pack as Exports@@ -32,6 +34,7 @@ import Lorentz.Referenced as Exports import Lorentz.ReferencedByName as Exports import Lorentz.Run as Exports+import Lorentz.Run.Simple as Exports import Lorentz.StoreClass as Exports import Lorentz.UParam as Exports import Lorentz.Util.TH as Exports

@@ -3,6 +3,7 @@ -- SPDX-License-Identifier: LicenseRef-MIT-TQ  {-# LANGUAGE FunctionalDependencies #-}+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}  module Lorentz.ADT   ( HasField@@ -52,9 +53,9 @@ import Lorentz.Instr import Michelson.Typed.Haskell.Instr import Michelson.Typed.Haskell.Value-import Util.TypeTuple import Util.Label (Label) import Util.Type (type (++), KnownList)+import Util.TypeTuple  -- | Allows field access and modification. type HasField dt fname =@@ -88,28 +89,28 @@ toField   :: forall dt name st.      InstrGetFieldC dt name-  => Label name -> dt & st :-> GetFieldType dt name & st+  => Label name -> dt : st :-> GetFieldType dt name : st toField = I . instrGetField @dt  -- | Like 'toField', but leaves field named. toFieldNamed   :: forall dt name st.      InstrGetFieldC dt name-  => Label name -> dt & st :-> (name :! GetFieldType dt name) & st+  => Label name -> dt : st :-> (name :! GetFieldType dt name) : st toFieldNamed l = toField l # forcedCoerce_  -- | Extract a field of a datatype, leaving the original datatype on stack. getField   :: forall dt name st.      InstrGetFieldC dt name-  => Label name -> dt & st :-> GetFieldType dt name & dt ': st+  => Label name -> dt : st :-> GetFieldType dt name : dt ': st getField l = dup # toField @dt l  -- | Like 'getField', but leaves field named. getFieldNamed   :: forall dt name st.      InstrGetFieldC dt name-  => Label name -> dt & st :-> (name :! GetFieldType dt name) & dt ': st+  => Label name -> dt : st :-> (name :! GetFieldType dt name) : dt ': st getFieldNamed l = getField l # coerceWrap  -- | Set a field of a datatype.@@ -127,7 +128,7 @@      )   => Label name   -> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))-  -> dt & st :-> dt & st+  -> dt : st :-> dt : st modifyField l i = getField @dt l # i # setField @dt l  -- | Make up a datatype. You provide a pack of individual fields constructors.@@ -144,7 +145,7 @@      , RMap (ConstructorFieldTypes dt)      )   => Rec (FieldConstructor st) (ConstructorFieldTypes dt)-  -> st :-> dt & st+  -> st :-> dt : st construct fctors =   I $ instrConstruct @dt $   rmap (\(FieldConstructor i) -> FieldConstructor i) fctors@@ -158,7 +159,7 @@      , RecFromTuple fctors      )   => IsoRecTuple fctors-  -> st :-> dt & st+  -> st :-> dt : st constructT = construct . recFromTuple  -- | Construct an object from fields on the stack.@@ -168,7 +169,7 @@   , ToTs fields ~ ToTs (ConstructorFieldTypes dt)   , KnownList fields   )-  => (fields ++ st) :-> dt & st+  => (fields ++ st) :-> dt : st constructStack =   I (instrConstructStack @dt @(ToTs fields))       \\ totsKnownLemma @fields@@ -181,14 +182,14 @@   , KnownList fields   , ToTs fields ~ ToTs (ConstructorFieldTypes dt)   )-  => dt & st :-> (fields ++ st)+  => dt : st :-> (fields ++ st) deconstruct =   I (instrDeconstruct @dt @(ToTs fields))     \\ totsKnownLemma @fields     \\ totsAppendLemma @fields @st  -- | Lift an instruction to field constructor.-fieldCtor :: HasCallStack => (st :-> f & st) -> FieldConstructor st f+fieldCtor :: HasCallStack => (st :-> f : st) -> FieldConstructor st f fieldCtor = \case   I i -> FieldConstructor i   FI _ -> error "Field constructor always fails"@@ -197,7 +198,7 @@ wrap_   :: forall dt name st.      InstrWrapC dt name-  => Label name -> (AppendCtorField (GetCtorField dt name) st) :-> dt & st+  => Label name -> (AppendCtorField (GetCtorField dt name) st) :-> dt : st wrap_ =   case appendCtorFieldAxiom @(GetCtorField dt name) @st of     Dict -> I . instrWrap @dt@@ -206,7 +207,7 @@ wrapOne   :: forall dt name st.      InstrWrapOneC dt name-  => Label name -> (CtorOnlyField name dt ': st) :-> dt & st+  => Label name -> (CtorOnlyField name dt ': st) :-> dt : st wrapOne = case appendCtorFieldAxiom @(GetCtorField dt name) @st of   Dict -> I . instrWrapOne @dt @@ -242,7 +243,7 @@      ( InstrCaseC dt      , RMap (CaseClauses dt)      )-  => Rec (CaseClauseL inp out) (CaseClauses dt) -> dt & inp :-> out+  => Rec (CaseClauseL inp out) (CaseClauses dt) -> dt : inp :-> out case_ = LorentzInstr . instrCase @dt . rmap coerceCaseClause   where     coerceCaseClause@@ -262,7 +263,7 @@ caseT   :: forall dt out inp clauses.      CaseTC dt out inp clauses-  => IsoRecTuple clauses -> dt & inp :-> out+  => IsoRecTuple clauses -> dt : inp :-> out caseT = case_ @dt . recFromTuple  type CaseTC dt out inp clauses =@@ -276,7 +277,7 @@ unwrapUnsafe_   :: forall dt name st.      InstrUnwrapC dt name-  => Label name -> dt & st :-> (CtorOnlyField name dt ': st)+  => Label name -> dt : st :-> (CtorOnlyField name dt ': st) unwrapUnsafe_ =   case appendCtorFieldAxiom @(GetCtorField dt name) @st of     Dict -> I . instrUnwrapUnsafe @dt

@@ -183,6 +183,8 @@ instance HasAnnotation Operation where   getAnnotation _ = starNotes +instance (HasAnnotation a, HasAnnotation b) => HasAnnotation (Either a b)+ instance (HasAnnotation a, HasAnnotation b) => HasAnnotation (a, b) instance (HasAnnotation a, HasAnnotation b, HasAnnotation c) => HasAnnotation (a, b, c) instance (HasAnnotation a, HasAnnotation b, HasAnnotation c, HasAnnotation d) => HasAnnotation (a, b, c, d)

@@ -10,7 +10,6 @@   , type (%>)   , type (&)   , (#)-  , (##)   , pattern I   , pattern FI   , iGenericIf@@ -100,7 +99,7 @@   RfAlwaysFails instr -> LorentzInstr $ RfAlwaysFails $     InstrWithVarNotes (NE.fromList $ map U.AnnotationUnsafe annots) instr --- There is also @instance IsoValue (i :-> o)@ in a separate module.+-- There is also @instance IsoValue (i :-> o)@ in the "Lorentz.Zip" module.  -- | Alias for ':->', seems to make signatures more readable sometimes. --@@ -117,6 +116,10 @@     => ContractCode cp st     -> SomeContractCode +-- | An alias for ':'.+--+-- We discourage its use as this hinders reading error messages+-- (the compiler inserts unnecessary parentheses and indentation). type (&) (a :: Kind.Type) (b :: [Kind.Type]) = a ': b infixr 2 & @@ -125,23 +128,6 @@ I l # FI r = FI (l `Seq` r) FI l # _ = FI l infixl 8 #---- | Version of '#' which performs some optimizations immediately.------ In particular, this avoids glueing @Nop@s.-(##) :: (a :-> b) -> (b :-> c) -> (a :-> c)-l ## r =-  -- We are very verbose about cases to avoid-  -- significant compilation time increase-  case l of-    I Nop -> case r of-      I x -> I x-      _ -> l # r-    I x -> case r of-      I Nop -> I x-      _ -> l # r-    _ -> l # r-  type Lambda i o = '[i] :-> '[o] 

@@ -0,0 +1,216 @@+-- SPDX-FileCopyrightText: 2020 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# LANGUAGE NoPolyKinds #-}++-- | Type-safe operations with @bytes@-like data.+module Lorentz.Bytes+  ( BytesLike (..)++  , Packed (..)++  , TSignature (..)+  , lSignEd22519++  , Hash (..)+  , DHashAlgorithm+  , KnownHashAlgorithm (..)+  , toHashHs+  , Sha256+  , Sha512+  , Blake2b+  ) where++import qualified Data.Kind as Kind+import Fmt (Buildable(..))+import qualified Type.Reflection as Refl+import Util.Markdown++import Lorentz.Annotation+import Lorentz.Base+import Lorentz.Constraints.Scopes+import Lorentz.Doc+import Lorentz.Value+import qualified Michelson.Typed as T+import Tezos.Crypto+import qualified Tezos.Crypto.Ed25519 as Ed22519+import qualified Tezos.Crypto.Hash as Crypto++-- | Everything which is represented as bytes inside.+class (KnownValue bs, ToT bs ~ ToT ByteString) => BytesLike bs where+  toBytes :: bs -> ByteString++instance BytesLike ByteString where+  toBytes = id++----------------------------------------------------------------------------+-- Packing+----------------------------------------------------------------------------++-- | Represents a 'ByteString' resulting from packing a value of type @a@.+--+-- This is /not/ guaranteed to keep some packed value, and @unpack@ can fail.+-- We do so because often we need to accept values of such type from user,+-- and also because there is no simple way to check validity of packed data+-- without performing full unpack.+-- So this wrapper is rather a hint for users.+newtype Packed a = Packed { unPacked :: ByteString }+  deriving stock (Show, Eq, Ord, Generic)+  deriving newtype (IsoValue, HasAnnotation, BytesLike)++instance Buildable (Packed a) where+  build = build . toVal++instance TypeHasDoc a => TypeHasDoc (Packed a) where+  typeDocMdDescription = [md|+    Packed value of the given type.+    This exactly matches the result of Michelson `PACK` instruction application+    to the given value.+    |]+  typeDocMdReference = poly1TypeDocMdReference+  typeDocDependencies p =+    genericTypeDocDependencies p <>+    [ dTypeDep @a+    , dTypeDep @MText, dTypeDep @Integer  -- for examples below+    ]+  typeDocHaskellRep = concreteTypeDocHaskellRep @(Packed (MText, Integer))+  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(Packed (MText, Integer))++----------------------------------------------------------------------------+-- Signatures+----------------------------------------------------------------------------++-- | Represents a signature, where signed data has given type.+--+-- Since we usually sign a packed data, a common pattern for this type is+-- @TSignature ('Packed' signedData)@.+-- If you don't want to use 'Packed', use plain @TSignature ByteString@ instead.+newtype TSignature a = TSignature { unTSignature :: Signature }+  deriving stock (Show, Generic)+  deriving newtype (IsoValue, HasAnnotation)++instance Buildable (TSignature a) where+  build = build . toVal++instance TypeHasDoc a => TypeHasDoc (TSignature a) where+  typeDocMdDescription = "Signature for data of the given type."+  typeDocMdReference = poly1TypeDocMdReference+  typeDocDependencies p =+    genericTypeDocDependencies p <>+    [ dTypeDep @a+    , dTypeDep @MText, dTypeDep @Integer  -- for examples below+    ]+  typeDocHaskellRep = concreteTypeDocHaskellRep @(TSignature (MText, Integer))+  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(TSignature (MText, Integer))++-- | Sign data using Ed25519 curve.+-- TODO [#456]: handle other methods, either all at once (if viable) or each one separately+lSignEd22519 :: BytesLike a => Ed22519.SecretKey -> a -> TSignature a+lSignEd22519 sk (toBytes -> bs) =+  TSignature . SignatureEd25519 $ Ed22519.sign sk bs++----------------------------------------------------------------------------+-- Hashes+----------------------------------------------------------------------------++-- | Open kind for hash algorithms, to make it more difficult to apply type+-- arguments incorrectly.+type HashAlgorithmKind = HashAlgoTag -> Kind.Type+data HashAlgoTag++-- | Hash of type @t@ evaluated from data of type @a@.+newtype Hash (alg :: HashAlgorithmKind) a = HashUnsafe { unHash :: ByteString }+  deriving stock (Show, Eq, Ord, Generic)+  deriving newtype (IsoValue, HasAnnotation, BytesLike)++instance Buildable (Hash alg a) where+  build = build . toVal++instance (KnownHashAlgorithm alg, TypeHasDoc a) => TypeHasDoc (Hash alg a) where+  typeDocMdDescription = [md|+    Hash of a value.++    First type argument denotes algorithm used to compute the hash, and the second+    argument describes the data being hashed.+    |]++  typeDocMdReference tp wp =+    T.applyWithinParens wp $ mconcat+      [ mdLocalRef (mdTicked "Hash") (docItemRef (DType tp))+      , " "+      , hashAlgorithmMdRef (Proxy @alg)+      , " "+      , typeDocMdReference (Proxy @a) (T.WithinParens True)+      ]++  typeDocDependencies p =+    genericTypeDocDependencies p <>+    [ SomeDocDefinitionItem (DHashAlgorithm (Proxy @alg)), dTypeDep @a+    , SomeDocDefinitionItem (DHashAlgorithm (Proxy @Blake2b)), dTypeDep @ByteString+        --- ^ for examples below+    ]+  typeDocHaskellRep = concreteTypeDocHaskellRep @(Hash Blake2b ByteString)+  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(Hash Blake2b ByteString)++-- | Hash algorithm used in Tezos.+class Typeable alg => KnownHashAlgorithm (alg :: HashAlgorithmKind) where+  hashAlgorithmName :: Proxy alg -> Text+  hashAlgorithmName _ =+    toText . Refl.tyConName . Refl.typeRepTyCon $ Refl.typeRep @alg++  computeHash :: ByteString -> ByteString+  toHash :: BytesLike bs => bs : s :-> Hash alg bs : s++-- | Evaluate hash in Haskell world.+toHashHs+  :: forall alg bs. (BytesLike bs, KnownHashAlgorithm alg)+  => bs -> Hash alg bs+toHashHs = HashUnsafe . computeHash @alg . toBytes++-- | Documentation item for hash algorithms.+data DHashAlgorithm where+  DHashAlgorithm :: KnownHashAlgorithm alg => Proxy alg -> DHashAlgorithm++instance Eq DHashAlgorithm where+  a == b = (a `compare` b) == EQ+instance Ord DHashAlgorithm where+  DHashAlgorithm a `compare` DHashAlgorithm b =+    hashAlgorithmName a `compare` hashAlgorithmName b++instance DocItem DHashAlgorithm where+  type DocItemPlacement DHashAlgorithm = 'DocItemInDefinitions+  type DocItemReferenced DHashAlgorithm = 'True+  docItemPos = 5310+  docItemSectionName = Just "Referenced hash algorithms"++  docItemRef (DHashAlgorithm alg) =+    DocItemRef $ DocItemId ("hash-alg-" <> hashAlgorithmName alg)++  docItemToMarkdown _ (DHashAlgorithm alg) =+    "* " <> build (hashAlgorithmName alg)++-- Creates a reference to given hash algorithm description.+hashAlgorithmMdRef :: KnownHashAlgorithm alg => Proxy alg -> Markdown+hashAlgorithmMdRef alg =+  mdLocalRef+    (mdTicked . build $ hashAlgorithmName alg)+    (docItemRef (DHashAlgorithm alg))++data Sha256 :: HashAlgorithmKind++instance KnownHashAlgorithm Sha256 where+  computeHash = Crypto.sha256+  toHash = I T.SHA256++data Sha512 :: HashAlgorithmKind++instance KnownHashAlgorithm Sha512 where+  computeHash = Crypto.sha512+  toHash = I T.SHA512++data Blake2b :: HashAlgorithmKind++instance KnownHashAlgorithm Blake2b where+  computeHash = Crypto.blake2b+  toHash = I T.BLAKE2B

@@ -2,6 +2,8 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ -- | Identity transformations between different Haskell types. module Lorentz.Coercions   ( -- * Safe coercions@@ -39,11 +41,13 @@  import Lorentz.Address import Lorentz.Base+import Lorentz.Bytes import Lorentz.Instr import Lorentz.Value import Lorentz.Wrappable (Wrappable(..)) import Lorentz.Zip import Michelson.Typed+ ---------------------------------------------------------------------------- -- Unsafe coercions ----------------------------------------------------------------------------@@ -72,7 +76,7 @@ -- Still, produced Michelson code will always be valid. -- -- Prefer using one of more specific functions from this module.-forcedCoerce_ :: MichelsonCoercible a b => a & s :-> b & s+forcedCoerce_ :: MichelsonCoercible a b => a : s :-> b : s forcedCoerce_ = I Nop  gForcedCoerce_ :: MichelsonCoercible (t a) (t b) => t a : s :-> t b : s@@ -250,3 +254,12 @@ instance Address `CanCastTo` TAddress p  instance FutureContract p `CanCastTo` EpAddress++instance Packed a `CanCastTo` ByteString+instance TSignature a `CanCastTo` ByteString+instance Hash alg a `CanCastTo` ByteString++instance CanCastTo a b => Packed a `CanCastTo` Packed b+instance CanCastTo a b => TSignature a `CanCastTo` TSignature b+instance (CanCastTo alg1 alg2, CanCastTo a1 a2) =>+         Hash alg1 a1 `CanCastTo` Hash alg2 a2

@@ -66,20 +66,29 @@ newtype ContractRegistry = ContractRegistry   { unContractRegistry :: Map Text ContractInfo } -getContract :: Text -> ContractRegistry -> IO ContractInfo-getContract name registry =-  case Map.lookup name (unContractRegistry registry) of+getContract :: Maybe Text -> ContractRegistry -> IO (ContractInfo, Text)+getContract mName registry =+  case mName of+    Just name ->+      case Map.lookup name (unContractRegistry registry) of+        Nothing ->+          die $ "No contract with name '" +| name |+ "' found\n" +| registry |+ ""+        Just c -> pure (c, name)     Nothing ->-      die $ "No contract with name '" +| name |+ "' found\n" +| registry |+ ""-    Just c -> pure c+      -- When there is exactly one contract, return it.+      case Map.toList (unContractRegistry registry) of+        [(ci, n)] -> pure (n, ci)+        [] -> die $ "No contract found"+        _ ->+          die $ "Multiple contracts found. Please provide a name.\n" +| registry |+ ""  instance Buildable ContractRegistry where   build registry =     nameF "Available contracts" (blockListF $ keys (unContractRegistry registry)) -printContractFromRegistryDoc :: Text -> ContractRegistry -> DGitRevision -> Maybe FilePath -> IO ()-printContractFromRegistryDoc name contracts gitRev mOutput = do-  ContractInfo{..} <- getContract name contracts+printContractFromRegistryDoc :: Maybe Text -> ContractRegistry -> DGitRevision -> Maybe FilePath -> IO ()+printContractFromRegistryDoc mName contracts gitRev mOutput = do+  (ContractInfo{..}, name) <- getContract mName contracts   if ciIsDocumented   then      writeFunc (toString name <> ".md") mOutput $@@ -92,9 +101,9 @@ -- | 'ContractRegistry' actions parsed from CLI. data CmdLnArgs   = List-  | Print Text (Maybe FilePath) Bool Bool-  | Document Text (Maybe FilePath) DGitRevision-  | Analyze Text+  | Print (Maybe Text) (Maybe FilePath) Bool Bool+  | Document (Maybe Text) (Maybe FilePath) DGitRevision+  | Analyze (Maybe Text)   | PrintStorage SomeNiceStorage Bool  argParser :: ContractRegistry -> DGitRevision -> Opt.Parser CmdLnArgs@@ -103,7 +112,14 @@   , printSubCmd   , documentSubCmd   , analyzerSubCmd-  ] <> mapMaybe storageSubCmd (Map.toList $ unContractRegistry registry)+  ] <> (+    case (nonEmpty $ Map.toList $ unContractRegistry registry) of+      Just (a :| []) ->+        -- When there is exactly one contract.+        mapMaybe storageSubCmdSingle [a]+      _ ->+        mapMaybe storageSubCmd (Map.toList $ unContractRegistry registry)+  )   where     mkCommandParser commandName parser desc =       Opt.command commandName $@@ -117,20 +133,20 @@      printSubCmd =       mkCommandParser "print"-      (Print <$> nameOption <*> outputOptions <*> onelineOption <*> michelineOption)+      (Print <$> mNameption <*> outputOptions <*> onelineOption <*> michelineOption)       "Dump a contract in form of Michelson code"      documentSubCmd =       mkCommandParser "document"-      (Document <$> nameOption <*> outputOptions <*> pure gitRev)+      (Document <$> mNameption <*> outputOptions <*> pure gitRev)       "Dump contract documentation in Markdown"      analyzerSubCmd =       mkCommandParser "analyze"-      (Analyze <$> nameOption)+      (Analyze <$> mNameption)       "Analyze the contract and prints statistics about it." -    nameOption = Opt.strOption $ mconcat+    mNameption = optional . Opt.strOption $ mconcat       [ Opt.short 'n'       , Opt.long "name"       , Opt.metavar "IDENTIFIER"@@ -165,12 +181,22 @@         (PrintStorage . SomeNiceStorage <$> storageParser <*> michelineOption)         ("Print initial storage for the contract '" <> name <> "'") +    -- | This will generated `storage` command instead of `storage-<contractName>` commands+    -- Useful when there is exactly one contract.+    storageSubCmdSingle ::+      (Text, ContractInfo) -> Maybe $ Opt.Mod Opt.CommandFields CmdLnArgs+    storageSubCmdSingle (toString -> name, ContractInfo {..}) = do+      storageParser <- ciStorageParser+      pure $ mkCommandParser "storage"+        (PrintStorage . SomeNiceStorage <$> storageParser <*> michelineOption)+        ("Print initial storage for the contract '" <> name <> "'")+ -- | Run an action operating with 'ContractRegistry'. runContractRegistry :: ContractRegistry -> CmdLnArgs -> IO () runContractRegistry registry = \case   List -> pretty registry-  Print name mOutput forceOneLine useMicheline -> do-    ContractInfo{..} <- getContract name registry+  Print mName mOutput forceOneLine useMicheline -> do+    (ContractInfo{..}, name) <- getContract mName registry     let       compiledContract = case ciStorageNotes of         Just notes -> (compileLorentzContract ciContract) { M.cStoreNotes = notes }@@ -179,10 +205,10 @@       if useMicheline       then toLazyText $ encodePrettyToTextBuilder $ toExpression compiledContract       else printTypedContract forceOneLine $ compiledContract-  Document name mOutput gitRev -> do-    printContractFromRegistryDoc name registry gitRev mOutput-  Analyze name -> do-    ContractInfo{..} <- getContract name registry+  Document mName mOutput gitRev -> do+    printContractFromRegistryDoc mName registry gitRev mOutput+  Analyze mName -> do+    (ContractInfo{..}, _) <- getContract mName registry     let compiledContract  =           compileLorentzContract ciContract     putTextLn $ pretty $ analyze $ M.cCode compiledContract

@@ -0,0 +1,50 @@+-- SPDX-FileCopyrightText: 2020 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- | Default values for Lorentz.+module Lorentz.Default+  ( LDefault (..)+  ) where++import qualified Prelude as P++import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Value+import Util.Named+import Util.TypeLits++-- | Lorentz version of 'Default'.+class LDefault a where+  ldef :: a+  default ldef :: Default a => a+  ldef = def++  lIsDef :: a : s :-> Bool : s+  default lIsDef+    :: (NiceConstant a, NiceComparable a) => a : s :-> Bool : s+  lIsDef = push ldef # eq++instance LDefault Integer+instance LDefault Natural++instance LDefault [a] where+  lIsDef = isEmpty+instance LDefault (Set k) where+  lIsDef = isEmpty+instance LDefault (Map k v) where+  lIsDef = isEmpty+-- We do not provide an instance for 'BigMap' since+-- it cannot be checked on emptiness++instance (LDefault a, KnownSymbol n) => LDefault (n :! a) where+  ldef = P.fromLabel .! ldef+  lIsDef = fromNamed P.fromLabel # lIsDef++instance (LDefault a, LDefault b) => LDefault (a, b) where+  ldef = (ldef, ldef)+  lIsDef = unpair # dip lIsDef # lIsDef # and

@@ -47,6 +47,7 @@   , docDefinitionRef   , contractDocToMarkdown   , subDocToMarkdown+  , docItemSectionRef    , TypeHasDoc (..)   , SomeTypeWithDoc (..)@@ -113,8 +114,10 @@  -- | Inserts general information about the contract using the default format. ----- Currently we only include git revision. It is unknown in the--- library code and is supposed to be updated in an executable.+-- This includes git revision and some other information common+-- for all contracts.+-- Git revision is left unknown in the library code and is supposed+-- to be updated in an executable using e.g. 'buildLorentzDocWithGitRev'. contractGeneralDefault :: s :-> s contractGeneralDefault =   (contractGeneral $ doc DGitRevisionUnknown) #@@ -179,6 +182,35 @@     ( Just "Code [Integer, Natural, MText, ()] [ByteString]"     , demote @(ToT ([Integer, Natural, MText, ()] :-> '[ByteString]))     )++instance TypeHasDoc p => TypeHasDoc (TAddress p) where+  typeDocMdDescription = [md|+    A typed version of address primitive.++    Type in `TAddress` denotes parameter type of the target contract.++    This is not assumed to carry an entrypoint name.+    |]+  typeDocMdReference = poly1TypeDocMdReference+  typeDocDependencies _ = [dTypeDep @()]+  typeDocHaskellRep _ _ = Nothing+  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(TAddress ())++instance TypeHasDoc p => TypeHasDoc (FutureContract p) where+  typeDocName _ = "FutureContract"+  typeDocMdDescription = [md|+    A typed version of address primitive.++    Type in `FutureContract` denotes argument type of the target _entrypoint_.+    This address can carry an entrypoint name.++    We use `FutureContract` as a replacement for Michelson's `contract`, since+    places where the latter can appear are severely restricted.+    |]+  typeDocMdReference = poly1TypeDocMdReference+  typeDocDependencies _ = [dTypeDep @()]+  typeDocHaskellRep _ _ = Nothing+  typeDocMichelsonRep = concreteTypeDocMichelsonRep @(FutureContract ())  -- | Modify the example value of an entrypoint data DEntrypointExample = forall t . ParameterScope t => DEntrypointExample (Value t)

@@ -2,12 +2,19 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ -- | Utilities for declaring and documenting entry points. module Lorentz.Entrypoints.Doc   ( DEntrypoint (..)+  , pattern DEntrypointDocItem+  , EntrypointKindHasDoc (..)+  , entrypointSection   , DEntrypointReference (..)   , EntryArrow (..)   , PlainEntrypointsKind+  , CommonContractBehaviourKind+  , CommonEntrypointsBehaviourKind   , diEntrypointToMarkdown   , DEntrypointArg (..)   , DType (..)@@ -64,6 +71,7 @@ import Util.Label (Label) import Util.Markdown import Util.Type+import Util.Typeable import Util.TypeLits import Util.TypeTuple @@ -80,7 +88,15 @@   , depSub :: SubDoc   } --- | Default implementation of 'docItemToMarkdown' for entry points.+-- | Pattern that checks whether given 'SomeDocItem' hides 'DEntrypoint' inside+-- (of any entrypoint kind).+--+-- In case a specific kind is necessary, use plain @(cast -> Just DEntrypoint{..})@+-- construction instead.+pattern DEntrypointDocItem :: DEntrypoint kind -> SomeDocItem+pattern DEntrypointDocItem dep <- SomeDocItem (castIgnoringPhantom -> Just dep)++-- | Default implementation of 'docItemToMarkdown' for entrypoints. diEntrypointToMarkdown :: HeaderLevel -> DEntrypoint level -> Markdown diEntrypointToMarkdown lvl (DEntrypoint name block) =   mdSeparator <>@@ -117,27 +133,82 @@       where         exampleId = "example-id" --- | Default value for 'DEntrypoint' type argument.-data PlainEntrypointsKind+-- | Describes location of entrypoints of the given kind.+--+-- All such entrypoints will be placed under the same "entrypoints" section,+-- and this instance defines characteristics of this section.+class Typeable ep => EntrypointKindHasDoc (ep :: Kind.Type) where+  -- | Position of the respective entrypoints section in the doc.+  -- This shares the same positions space with all other doc items.+  entrypointKindPos :: Natural -instance Show (DEntrypoint PlainEntrypointsKind) where-  show (DEntrypoint name _) = show name-instance Eq (DEntrypoint PlainEntrypointsKind) where-  (DEntrypoint a1 _) == (DEntrypoint a2 _) = a1 == a2-instance Ord (DEntrypoint PlainEntrypointsKind) where-  (DEntrypoint a1 _) `compare` (DEntrypoint a2 _) = a1 `compare` a2+  -- | Name of the respective entrypoints section.+  entrypointKindSectionName :: Text -instance DocItem (DEntrypoint PlainEntrypointsKind) where-  type DocItemPlacement (DEntrypoint PlainEntrypointsKind) = 'DocItemInlined-  type DocItemReferenced (DEntrypoint PlainEntrypointsKind) = 'True+  -- | Description in the respective entrypoints section.+  entrypointKindSectionDescription :: Maybe Markdown+  entrypointKindSectionDescription = Nothing++instance EntrypointKindHasDoc ep => DocItem (DEntrypoint ep) where+  type DocItemPlacement (DEntrypoint ep) = 'DocItemInlined+  type DocItemReferenced (DEntrypoint ep) = 'True   docItemRef (DEntrypoint name _) = DocItemRefInlined $     DocItemId ("entrypoints-" <> (over _head toLower $ name))-  docItemPos = 1000-  docItemSectionName = Just "Entrypoints"+  docItemPos = entrypointKindPos @ep+  docItemSectionName = Just $ entrypointKindSectionName @ep+  docItemSectionDescription = entrypointKindSectionDescription @ep   docItemToMarkdown = diEntrypointToMarkdown   docItemToToc lvl d@(DEntrypoint name _) =     mdTocFromRef lvl (build . over _head toLower $ name) d +-- | Mark code as part of entrypoint with given name.+--+-- This is automatically called at most of the appropriate situations, like+-- 'entryCase' calls.+entrypointSection+  :: EntrypointKindHasDoc kind+  => Text -> Proxy kind -> (i :-> o) -> (i :-> o)+entrypointSection name (_ :: Proxy kind) =+  docGroup (SomeDocItem . DEntrypoint @kind name)++-- | Default value for 'DEntrypoint' type argument.+data PlainEntrypointsKind++instance EntrypointKindHasDoc PlainEntrypointsKind where+  entrypointKindPos = 1000+  entrypointKindSectionName = "Entrypoints"++-- | Describes the behaviour common for all entrypoints.+--+-- For instance, if your contract runs some checks before calling any+-- entrypoint, you probably want to wrap those checks into+-- @entrypointSection "Prior checks" (Proxy \@CommonContractBehaviourKind)@.+data CommonContractBehaviourKind++instance EntrypointKindHasDoc CommonContractBehaviourKind where+  entrypointKindPos = 1800+  entrypointKindSectionName = "Common for all contract's entrypoints"++-- | Describes the behaviour common for entrypoints of given kind.+--+-- This has very special use cases, like contracts with mix of upgradeable+-- and permanent entrypoints.+data CommonEntrypointsBehaviourKind kind++instance EntrypointKindHasDoc kind =>+         EntrypointKindHasDoc (CommonEntrypointsBehaviourKind kind) where+  entrypointKindPos = entrypointKindPos @kind + 5+  entrypointKindSectionName =+    "Common for " <> entrypointKindSectionName @kind+  entrypointKindSectionDescription = Just $+    let refToBase = docItemSectionRef @(DEntrypoint kind)+                 ?: error "Unexpectedly cannot reference section with entrypoints"+    in "Logic common for all entrypoints in " <> refToBase <> " section."++-- | Inserts a reference to an existing entrypoint.+--+-- This helps to avoid duplication in the generated documentation, in order not+-- to overwhelm the reader. data DEntrypointReference = DEntrypointReference Text Anchor  instance DocItem DEntrypointReference where@@ -445,7 +516,7 @@      )   => Proxy entrypointKind   -> Rec (CaseClauseL inp out) (CaseClauses dt)-  -> dt & inp :-> out+  -> dt : inp :-> out entryCase_ _ = case_ . documentEntrypoints @dt @entrypointKind  -- | Version of 'entryCase_' for tuples.@@ -454,7 +525,7 @@      ( CaseTC dt out inp clauses      , DocumentEntrypoints entrypointKind dt      )-  => Proxy entrypointKind -> IsoRecTuple clauses -> dt & inp :-> out+  => Proxy entrypointKind -> IsoRecTuple clauses -> dt : inp :-> out entryCase p = entryCase_ p . recFromTuple  -- | Wrapper for documenting single entrypoint which parameter@@ -470,7 +541,7 @@      , HasAnnotation param      , KnownValue param      )-  => param & s :-> out -> param & s :-> out+  => param : s :-> out -> param : s :-> out documentEntrypoint instr =   let entrypointName = toText $ symbolVal (Proxy @epName) in     docGroup (SomeDocItem . DEntrypoint @kind entrypointName) $@@ -484,7 +555,7 @@   (#->) :: (Label name, Proxy kind) -> body -> body  instance ( name ~ ("e" `AppendSymbol` epName)-         , body ~ (param & s :-> out)+         , body ~ (param : s :-> out)          , KnownSymbol epName          , DocItem (DEntrypoint kind)          , TypeHasDoc param@@ -502,6 +573,8 @@ -- will not consider entrypoints and thus may be incorrect. -- -- Calling this twice over the same code is also prohibited.+--+-- In simple contracts you may prefer using 'entryCaseSimple'. finalizeParamCallingDoc   :: forall cp inp out.      (NiceParameterFull cp, RequireSumType cp, HasCallStack)@@ -579,7 +652,7 @@      , RequireFlatParamEps cp      )   => Rec (CaseClauseL inp out) (CaseClauses cp)-  -> cp & inp :-> out+  -> cp : inp :-> out entryCaseSimple_ =   finalizeParamCallingDoc . entryCase_ (Proxy @PlainEntrypointsKind)   where@@ -596,7 +669,7 @@      , NiceParameterFull cp      , RequireFlatParamEps cp      )-  => IsoRecTuple clauses -> cp & inp :-> out+  => IsoRecTuple clauses -> cp : inp :-> out entryCaseSimple = entryCaseSimple_ . recFromTuple  type family RequireFlatParamEps cp :: Constraint where

@@ -17,6 +17,7 @@   , ErrorHasDoc (..)   , typeDocMdDescriptionReferToError   , customErrorDocHaskellRepGeneral+  , isInternalErrorClass    , UnspecifiedError (..)   , SomeError (..)@@ -475,6 +476,10 @@     ErrClassContractInternal -> "Internal"     ErrClassUnknown -> "-" +-- | Whether given error class is about internal errors.+--+-- Internal errors are not enlisted on per-entrypoint basis, only once for+-- the entire contract. isInternalErrorClass :: ErrorClass -> Bool isInternalErrorClass = \case   ErrClassActionException -> False

@@ -2,6 +2,9 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}++-- | Lorentz wrappers over instructions from Morley extension. module Lorentz.Ext   ( stackRef   , printComment@@ -17,27 +20,48 @@ import Michelson.Typed.Instr import Util.Peano hiding (Nat) +-- | Include a value at given position on stack into comment produced+-- by 'printComment'.+--+-- >>> stackRef @0+-- <includes the top of the stack> stackRef   :: forall (gn :: Nat) st n.       (n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n)   => PrintComment st stackRef = PrintComment . one . Right $ mkStackRef @gn +-- | Print a comment. It will be visible in tests.+--+-- >>> printComment "Hello world!"+-- >>> printComment $ "On top of the stack I see " <> stackRef @0 printComment :: PrintComment (ToTs s) -> s :-> s printComment = I . Ext . PRINT +-- | Test an invariant, fail if it does not hold.+--+-- This won't be included into production contract and is executed only in tests. testAssert   :: (Typeable (ToTs out), HasCallStack)-  => Text -> PrintComment (ToTs inp) -> inp :-> Bool & out -> inp :-> inp+  => Text -> PrintComment (ToTs inp) -> inp :-> Bool : out -> inp :-> inp testAssert msg comment = \case   I instr -> I . Ext . TEST_ASSERT $ TestAssert msg comment instr   FI _ -> error "test assert branch always fails" +-- | Fix the current type of the stack to be given one.+--+-- >>> stackType @'[Natural]+-- >>> stackType @(Integer : Natural : s)+-- >>> stackType @'["balance" :! Integer, "toSpend" :! Integer, BigMap Address Integer]+--+-- Note that you can omit arbitrary parts of the type.+--+-- >>> stackType @'["balance" :! Integer, "toSpend" :! _, BigMap _ _] stackType :: forall s. s :-> s stackType = I Nop -_sample1 :: s ~ (a & s') => s :-> s+_sample1 :: s ~ (a : s') => s :-> s _sample1 = printComment $ "Head is " <> stackRef @0 -_sample2 :: Integer & Natural & s :-> Integer & Natural & s-_sample2 = stackType @(Integer & _)+_sample2 :: Integer : Natural : s :-> Integer : Natural : s+_sample2 = stackType @(Integer : _)

@@ -104,10 +104,10 @@  instance (NicePackedValue param) =>          WrapExt ('OneField param) where-  packForWrap = pack+  packForWrap = packRaw  instance WrapExt 'NoFields where-  packForWrap = unit # pack+  packForWrap = unit # packRaw  -- | Wraps an argument on top of the stack into an Extensible representation wrapExt@@ -186,7 +186,7 @@          => GExtVal t (G.C1 ('G.MetaCons name _1 _2) G.U1) where   gToExtVal (G.M1 G.U1) = Extensible     ( natVal (Proxy @n)-    , lPackValue ()+    , lPackValueRaw ()     )   gFromExtVal (Extensible (idx, _))     | idx == natVal (Proxy @n)@@ -200,12 +200,12 @@          => GExtVal t (G.C1 ('G.MetaCons name _1 _2) (G.S1 _3 (G.Rec0 param))) where   gToExtVal (G.M1 (G.M1 (G.K1 param))) = Extensible     ( natVal (Proxy @n)-    , lPackValue param+    , lPackValueRaw param     )   gFromExtVal (Extensible (idx, bs))     | idx == natVal (Proxy @n)         = first (\_ -> ArgumentUnpackFailed) $-          fmap (G.M1 . G.M1 . G.K1) $ lUnpackValue @param bs+          fmap (G.M1 . G.M1 . G.K1) $ lUnpackValueRaw @param bs     | otherwise = Left $ ConstructorIndexNotFound idx  instance (GExtVal t x, GExtVal t y) => GExtVal t (x :+: y) where

@@ -2,6 +2,8 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}+ module Lorentz.Instr   ( nop   , justComment@@ -50,6 +52,7 @@   , exec   , execute   , apply+  , applicate   , dip   , ConstraintDIPNLorentz   , dipNPeano@@ -58,6 +61,8 @@   , cast   , pack   , unpack+  , packRaw+  , unpackRaw   , concat   , concat'   , slice, isNat, add, sub, rsub, mul, ediv, abs@@ -116,6 +121,7 @@ import Lorentz.Address import Lorentz.Arith import Lorentz.Base+import Lorentz.Bytes import Lorentz.Constraints import Lorentz.Entrypoints import Lorentz.Polymorphic@@ -125,7 +131,7 @@ import Michelson.Typed   (pattern CAR, pattern CDR, CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN,   ConstraintDIPN', ConstraintDUG, ConstraintDUG', EntrypointCallT(..), ExtInstr(..), Instr(..),-  RemFail(..), pattern PAIR, SomeEntrypointCallT(..), Value'(..), sepcName, starNotes)+  pattern PAIR, RemFail(..), SomeEntrypointCallT(..), Value'(..), sepcName, starNotes) import Michelson.Typed.Arith import Michelson.Typed.Haskell.Value import Util.Peano@@ -154,7 +160,7 @@   comment (StatementEnds stmtName)  -drop :: a & s :-> s+drop :: a : s :-> s drop = I DROP  -- | Drop top @n@ elements from the stack.@@ -172,10 +178,10 @@     _example :: '[ Integer, Integer, Integer ] :-> '[]     _example = dropN @3 -dup  :: a & s :-> a & a & s+dup  :: a : s :-> a : a : s dup = I DUP -swap :: a & b & s :-> b & a & s+swap :: a : b : s :-> b : a : s swap = I SWAP  -- See a comment about `ConstraintDIPNLorentz'.@@ -229,104 +235,104 @@       '[ Integer, Integer, Integer, Bool ]     _example = dug @3 -push :: forall t s . NiceConstant t => t -> (s :-> t & s)+push :: forall t s . NiceConstant t => t -> (s :-> t : s) push a = I $ PUSH (toVal a) \\ niceConstantEvi @t -some :: a & s :-> Maybe a & s+some :: a : s :-> Maybe a : s some = I SOME -none :: forall a s . KnownValue a => s :-> (Maybe a & s)+none :: forall a s . KnownValue a => s :-> (Maybe a : s) none = I NONE -unit :: s :-> () & s+unit :: s :-> () : s unit = I UNIT  ifNone-  :: (s :-> s') -> (a & s :-> s') -> (Maybe a & s :-> s')+  :: (s :-> s') -> (a : s :-> s') -> (Maybe a : s :-> s') ifNone = iGenericIf IF_NONE -pair :: a & b & s :-> (a, b) & s+pair :: a : b : s :-> (a, b) : s pair = I PAIR -car :: (a, b) & s :-> a & s+car :: (a, b) : s :-> a : s car = I CAR -cdr :: (a, b) & s :-> b & s+cdr :: (a, b) : s :-> b : s cdr = I CDR -left :: forall a b s. KnownValue b => a & s :-> Either a b & s+left :: forall a b s. KnownValue b => a : s :-> Either a b : s left = I LEFT -right :: forall a b s. KnownValue a => b & s :-> Either a b & s+right :: forall a b s. KnownValue a => b : s :-> Either a b : s right = I RIGHT  ifLeft-  :: (a & s :-> s') -> (b & s :-> s') -> (Either a b & s :-> s')+  :: (a : s :-> s') -> (b : s :-> s') -> (Either a b : s :-> s') ifLeft = iGenericIf IF_LEFT -nil :: KnownValue p => s :-> List p & s+nil :: KnownValue p => s :-> List p : s nil = I NIL -cons :: a & List a & s :-> List a & s+cons :: a : List a : s :-> List a : s cons = I CONS  ifCons-  :: (a & List a & s :-> s') -> (s :-> s') -> (List a & s :-> s')+  :: (a : List a : s :-> s') -> (s :-> s') -> (List a : s :-> s') ifCons = iGenericIf IF_CONS -size :: SizeOpHs c => c & s :-> Natural & s+size :: SizeOpHs c => c : s :-> Natural : s size = I SIZE -emptySet :: (NiceComparable e) => s :-> Set e & s+emptySet :: (NiceComparable e) => s :-> Set e : s emptySet = I EMPTY_SET  emptyMap :: (NiceComparable k, KnownValue v)-         => s :-> Map k v & s+         => s :-> Map k v : s emptyMap = I EMPTY_MAP  emptyBigMap :: (NiceComparable k, KnownValue v)-            => s :-> BigMap k v & s+            => s :-> BigMap k v : s emptyBigMap = I EMPTY_BIG_MAP  map   :: (MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack)-  => (MapOpInpHs c & s :-> b & s) -> (c & s :-> MapOpResHs c b & s)+  => (MapOpInpHs c : s :-> b : s) -> (c : s :-> MapOpResHs c b : s) map (iNonFailingCode -> action) = I (MAP action)  iter   :: (IterOpHs c, HasCallStack)-  => (IterOpElHs c & s :-> s) -> (c & s :-> s)+  => (IterOpElHs c : s :-> s) -> (c : s :-> s) iter (iNonFailingCode -> action) = I (ITER action) -mem :: MemOpHs c => MemOpKeyHs c & c & s :-> Bool & s+mem :: MemOpHs c => MemOpKeyHs c : c : s :-> Bool : s mem = I MEM  get   :: (GetOpHs c, KnownValue (GetOpValHs c))-  => GetOpKeyHs c & c & s :-> Maybe (GetOpValHs c) & s+  => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s get = I GET -update :: UpdOpHs c => UpdOpKeyHs c & UpdOpParamsHs c & c & s :-> c & s+update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s update = I UPDATE -if_ :: (s :-> s') -> (s :-> s') -> (Bool & s :-> s')+if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s') if_ = iGenericIf IF -loop :: (s :-> Bool & s) -> (Bool & s :-> s)+loop :: (s :-> Bool : s) -> (Bool : s :-> s) loop (iAnyCode -> b) = I (LOOP b)  loopLeft-  :: (a & s :-> Either a b & s) -> (Either a b & s :-> b & s)+  :: (a : s :-> Either a b : s) -> (Either a b : s :-> b : s) loopLeft (iAnyCode -> b) = I (LOOP_LEFT b)  lambda   :: ZipInstrs [i, o]-  => (i :-> o) -> (s :-> (i :-> o) & s)+  => (i :-> o) -> (s :-> (i :-> o) : s) lambda instr = case zippingStack instr of   I l -> I (LAMBDA . VLam $ RfNormal l)   FI l -> I (LAMBDA . VLam $ RfAlwaysFails l) -exec :: a & Lambda a b & s :-> b & s+exec :: a : Lambda a b : s :-> b : s exec = I EXEC  -- | Similar to 'exec' but works for lambdas with arbitrary size of input@@ -348,10 +354,18 @@  apply   :: forall a b c s. (NiceConstant a, KnownValue b)-  => a & Lambda (a, b) c & s :-> Lambda b c & s+  => a : Lambda (a, b) c : s :-> Lambda b c : s apply = I $ APPLY \\ niceConstantEvi @a -dip :: forall a s s'. HasCallStack => (s :-> s') -> (a & s :-> a & s')+-- | Version of 'apply' that works for lambdas with arbitrary length+-- input and output.+applicate+  :: forall a b c inp2nd inpTail s.+     (NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail))+  => a : (a : b :-> c) : s :-> (b :-> c) : s+applicate = I APPLY \\ niceConstantEvi @a++dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s') dip (iNonFailingCode -> a) = I (DIP a)  -- Helper constraint we need for 'dipN'.@@ -386,118 +400,128 @@     _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]     _example = dipN @3 unit -failWith :: KnownValue a => a & s :-> t+failWith :: KnownValue a => a : s :-> t failWith = FI FAILWITH -cast :: KnownValue a => (a & s :-> a & s)+cast :: KnownValue a => (a : s :-> a : s) cast = I CAST  pack   :: forall a s. (NicePackedValue a)-  => a & s :-> ByteString & s+  => a : s :-> Packed a : s pack = I $ PACK \\ nicePackedValueEvi @a  unpack   :: forall a s. (NiceUnpackedValue a)-  => ByteString & s :-> Maybe a & s+  => Packed a : s :-> Maybe a : s unpack = I $ UNPACK \\ niceUnpackedValueEvi @a -concat :: ConcatOpHs c => c & c & s :-> c & s+packRaw+  :: forall a s. (NicePackedValue a)+  => a : s :-> ByteString : s+packRaw = I $ PACK \\ nicePackedValueEvi @a++unpackRaw+  :: forall a s. (NiceUnpackedValue a)+  => ByteString : s :-> Maybe a : s+unpackRaw = I $ UNPACK \\ niceUnpackedValueEvi @a++concat :: ConcatOpHs c => c : c : s :-> c : s concat = I CONCAT -concat' :: ConcatOpHs c => List c & s :-> c & s+concat' :: ConcatOpHs c => List c : s :-> c : s concat' = I CONCAT'  slice   :: (SliceOpHs c, KnownValue c)-  => Natural & Natural & c & s :-> Maybe c & s+  => Natural : Natural : c : s :-> Maybe c : s slice = I SLICE -isNat :: Integer & s :-> Maybe Natural & s+isNat :: Integer : s :-> Maybe Natural : s isNat = I ISNAT  add   :: ArithOpHs Add n m-  => n & m & s :-> ArithResHs Add n m & s+  => n : m : s :-> ArithResHs Add n m : s add = I ADD  sub   :: ArithOpHs Sub n m-  => n & m & s :-> ArithResHs Sub n m & s+  => n : m : s :-> ArithResHs Sub n m : s sub = I SUB  rsub   :: ArithOpHs Sub n m-  => m & n & s :-> ArithResHs Sub n m & s+  => m : n : s :-> ArithResHs Sub n m : s rsub = swap # sub  mul   :: ArithOpHs Mul n m-  => n & m & s :-> ArithResHs Mul n m & s+  => n : m : s :-> ArithResHs Mul n m : s mul = I MUL  ediv :: EDivOpHs n m-     => n & m & s-     :-> Maybe ((EDivOpResHs n m, EModOpResHs n m)) & s+     => n : m : s+     :-> Maybe ((EDivOpResHs n m, EModOpResHs n m)) : s ediv = I EDIV -abs :: UnaryArithOpHs Abs n => n & s :-> UnaryArithResHs Abs n & s+abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s abs = I ABS -neg :: UnaryArithOpHs Neg n => n & s :-> UnaryArithResHs Neg n & s+neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s neg = I NEG   lsl   :: ArithOpHs Lsl n m-  => n & m & s :-> ArithResHs Lsl n m & s+  => n : m : s :-> ArithResHs Lsl n m : s lsl = I LSL  lsr   :: ArithOpHs Lsr n m-  => n & m & s :-> ArithResHs Lsr n m & s+  => n : m : s :-> ArithResHs Lsr n m : s lsr = I LSR  or   :: ArithOpHs Or n m-  => n & m & s :-> ArithResHs Or n m & s+  => n : m : s :-> ArithResHs Or n m : s or = I OR  and   :: ArithOpHs And n m-  => n & m & s :-> ArithResHs And n m & s+  => n : m : s :-> ArithResHs And n m : s and = I AND  xor   :: (ArithOpHs Xor n m)-  => n & m & s :-> ArithResHs Xor n m & s+  => n : m : s :-> ArithResHs Xor n m : s xor = I XOR -not :: UnaryArithOpHs Not n => n & s :-> UnaryArithResHs Not n & s+not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s not = I NOT -compare :: NiceComparable n => n & n & s :-> Integer & s+compare :: NiceComparable n => n : n : s :-> Integer : s compare = I COMPARE -eq0 :: UnaryArithOpHs Eq' n => n & s :-> UnaryArithResHs Eq' n & s+eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s eq0 = I EQ -neq0 :: UnaryArithOpHs Neq n => n & s :-> UnaryArithResHs Neq n & s+neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s neq0 = I NEQ -lt0 :: UnaryArithOpHs Lt n => n & s :-> UnaryArithResHs Lt n & s+lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s lt0 = I LT -gt0 :: UnaryArithOpHs Gt n => n & s :-> UnaryArithResHs Gt n & s+gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s gt0 = I GT -le0 :: UnaryArithOpHs Le n => n & s :-> UnaryArithResHs Le n & s+le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s le0 = I LE -ge0 :: UnaryArithOpHs Ge n => n & s :-> UnaryArithResHs Ge n & s+ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s ge0 = I GE -int :: Natural & s :-> Integer & s+int :: Natural : s :-> Integer : s int = I INT  -- | Get a reference to the current contract.@@ -515,7 +539,7 @@ self   :: forall p s.       (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p)-  => s :-> ContractRef p & s+  => s :-> ContractRef p : s self = I (SELF $ sepcCallRootChecked @p) \\ niceParameterEvi @p  -- | Make a reference to the current contract, maybe a specific entrypoint.@@ -527,7 +551,7 @@   :: forall p mname s.      (NiceParameterFull p)   => EntrypointRef mname-  -> s :-> ContractRef (GetEntrypointArgCustom p mname) & s+  -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s selfCalling epRef = I $   withDict (niceParameterEvi @p) $   case parameterEntrypointCallCustom @p epRef of@@ -545,7 +569,7 @@       ( NiceParameterFull p, ForbidExplicitDefaultEntrypoint p       , ToTAddress_ p addr       )-  => addr & s :-> Maybe (ContractRef p) & s+  => addr : s :-> Maybe (ContractRef p) : s contract = I (CONTRACT starNotes epName) \\ niceParameterEvi @p   where     epName = sepcName (sepcCallRootChecked @p)@@ -559,7 +583,7 @@   :: forall cp epRef epArg addr s.      (HasEntrypointArg cp epRef epArg, ToTAddress_ cp addr)   => epRef-  -> addr & s :-> Maybe (ContractRef epArg) & s+  -> addr : s :-> Maybe (ContractRef epArg) : s contractCalling epRef = I $   case useHasEntrypointArg @cp @epRef @epArg epRef of     (Dict, epName) -> CONTRACT starNotes epName@@ -573,7 +597,7 @@   :: forall arg s.      (NiceParameter arg)   => EpName-  -> Address & s :-> Maybe (ContractRef arg) & s+  -> Address : s :-> Maybe (ContractRef arg) : s contractCallingUnsafe epName = contractCalling (TrustEpName epName)  -- | Version of 'contract' instruction which may accept address with already@@ -583,7 +607,7 @@ -- conflict. runFutureContract   :: forall p s. (NiceParameter p)-  => FutureContract p & s :-> Maybe (ContractRef p) & s+  => FutureContract p : s :-> Maybe (ContractRef p) : s runFutureContract =   I Nop # epAddressToContract @@ -592,68 +616,68 @@ -- Validity of such operation cannot be ensured at compile time. epAddressToContract   :: forall p s. (NiceParameter p)-  => EpAddress & s :-> Maybe (ContractRef p) & s+  => EpAddress : s :-> Maybe (ContractRef p) : s epAddressToContract =   I (CONTRACT starNotes DefEpName) \\ niceParameterEvi @p  transferTokens   :: forall p s. (NiceParameter p)-  => p & Mutez & ContractRef p & s :-> Operation & s+  => p : Mutez : ContractRef p : s :-> Operation : s transferTokens = I $ TRANSFER_TOKENS \\ niceParameterEvi @p -setDelegate :: Maybe KeyHash & s :-> Operation & s+setDelegate :: Maybe KeyHash : s :-> Operation : s setDelegate = I SET_DELEGATE  createContract   :: forall p g s. (NiceStorage g, NiceParameterFull p)   => Contract p g-  -> Maybe KeyHash & Mutez & g & s-  :-> Operation & Address & s+  -> Maybe KeyHash : Mutez : g : s+  :-> Operation : Address : s createContract cntrc =   I $ CREATE_CONTRACT (compileLorentzContract cntrc)     \\ niceParameterEvi @p     \\ niceStorageEvi @g -implicitAccount :: KeyHash & s :-> ContractRef () & s+implicitAccount :: KeyHash : s :-> ContractRef () : s implicitAccount = I IMPLICIT_ACCOUNT -now :: s :-> Timestamp & s+now :: s :-> Timestamp : s now = I NOW -amount :: s :-> Mutez & s+amount :: s :-> Mutez : s amount = I AMOUNT -balance :: s :-> Mutez & s+balance :: s :-> Mutez : s balance = I BALANCE -checkSignature :: PublicKey & Signature & ByteString & s :-> Bool & s+checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s checkSignature = I CHECK_SIGNATURE -sha256 :: ByteString & s :-> ByteString & s+sha256 :: BytesLike bs => bs : s :-> Hash Sha256 bs : s sha256 = I SHA256 -sha512 :: ByteString & s :-> ByteString & s+sha512 :: BytesLike bs => bs : s :-> Hash Sha512 bs : s sha512 = I SHA512 -blake2B :: ByteString & s :-> ByteString & s+blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s blake2B = I BLAKE2B -hashKey :: PublicKey & s :-> KeyHash & s+hashKey :: PublicKey : s :-> KeyHash : s hashKey = I HASH_KEY  {-# WARNING source     "Using `source` is considered a bad practice.\n\ \    Consider using `sender` instead until further investigation" #-}-source :: s :-> Address & s+source :: s :-> Address : s source = I SOURCE -sender :: s :-> Address & s+sender :: s :-> Address : s sender = I SENDER -address :: ContractRef a & s :-> Address & s+address :: ContractRef a : s :-> Address : s address = I ADDRESS -chainId :: s :-> ChainId & s+chainId :: s :-> ChainId : s chainId = I CHAIN_ID  -- | Execute given instruction on truncated stack.@@ -683,7 +707,7 @@   :: forall c k s v st e.      ( MemOpHs c, k ~ MemOpKeyHs c      , KnownValue e-     , st ~ (k & v & c & s)+     , st ~ (k : v : c : s)      )   => (forall s0. k : s0 :-> e : s0)   -> st :-> st@@ -698,7 +722,7 @@      , KnownValue e      )   => (forall s0. k : s0 :-> e : s0)-  -> k & UpdOpParamsHs c & c & s :-> c & s+  -> k : UpdOpParamsHs c : c : s :-> c : s updateNew mkErr = failingWhenPresent mkErr # update  class LorentzFunctor (c :: Kind.Type -> Kind.Type) where

@@ -0,0 +1,67 @@+-- SPDX-FileCopyrightText: 2020 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- | Isomorphisms in Lorentz.+module Lorentz.Iso+  ( LIso (..)+  , invertIso+  , involutedIso+  , checkedCoerceIso+  , forcedCoerceIso+  , namedIso+  , nonIso+  , nonDefIso+  ) where++import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints+import Lorentz.Default+import Lorentz.Instr+import Lorentz.Macro+import Util.Label+import Util.Named++-- | Lorentz version of 'Control.Lens.Iso'.+data LIso a b = LIso+  { liTo :: forall s. a : s :-> b : s+  , liFrom :: forall s. b : s :-> a : s+  }++-- | Invert an isomorphism.+invertIso :: LIso a b -> LIso b a+invertIso LIso{..} = LIso{ liTo = liFrom, liFrom = liTo }++-- | Given a function that is its own inverse, make an 'LIso' using it+-- in both directions.+involutedIso :: Lambda a a -> LIso a a+involutedIso l = LIso (framed l) (framed l)++-- | The isomorphism between two values with identical representation+-- and semantics.+checkedCoerceIso :: Coercible_ a b => LIso a b+checkedCoerceIso = LIso checkedCoerce_ checkedCoerce_++-- | The isomorphism between two values with identical representation.+--+-- The same precautions as for 'forcedCoerce' apply here.+forcedCoerceIso :: MichelsonCoercible a b => LIso a b+forcedCoerceIso = LIso forcedCoerce_ forcedCoerce_++-- | The isomorphism between raw and named value.+namedIso :: Label n -> LIso a (n :! a)+namedIso l = LIso (toNamed l) (fromNamed l)++-- | Absence of value on the left hand side is associated with+-- the given value on the right hand side.+nonIso :: (NiceConstant a, NiceComparable a) => a -> LIso (Maybe a) a+nonIso defVal = LIso (fromOption defVal) (non defVal)++-- | Absence of value on the left hand side is associated with+-- the default value on the right hand side.+--+-- This is more general version of @nonIso ldef@ since it can+-- work with e.g. containers.+nonDefIso :: (LDefault a, NiceConstant a) => LIso (Maybe a) a+nonDefIso = LIso (fromOption ldef) (non' lIsDef)

@@ -2,8 +2,8 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ -{-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}  -- | Common Michelson macros defined using Lorentz syntax. module Lorentz.Macro@@ -108,6 +108,11 @@   , unwrapVoid   , voidResultTag   , dupTop2+  , fromOption+  , isSome+  , non+  , non'+  , isEmpty    -- * Buildable utils for additional Morley macros   , buildView@@ -116,9 +121,10 @@   -- * Macros for working with @address@ and @contract@-like types   , addressToEpAddress   , pushContractRef+  , selfAddress   ) where -import Prelude hiding (compare, drop, some, swap)+import Prelude hiding (and, compare, drop, some, swap)  import qualified Data.Kind as Kind import Data.Singletons (SingI(..))@@ -137,6 +143,7 @@ import Lorentz.Errors import Lorentz.Ext (stackType) import Lorentz.Instr+import Lorentz.Polymorphic import Lorentz.Value import Michelson.Typed (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T) import Michelson.Typed.Arith@@ -150,27 +157,27 @@ ----------------------------------------------------------------------------  eq :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s eq = compare # eq0  neq :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s neq = compare # neq0  gt :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s gt = compare # gt0  le :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s le = compare # le0  ge :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s ge = compare # ge0  lt :: NiceComparable n-   => n & n & s :-> Bool & s+   => n : n : s :-> Bool : s lt = compare # lt0  type IfCmp0Constraints a op =@@ -178,62 +185,62 @@  ifEq0   :: (IfCmp0Constraints a Eq')-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifEq0 l r = eq0 # if_ l r  ifNeq0   :: (IfCmp0Constraints a Neq)-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifNeq0 l r = neq0 # if_ l r  ifLt0   :: (IfCmp0Constraints a Lt)-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifLt0 l r = lt0 # if_ l r  ifGt0   :: (IfCmp0Constraints a Gt)-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifGt0 l r = gt0 # if_ l r  ifLe0   :: (IfCmp0Constraints a Le)-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifLe0 l r = le0 # if_ l r  ifGe0   :: (IfCmp0Constraints a Ge)-  => (s :-> s') -> (s :-> s') -> (a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : s :-> s') ifGe0 l r = ge0 # if_ l r  ifEq   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifEq l r = eq # if_ l r  ifNeq   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifNeq l r = neq # if_ l r  ifLt   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifLt l r = lt # if_ l r  ifGt   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifGt l r = gt # if_ l r  ifLe   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifLe l r = le # if_ l r  ifGe   :: NiceComparable a-  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')+  => (s :-> s') -> (s :-> s') -> (a : a : s :-> s') ifGe l r = ge # if_ l r  ----------------------------------------------------------------------------@@ -250,60 +257,60 @@ -- Assertions ---------------------------------------------------------------------------- -assert :: IsError err => err -> Bool & s :-> s+assert :: IsError err => err -> Bool : s :-> s assert reason = if_ nop (failUsing reason) -assertEq0 :: (IfCmp0Constraints a Eq', IsError err) => err -> a & s :-> s+assertEq0 :: (IfCmp0Constraints a Eq', IsError err) => err -> a : s :-> s assertEq0 reason = ifEq0 nop (failUsing reason) -assertNeq0 :: (IfCmp0Constraints a Neq, IsError err) => err -> a & s :-> s+assertNeq0 :: (IfCmp0Constraints a Neq, IsError err) => err -> a : s :-> s assertNeq0 reason = ifNeq0 nop (failUsing reason) -assertLt0 :: (IfCmp0Constraints a Lt, IsError err) => err -> a & s :-> s+assertLt0 :: (IfCmp0Constraints a Lt, IsError err) => err -> a : s :-> s assertLt0 reason = ifLt0 nop (failUsing reason) -assertGt0 :: (IfCmp0Constraints a Gt, IsError err) => err -> a & s :-> s+assertGt0 :: (IfCmp0Constraints a Gt, IsError err) => err -> a : s :-> s assertGt0 reason = ifGt0 nop (failUsing reason) -assertLe0 :: (IfCmp0Constraints a Le, IsError err) => err -> a & s :-> s+assertLe0 :: (IfCmp0Constraints a Le, IsError err) => err -> a : s :-> s assertLe0 reason = ifLe0 nop (failUsing reason) -assertGe0 :: (IfCmp0Constraints a Ge, IsError err) => err -> a & s :-> s+assertGe0 :: (IfCmp0Constraints a Ge, IsError err) => err -> a : s :-> s assertGe0 reason = ifGe0 nop (failUsing reason) -assertEq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertEq :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertEq reason = ifEq nop (failUsing reason) -assertNeq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertNeq :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertNeq reason = ifNeq nop (failUsing reason) -assertLt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertLt :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertLt reason = ifLt nop (failUsing reason) -assertGt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertGt :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertGt reason = ifGt nop (failUsing reason) -assertLe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertLe :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertLe reason = ifLe nop (failUsing reason) -assertGe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s+assertGe :: (NiceComparable a, IsError err) => err -> a : a : s :-> s assertGe reason = ifGe nop (failUsing reason) -assertNone :: IsError err => err -> Maybe a & s :-> s+assertNone :: IsError err => err -> Maybe a : s :-> s assertNone reason = ifNone nop (failUsing reason) -assertSome :: IsError err => err -> Maybe a & s :-> a & s+assertSome :: IsError err => err -> Maybe a : s :-> a : s assertSome reason = ifNone (failUsing reason) nop -assertLeft :: IsError err => err -> Either a b & s :-> a & s+assertLeft :: IsError err => err -> Either a b : s :-> a : s assertLeft reason = ifLeft nop (failUsing reason) -assertRight :: IsError err => err -> Either a b & s :-> b & s+assertRight :: IsError err => err -> Either a b : s :-> b : s assertRight reason = ifLeft (failUsing reason) nop  assertUsing   :: IsError a-  => a -> Bool & s :-> s+  => a -> Bool : s :-> s assertUsing err = if_ nop $ failUsing err  ----------------------------------------------------------------------------@@ -322,9 +329,9 @@  class CloneX (n :: Peano) a s where   type CloneXT n a s :: [Kind.Type]-  cloneXImpl :: a & s :-> CloneXT n a s+  cloneXImpl :: a : s :-> CloneXT n a s instance CloneX 'Z a s where-  type CloneXT 'Z a s = a & s+  type CloneXT 'Z a s = a : s   cloneXImpl = nop instance (CloneX n a s) => CloneX ('S n) a s where   type CloneXT ('S n) a s = a ': CloneXT n a s@@ -332,10 +339,10 @@  -- | Duplicate the top of the stack @n@ times. ----- For example, `cloneX @3` has type `a & s :-> a & a & a & a & s`.+-- For example, `cloneX @3` has type `a : s :-> a : a : a : a : s`. cloneX   :: forall (n :: GHC.Nat) a s. CloneX (ToPeano n) a s-  => a & s :-> CloneXT (ToPeano n) a s+  => a : s :-> CloneXT (ToPeano n) a s cloneX = cloneXImpl @(ToPeano n)  -- | Kind-agnostic constraint for duupX@@ -414,48 +421,48 @@     -> Integer : Natural : () : s :-> ByteString : () : s   _example = framedN @2 -papair :: a & b & c & s :-> ((a, b), c) & s+papair :: a : b : c : s :-> ((a, b), c) : s papair = pair # pair -ppaiir :: a & b & c & s :-> (a, (b, c)) & s+ppaiir :: a : b : c : s :-> (a, (b, c)) : s ppaiir = dip pair # pair -unpair :: (a, b) & s :-> a & b & s+unpair :: (a, b) : s :-> a : b : s unpair = dup # car # dip cdr -cdar :: (a1, (a2, b)) & s :-> a2 & s+cdar :: (a1, (a2, b)) : s :-> a2 : s cdar = cdr # car -cddr :: (a1, (a2, b)) & s :-> b & s+cddr :: (a1, (a2, b)) : s :-> b : s cddr = cdr # cdr -caar :: ((a, b1), b2) & s :-> a & s+caar :: ((a, b1), b2) : s :-> a : s caar = car # car -cadr :: ((a, b1), b2) & s :-> b1 & s+cadr :: ((a, b1), b2) : s :-> b1 : s cadr = car # cdr -setCar :: (a, b1) & (b2 & s) :-> (b2, b1) & s+setCar :: (a, b1) : (b2 : s) :-> (b2, b1) : s setCar = cdr # swap # pair -setCdr :: (a, b1) & (b2 & s) :-> (a, b2) & s+setCdr :: (a, b1) : (b2 : s) :-> (a, b2) : s setCdr = car # pair  mapCar-  :: a & s :-> a1 & s-  -> (a, b) & s :-> (a1, b) & s+  :: a : s :-> a1 : s+  -> (a, b) : s :-> (a1, b) : s mapCar op = dup # cdr # dip (car # op) # swap # pair  mapCdr-  :: b & (a, b) & s :-> b1 & (a, b) & s-  -> (a, b) & s :-> (a, b1) & s+  :: b : (a, b) : s :-> b1 : (a, b) : s+  -> (a, b) : s :-> (a, b1) : s mapCdr op = dup # cdr # op # swap # car # pair -ifRight :: (b & s :-> s') -> (a & s :-> s') -> (Either a b & s :-> s')+ifRight :: (b : s :-> s') -> (a : s :-> s') -> (Either a b : s :-> s') ifRight l r = ifLeft r l  ifSome-  :: (a & s :-> s') -> (s :-> s') -> (Maybe a & s :-> s')+  :: (a : s :-> s') -> (s :-> s') -> (Maybe a : s :-> s') ifSome s n = ifNone n s  when_ :: (s :-> s) -> (Bool : s :-> s)@@ -505,7 +512,7 @@ -- -- This is a separate function from 'updateMap' because stacks they operate with -- differ in length.-setInsert :: NiceComparable e => e & Set e & s :-> Set e & s+setInsert :: NiceComparable e => e : Set e : s :-> Set e : s setInsert = dip (push True) # update  -- | Insert given element into set, ensuring that it does not overwrite@@ -515,11 +522,11 @@ setInsertNew   :: (NiceComparable e, KnownValue err)   => (forall s0. e : s0 :-> err : s0)-  -> e & Set e & s :-> Set e & s+  -> e : Set e : s :-> Set e : s setInsertNew desc = dip (push True) # failingWhenPresent desc # update  -- | Delete given element from the set.-setDelete :: NiceComparable e => e & Set e & s :-> Set e & s+setDelete :: NiceComparable e => e : Set e : s :-> Set e : s setDelete = dip (push False) # update  -- | Kind-agnostic constraint for replaceN@@ -688,8 +695,8 @@  view_ ::      (NiceParameter r)-  => (forall s0. a & storage & s0 :-> r : s0)-  -> View a r & storage & s :-> (List Operation, storage) & s+  => (forall s0. a : storage : s0 :-> r : s0)+  -> View a r : storage : s :-> (List Operation, storage) : s view_ code =   unwrapView #   unpair # dip (duupX @2) # code # dip amount #@@ -798,7 +805,7 @@ void_   :: forall a b s s' anything.       (IsError (VoidResult b), KnownValue b)-  => a & s :-> b & s' -> Void_ a b & s :-> anything+  => a : s :-> b : s' -> Void_ a b : s :-> anything void_ code =   doc (DThrows (Proxy @(VoidResult b))) #   forcedCoerce_ @_ @(_, Lambda b b) #@@ -837,8 +844,48 @@     push (FutureContract contractRef) # dup #     runFutureContract # ifNone onContractNotFound (dip drop) +-- | Get address of the current contract.+--+-- TODO [#373]: reimplement this using SELF_ADDRESS+selfAddress :: s :-> Address : s+selfAddress = self @() # address+ -- | Duplicate two topmost items on top of the stack. dupTop2 ::   forall (a :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).   a ': b ': s :-> a ': b ': a ': b ': s dupTop2 = duupX @2 # duupX @2++fromOption+  :: (NiceConstant a)+  => a -> Maybe a : s :-> a : s+fromOption a = ifSome nop (push a)++isSome :: Maybe a : s :-> Bool : s+isSome = ifSome (drop # push True) (push False)++-- | Retain the value if it is not equal to the given one.+--+-- >>> non 0 -$ 5+-- Just 5+-- >>> non 0 -$ 0+-- Nothing+non+  :: (NiceConstant a, NiceComparable a)+  => a -> a : s :-> Maybe a : s+non a = non' (push a # eq)++-- | Version of 'non' with a custom predicate.+--+-- >>> non' eq0 -$ 5+-- Just 5+-- >>> non' eq0 -$ 0+-- Nothing+non'+  :: (NiceConstant a)+  => Lambda a Bool -> a : s :-> Maybe a : s+non' p = dup # framed p # if_ (drop # none) some++-- | Check whether container is empty.+isEmpty :: SizeOpHs c => c : s :-> Bool : s+isEmpty = size # int # eq0

@@ -4,7 +4,9 @@  -- | Packing utilities. module Lorentz.Pack-  ( lPackValue+  ( lPackValueRaw+  , lUnpackValueRaw+  , lPackValue   , lUnpackValue   , lEncodeValue   , valueToScriptExpr@@ -14,6 +16,7 @@ import qualified Data.ByteString as BS import Data.Constraint ((\\)) +import Lorentz.Bytes import Lorentz.Constraints import Michelson.Interpret.Pack import Michelson.Interpret.Unpack@@ -21,20 +24,34 @@ import Morley.Micheline (Expression, encodeExpression) import Tezos.Crypto (blake2b) -lPackValue+lPackValueRaw   :: forall a.      (NicePackedValue a)   => a -> ByteString-lPackValue =+lPackValueRaw =   packValue' . toVal \\ nicePackedValueEvi @a -lUnpackValue+lUnpackValueRaw   :: forall a.      (NiceUnpackedValue a)   => ByteString -> Either UnpackError a-lUnpackValue =+lUnpackValueRaw =   fmap fromVal . unpackValue' \\ niceUnpackedValueEvi @a +lPackValue+  :: forall a.+     (NicePackedValue a)+  => a -> Packed a+lPackValue =+  Packed . lPackValueRaw++lUnpackValue+  :: forall a.+     (NiceUnpackedValue a)+  => Packed a -> Either UnpackError a+lUnpackValue =+  lUnpackValueRaw . unPacked+ lEncodeValue   :: forall a. (NicePrintedValue a)   => a -> ByteString@@ -52,7 +69,7 @@ valueToScriptExpr   :: forall t. (NicePackedValue t)   => t -> ByteString-valueToScriptExpr = addScriptExprPrefix . blake2b . lPackValue+valueToScriptExpr = addScriptExprPrefix . blake2b . lPackValueRaw  -- | Similar to 'valueToScriptExpr', but for values encoded as 'Expression's. -- This is only used in tests.

@@ -16,6 +16,7 @@      -- * Instructions   , dupL+  , dupLNamed      -- * Other   , VarIsUnnamed@@ -166,17 +167,23 @@         \\ provideConstraintUnsafe @(ConstraintDIPNLorentz n s s' (var : s0) (var : var : s0))         \\ provideConstraintUnsafe @(ConstraintDIGLorentz n s' (var : s) var) +-- | Version of 'dupL' that leaves a named variable on stack.+dupLNamed+  :: forall var name s.+     (HasNamedVar s name var)+  => Label name -> s :-> (name :! var) : s+dupLNamed _ =+  case varPosition @s @name @var of+    VarPosition sn -> dupLUnsafe sn+ -- | Take the element with given label on stack and copy it on top. -- -- If there are multiple variables with given label, the one closest -- to the top of the stack is picked.------ TODO: maybe call it duupL for consistency? Or better not? :thinking: dupL :: forall var name s.         (HasNamedVar s name var)      => Label name -> s :-> var : s-dupL l = case varPosition @s @name @var of-  VarPosition sn -> dupLUnsafe sn # fromNamed l+dupL l = dupLNamed l # fromNamed l  {- Note about optimizations: 

@@ -0,0 +1,89 @@+-- SPDX-FileCopyrightText: 2020 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++-- | Running Lorentz code easily.+--+-- For testing and demonstration purposes.+module Lorentz.Run.Simple+  ( (-$?)+  , (-$)+  , (&?-)+  , (&-)+  , (<-$>)+  ) where++import Fmt (pretty)++import Lorentz.Base+import Lorentz.Run+import Lorentz.Value+import Lorentz.Zip+import Michelson.Interpret+import Michelson.Runtime.Dummy (dummyContractEnv)++{- Note about priority:++We want priority of our operators to be higher than of operators from HUnit+(which is 1), but less than priority of the most our other operators like '#'.+-}++----------------------------------------------------------------------------+-- Common case+----------------------------------------------------------------------------++-- | Run a lambda with given input.+--+-- Note that this always returns one value, but can accept multiple+-- input values (in such case they are grouped into nested pairs).+--+-- For testing and demonstration purposes.+infixr 2 -$?+(-$?) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)+      => (inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailed out+code -$? inp = interpretLorentzLambda dummyContractEnv (unzipInstr # code) inp++-- | Like @'-$?'@, assumes that no failure is possible.+--+-- For testing and demonstration purposes.+--+-- >>> import Lorentz.Instr+--+-- >>> nop -$ 5+-- 5+-- >>> sub -$ (3, 2)+-- 1+-- >>> push 9 -$ ()+-- 9+-- >>> add # add -$ ((1, 2), 3)+-- 6+infixr 2 -$+(-$) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)+     => inps :-> '[out] -> ZippedStack inps -> out+code -$ inp = either (error . pretty) id $ code -$? inp++----------------------------------------------------------------------------+-- Flipped versions+----------------------------------------------------------------------------++-- | Version of (-$?) with arguments flipped.+infixl 2 &?-+(&?-) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)+      => ZippedStack inps -> (inps :-> '[out]) -> Either MichelsonFailed out+(&?-) = flip (-$?)++-- | Version of (-$) with arguments flipped.+infixl 2 &-+(&-) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)+     => ZippedStack inps -> (inps :-> '[out]) -> out+(&-) = flip (-$)++----------------------------------------------------------------------------+-- Experimental versions+----------------------------------------------------------------------------++-- | Version of (-$) applicable to a series of values.+infixl 2 <-$>+(<-$>) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)+       => (inps :-> '[out]) -> [ZippedStack inps] -> [out]+code <-$> inps = map (code -$) inps

@@ -4,7 +4,19 @@  {-# LANGUAGE FunctionalDependencies #-} --- | This module provides storage interfaces.+{- | This module provides storage interfaces.++Whenever you need to write a generic code applicable to different storage+formats, consider using this module.++Use methods like 'stToField' and 'stUpdate' to work with storage from your code.++To explain how e.g. required fields are obtainable from your storage you define+'StoreHasField' instance (and a similar case is for other typeclasses).+We provide the most common building blocks for implementing these instances,+see @Implementations@ section.++-} module Lorentz.StoreClass   ( -- * Class     StoreHasField (..)@@ -51,10 +63,15 @@   , storeEntrypointOpsDeeper   , storeFieldOpsReferTo   , storeSubmapOpsReferTo+  , mapStoreFieldOps+  , mapStoreSubmapOpsKey+  , mapStoreSubmapOpsValue   , storeEntrypointOpsReferTo   , composeStoreFieldOps   , composeStoreSubmapOps+  , sequenceStoreSubmapOps   , composeStoreEntrypointOps+  , zoomStoreSubmapOps      -- * Storage generation   , mkStoreEp@@ -64,8 +81,9 @@  import Lorentz.ADT import Lorentz.Base-import Lorentz.Errors (failUnexpected)+import Lorentz.Iso import Lorentz.Constraints+import Lorentz.Errors (failUnexpected) import qualified Lorentz.Instr as L import qualified Lorentz.Macro as L import Lorentz.Value@@ -141,10 +159,10 @@     -- available.   , sopDelete       :: forall s.-         Maybe (Label mname -> key : store : s :-> store : s)+         Label mname -> key : store : s :-> store : s   , sopInsert       :: forall s.-         Maybe (Label mname -> key : value : store : s :-> store : s)+         Label mname -> key : value : store : s :-> store : s   }  -- | Provides operations on submaps of storage.@@ -172,19 +190,15 @@ -- | Delete a value in storage. stDelete   :: forall store mname key value s.-     (StoreHasSubmap store mname key value, KnownValue value)+     (StoreHasSubmap store mname key value)   => Label mname -> key : store : s :-> store : s-stDelete l = case sopDelete storeSubmapOps of-  Just delOp -> delOp l-  Nothing -> L.dip L.none # stUpdate l+stDelete = sopDelete storeSubmapOps  -- | Add a value in storage. stInsert   :: StoreHasSubmap store mname key value   => Label mname -> key : value : store : s :-> store : s-stInsert l = case sopInsert storeSubmapOps of-  Just insOp -> insOp l-  Nothing -> L.dip L.some # stUpdate l+stInsert = sopInsert storeSubmapOps  -- | Add a value in storage, but fail if it will overwrite some existing entry. stInsertNew@@ -202,25 +216,25 @@  -- | 'BigMap' can be used as standalone key-value storage, -- name of submap is not accounted in this case.-instance (key ~ key', value ~ value', NiceComparable key) =>+instance (key ~ key', value ~ value', NiceComparable key, KnownValue value) =>          StoreHasSubmap (BigMap key' value') name key value where   storeSubmapOps = StoreSubmapOps     { sopMem = \_label -> L.mem     , sopGet = \_label -> L.get     , sopUpdate = \_label -> L.update-    , sopDelete = Nothing-    , sopInsert = Nothing+    , sopDelete = \_label -> L.deleteMap+    , sopInsert = \_label -> L.mapInsert     }  -- | 'Map' can be used as standalone key-value storage if very needed.-instance (key ~ key', value ~ value', NiceComparable key) =>+instance (key ~ key', value ~ value', NiceComparable key, KnownValue value) =>          StoreHasSubmap (Map key' value') name key value where   storeSubmapOps = StoreSubmapOps     { sopMem = \_label -> L.mem     , sopGet = \_label -> L.get     , sopUpdate = \_label -> L.update-    , sopDelete = Nothing-    , sopInsert = Nothing+    , sopDelete = \_label -> L.deleteMap+    , sopInsert = \_label -> L.mapInsert     }  ----------------------------------------------------------------------------@@ -440,8 +454,8 @@   { sopMem = \_l -> sopMem l   , sopGet = \_l -> sopGet l   , sopUpdate = \_l -> sopUpdate l-  , sopDelete = (\op _l -> op l) <$> sopDelete-  , sopInsert = (\op _l -> op l) <$> sopInsert+  , sopDelete = \_l -> sopDelete l+  , sopInsert = \_l -> sopInsert l   }  -- | Pretend that given 'StoreFieldOps' implementation is made up@@ -475,6 +489,60 @@   , sopSetEpStore = \_l -> sopSetEpStore l   } +-- | Change field operations so that they work on a modified field.+--+-- For instance, to go from+-- @StoreFieldOps Storage "name" Integer@+-- to+-- @StoreFieldOps Storage "name" (value :! Integer)@+-- you can use+-- @mapStoreFieldOps (namedIso #value)@+mapStoreFieldOps+  :: LIso field1 field2+  -> StoreFieldOps store name field1+  -> StoreFieldOps store name field2+mapStoreFieldOps LIso{..} StoreFieldOps{..} = StoreFieldOps+  { sopToField = \l -> sopToField l # liTo+  , sopSetField = \l -> liFrom # sopSetField l+  }++-- | Change submap operations so that they work on a modified key.+mapStoreSubmapOpsKey+  :: Lambda key2 key1+  -> StoreSubmapOps store name key1 value+  -> StoreSubmapOps store name key2 value+mapStoreSubmapOpsKey mapper StoreSubmapOps{..} = StoreSubmapOps+  { sopMem = \l ->+      L.framed mapper # sopMem l+  , sopGet = \l ->+      L.framed mapper # sopGet l+  , sopUpdate = \l ->+      L.framed mapper # sopUpdate l+  , sopDelete = \l ->+      L.framed mapper # sopDelete l+  , sopInsert = \l ->+      L.framed mapper # sopInsert l+  }++-- | Change submap operations so that they work on a modified value.+mapStoreSubmapOpsValue+  :: (KnownValue value1)+  => LIso value1 value2+  -> StoreSubmapOps store name key value1+  -> StoreSubmapOps store name key value2+mapStoreSubmapOpsValue LIso{..} StoreSubmapOps{..} = StoreSubmapOps+  { sopMem = \l ->+      sopMem l+  , sopGet = \l ->+      sopGet l # L.lmap liTo+  , sopUpdate = \l ->+      L.dip (L.lmap liFrom) # sopUpdate l+  , sopInsert = \l ->+      L.dip liFrom # sopInsert l+  , sopDelete = \l ->+      sopDelete l+  }+ -- | Chain two implementations of field operations. -- -- Suits for a case when your store does not contain its fields directly@@ -510,20 +578,82 @@       L.dip (L.dip (L.dup # sopToField ops1 l1)) #       sopUpdate ops2 l2 #       sopSetField ops1 l1-  , sopDelete = case sopDelete ops2 of-      Nothing -> Nothing-      Just delOp -> Just $ \l2 ->-        L.dip (L.dup # sopToField ops1 l1) #-        delOp l2 #-        sopSetField ops1 l1-  , sopInsert = case sopInsert ops2 of-      Nothing -> Nothing-      Just insOp -> Just $ \l2 ->-        L.dip (L.dip (L.dup # sopToField ops1 l1)) #-        insOp l2 #-        sopSetField ops1 l1+  , sopDelete = \l2 ->+      L.dip (L.dup # sopToField ops1 l1) #+      sopDelete ops2 l2 #+      sopSetField ops1 l1+  , sopInsert = \l2 ->+      L.dip (L.dip (L.dup # sopToField ops1 l1)) #+      sopInsert ops2 l2 #+      sopSetField ops1 l1   } +-- | Chain implementations of two submap operations sets.+-- Used to provide shortcut access to a nested submap.+--+-- This is very inefficient since on each access to substore+-- it has to be serialized/deserialized. Use this implementation+-- only if due to historical reasons migrating storage is difficult.+--+-- @LIso (Maybe substore) substore@ argument describes how to get+-- @substore@ value if it was absent in map and how to detect when+-- it can be safely removed.+--+-- Example of use:+-- @sequenceStoreSubmapOps #mySubmap nonDefIso storeSubmapOps storeSubmapOps@+sequenceStoreSubmapOps+  :: forall store substore value name subName key1 key2.+     (NiceConstant substore, KnownValue value)+  => Label name+  -> LIso (Maybe substore) substore+  -> StoreSubmapOps store name key1 substore+  -> StoreSubmapOps substore subName key2 value+  -> StoreSubmapOps store subName (key1, key2) value+sequenceStoreSubmapOps l1 substoreIso ops1 ops2 =+  fix $ \res ->+  StoreSubmapOps+  { sopMem = \l2 ->+      L.unpair # L.swap #+      L.dip (sopGet ops1 l1) # L.swap #+      L.ifSome+        (L.swap # sopMem ops2 l2)+        (L.drop # L.push False)+  , sopGet = \l2 ->+      L.unpair # L.swap #+      L.dip (sopGet ops1 l1) # L.swap #+      L.ifSome+        (L.swap # sopGet ops2 l2)+        (L.drop # L.none)+  , sopUpdate = \l2 ->+      prepareUpdate #+      L.dip (sopUpdate ops2 l2 # liFrom substoreIso) #+      sopUpdate ops1 l1+  , sopDelete = \l2 ->+      L.dip L.none # sopUpdate res l2+  , sopInsert = \l2 ->+      prepareUpdate #+      L.dip (sopInsert ops2 l2) #+      sopInsert ops1 l1+  }+  where+    -- Extract all the necessary things prior to update+    prepareUpdate+      :: (key1, key2) : value' : store : s+         :-> key1 : key2 : value' : substore : store : s+    prepareUpdate =+      L.dup # L.car #+      L.dip+        ( L.swap #+          L.dip+            ( L.unpair # L.swap #+              L.dip+                ( L.dip (L.dup @store) #+                  sopGet ops1 l1 # liTo substoreIso+                )+            ) #+          L.swap+        )+ composeStoreEntrypointOps   :: Label nameInStore   -> StoreFieldOps store nameInStore substore@@ -544,6 +674,74 @@       sopSetField ops1 l1   } ++{- | Turn submap operations into operations on a part of the submap value.++Normally, if you need this set of operations, it would be better to split your+submap into several separate submaps, each operating with its own part of the value.+This set of operations is pretty inefficient and exists only as a temporary+measure, if due to historical reasons you have to leave storage format intact.++This implementation puts no distinction between @value == Nothing@ and+@value == Just defValue@ cases.+Getters, when notice a value equal to the default value, report its absence.+Setters tend to remove the value from submap when possible.++@LIso (Maybe value) value@ and @LIso (Maybe subvalue) subvalue@ arguments+describe how to get a value if it was absent in map and how to detect when+it can be safely removed from map.++Example of use:+@zoomStoreSubmapOps #mySubmap nonDefIso nonDefIso storeSubmapOps storeFieldOpsADT@+-}+zoomStoreSubmapOps+  :: forall store submapName nameInSubmap key value subvalue.+     (NiceConstant value, NiceConstant subvalue)+  => Label submapName+  -> LIso (Maybe value) value+  -> LIso (Maybe subvalue) subvalue+  -> StoreSubmapOps store submapName key value+  -> StoreFieldOps value nameInSubmap subvalue+  -> StoreSubmapOps store nameInSubmap key subvalue+zoomStoreSubmapOps l1 valueIso subvalueIso ops1 ops2 =+  fix $ \res ->+  StoreSubmapOps+  { sopMem = \l2 ->+      sopGet ops1 l1 #+      L.ifSome+        (sopToField ops2 l2 # liFrom subvalueIso # L.isSome)+        (L.push False)+  , sopGet = \l2 ->+      sopGet ops1 l1 #+      L.ifSome+        (sopToField ops2 l2 # liFrom subvalueIso)+        L.none+  , sopUpdate = \l2 ->+      L.dip (liTo subvalueIso) #+      updateSubmapValue l2 #+      L.dip (liFrom valueIso) #+      sopUpdate ops1 l1+  , sopDelete = \l2 ->+      L.dip L.none # sopUpdate res l2+  , sopInsert = \l2 ->+      updateSubmapValue l2 #+      sopInsert ops1 l1+  }+  where+    updateSubmapValue+      :: Label nameInSubmap+      -> key : subvalue : store : s+         :-> key : value : store : s+    updateSubmapValue l2 =+      L.dup #+      L.dip+          -- First getting the existing value+        ( L.swap #+          L.dip (L.dip L.dup # sopGet ops1 l1 # liTo valueIso) #+          -- Injecting new subvalue into value+          sopSetField ops2 l2+        )+ -- | Utility to 'push' the 'MText' name of and entrypoint from its 'Label' pushStEp :: Label name -> s :-> MText : s pushStEp = L.push . labelToMText@@ -613,9 +811,12 @@ -} type family StorageContains store (content :: [NamedField]) :: Constraint where   StorageContains _ '[] = ()+  StorageContains store ((n := Identity ty) ': ct) =+    (StoreHasField store n ty, StorageContains store ct)   StorageContains store ((n := k ~> v) ': ct) =     (StoreHasSubmap store n k v, StorageContains store ct)   StorageContains store ((n := ep ::-> es) ': ct) =     (StoreHasEntrypoint store n ep es, StorageContains store ct)+  -- Convenient default case, but not applicable when field type is polymorphic   StorageContains store ((n := ty) ': ct) =     (StoreHasField store n ty, StorageContains store ct)

@@ -139,7 +139,7 @@      )   => Label name -> a -> UParam entries mkUParam label (a :: a) =-  UParamUnsafe (labelToMText label, lPackValue a)+  UParamUnsafe (labelToMText label, lPackValueRaw a)     \\ nicePackedValueEvi @a  -- Example@@ -190,7 +190,7 @@       fmap (name,) .       first (const ArgumentUnpackFailed) .       fmap ConstrainedSome .-      lUnpackValue @arg $+      lUnpackValueRaw @arg $       bytes     | otherwise = unpackUParam @c @entries (UParamUnsafe (name, bytes)) @@ -279,7 +279,7 @@   caseUParamUnsafe (CaseClauseU clause :& clauses) fallback =     dup # unwrapUParam # car #     push (mkMTextUnsafe $ symbolValT' @name) # eq #-    if_ (unwrapUParam # cdr # unpack #+    if_ (unwrapUParam # cdr # unpackRaw #          ifSome nop (failCustom_ #uparamArgumentUnpackFailed) # clause)         (cutUParamEntry # caseUParamUnsafe clauses fallback)     where@@ -371,7 +371,7 @@    adtToRec (G.M1 (G.M1 (G.K1 a))) = UParamUnsafe     ( symbolToMText @name-    , lPackValue a+    , lPackValueRaw a     )  instance

@@ -61,22 +61,36 @@     -- * Misc   , Default (..)   , Label (..)+  , PrintAsValue (..)    -- * Re-exports   , module ReExports   ) where +import Data.Constraint ((\\)) import Data.Default (Default(..)) +import Fmt (Buildable(..)) import Lorentz.Address+import Lorentz.Constraints.Scopes import Michelson.Text import Michelson.Typed (EntrypointCall, IsoValue(..), SomeEntrypointCall, Value, WellTypedIsoValue) import qualified Michelson.Typed as M import Tezos.Core-  (ChainId, Mutez, Timestamp, timestampFromSeconds, timestampFromUTCTime, timestampQuote, toMutez,-  zeroMutez, oneMutez)+  (ChainId, Mutez, Timestamp, oneMutez, timestampFromSeconds, timestampFromUTCTime, timestampQuote,+  toMutez, zeroMutez) import Tezos.Crypto (KeyHash, PublicKey, Signature) import Util.CustomGeneric as ReExports import Util.Label (Label(..))  type List = []++-- | Provides 'Buildable' instance that prints Lorentz value via Michelson's+-- 'Value'.+--+-- Result won't be very pretty, but this avoids requiring 'Show' or+-- 'Buildable' instances.+newtype PrintAsValue a = PrintAsValue a++instance NicePrintedValue a => Buildable (PrintAsValue a) where+  build (PrintAsValue a) = build (toVal a) \\ nicePrintedValueEvi @a

@@ -12,6 +12,8 @@ -- not only lambdas, into a valid value. module Lorentz.Zip   ( ZipInstr (..)+  , zipInstr+  , unzipInstr   , ZipInstrs   , zippingStack   , unzippingStack@@ -26,37 +28,65 @@ import Michelson.Typed import Michelson.Untyped (noAnn) +-- | Version of '#' which performs some optimizations immediately.+--+-- In particular, this avoids glueing @Nop@s and @DIP Nop@s.+(##) :: (a :-> b) -> (b :-> c) -> (a :-> c)+I l ## I r = I (seqOpt l r)+l ## r = l # r++seqOpt :: Instr a b -> Instr b c -> Instr a c+seqOpt l r =+  -- We are very verbose about cases to avoid+  -- significant compilation time increase+  case l of+    Nop -> r+    DIP Nop -> r+    x -> case r of+      Nop -> x+      DIP Nop -> x+      _ -> l `Seq` r++{- We have to work on low level because even "Lorentz.Instr" depends+   on this module.+-}+ -- | Zipping stack into tuple and back. class (KnownIsoT (ZippedStack s)) => ZipInstr (s :: [Kind.Type]) where   -- | A type which contains the whole stack zipped.   type ZippedStack s :: Kind.Type -  -- | Fold given stack into single value.-  zipInstr :: s :-> '[ZippedStack s]+  -- | Fold given stack into single value in typed Michelson.+  zipInstrTyped :: Instr (ToTs s) '[ToT (ZippedStack s)] -  -- | Unfold given stack from a single value.-  unzipInstr :: '[ZippedStack s] :-> s+  -- | Unfold given stack from a single value in typed Michelson.+  unzipInstrTyped :: Instr '[ToT (ZippedStack s)] (ToTs s) -{- Further we have to work on low level because even "Lorentz.Instr" depends-   on this module.--} +-- | Fold given stack into single value.+zipInstr :: forall s. ZipInstr s => s :-> '[ZippedStack s]+zipInstr = I (zipInstrTyped @s)++-- | Unfold given stack from a single value.+unzipInstr :: forall s. ZipInstr s => '[ZippedStack s] :-> s+unzipInstr = I (unzipInstrTyped @s)+ instance ZipInstr '[] where   type ZippedStack '[] = ()-  zipInstr = I UNIT-  unzipInstr = I DROP+  zipInstrTyped = UNIT+  unzipInstrTyped = DROP  instance (KnownIsoT a) => ZipInstr '[a] where   type ZippedStack '[a] = a-  zipInstr = I Nop-  unzipInstr = I Nop+  zipInstrTyped = Nop+  unzipInstrTyped = Nop  -- | Such definition seems the only possible one we can support -- efficiently.-instance ZipInstr ((a, b) ': s) => ZipInstr (a ': b ': s) where-  type ZippedStack (a ': b ': s) = ZippedStack ((a, b) ': s)-  zipInstr = I PAIR ## zipInstr @((a, b) ': s)-  unzipInstr = unzipInstr @((a, b) ': s) ## I (DUP `Seq` CAR `Seq` DIP CDR)+instance (ZipInstr (b ': s), KnownIsoT a) => ZipInstr (a ': b ': s) where+  type ZippedStack (a ': b ': s) = (a, ZippedStack (b ': s))+  zipInstrTyped = DIP (zipInstrTyped @(b ': s)) `seqOpt` PAIR+  unzipInstrTyped = UNPAIR `seqOpt` DIP (unzipInstrTyped @(b ': s))  -- | Require several stacks to comply 'ZipInstr' constraint. type ZipInstrs ss = Each '[ZipInstr] ss