lorentz 0.11.0 → 0.12.0

raw patch · 31 files changed

+947/−324 lines, 31 files

Files

• CHANGES.md +31/−0
• lorentz.cabal +2/−1
• src/Lorentz.hs +1/−0
• src/Lorentz/ADT.hs +20/−12
• src/Lorentz/Annotation.hs +11/−5
• src/Lorentz/Base.hs +42/−3
• src/Lorentz/Bytes.hs +2/−2
• src/Lorentz/Constraints/Derivative.hs +32/−0
• src/Lorentz/Constraints/Scopes.hs +32/−21
• src/Lorentz/ContractRegistry.hs +5/−9
• src/Lorentz/Doc.hs +10/−3
• src/Lorentz/Entrypoints/Core.hs +1/−1
• src/Lorentz/Entrypoints/Doc.hs +1/−2
• src/Lorentz/Entrypoints/Helpers.hs +2/−2
• src/Lorentz/Entrypoints/Impl.hs +5/−4
• src/Lorentz/Errors.hs +17/−22
• src/Lorentz/Errors/Numeric/Contract.hs +7/−6
• src/Lorentz/Expr.hs +269/−0
• src/Lorentz/Ext.hs +2/−2
• src/Lorentz/Instr.hs +81/−32
• src/Lorentz/Macro.hs +35/−31
• src/Lorentz/OpSize.hs +2/−4
• src/Lorentz/Pack.hs +3/−3
• src/Lorentz/Print.hs +2/−4
• src/Lorentz/Rebinded.hs +50/−34
• src/Lorentz/Referenced.hs +8/−4
• src/Lorentz/ReferencedByName.hs +11/−10
• src/Lorentz/Run.hs +109/−45
• src/Lorentz/StoreClass.hs +123/−47
• src/Lorentz/UParam.hs +16/−15
• src/Lorentz/Value.hs +15/−0

@@ -2,6 +2,33 @@ ========== <!-- Append new entries here --> +0.12.0+======++* [!854](https://gitlab.com/morley-framework/morley/-/merge_requests/854)+  + `StoreHasField` instance definition is no more necessary for simple ADT storage types.+* [!846](https://gitlab.com/morley-framework/morley/-/merge_requests/846)+  + Reorganized `Contract` type and related stuff.+  + Added methods for reading `Contract` from file.++  Migration guide (sufficient unless you worked on framework internals):+  + In case you needed to use non-default contract compilation options, use `mkContractWith` now.++  For more details, see documentation of `Lorentz.Run`.+* [!832](https://gitlab.com/morley-framework/morley/-/merge_requests/832)+  + Add tickets feature.+  + Add dupable restriction to `dup`-like instructions and some high-level helpers.+    See `dup`'s documentation for notes on how to live in this brand new world.+* [!838](https://gitlab.com/morley-framework/morley/-/merge_requests/838)+  + All unsafe functions and data constructors now contain "unsafe" word+    at prefix position. E.g `UnsafeMText`, `unsafeMkAnnotation`.+* [!794](https://gitlab.com/morley-framework/morley/-/merge_requests/794)+  [!833](https://gitlab.com/morley-framework/morley/-/merge_requests/833)+  + Added `Lorentz.Expr` module with primitives for convenient expressions evaluation.+    * Added `listE` to construct an expression list from a list of expressions.+  + `if ... then ... else` now is polymorphic in the first argument.+    * Boolean expressions now can appear as condition for `if`.+ 0.11.0 ====== * [!814](https://gitlab.com/morley-framework/morley/-/merge_requests/814)@@ -28,6 +55,10 @@   + Added new Edo macros: `CAR k` and `CDR k` as `carN` and `cdrN`. * [!798](https://gitlab.com/morley-framework/morley/-/merge_requests/798)   + Added back the `UnaryArithOpHs Abs Integer` instance that was removed by accident.+* [!802](https://gitlab.com/morley-framework/morley/-/merge_requests/802)+  + Add `NiceParameterFull` and `NiceStorage` constraints to Lorentz `Contract` constructor.+  + Moved `coDisableInitialCast` to `CompilationOptions` datatype.+  0.10.0 ======

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           lorentz-version:        0.11.0+version:        0.12.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@@ -54,6 +54,7 @@       Lorentz.Errors.Numeric       Lorentz.Errors.Numeric.Contract       Lorentz.Errors.Numeric.Doc+      Lorentz.Expr       Lorentz.Ext       Lorentz.Extensible       Lorentz.Instr

@@ -21,6 +21,7 @@ import Lorentz.Errors as Exports import Lorentz.Errors.Common as Exports () import Lorentz.Errors.Numeric as Exports+import Lorentz.Expr as Exports import Lorentz.Ext as Exports import Lorentz.Instr as Exports import Lorentz.Iso as Exports

@@ -26,7 +26,7 @@   , wrapOne   , case_   , caseT-  , unwrapUnsafe_+  , unsafeUnwrap_   , CaseTC   , CaseArrow (..)   , CaseClauseL (..)@@ -45,15 +45,16 @@ import Data.Constraint ((\\)) import Data.Vinyl.Core (RMap(..), Rec(..)) import GHC.TypeLits (AppendSymbol, Symbol)-import Named ((:!), (:?), arg, argDef, argF)+import Named (arg, argDef, argF, (:!), (:?))  import Lorentz.Base import Lorentz.Coercions+import Lorentz.Constraints import Michelson.Typed.Haskell.Instr import Michelson.Typed.Haskell.Value import Michelson.Typed.Instr import Util.Label (Label)-import Util.Type (type (++), KnownList)+import Util.Type (KnownList, type (++)) import Util.TypeTuple  -- | Allows field access and modification.@@ -89,7 +90,7 @@   :: forall dt name st.      InstrGetFieldC dt name   => Label name -> dt : st :-> GetFieldType dt name : st-toField = I . instrGetField @dt+toField = I . instrToField @dt  -- | Like 'toField', but leaves field named. toFieldNamed@@ -99,16 +100,22 @@ toFieldNamed l = toField l # forcedCoerce_  -- | Extract a field of a datatype, leaving the original datatype on stack.+--+-- TODO: [#585] Make this and all depending functions require only+-- @Dupable (GetFieldType dt name)@ getField   :: forall dt name st.-     InstrGetFieldC dt name+     (InstrGetFieldC dt name, Dupable dt)   => Label name -> dt : st :-> GetFieldType dt name : dt ': st-getField l = I DUP # toField @dt l+getField l = dup # toField l+  where+    dup :: forall a s. Dupable a => a : s :-> a : a : s+    dup = I DUP \\ dupableEvi @a  -- | Like 'getField', but leaves field named. getFieldNamed   :: forall dt name st.-     InstrGetFieldC dt name+     (InstrGetFieldC dt name, Dupable dt)   => Label name -> dt : st :-> (name :! GetFieldType dt name) : dt ': st getFieldNamed l = getField l # coerceWrap @@ -124,6 +131,7 @@   :: forall dt name st.      ( InstrGetFieldC dt name      , InstrSetFieldC dt name+     , Dupable dt      )   => Label name   -> (forall st0. (GetFieldType dt name ': st0) :-> (GetFieldType dt name ': st0))@@ -165,7 +173,7 @@ constructStack   :: forall dt fields st .   ( InstrConstructC dt-  , ToTs fields ~ ToTs (ConstructorFieldTypes dt)+  , fields ~ ConstructorFieldTypes dt   , KnownList fields   )   => (fields ++ st) :-> dt : st@@ -179,7 +187,7 @@   :: forall dt fields st .   ( InstrDeconstructC dt   , KnownList fields-  , ToTs fields ~ ToTs (ConstructorFieldTypes dt)+  , fields ~ ConstructorFieldTypes dt   )   => dt : st :-> (fields ++ st) deconstruct =@@ -273,10 +281,10 @@   )  -- | Unwrap a constructor with the given name. Useful for sum types.-unwrapUnsafe_+unsafeUnwrap_   :: forall dt name st.      InstrUnwrapC dt name   => Label name -> dt : st :-> (CtorOnlyField name dt ': st)-unwrapUnsafe_ =+unsafeUnwrap_ =   case appendCtorFieldAxiom @(GetCtorField dt name) @st of-    Dict -> I . instrUnwrapUnsafe @dt+    Dict -> I . unsafeInstrUnwrap @dt

@@ -32,10 +32,10 @@  import Michelson.Text import Michelson.Typed-  (BigMap, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, ToT, insertTypeAnn,-  starNotes)+  (BigMap, BigMapId, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, Ticket, ToT,+  insertTypeAnn, starNotes) import Michelson.Typed.Haskell.Value (GValueType)-import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, mkAnnotationUnsafe, noAnn)+import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, noAnn, unsafeMkAnnotation) import Tezos.Address import Tezos.Core import Tezos.Crypto@@ -75,7 +75,7 @@ ----------------------------------------------------------------------------  ctorNameToAnnWithOptions :: forall ctor. (KnownSymbol ctor, HasCallStack) => AnnOptions -> FieldAnn-ctorNameToAnnWithOptions o = mkAnnotationUnsafe . fieldAnnModifier o $ headToLower $ (symbolValT' @ctor)+ctorNameToAnnWithOptions o = unsafeMkAnnotation . fieldAnnModifier o $ headToLower $ (symbolValT' @ctor)  -- | Used in `GHasAnnotation` and `HasAnnotation` as a flag to track -- whether or not it directly follows an entrypoint to avoid introducing@@ -114,7 +114,7 @@     getAnnotation @a b     where       symbolAnn :: forall s. KnownSymbol s => TypeAnn-      symbolAnn = mkAnnotationUnsafe $ symbolValT' @s+      symbolAnn = unsafeMkAnnotation $ symbolValT' @s  instance (HasAnnotation (Maybe a), KnownSymbol name)   => HasAnnotation (NamedF Maybe a name) where@@ -168,11 +168,17 @@ instance (HasAnnotation a) => HasAnnotation (ContractRef a) where   getAnnotation _ = NTContract noAnn (getAnnotation @a NotFollowEntrypoint) +instance (HasAnnotation d) => HasAnnotation (Ticket d) where+  getAnnotation _ = NTTicket noAnn (getAnnotation @d NotFollowEntrypoint)+ instance (HasAnnotation k, HasAnnotation v) => HasAnnotation (Map k v) where   getAnnotation _ = NTMap noAnn (getAnnotation @k NotFollowEntrypoint) (getAnnotation @v NotFollowEntrypoint)  instance (HasAnnotation k, HasAnnotation v) => HasAnnotation (BigMap k v) where   getAnnotation _ = NTBigMap noAnn (getAnnotation @k NotFollowEntrypoint) (getAnnotation @v NotFollowEntrypoint)++instance (HasAnnotation k, HasAnnotation v) => HasAnnotation (BigMapId k v) where+  getAnnotation _ = starNotes  instance (KnownIsoT v) => HasAnnotation (Set v) where   getAnnotation _ = starNotes

