lorentz 0.13.4 → 0.14.0

raw patch · 33 files changed

+1337/−735 lines, 33 filesdep +singletons-basePVP ok

version bump matches the API change (PVP)

Dependencies added: singletons-base

API changes (from Hackage documentation)

Files

• CHANGES.md +43/−0
• lorentz.cabal +8/−4
• src/Lorentz.hs +2/−3
• src/Lorentz/Address.hs +3/−24
• src/Lorentz/Annotation.hs +3/−0
• src/Lorentz/Arith.hs +0/−58
• src/Lorentz/Base.hs +27/−19
• src/Lorentz/Bytes.hs +1/−1
• src/Lorentz/ContractRegistry.hs +1/−1
• src/Lorentz/CustomArith.hs +12/−0
• src/Lorentz/CustomArith/Common.hs +35/−0
• src/Lorentz/CustomArith/Conversions.hs +123/−0
• src/Lorentz/CustomArith/FixedArith.hs +380/−0
• src/Lorentz/CustomArith/RationalArith.hs +489/−0
• src/Lorentz/Doc.hs +13/−52
• src/Lorentz/Empty.hs +0/−59
• src/Lorentz/Entrypoints/Doc.hs +0/−5
• src/Lorentz/Entrypoints/Impl.hs +1/−2
• src/Lorentz/Errors.hs +1/−10
• src/Lorentz/Expr.hs +13/−3
• src/Lorentz/FixedArith.hs +0/−263
• src/Lorentz/Instr.hs +25/−18
• src/Lorentz/Iso.hs +1/−1
• src/Lorentz/Lambda.hs +34/−0
• src/Lorentz/Macro.hs +9/−7
• src/Lorentz/OpSize.hs +0/−35
• src/Lorentz/Rebinded.hs +0/−5
• src/Lorentz/Run.hs +34/−65
• src/Lorentz/Run/Simple.hs +6/−6
• src/Lorentz/StoreClass.hs +2/−1
• src/Lorentz/Util/TH.hs +67/−25
• src/Lorentz/Value.hs +1/−65
• src/Lorentz/Zip.hs +3/−3

@@ -1,6 +1,49 @@ <!-- Unreleased: append new entries here -->  +0.14.0+======+* [!1123](https://gitlab.com/morley-framework/morley/-/merge_requests/1123)+  Remove deprecated exports+* [!1169](https://gitlab.com/morley-framework/morley/-/merge_requests/1169)+  Support MIN_BLOCK_TIME instruction+  + Add the corresponding Lorentz `minBlockTime` instruction.+* [!1158](https://gitlab.com/morley-framework/morley/-/merge_requests/1158)+  Refactor (out) annotation checking support+  + `iWithVarAnnotations` removed.+  + Initial cast in lorentz contracts is redundant since annotations are+    ignored, hence it is removed.+  + Hence, `coDisableInitialCast` and `coDisableInitialCastL` are removed.+* [!1163](https://gitlab.com/morley-framework/morley/-/merge_requests/1163)+  Prohibit some operations in views+  + `ContractCode` is now a newtype wrapper instead of type synonym; this is+    required to avoid accidentally pasting contract code in views.+  + Lorentz lambdas are now newtype-wrapped with `WrappedLambda`, for the same+    reason.+  + `Lambda` is a type synonym for `WrappedLambda` with singleton input and+    output stacks.+  + The old `Lambda` synonym (which was a sequence of instructions with+    singleton i/o stacks) is renamed to `Fn`.+  + New "smart" constructors, `mkContractCode` and `mkLambda`, which conjure the+    required constraints.+* [!1153](https://gitlab.com/morley-framework/morley/-/merge_requests/1153)+  Remove 'OpSize' module.+* [!1114](https://gitlab.com/morley-framework/morley/-/merge_requests/1114)+  Update to ghc-9.0.2+* [!1108](https://gitlab.com/morley-framework/morley/-/merge_requests/1108)+  Remove support for the deprecated morley extensions+* [!1007](https://gitlab.com/morley-framework/morley/-/merge_requests/1007)+  Add `Rational` datatype in Lorentz and arithmetic operations with it+  + Move all custom arithmetics in Lorentz the a separate module+* [!1146](https://gitlab.com/morley-framework/morley/-/merge_requests/1146)+  Optimize `lmap` for `Maybe`.+* [!1111](https://gitlab.com/morley-framework/morley/-/merge_requests/1111)+  Add `errorDocArg`, deprecate `errorDoc`+  + Added `errorDocArg`, a quasi-quoter replacing `errorDoc`. The main+    difference is `errorDocArg` allows optionally specifying the error+    argument type.+  + Since `errorDocArg` subsumes `errorDoc`, the latter is deprecated.+ 0.13.4 ====== * [!1078](https://gitlab.com/morley-framework/morley/-/merge_requests/1078)

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           lorentz-version:        0.13.4+version:        0.14.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@@ -40,9 +40,13 @@       Lorentz.Constraints.Derivative       Lorentz.Constraints.Scopes       Lorentz.ContractRegistry+      Lorentz.CustomArith+      Lorentz.CustomArith.Common+      Lorentz.CustomArith.Conversions+      Lorentz.CustomArith.FixedArith+      Lorentz.CustomArith.RationalArith       Lorentz.Default       Lorentz.Doc-      Lorentz.Empty       Lorentz.Entrypoints       Lorentz.Entrypoints.Core       Lorentz.Entrypoints.Doc@@ -56,13 +60,12 @@       Lorentz.Expr       Lorentz.Ext       Lorentz.Extensible-      Lorentz.FixedArith       Lorentz.Instr       Lorentz.Iso+      Lorentz.Lambda       Lorentz.Layouts       Lorentz.Layouts.NonDupable       Lorentz.Macro-      Lorentz.OpSize       Lorentz.Pack       Lorentz.Polymorphic       Lorentz.Prelude@@ -156,6 +159,7 @@     , named     , optparse-applicative     , singletons+    , singletons-base     , template-haskell     , text     , text-manipulate

@@ -14,19 +14,18 @@ import Lorentz.Coercions as Exports import Lorentz.Common as Exports import Lorentz.Constraints as Exports+import Lorentz.CustomArith as Exports import Lorentz.Doc as Exports-import Lorentz.Empty as Exports import Lorentz.Entrypoints as Exports import Lorentz.Entrypoints.Doc as Exports import Lorentz.Errors as Exports import Lorentz.Errors.Numeric as Exports import Lorentz.Expr as Exports import Lorentz.Ext as Exports-import Lorentz.FixedArith as Exports import Lorentz.Instr as Exports import Lorentz.Iso as Exports+import Lorentz.Lambda as Exports (Lambda, WrappedLambda, mkLambda) import Lorentz.Macro as Exports-import Lorentz.OpSize as Exports import Lorentz.Pack as Exports import Lorentz.Polymorphic as Exports import Lorentz.Prelude as Exports

@@ -36,8 +36,6 @@   , asAddressOf_   , callingAddress   , callingDefAddress-  , callingTAddress-  , callingDefTAddress   , ToAddress (..)   , ToTAddress (..)   , ToTAddress_@@ -89,29 +87,10 @@ asAddressOf_ :: contract cp st vd -> Address : s :-> TAddress cp vd : s asAddressOf_ _ = I M.Nop --- | Turn 'TAddress' to 'ContractRef' in /Haskell/ world.+-- | Turn any typed address to 'ContractRef' in /Haskell/ world. -- -- This is an analogy of @address@ to @contract@ convertion in Michelson world, -- thus you have to supply an entrypoint (or call the default one explicitly).-callingTAddress-  :: forall cp vd mname.-     (NiceParameterFull cp)-  => TAddress cp vd-  -> Ep.EntrypointRef mname-  -> ContractRef (Ep.GetEntrypointArgCustom cp mname)-callingTAddress = callingAddress @cp @vd-{-# DEPRECATED callingTAddress "Use `callingAddress`" #-}---- | Specification of 'callingTAddress' to call the default entrypoint.-callingDefTAddress-  :: forall cp vd.-     (NiceParameterFull cp)-  => TAddress cp vd-  -> ContractRef (Ep.GetDefaultEntrypointArg cp)-callingDefTAddress taddr = callingTAddress taddr Ep.CallDefault-{-# DEPRECATED callingDefTAddress "Use `callingDefAddress`" #-}---- | Generalization of 'callingTAddress' to any typed address. callingAddress   :: forall cp vd addr mname.      (ToTAddress cp vd addr, NiceParameterFull cp)@@ -123,7 +102,7 @@   case Ep.parameterEntrypointCallCustom @cp epRef of     epc@M.EntrypointCall{} -> ContractRef addr (M.SomeEpc epc) --- | Generalization of 'callingDefTAddress' to any typed address.+-- | Specialization of 'callingAddress' to call the default entrypoint. callingDefAddress   :: forall cp vd addr.      (ToTAddress cp vd addr, NiceParameterFull cp)@@ -228,7 +207,7 @@          , NiceParameterFull cp, Ep.GetDefaultEntrypointArg cp ~ cp          ) =>          ToContractRef arg (TAddress cp vd) where-  toContractRef = callingDefTAddress+  toContractRef taddr = callingAddress @cp @vd taddr Ep.CallDefault  -- | Convert something from 'ContractRef' in /Haskell/ world. class FromContractRef (cp :: Type) (contract :: Type) where

@@ -146,6 +146,9 @@ instance HasAnnotation Address where   getAnnotation _ = starNotes +instance HasAnnotation TxRollupL2Address where+  getAnnotation _ = starNotes+ instance HasAnnotation EpAddress where   getAnnotation _ = starNotes 

@@ -10,7 +10,6 @@   , ToIntegerArithOpHs (..)   ) where -import GHC.TypeLits (type (+)) import Prelude hiding (natVal)  import Lorentz.Base@@ -112,21 +111,7 @@ instance (r ~ Bls12381G1) => ArithOpHs Add Bls12381G1 Bls12381G1 r instance (r ~ Bls12381G2) => ArithOpHs Add Bls12381G2 Bls12381G2 r -instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Integer r-instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Add Integer (Fixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Add Natural (Fixed p) r -instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) (NFixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) Integer r-instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Add Integer (NFixed p) r-instance (r ~ (NFixed p)) => ArithOpHs Add Natural (NFixed p) r--instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (NFixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) (Fixed p) r- instance (r ~ Integer) => ArithOpHs Sub Natural Integer r instance (r ~ Integer) => ArithOpHs Sub Integer Natural r instance (r ~ Integer) => ArithOpHs Sub Natural Natural r@@ -134,21 +119,6 @@ instance (r ~ Timestamp) => ArithOpHs Sub Timestamp Integer r instance (r ~ Integer) => ArithOpHs Sub Timestamp Timestamp r -instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (Fixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Integer r-instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (Fixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (Fixed p) r--instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (NFixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Integer r-instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (NFixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (NFixed p) r--instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (NFixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) r- instance (r ~ Integer) => ArithOpHs Mul Natural Integer r instance (r ~ Integer) => ArithOpHs Mul Integer Natural r instance (r ~ Natural) => ArithOpHs Mul Natural Natural r@@ -167,25 +137,6 @@ instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381Fr Bls12381G2 r where   evalArithOpHs = I (M.SWAP `M.Seq` M.MUL) -instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))-instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))-instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r-instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r-instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r--instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))-instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))-instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r-instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r-instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r-instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r--instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))-instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))-instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))-instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))- instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Natural Integer r instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Integer Natural r instance (r ~ Maybe (Natural, Natural)) => ArithOpHs EDiv Natural Natural r@@ -193,10 +144,6 @@ instance (r ~ Maybe (Natural, Mutez)) => ArithOpHs EDiv Mutez Mutez r instance (r ~ Maybe (Mutez, Mutez)) => ArithOpHs EDiv Mutez Natural r --instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r-instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r- instance UnaryArithOpHs Neg Integer where   type UnaryArithResHs Neg Integer = Integer instance UnaryArithOpHs Neg Natural where@@ -207,10 +154,6 @@   type UnaryArithResHs Neg Bls12381G1 = Bls12381G1 instance UnaryArithOpHs Neg Bls12381G2 where   type UnaryArithResHs Neg Bls12381G2 = Bls12381G2-instance UnaryArithOpHs Neg (Fixed p) where-  type UnaryArithResHs Neg (Fixed p) = (Fixed p)-instance UnaryArithOpHs Neg (NFixed p) where-  type UnaryArithResHs Neg (NFixed p) = (Fixed p)   instance (r ~ Natural) => ArithOpHs Or Natural Natural r@@ -274,5 +217,4 @@   evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Ge  instance ToIntegerArithOpHs Natural-instance ToIntegerArithOpHs (NFixed a) instance ToIntegerArithOpHs Bls12381Fr

