diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,35 @@ +0.15.1 +====== +* [!1325](https://gitlab.com/morley-framework/morley/-/merge_requests/1325) + Add `AND`, `NOT`, `OR`, `XOR`, `LSL` and `LSR` operations support on `bytes` +* [!1326](https://gitlab.com/morley-framework/morley/-/merge_requests/1326) + Add support for bytes to nat and int conversions + + Support `nat` and `bytes` instructions, and the new operands to `int` + instruction. +* [!1331](https://gitlab.com/morley-framework/morley/-/merge_requests/1331) + Support implicit account tickets + + Allow tickets as parameter to `ImplicitAddress` in `ToTAddress`; +* [!1328](https://gitlab.com/morley-framework/morley/-/merge_requests/1328) + Kill support for TORUs, minimal sr1 address support, tz4 address support + + Module `Lorentz.Txr1Call` removed. +* [!1314](https://gitlab.com/morley-framework/morley/-/merge_requests/1314) + Preserve docs after failWith +* [!1289](https://gitlab.com/morley-framework/morley/-/merge_requests/1289) + Simplify/fix ReferencedByName + + `dupL` and `dupLNamed` could under some specific circumstances crash at + runtime due to not-always-valid unsafe coercions. The unsafe coercions have + been removed. +* [!1235](https://gitlab.com/morley-framework/morley/-/merge_requests/1235) + Make it easier to have consistent field naming between HasAnnotation and + TypeHasDoc + + Require newly introduced `TypeHasFieldNamingStrategy` constraint in the + default implementation `annOptions`. Apply the strategy as appropriate. + + Add an optional field to `typeDoc` which allows specifying the strategy. + + See also the corresponding `morley` changelog. + 0.15.0 ====== * [!1273](https://gitlab.com/morley-framework/morley/-/merge_requests/1273) diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,5 +1,5 @@ MIT License -Copyright (c) 2021-2022 Oxhead Alpha +Copyright (c) 2021-2023 Oxhead Alpha Copyright (c) 2019-2021 Tocqueville Group Permission is hereby granted, free of charge, to any person obtaining a copy diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,3 +1,7 @@ +> :warning: **Note: this project is being deprecated.** +> +> It will no longer be maintained after the activation of protocol "N" on the Tezos mainnet. + # Morley Lorentz EDSL [![Hackage](https://img.shields.io/hackage/v/lorentz.svg)](https://hackage.haskell.org/package/lorentz) diff --git a/lorentz.cabal b/lorentz.cabal --- a/lorentz.cabal +++ b/lorentz.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: lorentz -version: 0.15.0 +version: 0.15.1 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 @@ -13,7 +13,7 @@ bug-reports: https://gitlab.com/morley-framework/morley/-/issues author: camlCase, Serokell, Tocqueville Group maintainer: Serokell -copyright: 2019-2021 Tocqueville Group, 2021-2022 Oxhead Alpha +copyright: 2019-2021 Tocqueville Group, 2021-2023 Oxhead Alpha license: MIT license-file: LICENSE build-type: Simple @@ -79,7 +79,6 @@ Lorentz.StoreClass Lorentz.StoreClass.Extra Lorentz.Tickets - Lorentz.Txr1Call Lorentz.UParam Lorentz.Util.TH Lorentz.Value @@ -165,7 +164,6 @@ , singletons-base , template-haskell , text - , text-manipulate , type-errors , unordered-containers , vinyl diff --git a/src/Lorentz.hs b/src/Lorentz.hs --- a/src/Lorentz.hs +++ b/src/Lorentz.hs @@ -5,8 +5,8 @@ ( module Exports ) where -import Lorentz.ADT as Exports import Lorentz.Address as Exports +import Lorentz.ADT as Exports import Lorentz.Annotation as Exports import Lorentz.Arith as Exports import Lorentz.Base as Exports @@ -36,7 +36,6 @@ import Lorentz.Run as Exports import Lorentz.Run.Simple as Exports import Lorentz.StoreClass as Exports -import Lorentz.Txr1Call as Exports import Lorentz.UParam as Exports import Lorentz.Util.TH as Exports import Lorentz.Value as Exports diff --git a/src/Lorentz/Address.hs b/src/Lorentz/Address.hs --- a/src/Lorentz/Address.hs +++ b/src/Lorentz/Address.hs @@ -1,6 +1,8 @@ -- SPDX-FileCopyrightText: 2021 Oxhead Alpha -- SPDX-License-Identifier: LicenseRef-MIT-OA +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + {- | This module introduces several types for safe work with @address@ and @@ -43,6 +45,7 @@ , ToContractRef (..) , FromContractRef (..) , convertContractRef + , ImplicitContractParameter -- * Re-exports , Address @@ -185,7 +188,27 @@ instance ToTAddress cp vd ContractAddress where toTAddress = TAddress . MkAddress -instance (cp ~ (), vd ~ ()) => ToTAddress cp vd ImplicitAddress where +type CheckImplicitContractParameter :: Type -> M.T -> Constraint +type family CheckImplicitContractParameter cp totcp where + CheckImplicitContractParameter _ 'M.TUnit = () + CheckImplicitContractParameter _ ('M.TTicket _) = () + CheckImplicitContractParameter cp totcp = TypeError + ( 'Text "Implicit address parameter may be either 'unit' or 'ticket', but it was" + ':$$: 'ShowType cp ':<>: 'Text " (" ':<>: 'ShowType totcp ':<>: 'Text ")" + ) + +-- | We use this type class to forcibly default ambiguous parameter type to +-- @()@, but still allow for other types. It also doubles as a proxy for a +-- custom 'TypeError'. +class ToT cp ~ totcp => ImplicitContractParameter cp totcp +instance ToT cp ~ 'M.TTicket t => ImplicitContractParameter cp ('M.TTicket t) +instance {-# incoherent #-} (CheckImplicitContractParameter cp totcp, cp ~ (), totcp ~ 'M.TUnit) + => ImplicitContractParameter cp totcp + +instance (ImplicitContractParameter cp (ToT cp), vd ~ ()) => ToTAddress cp vd ImplicitAddress where + toTAddress = TAddress . MkAddress + +instance (vd ~ ()) => ToTAddress cp vd SmartRollupAddress where toTAddress = TAddress . MkAddress instance ToTAddress cp vd L1Address where diff --git a/src/Lorentz/Annotation.hs b/src/Lorentz/Annotation.hs --- a/src/Lorentz/Annotation.hs +++ b/src/Lorentz/Annotation.hs @@ -7,11 +7,13 @@ module Lorentz.Annotation ( AnnOptions (..) , defaultAnnOptions + , dropPrefix , dropPrefixThen , appendTo , toCamel , toPascal , toSnake + , stripFieldPrefix , ctorNameToAnnWithOptions , FollowEntrypointFlag (..) @@ -23,15 +25,14 @@ , insertTypeAnn ) where -import Data.Char (isUpper) -import Data.Text qualified as T -import Data.Text.Manipulate (toCamel, toPascal, toSnake) +import Data.Default (Default(..)) import GHC.Generics qualified as G import Morley.Michelson.Text import Morley.Michelson.Typed (BigMap, BigMapId, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, Ticket, ToT, insertTypeAnn, starNotes) +import Morley.Michelson.Typed.Haskell.Doc (TypeHasFieldNamingStrategy(..)) import Morley.Michelson.Typed.Haskell.Value (GValueType) import Morley.Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, mkAnnotation, noAnn) import Morley.Tezos.Address @@ -51,16 +52,23 @@ { fieldAnnModifier :: Text -> Text } +instance Default AnnOptions where + def = AnnOptions id + defaultAnnOptions :: AnnOptions -defaultAnnOptions = AnnOptions id +defaultAnnOptions = def +{-# DEPRECATED defaultAnnOptions "Use 'Data.Default.def' instead." #-} -- | Drops the field name prefix from a field. -- We assume a convention of the prefix always being lower case, -- and the first letter of the actual field name being uppercase. -- It also accepts another function which will be applied directly -- after dropping the prefix. +-- +-- Left for compatibility. dropPrefixThen :: (Text -> Text) -> Text -> Text -dropPrefixThen f = f . T.dropWhile (Prelude.not . isUpper) +dropPrefixThen = (. dropPrefix) +{-# DEPRECATED dropPrefixThen " Use 'dropPrefix' and function composition instead." #-} -- | @appendTo suffix fields field@ appends the given suffix to @field@ -- if the field exists in the @fields@ list. @@ -90,7 +98,8 @@ gGetAnnotationNoField :: forall a. (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a) => FollowEntrypointFlag -> Notes (ToT a) -gGetAnnotationNoField = \_ -> gGetAnnotation @(G.Rep a) defaultAnnOptions NotFollowEntrypoint NotGenerateFieldAnn ^. _1 +gGetAnnotationNoField = + \_ -> gGetAnnotation @(G.Rep a) def NotFollowEntrypoint NotGenerateFieldAnn ^. _1 -- | This class defines the type and field annotations for a given type. Right now -- the type annotations come from names in a named field, and field annotations are @@ -98,15 +107,22 @@ class HasAnnotation a where getAnnotation :: FollowEntrypointFlag -> Notes (ToT a) default getAnnotation - :: (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a) + :: ( GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a + , GIsSumType (G.Rep a), TypeHasFieldNamingStrategy a + ) => FollowEntrypointFlag -> Notes (ToT a) - getAnnotation b = gGetAnnotation @(G.Rep a) (annOptions @a) b GenerateFieldAnn ^. _1 + getAnnotation b = + gGetAnnotation @(G.Rep a) (fromMaybe (gAnnOptions @a) $ annOptions @a) b GenerateFieldAnn ^. _1 - annOptions :: AnnOptions - default annOptions :: AnnOptions - annOptions = defaultAnnOptions + annOptions :: Maybe AnnOptions + annOptions = Nothing +gAnnOptions :: forall a. (GIsSumType (G.Rep a), TypeHasFieldNamingStrategy a) => AnnOptions +gAnnOptions + | gIsSumType @(G.Rep a) = def + | otherwise = def { fieldAnnModifier = typeFieldNamingStrategy @a } + instance (HasAnnotation a, KnownSymbol name) => HasAnnotation (NamedF Identity a name) where getAnnotation b = insertTypeAnn (symbolAnn @name) $ @@ -146,9 +162,6 @@ instance HasAnnotation Address where getAnnotation _ = starNotes -instance HasAnnotation TxRollupL2Address where - getAnnotation _ = starNotes - instance HasAnnotation EpAddress where getAnnotation _ = starNotes @@ -179,7 +192,7 @@ instance (HasAnnotation k, HasAnnotation v) => HasAnnotation (BigMap k v) where getAnnotation _ = NTBigMap noAnn (getAnnotation @k NotFollowEntrypoint) (getAnnotation @v NotFollowEntrypoint) -instance (HasAnnotation k, HasAnnotation v) => HasAnnotation (BigMapId k v) where +instance HasAnnotation (BigMapId k v) where getAnnotation _ = starNotes instance (KnownIsoT v) => HasAnnotation (Set v) where @@ -288,3 +301,16 @@ instance (HasAnnotation x) => GHasAnnotation (G.Rec0 x) where gGetAnnotation _ b _ = (getAnnotation @x b, noAnn, noAnn) + +-- | Check if a 'Generic' type is a sum type. +class GIsSumType a where + gIsSumType :: Bool + +instance GIsSumType G.U1 where gIsSumType = False +instance GIsSumType G.V1 where gIsSumType = False +instance GIsSumType (x G.:+: y) where gIsSumType = True +instance GIsSumType (x G.:*: y) where gIsSumType = False +instance GIsSumType (G.S1 _a x) where gIsSumType = False +instance GIsSumType (G.C1 _a x) where gIsSumType = False +instance GIsSumType (G.Rec0 x) where gIsSumType = False +instance GIsSumType x => GIsSumType (G.D1 _a x) where gIsSumType = gIsSumType @x diff --git a/src/Lorentz/Arith.hs b/src/Lorentz/Arith.hs --- a/src/Lorentz/Arith.hs +++ b/src/Lorentz/Arith.hs @@ -8,12 +8,15 @@ , UnaryArithOpHs (..) , DefUnaryArithOp (..) , ToIntegerArithOpHs (..) + , ToBytesArithOpHs (..) ) where import Prelude hiding (natVal) import Lorentz.Base +import Lorentz.Bytes (BytesLike) import Lorentz.Value +import Morley.Michelson.Typed (SingI, T) import Morley.Michelson.Typed.Arith import Morley.Michelson.Typed.Instr qualified as M @@ -44,15 +47,19 @@ :: ( DefUnaryArithOp aop , UnaryArithOp aop (ToT n) , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n) + , DefUnaryArithOpExtraConstraints aop (ToT n) ) => n : s :-> UnaryArithResHs aop n : s evalUnaryArithOpHs = I (defUnaryArithOpHs @aop) -- | Helper typeclass that provides default definition of 'evalUnaryArithOpHs'. class DefUnaryArithOp aop where + type DefUnaryArithOpExtraConstraints aop (n :: T) :: Constraint + type DefUnaryArithOpExtraConstraints _ _ = () defUnaryArithOpHs :: ( UnaryArithOp aop n , r ~ UnaryArithRes aop n + , DefUnaryArithOpExtraConstraints aop n ) => M.Instr (n : s) (r : s) @@ -63,6 +70,13 @@ => n : s :-> Integer : s evalToIntOpHs = I M.INT +class ToBytesArithOpHs (n :: Type) where + evalToBytesOpHs :: BytesLike bs => n : s :-> bs : s + default evalToBytesOpHs + :: (ToBytesArithOp (ToT n), BytesLike bs) + => n : s :-> bs : s + evalToBytesOpHs = I M.BYTES + instance DefArithOp Add where defEvalOpHs = M.ADD instance DefArithOp Sub where @@ -82,6 +96,7 @@ instance DefArithOp EDiv where defEvalOpHs = M.EDIV instance DefUnaryArithOp Not where + type DefUnaryArithOpExtraConstraints Not n = SingI n defUnaryArithOpHs = M.NOT instance DefUnaryArithOp Abs where defUnaryArithOpHs = M.ABS @@ -158,17 +173,22 @@ instance (r ~ Natural) => ArithOpHs Or Natural Natural r instance (r ~ Bool) => ArithOpHs Or Bool Bool r +instance (r ~ ByteString) => ArithOpHs Or ByteString ByteString r instance (r ~ Natural) => ArithOpHs And Integer Natural r instance (r ~ Natural) => ArithOpHs And Natural Natural r instance (r ~ Bool) => ArithOpHs And Bool Bool r +instance (r ~ ByteString) => ArithOpHs And ByteString ByteString r instance (r ~ Natural) => ArithOpHs Xor Natural Natural r instance (r ~ Bool) => ArithOpHs Xor Bool Bool r +instance (r ~ ByteString) => ArithOpHs Xor ByteString ByteString r instance (r ~ Natural) => ArithOpHs Lsl Natural Natural r where +instance (r ~ ByteString) => ArithOpHs Lsl ByteString Natural r where instance (r ~ Natural) => ArithOpHs Lsr Natural Natural r +instance (r ~ ByteString) => ArithOpHs Lsr ByteString Natural r instance UnaryArithOpHs Abs Integer where type UnaryArithResHs Abs Integer = Natural @@ -179,6 +199,8 @@ type UnaryArithResHs Not Natural = Integer instance UnaryArithOpHs Not Bool where type UnaryArithResHs Not Bool = Bool +instance UnaryArithOpHs Not ByteString where + type UnaryArithResHs Not ByteString = ByteString instance UnaryArithOpHs Eq' Integer where type UnaryArithResHs Eq' Integer = Bool @@ -218,3 +240,12 @@ instance ToIntegerArithOpHs Natural instance ToIntegerArithOpHs Bls12381Fr + +-- This is an unfortunate overpapping instance, but what can you do. +-- +-- In case this becomes an issue, see this discussion: +-- https://gitlab.com/morley-framework/morley/-/merge_requests/1326#note_1324175008 +instance {-# overlappable #-} BytesLike bs => ToIntegerArithOpHs bs + +instance ToBytesArithOpHs Natural +instance ToBytesArithOpHs Integer diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs --- a/src/Lorentz/Base.hs +++ b/src/Lorentz/Base.hs @@ -43,7 +43,7 @@ import Lorentz.Annotation (HasAnnotation(..)) import Lorentz.Constraints import Morley.Micheline (ToExpression(..)) -import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf) +import Morley.Michelson.Optimizer (OptimizerConf, optimize, optimizeWithConf) import Morley.Michelson.Parser (MichelsonSource, ParserException, parseExpandValue) import Morley.Michelson.Preprocess (transformBytes, transformStrings) import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended) @@ -54,6 +54,7 @@ rfAnyInstr, rfMapAnyInstr, rfMerge) import Morley.Michelson.Typed qualified as M (Contract) import Morley.Michelson.Typed.Contract (giveNotInView) +import Morley.Michelson.Typed.Doc (cutInstrNonDoc) import Morley.Michelson.Untyped qualified as U -- | Alias for instruction which hides inner types representation via @T@. @@ -230,7 +231,7 @@ (#) :: (a :-> b) -> (b :-> c) -> a :-> c I l # I r = I (l `Seq` r) I l # FI r = FI (l `Seq` r) -FI l # _ = FI l +FI l # r = FI (l `Seq` cutInstrNonDoc optimize (iAnyCode r)) infixl 8 # -- | An instruction sequence taking one stack element as input and returning one diff --git a/src/Lorentz/Constraints/Scopes.hs b/src/Lorentz/Constraints/Scopes.hs --- a/src/Lorentz/Constraints/Scopes.hs +++ b/src/Lorentz/Constraints/Scopes.hs @@ -22,15 +22,6 @@ , NiceViewable , NiceNoBigMap - , niceParameterEvi - , niceStorageEvi - , niceConstantEvi - , dupableEvi - , nicePackedValueEvi - , niceUnpackedValueEvi - , niceUntypedValueEvi - , niceViewableEvi - -- * Individual constraints (internals) , CanHaveBigMap , KnownValue @@ -94,32 +85,3 @@ type NiceComparable n = (ProperNonComparableValBetterErrors (ToT n), KnownValue n, Comparable (ToT n)) type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n)) - -{-# DEPRECATED niceParameterEvi, niceStorageEvi, niceConstantEvi, dupableEvi - , nicePackedValueEvi, niceUnpackedValueEvi, niceUntypedValueEvi - , niceViewableEvi - "This is no longer needed; the constraint implication is now trivial." - #-} -niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a) -niceParameterEvi = Sub Dict - -niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a) -niceStorageEvi = Sub Dict - -niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a) -niceConstantEvi = Sub Dict - -dupableEvi :: forall a. Dupable a :- DupableScope (ToT a) -dupableEvi = Sub Dict - -nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a) -nicePackedValueEvi = Sub Dict - -niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a) -niceUnpackedValueEvi = Sub Dict - -niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a) -niceUntypedValueEvi = Sub Dict - -niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a) -niceViewableEvi = Sub Dict diff --git a/src/Lorentz/Doc.hs b/src/Lorentz/Doc.hs --- a/src/Lorentz/Doc.hs +++ b/src/Lorentz/Doc.hs @@ -60,6 +60,7 @@ , attachDocCommons , TypeHasDoc (..) + , TypeHasFieldNamingStrategy (..) , SomeTypeWithDoc (..) , typeDocBuiltMichelsonRep diff --git a/src/Lorentz/Entrypoints/Impl.hs b/src/Lorentz/Entrypoints/Impl.hs --- a/src/Lorentz/Entrypoints/Impl.hs +++ b/src/Lorentz/Entrypoints/Impl.hs @@ -282,7 +282,7 @@ type GLookupEntrypoint mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) = JustOnEq ctor (GExtractField x) gMkEntrypointsNotes = - (gGetAnnotation @x defaultAnnOptions FollowEntrypoint NotGenerateFieldAnn ^. _1, ctorNameToAnn @ctor) + (gGetAnnotation @x def FollowEntrypoint NotGenerateFieldAnn ^. _1, ctorNameToAnn @ctor) gMkEpLiftSequence (Label :: Label name) = case sing @ctor %== sing @name of STrue -> EpConstructed EplArgHere diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs --- a/src/Lorentz/Instr.hs +++ b/src/Lorentz/Instr.hs @@ -91,6 +91,8 @@ , le0 , ge0 , int + , nat + , bytes , toTAddress_ , view' , self @@ -158,13 +160,12 @@ import Lorentz.ViewBase import Lorentz.Zip import Morley.Michelson.Typed - (ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG, ConstraintDUG', - ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN, EntrypointCallT(..), GetN, - Instr(..), Notes, RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, pattern CAR, pattern CDR, - pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes) + (EntrypointCallT(..), Instr(..), Notes, RemFail(..), SingI, SomeEntrypointCallT(..), pattern CAR, + pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes) import Morley.Michelson.Typed.Arith import Morley.Michelson.Typed.Contract (giveNotInView) import Morley.Michelson.Typed.Haskell.Value +import Morley.Michelson.Typed.Instr.Constraints import Morley.Michelson.Untyped (FieldAnn) import Morley.Util.Named import Morley.Util.Peano @@ -644,6 +645,12 @@ int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s int = evalToIntOpHs + +nat :: BytesLike bs => bs : s :-> Natural : s +nat = I NAT + +bytes :: (BytesLike bs, ToBytesArithOpHs i) => i : s :-> bs : s +bytes = evalToBytesOpHs -- | Manual variation of @VIEW@ instruction. -- It is pretty much like Michelson's @VIEW@, you must make sure that the compiler can diff --git a/src/Lorentz/Instr/Framed.hs b/src/Lorentz/Instr/Framed.hs --- a/src/Lorentz/Instr/Framed.hs +++ b/src/Lorentz/Instr/Framed.hs @@ -22,12 +22,16 @@ -- -- This instruction requires you to specify the piece of stack to truncate -- as type argument. +-- +-- The complexity of this operation is linear in the number of instructions. If +-- possible, avoid nested uses as that would imply multiple traversals. Worst +-- case, complexity can become quadratic. framed :: forall s i o. (KnownList i, KnownList o) => (i :-> o) -> ((i ++ s) :-> (o ++ s)) framed (iNonFailingCode -> i) = - I $ FrameInstr (Proxy @(ToTs s)) i + I $ frameInstr @(ToTs s) i \\ totsKnownLemma @i \\ totsAppendLemma @i @s \\ totsAppendLemma @o @s diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs --- a/src/Lorentz/Macro.hs +++ b/src/Lorentz/Macro.hs @@ -158,9 +158,10 @@ import Lorentz.Value import Lorentz.ViewBase import Morley.AsRPC (HasRPCRepr(..)) -import Morley.Michelson.Typed (ConstraintDIPN', ConstraintDUG', T, viewNameToMText) +import Morley.Michelson.Typed (T, viewNameToMText) import Morley.Michelson.Typed.Arith import Morley.Michelson.Typed.Haskell.Value +import Morley.Michelson.Typed.Instr.Constraints (ConstraintDIPN', ConstraintDUG') import Morley.Michelson.Typed.Scope import Morley.Util.Markdown import Morley.Util.Peano diff --git a/src/Lorentz/ReferencedByName.hs b/src/Lorentz/ReferencedByName.hs --- a/src/Lorentz/ReferencedByName.hs +++ b/src/Lorentz/ReferencedByName.hs @@ -3,10 +3,67 @@ {-# LANGUAGE FunctionalDependencies #-} --- | Referenced-by-name versions of some instructions. +{- | Referenced-by-name versions of some instructions. + +They allow to "dig" into stack or copy elements of stack referring them +by label. + +When operating on a polymorphic stack, you'll need 'HasNamedVar' constraint: + +>>> :{ +_foo :: s :-> ("bar" :! Natural) : s +_foo = dupLNamed #bar -- --- They allow to "dig" into stack or copy elements of stack referring them --- by label. +_bar :: s :-> MText : s +_bar = dupL #baz +:} +... +... No instance for (HasNamedVar s "bar" Natural) +... +... No instance for (HasNamedVar s "baz" MText) +... + +>>> :{ +_foo :: HasNamedVar s "bar" Natural => s :-> ("bar" :! Natural) : s +_foo = dupLNamed #bar +-- +_bar :: HasNamedVar s "bar" Natural => s :-> Natural : s +_bar = dupL #bar +:} + +When the stack contains type variables, you may need 'VarIsUnnamed' constraint: + +>>> :{ +_bar + :: HasNamedVar s "foo" MText + => qux : s :-> ("foo" :! MText) : qux : s +_bar = dupLNamed #foo +-- +_baz + :: HasNamedVar s "bar" MText + => corge : s :-> MText : corge : s +_baz = dupL #bar +:} +... +... Not clear which name `qux` variable has +... Consider adding `VarIsUnnamed qux` constraint +... or carrying a named variable instead +... +... Not clear which name `corge` variable has +... + +>>> :{ +_bar + :: (HasNamedVar s "foo" MText, VarIsUnnamed qux) + => qux : s :-> ("foo" :! MText) : qux : s +_bar = dupLNamed #foo +-- +_baz + :: (HasNamedVar s "bar" MText, VarIsUnnamed corge) + => corge : s :-> MText : corge : s +_baz = dupL #bar +:} +-} module Lorentz.ReferencedByName ( -- * Constraints HasNamedVar @@ -21,7 +78,7 @@ , VarIsUnnamed ) where -import Data.Constraint (Bottom(..), (\\)) +import Data.Constraint (Bottom(..)) import Data.Singletons (Sing) import Fcf qualified import Type.Errors (DelayError, IfStuck) @@ -32,13 +89,16 @@ import Lorentz.Constraints import Lorentz.Instr import Morley.Michelson.Text -import Morley.Michelson.Typed import Morley.Util.Label import Morley.Util.Named import Morley.Util.Peano import Morley.Util.Type import Morley.Util.TypeLits +-- $setup +-- >>> import Prelude () +-- >>> :m +Lorentz Lorentz.Zip Morley.Util.Named Fmt + -- Errors ---------------------------------------------------------------------------- @@ -84,10 +144,10 @@ -- Dup ---------------------------------------------------------------------------- --- | Indicates that stack @s@ contains a @name :! var@ or @name :? var@ value. +-- | Indicates that stack @s@ contains a @name :! var@ value. {- Implementation notes: -We intentially keep this typeclass as simple as possible so that if a user has +We intentionally keep this typeclass as simple as possible so that if a user has @ myFunc :: Integer : s :-> Integer : s @@ -100,30 +160,28 @@ -} type HasNamedVar :: [Type] -> Symbol -> Type -> Constraint class HasNamedVar s name var | s name -> var where - -- | 1-based position of the variable on stack. + -- | 0-based position of the variable on stack. varPosition :: VarPosition s name var -type ConstraintVarPosition :: [Type] -> Peano -> Constraint -type ConstraintVarPosition s n = - ( SingI n, n > 'Z ~ 'True - , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n - ) - type VarPosition :: [Type] -> Symbol -> Type -> Type data VarPosition s name var where - VarPosition :: (ConstraintVarPosition s n) => Sing (n :: Peano) -> VarPosition s name var + VarPosition + :: (x ~ name :! var, ConstraintDUPNLorentz ('S n) s (x : s) x) + -- NB: 'ConstraintDUPNLorentz' is a slight overkill here, as it also asserts + -- @x : s ~ x : s@, which is a triviality. However, introducing a new + -- constraint synonym without that assertion doesn't seem justified at this + -- point, and replacing 'ConstraintDUPNLorentz' with its definition is + -- rather ugly in itself. If you're looking to implement dugNamed or + -- something like this, you may want to do the legwork of introducing a new + -- constraint synonym. -- @lierdakil + => Sing (n :: Peano) -> VarPosition s name var -instance ( Bottom - , StackElemNotFound name - , var ~ NamedVariableNotFound name - ) => - HasNamedVar '[] name var where +instance (Bottom, StackElemNotFound name, var ~ NamedVariableNotFound name) + => HasNamedVar '[] name var where varPosition = no -instance ( ElemHasNamedVar (ty : s) name var - (VarNamePretty ty == 'VarNamed name) - ) => - HasNamedVar (ty : s) name var where +instance ElemHasNamedVar (ty : s) name var (VarNamePretty ty == 'VarNamed name) + => HasNamedVar (ty : s) name var where varPosition = elemVarPosition @(ty : s) @name @var @(VarNamePretty ty == 'VarNamed name) -- Helper for handling each separate variable on stack @@ -131,14 +189,12 @@ class ElemHasNamedVar s name var nameMatch | s name nameMatch -> var where elemVarPosition :: VarPosition s name var -instance (ty ~ NamedF f var name) => - ElemHasNamedVar (ty : s) name var 'True where - elemVarPosition = VarPosition (SS SZ) +instance ty ~ (name :! var) => ElemHasNamedVar (ty : s) name var 'True where + elemVarPosition = VarPosition SZ -instance (HasNamedVar s name var) => - ElemHasNamedVar (ty : s) name var 'False where +instance HasNamedVar s name var => ElemHasNamedVar (ty : s) name var 'False where elemVarPosition = case varPosition @s @name @var of - VarPosition n -> VarPosition (SS n) + VarPosition n -> VarPosition $ SS n -- | Version of 'HasNamedVar' for multiple variables. -- @@ -148,36 +204,43 @@ HasNamedVars _ '[] = () HasNamedVars s ((n := ty) ': vs) = (HasNamedVar s n ty, HasNamedVars s vs) --- | Get the variable at @n@-th position on stack, assuming that caller is sure --- that stack is long enough. --- --- @martoon: I'm not ready to fight the compiler regarding numerous --- complex constraints, so just assuring it that those constraints will hold. --- --- @heitor.toledo: GHC doesn't seem to enjoy it that we use 'ConstraintDUPNLorentz', --- so I replaced it with the expanded definition. -unsafeDupL - :: forall n s var. - (ConstraintVarPosition s n, Dupable var) - => Sing (n :: Peano) -> s :-> var : s -unsafeDupL _ = - dupNPeano @n - \\ unsafeProvideConstraint @(LazyTake (Decrement n) s ++ (var : Drop n s) ~ s) - \\ unsafeProvideConstraint @(LazyTake (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s) +{- | Version of 'dupL' that leaves a named variable on stack. --- | Version of 'dupL' that leaves a named variable on stack. +>>> dupLNamed #foo # pair -$ (#foo :! (123 :: Integer)) +(fromLabel @"foo" :! 123,fromLabel @"foo" :! 123) + +>>> (dupLNamed #bar # ppaiir) -$ (#foo :! (123 :: Integer)) ::: (#bar :! (321 :: Integer)) +(fromLabel @"bar" :! 321,(fromLabel @"foo" :! 123,fromLabel @"bar" :! 321)) + +>>> (dupLNamed #baz # ppaiir) -$ (#foo :! (123 :: Integer)) ::: (#bar :! (321 :: Integer)) +... +... Element with name "baz" is not present on stack +... +-} dupLNamed :: forall var name s. (HasNamedVar s name var, Dupable var) => Label name -> s :-> (name :! var) : s dupLNamed Label{} = case varPosition @s @name @var of - VarPosition sn -> unsafeDupL sn + VarPosition (_ :: Sing n) -> dupNPeano @('S n) --- | Take the element with given label on stack and copy it on top. --- --- If there are multiple variables with given label, the one closest --- to the top of the stack is picked. +{- | Take the element with given label on stack and copy it on top. + +If there are multiple variables with given label, the one closest to the top of +the stack is picked. + +>>> dupL #foo # pair -$ (#foo :! (123 :: Integer)) +(123,fromLabel @"foo" :! 123) + +>>> (dupL #bar # ppaiir) -$ (#foo :! (123 :: Integer)) ::: (#bar :! (321 :: Integer)) +(321,(fromLabel @"foo" :! 123,fromLabel @"bar" :! 321)) + +>>> (dupL #baz # ppaiir) -$ (#foo :! (123 :: Integer)) ::: (#bar :! (321 :: Integer)) +... +... Element with name "baz" is not present on stack +... +-} dupL :: forall var name s. (HasNamedVar s name var, Dupable var) => Label name -> s :-> var : s diff --git a/src/Lorentz/Txr1Call.hs b/src/Lorentz/Txr1Call.hs deleted file mode 100644 --- a/src/Lorentz/Txr1Call.hs +++ /dev/null @@ -1,30 +0,0 @@ --- SPDX-FileCopyrightText: 2022 Oxhead Alpha --- SPDX-License-Identifier: LicenseRef-MIT-OA - -{-# OPTIONS_GHC -Wno-orphans #-} - --- | Definitions for calling @txr1@ addresses -module Lorentz.Txr1Call - ( Txr1CallParam - ) where - -import Lorentz.Annotation -import Lorentz.Constraints.Scopes -import Lorentz.Entrypoints -import Lorentz.Value -import Morley.Tezos.Address - --- | Call parameter for @txr1@ addresses. Default entrypoint doesn't exist, but --- here we simply represent it as having @never@ parameter, thus uncallable. -data Txr1CallParam a = Deposit (Ticket a, TxRollupL2Address) | Default Never - deriving stock Generic - deriving anyclass (HasAnnotation) - -instance NiceComparable a => IsoValue (Txr1CallParam a) - -instance (HasAnnotation a, NiceComparable a) => ParameterHasEntrypoints (Txr1CallParam a) where - type ParameterEntrypointsDerivation (Txr1CallParam a) = EpdPlain - --- NB: This is an orphan, because otherwise we have nasty circular dependencies between modules -instance (cp ~ Txr1CallParam a, vd ~ ()) => ToTAddress cp vd TxRollupAddress where - toTAddress = TAddress . MkAddress diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs --- a/src/Lorentz/UParam.hs +++ b/src/Lorentz/UParam.hs @@ -59,7 +59,7 @@ import Lorentz.Constraints import Lorentz.Entrypoints.Doc import Lorentz.Errors -import Lorentz.Instr as L +import Lorentz.Instr as L hiding (bytes) import Lorentz.Macro import Lorentz.Pack import Morley.AsRPC (HasRPCRepr(..)) diff --git a/src/Lorentz/Util/TH.hs b/src/Lorentz/Util/TH.hs --- a/src/Lorentz/Util/TH.hs +++ b/src/Lorentz/Util/TH.hs @@ -8,13 +8,12 @@ , typeDoc ) where -import Prelude hiding (lift) +import Prelude -import Data.Text (strip, stripPrefix, stripSuffix) -import Language.Haskell.TH (Dec, Q, TypeQ, appT, conT, litE, litT, mkName, strTyLit, stringL) +import Data.Char (isSpace) +import Language.Haskell.TH (Dec, Q, conE, conT, litE, litT, mkName, strTyLit, stringL, varE) import Language.Haskell.TH.Quote (QuasiQuoter(..)) -import Language.Haskell.TH.Syntax (lift) -import Text.ParserCombinators.ReadP (choice, readP_to_S, skipSpaces, string) +import Text.ParserCombinators.ReadP (ReadP, choice, eof, munch1, readP_to_S, skipSpaces, string) import Text.Read.Lex (Lexeme(..), lex) import Lorentz.Doc @@ -26,7 +25,7 @@ -- Usage: -- -- @ --- [entrypointDoc| Parameter \ \ |] +-- [entrypointDoc| Parameter \ [\] |] -- [entrypointDoc| Parameter plain |] -- [entrypointDoc| Parameter plain "root"|] -- @ @@ -35,48 +34,30 @@ -- includes this quasiquote. -- entrypointDoc :: QuasiQuoter -entrypointDoc = QuasiQuoter - { quoteExp = const $ failQQType qqName "expression" - , quotePat = const $ failQQType qqName "pattern" - , quoteType = const $ failQQType qqName "type" - , quoteDec = go - } - where - qqName = "entrypointDoc" - - go :: String -> Q [Dec] - go input = - let - mkEpdWithRoot :: Text -> Text -> TypeQ - mkEpdWithRoot epd r = - appT (appT (conT $ mkName "EpdWithRoot") (litT $ strTyLit $ toString $ stripQuote r)) - (conT $ mkName (toString epd)) - extract :: [Text] -> Either Text (Text, TypeQ) - extract a = - case a of - [x, "plain"] -> Right (x, conT $ mkName $ "EpdPlain") - [x, "delegate"] -> Right (x, conT $ mkName $ "EpdDelegate") - [x, "recursive"] -> Right (x, conT $ mkName $ "EpdRecursive") - [x, "none"] -> Right (x, conT $ mkName $ "EpdNone") - [x, "plain", r] -> Right (x, mkEpdWithRoot "EpdPlain" r) - [x, "delegate", r] -> Right (x, mkEpdWithRoot "EpdDelegate" r) - [x, "recursive", r] -> Right (x, mkEpdWithRoot "EpdRecursive" r) - i -> Left $ unlines - [ "Invalid arguments." - , " Expected arguments to be in the format of:" - , " - [" <> qqName <> "| Parameter |]" - , " Examples:" - , " - [" <> qqName <> "| Parameter plain |]" - , " - [" <> qqName <> "| Parameter recursive |]" - , " - [" <> qqName <> "| Parameter plain \"root\" |]" - , " But instead got: " <> unwords i - ] - in case extract $ words $ toText input of - Right (param, paramValue) -> [d| - instance ParameterHasEntrypoints $(conT $ mkName $ toString param) where - type ParameterEntrypointsDerivation $(conT $ mkName $ toString param) = $(paramValue) - |] - Left err -> failQQ qqName err +entrypointDoc = mkParserQQ "entrypointDoc" + "Parameter []" + [ "Parameter plain" + , "Parameter recursive" + , "Parameter plain \"root\"" + ] do + skipSpaces + typeName <- conT . mkName <$> hsIdent + skipSpaces + paramType <- conT <$> choice + [ string "plain" $> ''EpdPlain + , string "delegate" $> ''EpdDelegate + , string "recursive" $> ''EpdRecursive + , string "none" $> ''EpdNone + ] + skipSpaces + mbRootAnn <- optional $ litT . strTyLit <$> hsString + skipSpaces + eof + let epd = maybe paramType (\ann -> [t|EpdWithRoot $ann $paramType|]) mbRootAnn + pure $ [d| + instance ParameterHasEntrypoints $typeName where + type ParameterEntrypointsDerivation $typeName = $epd + |] -- | QuasiQuote that helps generating @CustomErrorHasDoc@ instance. -- @@ -96,98 +77,78 @@ -- 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 <> "| [] |]" - , " Examples:" - , " - [" <> qqName <> "| \"errorName\" exception \"Error description\" |]" - , " - [" <> qqName <> "| \"myError\" bad-argument \"An error happened\" () |]" - , " But instead got: " <> fromString i +errorDocArg = mkParserQQ "errorDocArg" + " []" + [ "\"errorName\" exception \"Error description\"" + , "\"myError\" bad-argument \"An error happened\" ()" + , "\"ctrError\" contract-internal \"Internal counter error\" Integer" + ] do + skipSpaces + errorName <- litT . strTyLit <$> hsString + skipSpaces + errorClass <- conE <$> choice + [ string "exception" $> 'ErrClassActionException + , string "bad-argument" $> 'ErrClassBadArgument + , string "contract-internal" $> 'ErrClassContractInternal + , string "unknown" $> 'ErrClassUnknown ] - - go :: String -> Q [Dec] - go input = - let - 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) = $errorArgType - instance CustomErrorHasDoc $(litT . strTyLit $ toString $ errorName) where - customErrClass = $(lift errorClassVal) - customErrDocMdCause = $(litE $ stringL $ toString $ errorDesc) - |] - Left err -> failQQ qqName err + skipSpaces + errorDesc <- litE . stringL <$> hsString + skipSpaces + errorArg <- optional $ conT . mkName <$> hsIdent + skipSpaces + eof + let errorArgType = fromMaybe [t|NoErrorArg|] errorArg + pure [d| + type instance ErrorArg $errorName = $errorArgType + instance CustomErrorHasDoc $errorName where + customErrClass = $errorClass + customErrDocMdCause = $errorDesc + |] -- | QuasiQuote that helps generating @TypeHasDoc@ instance. -- -- Usage: -- -- @ --- [typeDoc| \ \ |] --- [typeDoc| Storage "This is storage description" |] +-- [typeDoc| \ \ [\] |] +-- [typeDoc| Storage "This is storage description" |] +-- [typeDoc| Storage "This is storage description" stripFieldPrefix |] -- @ -- +-- @field naming strategy@ is optional, and is a function with signature @Text +-- -> Text@. Common strategies include 'id' and @stripFieldPrefix@. If +-- unspecified, ultimately defaults to 'id'. +-- -- See this [tutorial](https://indigo-lang.gitlab.io/contract-docs/) which -- includes this quasiquote. -- typeDoc :: QuasiQuoter -typeDoc = QuasiQuoter - { quoteExp = const $ failQQType qqName "expression" - , quotePat = const $ failQQType qqName "pattern" - , quoteType = const $ failQQType qqName "type" - , quoteDec = go - } - where - qqName = "typeDoc" - - go :: String -> Q [Dec] - go input = - case words $ toText $ input of - (param:value) -> +typeDoc = mkParserQQ "typeDoc" + " []" + [ "Storage \"This is storage description\"" + , "Storage \"This is storage description\" stripFieldPrefix" + ] do + skipSpaces + typeName <- conT . mkName <$> hsIdent + skipSpaces + desc <- litE . stringL <$> hsString + skipSpaces + fnstrategy <- optional $ varE . mkName <$> hsIdent + skipSpaces + eof + pure $ liftA2 (<>) + [d| + instance TypeHasDoc $typeName where + typeDocMdDescription = $desc + |] + case fnstrategy of + Nothing -> mempty + Just strat' -> [d| - instance TypeHasDoc $(conT $ mkName $ toString $ param) where - typeDocMdDescription = $(litE $ stringL $ toString $ stripQuote $ unwords value) + instance TypeHasFieldNamingStrategy $typeName where + typeFieldNamingStrategy = $strat' |] - i -> - failQQ qqName $ unlines - [ "Invalid arguments." - , " Expected arguments to be in the format of:" - , " - [" <> qqName <> "| |]" - , " Example:" - , " - [" <> qqName <> "| Storage \"This is storage description\" |]" - , " But instead got: " <> unwords i - ] -------------------------------------------------- -- Helper @@ -200,9 +161,31 @@ failQQType :: MonadFail m => Text -> Text -> m a failQQType qq typeTxt = failQQ qq $ "This QuasiQuoter cannot be used as a " <> typeTxt -stripQuote :: Text -> Text -stripQuote txt = - let - h = stripPrefix "\"" txt ?: txt - g = stripSuffix "\"" h ?: h - in g +mkParserQQ :: Text -> Text -> [Text] -> ReadP (Q [Dec]) -> QuasiQuoter +mkParserQQ qqName format examples parser = QuasiQuoter + { quoteExp = const $ failQQType qqName "expression" + , quotePat = const $ failQQType qqName "pattern" + , quoteType = const $ failQQType qqName "type" + , quoteDec = go + } + where + parse = readP_to_S parser + mkSample text = " - [" <> qqName <> "| " <> text <> " |]" + go input = case parse input of + [(res, "")] -> res + _ -> failQQ qqName $ errTemplate <> toText input + errTemplate = unlines $ + [ "Invalid arguments." + , " Expected arguments to be in the format of:" + , " - [" <> qqName <> "| " <> format <> " |]" + , " Examples:" + ] <> map mkSample examples <> + [ " But instead got: " ] + +hsIdent :: ReadP String +hsIdent = munch1 (not . isSpace) + +hsString :: ReadP String +hsString = do + String x <- lex + pure x