@@ -29,6 +29,8 @@   , ContractOut   , ContractCode   , SomeContractCode (..)+  , Contract (..)+  , toMichelsonContract   , Lambda   ) where @@ -42,11 +44,13 @@ import Michelson.Parser (ParserException, parseExpandValue) import Michelson.Preprocess (transformBytes, transformStrings) import Michelson.Text (MText)-import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue)+import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue, typeCheckingWith) import Michelson.Typed   (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,   rfMerge)+import qualified Michelson.Typed as M (Contract(..)) import qualified Michelson.Untyped as U+import Morley.Micheline (ToExpression(..))  -- | Alias for instruction which hides inner types representation via 'T'. newtype (inp :: [Type]) :-> (out :: [Type]) = LorentzInstr@@ -54,6 +58,9 @@   } deriving newtype (Show, Eq) infixr 1 :-> +instance NFData (i :-> o) where+  rnf (LorentzInstr i) = rnf i+ instance Semigroup (s :-> s) where   (<>) = (#) instance Monoid (s :-> s) where@@ -94,9 +101,9 @@ iWithVarAnnotations :: HasCallStack => [Text] -> inp :-> out -> inp :-> out iWithVarAnnotations annots (LorentzInstr i) = case i of   RfNormal instr -> LorentzInstr $ RfNormal $-    InstrWithVarNotes (NE.fromList $ map U.AnnotationUnsafe annots) instr+    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr   RfAlwaysFails instr -> LorentzInstr $ RfAlwaysFails $-    InstrWithVarNotes (NE.fromList $ map U.AnnotationUnsafe annots) instr+    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr  -- There is also @instance IsoValue (i :-> o)@ in the "Lorentz.Zip" module. @@ -115,6 +122,34 @@     => ContractCode cp st     -> SomeContractCode +-- | Compiled Lorentz contract.+data Contract cp st =+  (NiceParameterFull cp, NiceStorage st) =>+  Contract+  { -- | Ready contract code.+    cMichelsonContract :: M.Contract (ToT cp) (ToT st)++    -- | Contract that contains documentation.+    --+    -- We have to keep it separately, since optimizer is free to destroy+    -- documentation blocks.+    -- Also, it is not 'ContractDoc' but Lorentz code because the latter is+    -- easier to modify.+  , cDocumentedCode :: ~(ContractCode cp st)+  }++deriving stock instance Show (Contract cp st)+deriving stock instance Eq (Contract cp st)+instance NFData (Contract cp st) where+  rnf (Contract c d) = rnf c `seq` rnf d++instance ToExpression (Contract cp st) where+  toExpression = toExpression . toMichelsonContract++-- | Demote Lorentz 'Contract' to Michelson typed 'M.Contract'.+toMichelsonContract :: Contract cp st -> M.Contract (ToT cp) (ToT st)+toMichelsonContract = cMichelsonContract+ -- | An alias for ':'. -- -- We discourage its use as this hinders reading error messages@@ -122,6 +157,9 @@ type (&) (a :: Type) (b :: [Type]) = a ': b infixr 2 & +-- | Function composition for instructions.+--+-- Note that, unlike Morley's '(:#)' operator, '(#)' is left-associative. (#) :: (a :-> b) -> (b :-> c) -> a :-> c I l # I r = I (l `Seq` r) I l # FI r = FI (l `Seq` r)@@ -160,6 +198,7 @@     toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))     toTyped =       first ParseLorentzTypecheckError .+      typeCheckingWith def .       runTypeCheckIsolated .       usingReaderT (def @InstrCallStack) .       typeCheckValue

@@ -121,7 +121,7 @@ data HashAlgoTag  -- | Hash of type @t@ evaluated from data of type @a@.-newtype Hash (alg :: HashAlgorithmKind) a = HashUnsafe { unHash :: ByteString }+newtype Hash (alg :: HashAlgorithmKind) a = UnsafeHash { unHash :: ByteString }   deriving stock (Show, Eq, Ord, Generic)   deriving newtype (IsoValue, HasAnnotation, BytesLike) @@ -167,7 +167,7 @@ toHashHs   :: forall alg bs. (BytesLike bs, KnownHashAlgorithm alg)   => bs -> Hash alg bs-toHashHs = HashUnsafe . computeHash @alg . toBytes+toHashHs = UnsafeHash . computeHash @alg . toBytes  -- | Documentation item for hash algorithms. data DHashAlgorithm where

@@ -8,9 +8,41 @@ -- modules dependencies graph (unlike "Lorentz.Constraints.Scopes"). module Lorentz.Constraints.Derivative   ( NiceParameterFull+  , DupableDecision (..)+  , decideOnDupable   ) where +import Lorentz.Constraints.Scopes import Lorentz.Entrypoints.Core+import Michelson.Typed.Haskell.Value+import Michelson.Typed.Scope  -- | Constraint applied to a whole parameter type. type NiceParameterFull cp = (Typeable cp, ParameterDeclaresEntrypoints cp)++-- | Tells whether given type is dupable or not.+data DupableDecision a+  = Dupable a => IsDupable+  | IsNotDupable++-- | Check whether given value is dupable, returning a proof of that when it is.+--+-- This lets defining methods that behave differently depending on whether given+-- value is dupable or not. This may be suitable when for the dupable case you+-- can provide a more efficient implementation, but you also want your+-- implementation to be generic.+--+-- Example:+--+-- @+-- code = case decideOnDupable @a of+--   IsDupable -> do dup; ...+--   IsNotDupable -> ...+-- @+--+decideOnDupable+  :: forall a. (KnownValue a) => DupableDecision a+decideOnDupable =+  case checkScope @(DupableScope (ToT a)) of+    Right Dict -> IsDupable+    Left _ -> IsNotDupable

@@ -12,16 +12,19 @@   ( -- * Grouped constraints     NiceComparable   , NiceConstant+  , Dupable   , NiceFullPackedValue   , NicePackedValue   , NiceParameter   , NicePrintedValue   , NiceStorage   , NiceUnpackedValue+  , NiceNoBigMap    , niceParameterEvi   , niceStorageEvi   , niceConstantEvi+  , dupableEvi   , nicePackedValueEvi   , niceUnpackedValueEvi   , nicePrintedValueEvi@@ -37,7 +40,7 @@     withDict   ) where -import Data.Constraint (evidence, trans, weaken2)+import Data.Constraint (evidence, trans, weaken1)  import Lorentz.Annotation (HasAnnotation) import Michelson.Typed@@ -50,17 +53,17 @@ instance (IsoValue a, Typeable a) => KnownValue a  -- | Ensure given type does not contain "operation".-class (IsoValue a, ForbidOp (ToT a)) => NoOperation a-instance (IsoValue a, ForbidOp (ToT a)) => NoOperation a+class (ForbidOp (ToT a), IsoValue a) => NoOperation a+instance (ForbidOp (ToT a), IsoValue a) => NoOperation a -class (IsoValue a, ForbidContract (ToT a)) => NoContractType a-instance (IsoValue a, ForbidContract (ToT a)) => NoContractType a+class (ForbidContract (ToT a), IsoValue a) => NoContractType a+instance (ForbidContract (ToT a), IsoValue a) => NoContractType a -class (IsoValue a, ForbidBigMap (ToT a)) => NoBigMap a-instance (IsoValue a, ForbidBigMap (ToT a)) => NoBigMap a+class (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a+instance (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a -class (IsoValue a, HasNoNestedBigMaps (ToT a)) => CanHaveBigMap a-instance (IsoValue a, HasNoNestedBigMaps (ToT a)) => CanHaveBigMap a+class (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a+instance (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a  -- | Constraint applied to any part of parameter type. --@@ -69,26 +72,30 @@ -- -- Using this type is justified e.g. when calling another contract, there -- you usually supply an entrypoint argument, not the whole parameter.-type NiceParameter a = (KnownValue a, ProperParameterBetterErrors (ToT a))+type NiceParameter a = (ProperParameterBetterErrors (ToT a), KnownValue a)  type NiceStorage a =-  (HasAnnotation a, KnownValue a, ProperStorageBetterErrors (ToT a))+  (ProperStorageBetterErrors (ToT a), HasAnnotation a, KnownValue a) -type NiceConstant a = (KnownValue a, ProperConstantBetterErrors (ToT a))+type NiceConstant a = (ProperConstantBetterErrors (ToT a), KnownValue a) -type NicePackedValue a = (KnownValue a, ProperPackedValBetterErrors (ToT a))+type Dupable a = (ProperDupableBetterErrors (ToT a), KnownValue a) -type NiceUnpackedValue a = (KnownValue a, ProperUnpackedValBetterErrors (ToT a))+type NicePackedValue a = (ProperPackedValBetterErrors (ToT a), KnownValue a) +type NiceUnpackedValue a = (ProperUnpackedValBetterErrors (ToT a), KnownValue a)+ type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a) -type NicePrintedValue a = (KnownValue a, ProperPrintedValBetterErrors (ToT a))+type NicePrintedValue a = (ProperPrintedValBetterErrors (ToT a), KnownValue a) -type NiceComparable n = (KnownValue n, Comparable (ToT n))+type NiceComparable n = (Comparable (ToT n), KnownValue n) +type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n))+ niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a) niceParameterEvi =-  properParameterEvi @(ToT a) `trans` weaken2+  properParameterEvi @(ToT a) `trans` weaken1  niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a) niceStorageEvi =@@ -96,16 +103,20 @@  niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a) niceConstantEvi =-  properConstantEvi @(ToT a) `trans` weaken2+  properConstantEvi @(ToT a) `trans` weaken1 +dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)+dupableEvi =+  properDupableEvi @(ToT a) `trans` weaken1+ nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a) nicePackedValueEvi =-  properPackedValEvi @(ToT a) `trans` weaken2+  properPackedValEvi @(ToT a) `trans` weaken1  niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a) niceUnpackedValueEvi =-  properUnpackedValEvi @(ToT a) `trans` weaken2+  properUnpackedValEvi @(ToT a) `trans` weaken1  nicePrintedValueEvi :: forall a. NicePrintedValue a :- PrintedValScope (ToT a) nicePrintedValueEvi =-  properPrintedValEvi @(ToT a) `trans` weaken2+  properPrintedValEvi @(ToT a) `trans` weaken1

@@ -39,10 +39,11 @@ import Michelson.Typed (IsoValue(..), Notes) import qualified Michelson.Typed as M (Contract(..)) import Morley.Micheline+import Util.CLI (mkCommandParser)  data ContractInfo =   forall cp st.-    (NiceParameterFull cp, NiceStorage st) =>+    (NiceStorage st) =>   ContractInfo   { ciContract :: Contract cp st   , ciIsDocumented :: Bool@@ -121,11 +122,6 @@         mapMaybe storageSubCmd (Map.toList $ unContractRegistry registry)   )   where-    mkCommandParser commandName parser desc =-      Opt.command commandName $-      Opt.info (Opt.helper <*> parser) $-      Opt.progDesc desc-     listSubCmd =       mkCommandParser "list"       (pure List)@@ -199,8 +195,8 @@     (ContractInfo{..}, name) <- getContract mName registry     let       compiledContract = case ciStorageNotes of-        Just notes -> (compileLorentzContract ciContract) { M.cStoreNotes = notes }-        Nothing -> compileLorentzContract ciContract+        Just notes -> (toMichelsonContract ciContract) { M.cStoreNotes = notes }+        Nothing -> toMichelsonContract ciContract     writeFunc (toString name <> ".tz") mOutput $       if useMicheline       then toLazyText $ encodePrettyToTextBuilder $ toExpression compiledContract@@ -210,7 +206,7 @@   Analyze mName -> do     (ContractInfo{..}, _) <- getContract mName registry     let compiledContract  =-          compileLorentzContract ciContract+          toMichelsonContract ciContract     putTextLn $ pretty $ analyze $ M.cCode compiledContract   PrintStorage (SomeNiceStorage (storage :: st)) useMicheline ->     if useMicheline

@@ -72,13 +72,13 @@   , poly2TypeDocMdReference   , homomorphicTypeDocHaskellRep   , concreteTypeDocHaskellRep-  , concreteTypeDocHaskellRepUnsafe+  , unsafeConcreteTypeDocHaskellRep   , haskellAddNewtypeField   , haskellRepNoFields   , haskellRepStripFieldPrefix   , homomorphicTypeDocMichelsonRep   , concreteTypeDocMichelsonRep-  , concreteTypeDocMichelsonRepUnsafe+  , unsafeConcreteTypeDocMichelsonRep   , mdTocFromRef   ) where @@ -92,7 +92,7 @@ import Michelson.Doc import Michelson.Optimizer import Michelson.Printer-import Michelson.Typed+import Michelson.Typed hiding (Contract) import Util.Markdown import Util.Type @@ -147,6 +147,13 @@   buildDocUnfinalized = buildDocUnfinalized . iAnyCode instance ContainsUpdateableDoc (i :-> o) where   modifyDocEntirely how = iMapAnyCode $ modifyDocEntirely how++instance ContainsDoc (Contract cp st) where+  buildDocUnfinalized =+    buildDocUnfinalized . cDocumentedCode+instance ContainsUpdateableDoc (Contract cp st) where+  modifyDocEntirely how c =+    c{ cDocumentedCode = modifyDocEntirely how (cDocumentedCode c) }  {-# DEPRECATED buildLorentzDocWithGitRev     "Use `buildDoc . attachDocCommons gitRev` instead."

@@ -353,7 +353,7 @@   :: forall cp.      (NiceParameter cp, ForbidExplicitDefaultEntrypoint cp)   => SomeEntrypointCall cp-sepcCallRootChecked = sepcCallRootUnsafe \\ niceParameterEvi @cp+sepcCallRootChecked = unsafeSepcCallRoot \\ niceParameterEvi @cp   where     -- Avoiding redundant-constraints warning.     _validUsage = Dict @(ForbidExplicitDefaultEntrypoint cp)

@@ -47,7 +47,6 @@ import Data.Char (toLower) import Data.Constraint (Dict(..)) import qualified Data.Map as Map-import Data.Singletons (sing) import qualified Data.Text as T import Data.Vinyl.Core (RMap, rappend) import Fmt (Buildable(..), build, fmt, listF)@@ -65,7 +64,7 @@ import Lorentz.Entrypoints.Impl import Michelson.Printer (printTypedValue) import Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)-import Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue)+import Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue, sing) import qualified Michelson.Typed as T import Michelson.Typed.Haskell.Doc import Michelson.Typed.Haskell.Instr

@@ -12,13 +12,13 @@  import Michelson.Typed.Haskell import Michelson.Typed.T-import Michelson.Untyped (EpName, FieldAnn, mkAnnotationUnsafe, epNameFromParamAnn)+import Michelson.Untyped (EpName, FieldAnn, unsafeMkAnnotation, epNameFromParamAnn) import Util.Text import Util.Type import Util.TypeLits  ctorNameToAnn :: forall ctor. (KnownSymbol ctor, HasCallStack) => FieldAnn-ctorNameToAnn = mkAnnotationUnsafe . headToLower $ (symbolValT' @ctor)+ctorNameToAnn = unsafeMkAnnotation . headToLower $ (symbolValT' @ctor)  ctorNameToEp :: forall ctor. (KnownSymbol ctor, HasCallStack) => EpName ctorNameToEp =