@@ -16,7 +16,6 @@   , iNonFailingCode   , iMapAnyCode   , iForceNotFail-  , iWithVarAnnotations    , parseLorentzValue   , transformStringsLorentz@@ -26,21 +25,21 @@   , MapLorentzInstr (..)    , ContractOut-  , ContractCode+  , ContractCode (..)+  , mkContractCode+  , IsNotInView   , SomeContractCode (..)   , ViewCode   , Contract (..)   , toMichelsonContract-  , Lambda+  , Fn   ) where  import Data.Default (def)-import Data.List.NonEmpty qualified as NE (fromList) import Fmt (Buildable(..))  import Lorentz.Constraints import Morley.Micheline (ToExpression(..))-import Morley.Michelson.ErrorPos (InstrCallStack) import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf) import Morley.Michelson.Parser (MichelsonSource, ParserException, parseExpandValue) import Morley.Michelson.Preprocess (transformBytes, transformStrings)@@ -48,9 +47,10 @@ import Morley.Michelson.Text (MText) import Morley.Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue, typeCheckingWith) import Morley.Michelson.Typed-  (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,-  rfMerge)+  (Instr(..), IsNotInView, IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr,+  rfMapAnyInstr, rfMerge) import Morley.Michelson.Typed qualified as M (Contract)+import Morley.Michelson.Typed.Contract (giveNotInView) import Morley.Michelson.Untyped qualified as U  -- | Alias for instruction which hides inner types representation via @T@.@@ -103,15 +103,6 @@ iForceNotFail :: (i :-> o) -> (i :-> o) iForceNotFail = I . iAnyCode --- | Wrap Lorentz instruction with variable annotations, @annots@ list has to be--- non-empty, otherwise this function raises an error.-iWithVarAnnotations :: HasCallStack => [Text] -> inp :-> out -> inp :-> out-iWithVarAnnotations annots (LorentzInstr i) = case i of-  RfNormal instr -> LorentzInstr $ RfNormal $-    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr-  RfAlwaysFails instr -> LorentzInstr $ RfAlwaysFails $-    InstrWithVarNotes (NE.fromList $ map U.UnsafeAnnotation annots) instr- -- There is also @instance IsoValue (i :-> o)@ in the "Lorentz.Zip" module.  -- | Alias for ':->', seems to make signatures more readable sometimes.@@ -121,8 +112,14 @@ infixr 1 %>  type ContractOut st = '[([Operation], st)]-type ContractCode cp st = '[(cp, st)] :-> ContractOut st +-- | Wrap contract code capturing the constraint that the code is not inside a+-- view.+newtype ContractCode cp st = ContractCode+  { unContractCode :: '[(cp, st)] :-> ContractOut st }+  deriving stock (Show, Eq)+  deriving newtype NFData+ data SomeContractCode where   SomeContractCode     :: (NiceParameter cp, NiceStorage st)@@ -131,6 +128,10 @@  type ViewCode arg st ret = '[(arg, st)] :-> '[ret] +-- | A helper to construct 'ContractCode' that provides 'IsNotInView' constraint.+mkContractCode :: (IsNotInView => '[(cp, st)] :-> ContractOut st) -> ContractCode cp st+mkContractCode x = ContractCode $ giveNotInView x+ -- | Compiled Lorentz contract. -- -- Note, that the views argument (views descriptor) is added comparing to the@@ -179,7 +180,14 @@ FI l # _ = FI l infixl 8 # -type Lambda i o = '[i] :-> '[o]+-- | An instruction sequence taking one stack element as input and returning one+-- stack element as output. Essentially behaves as a Michelson lambda without+-- any additional semantical meaning.+--+-- The reason for this distinction is Michelson lambdas allow instructions+-- inside them that might be forbidden in the outer scope. This type doesn't add+-- any such conditions.+type Fn a b = '[a] :-> '[b]  -- | Errors that can happen during parsing into a Lorentz value. data ParseLorentzError@@ -214,7 +222,7 @@       first ParseLorentzTypecheckError .       typeCheckingWith def .       runTypeCheckIsolated .-      usingReaderT (def @InstrCallStack) .+      usingReaderT def .       typeCheckValue  -- | Lorentz version of 'transformStrings'.

@@ -43,7 +43,7 @@ import Lorentz.Value import Morley.AsRPC (HasRPCRepr(..)) import Morley.Michelson.Typed qualified as T-import Morley.Tezos.Crypto+import Morley.Tezos.Crypto hiding (Hash) import Morley.Tezos.Crypto.Hash qualified as Crypto  -- | Everything which is represented as bytes inside.

@@ -206,7 +206,7 @@     (ContractInfo{..}, _) <- getContract mName registry     let compiledContract  =           toMichelsonContract ciContract-    putTextLn $ pretty $ analyze $ M.cCode compiledContract+    putTextLn $ pretty $ analyze $ M.unContractCode $ M.cCode compiledContract   PrintStorage (SomeNiceStorage (storage :: st)) useMicheline ->     if useMicheline     then BS.putStrLn $ encodePretty $ toExpressionHelper storage

@@ -0,0 +1,12 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++module Lorentz.CustomArith+  ( module Exports+  ) where++import Lorentz.CustomArith.Common as Exports+import Lorentz.CustomArith.Conversions as Exports+import Lorentz.CustomArith.FixedArith as Exports+import Lorentz.CustomArith.RationalArith as Exports

@@ -0,0 +1,35 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++module Lorentz.CustomArith.Common+  ( -- * Arithmetic operations+    div+    -- * Lorentz casts+  , LorentzRounding (..)++    -- * Additional Arithmetic operations+  , Div++  ) where++import Prelude hiding (div)++import Lorentz.Arith+import Lorentz.Base++-- | Since Michelson doesn't support divide operation, we will use our own to represent+-- divison of Fixed and Rational values+data Div++-- | Operation that represents division of two values with a given result+div+  :: forall r n m s. ArithOpHs Div n m r+  => n : m : s :-> r : s+div = evalArithOpHs @Div++-- | Class that enables support of rounding operations for Lorentz non-integer values+class LorentzRounding a b where+  round_ :: a : s :-> b : s+  ceil_ :: a : s :-> b : s+  floor_ :: a : s :-> b : s

@@ -0,0 +1,123 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE NoApplicativeDo #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Lorentz.CustomArith.Conversions+ ( -- * Rational to Fixed/NFixed+   convertFixedToRational+ , convertNFixedToRational+ , convertRationalToFixed+ , convertRationalToNFixed+ , unsafeConvertRationalToNFixed++   -- * NRational to Fixed/NFixed+ , convertFixedToNRational+ , unsafeConvertFixedToNRational+ , convertNFixedToNRational+ , convertNRationalToFixed+ , convertNRationalToNFixed+ ) where++import Data.Fixed (HasResolution)+import Prelude (Maybe)++import Lorentz.CustomArith.FixedArith+import Lorentz.CustomArith.RationalArith++import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Errors+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Rebinded++convertRationalToNRational :: Rational : s :-> Maybe (NRational) : s+convertRationalToNRational = do+  dup; numerator+  ifGe0 (unsafeConvertRationalToNRational # some) (drop # none)++unsafeConvertRationalToNRational :: Rational : s :-> NRational : s+unsafeConvertRationalToNRational = deconstructRational # abs # constructRational++convertNRationalToRational :: NRational : s :-> Rational : s+convertNRationalToRational = deconstructRational # int # constructRational++----------------------------------------------------------------------------------------------------+-- Rationals+----------------------------------------------------------------------------------------------------++-- | Converts 'Rational' to 'Fixed' using value inside as numerator and base as denominator+convertFixedToRational :: forall a s. HasResolution a =>  Fixed a : s :-> Rational : s+convertFixedToRational = do+  coerceUnwrap+  push (resolution_ @a)+  swap+  constructRational++-- | Converts 'Rational' to 'NFixed' using value inside as numerator and base as denominator+convertNFixedToRational ::forall a s. HasResolution a => NFixed a : s :-> Rational : s+convertNFixedToRational = do+  coerceUnwrap; int+  push (resolution_ @a)+  swap+  constructRational++-- | Converts 'Fixed' to 'Rational' according to formulae: numerator * base / denominator+-- Note: Since result's base is determined by user, it is recommended to use higher value in order to achieve+-- better accuracy+convertRationalToFixed :: forall a s. HasResolution a => Rational : s :-> Fixed a : s+convertRationalToFixed = do+  deconstructRational+  push (resolution_ @a)+  mul+  ediv+  assertSome (Impossible @"Division by zero impossible")+  unpair+  add+  unsafeCoerceWrap++unsafeConvertRationalToNFixed :: forall a s. HasResolution a => Rational : s :-> NFixed a : s+unsafeConvertRationalToNFixed = convertRationalToFixed # unsafeCastFixedToNFixed++convertRationalToNFixed :: forall a s. HasResolution a => Rational : s :-> Maybe (NFixed a) : s+convertRationalToNFixed = convertRationalToFixed # castFixedToNFixed++----------------------------------------------------------------------------------------------------+-- NRationals+----------------------------------------------------------------------------------------------------+-- | Converts 'NRational' to 'Fixed'.+convertNRationalToFixed :: forall a s. HasResolution a => NRational : s :-> Fixed a : s+convertNRationalToFixed = convertNRationalToRational # convertRationalToFixed++-- | Converts 'NRational' to 'NFixed'.+convertNRationalToNFixed :: forall a s. HasResolution a => NRational : s :-> NFixed a : s+convertNRationalToNFixed = do+  deconstructRational+  push (resolution_ @a)+  mul+  ediv+  assertSome (Impossible @"Division by zero impossible")+  unpair+  add+  unsafeCoerceWrap++-- | Converts 'NFixed' to 'NRational'.+convertNFixedToNRational :: forall a s. HasResolution a => NFixed a : s :-> NRational : s+convertNFixedToNRational = do+  coerceUnwrap+  push (resolution_ @a)+  swap+  constructRational++-- | Converts 'Fixed' to 'NRational' if it is greater than zero. If not, returns 'Data.Maybe.Nothing'+convertFixedToNRational :: forall a s. HasResolution a => Fixed a : s :-> Maybe (NRational) : s+convertFixedToNRational = convertFixedToRational # convertRationalToNRational++-- | Converts 'Fixed' to 'NRational', using 'abs' on numerator.+unsafeConvertFixedToNRational :: forall a s. HasResolution a => Fixed a : s :-> NRational : s+unsafeConvertFixedToNRational = convertFixedToRational # unsafeConvertRationalToNRational

