packages feed

lorentz 0.9.1 → 0.10.0

raw patch · 17 files changed

+413/−252 lines, 17 filesdep +base-nopreludedep −base

Dependencies added: base-noprelude

Dependencies removed: base

Files

CHANGES.md view
@@ -2,9 +2,27 @@ ========== <!-- Append new entries here --> +0.10.0+======+* [!774](https://gitlab.com/morley-framework/morley/-/merge_requests/774)+  + Added support for `BLS12-381` crypto primitives (types, instructions, arithmetics).+  + Now it is possible to use `int` instruction for newtypes over `Natural`.+* [!786](https://gitlab.com/morley-framework/morley/-/merge_requests/786)+* [!791](https://gitlab.com/morley-framework/morley/-/merge_requests/791)+  + Add new Edo instructions: `pairGet` and `pairUpdate`.+* [!755](https://gitlab.com/morley-framework/morley/-/merge_requests/755)+  Restricted `FAILWITH` only to packable values, except `CONTRACT`s+* [!759](https://gitlab.com/morley-framework/morley/-/merge_requests/759)+  + Add `UnitErrorArg` and `NoErrorArg` to be used with `ErrorArg` instance.+    + `UnitErrorArg` is preferred to `()`+    + `NoErrorArg` allows failing with just a string instead of a `pair string unit`.+* [!764](https://gitlab.com/morley-framework/morley/-/merge_requests/764)+  + Added `Never` type, deprecated `Empty` type.  0.9.1 =====+* [!781](https://gitlab.com/morley-framework/morley/-/merge_requests/781)+  + Replaced mixins and dependency on `base` with `base-noprelude`. * [!751](https://gitlab.com/morley-framework/morley/-/merge_requests/751)   + Add new Edo instruction: `LEVEL`. * [!741](https://gitlab.com/morley-framework/morley/-/merge_requests/741)
lorentz.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           lorentz-version:        0.9.1+version:        0.10.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@@ -85,7 +85,7 @@   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude   build-depends:       aeson-pretty-    , base >=4.7 && <5+    , base-noprelude >=4.7 && <5     , bimap     , bytestring     , constraints >=0.11@@ -107,6 +107,4 @@     , unordered-containers     , vinyl     , with-utf8-  mixins:-      base hiding (Prelude)   default-language: Haskell2010
src/Lorentz/Annotation.hs view
@@ -35,7 +35,7 @@   (BigMap, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, ToT, insertTypeAnn,   starNotes) import Michelson.Typed.Haskell.Value (GValueType)-import Michelson.Untyped (FieldAnn, TypeAnn, ann, noAnn)+import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, ann, noAnn) import Tezos.Address import Tezos.Core import Tezos.Crypto@@ -91,7 +91,7 @@ gGetAnnotationNoField     :: forall a. (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a)     => FollowEntrypointFlag -> Notes (ToT a)-gGetAnnotationNoField = \_ -> fst $ gGetAnnotation @(G.Rep a) defaultAnnOptions NotFollowEntrypoint NotGenerateFieldAnn+gGetAnnotationNoField = \_ -> gGetAnnotation @(G.Rep a) defaultAnnOptions NotFollowEntrypoint NotGenerateFieldAnn ^. _1  -- | This class defines the type and field annotations for a given type. Right now -- the type annotations come from names in a named field, and field annotations are@@ -102,7 +102,7 @@     :: (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a)     => FollowEntrypointFlag     -> Notes (ToT a)-  getAnnotation b = fst $ gGetAnnotation @(G.Rep a) (annOptions @a) b GenerateFieldAnn+  getAnnotation b = gGetAnnotation @(G.Rep a) (annOptions @a) b GenerateFieldAnn ^. _1    annOptions :: AnnOptions   default annOptions :: AnnOptions@@ -199,10 +199,10 @@  -- | A Generic @HasAnnotation@ implementation class GHasAnnotation a where-  gGetAnnotation :: AnnOptions -> FollowEntrypointFlag -> GenerateFieldAnnFlag -> (Notes (GValueType a), FieldAnn)+  gGetAnnotation :: AnnOptions -> FollowEntrypointFlag -> GenerateFieldAnnFlag -> (Notes (GValueType a), FieldAnn, VarAnn)  instance GHasAnnotation G.U1 where-  gGetAnnotation _ _ _ = (starNotes, noAnn)+  gGetAnnotation _ _ _ = (starNotes, noAnn, noAnn)  instance (GHasAnnotation x)   => GHasAnnotation (G.M1 G.S ('G.MetaSel 'Nothing b c d) x)@@ -213,13 +213,14 @@   => GHasAnnotation (G.M1 G.S ('G.MetaSel ('Just a) b c d) x)   where   gGetAnnotation o b b2 = case b2 of-    GenerateFieldAnn -> (fst $ gGetAnnotation @x o b b2, ctorNameToAnnWithOptions @a o)-    NotGenerateFieldAnn -> (fst $ gGetAnnotation @x o b b2, noAnn)+    GenerateFieldAnn -> (gGetAnnotation @x o b b2 ^. _1, ctorNameToAnnWithOptions @a o, noAnn)+    NotGenerateFieldAnn -> (gGetAnnotation @x o b b2 ^. _1, noAnn, noAnn)  instance (GHasAnnotation x, KnownSymbol a) => GHasAnnotation (G.M1 G.C ('G.MetaCons a _p _f) x) where   gGetAnnotation o b b2 =-    ( fst $ gGetAnnotation @x o b b2+    ( gGetAnnotation @x o b b2 ^. _1     , ctorNameToAnnWithOptions @a o+    , noAnn     )  instance (GHasAnnotation x) => GHasAnnotation (G.M1 G.D i1 x) where@@ -234,20 +235,22 @@   where    gGetAnnotation o followEntrypointFlag generateAnnFlag =-    let (xTypeAnn, xFieldAnn) = gGetAnnotation @x o followEntrypointFlag generateAnnFlag-        (yTypeAnn, yFieldAnn) = gGetAnnotation @y o followEntrypointFlag generateAnnFlag+    let (xTypeAnn, xFieldAnn, xVarAnn) = gGetAnnotation @x o followEntrypointFlag generateAnnFlag+        (yTypeAnn, yFieldAnn, yVarAnn) = gGetAnnotation @y o followEntrypointFlag generateAnnFlag     in case (followEntrypointFlag, generateAnnFlag) of           (NotFollowEntrypoint, GenerateFieldAnn) ->             ( NTOr noAnn                 xFieldAnn yFieldAnn                 xTypeAnn yTypeAnn             , noAnn+            , xVarAnn             )           _ ->             ( NTOr noAnn                 noAnn noAnn                 xTypeAnn yTypeAnn             , noAnn+            , yVarAnn             )  instance@@ -258,14 +261,16 @@     GHasAnnotation (x G.:*: y)   where   gGetAnnotation o _ b2 =-    let  (xTypeAnn, xFieldAnn) = gGetAnnotation @x o NotFollowEntrypoint b2-         (yTypeAnn, yFieldAnn) = gGetAnnotation @y o NotFollowEntrypoint b2+    let  (xTypeAnn, xFieldAnn, xVarAnn) = gGetAnnotation @x o NotFollowEntrypoint b2+         (yTypeAnn, yFieldAnn, yVarAnn) = gGetAnnotation @y o NotFollowEntrypoint b2     in       ( NTPair noAnn           xFieldAnn yFieldAnn+          xVarAnn yVarAnn           xTypeAnn yTypeAnn       , noAnn+      , noAnn       )  instance (HasAnnotation x) => GHasAnnotation (G.Rec0 x) where-  gGetAnnotation _ b _ = (getAnnotation @x b, noAnn)+  gGetAnnotation _ b _ = (getAnnotation @x b, noAnn, noAnn)
src/Lorentz/Arith.hs view
@@ -6,28 +6,30 @@ module Lorentz.Arith   ( ArithOpHs (..)   , UnaryArithOpHs (..)+  , ToIntegerArithOpHs   ) where  import qualified Data.Kind as Kind  import Lorentz.Value-import Lorentz.Constraints.Scopes (NiceComparable) import Michelson.Typed.Arith  -- | Lifted 'ArithOp'. class ( ArithOp aop (ToT n) (ToT m)-      , NiceComparable n, NiceComparable m       , ToT (ArithResHs aop n m) ~ ArithRes aop (ToT n) (ToT m)       ) => ArithOpHs (aop :: Kind.Type) (n :: Kind.Type) (m :: Kind.Type) where   type ArithResHs aop n m :: Kind.Type  -- | Lifted 'UnaryArithOp'. class ( UnaryArithOp aop (ToT n)-      , NiceComparable n       , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)       ) => UnaryArithOpHs (aop :: Kind.Type) (n :: Kind.Type) where   type UnaryArithResHs aop n :: Kind.Type +class ( ToIntArithOp (ToT n)+      ) =>+      ToIntegerArithOpHs (n :: Kind.Type)+ instance ArithOpHs Add Natural Integer where   type ArithResHs Add Natural Integer = Integer instance ArithOpHs Add Integer Natural where@@ -42,6 +44,12 @@   type ArithResHs Add Integer Timestamp = Timestamp instance ArithOpHs Add Mutez Mutez where   type ArithResHs Add Mutez Mutez = Mutez+instance ArithOpHs Add Bls12381Fr Bls12381Fr where+  type ArithResHs Add Bls12381Fr Bls12381Fr = Bls12381Fr+instance ArithOpHs Add Bls12381G1 Bls12381G1 where+  type ArithResHs Add Bls12381G1 Bls12381G1 = Bls12381G1+instance ArithOpHs Add Bls12381G2 Bls12381G2 where+  type ArithResHs Add Bls12381G2 Bls12381G2 = Bls12381G2  instance ArithOpHs Sub Natural Integer where   type ArithResHs Sub Natural Integer = Integer@@ -70,14 +78,37 @@   type ArithResHs Mul Natural Mutez = Mutez instance ArithOpHs Mul Mutez Natural where   type ArithResHs Mul Mutez Natural = Mutez--instance UnaryArithOpHs Abs Integer where-  type UnaryArithResHs Abs Integer = Natural+instance ArithOpHs Mul Integer Bls12381Fr where+  type ArithResHs Mul Integer Bls12381Fr = Bls12381Fr+instance ArithOpHs Mul Natural Bls12381Fr where+  type ArithResHs Mul Natural Bls12381Fr = Bls12381Fr+instance ArithOpHs Mul Bls12381Fr Integer where+  type ArithResHs Mul Bls12381Fr Integer = Bls12381Fr+instance ArithOpHs Mul Bls12381Fr Natural where+  type ArithResHs Mul Bls12381Fr Natural = Bls12381Fr+instance ArithOpHs Mul Bls12381Fr Bls12381Fr where+  type ArithResHs Mul Bls12381Fr Bls12381Fr = Bls12381Fr+instance ArithOpHs Mul Bls12381G1 Bls12381Fr where+  type ArithResHs Mul Bls12381G1 Bls12381Fr = Bls12381G1+instance ArithOpHs Mul Bls12381G2 Bls12381Fr where+  type ArithResHs Mul Bls12381G2 Bls12381Fr = Bls12381G2+instance Bls12381MulBadOrder Bls12381Fr Bls12381G1 =>+         ArithOpHs Mul Bls12381Fr Bls12381G1 where+  type ArithResHs Mul Bls12381Fr Bls12381G1 = Bls12381G1+instance Bls12381MulBadOrder Bls12381Fr Bls12381G2 =>+         ArithOpHs Mul Bls12381Fr Bls12381G2 where+  type ArithResHs Mul Bls12381Fr Bls12381G2 = Bls12381G2  instance UnaryArithOpHs Neg Integer where   type UnaryArithResHs Neg Integer = Integer instance UnaryArithOpHs Neg Natural where   type UnaryArithResHs Neg Natural = Integer+instance UnaryArithOpHs Neg Bls12381Fr where+  type UnaryArithResHs Neg Bls12381Fr = Bls12381Fr+instance UnaryArithOpHs Neg Bls12381G1 where+  type UnaryArithResHs Neg Bls12381G1 = Bls12381G1+instance UnaryArithOpHs Neg Bls12381G2 where+  type UnaryArithResHs Neg Bls12381G2 = Bls12381G2  instance ArithOpHs Or Natural Natural where   type ArithResHs Or Natural Natural = Natural@@ -126,3 +157,6 @@  instance UnaryArithOpHs Ge Integer where   type UnaryArithResHs Ge Integer = Bool++instance ToIntegerArithOpHs Natural+instance ToIntegerArithOpHs Bls12381Fr
src/Lorentz/Empty.hs view
@@ -6,11 +6,10 @@  -- | Support for uninhabited type. ----- Currently they are not supported my Michelson, so we provide--- a sort of replacement.+-- Note: this module exists solely for historical reasons since the time when+-- 'Never' was not yet supported by the Michelson. ----- This module should be removed once the proposal is implemented:--- https://gitlab.com/tezos/tezos/issues/662+-- TODO [#549]: remove this module. module Lorentz.Empty   ( Empty   , absurd_@@ -26,6 +25,7 @@ import Michelson.Typed.Haskell.Doc  -- | Replacement for uninhabited type.+{-# DEPRECATED Empty "Use Never type instead" #-} newtype Empty = Empty ()   deriving stock Generic   deriving anyclass (IsoValue, HasAnnotation)@@ -37,10 +37,10 @@     \should never be called."  -- | Someone constructed 'Empty' type.-type instance ErrorArg "emptySupplied" = ()+type instance ErrorArg "emptySupplied" = UnitErrorArg  instance Buildable (CustomError "emptySupplied") where-  build (CustomError _ ()) =+  build (CustomError _ (_, ())) =     "'Empty' value was passed to the contract."  instance CustomErrorHasDoc "emptySupplied" where
src/Lorentz/Entrypoints/Doc.hs view
@@ -16,6 +16,7 @@   , CommonContractBehaviourKind   , CommonEntrypointsBehaviourKind   , diEntrypointToMarkdown+  , SomeEntrypointArg (..)   , DEntrypointArg (..)   , DType (..)   , DeriveCtorFieldDoc (..)@@ -47,6 +48,7 @@ import Data.Constraint (Dict(..)) import qualified Data.Kind as Kind 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)@@ -62,18 +64,19 @@ import Lorentz.Entrypoints.Core import Lorentz.Entrypoints.Helpers import Lorentz.Entrypoints.Impl-import Michelson.Printer (printUntypedValue)+import Michelson.Printer (printTypedValue) import Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)-import Michelson.Typed (pattern DefEpName, EpName, mkUType, sampleValueFromUntype)+import Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue)+import qualified Michelson.Typed as T import Michelson.Typed.Haskell.Doc import Michelson.Typed.Haskell.Instr import qualified Michelson.Untyped as Untyped import Util.Label (Label) import Util.Markdown import Util.Type-import Util.Typeable import Util.TypeLits import Util.TypeTuple+import Util.Typeable  -- | Gathers information about single entrypoint. --@@ -292,10 +295,14 @@     , pbdMichelson = michDesc     } +-- | Entrypoint argument type in typed representation.+data SomeEntrypointArg =+  forall a. (NiceParameter a, TypeHasDoc a) => SomeEntrypointArg (Proxy a)+ -- | Describes argument of an entrypoint. data DEntrypointArg =   DEntrypointArg-  { epaArg :: Maybe DType+  { epaArg :: Maybe SomeEntrypointArg     -- ^ Argument of the entrypoint. Pass 'Nothing' if no argument is required.   , epaBuilding :: [ParamBuildingStep]     -- ^ Describes a way to lift an entrypoint argument into full parameter@@ -307,29 +314,23 @@     -- then the first step (actual last) should describe wrapping into @Run@     -- constructor, and the second step (actual first) should be about wrapping     -- into @Service1@ constructor.-  , epaType :: Untyped.Type-    -- ^ Untyped representation of entrypoint, used for printing its michelson-    -- type representation.   }  constructDEpArg   :: forall arg.-     ( TypeHasDoc arg-     , HasAnnotation arg-     , KnownValue arg+     ( NiceParameter arg+     , TypeHasDoc arg      )   => DEntrypointArg constructDEpArg = DEntrypointArg-  { epaArg = Just $ DType (Proxy @arg)+  { epaArg = Just $ SomeEntrypointArg (Proxy @arg)   , epaBuilding = []-  , epaType = mkDEpUType @arg   }  emptyDEpArg :: DEntrypointArg emptyDEpArg = DEntrypointArg   { epaArg = Nothing   , epaBuilding = []-  , epaType = Untyped.Type Untyped.TUnit Untyped.noAnn   }  mkDEpUType :: forall t. (KnownValue t, HasAnnotation t) => Untyped.Type@@ -337,15 +338,13 @@  mkDEntrypointArgSimple   :: forall t.-     ( KnownValue t-     , HasAnnotation t+     ( NiceParameter t      , TypeHasDoc t      )   => DEntrypointArg mkDEntrypointArgSimple = DEntrypointArg-  { epaArg = Just $ DType (Proxy @t)+  { epaArg = Just $ SomeEntrypointArg (Proxy @t)   , epaBuilding = []-  , epaType = mkDEpUType @t   }  -- | Go over contract code and update every occurrence of 'DEntrypointArg'@@ -367,27 +366,29 @@ instance DocItem DEntrypointArg where   docItemPos = 20   docItemSectionName = Nothing-  docItemDependencies (DEntrypointArg mdty _ _) =-    [SomeDocDefinitionItem dty | Just dty <- pure mdty]-  docItemToMarkdown _ (DEntrypointArg mdty psteps et) =+  docItemDependencies (DEntrypointArg mdty _) =+    [ SomeDocDefinitionItem (DType $ Proxy @ty)+    | Just (SomeEntrypointArg (_ :: Proxy ty)) <- pure mdty ]+  docItemToMarkdown _ (DEntrypointArg mdty psteps) =     mconcat . Prelude.map (<> "\n\n") $       [ mdSubsection "Argument" $           case mdty of             Nothing -> "none (pass unit)"-            Just (DType (dty :: Proxy ep)) -> mconcat . Prelude.intersperse "\n" $+            Just (SomeEntrypointArg (dty :: Proxy ep)) -> mconcat . Prelude.intersperse "\n" $               [ mempty               , "  + " <>                 mdSubsection "In Haskell"                   (typeDocMdReference dty (WithinParens False))               , "  + " <>                 mdSubsection "In Michelson"-                  (mdTicked $ printDocB False . renderDoc needsParens $ et)-              , "    + " <>+                  (mdTicked $ printDocB False . renderDoc needsParens $+                     T.untypeDemoteT @(T.ToT ep))+              , fromMaybe "" $ sampleTypedValue (sing @(ToT ep)) <&> \sampleVal ->+                "    + " <>                 mdSubsection "Example"                   (mdAddId "example-id"                     $ mdTicked-                    $ build $ printUntypedValue True-                    $ sampleValueFromUntype et+                    $ build $ printTypedValue True sampleVal                   )               ],           mdSpoiler "How to call this entrypoint" $@@ -439,7 +440,7 @@   deriveCtorFieldDoc = emptyDEpArg  instance-    (TypeHasDoc ty, HasAnnotation ty, KnownValue ty, KnownSymbol con)+    (NiceParameter ty, TypeHasDoc ty, KnownValue ty, KnownSymbol con)   =>     DeriveCtorFieldDoc con ('OneField ty)   where@@ -536,9 +537,8 @@   :: forall kind epName param s out.      ( KnownSymbol epName      , DocItem (DEntrypoint kind)+     , NiceParameter param      , TypeHasDoc param-     , HasAnnotation param-     , KnownValue param      )   => param : s :-> out -> param : s :-> out documentEntrypoint instr =@@ -557,8 +557,8 @@          , body ~ (param : s :-> out)          , KnownSymbol epName          , DocItem (DEntrypoint kind)+         , NiceParameter param          , TypeHasDoc param-         , HasAnnotation param          , KnownValue param          ) => EntryArrow kind name body where   (#->) _ = documentEntrypoint @kind @epName
src/Lorentz/Entrypoints/Impl.hs view
@@ -282,7 +282,7 @@   type GLookupEntrypoint mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =     JustOnEq ctor (GExtractField x)   gMkEntrypointsNotes =-    (fst $ gGetAnnotation @x defaultAnnOptions FollowEntrypoint NotGenerateFieldAnn, ctorNameToAnn @ctor)+    (gGetAnnotation @x defaultAnnOptions FollowEntrypoint NotGenerateFieldAnn ^. _1, ctorNameToAnn @ctor)   gMkEpLiftSequence (Label :: Label name) =     case sing @ctor %== sing @name of       STrue -> EpConstructed EplArgHere
src/Lorentz/Errors.hs view
@@ -16,7 +16,6 @@   , isoErrorFromVal   , ErrorHasDoc (..)   , typeDocMdDescriptionReferToError-  , customErrorDocHaskellRepGeneral   , isInternalErrorClass    , UnspecifiedError (..)@@ -27,11 +26,16 @@   , failUnexpected      -- * Custom errors+  , NoErrorArg+  , UnitErrorArg   , ErrorArg   , CustomError (..)+  , CustomErrorRep+  , IsCustomErrorArgRep (..)+  , MustHaveErrorArg   , failCustom-  , RequireNoArgError   , failCustom_+  , failCustomNoArg      -- * Documentation   , ErrorClass (..)@@ -63,7 +67,6 @@ import Michelson.Typed.Haskell import Michelson.Typed.Instr import Michelson.Typed.Scope-import Michelson.Typed.T import Util.Markdown import Util.Type import Util.Typeable@@ -74,9 +77,10 @@ ----------------------------------------------------------------------------  type ErrorScope t =-  -- We can require a weaker constraint (e.g. no 'HasNoOp'), but-  -- for now it's the simplest way to make 'failUsing' work   ( 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   ) @@ -168,7 +172,7 @@ instance ErrorHasDoc MText where   errorDocName = "InternalError"   errorDocMdCause =-    "Some internal error occured."+    "Some internal error occurred."   errorDocHaskellRep =     "Textual error message, see " <>     typeDocMdReference (Proxy @MText) (WithinParens False) <> "."@@ -197,7 +201,7 @@  instance ErrorHasDoc UnspecifiedError where   errorDocName = "Unspecified error"-  errorDocMdCause = "Some error occured."+  errorDocMdCause = "Some error occurred."   errorDocHaskellRep = typeDocMdReference (Proxy @()) (WithinParens False) <> "."   errorDocDependencies = typeDocDependencies (Proxy @()) @@ -282,79 +286,111 @@ -- Use this in pattern matches against error (e.g. in tests). data CustomError (tag :: Symbol) = CustomError   { ceTag :: Label tag-  , ceArg :: ErrorArg tag+  , ceArg :: CustomErrorRep tag   } -deriving stock instance Eq (ErrorArg tag) => Eq (CustomError tag)-deriving stock instance Show (ErrorArg tag) => Show (CustomError tag)+deriving stock instance Eq (CustomErrorRep tag) => Eq (CustomError tag)+deriving stock instance Show (CustomErrorRep tag) => Show (CustomError tag)  instance Buildable (CustomError tag) where   build (CustomError tg _err) = "CustomError #" +| build tg +-- | To be used as @ErrorArg@ instance when failing with just+-- a @string@ instead of @pair string x@+data NoErrorArg++-- | To be used as @ErrorArg@ instances. This is equivalent to using+-- @()@ but using @UnitErrorArg@ is preferred since @()@ behavior could+-- be changed in the future.+data UnitErrorArg++ -- | How 'CustomError' is actually represented in Michelson.-type CustomErrorRep tag = (MText, ErrorArg tag)+type CustomErrorRep tag = CustomErrorArgRep (ErrorArg tag) +type family CustomErrorArgRep (errArg :: Kind.Type) where+  CustomErrorArgRep NoErrorArg = MText+  CustomErrorArgRep UnitErrorArg = (MText, ())+  CustomErrorArgRep errArg = (MText, errArg)++-- | Typeclass implements various method that work with `CustomErrorArgRep`.+class IsCustomErrorArgRep a where+  verifyErrorTag :: MText -> a -> Either Text a+  customErrorRepDocDeps :: [SomeDocDefinitionItem]+  customErrorHaskellRep+    :: (KnownSymbol tag, CustomErrorHasDoc tag)+    => Proxy tag -> Markdown++instance IsCustomErrorArgRep MText where+  verifyErrorTag expectedTag tag =+    if tag == expectedTag+    then Right tag+    else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""+  customErrorRepDocDeps = []+  customErrorHaskellRep (_ :: Proxy tag) =+    mdTicked $ build (errorTagToText @tag)++instance (TypeHasDoc errArg)+  => IsCustomErrorArgRep (MText, errArg) where+  verifyErrorTag expectedTag (tag, arg) =+    if tag == expectedTag+    then Right (tag, arg)+    else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""+  customErrorRepDocDeps =+    [ SomeDocDefinitionItem $ DType $ Proxy @errArg ]+  customErrorHaskellRep (_ :: Proxy tag) = mconcat+    [ mdTicked ("(" <> build (errorTagToText @tag) <> ", " <> "<error argument>" <> ")")+    , ("\n\nProvided error argument will be of type "+      <> typeDocMdReference (Proxy @(MText, errArg)) (WithinParens False)+      <> (maybe "" (\txt -> " and stand for " <> txt) (customErrArgumentSemantics @tag))+      <> "."+      )+    ]+ -- | This instance cannot be implemented, use 'IsError' instance instead.-instance (WellTypedIsoValue (ErrorArg tag), TypeError ('Text "CustomError has no IsoValue instance")) =>+instance (WellTypedIsoValue (CustomErrorRep tag), TypeError ('Text "CustomError has no IsoValue instance")) =>          IsoValue (CustomError tag) where   -- Originally we had a `TypeError` here, but that had to be changed when   -- `WellTyped (ToT a)` was added as a superclass of `IsoValue`, because it   -- resulted in the type error being triggerred from the evaluation of `ToT`   -- typefamily in the super class clause.-  type ToT (CustomError tag) = (ToT (MText, ErrorArg tag))+  type ToT (CustomError tag) = (ToT (CustomErrorRep tag))   toVal = error "impossible"   fromVal = error "impossible" -instance (CustomErrorHasDoc tag, KnownError (ErrorArg tag), IsoValue (ErrorArg tag)) =>-         IsError (CustomError tag) where-  errorToVal (CustomError l arg) cont =-    cont $ toVal @(CustomErrorRep tag) (errorTagToMText l, arg)+instance ( CustomErrorHasDoc tag+         , KnownError (CustomErrorRep tag)+         , IsoValue (CustomErrorRep tag)+         , IsCustomErrorArgRep (CustomErrorRep tag)+         )+  => IsError (CustomError tag) where++  errorToVal (CustomError _ arg) cont =+    cont $ toVal @(CustomErrorRep tag) arg+   errorFromVal (v :: Value t) =     let expectedTag = errorTagToMText (fromLabel @tag)     in case cast v of-        Just v' ->-          let (tag, arg) = fromVal @(CustomErrorRep tag) v'-          in if tag == expectedTag-             then Right $ CustomError fromLabel arg-             else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""+        Just v' -> do+          errArg <- verifyErrorTag @(CustomErrorRep tag) expectedTag+            $ fromVal @(CustomErrorRep tag) v'+          pure $ CustomError fromLabel errArg         Nothing -> Left $ "Wrong type for custom error: " <> pretty (demote @t) -instance (CustomErrorHasDoc tag, SingI (ToT (ErrorArg tag))) =>-         ErrorHasDoc (CustomError tag) where+instance ( CustomErrorHasDoc tag+         , IsCustomErrorArgRep (CustomErrorRep tag)+         )+  => ErrorHasDoc (CustomError tag) where   errorDocName = errorTagToText @tag-  errorDocDependencies = [SomeDocDefinitionItem $ DType $ Proxy @(ErrorArg tag)]+  errorDocDependencies = customErrorRepDocDeps @(CustomErrorRep tag)   errorDocMdCause = customErrDocMdCause @tag   errorDocMdCauseInEntrypoint = customErrDocMdCauseInEntrypoint @tag   errorDocClass = customErrClass @tag-  errorDocHaskellRep =-    customErrorDocHaskellRepGeneral (show $ errorTagToText @tag) (Proxy @tag)+  errorDocHaskellRep = customErrorHaskellRep @(CustomErrorRep tag) (Proxy @tag) -  type ErrorRequirements (CustomError tag) = (CustomErrorHasDoc tag, SingI (ToT (ErrorArg tag)))+  type ErrorRequirements (CustomError tag) = (CustomErrorHasDoc tag, IsCustomErrorArgRep (CustomErrorRep tag))   errorDocRequirements = Dict --- | Description of error representation in Haskell.-customErrorDocHaskellRepGeneral-  :: ( SingI (ToT (ErrorArg tag)), IsError (CustomError tag)-     , TypeHasDoc (ErrorArg tag), CustomErrorHasDoc tag-     )-  => Text -> Proxy tag -> Markdown-customErrorDocHaskellRepGeneral tagName (_ :: Proxy tag) =-  let hasArg = demote @(ToT (ErrorArg tag)) /= TUnit-      tagName' = build tagName-  in mconcat $ catMaybes-    [ Just $-        ( if hasArg-          then mdTicked ("(" <> tagName' <> ", " <> "<error argument>" <> ")")-          else mdTicked ("(" <> tagName' <> ", ())")-        ) <> "."-    , guard hasArg $>-        ("\n\nProvided error argument will be of type "-        <> typeDocMdReference (Proxy @(ErrorArg tag)) (WithinParens False)-        <> (maybe "" (\txt -> " and stand for " <> txt) (customErrArgumentSemantics @tag))-        <> "."-        )-    ]- -- | Demote error tag to term level. errorTagToMText :: Label tag -> MText errorTagToMText l =@@ -370,7 +406,7 @@ -- | Fail with given custom error. failCustom   :: forall tag err s any.-     ( err ~ ErrorArg tag+     ( MustHaveErrorArg tag (MText, err)      , CustomErrorHasDoc tag      , KnownError err      )@@ -378,38 +414,55 @@ failCustom l =   doc (DThrows (Proxy @(CustomError tag))) #   push (errorTagToMText l) # pair @MText @err #-  FI (FAILWITH @(ToT (CustomErrorRep tag)))+  FI (FAILWITH @(ToT (MText, err))) -type RequireNoArgError tag msg =-  ( TypeErrorUnless (ErrorArg tag == ()) msg-  , msg ~-    ('Text "Expected no-arg error, but given error requires argument of type "-      ':<>: 'ShowType (ErrorArg tag)-    )+-- | Fail with given custom error.+failCustomNoArg+  :: forall tag s any.+     ( MustHaveErrorArg tag MText+     , CustomErrorHasDoc tag+     )+  => Label tag -> s :-> any+failCustomNoArg l =+  doc (DThrows (Proxy @(CustomError tag))) #+  push (errorTagToMText l) #+  FI (FAILWITH @(ToT (MText)))+++type MustHaveErrorArg errorTag expectedArgRep =+  ( TypeErrorUnless (CustomErrorRep errorTag == expectedArgRep)+      ('Text "Error argument type is "+        ':<>: 'ShowType (expectedArgRep)+        ':<>: 'Text " but given error requires argument of type "+        ':<>: 'ShowType (CustomErrorRep errorTag)+      )+  , CustomErrorRep errorTag ~ expectedArgRep   ) --- | Specialization of 'failCustom' for no-arg errors.+-- | Specialization of 'failCustom' for unit-arg errors. failCustom_-  :: forall tag s any notVoidErrorMsg.-     ( RequireNoArgError tag notVoidErrorMsg+  :: forall tag s any.+     ( MustHaveErrorArg tag (MText, ())      , CustomErrorHasDoc tag      )   => Label tag -> s :-> any failCustom_ l =-  inTypeErrorUnless @(ErrorArg tag == ()) @notVoidErrorMsg $-  reifyTypeEquality @(ErrorArg tag) @() $-    unit # failCustom l+  reifyTypeEquality @(CustomErrorRep tag) @(MText, ()) $+    doc (DThrows (Proxy @(CustomError tag))) #+    unit #+    push (errorTagToMText l) # pair @MText @() #+    FI (FAILWITH @(ToT (MText, ())))  -- Special treatment of no-arg errors ---------------------------------------------------------------------------- -instance Eq (ErrorArg tag) => Eq (() -> CustomError tag) where+instance Eq (CustomErrorRep tag) => Eq (() -> CustomError tag) where   e1 == e2 = e1 () == e2 ()-instance Show (ErrorArg tag) => Show (() -> CustomError tag) where+instance Show (CustomErrorRep tag) => Show (() -> CustomError tag) where   show e = show (e ())  -- | If 'CustomError' constructor is not provided its argument, we assume--- that this is no-arg error and interpret the passed value as complete.+-- that this is unit-arg error and interpret the passed value as complete. instance ( Typeable arg          , IsError (CustomError tag)          , TypeErrorUnless (arg == ()) notVoidError@@ -421,13 +474,11 @@          ) =>          IsError (arg -> CustomError tag) where   errorToVal mkCustomError cont =-    inTypeErrorUnless @(arg == ()) @notVoidError $     reifyTypeEquality @arg @() $       errorToVal (mkCustomError ()) cont   errorFromVal v =-    inTypeErrorUnless @(arg == ()) @notVoidError $     reifyTypeEquality @arg @() $-      errorFromVal v <&> \(CustomError l ()) -> CustomError l+      errorFromVal v <&> \(CustomError l (a, ())) -> \b -> CustomError l (a, b)  instance (Typeable arg, ErrorHasDoc (CustomError tag)) =>          ErrorHasDoc (arg -> CustomError tag) where@@ -487,7 +538,7 @@   ErrClassContractInternal -> True   ErrClassUnknown -> False -class (KnownSymbol tag, TypeHasDoc (ErrorArg tag), IsError (CustomError tag)) =>+class (KnownSymbol tag, TypeHasDoc (CustomErrorRep tag), IsError (CustomError tag)) =>       CustomErrorHasDoc tag where   -- | What should happen for this error to be raised.   customErrDocMdCause :: Markdown@@ -608,9 +659,8 @@   given entrypoint call two different errors may take place, the one which   appears in the list first will be thrown. -  Most of the errors are represented according to the same-  `(error tag, error argument)` pattern. See the list of errors below-  for details.+  The errors are represented either as a string `error tag` or a pair `(error tag, error argument)`.+  See the list of errors below for details.    We distinquish several error classes:   + #{mdBold $ build ErrClassActionException}: given action cannot be performed with
src/Lorentz/Errors/Common.hs view
@@ -19,10 +19,10 @@  -- | Contract initiator should be contract admin in order to perform this -- operation.-type instance ErrorArg "senderIsNotAdmin" = ()+type instance ErrorArg "senderIsNotAdmin" = UnitErrorArg  instance Buildable (CustomError "senderIsNotAdmin") where-  build (CustomError _ ()) =+  build (CustomError _ (_, ())) =     "This operation can be executed only by admin, but is invoked by \     \someone else"
src/Lorentz/Errors/Numeric/Doc.hs view
@@ -221,8 +221,7 @@   numericErrorDocTextualTag :: ErrorRequirements err => Text  instance ErrorHasNumericDoc (CustomError tag) where-  numericErrorDocHaskellRep numTag =-    customErrorDocHaskellRepGeneral numTag (Proxy @tag)+  numericErrorDocHaskellRep _ = customErrorHaskellRep @(CustomErrorRep tag) (Proxy @tag)   numericErrorDocTextualTag = errorTagToText @tag  instance ErrorHasDoc (VoidResult res) =>
src/Lorentz/Instr.hs view
@@ -12,7 +12,10 @@   , commentAroundStmt   , drop   , dropN+  , ConstraintDUPNLorentz   , dup+  , dupNPeano+  , dupN   , swap   , ConstraintDIGLorentz   , digPeano@@ -41,7 +44,13 @@   , iter   , mem   , get+  , ConstraintPairGetLorentz+  , PairGetHs+  , pairGet   , update+  , ConstraintPairUpdateLorentz+  , PairUpdateHs+  , pairUpdate   , failingWhenPresent   , updateNew   , if_@@ -96,6 +105,8 @@   , now   , amount   , balance+  , votingPower+  , totalVotingPower   , checkSignature   , sha256   , sha512@@ -103,11 +114,14 @@   , sha3   , keccak   , hashKey+  , pairingCheck   , source   , sender   , address+  , selfAddress   , chainId   , level+  , never   , framed   , LorentzFunctor (..)   , NonZero (..)@@ -132,9 +146,10 @@ import Lorentz.Value import Lorentz.Zip import Michelson.Typed-  (pattern CAR, pattern CDR, CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN,-  ConstraintDIPN', ConstraintDUG, ConstraintDUG', EntrypointCallT(..), ExtInstr(..), Instr(..),-  pattern PAIR, RemFail(..), SomeEntrypointCallT(..), Value'(..), sepcName, starNotes)+  (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,+  ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,+  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), RemFail(..), SomeEntrypointCallT(..), UpdateN,+  Value'(..), pattern CAR, pattern CDR, pattern PAIR, sepcName, starNotes) import Michelson.Typed.Arith import Michelson.Typed.Haskell.Value import Util.Peano@@ -143,7 +158,6 @@ nop :: s :-> s nop = I Nop - justComment :: Text -> s :-> s justComment = comment . JustComment @@ -176,14 +190,35 @@   -- ↓ Kinda obvious, but not to GHC.   , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)   ) => s :-> Drop (ToPeano n) s-dropN = I (DROPN $ sing @(ToPeano n))+dropN = I (DROPN $ peanoSing @n)   where     _example :: '[ Integer, Integer, Integer ] :-> '[]     _example = dropN @3 -dup  :: a : s :-> a : a : s+dup :: a : s :-> a : a : s dup = I DUP +type ConstraintDUPNLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])+  (a :: Kind.Type) =+  ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)+  , ConstraintDUPN' Kind.Type n inp out a+  )++dupNPeano ::+  forall (n :: Peano) inp out a.+  ( ConstraintDUPNLorentz n inp out a+  ) => inp :-> out+dupNPeano = I (DUPN (sing @n))++dupN ::+  forall (n :: GHC.Nat) inp out a.+  ( ConstraintDUPNLorentz (ToPeano n) inp out a+  ) => inp :-> out+dupN = dupNPeano @(ToPeano n)+  where+    _example :: '[ Integer, (), Bool ] :-> '[ Bool, Integer, (), Bool ]+    _example = dupN @3+ swap :: a : b : s :-> b : a : s swap = I SWAP @@ -201,7 +236,7 @@   )  -- | Version of `dig` which uses Peano number.--- It is inteded for internal usage in Lorentz.+-- It is intended for internal usage in Lorentz. digPeano ::   forall (n :: Peano) inp out a.   ( ConstraintDIGLorentz n inp out a@@ -220,7 +255,7 @@     _example = dig @3  -- | Version of `dug` which uses Peano number.--- It is inteded for internal usage in Lorentz.+-- It is intended for internal usage in Lorentz. dugPeano ::   forall (n :: Peano) inp out a.   ( ConstraintDUGLorentz n inp out a@@ -315,9 +350,47 @@   => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s get = I GET +type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Kind.Type) =+  ( ConstraintGetN (ToPeano n) (ToT pair)+  , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)+  )++type family PairGetHs (ix :: Peano) (pair :: Kind.Type) :: Kind.Type where+  PairGetHs 'Z val                 = val+  PairGetHs ('S 'Z) (left, _)      = left+  PairGetHs ('S ('S n)) (_, right) = PairGetHs n right++pairGet+  :: forall (n :: GHC.Nat) (pair :: Kind.Type) (s :: [Kind.Type]).+     ConstraintPairGetLorentz n pair+  => pair : s :-> PairGetHs (ToPeano n) pair : s+pairGet = I (GETN (peanoSing @n))+  where+    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]+    _example = pairGet @1+ update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s update = I UPDATE +type ConstraintPairUpdateLorentz (n :: GHC.Nat) (val :: Kind.Type) (pair :: Kind.Type) =+  ( ConstraintUpdateN (ToPeano n) (ToT pair)+  , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)+  )++type family PairUpdateHs (ix :: Peano) (val :: Kind.Type) (pair :: Kind.Type) :: Kind.Type where+  PairUpdateHs 'Z          val _             = val+  PairUpdateHs ('S 'Z)     val (_, right)    = (val, right)+  PairUpdateHs ('S ('S n)) val (left, right) = (left, PairUpdateHs n val right)++pairUpdate+  :: forall (n :: GHC.Nat) (val :: Kind.Type) (pair :: Kind.Type) (s :: [Kind.Type]).+     ConstraintPairUpdateLorentz n val pair+  => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s+pairUpdate = I (UPDATEN (peanoSing @n))+  where+    _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]+    _example = pairUpdate @1+ if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s') if_ = iGenericIf IF @@ -387,7 +460,7 @@   )  -- | Version of `dipN` which uses Peano number.--- It is inteded for internal usage in Lorentz.+-- It is intended for internal usage in Lorentz. dipNPeano ::   forall (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.Type]).   ( ConstraintDIPNLorentz n inp out s s'@@ -403,8 +476,11 @@     _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]     _example = dipN @3 unit -failWith :: KnownValue a => a : s :-> t-failWith = FI FAILWITH+-- Since 008 it's prohibited to fail with non-packable values and with the+-- 'Contract t' type values, which is equivalent to our @NiceConstant@ constraint.+-- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.+failWith :: forall a s t. NiceConstant a => a : s :-> t+failWith = FI FAILWITH \\ niceConstantEvi @a  cast :: KnownValue a => (a : s :-> a : s) cast = I CAST@@ -524,7 +600,7 @@ ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s ge0 = I GE -int :: Natural : s :-> Integer : s+int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s int = I INT  -- | Get a reference to the current contract.@@ -653,6 +729,12 @@ balance :: s :-> Mutez : s balance = I BALANCE +votingPower :: KeyHash : s :-> Natural : s+votingPower = I VOTING_POWER++totalVotingPower :: s :-> Natural : s+totalVotingPower = I TOTAL_VOTING_POWER+ checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s checkSignature = I CHECK_SIGNATURE @@ -665,17 +747,18 @@ blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s blake2B = I BLAKE2B -{-# WARNING sha3 "Introduced by the Edo Protocol (008); This won't work on previous versions." #-} sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s sha3 = I SHA3 -{-# WARNING keccak "Introduced by the Edo Protocol (008); This won't work on previous versions." #-} keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s keccak = I KECCAK  hashKey :: PublicKey : s :-> KeyHash : s hashKey = I HASH_KEY +pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s+pairingCheck = I PAIRING_CHECK+ {-# WARNING source     "Using `source` is considered a bad practice.\n\ \    Consider using `sender` instead until further investigation" #-}@@ -691,10 +774,15 @@ chainId :: s :-> ChainId : s chainId = I CHAIN_ID -{-# WARNING level "Introduced by the Edo Protocol (008); This won't work on previous versions." #-} level :: s :-> Natural : s level = I LEVEL +selfAddress :: s :-> Address : s+selfAddress = I SELF_ADDRESS++never :: Never : s :-> s'+never = FI NEVER+ -- | Execute given instruction on truncated stack. -- -- This instruction requires you to specify the piece of stack to truncate@@ -721,20 +809,20 @@ failingWhenPresent   :: forall c k s v st e.      ( MemOpHs c, k ~ MemOpKeyHs c-     , KnownValue e+     , NiceConstant e      , st ~ (k : v : c : s)      )   => (forall s0. k : s0 :-> e : s0)   -> st :-> st failingWhenPresent mkErr =-  dip (dip dup # swap) # swap # dip dup # swap # mem #+  dupN @3 # dupN @2 # mem #   if_ (mkErr # failWith) nop  -- | 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-     , KnownValue e+     , NiceConstant e      )   => (forall s0. k : s0 :-> e : s0)   -> k : UpdOpParamsHs c : c : s :-> c : s
src/Lorentz/Macro.hs view
@@ -58,10 +58,8 @@   , assertUsing    -- * Syntactic Conveniences-  , ConstraintDuupXLorentz   , ConstraintReplaceNLorentz   , ConstraintUpdateNLorentz-  , DuupX (..)   , ReplaceN (..)   , UpdateN (..)   , dropX@@ -145,7 +143,7 @@ import Lorentz.Instr import Lorentz.Polymorphic import Lorentz.Value-import Michelson.Typed (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T)+import Michelson.Typed (ConstraintDIPN', ConstraintDUG', T) import Michelson.Typed.Arith import Michelson.Typed.Haskell.Value import Util.Markdown@@ -345,61 +343,17 @@   => a : s :-> CloneXT (ToPeano n) a s cloneX = cloneXImpl @(ToPeano n) --- | Kind-agnostic constraint for duupX-type DuupXConstraint' kind (n :: Peano)-  (s :: [kind]) (a :: kind) (s1 :: [kind]) (tail :: [kind]) =-  ( tail ~ Drop ('S n) s-  , ConstraintDIPN' kind n s s1 (a ': tail) (a ': a ': tail)-  , ConstraintDIG' kind n s1 (a ': s) a-  )---- | Constraint for duupX that combines kind-agnostic constraint for--- Lorentz (Haskell) types and for our typed Michelson.-type ConstraintDuupXLorentz (n :: Peano)-  (s :: [Kind.Type]) (a :: Kind.Type)-  (s1 :: [Kind.Type]) (tail :: [Kind.Type]) =-  ( DuupXConstraint' T n (ToTs s) (ToT a) (ToTs s1) (ToTs tail)-  , DuupXConstraint' Kind.Type n s a s1 tail-  )--class DuupX (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) s1 tail where-  duupXImpl :: s :-> a ': s--instance (s ~ (a ': xs)) => DuupX ('S 'Z) s a s1 tail where-  duupXImpl = dup--instance DuupX ('S ('S 'Z)) (b ': a ': xs) a s1 tail where-  duupXImpl = dip dup # swap--instance (ConstraintDuupXLorentz ('S ('S n)) s a s1 tail) =>-  DuupX ('S ('S ('S n))) s a s1 tail where-  duupXImpl =-    -- 'stackType' helps GHC deduce types-    dipNPeano @('S ('S n)) (dup # stackType @(a ': a ': tail)) #-    digPeano @('S ('S n))- -- | @DUU+P@ macro. For example, `duupX @3` is `DUUUP`, it puts -- the 3-rd (starting from 1) element to the top of the stack.--- Note that it is implemented differently for `n ≤ 2` and for `n > 2`.--- In the latter case it is implemented using `dipN`, `dig` and `dup`.--- In the former case it uses specialized versions.--- There is also a minor difference with the implementation of `DUU*P` in--- Michelson.--- They implement `DUUUUP` as `DIP 3 { DUP }; DIG 4`.--- We implement it as `DIP 3 { DUP }; DIG 3`. These are equivalent.--- Our version is supposedly cheaper, at least it should be packed--- more efficiently due to the way numbers are packed.-duupX :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).-  ( ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail-  , DuupX (ToPeano n) s a s1 tail-  )+--+-- Note that @DUU+P@ has since been added as the @DUP n@ instruction and so this+-- macro is defined simply as follows:+--+-- > duupX = dupN @n+duupX+  :: forall (n :: GHC.Nat) s s' a. ConstraintDUPNLorentz (ToPeano n) s s' a   => s :-> a ': s-duupX = duupXImpl @(ToPeano n) @s @a @s1 @tail-  where-    _example ::-      '[ Integer, (), Bool ] :->-      '[ Bool, Integer, (), Bool ]-    _example = duupX @3+duupX = dupN @n  -- | Version of 'framed' which accepts number of elements on input stack -- which should be preserved.@@ -491,7 +445,7 @@   --   -- As first argument accepts container name (for error message).   mapInsertNew-    :: (NiceComparable k, KnownValue e)+    :: (NiceComparable k, NiceConstant e)     => (forall s0. k : s0 :-> e : s0)     -> k : v : map k v : s :-> map k v : s @@ -520,7 +474,7 @@ -- -- As first argument accepts container name. setInsertNew-  :: (NiceComparable e, KnownValue err)+  :: (NiceComparable e, NiceConstant err)   => (forall s0. e : s0 :-> err : s0)   -> e : Set e : s :-> Set e : s setInsertNew desc = dip (push True) # failingWhenPresent desc # update@@ -699,7 +653,7 @@   -> View a r : storage : s :-> (List Operation, storage) : s view_ code =   unwrapView #-  unpair # dip (duupX @2) # code # dip amount #+  unpair # dip (dupN @2) # code # dip amount #   transferTokens # nil # swap # cons # pair  -- | @void@ type synonym as described in A1.@@ -808,7 +762,7 @@  void_   :: forall a b s s' anything.-      (IsError (VoidResult b), KnownValue b)+      (IsError (VoidResult b), NiceConstant b)   => a : s :-> b : s' -> Void_ a b : s :-> anything void_ code =   doc (DThrows (Proxy @(VoidResult b))) #@@ -848,17 +802,11 @@     push (FutureContract contractRef) # dup #     runFutureContract # ifNone onContractNotFound (dip drop) --- | Get address of the current contract.------ TODO [#373]: reimplement this using SELF_ADDRESS-selfAddress :: s :-> Address : s-selfAddress = self @() # address- -- | Duplicate two topmost items on top of the stack. dupTop2 ::   forall (a :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).   a ': b ': s :-> a ': b ': a ': b ': s-dupTop2 = duupX @2 # duupX @2+dupTop2 = dupN @2 # dupN @2  fromOption   :: (NiceConstant a)
src/Lorentz/Rebinded.hs view
@@ -117,7 +117,7 @@     fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r    PreserveArgsBinCondition condition -> \l r ->-    dip dup # swap # dip dup # swap #+    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
src/Lorentz/ReferencedByName.hs view
@@ -24,7 +24,7 @@  import Data.Constraint ((\\)) import qualified Data.Kind as Kind-import Data.Singletons (Sing, SingI)+import Data.Singletons (Sing) import Named (NamedF(..))  import Lorentz.ADT@@ -32,6 +32,7 @@ import Lorentz.Coercions import Lorentz.Instr import Michelson.Text+import Michelson.Typed import Util.Label import Util.Peano import Util.Type@@ -110,9 +111,14 @@   -- | 1-based position of the variable on stack.   varPosition :: VarPosition s name var +type ConstraintVarPosition s n =+  ( SingI n, KnownPeano n, n > 'Z ~ 'True+  , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n+  )+ data VarPosition (s :: [Kind.Type]) (name :: Symbol) (var :: Kind.Type) where   VarPosition-    :: (SingI n, KnownPeano n)+    :: (ConstraintVarPosition s n)     => (Sing (n :: Nat))     -> VarPosition s name var @@ -135,7 +141,7 @@  instance (ty ~ NamedF f var name) =>          ElemHasNamedVar (ty : s) name var 'True where-  elemVarPosition = VarPosition SZ+  elemVarPosition = VarPosition (SS SZ)  instance (HasNamedVar s name var) =>          ElemHasNamedVar (ty : s) name var 'False where@@ -154,18 +160,17 @@ -- -- @martoon: I'm not ready to fight the compiler regarding numerous -- complex constraints, so just assuring it that those constraints will hold.+--+-- @heitor.toledo: GHC doesn't seem to enjoy it that we use 'ConstraintDUPNLorentz',+-- so I replaced it with the expanded definition. dupLUnsafe   :: forall n s var.-     (SingI n, KnownPeano n)+     (ConstraintVarPosition s n)   => Sing (n :: Nat) -> s :-> var : s dupLUnsafe _ =-  -- generate dummy type variables-  case (Proxy, Proxy) of-    (_ :: Proxy s', _ :: Proxy (s0 :: [Kind.Type])) ->-      dipNPeano @n (dup :: var : s0 :-> var : var : s0) #-      digPeano @n-        \\ provideConstraintUnsafe @(ConstraintDIPNLorentz n s s' (var : s0) (var : var : s0))-        \\ provideConstraintUnsafe @(ConstraintDIGLorentz n s' (var : s) var)+  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)  -- | Version of 'dupL' that leaves a named variable on stack. dupLNamed@@ -184,20 +189,6 @@         (HasNamedVar s name var)      => Label name -> s :-> var : s dupL l = dupLNamed l # fromNamed l--{- Note about optimizations:--In @duupX@ we have several separate instances in order to optimize-"duupX @1" and "duupX @2" cases, but I'm not sure whether can we do the same-here and at the same time preserve sane error messages-(like "missing `HasNamedVar s name Integer` instance", without mentioning any internal-details).--Since we are already delving into severely deceving the type system here,-I think we'd better optimize those cases via adding respective rules in-our optimizer (that would be difficult to do in an honest way).---}  -- Samples ----------------------------------------------------------------------------
src/Lorentz/StoreClass.hs view
@@ -237,6 +237,15 @@     , sopInsert = \_label -> L.mapInsert     } +instance NiceComparable key => StoreHasSubmap (Set key) name key () where+  storeSubmapOps = StoreSubmapOps+    { sopMem = \_label -> L.mem+    , sopGet = \_label -> L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)+    , sopUpdate = \_label -> L.dip L.isSome # L.update+    , sopDelete = \_label -> L.setDelete+    , sopInsert = \_label -> L.dip L.drop # L.setInsert+    }+ ---------------------------------------------------------------------------- -- Stored Entrypoints ----------------------------------------------------------------------------
src/Lorentz/UParam.hs view
@@ -222,13 +222,13 @@       ArgumentUnpackFailed -> "UNPACK failed"  type instance ErrorArg "uparamNoSuchEntrypoint" = MText-type instance ErrorArg "uparamArgumentUnpackFailed" = ()+type instance ErrorArg "uparamArgumentUnpackFailed" = UnitErrorArg  instance Buildable (CustomError "uparamNoSuchEntrypoint") where-  build (CustomError _ name) = "No such entrypoint: " <> build name+  build (CustomError _ (_, name)) = "No such entrypoint: " <> build name  instance Buildable (CustomError "uparamArgumentUnpackFailed") where-  build (CustomError _ ()) = "UNPACK failed"+  build (CustomError _ (_, ())) = "UNPACK failed"  instance CustomErrorHasDoc "uparamNoSuchEntrypoint" where   customErrClass = ErrClassBadArgument
src/Lorentz/Value.hs view
@@ -2,6 +2,8 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +{-# LANGUAGE EmptyDataDeriving #-}+ -- | Re-exports typed Value, CValue, some core types, some helpers and -- defines aliases for constructors of typed values. --@@ -19,11 +21,15 @@   , Address   , EpAddress (..)   , Mutez+  , Never   , Timestamp   , ChainId   , KeyHash   , PublicKey   , Signature+  , Bls12381Fr+  , Bls12381G1+  , Bls12381G2   , Set   , Map   , M.BigMap (..)@@ -81,11 +87,26 @@ import Tezos.Core   (ChainId, Mutez, Timestamp, oneMutez, timestampFromSeconds, timestampFromUTCTime, timestampQuote,   toMutez, zeroMutez)-import Tezos.Crypto (KeyHash, PublicKey, Signature)+import Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature) import Util.CustomGeneric as ReExports import Util.Label (Label(..)) +import Lorentz.Annotation+ type List = []++data Never+  deriving stock (Generic, Show, Eq, Ord)+  deriving anyclass (IsoValue, NFData)++instance Buildable Never where+  build = \case++instance HasAnnotation Never where+  getAnnotation _ = M.starNotes++instance M.TypeHasDoc Never where+  typeDocMdDescription = "An uninhabited type."  -- | Provides 'Buildable' instance that prints Lorentz value via Michelson's -- 'Value'.