@@ -16,6 +16,7 @@   , BuildEPTree   ) where +import Data.Singletons (withSingI) import Data.Singletons.Prelude (SBool(SFalse, STrue)) import Data.Singletons.Prelude.Eq ((%==)) import Data.Vinyl.Core (Rec(..), (<+>))@@ -28,7 +29,7 @@ import Lorentz.Value import Michelson.Typed import Michelson.Typed.Haskell.Value (GValueType)-import Michelson.Untyped (FieldAnn, mkAnnotationUnsafe, noAnn)+import Michelson.Untyped (FieldAnn, unsafeMkAnnotation, noAnn) import Util.Fcf (type (<|>), Over2, TyEqSing) import Util.Type @@ -107,7 +108,7 @@       '[ Fcf.Is (TyEqSing r) ('Just cp)        , Fcf.Else (PlainLookupEntrypointExt deriv cp)        ]-  epdNotes = (plainEpdNotesExt @deriv @cp, mkAnnotationUnsafe (symbolValT' @r))+  epdNotes = (plainEpdNotesExt @deriv @cp, unsafeMkAnnotation (symbolValT' @r))   epdCall label@(Label :: Label name) = case sing @r %== sing @name of       STrue -> EpConstructed EplArgHere       SFalse -> plainEpdCallExt @deriv @cp label@@ -261,7 +262,7 @@     in (NTOr noAnn xann yann xnotes ynotes, noAnn)   gMkEpLiftSequence label =     case sing @(GValueType (x G.:+: y)) of-      STOr sl _ -> case (checkOpPresence sl, checkNestedBigMapsPresence sl) of+      STOr sl sr -> withSingI sl $ withSingI sr $ case (checkOpPresence sl, checkNestedBigMapsPresence sl) of         (OpAbsent, NestedBigMapsAbsent) ->           case gMkEpLiftSequence @mode @epx @x label of             EpConstructed liftSeq -> EpConstructed (EplWrapLeft liftSeq)@@ -355,7 +356,7 @@   gMkEpLiftSequence _ = EpConstructionFailed   gMkDescs = RNil -instance Each '[KnownT] [GValueType x, GValueType y] =>+instance Each '[SingI] [GValueType x, GValueType y] =>          GEntrypointsNotes mode 'EPLeaf (x G.:*: y) where   type GAllEntrypoints mode 'EPLeaf (x G.:*: y) = '[]   type GLookupEntrypoint mode 'EPLeaf (x G.:*: y) = Fcf.ConstFn 'Nothing