@@ -0,0 +1,380 @@+-- SPDX-FileCopyrightText: 2021 Oxhead Alpha+--+-- SPDX-License-Identifier: LicenseRef-MIT-OA++{-# LANGUAGE InstanceSigs #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Lorentz.CustomArith.FixedArith+  ( -- * Lorentz instructions+    castNFixedToFixed+  , castFixedToNFixed+  , unsafeCastFixedToNFixed+    -- * Typeclasses+  , LorentzFixedCast (..)+  , Fixed (..)+  , NFixed (..)++  -- * Support types and functions+  , DecBase (..)+  , BinBase (..)+  , resolution_++  ) where++import Data.Fixed (Fixed(..), HasResolution(..))+import GHC.Num qualified (fromInteger)+import GHC.TypeLits qualified as Lit+import Prelude hiding (and, compare, drop, natVal, some, swap)+import Prelude qualified as P+import Text.Show qualified++import Lorentz.Arith+import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints.Scopes+import Lorentz.CustomArith.Common+import Lorentz.Errors+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Value+import Morley.Michelson.Typed++import Unsafe qualified++{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}++-- | Datatypes, representing base of the fixed-point values+data DecBase p where+  DecBase :: KnownNat p => DecBase p+data BinBase p where+  BinBase :: KnownNat p => BinBase p++instance KnownNat p => HasResolution (DecBase p) where+  resolution _ = 10 ^ (Lit.natVal (Proxy @p))++instance KnownNat p => HasResolution (BinBase p) where+  resolution _ = 2 ^ (Lit.natVal (Proxy @p))++-- | Special function to get resolution without argument+resolution_ :: forall a. HasResolution a => Natural+resolution_ =+  let r = resolution (Proxy @a)+    in if r <= 0+       then error "Lorentz Rationals support only positive resolutions"+       else Unsafe.fromIntegral @Integer @Natural r+++-- | Like @Fixed@ but with a @Natural@ value inside constructor+newtype NFixed p = MkNFixed Natural deriving stock (Eq, Ord)++convertNFixedToFixed :: NFixed a -> Fixed a+convertNFixedToFixed (MkNFixed a) = MkFixed (Unsafe.fromIntegral @Natural @Integer a)++instance (HasResolution a) => Show (NFixed a) where+  show = show . convertNFixedToFixed++-- Note: This instances are copies of those in Data.Fixed for Fixed datatype+instance (HasResolution a) => Num (NFixed a) where+  (MkNFixed a) + (MkNFixed b) = MkNFixed (a + b)+  (MkNFixed a) - (MkNFixed b) = MkNFixed (a - b)+  fa@(MkNFixed a) * (MkNFixed b) = MkNFixed (P.div (a * b) (fromInteger (resolution fa)))+  negate (MkNFixed a) = MkNFixed (negate a)+  abs = id+  signum (MkNFixed a) = MkNFixed (signum a)+  fromInteger i = withResolution (\res -> MkNFixed ((fromInteger i) * res))++instance (HasResolution a) => Fractional (NFixed a) where+  fa@(MkNFixed a) / (MkNFixed b) = MkNFixed (P.div (a * (fromInteger (resolution fa))) b)+  recip fa@(MkNFixed a) = MkNFixed (P.div (res * res) a) where+      res = fromInteger $ resolution fa+  fromRational r = withResolution (\res -> MkNFixed (floor (r * (toRational res))))++instance IsoValue (NFixed p) where+  type ToT (NFixed p) = 'TNat+  toVal (MkNFixed x) = VNat x+  fromVal (VNat x) = MkNFixed x++instance Unwrappable (NFixed a) where+  type Unwrappabled (NFixed a) = Natural++-- Helpers copied from Data.Fixed, because they are not exported from there+withResolution :: forall a f. (HasResolution a) => (Natural -> f a) -> f a+withResolution foo = foo . fromInteger . resolution $ Proxy @a++------------------------------------------------------------------------------+-- Arithmetic operations' Insances+------------------------------------------------------------------------------++instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Add Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add Natural (Fixed p) r++instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) Integer r+instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Add Integer (NFixed p) r+instance (r ~ (NFixed p)) => ArithOpHs Add Natural (NFixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) (Fixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (Fixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (NFixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) r+++instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))+instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r++instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))+instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))+instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r+instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r+instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r++instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))+instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))++instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r+instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r++instance UnaryArithOpHs Neg (Fixed p) where+  type UnaryArithResHs Neg (Fixed p) = (Fixed p)+instance UnaryArithOpHs Neg (NFixed p) where+  type UnaryArithResHs Neg (NFixed p) = (Fixed p)++instance ToIntegerArithOpHs (NFixed a)++-- | Round is implemented using "banker's rounding" strategy, rounding half-way values+-- towards nearest even value+instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where+  round_ = roundingHelper @a @b Round 10+  ceil_ = roundingHelper @a @b Ceil 10+  floor_ = roundingHelper @a @b Floor 10++instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where+  round_ = roundingHelper @a @b Round 2+  ceil_ = roundingHelper @a @b Ceil 2+  floor_ = roundingHelper @a @b Floor 2++instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))+  => LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where+  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed+  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed+  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed++instance (KnownNat a, KnownNat b)+  => LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where+  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed+  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed+  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed++-- | Class that allows casting @Fixed@ values to Integer in vice versa+class LorentzFixedCast a where+  fromFixed :: a : s :-> Integer : s+  toFixed :: Integer : s :-> a : s++instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where+  fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s+  fromFixed = (round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) # forcedCoerce_+  toFixed = let pow :: Integer = 10 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (DecBase a))++instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where+  fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s+  fromFixed = (round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) # forcedCoerce_+  toFixed = let pow :: Integer = 2 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (BinBase a))++instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where+  fromFixed = castNFixedToFixed # fromFixed+  toFixed = toFixed # castFixedToNFixed # assertSome [mt|casting negative value to NFixed|]++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 10++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 2++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 10++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 2+++castNFixedToFixed :: NFixed p : s :-> Fixed p : s+castNFixedToFixed = int # forcedCoerce_++castFixedToNFixed :: Fixed p : s :-> Maybe (NFixed p) : s+castFixedToNFixed = coerceUnwrap # isNat # forcedCoerce_++unsafeCastFixedToNFixed ::  Fixed p : s :-> NFixed p : s+unsafeCastFixedToNFixed = coerceUnwrap # Lorentz.Instr.abs # forcedCoerce_++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 10++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 2++----------------------------------------------------------------------------+-- Helpers+----------------------------------------------------------------------------++data RoundingPattern = Round | Ceil | Floor++-- Note: Round is implemented using "banker's rounding" strategy, rounding half-way values+-- towards the nearest even value.+roundingHelper+  :: forall a b r1 r2 s.+    ( KnownNat a, KnownNat b+    , FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1)))+    , MichelsonCoercible r1 r2+    , Typeable (Unwrappabled r2)+    , IsoValue (Unwrappabled r2)+    , SingI (ToT (Unwrappabled r1))+    , Unwrappable r2+    , Unwrappable r1+    , ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)+    , ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)+    , ArithOpHs And (Unwrappabled r2) Natural Natural+    , ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))+    , ArithOpHs Mul Integer r1 r1+    )+  => RoundingPattern -> Natural -> (r1 : s :-> r2 : s)+roundingHelper rp base =+  let halfBase :: Natural = base `P.div` 2+      powDifference :: Integer = (Lit.natVal (Proxy @b)) - (Lit.natVal (Proxy @a))+      newPow :: Integer = fromIntegral $ 2 * halfNewPow+      halfNewPow :: Natural = halfBase * (base ^ (Prelude.abs powDifference - 1))+   in case () of+        _ | powDifference == 0 -> (forcedCoerce_ :: (r1 : s :-> r2 : s))+          | powDifference > 0 ->+              push newPow # mul # (forcedCoerce_ :: (r1 : s :-> r2 : s))+          | otherwise ->+              push newPow #+              swap #+              coerceUnwrap # ediv #+              assertSome (Impossible @"Division by zero impossible here") #+              case rp of+                Round ->+                  unpair #+                  swap #+                  push halfNewPow #+                  compare #+                  dup #+                  ifGe0 drop (+                    -- rem >= halfNewPow+                    dip (push (1 :: Natural)) #+                    -- if rem == halfNewPow, check if quot is odd+                    ifEq0 (dupN @2 # and) nop #+                    -- if quot is odd or rem > halfNewPow, add 1 to quot.+                    add+                   )+                Ceil ->+                  unpair #+                  swap #+                  ifNeq0 (push (1 :: Integer) # add) nop+                Floor -> car+              # unsafeCoerceWrap++fixedDivHelper+  :: forall t1 t2 t3 base b1 b2 a r s.+     ( KnownNat t1, KnownNat t2, KnownNat t3+     , Num base, NiceConstant base+     , Unwrappable r, Unwrappable b1, Unwrappable a+     , Unwrappabled a ~ base+     , ArithOpHs Mul base r r+     , ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))+     , IsoValue a, Typeable a+     )+  => base -> (r : b1 : s) :-> (Maybe a : s)+fixedDivHelper base =+  let powA = Lit.natVal (Proxy @t1)+      powB = Lit.natVal (Proxy @t2)+      powR = base ^ (Lit.natVal (Proxy @t3) - 1)+   in+     push powB #+     push powA #+     ifGt (push powR # mul) nop #+     dip coerceUnwrap #+     coerceUnwrap #+     ediv @_ @_ @(Maybe (base, b2)) #+     ifNone (none) (car # unsafeCoerceWrap # some)++edivHelper+  :: forall a base x y r1 r2 m s.+     ( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m+     , UnaryArithOpHs Eq' m, ArithOpHs Mul base y m+     , ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))+     , Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool+     )+  => base -> (x : y : s) :-> (Maybe (r1, r2) : s)+edivHelper base =+  let powA = base ^ (Lit.natVal (Proxy @a))+   in+     swap  #+     push powA #+     mul #+     dup #+     ifEq0 @m (dropN @2 # none)+     (+       swap #+       coerceUnwrap #+       ediv #+       assertSome (Impossible @"Division by zero impossible here") #+       unpair #+       dip unsafeCoerceWrap #+       pair #+       some+     )

@@ -0,0 +1,489 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE NoApplicativeDo #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}+{-# OPTIONS_GHC -Wno-orphans #-}++module Lorentz.CustomArith.RationalArith+  ( Rational+  , NRational++  -- * Common functions+  , oppositeRational+  , gcdEuclid+  , euclidExtendedNormalization+  , reduce+  , tripleMul++    -- * Constructor functions for Rational+  , mkRational+  , (%!)++   -- * Constructor functions for NRational+  , mkNRational+  , (%%!)++    -- * Rational specific typeclasses+  , LorentzRational++    -- * Constructors+  , mkRational_+  , numerator+  , denominator+  , constructRational+  , deconstructRational+  , uncheckedPairToRational+  , unsafePairToRational+  , pairToRational+  ) where++import Prelude (Either(..), Eq, Integer, Maybe, Natural, Show, Text, show, unsafe, ($), (++), (==))+import Text.Show qualified++import Lorentz.Annotation+import Lorentz.Arith+import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints.Scopes+import Lorentz.CustomArith.Common+import Lorentz.Errors+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Rebinded+import Morley.Michelson.Text+import Morley.Michelson.Typed+import Morley.Util.Named+import Morley.Util.Type++newtype Rational =+  UnsafeRational (Integer, Natural)+  deriving newtype (Eq)++infixl 7 %!+(%!) :: Integer -> Natural -> Rational+(%!) x y = unsafe $ mkRational (x, y)++mkRational :: (Integer, Natural) -> Either Text Rational+mkRational (x, y) = case y of+  0 -> Left $ "Attempt to construct Rational with zero denominator."+  _ -> Right $ UnsafeRational (x, y)++instance Show Rational where+  show (UnsafeRational (a, b)) = show a ++ " / " ++ show b++instance HasAnnotation Rational where+  getAnnotation _ = starNotes++instance IsoValue Rational where+  type ToT Rational = 'TPair 'TInt 'TNat+  toVal (UnsafeRational (a, b)) = VPair (VInt a, VNat b)+  fromVal (VPair (VInt a, VNat b)) = UnsafeRational (a, b)++instance Unwrappable Rational where+  type Unwrappabled Rational = (Integer, Natural)++newtype NRational =+  UnsafeNRational (Natural, Natural)+  deriving newtype (Eq)++mkNRational :: (Natural, Natural) -> Either Text NRational+mkNRational (x, y) = case y of+  0 -> Left "Attempt to construct NRational with zero denominator."+  _ -> Right $ UnsafeNRational (x, y)++infixl 7 %%!+(%%!) :: Natural -> Natural -> NRational+(%%!) x y = unsafe $ mkNRational (x, y)++instance Show NRational where+  show (UnsafeNRational (a, b)) = show a ++ " / " ++ show b++instance HasAnnotation NRational where+  getAnnotation _ = starNotes++instance IsoValue NRational where+  type ToT NRational = 'TPair 'TNat 'TNat+  toVal (UnsafeNRational (a, b)) = VPair (VNat a, VNat b)+  fromVal (VPair (VNat a, VNat b)) = UnsafeNRational (a, b)++instance Unwrappable NRational where+  type Unwrappabled NRational = (Natural, Natural)++class Unwrappable r => LorentzRational r where+  numerator :: Unwrappabled r ~ (a, Natural) => r : s :-> a : s+  numerator = coerceUnwrap # car++  denominator :: Unwrappabled r ~ (a, Natural) => r : s :-> Natural : s+  denominator = coerceUnwrap # cdr++  deconstructRational :: Unwrappabled r ~ (a, Natural) => r : s :-> a : Natural : s+  deconstructRational = coerceUnwrap # unpair++  constructRational :: Unwrappabled r ~ (a, Natural) => a : Natural : s :-> r : s+  constructRational = pair # uncheckedPairToRational++  unsafePairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s+  unsafePairToRational = unpair # dip (dup # assertNeq0 [mt|Attempt to construct rational with zero denominator|]) # pair # unsafeCoerceWrap++  uncheckedPairToRational :: Unwrappabled r ~ (a, Natural) => (a, Natural) : s :-> r : s+  uncheckedPairToRational = unsafeCoerceWrap++  pairToRational :: (Unwrappabled r ~ (a, Natural), KnownValue r) => (a, Natural) : s :-> Maybe r : s+  pairToRational = do+    unpair; swap+    dup+    ifEq0+      do+        dropN @2+        none+      do+        swap+        pair+        unsafeCoerceWrap+        some++  oppositeRational :: r : s :-> r : s++  reduce :: (KnownList s, KnownList (ToTs s)) => r : s :-> r : s++instance LorentzRational Rational where+  oppositeRational = do+    deconstructRational+    dup+    ifLt0 (dip neg) (dip int)+    abs+    swap+    constructRational+  reduce = reduceRationalHelper++instance LorentzRational NRational where+  oppositeRational = do+    deconstructRational+    swap+    constructRational+  reduce = reduceNRationalHelper++instance (r ~ Rational) => ArithOpHs Add Rational Integer r where+  evalArithOpHs = swap # add+instance (r ~ Rational) => ArithOpHs Add Integer Rational r where+  evalArithOpHs = addSubHelper add+instance (r ~ Rational) => ArithOpHs Add Rational Natural r where+  evalArithOpHs = swap # add+instance (r ~ Rational) => ArithOpHs Add Natural Rational r where+  evalArithOpHs = addSubHelper add+instance (r ~ Rational) => ArithOpHs Add Rational Rational r where+  evalArithOpHs = addSubRationalHelper add++instance (r ~ Rational) => ArithOpHs Sub Rational Integer r where+  evalArithOpHs = swap # sub # negRational+instance (r ~ Rational) => ArithOpHs Sub Integer Rational r where+  evalArithOpHs = addSubHelper sub+instance (r ~ Rational) => ArithOpHs Sub Rational Natural r where+  evalArithOpHs = swap # sub # negRational+instance (r ~ Rational) => ArithOpHs Sub Natural Rational r where+  evalArithOpHs = addSubHelper sub+instance (r ~ Rational) => ArithOpHs Sub Rational Rational r where+  evalArithOpHs = addSubRationalHelper sub++instance (r ~ Rational) => ArithOpHs Mul Rational Integer r where+  evalArithOpHs = swap # mul+instance (r ~ Rational) => ArithOpHs Mul Integer Rational r where+  evalArithOpHs = dip deconstructRational # mul # constructRational+instance (r ~ Rational) => ArithOpHs Mul Rational Natural r where+  evalArithOpHs = swap # mul+instance (r ~ Rational) => ArithOpHs Mul Natural Rational r where+  evalArithOpHs = dip deconstructRational # mul # constructRational++instance (r ~ Rational) => ArithOpHs Mul Rational Rational r where+  evalArithOpHs = mulRationalHelper @Rational @Rational @Rational++instance (r ~ Rational) => ArithOpHs Div Integer Rational r where+  evalArithOpHs = dip oppositeRational # mul+instance (r ~ Rational) => ArithOpHs Div Natural Rational r where+  evalArithOpHs = dip oppositeRational # mul+instance (r ~ Rational) => ArithOpHs Div Rational Integer r where+  evalArithOpHs = oppositeRational # mul # oppositeRational+instance (r ~ Rational) => ArithOpHs Div Rational Natural r where+  evalArithOpHs = oppositeRational # mul+instance (r ~ Rational) => ArithOpHs Div Rational Rational r where+  evalArithOpHs = dip oppositeRational # mul++instance (r ~ Rational) => ArithOpHs Add NRational Integer r where+  evalArithOpHs = swap # add+instance (r ~ Rational) => ArithOpHs Add Integer NRational r where+  evalArithOpHs = addSubHelper add+instance (r ~ NRational) => ArithOpHs Add NRational Natural r where+  evalArithOpHs = swap # add+instance (r ~ NRational) => ArithOpHs Add Natural NRational r where+  evalArithOpHs = addSubHelper add+instance (r ~ NRational) => ArithOpHs Add NRational NRational r where+  evalArithOpHs = addSubRationalHelper add++instance (r ~ Rational) => ArithOpHs Sub NRational Integer r where+  evalArithOpHs = swap # sub # negRational+instance (r ~ Rational) => ArithOpHs Sub Integer NRational r where+  evalArithOpHs = addSubHelper sub+instance (r ~ Rational) => ArithOpHs Sub NRational Natural r where+  evalArithOpHs = swap # sub # negRational+instance (r ~ Rational) => ArithOpHs Sub Natural NRational r where+  evalArithOpHs = addSubHelper sub+instance (r ~ Rational) => ArithOpHs Sub NRational NRational r where+  evalArithOpHs = addSubRationalHelper sub++instance (r ~ Rational) => ArithOpHs Mul NRational Integer r where+  evalArithOpHs = swap # mul+instance (r ~ Rational) => ArithOpHs Mul Integer NRational r where+  evalArithOpHs = dip deconstructRational # mul # constructRational+instance (r ~ NRational) => ArithOpHs Mul NRational Natural r where+  evalArithOpHs = swap # mul+instance (r ~ NRational) => ArithOpHs Mul Natural NRational r where+  evalArithOpHs = dip deconstructRational # mul # constructRational++instance (r ~ NRational) => ArithOpHs Mul NRational NRational r where+  evalArithOpHs = mulRationalHelper @NRational @NRational @NRational++instance (r ~ Rational) => ArithOpHs Div Integer NRational r where+  evalArithOpHs = dip oppositeRational # mul+instance (r ~ NRational) => ArithOpHs Div Natural NRational r where+  evalArithOpHs = dip oppositeRational # mul+instance (r ~ Rational) => ArithOpHs Div NRational Integer r where+  evalArithOpHs = oppositeRational # mul # oppositeRational+instance (r ~ NRational) => ArithOpHs Div NRational Natural r where+  evalArithOpHs = oppositeRational # mul+instance (r ~ NRational) => ArithOpHs Div NRational NRational r where+  evalArithOpHs = dip oppositeRational # mul++instance (r ~ Rational) => ArithOpHs Add Rational NRational r where+  evalArithOpHs = addSubRationalHelper add+instance (r ~ Rational) => ArithOpHs Add NRational Rational r where+  evalArithOpHs = addSubRationalHelper add+instance (r ~ Rational) => ArithOpHs Sub Rational NRational r where+  evalArithOpHs = addSubRationalHelper sub+instance (r ~ Rational) => ArithOpHs Sub NRational Rational r where+  evalArithOpHs = addSubRationalHelper sub+instance (r ~ Rational) => ArithOpHs Mul Rational NRational r where+  evalArithOpHs = mulRationalHelper @Rational @NRational @Rational+instance (r ~ Rational) => ArithOpHs Mul NRational Rational r where+  evalArithOpHs = mulRationalHelper @NRational @Rational @Rational+instance (r ~ Rational) => ArithOpHs Div Rational NRational r where+  evalArithOpHs = dip oppositeRational # mul+instance (r ~ Rational) => ArithOpHs Div NRational Rational r where+  evalArithOpHs = dip oppositeRational # mul+++instance {-# OVERLAPPABLE #-} ( LorentzRational r+         , Unwrappabled r ~ (a, Natural)+         , ArithOpHs EDiv a Natural (Maybe (a, Natural))+         , ArithOpHs Add a Natural a+         , ArithOpHs Add Natural a a+         ) => LorentzRounding r a where+  round_ = do+    deconstructRational; dip dup+    ediv @a @Natural @(Maybe (a, Natural)); assertSome (Impossible @"Division by zero impossible here")+    unpair+    dip do+      push (2 :: Natural)+      mul+      ifGt (push (1 :: Natural)) (push (0 :: Natural))+    add+  ceil_ = do+    deconstructRational+    ediv @a @Natural @(Maybe (a, Natural)); assertSome (Impossible @"Division by zero impossible here")+    unpair+    swap+    ifEq0 nop $ do+      push (1 :: Natural)+      add+  floor_ = do+    deconstructRational+    ediv @a @Natural @(Maybe (a, Natural)); assertSome (Impossible @"Division by zero impossible here")+    car++-- | Special multiplication helper, in case you want to multiply three 'Rational values'+-- given values @(a / b) * (c / d) * (e / f)@ performs @(a * c * e) / (b * d * f)@.+tripleMul :: forall r a s. (ArithOpHs Mul a a a, Unwrappabled r ~ (a, Natural), LorentzRational r) => r : r : r : s :-> r : s+tripleMul = do+  dip do+    dip deconstructRational+    deconstructRational+  deconstructRational+  dip (swap)+  dipN @3 (swap)+  dipN @2 (swap)+  mul @a @a @a; mul @a @a @a+  dip (do mul; mul)+  constructRational++----------------------------------------------------------------------------+-- Helpers+----------------------------------------------------------------------------++-- | For a given 'Natural' values, calculates their gcd, using Euclid algorithm.+gcdEuclid :: Natural : Natural : s :-> Natural : s+gcdEuclid = do+  dupTop2+  ifLt swap nop+  dupN @2+  neq0+  loop do+    dip dup+    ediv+    assertSome (Impossible @"Division by zero impossible here")+    cdr+    dup+    neq0+    dip swap+  dip drop++-- | Reduce 'Rational' value to the point, when numerator's and denominator's gcd is 1.+-- This operation should be commonly used after several arithmetic operations, because+-- numerator and denominator can become quite big. That in order, can lead to serious+-- gas consumption.+reduceRationalHelper :: (KnownList s, KnownList (ToTs s)) => Rational : s :-> Rational : s+reduceRationalHelper = do+  deconstructRational+  dup; ifLt0 (push (-1 :: Integer)) (push (1 :: Integer)); dug @2; abs;+  reduceHelper; dig @2; mul; pair; uncheckedPairToRational++reduceNRationalHelper :: NRational : s :-> NRational : s+reduceNRationalHelper = do+  deconstructRational+  reduceHelper;+  constructRational++reduceHelper :: Natural : Natural : s :-> Natural : Natural : s+reduceHelper = do+  dupTop2; gcdEuclid; dup; push (1 :: Natural)+  ifEq drop $ do+    dup; dug @3; swap;+    ediv; assertSome (Impossible @"Division by zero impossible here"); car; dug @2+    ediv; assertSome (Impossible @"Division by zero impossible here"); car+    swap++-- | Reduce 'Rational' value, using extended Euclid algorithm.+-- Consumes slightly more gas, than @reduce@, but contract with it is cheaper in terms of origination.+euclidExtendedNormalization :: forall s. (KnownList s, KnownList (ToTs s)) => Rational : s :-> Rational : s+euclidExtendedNormalization = do+  deconstructRational; dip int+  dipN @2 do+    push (1 :: Integer)+    push (0 :: Integer)+    push (0 :: Integer)+    push (1 :: Integer)+  swap; dup; neq0; dip swap;+  loop do+    dupTop2+    ediv+    assertSome (Impossible @"Division by zero impossible here")+    car+    dup+    dup+    dupN @9; mul; dig @7; sub; dug @2+    dupN @7; mul; dig @5; sub; swap+    dupN @5; mul; dig @3; sub+    dig @3; dig @4; dug @2; dipN @4 (swap)+    swap; dup; neq0; dip swap+  dropN @3; dip drop+  dup; ifLt0 (dip neg) (nop); abs; swap+  neg; pair; uncheckedPairToRational++addSubHelper+  :: forall a1 a2 a3 a4 a5 a6 b r s1 s2.+     (  b ~ Natural+     , NiceConstant a1+     , ArithOpHs Mul a2 a1 r+     , Unwrappable a3+     , Unwrappabled a3 ~ (a5, a1)+     , Unwrappabled a4 ~ (a6, Natural)+     , LorentzRational a4+     )+  => ((r : a5 : a1 : s1) :-> (a6 : b : s2))+  -> (a2 : a3 : s1) :-> (a4 : s2)+addSubHelper oper = do+  dip do+    coerceUnwrap+    unpair+    dupN @2+  mul+  oper+  pair+  uncheckedPairToRational++addSubRationalHelper+  :: forall a1 a2 a3 a4 a5 a6 a7 a8 r1 r2 r3 n m s1 s2.+    ( NiceConstant a1+    , NiceConstant a2+    , LorentzRational a7+    , r3 ~ Natural+    , ArithOpHs Mul a1 a3 r1, ArithOpHs Mul a2 a4 r2+    , ArithOpHs Mul n m r3, Unwrappable a5, Unwrappable a6+    , Unwrappabled a7 ~ (a8, r3)+    , Unwrappabled a5 ~ (a3, a2), Unwrappabled a6 ~ (a4, a1)+    )+  => ((r2 : r1 : a1 : a2 : s1) :-> (a8 : n : m : s2))+  -> (a6 : a5 : s1) :-> (a7 : s2)+addSubRationalHelper oper = do+  dip do+    coerceUnwrap+    unpair+  coerceUnwrap; unpair+  dip do+    dup+    dug @2+    mul+  dupN @4+  mul+  oper+  dip mul+  pair+  uncheckedPairToRational++mulRationalHelper+  :: forall r1 r2 r3 a b c s.+     ( LorentzRational r1+     , LorentzRational r2+     , LorentzRational r3+     , Unwrappabled r1 ~ (a, Natural)+     , Unwrappabled r2 ~ (b, Natural)+     , Unwrappabled r3 ~ (c, Natural)+     , ArithOpHs Mul a b c+     )+  => r1 : r2 : s :-> r3 : s+mulRationalHelper = do+  dip deconstructRational+  deconstructRational+  dip swap+  mul+  dip mul+  constructRational++negRational :: Rational : s :-> Rational : s+negRational = deconstructRational # neg # constructRational++mkRational_+  :: (forall s0. ErrInstr (("numerator" :! Integer, "denominator" :! Natural) : s0))+  -> Integer : Natural : s :-> Rational : s+mkRational_ onZeroDenominator = do+  swap+  dup+  ifEq0+    do+      toNamed #denominator+      swap+      toNamed #numerator+      pair+      onZeroDenominator+    do+      swap+      constructRational++type instance ErrorArg "zero_denominator" =+  ("numerator" :! Integer, "denominator" :! Natural)++instance CustomErrorHasDoc "zero_denominator" where+  customErrClass = ErrClassActionException+  customErrDocMdCause =+    "Attempt to construct rational with zero denominator."

@@ -7,13 +7,6 @@   ( doc   , docGroup   , dStorage-  , docStorage-  , buildLorentzDoc-  , buildLorentzDocWithGitRev-  , renderLorentzDoc-  , renderLorentzDocWithGitRev-  , contractName-  , contractGeneral   , contractGeneralDefault   , cutLorentzNonDoc @@ -95,13 +88,14 @@  import Lorentz.Base import Lorentz.Constraints+import Lorentz.Lambda import Lorentz.Value import Lorentz.ViewBase import Lorentz.Zip () import Morley.Michelson.Doc import Morley.Michelson.Optimizer import Morley.Michelson.Printer-import Morley.Michelson.Typed hiding (Contract)+import Morley.Michelson.Typed hiding (Contract, ContractCode, ContractCode'(..)) import Morley.Util.Generic import Morley.Util.Markdown import Morley.Util.Type@@ -118,34 +112,12 @@ docGroup :: DocItem di => (SubDoc -> di) -> (inp :-> out) -> (inp :-> out) docGroup gr = iMapAnyCode (DocGroup $ SomeDocItem . gr) --- | Insert documentation of the contract storage type. The type--- should be passed using type applications.-{-# DEPRECATED docStorage "Use `doc (dStorage @storage)` instead." #-}-docStorage :: forall storage s. TypeHasDoc storage => s :-> s-docStorage = doc $ DStorageType $ DType $ Proxy @storage---- | Give a name to given contract. Apply it to the whole contract code.-{-# DEPRECATED contractName "Use `docGroup name` instead." #-}-contractName :: Text -> (inp :-> out) -> (inp :-> out)-contractName name = docGroup (DName name)--{-# DEPRECATED buildLorentzDoc "Use 'buildDoc' instead." #-}-buildLorentzDoc :: inp :-> out -> ContractDoc-buildLorentzDoc = buildDocUnfinalized---- | Takes an instruction that inserts documentation items with--- general information about the contract. Inserts it into general--- section. See 'DGeneralInfoSection'.-{-# DEPRECATED contractGeneral "Use `docGroup DGeneralInfoSection` instead." #-}-contractGeneral :: (inp :-> out) -> (inp :-> out)-contractGeneral = docGroup DGeneralInfoSection- -- | Inserts general information about the contract using the default format. -- -- This includes git revision and some other information common -- for all contracts. -- Git revision is left unknown in the library code and is supposed--- to be updated in an executable using e.g. 'buildLorentzDocWithGitRev'.+-- to be updated in an executable using e.g. 'attachDocCommons'. contractGeneralDefault :: s :-> s contractGeneralDefault =   (docGroup DGeneralInfoSection $@@ -159,6 +131,12 @@ instance ContainsUpdateableDoc (i :-> o) where   modifyDocEntirely how = iMapAnyCode $ modifyDocEntirely how +instance ContainsDoc (ContractCode i o) where+  buildDocUnfinalized = buildDocUnfinalized . iAnyCode . unContractCode+instance ContainsUpdateableDoc (ContractCode i o) where+  modifyDocEntirely how (ContractCode x) = ContractCode $+    iMapAnyCode (modifyDocEntirely how) x+ instance ContainsDoc (Contract cp st vd) where   buildDocUnfinalized =     buildDocUnfinalized . cDocumentedCode@@ -166,22 +144,6 @@   modifyDocEntirely how c =     c{ cDocumentedCode = modifyDocEntirely how (cDocumentedCode c) } -{-# DEPRECATED buildLorentzDocWithGitRev-    "Use `buildDoc . attachDocCommons gitRev` instead."-  #-}-buildLorentzDocWithGitRev :: DGitRevision -> inp :-> out -> ContractDoc-buildLorentzDocWithGitRev gitRev = buildDoc . attachDocCommons gitRev--{-# DEPRECATED renderLorentzDoc "Use 'buildMarkdownDoc' instead." #-}-renderLorentzDoc :: inp :-> out -> LText-renderLorentzDoc = buildMarkdownDoc . finalizedAsIs--{-# DEPRECATED renderLorentzDocWithGitRev-    "Use `buildMarkdownDoc . attachDocCommons gitRev` instead."-  #-}-renderLorentzDocWithGitRev :: DGitRevision -> inp :-> out -> LText-renderLorentzDocWithGitRev gitRev = contractDocToMarkdown . buildLorentzDocWithGitRev gitRev- -- | Leave only instructions related to documentation. -- -- This function is useful when your method executes a lambda coming from outside,@@ -190,12 +152,11 @@ cutLorentzNonDoc :: (inp :-> out) -> (s :-> s) cutLorentzNonDoc (iAnyCode -> code) = I $ cutInstrNonDoc optimize code -instance Each [Typeable, ReifyList TypeHasDoc] [i, o] =>-         TypeHasDoc (i :-> o) where-  typeDocName _ = "Code (extended lambda)"+instance Each [Typeable, ReifyList TypeHasDoc] [i, o] => TypeHasDoc (WrappedLambda i o) where+  typeDocName _ = "WrappedLambda (extended lambda)"   typeDocMdReference tp wp =     let DocItemRef ctorDocItemId = docItemRef (DType tp)-        refToThis = mdLocalRef (mdTicked "Code") ctorDocItemId+        refToThis = mdLocalRef (mdTicked "WrappedLambda") ctorDocItemId     in applyWithinParens wp $       mconcat $ intersperse " " [refToThis, refToStack @i, refToStack @o]     where@@ -211,7 +172,7 @@           ]    typeDocMdDescription =-    "`Code i o` stands for a sequence of instructions which accepts stack \+    "`WrappedLambda i o` stands for a sequence of instructions which accepts stack \     \of type `i` and returns stack of type `o`.\n\n\     \When both `i` and `o` are of length 1, this primitive corresponds to \     \the Michelson lambda. In more complex cases code is surrounded with `pair`\

@@ -1,59 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA--{-# OPTIONS_GHC -Wno-orphans #-}---- | Support for uninhabited type.------ Note: this module exists solely for historical reasons since the time when--- 'Never' was not yet supported by the Michelson.------ TODO [#549]: remove this module.-module Lorentz.Empty-  ( Empty-  , absurd_-  ) where--import Fmt (Buildable(..))--import Lorentz.Annotation (HasAnnotation)-import Lorentz.Base-import Lorentz.Doc-import Lorentz.Errors-import Lorentz.Value-import Morley.AsRPC (HasRPCRepr(..))-import Morley.Michelson.Typed.Haskell.Doc---- | Replacement for uninhabited type.-{-# DEPRECATED Empty "Use Never type instead" #-}-newtype Empty = Empty ()-  deriving stock Generic-  deriving anyclass (IsoValue, HasAnnotation)--instance HasRPCRepr Empty where-  type AsRPC Empty = Empty--instance TypeHasDoc Empty where-  typeDocMdDescription =-    "Type which should never be constructed.\n\n\-    \If appears as part of entrypoint argument, this means that the entrypoint \-    \should never be called."---- | Someone constructed 'Empty' type.-type instance ErrorArg "emptySupplied" = UnitErrorArg--instance Buildable (CustomError "emptySupplied") where-  build (CustomError _ (_, ())) =-    "'Empty' value was passed to the contract."--instance CustomErrorHasDoc "emptySupplied" where-  customErrClass = ErrClassBadArgument-  customErrDocMdCause =-    "Value of type " <> typeDocMdReference (Proxy @Empty) (WithinParens False)-    <> " has been supplied."---- | Witness of that this code is unreachable.-absurd_ :: Empty : s :-> s'-absurd_ =-  failCustom_ #emptySupplied #-  doc (DDescription "Should never be called")

@@ -27,7 +27,6 @@   , ParamBuildingStep (..)   , mkPbsWrapIn   , clarifyParamBuildingSteps-  , constructDEpArg   , emptyDEpArg   , mkUType   , mkDEpUType@@ -369,10 +368,6 @@     -- constructor, and the second step (actual first) should be about wrapping     -- into @Service1@ constructor.   }--constructDEpArg :: forall arg. (NiceParameter arg, TypeHasDoc arg) => DEntrypointArg-constructDEpArg = mkDEntrypointArgSimple @arg-{-# DEPRECATED constructDEpArg "Use `mkDEntrypointArgSimple` instead" #-}  emptyDEpArg :: DEntrypointArg emptyDEpArg = DEntrypointArg

@@ -16,14 +16,13 @@   ) where  import Data.Singletons (withSingI)-import Data.Singletons.Prelude (SBool(SFalse, STrue))-import Data.Singletons.Prelude.Eq ((%==)) import Data.Vinyl.Core (Rec(..), (<+>)) import Data.Vinyl.Recursive (rmap) import Fcf (Eval, Exp) import Fcf qualified import GHC.Generics qualified as G import Morley.Util.TypeLits+import Prelude.Singletons (SBool(SFalse, STrue), (%==))  import Lorentz.Value import Morley.Michelson.Typed

@@ -53,7 +53,6 @@ import Data.List qualified as L import Fmt (Buildable, build, fmt, pretty, (+|), (|+)) import Language.Haskell.TH.Syntax (Lift)-import Text.Read (readsPrec)  import Lorentz.Base import Lorentz.Doc@@ -224,7 +223,7 @@ data Impossible (reason :: Symbol) = HasCallStack => Impossible  instance KnownSymbol reason => IsError (Impossible reason) where-  errorToVal Impossible = ($ toVal ())+  errorToVal Impossible cont = cont $ toVal ()   errorFromVal = error "Extracting impossible error"    failUsing err@Impossible =@@ -530,14 +529,6 @@   | ErrClassUnknown     -- ^ It's possible to leave error class unspecified.   deriving stock (Lift)--instance Read ErrorClass where-  readsPrec _ = \case-    "exception" -> [(ErrClassActionException, "")]-    "bad-argument" -> [(ErrClassBadArgument, "")]-    "contract-internal" -> [(ErrClassContractInternal, "")]-    "unknown" -> [(ErrClassUnknown, "")]-    _ -> []  instance Buildable ErrorClass where   build = \case

@@ -88,17 +88,20 @@   , (|:|)   , pairE   , (|@|)+  , (|%!|)   , listE   , transferTokensE   , createContractE   , viewE   ) where -import Prelude (HasCallStack, foldr, uncurry)+import Prelude (HasCallStack, foldr, uncurry, ($))  import Lorentz.Arith import Lorentz.Base import Lorentz.Constraints+import Lorentz.CustomArith+import Lorentz.Errors import Lorentz.Instr import Lorentz.Macro import Lorentz.Rebinded@@ -270,6 +273,12 @@ (|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b) (|@|) = binaryExpr pair +-- | Construct a 'Rational' value from a given nominator and denominator.+-- In case denominator is 0, fails with custom exception.+infixl 7 |%!|+(|%!|) :: Expr s0 s1 Integer -> Expr s1 s2 Natural -> Expr s0 s2 Rational+(|%!|) = binaryExpr $ mkRational_ (failCustom #zero_denominator)+ -- | An alias for '|@|'. -- -- @@@ -303,7 +312,7 @@ -- @amount@ expression, and stack changes in @amount@ expression affect -- stack changes in @contract@ expression. transferTokensE-  :: (NiceParameter p)+  :: (NiceParameter p, IsNotInView)   => ("arg" :! Expr s0 s1 p)   -> ("amount" :! Expr s1 s2 Mutez)   -> ("contract" :! Expr s2 s3 (ContractRef p))@@ -327,7 +336,8 @@ -- Note that this returns an operation, and pushes the address of the newly -- created contract as a side-effect. createContractE-  :: ("delegate" :! Expr s0 s1 (Maybe KeyHash))+  :: IsNotInView+  => ("delegate" :! Expr s0 s1 (Maybe KeyHash))   -> ("balance" :! Expr s1 s2 Mutez)   -> ("storage" :! Expr s2 s3 st)   -> ("contract" :! Contract p st vd)

@@ -1,263 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA--{-# LANGUAGE InstanceSigs #-}--- This option was enabled, because of-{-# OPTIONS_GHC -Wno-orphans #-}--module Lorentz.FixedArith-  ( -- * Lorentz instructions-    Lorentz.FixedArith.div-  , castNFixedToFixed-  , castFixedToNFixed--    -- * Lorentz casts-  , LorentzRounding (..)-  , LorentzFixedCast (..)--  ) where--import GHC.TypeLits qualified as Lit-import Prelude hiding (and, compare, drop, natVal, some, swap)-import Prelude qualified as P--import Lorentz.Arith-import Lorentz.Base-import Lorentz.Coercions-import Lorentz.Constraints.Scopes-import Lorentz.Errors-import Lorentz.Instr-import Lorentz.Macro-import Lorentz.Value-import Morley.Michelson.Typed.Arith-import Morley.Michelson.Typed.Scope--{-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}---- | Class that enables support of rounding operations for Lorentz non-integer values--- Note: Round is implemented using "banker's rounding" strategy, rounding half-way values--- towards nearest even value-class LorentzRounding a b where-  round_ :: a : s :-> b : s-  ceil_ :: a : s :-> b : s-  floor_ :: a : s :-> b : s--instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where-  round_ = roundingHelper @a @b Round 10-  ceil_ = roundingHelper @a @b Ceil 10-  floor_ = roundingHelper @a @b Floor 10--instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where-  round_ = roundingHelper @a @b Round 2-  ceil_ = roundingHelper @a @b Ceil 2-  floor_ = roundingHelper @a @b Floor 2--instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))-  => LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where-  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed-  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed-  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed--instance (KnownNat a, KnownNat b)-  => LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where-  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed-  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed-  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed---- | Class that allows casting @Fixed@ values to Integer in vice versa-class LorentzFixedCast a where-  fromFixed :: a : s :-> Integer : s-  toFixed :: Integer : s :-> a : s--instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where-  fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s-  fromFixed = (round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) # forcedCoerce_-  toFixed = let pow :: Integer = 10 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (DecBase a))--instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where-  fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s-  fromFixed = (round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) # forcedCoerce_-  toFixed = let pow :: Integer = 2 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (BinBase a))--instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where-  fromFixed = castNFixedToFixed # fromFixed-  toFixed = toFixed # castFixedToNFixed # assertSome [mt|casting negative value to NFixed|]---- | Since Michelson doesn't support divide operation, we will use our own to represent--- divison of Fixed and Rational values-data Div--instance ( KnownNat a-         , KnownNat b-         , KnownNat r-         ) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where-  evalArithOpHs = fixedDivHelper @a @b @r 10--instance ( KnownNat a-         , KnownNat b-         , KnownNat r-         ) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where-  evalArithOpHs = fixedDivHelper @a @b @r 2--instance ( KnownNat a-         , KnownNat b-         , KnownNat r-         ) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where-  evalArithOpHs = fixedDivHelper @a @b @r 10--instance ( KnownNat a-         , KnownNat b-         , KnownNat r-         ) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where-  evalArithOpHs = fixedDivHelper @a @b @r 2----- | Operation that represents division of two values with a given result-div-  :: forall r n m s. ArithOpHs Div n m r-  => n : m : s :-> r : s-div = evalArithOpHs @Div---castNFixedToFixed :: NFixed p : s :-> Fixed p : s-castNFixedToFixed = int # forcedCoerce_--castFixedToNFixed :: Fixed p : s :-> Maybe (NFixed p) : s-castFixedToNFixed = coerceUnwrap # isNat # forcedCoerce_--unsafeCastFixedToNFixed ::  Fixed p : s :-> NFixed p : s-unsafeCastFixedToNFixed = coerceUnwrap # Lorentz.Instr.abs # forcedCoerce_--instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where-  evalArithOpHs = edivHelper @a @Integer 10--instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where-  evalArithOpHs = edivHelper @a @Integer 10--instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where-  evalArithOpHs = edivHelper @a @Natural 2--instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where-  evalArithOpHs = edivHelper @a @Natural 2--instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where-  evalArithOpHs = edivHelper @a @Integer 10--instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where-  evalArithOpHs = edivHelper @a @Natural 10--instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where-  evalArithOpHs = edivHelper @a @Natural 2--instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where-  evalArithOpHs = edivHelper @a @Natural 2--------------------------------------------------------------------------------- Helpers-------------------------------------------------------------------------------data RoundingPattern = Round | Ceil | Floor--roundingHelper-  :: forall a b r1 r2 s.-    ( KnownNat a, KnownNat b-    , FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1)))-    , MichelsonCoercible r1 r2-    , Typeable (Unwrappabled r2)-    , IsoValue (Unwrappabled r2)-    , SingI (ToT (Unwrappabled r1))-    , Unwrappable r2-    , Unwrappable r1-    , ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)-    , ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)-    , ArithOpHs And (Unwrappabled r2) Natural Natural-    , ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))-    , ArithOpHs Mul Integer r1 r1-    )-  => RoundingPattern -> Natural -> (r1 : s :-> r2 : s)-roundingHelper rp base =-  let halfBase :: Natural = base `P.div` 2-      powDifference :: Integer = (Lit.natVal (Proxy @b)) - (Lit.natVal (Proxy @a))-      newPow :: Integer = fromIntegral $ 2 * halfNewPow-      halfNewPow :: Natural = halfBase * (base ^ (Prelude.abs powDifference - 1))-   in case () of-        _ | powDifference == 0 -> (forcedCoerce_ :: (r1 : s :-> r2 : s))-          | powDifference > 0 ->-              push newPow # mul # (forcedCoerce_ :: (r1 : s :-> r2 : s))-          | otherwise ->-              push newPow #-              swap #-              coerceUnwrap # ediv #-              assertSome (Impossible @"Division by zero impossible here") #-              case rp of-                Round ->-                  unpair #-                  swap #-                  push halfNewPow #-                  compare #-                  dup #-                  ifGe0 drop (-                    -- rem >= halfNewPow-                    dip (push (1 :: Natural)) #-                    -- if rem == halfNewPow, check if quot is odd-                    ifEq0 (dupN @2 # and) nop #-                    -- if quot is odd or rem > halfNewPow, add 1 to quot.-                    add-                   )-                Ceil ->-                  unpair #-                  swap #-                  ifNeq0 (push (1 :: Integer) # add) nop-                Floor -> car-              # unsafeCoerceWrap--fixedDivHelper-  :: forall t1 t2 t3 base b1 b2 a r s.-     ( KnownNat t1, KnownNat t2, KnownNat t3-     , Num base, NiceConstant base-     , Unwrappable r, Unwrappable b1, Unwrappable a-     , Unwrappabled a ~ base-     , ArithOpHs Mul base r r-     , ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))-     , IsoValue a, Typeable a-     )-  => base -> (r : b1 : s) :-> (Maybe a : s)-fixedDivHelper base =-  let powA = Lit.natVal (Proxy @t1)-      powB = Lit.natVal (Proxy @t2)-      powR = base ^ (Lit.natVal (Proxy @t3) - 1)-   in-     push powB #-     push powA #-     ifGt (push powR # mul) nop #-     dip coerceUnwrap #-     coerceUnwrap #-     ediv @_ @_ @(Maybe (base, b2)) #-     ifNone (none) (car # unsafeCoerceWrap # some)--edivHelper-  :: forall a base x y r1 r2 m s.-     ( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m-     , UnaryArithOpHs Eq' m, ArithOpHs Mul base y m-     , ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))-     , Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool-     )-  => base -> (x : y : s) :-> (Maybe (r1, r2) : s)-edivHelper base =-  let powA = base ^ (Lit.natVal (Proxy @a))-   in-     swap  #-     push powA #-     mul #-     dup #-     ifEq0 @m (dropN @2 # none)-     (-       swap #-       coerceUnwrap #-       ediv #-       assertSome (Impossible @"Division by zero impossible here") #-       unpair #-       dip unsafeCoerceWrap #-       pair #-       some-     )

@@ -102,6 +102,7 @@   , createContract   , implicitAccount   , now+  , minBlockTime   , amount   , balance   , votingPower@@ -144,6 +145,7 @@ import Lorentz.Bytes import Lorentz.Constraints import Lorentz.Entrypoints+import Lorentz.Lambda import Lorentz.Polymorphic import Lorentz.Value import Lorentz.ViewBase@@ -152,8 +154,9 @@   (ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG, ConstraintDUG',   ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN, EntrypointCallT(..), GetN,   Instr(..), RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, Value'(..), pattern CAR,-  pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)+  pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName) import Morley.Michelson.Typed.Arith+import Morley.Michelson.Typed.Contract (giveNotInView) import Morley.Michelson.Typed.Haskell.Value import Morley.Util.Named import Morley.Util.Peano@@ -418,10 +421,10 @@  lambda   :: ZipInstrs [i, o]-  => (i :-> o) -> (s :-> (i :-> o) : s)-lambda instr = case zippingStack instr of-  I l -> I (LAMBDA . VLam $ RfNormal l)-  FI l -> I (LAMBDA . VLam $ RfAlwaysFails l)+  => (IsNotInView => i :-> o) -> (s :-> WrappedLambda i o : s)+lambda instr = case zippingStack $ giveNotInView instr of+  I l -> I (LAMBDA $ VLam $ RfNormal l)+  FI l -> I (LAMBDA $ VLam $ RfAlwaysFails l)  exec :: a : Lambda a b : s :-> b : s exec = I EXEC@@ -434,12 +437,12 @@ execute   :: forall i o s.       (Each [KnownList, ZipInstr] [i, o])-  => ((i :-> o) : (i ++ s)) :-> (o ++ s)+  => (WrappedLambda i o : (i ++ s)) :-> (o ++ s) execute = framed @s $   dip (zipInstr @i) # swap # I EXEC # unzipInstr @o   where     _example-      :: ([Integer, Natural] :-> [(), ()]) : Integer : Natural : s+      :: (WrappedLambda [Integer, Natural] [(), ()]) : Integer : Natural : s       :-> () : () : s     _example = execute @@ -453,7 +456,7 @@ applicate   :: forall a b c inp2nd inpTail s.      (NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail))-  => a : (a : b :-> c) : s :-> (b :-> c) : s+  => a : WrappedLambda (a : b) c : s :-> WrappedLambda b c : s applicate = I APPLY \\ niceConstantEvi @a  dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')@@ -633,7 +636,7 @@   :: forall name ret arg s.     (HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret)   => arg : Address : s :-> Maybe ret : s-view' = I $ VIEW (demoteViewName @name) starNotes+view' = I $ VIEW (demoteViewName @name)   \\ niceViewableEvi @ret  -- | Get a reference to the current contract.@@ -650,7 +653,7 @@ -- If you are going to call a specific entrypoint of the contract, see 'selfCalling'. self   :: forall p s.-      (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p)+      (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p, IsNotInView)   => s :-> ContractRef p : s self = I (SELF $ sepcCallRootChecked @p) \\ niceParameterEvi @p @@ -661,7 +664,7 @@ -- explicitly. selfCalling   :: forall p mname s.-     (NiceParameterFull p)+     (NiceParameterFull p, IsNotInView)   => EntrypointRef mname   -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s selfCalling epRef = I $@@ -682,7 +685,7 @@       , ToTAddress_ p vd addr       )   => addr : s :-> Maybe (ContractRef p) : s-contract = I (CONTRACT starNotes epName) \\ niceParameterEvi @p+contract = I (CONTRACT epName) \\ niceParameterEvi @p   where     epName = sepcName (sepcCallRootChecked @p) @@ -698,7 +701,7 @@   -> addr : s :-> Maybe (ContractRef epArg) : s contractCalling epRef = I $   case useHasEntrypointArg @cp @epRef @epArg epRef of-    (Dict, epName) -> CONTRACT starNotes epName+    (Dict, epName) -> CONTRACT epName  -- | Specialized version of 'contractCalling' for the case when you do -- not have compile-time evidence of appropriate 'HasEntrypointArg'.@@ -730,18 +733,19 @@   :: forall p s. (NiceParameter p)   => EpAddress : s :-> Maybe (ContractRef p) : s epAddressToContract =-  I (CONTRACT starNotes DefEpName) \\ niceParameterEvi @p+  I (CONTRACT DefEpName) \\ niceParameterEvi @p  transferTokens-  :: forall p s. (NiceParameter p)+  :: forall p s. (NiceParameter p, IsNotInView)   => p : Mutez : ContractRef p : s :-> Operation : s transferTokens = I $ TRANSFER_TOKENS \\ niceParameterEvi @p -setDelegate :: Maybe KeyHash : s :-> Operation : s+setDelegate :: IsNotInView => Maybe KeyHash : s :-> Operation : s setDelegate = I SET_DELEGATE  createContract-  :: forall p g vd s. Contract p g vd+  :: forall p g vd s. IsNotInView+  => Contract p g vd   -> Maybe KeyHash : Mutez : g : s   :-> Operation : TAddress p vd : s createContract cntrc@Contract{} =@@ -755,6 +759,9 @@ now :: s :-> Timestamp : s now = I NOW +minBlockTime :: s :-> Natural : s+minBlockTime = I MIN_BLOCK_TIME+ amount :: s :-> Mutez : s amount = I AMOUNT @@ -891,4 +898,4 @@   lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)  instance LorentzFunctor Maybe where-  lmap f = ifNone none (f # some)+  lmap = map

@@ -34,7 +34,7 @@  -- | Given a function that is its own inverse, make an 'LIso' using it -- in both directions.-involutedIso :: Lambda a a -> LIso a a+involutedIso :: Fn a a -> LIso a a involutedIso l = LIso (framed l) (framed l)  -- | The isomorphism between two values with identical representation

@@ -0,0 +1,34 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++module Lorentz.Lambda+  ( WrappedLambda(..)+  , Lambda+  , mkLambda+  ) where++import Lorentz.Annotation+import Lorentz.Base+import Morley.AsRPC (HasRPCRepr(..))+import Morley.Michelson.Typed+import Morley.Michelson.Typed.Contract (giveNotInView)++-- | A helper type to construct Lorentz lambda values; Use this for lambda+-- values outside of Lorentz contracts or with @push@.+--+-- The primary reason this is a newtype and not a type synonym is to avoid+-- accidentally splicing the output of 'mkLambda' in-line.+newtype WrappedLambda i o = WrappedLambda {unWrappedLambda :: i :-> o}+  deriving stock (Show, Eq)++deriving newtype instance IsoValue (a :-> b) => IsoValue (WrappedLambda a b)+deriving newtype instance HasAnnotation (i :-> o) => HasAnnotation (WrappedLambda i o)+deriving newtype instance HasRPCRepr (i :-> o) => HasRPCRepr (WrappedLambda i o)++-- | A constructor providing the required constraint for 'WrappedLambda'. This is+-- the only way to construct a lambda that uses operations forbidden in views.+mkLambda :: (IsNotInView => i :-> o) -> WrappedLambda i o+mkLambda i = WrappedLambda $ giveNotInView i++-- | A type synonym representing Michelson lambdas.+type Lambda i o = WrappedLambda '[i] '[o]

@@ -147,6 +147,7 @@ import Lorentz.Errors import Lorentz.Ext (stackType) import Lorentz.Instr+import Lorentz.Lambda import Lorentz.Polymorphic import Lorentz.Value import Lorentz.ViewBase@@ -391,7 +392,8 @@ -- >>> framedN @1 (drop # drop) -$ arg -- ... -- ... error:--- ... Couldn't match type ‘'[]’ with ‘Integer : o'0’+-- ... Couldn't match type: '[]+-- ...                with: a0 : o'0 -- ... -- -- When the number of elements is larger than the size of the stack, @framedN@@@ -403,8 +405,8 @@ -- >>> framedN @5 (drop # drop # drop # drop) -$ arg -- ... -- ... error:--- ... Couldn't match type ‘Integer’--- ... with ‘ZippedStackRepr a0 (ZippedStackRepr a1 out)’+-- ... Couldn't match type ‘ZippedStackRepr a0 (ZippedStackRepr a1 out)’+-- ... with ‘Integer’ -- ...  framedN@@ -837,7 +839,7 @@ unwrapView_ = forcedCoerce_  view_ ::-     (NiceParameter r, Dupable storage)+     (NiceParameter r, Dupable storage, IsNotInView)   => (forall s0. a : storage : s0 :-> r : s0)   -> View_ a r : storage : s :-> (List Operation, storage) : s view_ code =@@ -950,7 +952,7 @@   fromVal = error "impossible"  mkVoid :: forall b a. a -> Void_ a b-mkVoid a = Void_ a nop+mkVoid a = Void_ a (mkLambda nop)  void_   :: forall a b s s' anything.@@ -958,7 +960,7 @@   => a : s :-> b : s' -> Void_ a b : s :-> anything void_ code =   doc (DThrows (Proxy @(VoidResult b))) #-  forcedCoerce_ @_ @(_, Lambda b b) #+  unwrapVoid #   unpair # swap # dip code # swap # exec #   push voidResultTag # pair # failWith @(MText, b) @@ -1028,7 +1030,7 @@ -- Nothing non'   :: (NiceConstant a)-  => Lambda a Bool -> a : s :-> Maybe a : s+  => ('[a] :-> '[Bool]) -> a : s :-> Maybe a : s non' p = dup # framed p # if_ (drop # none) some  -- | Check whether container is empty.

@@ -1,35 +0,0 @@--- SPDX-FileCopyrightText: 2021 Oxhead Alpha--- SPDX-License-Identifier: LicenseRef-MIT-OA---- | Operation size evaluation.-module Lorentz.OpSize-  ( OpSize (..)-  , T.opSizeHardLimit-  , T.smallTransferOpSize--  , contractOpSize-  , valueOpSize-  ) where--import Data.Constraint ((\\))--import Lorentz.Constraints-import Lorentz.Run-import Lorentz.Value-import Morley.Michelson.Typed (OpSize)-import Morley.Michelson.Typed qualified as T---- | Estimate code operation size.-contractOpSize :: Contract cp st vd -> OpSize-contractOpSize =-  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).--}---- | Estimate value operation size.-valueOpSize :: forall a. (NiceUntypedValue a) => a -> OpSize-valueOpSize =-  T.valueOpSize . toVal-  \\ niceUntypedValueEvi @a

@@ -69,8 +69,6 @@    IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)          => Condition (a ': s) s s o o-  IsNotZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)-         => Condition (a ': s) s s o o    IsEq :: NiceComparable a => Condition (a ': a ': s) s s o o   IsNeq :: NiceComparable a => Condition (a ': a ': s) s s o o@@ -115,7 +113,6 @@     Not cond -> \l r -> ifThenElse cond r l      IsZero -> \l r -> eq0 # if_ l r-    IsNotZero -> \l r -> eq0 # if_ r l      IsEq -> ifEq     IsNeq -> ifNeq@@ -135,8 +132,6 @@         -- 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'. --

@@ -46,7 +46,6 @@   , setViewsRec   , noViews   , cdCodeL-  , coDisableInitialCastL   , cdCompilationOptionsL    , interpretLorentzInstr@@ -75,10 +74,9 @@ import Morley.Michelson.Interpret import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf) import Morley.Michelson.Text (MText)-import Morley.Michelson.TypeCheck (typeCheckingWith, typeVerifyContract, typeVerifyView)-import Morley.Michelson.Typed-  (Instr(..), IsoValue, IsoValuesStack(..), ToT, ToTs, convertContract, convertView, starParamNotes)+import Morley.Michelson.Typed (Instr(..), IsoValue, IsoValuesStack(..), ToTs) import Morley.Michelson.Typed qualified as M+import Morley.Michelson.Typed.Contract (giveNotInView) import Morley.Michelson.Untyped qualified as U (canonicalEntriesOrder) import Morley.Util.Lens import Morley.Util.TypeLits@@ -92,12 +90,6 @@   -- ^ 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.@@ -106,7 +98,6 @@   { coOptimizerConf = Just def   , coStringTransformer = (False, id)   , coBytesTransformer = (False, id)-  , coDisableInitialCast = False   }  -- | Leave contract without any modifications. For testing purposes.@@ -115,7 +106,6 @@   { coOptimizerConf = Nothing   , coStringTransformer = (False, id)   , coBytesTransformer = (False, id)-  , coDisableInitialCast = False   }  -- | For use outside of Lorentz. Will use 'defaultCompilationOptions'.@@ -135,9 +125,9 @@ -- This is an alias for 'mkContract'. defaultContract   :: (NiceParameterFull cp, NiceStorageFull st)-  => ContractCode cp st -> Contract cp st ()+  => (IsNotInView => '[(cp, st)] :-> ContractOut st) -> Contract cp st () defaultContract code =-  compileLorentzContract $ ContractData code mempty defaultCompilationOptions+  compileLorentzContract $ defaultContractData code  -- | Construct and compile Lorentz contract. --@@ -205,9 +195,9 @@ -- | Compile contract with 'defaultCompilationOptions'. defaultContractData   :: forall cp st. (NiceParameterFull cp, NiceStorageFull st)-  => ContractCode cp st -> ContractData cp st ()+  => (IsNotInView => '[(cp, st)] :-> ContractOut st) -> ContractData cp st () defaultContractData code = ContractData-  { cdCode = code+  { cdCode = mkContractCode code   , cdViews = RNil   , cdCompilationOptions = defaultCompilationOptions   }@@ -215,27 +205,15 @@ -- | Compile a whole contract to Michelson. -- -- Note that compiled contract can be ill-typed in terms of Michelson code--- when some of the compilation options are used (e.g. when 'coDisableInitialCast'--- is @True@, resulted contract can be ill-typed).+-- when some of the compilation options are used. -- However, compilation with 'defaultCompilationOptions' should be valid. compileLorentzContract   :: forall cp st vd. ContractData cp st vd -> Contract cp st vd compileLorentzContract ContractData{..} = Contract{..}   where-    verify = typeVerifyContract @(ToT cp) @(ToT st) (convertContract cMichelsonContractRaw)-    cMichelsonContract-      | cpNotes == starParamNotes || coDisableInitialCast cdCompilationOptions-      -- If contract parameter type has no annotations or explicitly asked, we drop CAST.-      = cMichelsonContractRaw-      | Right{} <- typeCheckingWith def verify = cMichelsonContractRaw-      -- Check if the contract typechecks-      | otherwise-      -- Perform CAST if it doesn't-      = cMichelsonContractRaw-          { M.cCode = compileLorentzWithOptions-              cdCompilationOptions (I CAST # cdCode :: ContractCode cp st) }-    cMichelsonContractRaw = M.Contract-      { cCode = compileLorentzWithOptions cdCompilationOptions cdCode+    cMichelsonContract = M.Contract+      { cCode = M.ContractCode $+          compileLorentzWithOptions cdCompilationOptions $ unContractCode cdCode       , cParamNotes = cpNotes       , cStoreNotes = getAnnotation @st NotFollowEntrypoint       , cEntriesOrder = U.canonicalEntriesOrder@@ -243,12 +221,13 @@       } \\ niceParameterEvi @cp         \\ niceStorageEvi @st -    cDocumentedCode =-      finalizeParamCallingDoc' (Proxy @cp) cdCode #-      foldr (#) (I Nop)-        ( Rec.recordToList $-           Rec.rmap (\(ContractView code) -> Rec.Const $ fakeCoercing code) cdViews-        )+    cDocumentedCode = case cdCode of+      ContractCode x -> ContractCode $+        finalizeParamCallingDoc' (Proxy @cp) x #+        foldr (#) (I Nop)+          ( Rec.recordToList $+            Rec.rmap (\(ContractView code) -> Rec.Const $ fakeCoercing code) cdViews+          )      cpNotes = parameterEntrypointsToNotes @cp @@ -269,7 +248,7 @@   in case M.mkViewsSet viewsList of       Right viewsSet -> viewsSet       Left e@M.DuplicatedViewName{} ->-        error $ "An impossble happened: " +| e |+ ""+        error $ "An impossible happened: " +| e |+ ""  -- | Compile a single view. compileLorentzView@@ -280,25 +259,14 @@   -> M.SomeView (M.ToT st) compileLorentzView co (ContractView viewCode)   | (_ :: Proxy ('ViewTyInfo name arg ret)) <- Proxy @vt =-    let argNotes = getAnnotation @arg NotFollowEntrypoint-        retNotes = getAnnotation @ret NotFollowEntrypoint-        stNotes = getAnnotation @ret NotFollowEntrypoint-        verify = typeVerifyView @(ToT arg) @(ToT st) @(ToT ret) stNotes (convertView viewRaw)-        viewRaw, viewWithNecessaryCast :: M.View (ToT arg) (ToT st) (ToT ret)-        viewRaw = M.View-          { M.vName = demoteViewName @name-          , M.vArgument = argNotes-          , M.vReturn = retNotes-          , M.vCode = compileLorentzWithOptions co viewCode-          }-          \\ niceViewableEvi @arg-          \\ niceViewableEvi @ret-        viewWithNecessaryCast-          | argNotes == M.starNotes || coDisableInitialCast co = viewRaw-          | Right{} <- typeCheckingWith def verify = viewRaw-          | otherwise = viewRaw {-              M.vCode = compileLorentzWithOptions co (I CAST # viewCode :: ViewCode arg st ret) }-    in M.SomeView viewWithNecessaryCast+      M.SomeView M.View+        { M.vName = demoteViewName @name+        , M.vArgument = getAnnotation @arg NotFollowEntrypoint+        , M.vReturn = getAnnotation @ret NotFollowEntrypoint+        , M.vCode = compileLorentzWithOptions co viewCode+        }+        \\ niceViewableEvi @arg+        \\ niceViewableEvi @ret  {- | Set all the contract's views. @@ -346,18 +314,18 @@ interpretLorentzInstr   :: (IsoValuesStack inp, IsoValuesStack out)   => ContractEnv-  -> inp :-> out+  -> (IsNotInView => inp :-> out)   -> Rec Identity inp   -> Either MichelsonFailureWithStack (Rec Identity out)-interpretLorentzInstr env (compileLorentz -> instr) inp =-  fromValStack <$> interpretInstr env instr (toValStack inp)+interpretLorentzInstr env instr inp =+  fromValStack <$> interpretInstr env (compileLorentz $ giveNotInView instr) (toValStack inp) --- | Like 'interpretLorentzInstr', but works on lambda rather than--- arbitrary instruction.+-- | Like 'interpretLorentzInstr', but works on singleton input and output+-- stacks. interpretLorentzLambda   :: (IsoValue inp, IsoValue out)   => ContractEnv-  -> Lambda inp out+  -> (IsNotInView => Fn inp out)   -> inp   -> Either MichelsonFailureWithStack out interpretLorentzLambda env instr inp = do@@ -370,7 +338,8 @@     buildDocUnfinalized . compileLorentzContract instance ContainsUpdateableDoc (ContractData cp st vd) where   modifyDocEntirely how c =-    c{ cdCode = modifyDocEntirely how (cdCode c) }+    c{ cdCode = case cdCode c of+        ContractCode x -> ContractCode $ modifyDocEntirely how x }  -- | Lorentz version of analyzer. analyzeLorentz :: inp :-> out -> AnalyzerRes

@@ -42,7 +42,7 @@ -- For testing and demonstration purposes. infixr 2 -$? (-$?) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)-      => (inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailureWithStack out+      => (IsNotInView => inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailureWithStack out code -$? inp = interpretLorentzLambda dummyContractEnv (unzipInstr # code) inp  -- | Like @'-$?'@, assumes that no failure is possible.@@ -63,7 +63,7 @@ -- 6 infixr 2 -$ (-$) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)-     => inps :-> '[out] -> ZippedStack inps -> out+     => (IsNotInView => inps :-> '[out]) -> ZippedStack inps -> out code -$ inp = unsafe $ code -$? inp  ----------------------------------------------------------------------------@@ -73,14 +73,14 @@ -- | Version of (-$?) with arguments flipped. infixl 2 &?- (&?-) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)-      => ZippedStack inps -> (inps :-> '[out]) -> Either MichelsonFailureWithStack out-(&?-) = flip (-$?)+      => ZippedStack inps -> (IsNotInView => inps :-> '[out]) -> Either MichelsonFailureWithStack out+(&?-) x y = (-$?) y x  -- | Version of (-$) with arguments flipped. infixl 2 &- (&-) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)-     => ZippedStack inps -> (inps :-> '[out]) -> out-(&-) = flip (-$)+     => ZippedStack inps -> (IsNotInView => inps :-> '[out]) -> out+(&-) x y = (-$) y x  ---------------------------------------------------------------------------- -- Experimental versions

@@ -119,6 +119,7 @@ import Lorentz.Ext import Lorentz.Instr qualified as L import Lorentz.Iso+import Lorentz.Lambda import Lorentz.Macro qualified as L import Lorentz.Value import Morley.Michelson.Text (labelToMText)@@ -678,7 +679,7 @@  -- | Change submap operations so that they work on a modified key. mapStoreSubmapOpsKey-  :: Lambda key2 key1+  :: Fn key2 key1   -> StoreSubmapOps store name key1 value   -> StoreSubmapOps store name key2 value mapStoreSubmapOpsKey mapper StoreSubmapOps{..} = StoreSubmapOps

@@ -5,14 +5,18 @@ module Lorentz.Util.TH   ( entrypointDoc   , errorDoc+  , errorDocArg   , typeDoc   ) where -import Data.Text (stripPrefix, stripSuffix)-import Language.Haskell.TH (Dec, ExpQ, Q, TypeQ, appT, conT, litE, litT, mkName, strTyLit, stringL)+import Prelude hiding (lift)++import Data.Text (strip, stripPrefix, stripSuffix)+import Language.Haskell.TH (Dec, Q, TypeQ, appT, conT, litE, litT, mkName, strTyLit, stringL) import Language.Haskell.TH.Quote (QuasiQuoter(..)) import Language.Haskell.TH.Syntax (lift)-import Prelude hiding (lift)+import Text.ParserCombinators.ReadP (choice, readP_to_S, skipSpaces, string)+import Text.Read.Lex (Lexeme(..), lex)  import Lorentz.Doc import Lorentz.Entrypoints@@ -84,51 +88,89 @@ -- [errorDoc| "errorName" exception "Error description" |] -- @ ----- See this [tutorial](https://indigo-lang.gitlab.io/contract-docs/) which--- includes this quasiquote.+-- This is equivalent to 'errorDocArg' with @()@ specified as error argument type. -- errorDoc :: QuasiQuoter errorDoc = QuasiQuoter   { quoteExp  = const $ failQQType qqName "expression"   , quotePat  = const $ failQQType qqName "pattern"   , quoteType = const $ failQQType qqName "type"-  , quoteDec  = go+  , quoteDec  = quoteDec errorDocArg . (<> " ()")   }   where     qqName = "errorDoc" +{-# DEPRECATED errorDoc "errorDoc is deprecated, use errorDocArg with () argument instead" #-}++-- | QuasiQuote that helps generating @CustomErrorHasDoc@ instance.+--+-- Usage:+--+-- @+-- [errorDocArg| \<error-name> \<error-type> \<error-description> [\<error-arg-type>] |]+-- [errorDocArg| "errorName" exception "Error description" |]+-- [errorDocArg| "errorName" contract-internal "Error description" () |]+-- [errorDocArg| "errorName" bad-argument "Error description" Integer |]+-- @+--+-- The default argument type is 'NoErrorArg'. Only a type name can be used,+-- if you need complex type, define a type synonym.+--+-- See this [tutorial](https://indigo-lang.gitlab.io/contract-docs/) which+-- includes this quasiquote.+--+errorDocArg :: QuasiQuoter+errorDocArg = QuasiQuoter+  { quoteExp  = const $ failQQType qqName "expression"+  , quotePat  = const $ failQQType qqName "pattern"+  , quoteType = const $ failQQType qqName "type"+  , quoteDec  = go+  }+  where+    qqName = "errorDocArg"+     errMsg i = unlines       [ "Invalid arguments."       , "      Expected arguments to be in the format of:"-      , "        - [" <> qqName <> "| <error-name> <error-type> <error-description> |]"+      , "        - [" <> qqName <> "| <error-name> <error-type> <error-description> [<error-argument>] |]"       , "      Examples:"       , "        - [" <> qqName <> "| \"errorName\" exception \"Error description\" |]"-      , "        - [" <> qqName <> "| \"myError\" bad-argument \"An error happened\" |]"-      , "      But instead got: " <> unwords i+      , "        - [" <> qqName <> "| \"myError\" bad-argument \"An error happened\" () |]"+      , "      But instead got: " <> fromString i       ]      go :: String -> Q [Dec]     go input =       let-        extract :: [Text] -> Either Text (Text, ExpQ, Text)-        extract i = case i of-            errorName:errorClassString:errorDesc ->-              case readMaybe @ErrorClass (toString errorClassString) of-                Just errorClass -> Right-                  ( stripQuote $ errorName-                  , lift errorClass-                  , stripQuote . unwords $ errorDesc-                  )-                Nothing -> Left . errMsg $ i-            _ -> Left . errMsg $ i-      in case  extract $ words $ toText input of-            Right (errorName, errorClassVal, errorDesc) ->+        parser = do+          skipSpaces+          String errorName <- lex+          skipSpaces+          errorClass <- choice+            [ string "exception"         $> ErrClassActionException+            , string "bad-argument"      $> ErrClassBadArgument+            , string "contract-internal" $> ErrClassContractInternal+            , string "unknown"           $> ErrClassUnknown+            ]+          skipSpaces+          String errorDesc <- lex+          skipSpaces+          pure (errorName, errorClass, errorDesc)+        extract :: String -> Either Text ((String, ErrorClass, String), String)+        extract i = readP_to_S parser i & \case+          [(res, type_)] -> Right (res, toString . strip $ fromString type_)+          _ -> Left $ errMsg i+      in case  extract input of+            Right ((errorName, errorClassVal, errorDesc), errorArg) -> do+              let errorArgType = case errorArg of+                    [] -> [t|NoErrorArg|]+                    _ -> conT $ mkName errorArg               [d|-                type instance ErrorArg $(litT . strTyLit $ toString $ errorName) = ()+                type instance ErrorArg $(litT . strTyLit $ toString $ errorName) = $errorArgType                 instance CustomErrorHasDoc $(litT . strTyLit $ toString $ errorName) where-                  customErrClass = $(errorClassVal)+                  customErrClass = $(lift errorClassVal)                   customErrDocMdCause = $(litE $ stringL $ toString $ errorDesc)-              |]+                |]             Left err -> failQQ qqName err  -- | QuasiQuote that helps generating @TypeHasDoc@ instance.

@@ -51,12 +51,6 @@   , M.EntrypointCall   , M.SomeEntrypointCall -    -- * Custom datatypes-  , Fixed (..)-  , NFixed (..)-  , DecBase (..)-  , BinBase (..)-     -- * Constructors   , tz   , toMutez@@ -71,8 +65,6 @@   , M.coerceContractRef   , callingAddress   , callingDefAddress-  , callingTAddress-  , callingDefTAddress   , ToAddress (..)   , ToTAddress (..)   , ToContractRef (..)@@ -91,16 +83,12 @@  import Data.Constraint ((\\)) import Data.Default (Default(..))-import Data.Fixed (Fixed(..), HasResolution(..))-import GHC.Num (fromInteger)-import Prelude hiding (fromInteger)-import Text.Show qualified+import Prelude hiding (Rational)  import Fmt (Buildable(..))  import Lorentz.Address import Lorentz.Constraints.Scopes-import Lorentz.Wrappable import Morley.AsRPC (HasRPCRepr(..)) import Morley.Michelson.Text import Morley.Michelson.Typed qualified as M@@ -154,61 +142,9 @@ instance NiceUntypedValue a => Buildable (PrintAsValue a) where   build (PrintAsValue a) = build (M.toVal a) \\ niceUntypedValueEvi @a --- | Datatypes, representing base of the fixed-point values-data DecBase p where-  DecBase :: KnownNat p => DecBase p-data BinBase p where-  BinBase :: KnownNat p => BinBase p--instance KnownNat p => HasResolution (DecBase p) where-  resolution _ = 10 ^ (natVal (Proxy @p))--instance KnownNat p => HasResolution (BinBase p) where-  resolution _ = 2 ^ (natVal (Proxy @p))---- | Like @Fixed@ but with a @Natural@ value inside constructor-newtype NFixed p = MkNFixed Natural deriving stock (Eq, Ord)--convertNFixedToFixed :: NFixed a -> Fixed a-convertNFixedToFixed (MkNFixed a) = MkFixed (fromIntegral a)--instance (HasResolution a) => Show (NFixed a) where-  showsPrec d = Text.Show.showsPrec d . convertNFixedToFixed---- Note: This instances are copies of those in Data.Fixed for Fixed datatype-instance (HasResolution a) => Num (NFixed a) where-  (MkNFixed a) + (MkNFixed b) = MkNFixed (a + b)-  (MkNFixed a) - (MkNFixed b) = MkNFixed (a - b)-  fa@(MkNFixed a) * (MkNFixed b) = MkNFixed (div (a * b) (fromInteger (resolution fa)))-  negate (MkNFixed a) = MkNFixed (negate a)-  abs = id-  signum (MkNFixed a) = MkNFixed (signum a)-  fromInteger i = withResolution (\res -> MkNFixed ((fromInteger i) * res))--instance (HasResolution a) => Fractional (NFixed a) where-  fa@(MkNFixed a) / (MkNFixed b) = MkNFixed (div (a * (fromInteger (resolution fa))) b)-  recip fa@(MkNFixed a) = MkNFixed (div (res * res) a) where-      res = fromInteger $ resolution fa-  fromRational r = withResolution (\res -> MkNFixed (floor (r * (toRational res))))--instance M.IsoValue (NFixed p) where-  type ToT (NFixed p) = 'M.TNat-  toVal (MkNFixed x) = M.VNat x-  fromVal (M.VNat x) = MkNFixed x--instance Unwrappable (NFixed a) where-  type Unwrappabled (NFixed a) = Natural---- Helpers copied from Data.Fixed, because they are not exported from there-withResolution :: forall a f. (HasResolution a) => (Natural -> f a) -> f a-withResolution foo = foo . fromInteger . resolution $ Proxy @a- data OpenChest = ChestContent ByteString | ChestOpenFailed Bool   deriving stock (Generic, Show, Eq)   deriving anyclass (M.IsoValue, HasAnnotation)--instance HasRPCRepr OpenChest where-  type AsRPC OpenChest = OpenChest  instance M.TypeHasDoc OpenChest where   typeDocMdDescription = "Result of opening a chest"

@@ -106,18 +106,18 @@ -- | Flatten both ends of instruction stack. zippingStack   :: ZipInstrs [inp, out]-  => inp :-> out -> Lambda (ZippedStack inp) (ZippedStack out)+  => inp :-> out -> Fn (ZippedStack inp) (ZippedStack out) zippingStack code = unzipInstr ## code ## zipInstr  -- | Unflatten both ends of instruction stack. unzippingStack   :: ZipInstrs [inp, out]-  => Lambda (ZippedStack inp) (ZippedStack out) -> inp :-> out+  => Fn (ZippedStack inp) (ZippedStack out) -> inp :-> out unzippingStack code = zipInstr ## code ## unzipInstr  instance (WellTypedToT (ZippedStack inp), WellTypedToT (ZippedStack out), ZipInstr inp, ZipInstr out) => IsoValue (inp :-> out) where   type ToT (inp :-> out) = 'TLambda (ToT (ZippedStack inp)) (ToT (ZippedStack out))-  toVal i = VLam . unLorentzInstr $ zippingStack i+  toVal i = mkVLam $ unLorentzInstr $ zippingStack i   fromVal (VLam i) = zipInstr ## LorentzInstr i ## unzipInstr  instance