@@ -12,6 +12,7 @@   ( -- * Haskell to 'Value' conversion     IsError (..)   , ErrorScope+  , ConstantScope   , isoErrorToVal   , isoErrorFromVal   , ErrorHasDoc (..)@@ -50,8 +51,6 @@  import qualified Data.Char as C import qualified Data.List as L-import Data.Singletons (demote)-import Data.Typeable (cast) import Fmt (Buildable, build, fmt, pretty, (+|), (|+)) import Language.Haskell.TH.Syntax (Lift) import Text.Read (readsPrec)@@ -66,33 +65,31 @@ import Michelson.Typed.Haskell import Michelson.Typed.Instr import Michelson.Typed.Scope+import Michelson.Typed.Sing (castM, castSingE) import Util.Markdown import Util.Type-import Util.Typeable import Util.TypeLits+import Util.Typeable  ---------------------------------------------------------------------------- -- IsError ---------------------------------------------------------------------------- -type ErrorScope t =-  ( Typeable t-  -- Since 008 it's prohibited to fail with non-packable values and with the-  -- 'Contract t' type values, which is equivalent to our @ConstantScope@ constraint.-  -- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.-  , ConstantScope t-  )+-- | Since 008 it's prohibited to fail with non-packable values and with the+-- 'Contract t' type values, which is equivalent to our @ConstantScope@ constraint.+-- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.+type ErrorScope t = ConstantScope t  type KnownError a = ErrorScope (ToT a)  -- | Haskell type representing error.-class (Typeable e, ErrorHasDoc e) => IsError e where+class (ErrorHasDoc e) => IsError e where    -- | Converts a Haskell error into @Value@ representation.   errorToVal :: e -> (forall t. ErrorScope t => Value t -> r) -> r    -- | Converts a @Value@ into Haskell error.-  errorFromVal :: (KnownT t) => Value t -> Either Text e+  errorFromVal :: (SingI t) => Value t -> Either Text e  -- | Implementation of 'errorToVal' via 'IsoValue'. isoErrorToVal@@ -102,9 +99,9 @@  -- | Implementation of 'errorFromVal' via 'IsoValue'. isoErrorFromVal-  :: (Typeable t, Typeable (ToT e), IsoValue e)+  :: (SingI t, KnownIsoT e, IsoValue e)   => Value t -> Either Text e-isoErrorFromVal e = fromVal <$> gcastE e+isoErrorFromVal e = fromVal <$> castSingE e  class Typeable e => ErrorHasDoc (e :: Type) where   -- | Name of error as it appears in the corresponding section title.@@ -367,14 +364,12 @@   errorToVal (CustomError _ arg) cont =     cont $ toVal @(CustomErrorRep tag) arg -  errorFromVal (v :: Value t) =+  errorFromVal v = do     let expectedTag = errorTagToMText (fromLabel @tag)-    in case cast v of-        Just v' -> do-          errArg <- verifyErrorTag @(CustomErrorRep tag) expectedTag+    v' <- castM v \vType _ -> Left $ "Wrong type for custom error: " <> pretty vType+    errArg <- verifyErrorTag @(CustomErrorRep tag) expectedTag             $ fromVal @(CustomErrorRep tag) v'-          pure $ CustomError fromLabel errArg-        Nothing -> Left $ "Wrong type for custom error: " <> pretty (demote @t)+    pure $ CustomError fromLabel errArg  instance ( CustomErrorHasDoc tag          , IsCustomErrorArgRep (CustomErrorRep tag)@@ -429,7 +424,7 @@   type MustHaveErrorArg errorTag expectedArgRep =-  ( TypeErrorUnless (CustomErrorRep errorTag == expectedArgRep)+  ( AssertTypesEqual (CustomErrorRep errorTag) expectedArgRep       ('Text "Error argument type is "         ':<>: 'ShowType (expectedArgRep)         ':<>: 'Text " but given error requires argument of type "@@ -464,7 +459,7 @@ -- that this is unit-arg error and interpret the passed value as complete. instance ( Typeable arg          , IsError (CustomError tag)-         , TypeErrorUnless (arg == ()) notVoidError+         , AssertTypesEqual arg () notVoidError          , arg ~ ErrorArg tag          , notVoidError ~             ('Text "This error requires argument of type "

@@ -34,6 +34,7 @@ import qualified Data.Bimap as Bimap import Data.Default (def) import qualified Data.HashSet as HS+import Data.Singletons (withSingI) import Fmt (pretty)  import Lorentz.Base@@ -140,7 +141,7 @@       { dsGoToValues = True       } -    tagToNatValue :: HasCallStack => MText -> SomeConstrainedValue ConstantScope'+    tagToNatValue :: HasCallStack => MText -> SomeConstrainedValue ConstantScope     tagToNatValue tag =       case (HS.member tag exclusions, Bimap.lookupR tag errorTagMap) of         (True, _) -> SomeConstrainedValue (VString tag)@@ -163,7 +164,7 @@ -- map, we conservatively preserve that number (because this whole -- approach is rather a heuristic). errorFromValNumeric ::-  (KnownT t, IsError e) => ErrorTagMap -> Value t -> Either Text e+  (SingI t, IsError e) => ErrorTagMap -> Value t -> Either Text e errorFromValNumeric errorTagMap v =   case v of     VNat tag@@ -172,7 +173,7 @@     (VPair (VNat tag, something) :: Value pair)       | Just textualTag <- Bimap.lookup tag errorTagMap ->         case sing @pair of-          STPair {} ->+          STPair l r -> withSingI l $ withSingI r $             errorFromVal $ VPair (VString textualTag, something)     _ -> errorFromVal v @@ -184,7 +185,7 @@ -- map, we conservatively preserve that string (because this whole -- approach is rather a heuristic). errorToValNumeric ::-  IsError e => ErrorTagMap -> e -> (forall t. ErrorScope t => Value t -> r) -> r+  IsError e => ErrorTagMap -> e -> (forall t. ConstantScope t => Value t -> r) -> r errorToValNumeric errorTagMap e cont =   errorToVal e $ \case     VString textualTag@@ -193,6 +194,6 @@     (VPair (VString textualTag, something) :: Value pair)       | Just tag <- Bimap.lookupR textualTag errorTagMap ->           case sing @pair of-            STPair {} ->-              cont (VPair (VNat tag, something))+            STPair l r ->+              withSingI l $ withSingI r $ cont (VPair (VNat tag, something))     v -> cont v

@@ -0,0 +1,269 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# OPTIONS_GHC -Wno-orphans #-}++{- | Evaluation of expressions.++Stack-based languages allow convenient expressions evaluation, for that+we just need binary instructions in infix notation, not in Polish postfix+notation that 'add' and other primitives provide. Compare:++>>> push 1; push 2; push 3; push 4; mul; rsub; add++vs++>>> push 1 |+| push 2 |-| push 3 |*| push 4++In these expressions each atom is some instruction providing a single value+on top of the stack, for example:++@+nthOdd :: Lambda Natural Natural+nthOdd = take |*| push @Natural 2 |+| push @Natural 1+@++For binary operations we provide the respective operators. Unary operations can+be lifted with 'unaryExpr':++@+implication :: [Bool, Bool] :-> '[Bool]+implication = unaryExpr not take |.|.| take+@++or with its alias in form of an operator:++@+implication :: [Bool, Bool] :-> '[Bool]+implication = not $: take |.|.| take+@++Stack changes are propagated from left to right. If an atom consumes an element+at the top of the stack, the next atom will accept only the remainder of the+stack.++In most cases you should prefer providing named variables to the formulas in+order to avoid messing up with the arguments:++@+f :: ("a" :! Natural) : ("b" :! Natural) : ("c" :! Natural) : s :-> Integer : s+f = fromNamed #a |+| fromNamed #b |-| fromNamed #c+@++Instead of putting all the elements on the stack upon applying the formula,+you may find it more convenient to evaluate most of the arguments right within+the formula:++@+withinRange+  :: Natural : a : b : c : ("config" :! Config) : s+  :-> Bool : a : b : c : ("config" :! Config) : s+withinRange =+  dup  |>=| do{ dupL #config; toField #minBound } |&|+  take |<=| do{ dupL #config; toField #maxBound }+@++-}+module Lorentz.Expr+  ( Expr+  , take+  , unaryExpr+  , ($:)+  , binaryExpr+  , (|+|)+  , (|-|)+  , (|*|)+  , (|==|)+  , (|/=|)+  , (|<|)+  , (|>|)+  , (|<=|)+  , (|>=|)+  , (|&|)+  , (|||)+  , (|.|.|)+  , (|^|)+  , (|<<|)+  , (|>>|)+  , (|:|)+  , (|@|)+  , listE+  ) where++import Prelude (foldr)++import Lorentz.Arith+import Lorentz.Base+import Lorentz.Constraints+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Rebinded+import Lorentz.Value+import Michelson.Typed.Arith++-- | Expression is just an instruction accepting stack @inp@ and producing+-- stack @out@ with evaluation result @res@ at the top.++-- Stack flows from left to right, so e.g. @ fromNamed #a |<| fromNamed #b @+-- consumes first the value with label @a@ from the stack's top, then the value+-- with label @b@.+type Expr inp out res = inp :-> res : out++{- Note on the type alias ↑++It was pretty difficult to decide whether 'Expr' should be a newtype or type+alias.++Pros of newtype:+* It is safer and clearer.+* It allows defining such 'IsLabel name (Expr ...)' instance that would allow+  writing @ #a |<| #b @ (which should consume values asserting their labels).++It would /not/ allow writing @5 :: Expr ... Natural@, because this way we lose+GHC checks on passing out-of-bounds numbers like @(-1) :: Natural@.++Cons:+* Any non-trivial operation like @push@, @dupL@ and others will require a+  wrapper.++To make all this as simple to use and understand as possible, we used a+type alias.+-}++-- | An expression producing 'Bool' can be placed as condition to 'if'.+instance (i ~ arg, o ~ argl, o ~ argr, r ~ Bool, outb ~ out) =>+         IsCondition (Expr i o r) arg argl argr outb out where+  ifThenElse e l r = e # if_ l r++-- | Consume an element at the top of stack. This is just an alias for @nop@.+take :: Expr (a : s) s a+take = nop++-- | Lift an instruction to an unary operation on expressions.+unaryExpr+  :: (forall s. a : s :-> r : s)+  -> Expr s0 s1 a -> Expr s0 s1 r+unaryExpr op a = a # op++-- | An alias for 'unaryExpr'.+infixr 9 $:+($:)+  :: (forall s. a : s :-> r : s)+  -> Expr s0 s1 a -> Expr s0 s1 r+($:) = unaryExpr++-- | Lift an instruction to a binary operation on expressions.+binaryExpr+  :: (forall s. a : b : s :-> r : s)+  -> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r+binaryExpr op l r = l # dip r # op++-- | Expressions addition.+infixl 6 |+|+(|+|)+  :: (ArithOpHs Add a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)+(|+|) = binaryExpr add++-- | Expressions subtraction.+infixl 6 |-|+(|-|)+  :: (ArithOpHs Sub a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)+(|-|) = binaryExpr sub++-- | Expressions multiplication.+infixl 7 |*|+(|*|)+  :: (ArithOpHs Mul a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)+(|*|) = binaryExpr mul++-- | Expressions comparison.+infix 4 |==|+infix 4 |/=|+infix 4 |<|+infix 4 |>|+infix 4 |<=|+infix 4 |>=|+(|==|), (|/=|), (|<|), (|>|), (|>=|), (|<=|)+  :: (NiceComparable a)+  => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool+(|==|) = binaryExpr eq+(|/=|) = binaryExpr neq+(|<|) = binaryExpr lt+(|>|) = binaryExpr gt+(|<=|) = binaryExpr le+(|>=|) = binaryExpr ge++-- | Bitwise/logical @AND@ on expressions.+infixl 2 |&|+(|&|)+  :: (ArithOpHs And a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)+(|&|) = binaryExpr and++-- | Bitwise/logical @OR@ on expressions.+--+-- In case you find this operator looking weird, see '|.|.|'+infixl 1 |||+(|||)+  :: (ArithOpHs Or a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)+(|||) = binaryExpr or++-- | An alias for '|||'.+infixl 1 |.|.|+(|.|.|)+  :: (ArithOpHs Or a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)+(|.|.|) = binaryExpr or++-- | Bitwise/logical @XOR@ on expressions.+infixl 3 |^|+(|^|)+  :: (ArithOpHs Xor a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)+(|^|) = binaryExpr xor++-- | Left shift on expressions.+infix 8 |<<|+(|<<|)+  :: (ArithOpHs Lsl a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)+(|<<|) = binaryExpr lsl++-- | Right shift on expressions.+infix 8 |>>|+(|>>|)+  :: (ArithOpHs Lsr a b)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)+(|>>|) = binaryExpr lsr++-- | 'cons' on expressions.+--+-- @+-- one :: a : s :-> [a] : s+-- one = take |:| nil+-- @+infix 1 |:|+(|:|) :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]+(|:|) = binaryExpr cons++-- | Construct a simple pair.+--+-- @+-- trivialContract :: ((), storage) :-> ([Operation], Storage)+-- trivialContract = nil |@| cdr+-- @+--+-- This is useful as pair appears even in simple contracts.+-- For more advanced types, use 'Lorentz.ADT.constructT'.+infix 0 |@|+(|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)+(|@|) = binaryExpr pair++-- | Construct a list given the constructor for each element.+listE :: KnownValue a => [Expr s s a] -> Expr s s [a]+listE = foldr (\pushElem pushRec -> pushElem # dip pushRec # cons) nil

@@ -27,7 +27,7 @@ -- <includes the top of the stack> stackRef   :: forall (gn :: Nat) st n.-      (n ~ ToPeano gn, SingI n, KnownPeano n, RequireLongerThan st n)+      (n ~ ToPeano gn, SingI n, RequireLongerThan st n)   => PrintComment st stackRef = PrintComment . one . Right $ mkStackRef @gn @@ -42,7 +42,7 @@ -- -- This won't be included into production contract and is executed only in tests. testAssert-  :: (Typeable (ToTs out), HasCallStack)+  :: (SingI (ToTs out), HasCallStack)   => Text -> PrintComment (ToTs inp) -> inp :-> Bool : out -> inp :-> inp testAssert msg comment = \case   I instr -> I . Ext . TEST_ASSERT $ TestAssert msg comment instr

@@ -31,6 +31,7 @@   , pair   , car   , cdr+  , unpair   , left   , right   , ifLeft@@ -48,6 +49,7 @@   , PairGetHs   , pairGet   , update+  , getAndUpdate   , ConstraintPairUpdateLorentz   , PairUpdateHs   , pairUpdate@@ -95,7 +97,7 @@   , selfCalling   , contract   , contractCalling-  , contractCallingUnsafe+  , unsafeContractCalling   , runFutureContract   , epAddressToContract   , transferTokens@@ -119,6 +121,11 @@   , sender   , address   , selfAddress+  , ticket+  , ReadTicket+  , readTicket+  , splitTicket+  , joinTickets   , chainId   , level   , never@@ -131,7 +138,6 @@   (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)  import Data.Constraint ((\\))-import Data.Singletons (SingI, sing) import qualified GHC.TypeNats as GHC (Nat)  import Lorentz.Address@@ -141,17 +147,18 @@ import Lorentz.Constraints import Lorentz.Entrypoints import Lorentz.Polymorphic-import Lorentz.Run (Contract, compileLorentzContract) import Lorentz.Value import Lorentz.Zip import Michelson.Typed   (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,   ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,-  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), RemFail(..), SomeEntrypointCallT(..), UpdateN,-  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, sepcName, starNotes)+  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), SingI, RemFail(..), SomeEntrypointCallT(..), UpdateN,+  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR,+  sepcName, starNotes) import Michelson.Typed.Arith import Michelson.Typed.Haskell.Value import Util.Peano+import Util.PeanoNatural import Util.Type  nop :: s :-> s@@ -184,35 +191,51 @@   forall (n :: GHC.Nat) (s :: [Type]).   -- Note: if we introduce `nPeano ~ ToPeano n` variable,   -- GHC will complain that this constraint is redundant.-  ( SingI (ToPeano n), KnownPeano (ToPeano n)+  ( SingI (ToPeano n)   , RequireLongerOrSameLength (ToTs s) (ToPeano n)   -- ↓ Kinda obvious, but not to GHC.   , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)   ) => s :-> Drop (ToPeano n) s-dropN = I (DROPN $ peanoSing @n)+dropN = I $ DROPN $ toPeanoNatural' @n   where     _example :: '[ Integer, Integer, Integer ] :-> '[]     _example = dropN @3 -dup :: a : s :-> a : a : s-dup = I DUP+-- | Copies a stack argument.+--+-- Hit the 'Dupable' constraint?+-- Polymorphism and abstractions do not play very well with this constraint,+-- you can enjoy suffering from the linear types feature under various sauces:+--+-- 1. The most trivial option is to just propagate 'Dupable' constraint when you+--    want to use 'dup', this suits for case when you are not planning to work+--    with non-dupable types like tickets.+-- 2. Sometimes it is possible to avoid 'dup' and use other instructions instead+--    (e.g. 'unpair' allows splitting a pair without using 'dup's,+--     'getAndUpdate' allows accessing a map value without implicit duplication).+--    But you may have to learn to write code in a completely different way,+--    and the result may be less efficient comparing to the option with using+--    @dup@.+-- 3. Use 'decideOnDupable' to provide two code paths - when type is dupable+--    and when it is not.+dup :: forall a s. Dupable a => a : s :-> a : a : s+dup = I DUP \\ dupableEvi @a  type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])   (a :: Type) =   ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)   , ConstraintDUPN' Type n inp out a+  , SingI n   )  dupNPeano ::-  forall (n :: Peano) inp out a.-  ( ConstraintDUPNLorentz n inp out a-  ) => inp :-> out-dupNPeano = I (DUPN (sing @n))+  forall (n :: Peano) a inp out.+  ( ConstraintDUPNLorentz n inp out a, Dupable a ) => inp :-> out+dupNPeano = (I $ DUPN $ toPeanoNatural @n) \\ dupableEvi @a  dupN ::-  forall (n :: GHC.Nat) inp out a.-  ( ConstraintDUPNLorentz (ToPeano n) inp out a-  ) => inp :-> out+  forall (n :: GHC.Nat) a inp out.+  ( ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a ) => inp :-> out dupN = dupNPeano @(ToPeano n)   where     _example :: '[ Integer, (), Bool ] :-> '[ Bool, Integer, (), Bool ]@@ -226,12 +249,14 @@   (a :: Type) =   ( ConstraintDIG n (ToTs inp) (ToTs out) (ToT a)   , ConstraintDIG' Type n inp out a+  , SingI n   )  type ConstraintDUGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])   (a :: Type) =   ( ConstraintDUG n (ToTs inp) (ToTs out) (ToT a)   , ConstraintDUG' Type n inp out a+  , SingI n   )  -- | Version of `dig` which uses Peano number.@@ -240,7 +265,7 @@   forall (n :: Peano) inp out a.   ( ConstraintDIGLorentz n inp out a   ) => inp :-> out-digPeano = I (DIG $ sing @n)+digPeano = I $ DIG $ toPeanoNatural @n  dig ::   forall (n :: GHC.Nat) inp out a.@@ -259,7 +284,7 @@   forall (n :: Peano) inp out a.   ( ConstraintDUGLorentz n inp out a   ) => inp :-> out-dugPeano = I (DUG $ sing @n)+dugPeano = I $ DUG $ toPeanoNatural @n  dug ::   forall (n :: GHC.Nat) inp out a.@@ -297,6 +322,9 @@ cdr :: (a, b) : s :-> b : s cdr = I CDR +unpair :: (a, b) : s :-> a : b : s+unpair = I UNPAIR+ left :: forall a b s. KnownValue b => a : s :-> Either a b : s left = I LEFT @@ -327,7 +355,7 @@          => s :-> Map k v : s emptyMap = I EMPTY_MAP -emptyBigMap :: (NiceComparable k, KnownValue v)+emptyBigMap :: (NiceComparable k, KnownValue v, NiceNoBigMap v)             => s :-> BigMap k v : s emptyBigMap = I EMPTY_BIG_MAP @@ -352,6 +380,7 @@ type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Type) =   ( ConstraintGetN (ToPeano n) (ToT pair)   , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)+  , SingI (ToPeano n)   )  type family PairGetHs (ix :: Peano) (pair :: Type) :: Type where@@ -363,7 +392,7 @@   :: forall (n :: GHC.Nat) (pair :: Type) (s :: [Type]).      ConstraintPairGetLorentz n pair   => pair : s :-> PairGetHs (ToPeano n) pair : s-pairGet = I (GETN (peanoSing @n))+pairGet = I $ GETN $ toPeanoNatural' @n   where     _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]     _example = pairGet @1@@ -371,9 +400,15 @@ update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s update = I UPDATE +getAndUpdate+  :: (GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c), UpdOpKeyHs c ~ GetOpKeyHs c)+  => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> Maybe (GetOpValHs c) : c : s+getAndUpdate = I GET_AND_UPDATE+ type ConstraintPairUpdateLorentz (n :: GHC.Nat) (val :: Type) (pair :: Type) =   ( ConstraintUpdateN (ToPeano n) (ToT pair)   , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)+  , SingI (ToPeano n)   )  type family PairUpdateHs (ix :: Peano) (val :: Type) (pair :: Type) :: Type where@@ -383,9 +418,9 @@  pairUpdate   :: forall (n :: GHC.Nat) (val :: Type) (pair :: Type) (s :: [Type]).-     ConstraintPairUpdateLorentz n val pair+     (ConstraintPairUpdateLorentz n val pair)   => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s-pairUpdate = I (UPDATEN (peanoSing @n))+pairUpdate = I $ UPDATEN $ toPeanoNatural' @n   where     _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]     _example = pairUpdate @1@@ -456,6 +491,7 @@   (s :: [Type]) (s' :: [Type]) =   ( ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s')   , ConstraintDIPN' Type n inp out s s'+  , SingI n   )  -- | Version of `dipN` which uses Peano number.@@ -464,7 +500,7 @@   forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).   ( ConstraintDIPNLorentz n inp out s s'   ) => s :-> s' -> inp :-> out-dipNPeano (iNonFailingCode -> a) = I (DIPN (sing @n) a)+dipNPeano (iNonFailingCode -> a) = I (DIPN (toPeanoNatural @n) a)  dipN ::   forall (n :: GHC.Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).@@ -671,12 +707,12 @@ -- For instance, if you have untyped 'EpName' you can not have this -- evidence (the value is only available in runtime). -- If you have typed 'EntrypointRef', use 'eprName' to construct 'EpName'.-contractCallingUnsafe+unsafeContractCalling   :: forall arg s.      (NiceParameter arg)   => EpName   -> Address : s :-> Maybe (ContractRef arg) : s-contractCallingUnsafe epName = contractCalling (TrustEpName epName)+unsafeContractCalling epName = contractCalling (TrustEpName epName)  -- | Version of 'contract' instruction which may accept address with already -- specified entrypoint name.@@ -707,12 +743,11 @@ setDelegate = I SET_DELEGATE  createContract-  :: forall p g s. (NiceStorage g, NiceParameterFull p)-  => Contract p g+  :: forall p g s. Contract p g   -> Maybe KeyHash : Mutez : g : s   :-> Operation : Address : s-createContract cntrc =-  I $ CREATE_CONTRACT (compileLorentzContract cntrc)+createContract cntrc@Contract{} =+  I $ CREATE_CONTRACT (toMichelsonContract cntrc)     \\ niceParameterEvi @p     \\ niceStorageEvi @g @@ -782,6 +817,18 @@ never :: Never : s :-> s' never = FI NEVER +ticket :: (NiceComparable a) => a : Natural : s :-> Ticket a : s+ticket = I TICKET++readTicket :: Ticket a : s :-> ReadTicket a : Ticket a : s+readTicket = I READ_TICKET++splitTicket :: Ticket a : (Natural, Natural) : s :-> Maybe (Ticket a, Ticket a) : s+splitTicket = I SPLIT_TICKET++joinTickets :: (Ticket a, Ticket a) : s :-> Maybe (Ticket a) : s+joinTickets = I JOIN_TICKETS+ -- | Execute given instruction on truncated stack. -- -- This instruction requires you to specify the piece of stack to truncate@@ -809,6 +856,7 @@   :: forall c k s v st e.      ( MemOpHs c, k ~ MemOpKeyHs c      , NiceConstant e+     , Dupable c, Dupable (MemOpKeyHs c)      , st ~ (k : v : c : s)      )   => (forall s0. k : s0 :-> e : s0)@@ -820,12 +868,13 @@ -- | Like 'update', but throw an error on attempt to overwrite existing entry. updateNew   :: forall c k s e.-     ( UpdOpHs c, MemOpHs c, k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c-     , NiceConstant e+     ( UpdOpHs c, MemOpHs c, GetOpHs c+     , k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c, k ~ GetOpKeyHs c+     , KnownValue (GetOpValHs c), NiceConstant e, Dupable k      )   => (forall s0. k : s0 :-> e : s0)   -> k : UpdOpParamsHs c : c : s :-> c : s-updateNew mkErr = failingWhenPresent mkErr # update+updateNew mkErr = dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith)  class LorentzFunctor (c :: Type -> Type) where   lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)

@@ -128,7 +128,6 @@  import Prelude hiding (and, compare, drop, some, swap) -import Data.Singletons (SingI(..)) import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+)) import Fmt.Internal.Tuple (TupleF) import qualified GHC.TypeLits as Lit@@ -149,6 +148,7 @@ import Michelson.Typed (ConstraintDIPN', ConstraintDUG', T) import Michelson.Typed.Arith import Michelson.Typed.Haskell.Value+import Michelson.Typed.Scope import Util.Markdown import Util.Peano import Util.Type@@ -182,7 +182,7 @@ lt = compare # lt0  type IfCmp0Constraints a op =-  (UnaryArithOpHs op a, (UnaryArithResHs op a ~ Bool), SingI (ToT a))+  (UnaryArithOpHs op a, (UnaryArithResHs op a ~ Bool), KnownIsoT a)  ifEq0   :: (IfCmp0Constraints a Eq')@@ -324,6 +324,7 @@   :: forall (n :: GHC.Nat) a inp out s s'.   ( ConstraintDIPNLorentz (ToPeano n) inp out s s'   , s ~ (a ': s')+  , SingI (ToPeano n)   )   => inp :-> out dropX = dipN @n @inp @out @s @s' drop@@ -334,7 +335,7 @@ instance CloneX 'Z a s where   type CloneXT 'Z a s = a : s   cloneXImpl = nop-instance (CloneX n a s) => CloneX ('S n) a s where+instance (CloneX n a s, Dupable a) => CloneX ('S n) a s where   type CloneXT ('S n) a s = a ': CloneXT n a s   cloneXImpl = dup # dip (cloneXImpl @n) @@ -354,7 +355,8 @@ -- -- > duupX = dupN @n duupX-  :: forall (n :: GHC.Nat) s s' a. ConstraintDUPNLorentz (ToPeano n) s s' a+  :: forall (n :: GHC.Nat) a s s'.+     (ConstraintDUPNLorentz (ToPeano n) s s' a, Dupable a)   => s :-> a ': s duupX = dupN @n @@ -411,9 +413,6 @@ ppaiir :: a : b : c : s :-> (a, (b, c)) : s ppaiir = dip pair # pair -unpair :: (a, b) : s :-> a : b : s-unpair = dup # car # dip cdr- cdar :: (a1, (a2, b)) : s :-> a2 : s cdar = cdr # car @@ -433,14 +432,14 @@ setCdr = car # pair  mapCar-  :: a : s :-> a1 : s+  :: (forall s0. a : s0 :-> a1 : s0)   -> (a, b) : s :-> (a1, b) : s-mapCar op = dup # cdr # dip (car # op) # swap # pair+mapCar op = unpair # op # pair  mapCdr-  :: b : (a, b) : s :-> b1 : (a, b) : s+  :: (forall s0. b : s0 :-> b1 : s0)   -> (a, b) : s :-> (a, b1) : s-mapCdr op = dup # cdr # op # swap # car # pair+mapCdr op = unpair # dip op # pair  ifRight :: (b : s :-> s') -> (a : s :-> s') -> (Either a b : s :-> s') ifRight l r = ifLeft r l@@ -475,7 +474,7 @@   --   -- As first argument accepts container name (for error message).   mapInsertNew-    :: (NiceComparable k, NiceConstant e)+    :: (IsoValue (map k v), NiceComparable k, NiceConstant e, Dupable k, KnownValue v)     => (forall s0. k : s0 :-> e : s0)     -> k : v : map k v : s :-> map k v : s @@ -487,10 +486,12 @@  instance MapInstrs Map where   mapUpdate = update-  mapInsertNew mkErr = failingWhenPresent mkErr # mapInsert+  mapInsertNew mkErr =+    dip some # dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith) instance MapInstrs BigMap where   mapUpdate = update-  mapInsertNew mkErr = failingWhenPresent mkErr # mapInsert+  mapInsertNew mkErr =+    dip some # dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith)  -- | Insert given element into set. --@@ -504,10 +505,12 @@ -- -- As first argument accepts container name. setInsertNew-  :: (NiceComparable e, NiceConstant err)+  :: (NiceConstant err, NiceComparable e, Dupable e, Dupable (Set e))   => (forall s0. e : s0 :-> err : s0)   -> e : Set e : s :-> Set e : s-setInsertNew desc = dip (push True) # failingWhenPresent desc # update+setInsertNew desc =+  dupTop2 # mem #+  if_ (desc # failWith) (dip (push True) # update)  -- | Delete given element from the set. setDelete :: NiceComparable e => e : Set e : s :-> Set e : s@@ -536,7 +539,7 @@ instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => ReplaceN ('S 'Z) s a mid tail where   replaceNImpl = swap # drop -instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail) =>+instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail, SingI n) =>   ReplaceN ('S ('S n)) s a mid tail where   replaceNImpl =     -- 'stackType' helps GHC deduce types@@ -589,7 +592,7 @@ instance {-# OVERLAPPING #-} (s ~ (x ': b ': tail)) => UpdateN ('S ('S 'Z)) s a b mid tail where   updateNImpl instr = swap # dip (framed instr) -instance {-# OVERLAPPABLE #-} (ConstraintUpdateNLorentz ('S ('S n)) s a b mid tail) =>+instance {-# OVERLAPPABLE #-} (ConstraintUpdateNLorentz ('S ('S n)) s a b mid tail, SingI n) =>   UpdateN ('S ('S ('S n))) s a b mid tail where   updateNImpl instr =     -- 'stackType' helps GHC deduce types@@ -630,7 +633,7 @@   } deriving stock (Eq, Show, Generic)     deriving anyclass (HasAnnotation) -deriving anyclass instance (WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (View a r)+deriving anyclass instance (HasNoOpToT r, WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (View a r)  instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View a1 r1) (View a2 r2) @@ -648,18 +651,18 @@   typeDocMichelsonRep =     concreteTypeDocMichelsonRep @(View MText Integer) -instance {-# OVERLAPPABLE #-} (Buildable a, WellTypedIsoValue r) => Buildable (View a r) where+instance {-# OVERLAPPABLE #-} (Buildable a, WellTypedIsoValue r, HasNoOpToT r) => Buildable (View a r) where   build = buildView build -instance {-# OVERLAPPING  #-} (WellTypedIsoValue r) => Buildable (View () r) where+instance {-# OVERLAPPING  #-} (WellTypedIsoValue r, HasNoOpToT r) => Buildable (View () r) where   build = buildView $ const "()" -buildViewTuple :: (WellTypedIsoValue r, TupleF a) => View a r -> Builder+buildViewTuple :: (HasNoOpToT r, WellTypedIsoValue r, TupleF a) => View a r -> Builder buildViewTuple = buildView tupleF -buildView :: (WellTypedIsoValue r) => (a -> Builder) -> View a r -> Builder+buildView :: (WellTypedIsoValue r, HasNoOpToT r) => (a -> Builder) -> View a r -> Builder buildView bfp (View {..}) =-  "(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo|+ ")"+  "(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo |+ ")"  -- | Polymorphic version of 'View' constructor. mkView :: ToContractRef r contract => a -> contract -> View a r@@ -678,7 +681,7 @@ unwrapView = forcedCoerce_  view_ ::-     (NiceParameter r)+     (NiceParameter r, Dupable storage)   => (forall s0. a : storage : s0 :-> r : s0)   -> View a r : storage : s :-> (List Operation, storage) : s view_ code =@@ -752,10 +755,10 @@ instance (TypeHasDoc r, IsError (VoidResult r)) => TypeHasDoc (VoidResult r) where   typeDocMdDescription = typeDocMdDescriptionReferToError @(VoidResult r)   typeDocMdReference = poly1TypeDocMdReference-  typeDocHaskellRep = concreteTypeDocHaskellRepUnsafe @(VoidResultRep Integer)-  typeDocMichelsonRep = concreteTypeDocMichelsonRepUnsafe @(VoidResultRep Integer)+  typeDocHaskellRep = unsafeConcreteTypeDocHaskellRep @(VoidResultRep Integer)+  typeDocMichelsonRep = unsafeConcreteTypeDocMichelsonRep @(VoidResultRep Integer) -instance (Typeable r, NiceConstant r, ErrorHasDoc (VoidResult r)) =>+instance (NiceConstant r, ErrorHasDoc (VoidResult r)) =>          IsError (VoidResult r) where   errorToVal (VoidResult e) cont =     withDict (niceConstantEvi @r) $@@ -833,9 +836,10 @@     runFutureContract # ifNone onContractNotFound (dip drop)  -- | Duplicate two topmost items on top of the stack.-dupTop2 ::-  forall (a :: Type) (b :: Type) (s :: [Type]).-  a ': b ': s :-> a ': b ': a ': b ': s+dupTop2+  :: forall (a :: Type) (b :: Type) (s :: [Type]).+     (Dupable a, Dupable b)+  => a ': b ': s :-> a ': b ': a ': b ': s dupTop2 = dupN @2 # dupN @2  fromOption

@@ -21,11 +21,9 @@ import qualified Michelson.Typed as T  -- | Estimate code operation size.-contractOpSize-  :: (NiceParameterFull cp, NiceStorage st)-  => Contract cp st -> OpSize+contractOpSize :: Contract cp st -> OpSize contractOpSize =-  T.contractOpSize . compileLorentzContract+  T.contractOpSize . toMichelsonContract  {- We do not provide a method for plain lorentz code because it can be    compiled differently (e.g. with optimizations or not).

@@ -21,7 +21,7 @@ import Michelson.Interpret.Pack import Michelson.Interpret.Unpack import Michelson.Typed-import Morley.Micheline (Expression, encodeExpression)+import Morley.Micheline (Expression, encodeExpression') import Tezos.Crypto (blake2b)  lPackValueRaw@@ -55,7 +55,7 @@ lEncodeValue   :: forall a. (NicePrintedValue a)   => a -> ByteString-lEncodeValue = encodeValue' . toVal \\ nicePrintedValueEvi @a+lEncodeValue = toBinary' . toVal \\ nicePrintedValueEvi @a  -- | This function transforms Lorentz values into @script_expr@. --@@ -74,7 +74,7 @@ -- | Similar to 'valueToScriptExpr', but for values encoded as 'Expression's. -- This is only used in tests. expressionToScriptExpr :: Expression -> ByteString-expressionToScriptExpr = addScriptExprPrefix . blake2b . mappend packValuePrefix . encodeExpression+expressionToScriptExpr = addScriptExprPrefix . blake2b . mappend packValuePrefix . encodeExpression'  addScriptExprPrefix :: ByteString -> ByteString addScriptExprPrefix = (BS.pack [0x0D, 0x2C, 0x40, 0x1B] <>)

@@ -26,8 +26,6 @@  -- | Pretty-print a Lorentz contract into Michelson code. printLorentzContract-  :: forall cp st.-     (NiceParameterFull cp, NiceStorage st)-  => Bool -> Contract cp st -> LText+  :: Bool -> Contract cp st -> LText printLorentzContract forceSingleLine =-  printTypedContract forceSingleLine . compileLorentzContract+  printTypedContract forceSingleLine . toMichelsonContract

@@ -14,7 +14,7 @@   ( (>>)   , pure   , return-  , ifThenElse+  , IsCondition (ifThenElse)   , Condition (..)   , (<.)   , (>.)@@ -32,13 +32,14 @@   ) where  -import Prelude hiding (drop, swap, (>>), (>>=))+import Prelude hiding (drop, not, swap, (>>), (>>=))  import Named ((:!))  import Lorentz.Arith import Lorentz.Base import Lorentz.Coercions+import Lorentz.Constraints.Scopes import Lorentz.Instr import Lorentz.Macro import Michelson.Typed.Arith@@ -48,7 +49,7 @@ (>>) :: (a :-> b) -> (b :-> c) -> (a :-> c) (>>) = (#) --- | Predicate for @if ... then .. else ...@ construction,+-- | The most basic predicate for @if ... then .. else ...@ construction, -- defines a kind of operation applied to the top elements of the current stack. -- -- Type arguments mean:@@ -66,6 +67,8 @@   IsCons :: Condition ([a] ': s) (a ': [a] ': s) s o o   IsNil :: Condition ([a] ': s) s (a ': [a] ': s) o o +  Not :: Condition s s1 s2 ob o -> Condition s s2 s1 ob o+   IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)          => Condition (a ': s) s s o o   IsNotZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)@@ -87,44 +90,56 @@    -- | Provide the compared arguments to @if@ branches.   PreserveArgsBinCondition ::+    (Dupable a, Dupable b) =>     (forall st o. Condition (a ': b ': st) st st o o) ->     Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s --- | Defines semantics of @if ... then ... else ...@ construction.-ifThenElse-  :: Condition arg argl argr outb out-  -> (argl :-> outb) -> (argr :-> outb) -> (arg :-> out)-ifThenElse = \case-  Holds -> if_-  IsSome -> flip ifNone-  IsNone -> ifNone-  IsLeft -> ifLeft-  IsRight -> flip ifLeft-  IsCons -> ifCons-  IsNil -> flip ifCons+-- | Everything that can be put after @if@ keyword.+--+-- The first type argument stands for the condition type, and all other type+-- arguments define stack types around/within the @if then else@ construction.+-- For semantics of each type argument see 'Condition'.+class IsCondition cond arg argl argr outb out where+  -- | Defines semantics of @if ... then ... else ...@ construction.+  ifThenElse :: cond -> (argl :-> outb) -> (argr :-> outb) -> (arg :-> out) -  IsZero -> \l r -> eq0 # if_ l r-  IsNotZero -> \l r -> eq0 # if_ r l+instance (arg ~ arg0, argl ~ argl0, argr ~ argr0, outb ~ outb0, out ~ out0) =>+         IsCondition (Condition arg argl argr outb out) arg0 argl0 argr0 outb0 out0 where+  ifThenElse = \case+    Holds -> if_+    IsSome -> flip ifNone+    IsNone -> ifNone+    IsLeft -> ifLeft+    IsRight -> flip ifLeft+    IsCons -> ifCons+    IsNil -> flip ifCons -  IsEq -> ifEq-  IsNeq -> ifNeq-  IsLt -> ifLt-  IsGt -> ifGt-  IsLe -> ifLe-  IsGe -> ifGe+    Not cond -> \l r -> ifThenElse cond r l -  NamedBinCondition condition l1 l2 -> \l r ->-    fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r+    IsZero -> \l r -> eq0 # if_ l r+    IsNotZero -> \l r -> eq0 # if_ r l -  PreserveArgsBinCondition condition -> \l r ->-    dupN @2 # dupN @2 #-    ifThenElse condition-      -- since this pattern is commonly used when one of the branches fails,-      -- it's essential to @drop@ within branches, not after @if@ - @drop@s-      -- appearing to be dead code will be cut off-      (l # drop # drop)-      (r # drop # drop)+    IsEq -> ifEq+    IsNeq -> ifNeq+    IsLt -> ifLt+    IsGt -> ifGt+    IsLe -> ifLe+    IsGe -> ifGe +    NamedBinCondition condition l1 l2 -> \l r ->+      fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r++    PreserveArgsBinCondition condition -> \l r ->+      dupN @2 # dupN @2 #+      ifThenElse condition+        -- since this pattern is commonly used when one of the branches fails,+        -- it's essential to @drop@ within branches, not after @if@ - @drop@s+        -- appearing to be dead code will be cut off+        (l # drop # drop)+        (r # drop # drop)++{-# DEPRECATED IsNotZero "Use `Not IsZero` instead" #-}+ -- | Named version of 'IsLt'. -- -- In this and similar operators you provide names of accepted stack operands as@@ -179,6 +194,7 @@ -- | Condition modifier, makes stack operands of binary comparison to be -- available within @if@ branches. keepIfArgs-  :: (forall st o. Condition (a ': b ': st) st st o o)+  :: (Dupable a, Dupable b)+  => (forall st o. Condition (a ': b ': st) st st o o)   -> Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s keepIfArgs = PreserveArgsBinCondition

@@ -28,7 +28,9 @@ import GHC.TypeLits (ErrorMessage(..), TypeError)  import Lorentz.Base+import Lorentz.Constraints import Lorentz.Instr+import Lorentz.Value import Util.Type  -- Errors@@ -56,9 +58,11 @@   dupTImpl = error "impossible"  instance {-# OVERLAPPING #-}-         If (a `IsElem` st)+         ( If (a `IsElem` st)             (TypeError (StackElemAmbiguous origSt a))-            (() :: Constraint) =>+            (() :: Constraint)+         , Dupable a+         ) =>          DupT origSt a (a : st) where   dupTImpl = dup @@ -73,8 +77,8 @@ dupT :: forall a st. DupT st a st => st :-> a : st dupT = dupTImpl @st @a @st -_dupSample1 :: [Integer, Text, ()] :-> [Text, Integer, Text, ()]-_dupSample1 = dupT @Text+_dupSample1 :: [Integer, MText, ()] :-> [MText, Integer, MText, ()]+_dupSample1 = dupT @MText  -- Dip ----------------------------------------------------------------------------

@@ -29,6 +29,7 @@ import Lorentz.ADT import Lorentz.Base import Lorentz.Coercions+import Lorentz.Constraints import Lorentz.Instr import Michelson.Text import Michelson.Typed@@ -111,7 +112,7 @@   varPosition :: VarPosition s name var  type ConstraintVarPosition s n =-  ( SingI n, KnownPeano n, n > 'Z ~ 'True+  ( SingI n, n > 'Z ~ 'True   , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n   ) @@ -162,30 +163,30 @@ -- -- @heitor.toledo: GHC doesn't seem to enjoy it that we use 'ConstraintDUPNLorentz', -- so I replaced it with the expanded definition.-dupLUnsafe+unsafeDupL   :: forall n s var.-     (ConstraintVarPosition s n)+     (ConstraintVarPosition s n, Dupable var)   => Sing (n :: Nat) -> s :-> var : s-dupLUnsafe _ =+unsafeDupL _ =   dupNPeano @n-    \\ provideConstraintUnsafe @(Take (Decrement n) s ++ (var : Drop n s) ~ s)-    \\ provideConstraintUnsafe @(Take (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s)+    \\ unsafeProvideConstraint @(Take (Decrement n) s ++ (var : Drop n s) ~ s)+    \\ unsafeProvideConstraint @(Take (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s)  -- | Version of 'dupL' that leaves a named variable on stack. dupLNamed   :: forall var name s.-     (HasNamedVar s name var)+     (HasNamedVar s name var, Dupable var)   => Label name -> s :-> (name :! var) : s-dupLNamed _ =+dupLNamed Label{} =   case varPosition @s @name @var of-    VarPosition sn -> dupLUnsafe sn+    VarPosition sn -> unsafeDupL 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. dupL :: forall var name s.-        (HasNamedVar s name var)+        (HasNamedVar s name var, Dupable var)      => Label name -> s :-> var : s dupL l = dupLNamed l # fromNamed l 

@@ -2,8 +2,30 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{- | Lorentz contracts compilation.++Compilation in one scheme:++@+                    mkContract+                  mkContractWith+  ContractCode  -----------------→  Contract+ (Lorentz code)              (ready compiled contract)+        ↓                                ↑+        ↓                                ↑+defaultContractData            compileLorentzContract+   ContractData                          ↑+        ↓         ContractData           ↑+       (Lorentz code + compilation options)+@++-} module Lorentz.Run-  ( CompilationOptions(..)+  ( Contract(..)+  , toMichelsonContract+  , defaultContract++  , CompilationOptions(..)   , defaultCompilationOptions   , intactCompilationOptions   , coBytesTransformerL@@ -13,12 +35,15 @@   , compileLorentz   , compileLorentzWithOptions -  , Contract(..)-  , defaultContract+  , mkContract+  , mkContractWith++  , ContractData(..)+  , defaultContractData   , compileLorentzContract-  , cCodeL-  , cDisableInitialCastL-  , cCompilationOptionsL+  , cdCodeL+  , coDisableInitialCastL+  , cdCompilationOptionsL    , interpretLorentzInstr   , interpretLorentzLambda@@ -26,6 +51,7 @@   , analyzeLorentz   ) where +import Control.Lens.Type as Lens (Lens, Lens') import Data.Constraint ((\\)) import Data.Default (def) import Data.Vinyl.Core (Rec(..))@@ -40,7 +66,7 @@ import Michelson.Interpret import Michelson.Optimizer (OptimizerConf, optimizeWithConf) import Michelson.Text (MText)-import Michelson.Typed (Instr(..), IsoValue, IsoValuesStack(..), ToT, ToTs, starParamNotes)+import Michelson.Typed (Instr(..), IsoValue, IsoValuesStack(..), ToTs, starParamNotes) import qualified Michelson.Typed as M (Contract(..)) import qualified Michelson.Untyped as U (canonicalEntriesOrder) import Util.Lens@@ -53,6 +79,12 @@   -- ^ Function to transform strings with. See 'transformStringsLorentz'.   , coBytesTransformer :: (Bool, ByteString -> ByteString)   -- ^ Function to transform byte strings with. See 'transformBytesLorentz'.+  , coDisableInitialCast :: Bool+  -- ^ Flag which defines whether compiled Michelson contract+  -- will have @CAST@ (which drops parameter annotations)+  -- as a first instruction. Note that when+  -- flag is false, there still may be no @CAST@ (in case+  -- when parameter type has no annotations).   }  -- | Runs Michelson optimizer with default config and does not touch strings and bytes.@@ -61,6 +93,7 @@   { coOptimizerConf = Just def   , coStringTransformer = (False, id)   , coBytesTransformer = (False, id)+  , coDisableInitialCast = False   }  -- | Leave contract without any modifications. For testing purposes.@@ -69,6 +102,7 @@   { coOptimizerConf = Nothing   , coStringTransformer = (False, id)   , coBytesTransformer = (False, id)+  , coDisableInitialCast = False   }  -- | For use outside of Lorentz. Will use 'defaultCompilationOptions'.@@ -83,6 +117,31 @@   . uncurry transformStringsLorentz coStringTransformer   . uncurry transformBytesLorentz coBytesTransformer +-- | Construct and compile Lorentz contract.+--+-- This is an alias for 'mkContract'.+defaultContract+  :: (NiceParameterFull cp, NiceStorage st)+  => ContractCode cp st -> Contract cp st+defaultContract code =+  compileLorentzContract $ ContractData code defaultCompilationOptions++-- | Construct and compile Lorentz contract.+--+-- Note that this accepts code with initial and final stacks unpaired for+-- simplicity.+mkContract+  :: (NiceParameterFull cp, NiceStorage st)+  => ContractCode cp st -> Contract cp st+mkContract = mkContractWith defaultCompilationOptions++-- | Version of 'mkContract' that accepts custom compilation options.+mkContractWith+  :: (NiceParameterFull cp, NiceStorage st)+  => CompilationOptions -> ContractCode cp st -> Contract cp st+mkContractWith opts code =+  compileLorentzContract $ ContractData code opts+ -- | Code for a contract along with compilation options for the Lorentz compiler. -- -- It is expected that a 'Contract' is one packaged entity, wholly controlled by its author.@@ -92,27 +151,20 @@ -- environments, like production and testing. -- -- Raw 'ContractCode' should not be used for distribution of contracts.-data Contract cp st = Contract-  { cCode :: ContractCode cp st-    -- ^ The contract itself.-  , cDisableInitialCast :: Bool-  -- ^ Flag which defines whether compiled Michelson contract-  -- will have @CAST@ (which drops parameter annotations)-  -- as a first instruction. Note that when-  -- flag is false, there still may be no @CAST@ (in case-  -- when parameter type has no annotations).-  , cCompilationOptions :: CompilationOptions+data ContractData cp st = (NiceParameterFull cp, NiceStorage st) => ContractData+  { cdCode :: ContractCode cp st+  -- ^ The contract itself.+  , cdCompilationOptions :: CompilationOptions   -- ^ General compilation options for the Lorentz compiler.   } --- | Compile contract with 'defaultCompilationOptions' and 'cDisableInitialCast' set to @False@.-defaultContract-  :: forall cp st. (NiceParameterFull cp, HasCallStack)-  => ContractCode cp st -> Contract cp st-defaultContract code = Contract-  { cCode = finalizeParamCallingDoc' (Proxy @cp) code-  , cDisableInitialCast = False-  , cCompilationOptions = defaultCompilationOptions+-- | Compile contract with 'defaultCompilationOptions'.+defaultContractData+  :: forall cp st. (NiceParameterFull cp, NiceStorage st)+  => ContractCode cp st -> ContractData cp st+defaultContractData code = ContractData+  { cdCode = code+  , cdCompilationOptions = defaultCompilationOptions   }  -- | Compile a whole contract to Michelson.@@ -122,22 +174,23 @@ -- is @True@, resulted contract can be ill-typed). -- However, compilation with 'defaultContractCompilationOptions' should be valid. compileLorentzContract-  :: forall cp st.-     (NiceParameterFull cp, NiceStorage st)-  => Contract cp st -> M.Contract (ToT cp) (ToT st)-compileLorentzContract Contract{..} =-  M.Contract-  { cCode = if (cpNotes == starParamNotes || cDisableInitialCast)-      then -- If contract parameter type has no annotations or explicitly asked, we drop CAST.-        compileLorentzWithOptions cCompilationOptions cCode-      else -- Perform CAST otherwise.-        compileLorentzWithOptions cCompilationOptions (I CAST # cCode :: ContractCode cp st)-  , cParamNotes = cpNotes-  , cStoreNotes = getAnnotation @st NotFollowEntrypoint-  , cEntriesOrder = U.canonicalEntriesOrder-  } \\ niceParameterEvi @cp-    \\ niceStorageEvi @st+  :: forall cp st. ContractData cp st -> Contract cp st+compileLorentzContract ContractData{..} = Contract{..}   where+    cMichelsonContract = M.Contract+      { cCode = if (cpNotes == starParamNotes || coDisableInitialCast cdCompilationOptions)+          then -- If contract parameter type has no annotations or explicitly asked, we drop CAST.+            compileLorentzWithOptions cdCompilationOptions cdCode+          else -- Perform CAST otherwise.+            compileLorentzWithOptions cdCompilationOptions (I CAST # cdCode :: ContractCode cp st)+      , cParamNotes = cpNotes+      , cStoreNotes = getAnnotation @st NotFollowEntrypoint+      , cEntriesOrder = U.canonicalEntriesOrder+      } \\ niceParameterEvi @cp+        \\ niceStorageEvi @st++    cDocumentedCode = finalizeParamCallingDoc' (Proxy @cp) cdCode+     cpNotes = parameterEntrypointsToNotes @cp  -- | Interpret a Lorentz instruction, for test purposes. Note that this does not run the@@ -164,16 +217,27 @@   let Identity out :& RNil = res   return out -instance ContainsDoc (Contract cp st) where+instance ContainsDoc (ContractData cp st) where   buildDocUnfinalized =-    buildDocUnfinalized . cCode-instance ContainsUpdateableDoc (Contract cp st) where+    buildDocUnfinalized . compileLorentzContract+instance ContainsUpdateableDoc (ContractData cp st) where   modifyDocEntirely how c =-    c{ cCode = modifyDocEntirely how (cCode c) }+    c{ cdCode = modifyDocEntirely how (cdCode c) }  -- | Lorentz version of analyzer. analyzeLorentz :: inp :-> out -> AnalyzerRes analyzeLorentz = analyze . compileLorentz  makeLensesWith postfixLFields ''CompilationOptions-makeLensesWith postfixLFields ''Contract++cdCodeL ::+  forall cp st cp1 st1. (NiceParameterFull cp1, NiceStorage st1) =>+  Lens.Lens (ContractData cp st) (ContractData cp1 st1) (ContractCode cp st) (ContractCode cp1 st1)+cdCodeL f (ContractData code options)+  = fmap (`ContractData` options) (f code)++cdCompilationOptionsL ::+  forall cp st.+  Lens.Lens' (ContractData cp st) CompilationOptions+cdCompilationOptionsL f (ContractData code options)+  = fmap (ContractData code) (f options)

@@ -57,6 +57,7 @@   , stMem   , stGet   , stUpdate+  , stGetAndUpdate   , stDelete   , stInsert   , stInsertNew@@ -107,7 +108,6 @@   import qualified Data.Kind as Kind-import Data.Map (singleton) import GHC.TypeLits (KnownSymbol, Symbol)  import Lorentz.ADT@@ -115,6 +115,7 @@ import Lorentz.Coercions import Lorentz.Constraints import Lorentz.Errors (failUnexpected)+import Lorentz.Ext import qualified Lorentz.Instr as L import Lorentz.Iso import qualified Lorentz.Macro as L@@ -209,6 +210,13 @@   { sopToField       :: forall s.          FieldRef fname -> store : s :-> ftype : s+  , sopGetField+      -- TODO: [#585] should be @Dupable ftype@+      -- here and everywhere below.+      -- Though note that very complex functions that compose various ops+      -- inherently require @(Dupable store)@.+      :: forall s. (Dupable store)+      => FieldRef fname -> store : s :-> ftype : store : s   , sopSetField       :: forall s.          FieldRef fname -> ftype : store : s :-> store : s@@ -220,12 +228,9 @@ class StoreHasField store fname ftype | store fname -> ftype where   storeFieldOps :: StoreFieldOps store fname ftype -instance HasFieldOfType (a, b) fname ftype =>-         StoreHasField (a, b) fname ftype where-  storeFieldOps = storeFieldOpsADT--instance HasFieldOfType (a, b, c) fname ftype =>-         StoreHasField (a, b, c) fname ftype where+instance {-# OVERLAPPABLE #-}+         HasFieldOfType store fname ftype =>+         StoreHasField store fname ftype where   storeFieldOps = storeFieldOpsADT  -- | Pick storage field.@@ -236,9 +241,9 @@  -- | Get storage field, preserving the storage itself on stack. stGetField-  :: StoreHasField store fname ftype+  :: (StoreHasField store fname ftype, Dupable store)   => FieldRef fname -> store : s :-> ftype : store : s-stGetField l = L.dup # sopToField storeFieldOps l+stGetField l = sopGetField storeFieldOps l  -- | Pick storage field retaining a name label attached. --@@ -250,13 +255,13 @@  -- | Version of 'stToFieldNamed' that preserves the storage on stack. stGetFieldNamed-  :: (StoreHasField store fname ftype, FieldRefHasFinalName fname)+  :: (StoreHasField store fname ftype, FieldRefHasFinalName fname, Dupable ftype)   => FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : store : s-stGetFieldNamed fr = L.dup # stToFieldNamed fr+stGetFieldNamed fr = stGetFieldNamed fr  -- | Update storage field. stSetField-  :: StoreHasField store fname ftype+  :: (StoreHasField store fname ftype)   => FieldRef fname -> ftype : store : s :-> store : s stSetField = sopSetField storeFieldOps @@ -282,6 +287,10 @@       :: forall s.          FieldRef mname -> key : Maybe value : store : s :-> store : s +  , sopGetAndUpdate+      :: forall s.+         FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s+     -- Methods below are derivatives of methods above, they can be provided     -- if for given specific storage type more efficient implementation is     -- available.@@ -304,6 +313,7 @@ instance ( StoreHasField store name submap          , StoreHasSubmap submap SelfRef key value          , KnownSymbol name+         , Dupable store          ) => StoreHasSubmap store (name :: Symbol) key value where   storeSubmapOps = storeSubmapOpsReferTo (fromLabel @name :-| this) storeSubmapOps @@ -325,6 +335,12 @@   => FieldRef mname -> key : Maybe value : store : s :-> store : s stUpdate = sopUpdate storeSubmapOps +-- | Atomically get and update a value in storage.+stGetAndUpdate+  :: StoreHasSubmap store mname key value+  => FieldRef mname -> key : Maybe value : store : s :-> Maybe value : store : s+stGetAndUpdate = sopGetAndUpdate storeSubmapOps+ -- | Delete a value in storage. stDelete   :: forall store mname key value s.@@ -340,14 +356,15 @@  -- | Add a value in storage, but fail if it will overwrite some existing entry. stInsertNew-  :: StoreHasSubmap store mname key value+  :: (StoreHasSubmap store mname key value, Dupable key)   => FieldRef mname   -> (forall s0 any. key : s0 :-> any)   -> key : value : store : s   :-> store : s stInsertNew l doFail =-  L.duupX @3 # L.duupX @2 # stMem l #-  L.if_ doFail (stInsert l)+  L.dip L.some # L.dup #+  L.dip (stGetAndUpdate l) # L.swap #+  L.ifNone L.drop (L.drop # doFail)  ---------------------------------------------------------------------------- -- Stored Entrypoints@@ -399,10 +416,10 @@ -- | Extracts and executes the @epName@ entrypoint lambda from storage, returing -- the updated full storage (@store@) and the produced 'Operation's. stEntrypoint-  :: StoreHasEntrypoint store epName epParam epStore+  :: (StoreHasEntrypoint store epName epParam epStore, Dupable store)   => Label epName -> epParam : store : s :-> ([Operation], store) : s stEntrypoint l =-  L.dip (L.dup # stGetEpLambda l # L.swap # stToEpStore l) #+  L.dip (stGetEpStore l # L.dip (stGetEpLambda l)) #   L.pair # L.exec # L.unpair #   L.dip (stSetEpStore l) # L.pair @@ -414,7 +431,7 @@  -- | Get stored entrypoint lambda, preserving the storage itself on the stack. stGetEpLambda-  :: StoreHasEntrypoint store epName epParam epStore+  :: (StoreHasEntrypoint store epName epParam epStore, Dupable store)   => Label epName -> store : s :-> (EntrypointLambda epParam epStore) : store : s stGetEpLambda l = L.dup # stToEpLambda l @@ -433,7 +450,7 @@ -- | Get the sub-storage that the entrypoint operates on, preserving the storage -- itself on the stack. stGetEpStore-  :: StoreHasEntrypoint store epName epParam epStore+  :: (StoreHasEntrypoint store epName epParam epStore, Dupable store)   => Label epName -> store : s :-> epStore : store : s stGetEpStore l = L.dup # stToEpStore l @@ -454,6 +471,7 @@   => StoreFieldOps dt (fname :: Symbol) ftype storeFieldOpsADT = StoreFieldOps   { sopToField = toField . fieldNameToLabel+  , sopGetField = getField . fieldNameToLabel   , sopSetField = setField . fieldNameToLabel   } @@ -464,6 +482,7 @@   :: ( HasFieldOfType store epmName (EntrypointsField epParam epStore)      , HasFieldOfType store epsName epStore      , KnownValue epParam, KnownValue epStore+     , Dupable store      )   => Label epmName -> Label epsName   -> StoreEntrypointOps store epName epParam epStore@@ -481,6 +500,7 @@   :: ( StoreHasField store epmName (EntrypointsField epParam epStore)      , StoreHasField store epsName epStore      , KnownValue epParam, KnownValue epStore+     , Dupable store      )   => Label epmName -> Label epsName   -> StoreEntrypointOps store epName epParam epStore@@ -519,6 +539,7 @@ storeFieldOpsDeeper   :: ( HasFieldOfType storage fieldsPartName fields      , StoreHasField fields fname ftype+     , Dupable storage      )   => FieldRef fieldsPartName   -> StoreFieldOps storage fname ftype@@ -531,6 +552,7 @@ storeSubmapOpsDeeper   :: ( HasFieldOfType storage bigMapPartName fields      , StoreHasSubmap fields SelfRef key value+     , Dupable storage      )   => FieldRef bigMapPartName   -> StoreSubmapOps storage mname key value@@ -544,6 +566,7 @@ storeEntrypointOpsDeeper   :: ( HasFieldOfType store nameInStore substore      , StoreHasEntrypoint substore epName epParam epStore+     , Dupable store      )   => FieldRef nameInStore   -> StoreEntrypointOps store epName epParam epStore@@ -572,6 +595,7 @@   { sopMem = \_l -> sopMem l   , sopGet = \_l -> sopGet l   , sopUpdate = \_l -> sopUpdate l+  , sopGetAndUpdate = \_l -> sopGetAndUpdate l   , sopDelete = \_l -> sopDelete l   , sopInsert = \_l -> sopInsert l   }@@ -588,6 +612,7 @@ storeFieldOpsReferTo l StoreFieldOps{..} =   StoreFieldOps   { sopToField = \_l -> sopToField l+  , sopGetField = \_l -> sopGetField l   , sopSetField = \_l -> sopSetField l   } @@ -621,6 +646,7 @@   -> StoreFieldOps store name field2 mapStoreFieldOps LIso{..} StoreFieldOps{..} = StoreFieldOps   { sopToField = \l -> sopToField l # liTo+  , sopGetField = \l -> sopGetField l # liTo   , sopSetField = \l -> liFrom # sopSetField l   } @@ -636,6 +662,8 @@       L.framed mapper # sopGet l   , sopUpdate = \l ->       L.framed mapper # sopUpdate l+  , sopGetAndUpdate = \l ->+      L.framed mapper # sopGetAndUpdate l   , sopDelete = \l ->       L.framed mapper # sopDelete l   , sopInsert = \l ->@@ -644,7 +672,7 @@  -- | Change submap operations so that they work on a modified value. mapStoreSubmapOpsValue-  :: (KnownValue value1)+  :: (KnownValue value1, KnownValue value2)   => LIso value1 value2   -> StoreSubmapOps store name key value1   -> StoreSubmapOps store name key value2@@ -655,6 +683,8 @@       sopGet l # L.lmap liTo   , sopUpdate = \l ->       L.dip (L.lmap liFrom) # sopUpdate l+  , sopGetAndUpdate = \l ->+      L.dip (L.lmap liFrom) # sopGetAndUpdate l # L.lmap liTo   , sopInsert = \l ->       L.dip liFrom # sopInsert l   , sopDelete = \l ->@@ -666,7 +696,8 @@ -- Suits for a case when your store does not contain its fields directly -- rather has a nested structure. composeStoreFieldOps-  :: FieldRef nameInStore+  :: (Dupable store)+  => FieldRef nameInStore   -> StoreFieldOps store nameInStore substore   -> StoreFieldOps substore nameInSubstore field   -> StoreFieldOps store nameInSubstore field@@ -674,15 +705,18 @@   StoreFieldOps   { sopToField = \l2 ->       sopToField ops1 l1 # sopToField ops2 l2+  , sopGetField = \l2 ->+      sopGetField ops1 l1 # sopToField ops2 l2   , sopSetField = \l2 ->-      L.dip (L.dup # sopToField ops1 l1) #+      L.dip (sopGetField ops1 l1) #       sopSetField ops2 l2 #       sopSetField ops1 l1   }  -- | Chain implementations of field and submap operations. composeStoreSubmapOps-  :: FieldRef nameInStore+  :: (Dupable store)+  => FieldRef nameInStore   -> StoreFieldOps store nameInStore substore   -> StoreSubmapOps substore mname key value   -> StoreSubmapOps store mname key value@@ -693,15 +727,19 @@   , sopGet = \l2 ->       L.dip (sopToField ops1 l1) # sopGet ops2 l2   , sopUpdate = \l2 ->-      L.dip (L.dip (L.dup # sopToField ops1 l1)) #+      L.dip (L.dip (sopGetField ops1 l1)) #       sopUpdate ops2 l2 #       sopSetField ops1 l1+  , sopGetAndUpdate = \l2 ->+      L.dip (L.dip (sopGetField ops1 l1)) #+      sopGetAndUpdate ops2 l2 #+      L.dip (sopSetField ops1 l1)   , sopDelete = \l2 ->-      L.dip (L.dup # sopToField ops1 l1) #+      L.dip (sopGetField ops1 l1) #       sopDelete ops2 l2 #       sopSetField ops1 l1   , sopInsert = \l2 ->-      L.dip (L.dip (L.dup # sopToField ops1 l1)) #+      L.dip (L.dip (sopGetField ops1 l1)) #       sopInsert ops2 l2 #       sopSetField ops1 l1   }@@ -721,7 +759,9 @@ -- @sequenceStoreSubmapOps #mySubmap nonDefIso storeSubmapOps storeSubmapOps@ sequenceStoreSubmapOps   :: forall store substore value name subName key1 key2.-     (NiceConstant substore, KnownValue value)+     ( NiceConstant substore, KnownValue value+     , Dupable (key1, key2), Dupable store+     )   => FieldRef name   -> LIso (Maybe substore) substore   -> StoreSubmapOps store name key1 substore@@ -746,6 +786,10 @@       prepareUpdate #       L.dip (sopUpdate ops2 l2 # liFrom substoreIso) #       sopUpdate ops1 l1+  , sopGetAndUpdate = \l2 ->+      prepareUpdate #+      L.dip (sopGetAndUpdate ops2 l2 # L.dip (liFrom substoreIso)) #+      L.swap # L.dip (sopUpdate ops1 l1)   , sopDelete = \l2 ->       L.dip L.none # sopUpdate res l2   , sopInsert = \l2 ->@@ -773,7 +817,8 @@         )  composeStoreEntrypointOps-  :: FieldRef nameInStore+  :: (Dupable store)+  => FieldRef nameInStore   -> StoreFieldOps store nameInStore substore   -> StoreEntrypointOps substore epName epParam epStore   -> StoreEntrypointOps store epName epParam epStore@@ -781,13 +826,13 @@   { sopToEpLambda = \l2 ->       sopToField ops1 l1 # sopToEpLambda ops2 l2   , sopSetEpLambda = \l2 ->-      L.dip (L.dup # sopToField ops1 l1) #+      L.dip (sopGetField ops1 l1) #       sopSetEpLambda ops2 l2 #       sopSetField ops1 l1   , sopToEpStore = \l2 ->       sopToField ops1 l1 # sopToEpStore ops2 l2   , sopSetEpStore = \l2 ->-      L.dip (L.dup # sopToField ops1 l1) #+      L.dip (sopGetField ops1 l1) #       sopSetEpStore ops2 l2 #       sopSetField ops1 l1   }@@ -814,7 +859,9 @@ -} zoomStoreSubmapOps   :: forall store submapName nameInSubmap key value subvalue.-     (NiceConstant value, NiceConstant subvalue)+     ( NiceConstant value, NiceConstant subvalue+     , Dupable key, Dupable store+     )   => FieldRef submapName   -> LIso (Maybe value) value   -> LIso (Maybe subvalue) subvalue@@ -836,30 +883,48 @@         L.none   , sopUpdate = \l2 ->       L.dip (liTo subvalueIso) #-      updateSubmapValue l2 #+      useSubmapValue l2 #       L.dip (liFrom valueIso) #       sopUpdate ops1 l1+  , sopGetAndUpdate = \l2 ->+      -- here we can't efficiently use @sopGetAndUpdate ops1@,+      -- so implementing with simpler primitives+      L.dip (liTo subvalueIso) #+      getSubmapValue #+      L.dip (L.dup @subvalue) # L.swap #+      L.dip @subvalue+        ( stackType @(key : subvalue : value : store : _) #+          L.dip (sopSetField ops2 l2) #+          L.dip (liFrom valueIso) #+          sopUpdate ops1 l1+        ) #+      liFrom subvalueIso   , sopDelete = \l2 ->       L.dip L.none # sopUpdate res l2   , sopInsert = \l2 ->-      updateSubmapValue l2 #+      useSubmapValue l2 #       sopInsert ops1 l1   }   where-    updateSubmapValue-      :: FieldRef nameInSubmap-      -> key : subvalue : store : s-         :-> key : value : store : s-    updateSubmapValue l2 =+    -- preparation: get current value in map+    getSubmapValue+      :: key : subvalue : store : s+         :-> key : subvalue : value : store : s+    getSubmapValue =       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+          L.dip (L.dip L.dup # sopGet ops1 l1 # liTo valueIso)         ) +    -- preparation: update value with subvalue from map+    useSubmapValue+      :: FieldRef nameInSubmap+      -> key : subvalue : store : s+         :-> key : value : store : s+    useSubmapValue l2 =+      getSubmapValue # L.dip (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@@ -898,7 +963,7 @@   :: Label epName   -> EntrypointLambda epParam epStore   -> EntrypointsField epParam epStore-mkStoreEp l = BigMap . singleton (labelToMText l)+mkStoreEp l lambda = one (labelToMText l, lambda)  ---------------------------------------------------------------------------- -- Complex field references@@ -925,6 +990,7 @@ instance ( StoreHasField store field substore          , StoreHasField substore subfield ty          , KnownFieldRef field, KnownFieldRef subfield+         , Dupable store          ) =>          StoreHasField store (field :-| subfield) ty where   storeFieldOps =@@ -934,6 +1000,7 @@ instance ( StoreHasField store field substore          , StoreHasSubmap substore subfield key value          , KnownFieldRef field, KnownFieldRef subfield+         , Dupable store          ) =>          StoreHasSubmap store (field :-| subfield) key value where   storeSubmapOps =@@ -968,6 +1035,7 @@ instance StoreHasField store SelfRef store where   storeFieldOps = StoreFieldOps     { sopToField = \SelfRef -> L.nop+    , sopGetField = \SelfRef -> L.dup     , sopSetField = \SelfRef -> L.dip L.drop     } @@ -977,6 +1045,7 @@     { sopMem = \SelfRef -> L.mem     , sopGet = \SelfRef -> L.get     , sopUpdate = \SelfRef -> L.update+    , sopGetAndUpdate = \SelfRef -> L.getAndUpdate     , sopDelete = \SelfRef -> L.deleteMap     , sopInsert = \SelfRef -> L.mapInsert     }@@ -987,18 +1056,25 @@     { sopMem = \SelfRef -> L.mem     , sopGet = \SelfRef -> L.get     , sopUpdate = \SelfRef -> L.update+    , sopGetAndUpdate = \SelfRef -> L.getAndUpdate     , sopDelete = \SelfRef -> L.deleteMap     , sopInsert = \SelfRef -> L.mapInsert     } -instance NiceComparable key => StoreHasSubmap (Set key) SelfRef key () where+instance (NiceComparable key, Ord key, Dupable key) =>+         StoreHasSubmap (Set key) SelfRef key () where   storeSubmapOps = StoreSubmapOps     { sopMem = \SelfRef -> L.mem-    , sopGet = \SelfRef -> L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)-    , sopUpdate = \SelfRef -> L.dip L.isSome # L.update+    , sopGet = \SelfRef -> doGet+    , sopUpdate = \SelfRef -> doUpdate+    , sopGetAndUpdate = \SelfRef ->+        L.dupN @3 # L.dupN @2 # doGet # L.dip doUpdate     , sopDelete = \SelfRef -> L.setDelete-    , sopInsert = \SelfRef -> L.dip L.drop # L.setInsert+    , sopInsert = \SelfRef -> L.dip (L.drop @()) # L.setInsert     }+    where+      doGet = L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)+      doUpdate = L.dip L.isSome # L.update  -- | Provides alternative variadic interface for deep entries access. --

@@ -83,7 +83,7 @@ -- -- In Haskell world, we keep an invariant of that contained value relates -- to one of entry points from @entries@ list.-newtype UParam (entries :: [EntrypointKind]) = UParamUnsafe (MText, ByteString)+newtype UParam (entries :: [EntrypointKind]) = UnsafeUParam (MText, ByteString)   deriving stock (Generic, Eq, Show)   deriving anyclass (IsoValue, HasAnnotation, Wrappable) @@ -138,7 +138,7 @@      )   => Label name -> a -> UParam entries mkUParam label (a :: a) =-  UParamUnsafe (labelToMText label, lPackValueRaw a)+  UnsafeUParam (labelToMText label, lPackValueRaw a)     \\ nicePackedValueEvi @a  -- Example@@ -176,7 +176,7 @@     UParam entries -> Either EntrypointLookupError (MText, ConstrainedSome c)  instance UnpackUParam c '[] where-  unpackUParam (UParamUnsafe (name, _)) = Left (NoSuchEntrypoint name)+  unpackUParam (UnsafeUParam (name, _)) = Left (NoSuchEntrypoint name)  instance   ( KnownSymbol name@@ -184,14 +184,14 @@   , NiceUnpackedValue arg   , c arg   ) => UnpackUParam c ((name ?: arg) ': entries) where-  unpackUParam (UParamUnsafe (name, bytes))+  unpackUParam (UnsafeUParam (name, bytes))     | name == symbolToMText @name =       fmap (name,) .       first (const ArgumentUnpackFailed) .       fmap ConstrainedSome .       lUnpackValueRaw @arg $       bytes-    | otherwise = unpackUParam @c @entries (UParamUnsafe (name, bytes))+    | otherwise = unpackUParam @c @entries (UnsafeUParam (name, bytes))  ---------------------------------------------------------------------------- -- Pattern-matching@@ -262,25 +262,26 @@   --   -- This function is unsafe because it does not make sure at type-level   -- that entry points' names do not repeat.-  caseUParamUnsafe+  unsafeCaseUParam     :: Rec (CaseClauseU inp out) entries     -> UParamFallback inp out     -> (UParam entries : inp) :-> out  instance CaseUParam '[] where-  caseUParamUnsafe RNil fallback = unwrapUParam # fallback+  unsafeCaseUParam RNil fallback = unwrapUParam # fallback  instance ( KnownSymbol name          , CaseUParam entries+         , Typeable entries          , NiceUnpackedValue arg          ) =>          CaseUParam ((name ?: arg) ': entries) where-  caseUParamUnsafe (CaseClauseU clause :& clauses) fallback =+  unsafeCaseUParam (CaseClauseU clause :& clauses) fallback =     dup # unwrapUParam # car #-    push (mkMTextUnsafe $ symbolValT' @name) # eq #+    push (unsafeMkMText $ symbolValT' @name) # eq #     if_ (unwrapUParam # cdr # unpackRaw #          ifSome nop (failCustom_ #uparamArgumentUnpackFailed) # clause)-        (cutUParamEntry # caseUParamUnsafe clauses fallback)+        (cutUParamEntry # unsafeCaseUParam clauses fallback)     where       cutUParamEntry :: UParam (e : es) : s :-> UParam es : s       cutUParamEntry = forcedCoerce_@@ -294,7 +295,7 @@   => Rec (CaseClauseU inp out) entries   -> UParamFallback inp out   -> (UParam entries : inp) :-> out-caseUParam = caseUParamUnsafe+caseUParam = unsafeCaseUParam  -- | Like 'caseUParam', but accepts a tuple of clauses, not a 'Rec'. caseUParamT@@ -306,7 +307,7 @@   => IsoRecTuple clauses   -> UParamFallback inp out   -> (UParam entries : inp) :-> out-caseUParamT clauses fallback = caseUParamUnsafe (recFromTuple clauses) fallback+caseUParamT clauses fallback = unsafeCaseUParam (recFromTuple clauses) fallback  -- Example ----------------------------------------------------------------------------@@ -360,15 +361,15 @@ instance (GUParamLinearize x, GUParamLinearize y) => GUParamLinearize (x :+: y) where   type GUParamLinearized (x :+: y) = GUParamLinearized x ++ GUParamLinearized y   adtToRec = \case-    G.L1 x -> let UParamUnsafe up = adtToRec x in UParamUnsafe up-    G.R1 y -> let UParamUnsafe up = adtToRec y in UParamUnsafe up+    G.L1 x -> let UnsafeUParam up = adtToRec x in UnsafeUParam up+    G.R1 y -> let UnsafeUParam up = adtToRec y in UnsafeUParam up  instance (KnownSymbol name, NicePackedValue a) =>          GUParamLinearize (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) where   type GUParamLinearized (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) =     '[ '(name, a) ] -  adtToRec (G.M1 (G.M1 (G.K1 a))) = UParamUnsafe+  adtToRec (G.M1 (G.M1 (G.K1 a))) = UnsafeUParam     ( symbolToMText @name     , lPackValueRaw a     )

@@ -32,13 +32,17 @@   , Bls12381G2   , Set   , Map+  , M.BigMapId (..)   , M.BigMap (..)+  , M.mkBigMap   , M.Operation   , Maybe (..)   , List+  , ReadTicket (..)   , ContractRef (..)   , TAddress (..)   , FutureContract (..)+  , M.Ticket (..)    , M.EpName   , pattern M.DefEpName@@ -107,6 +111,17 @@  instance M.TypeHasDoc Never where   typeDocMdDescription = "An uninhabited type."++-- | Value returned by @READ_TICKET@ instruction.+data ReadTicket a = ReadTicket+  { rtTicketer :: Address+  , rtData :: a+  , rtAmount :: Natural+  } deriving stock (Show, Eq, Ord)++customGeneric "ReadTicket" rightComb++deriving anyclass instance IsoValue a => IsoValue (ReadTicket a)  -- | Provides 'Buildable' instance that prints Lorentz value via Michelson's -- 'Value'.