diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,23 @@ +0.16.0 +====== +* [!1370](https://gitlab.com/morley-framework/morley/-/merge_requests/1370) + Add `OverloadedRecordDot` support for Lorentz `StoreClass` + + Deprecated `StoreClass.Extra`, as it does more or less the same thing as + `OverloadedRecordDot`, but a lot worse. +* [!1369](https://gitlab.com/morley-framework/morley/-/merge_requests/1369) + Add `IsLabel` and `Default` instances for `EntrypointRef` + + Now `OverloadedLabels` can be used instead of `Call` + + `def` from `Data.Default` can be used instead of `CallDefault` +* [!1364](https://gitlab.com/morley-framework/morley/-/merge_requests/1364) + Update to LTS-21.4 (GHC 9.4.5) +* [!1358](https://gitlab.com/morley-framework/morley/-/merge_requests/1358) + Make missing `Generic` errors more readable +* [!1367](https://gitlab.com/morley-framework/morley/-/merge_requests/1367) + Add Range type to Lorentz, see `Lorentz.Range` module documentation + 0.15.2 ====== * [!1362](https://gitlab.com/morley-framework/morley/-/merge_requests/1362) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -> :warning: **Note: this project is being deprecated.** +> :warning: **Note: this project is deprecated.** > -> It will no longer be maintained after the activation of protocol "N" on the Tezos mainnet. +> It is no longer maintained since the activation of protocol "Nairobi" on the Tezos mainnet (June 24th, 2023). # Morley Lorentz EDSL 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.2 +version: 0.16.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 @@ -71,6 +71,7 @@ Lorentz.Polymorphic Lorentz.Prelude Lorentz.Print + Lorentz.Range Lorentz.Rebound Lorentz.Referenced Lorentz.ReferencedByName @@ -142,7 +143,7 @@ UndecidableInstances UndecidableSuperClasses ViewPatterns - ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode + ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-missing-kind-signatures -Wno-implicit-lift -Wno-unticked-promoted-constructors build-depends: aeson-pretty , base-noprelude >=4.7 && <5 diff --git a/src/Lorentz.hs b/src/Lorentz.hs --- a/src/Lorentz.hs +++ b/src/Lorentz.hs @@ -30,6 +30,7 @@ import Lorentz.Polymorphic as Exports import Lorentz.Prelude as Exports import Lorentz.Print as Exports +import Lorentz.Range as Exports import Lorentz.Rebound as Exports import Lorentz.Referenced as Exports import Lorentz.ReferencedByName as Exports diff --git a/src/Lorentz/ADT.hs b/src/Lorentz/ADT.hs --- a/src/Lorentz/ADT.hs +++ b/src/Lorentz/ADT.hs @@ -47,7 +47,6 @@ ) where import Data.Vinyl.Core (RMap(..), Rec(..)) -import GHC.Generics qualified as G import GHC.TypeLits (AppendSymbol, Symbol) import Lorentz.Base @@ -55,6 +54,7 @@ import Lorentz.Constraints import Morley.Michelson.Typed.Haskell.Instr import Morley.Michelson.Typed.Haskell.Value +import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Named import Morley.Util.Type (type (++)) @@ -321,14 +321,30 @@ constructStack = I (instrConstructStack @dt @(ToTs fields)) --- | Decompose a complex object into its fields --- --- >>> deconstruct @TestProduct # constructStack @TestProduct -$ testProduct --- TestProduct {fieldA = True, fieldB = 42, fieldC = ()} +{- | Decompose a complex object into its fields + +>>> deconstruct @TestProduct # constructStack @TestProduct -$ testProduct +TestProduct {fieldA = True, fieldB = 42, fieldC = ()} + +Will show human-readable error on a missing `Generic` instance: + +>>> data Foo = Foo () () +>>> deconstruct @Foo +... +... GHC.Generics.Rep Foo +... is stuck. Likely +... Generic Foo +... instance is missing or out of scope. +... + +>>> data Foo = Foo () () deriving (Generic, IsoValue) +>>> pretty $ deconstruct @Foo +[UNPAIR, DIP { }] +-} deconstruct :: forall dt fields st . ( InstrDeconstructC dt (ToTs st) - , fields ~ GFieldTypes (G.Rep dt) '[] + , fields ~ GFieldTypes (GRep dt) '[] , ToTs fields ++ ToTs st ~ ToTs (fields ++ st) ) => dt : st :-> (fields ++ st) diff --git a/src/Lorentz/Annotation.hs b/src/Lorentz/Annotation.hs --- a/src/Lorentz/Annotation.hs +++ b/src/Lorentz/Annotation.hs @@ -36,10 +36,15 @@ import Morley.Tezos.Address import Morley.Tezos.Core import Morley.Tezos.Crypto +import Morley.Util.Generic import Morley.Util.Named import Morley.Util.Text import Morley.Util.TypeLits +{- $setup +>>> import Lorentz +-} + ---------------------------------------------------------------------------- -- Annotation Customization ---------------------------------------------------------------------------- @@ -79,31 +84,47 @@ -- | Use this in the instance of @HasAnnotation@ when field annotations -- should not be generated. gGetAnnotationNoField - :: forall a. (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a) + :: forall a. (GHasAnnotation (GRep a), GValueType (GRep a) ~ ToT a) => FollowEntrypointFlag -> Notes (ToT a) gGetAnnotationNoField = - \_ -> gGetAnnotation @(G.Rep a) def NotFollowEntrypoint NotGenerateFieldAnn ^. _1 + \_ -> gGetAnnotation @(GRep 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 --- generated from the record fields. +{- | 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 generated from the record fields. + +Allows generic derivation. The type must have @Generic@ and @IsoValue@ +instances. + +>>> data Foo = Foo +>>> instance HasAnnotation Foo +... +... GHC.Generics.Rep Foo +... is stuck. Likely +... Generic Foo +... instance is missing or out of scope. +... + +>>> data Foo = Foo deriving (Generic, IsoValue) +>>> instance HasAnnotation Foo +-} class HasAnnotation a where getAnnotation :: FollowEntrypointFlag -> Notes (ToT a) default getAnnotation - :: ( GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a - , GIsSumType (G.Rep a), TypeHasFieldNamingStrategy a + :: ( GHasAnnotation (GRep a), GValueType (GRep a) ~ ToT a + , GIsSumType (GRep a), TypeHasFieldNamingStrategy a ) => FollowEntrypointFlag -> Notes (ToT a) getAnnotation b = - gGetAnnotation @(G.Rep a) (fromMaybe (gAnnOptions @a) $ annOptions @a) b GenerateFieldAnn ^. _1 + gGetAnnotation @(GRep a) (fromMaybe (gAnnOptions @a) $ annOptions @a) b GenerateFieldAnn ^. _1 annOptions :: Maybe AnnOptions annOptions = Nothing -gAnnOptions :: forall a. (GIsSumType (G.Rep a), TypeHasFieldNamingStrategy a) => AnnOptions +gAnnOptions :: forall a. (GIsSumType (GRep a), TypeHasFieldNamingStrategy a) => AnnOptions gAnnOptions - | gIsSumType @(G.Rep a) = def + | gIsSumType @(GRep a) = def | otherwise = def { fieldAnnModifier = typeFieldNamingStrategy @a } instance (HasAnnotation a, KnownSymbol name) diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs --- a/src/Lorentz/Base.hs +++ b/src/Lorentz/Base.hs @@ -89,7 +89,7 @@ >>> import Lorentz >>> import Prelude () >>> :{ -some_code :: KnownValue a => s :-> Lambda a () : s +some_code :: KnownValue a => s :-> ('[a] :-> '[()]) : s some_code = Lorentz.do push Lorentz.do drop diff --git a/src/Lorentz/Coercions.hs b/src/Lorentz/Coercions.hs --- a/src/Lorentz/Coercions.hs +++ b/src/Lorentz/Coercions.hs @@ -46,6 +46,7 @@ import Lorentz.Wrappable import Lorentz.Zip import Morley.Michelson.Typed +import Morley.Util.Generic import Morley.Util.Named ---------------------------------------------------------------------------- @@ -219,14 +220,30 @@ , CanCastTo e1 e2, CanCastTo f1 f2 ) => CanCastTo (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2) --- | Implementation of 'castDummy' for types composed from smaller types. --- It helps to ensure that all necessary constraints are requested in instance --- head. +{- | Implementation of 'castDummy' for types composed from smaller types. +It helps to ensure that all necessary constraints are requested in instance +head. + +Shows human-readable errors when @up@ is stuck. + +>>> data Foo = Foo +>>> castDummyG (Proxy @Foo) (Proxy @()) +... +... GHC.Generics.Rep Foo +... is stuck. Likely +... Generic Foo +... instance is missing or out of scope. +... + +>>> data Foo = Foo deriving Generic +>>> castDummyG (Proxy @Foo) (Proxy @()) +() +-} castDummyG - :: (Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b)) + :: (Generic a, Generic b, GCanCastTo (GRep a) (GRep b)) => Proxy a -> Proxy b -> () castDummyG (_ :: Proxy a) (_ :: Proxy b) = () - where _dummy = Dict @(Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b)) + where _dummy = Dict @(Generic a, Generic b, GCanCastTo (GRep a) (GRep b)) type family GCanCastTo x y :: Constraint where GCanCastTo (G.M1 _ _ x) (G.M1 _ _ y) = GCanCastTo x y 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 @@ -87,9 +87,9 @@ >>> epAddressToContract ... ... Can't check if type -... ToT p +... ToT p0 ... contains `operation` or nested `big_map`s. Perhaps you need to add -... NiceParameter p +... NiceParameter p0 ... constraint? You can also try adding a type annotation. ... -} @@ -105,12 +105,12 @@ Shows human-readable errors on ambiguity: ->>> push 1 +>>> push undefined ... ... Can't check if type -... ToT t +... ToT t0 ... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add -... NiceConstant t +... NiceConstant t0 ... constraint? You can also try adding a type annotation. ... @@ -136,9 +136,9 @@ >>> dup ... ... Can't check if type -... ToT a +... ToT a0 ... contains `ticket`. Perhaps you need to add -... Dupable a +... Dupable a0 ... constraint? You can also try adding a type annotation. ... @@ -164,9 +164,9 @@ >>> pack ... ... Can't check if type -... ToT a +... ToT a0 ... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add -... NicePackedValue a +... NicePackedValue a0 ... constraint? You can also try adding a type annotation. ... -} @@ -189,9 +189,9 @@ >>> unpack ... ... Can't check if type -... ToT a +... ToT a0 ... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add -... NiceUnpackedValue a +... NiceUnpackedValue a0 ... constraint? You can also try adding a type annotation. ... -} @@ -219,9 +219,9 @@ >>> view' @"SomeView" ... ... Can't check if type -... ToT ret +... ToT ret0 ... contains `operation`, `big_map` or `ticket`. Perhaps you need to add -... NiceViewable ret +... NiceViewable ret0 ... constraint? You can also try adding a type annotation. ... -} @@ -241,9 +241,9 @@ >>> emptySet ... ... Can't check if type -... ToT e +... ToT e0 ... contains non-comparable types. Perhaps you need to add -... NiceComparable e +... NiceComparable e0 ... constraint? You can also try adding a type annotation. ... -} @@ -266,9 +266,9 @@ >>> emptyBigMap @Integer ... ... Can't check if type -... ToT v +... ToT v0 ... contains `big_map`. Perhaps you need to add -... NiceNoBigMap v +... NiceNoBigMap v0 ... constraint? You can also try adding a type annotation. ... -} diff --git a/src/Lorentz/CustomArith/RationalArith.hs b/src/Lorentz/CustomArith/RationalArith.hs --- a/src/Lorentz/CustomArith/RationalArith.hs +++ b/src/Lorentz/CustomArith/RationalArith.hs @@ -40,7 +40,7 @@ , pairToRational ) where -import Prelude (Either(..), Eq, Integer, Maybe, Natural, Show, Text, show, unsafe, ($), (++), (==)) +import Prelude (Either(..), Eq, Integer, Maybe, Natural, Show, Text, show, unsafe, ($), (++), (==), type (~)) import Text.Show qualified import Lorentz.Annotation diff --git a/src/Lorentz/Entrypoints/Core.hs b/src/Lorentz/Entrypoints/Core.hs --- a/src/Lorentz/Entrypoints/Core.hs +++ b/src/Lorentz/Entrypoints/Core.hs @@ -45,13 +45,18 @@ , RequireAllUniqueEntrypoints' ) where +import Data.Default (Default(..)) +import Data.Type.Bool (type (&&)) +import Data.Type.Equality ((:~:)(..)) import Data.Typeable (typeRep) import Data.Vinyl (Rec(..)) import Fcf (Eval, Exp) import Fcf qualified import Fcf.Utils qualified as Fcf import Fmt (pretty) -import Type.Errors (DelayError, DelayErrorFcf, IfStuck) +import GHC.TypeLits (CharToNat, ConsSymbol, NatToChar, UnconsSymbol, type (-), type (<=?)) +import Type.Errors (DelayError, IfStuck) +import Unsafe.Coerce (unsafeCoerce) import Morley.Michelson.Typed import Morley.Michelson.Untyped qualified as U @@ -366,12 +371,35 @@ -- | Call the given entrypoint; calling default is not treated specially. -- You have to provide entrypoint name via passing it as type argument. -- - -- Unfortunatelly, here we cannot accept a label because in most cases our + -- Unfortunately, here we cannot accept a label because in most cases our -- entrypoints begin from capital letter (being derived from constructor name), -- while labels must start from a lower-case letter, and there is no way to -- make a conversion at type-level. Call :: NiceEntrypointName name => EntrypointRef ('Just name) +type UppercaseFirstChar :: Symbol -> Symbol +type family UppercaseFirstChar s where + UppercaseFirstChar s = TryUppercase (UnconsSymbol s) + +type TryUppercase :: Maybe (Char, Symbol) -> Symbol +type family TryUppercase mb where + TryUppercase 'Nothing = "" + TryUppercase ('Just '(c, s)) = UppercaseChar c `ConsSymbol` s + +type UppercaseChar :: Char -> Char +type family UppercaseChar c where + UppercaseChar c = + If ('a' <=? c && c <=? 'z') + (NatToChar (CharToNat c - 0x20)) + c + +instance (NiceEntrypointName (UppercaseFirstChar name), mname ~ 'Just (UppercaseFirstChar name)) + => IsLabel name (EntrypointRef mname) where + fromLabel = Call + +instance mname ~ 'Nothing => Default (EntrypointRef mname) where + def = CallDefault + -- | Constraint on type-level entrypoint name specifier. type NiceEntrypointName name = (KnownSymbol name, ForbidDefaultName name) @@ -480,30 +508,24 @@ 'Text " " ':<>: 'ShowType constraint ':$$: 'Text "constraint" -type CheckStuckEp cp mname fixedArg freeArg = - -- NB: if you're wondering why we need @freeArg@ and @fixedArg@, when - -- @fixedArg@ is fully polymorphic, GHC will assign it to the stuck type - -- family, and @ShowType@ will show FCF internals, which is exactly what we - -- wanted to avoid. Hence if @fixedArg@ is also stuck, we show @freeArg@ - -- instead. Finally, when there are no errors, we equate @freeArg@ and - -- @fixedArg@. +type CheckStuckEp cp mname arg = IfStuck (GetEntrypointArgCustom cp mname) - (IfStuck fixedArg - (DelayError (StuckEpErrorTemplate cp - (HasEntrypointArg cp (EntrypointRef mname) freeArg) - )) - (DelayErrorFcf (StuckEpErrorTemplate cp - (HasEntrypointArg cp (EntrypointRef mname) fixedArg) - )) - ) - (Fcf.Pure (freeArg ~ fixedArg)) + (DelayError (StuckEpErrorTemplate cp + (HasEntrypointArg cp (EntrypointRef mname) arg) + )) + (Fcf.Pure (GetEntrypointArgCustom cp mname ~ arg)) instance - ( CheckStuckEp cp mname arg' arg - , GetEntrypointArgCustom cp mname ~ arg' + ( CheckStuckEp cp mname arg , ParameterDeclaresEntrypoints cp) => - HasEntrypointArg cp (EntrypointRef mname) arg' where - useHasEntrypointArg epRef = + HasEntrypointArg cp (EntrypointRef mname) arg where + useHasEntrypointArg epRef + -- this ugliness is the best I could come up with... GHC 9.4 shows equality + -- constraint errors before custom type errors apparently, hence we can't + -- put the equality into instance head. But unless we got a custom error, we + -- have the equality, so it's perfectly safe to unsafeCoerce here. + -- -- @lierdakil + | Refl :: GetEntrypointArgCustom cp mname :~: arg <- unsafeCoerce Refl = case parameterEntrypointCallCustom @cp epRef of EntrypointCall{} -> (Dict, eprName epRef) diff --git a/src/Lorentz/Entrypoints/Doc.hs b/src/Lorentz/Entrypoints/Doc.hs --- a/src/Lorentz/Entrypoints/Doc.hs +++ b/src/Lorentz/Entrypoints/Doc.hs @@ -73,6 +73,7 @@ import Morley.Michelson.Typed.Haskell.Doc import Morley.Michelson.Typed.Haskell.Instr import Morley.Michelson.Untyped qualified as Untyped +import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Markdown import Morley.Util.Type @@ -483,12 +484,12 @@ => Rec (CaseClauseL inp out) (CaseClauses a) -> Rec (CaseClauseL inp out) (CaseClauses a) documentEntrypoints r = - gDocumentEntrypoints @(BuildEPTree' a) @kind @(G.Rep a) @'[] + gDocumentEntrypoints @(BuildEPTree' a) @kind @(GRep a) @'[] (ParamBuilder id) r (\RNil -> RNil) -- | Constraint for 'documentEntrypoints'. type DocumentEntrypoints kind a = - (Generic a, GDocumentEntrypoints (BuildEPTree' a) kind (G.Rep a) '[]) + (Generic a, GDocumentEntrypoints (BuildEPTree' a) kind (GRep a) '[]) type BuildEPTree' a = BuildEPTree (GetParameterEpDerivation a) a @@ -530,7 +531,6 @@ instance {-# OVERLAPPABLE #-} ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x - , KnownSymbol ctor , DocItem (DEntrypoint (EntrypointKindOverride kind)) , DeriveCtorFieldDoc ctor cf ) => @@ -556,7 +556,6 @@ instance {-# OVERLAPPABLE #-} ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x - , KnownSymbol ctor , DeriveCtorFieldDoc ctor cf , T.SingI heps ) => @@ -669,7 +668,7 @@ | areFinalizedParamBuildingSteps pbs = error "Applying finalization second time" | otherwise = - fromMaybe [PbsUncallable pbs] . listToMaybe . catMaybes $ + fromMaybe [PbsUncallable pbs] . safeHead . catMaybes $ epDescs <&> \epDesc -> tryShortcut epDesc pbs -- Further we check whether given 'EpCallingStep's form prefix of 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 @@ -28,6 +28,7 @@ import Morley.Michelson.Typed.Haskell.Value (GValueType) import Morley.Michelson.Untyped (FieldAnn, mkAnnotation, noAnn) import Morley.Util.Fcf (Over2, TyEqSing, type (<|>)) +import Morley.Util.Generic import Morley.Util.Type import Lorentz.Annotation @@ -159,7 +160,7 @@ -- ^ We reached complex parameter part and will need to ask how to process it. -- | Build 'EPTree' by parameter type. -type BuildEPTree mode a = GBuildEntrypointsTree mode (G.Rep a) +type BuildEPTree mode a = GBuildEntrypointsTree mode (GRep a) type family GBuildEntrypointsTree (mode :: Type) (x :: Type -> Type) :: EPTree where @@ -191,14 +192,14 @@ -- | Traverses sum type and constructs 'Notes' which report -- constructor names via field annotations. -type EntrypointsNotes mode ep a = (Generic a, GEntrypointsNotes mode ep (G.Rep a)) +type EntrypointsNotes mode ep a = (Generic a, GEntrypointsNotes mode ep (GRep a)) -- | Makes up notes with proper field annotations for given parameter. mkEntrypointsNotes :: forall mode ep a. (EntrypointsNotes mode ep a, GenericIsoValue a, HasCallStack) => Notes (ToT a) -mkEntrypointsNotes = fst $ gMkEntrypointsNotes @mode @ep @(G.Rep a) +mkEntrypointsNotes = fst $ gMkEntrypointsNotes @mode @ep @(GRep a) -- | Makes up a way to lift entrypoint argument to full parameter. mkEpLiftSequence @@ -208,20 +209,20 @@ ) => Label name -> EpConstructionRes (ToT a) (Eval (LookupEntrypoint mode ep a name)) -mkEpLiftSequence = gMkEpLiftSequence @mode @ep @(G.Rep a) +mkEpLiftSequence = gMkEpLiftSequence @mode @ep @(GRep a) -- | Makes up descriptions of entrypoints calling. mkEpDescs :: forall mode ep a. (EntrypointsNotes mode ep a) => Rec EpCallingDesc (AllEntrypoints mode ep a) -mkEpDescs = gMkDescs @mode @ep @(G.Rep a) +mkEpDescs = gMkDescs @mode @ep @(GRep a) -- | Fetches information about all entrypoints - leaves of 'Or' tree. -type AllEntrypoints mode ep a = GAllEntrypoints mode ep (G.Rep a) +type AllEntrypoints mode ep a = GAllEntrypoints mode ep (GRep a) -- | Fetches information about all entrypoints - leaves of 'Or' tree. -type LookupEntrypoint mode ep a = GLookupEntrypoint mode ep (G.Rep a) +type LookupEntrypoint mode ep a = GLookupEntrypoint mode ep (GRep a) -- | Generic traversal for 'EntrypointsNotes'. class GEntrypointsNotes (mode :: Type) (ep :: EPTree) (x :: Type -> Type) where diff --git a/src/Lorentz/Expr.hs b/src/Lorentz/Expr.hs --- a/src/Lorentz/Expr.hs +++ b/src/Lorentz/Expr.hs @@ -95,7 +95,7 @@ , viewE ) where -import Prelude (HasCallStack, foldr, uncurry, ($)) +import Prelude (HasCallStack, foldr, uncurry, ($), type (~)) import Lorentz.Arith import Lorentz.Base diff --git a/src/Lorentz/Extensible.hs b/src/Lorentz/Extensible.hs --- a/src/Lorentz/Extensible.hs +++ b/src/Lorentz/Extensible.hs @@ -70,6 +70,7 @@ import Lorentz.Pack import Morley.AsRPC (HasRPCRepr(..)) import Morley.Michelson.Typed +import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Markdown import Morley.Util.Type @@ -82,8 +83,8 @@ instance HasRPCRepr (Extensible x) where type AsRPC (Extensible x) = Extensible x -type ExtVal x = (Generic x, GExtVal x (G.Rep x)) -type GetCtors x = GGetCtors (G.Rep x) +type ExtVal x = (NiceGeneric x, GExtVal x (GRep x)) +type GetCtors x = GGetCtors (GRep x) -- | Converts a value from a Haskell representation to its -- extensible Michelson representation (i.e. (Natural, Bytestring) pair). @@ -226,7 +227,7 @@ -- | Implementation for 'typeDocDependencies' of the corresponding @Extensible@. extensibleDocDependencies :: Proxy x -> [SomeDocDefinitionItem] default extensibleDocDependencies - :: (Generic x, GTypeHasDoc (G.Rep x)) + :: (Generic x, GTypeHasDoc (GRep x)) => Proxy x -> [SomeDocDefinitionItem] extensibleDocDependencies = genericTypeDocDependencies diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs --- a/src/Lorentz/Instr.hs +++ b/src/Lorentz/Instr.hs @@ -348,7 +348,7 @@ => s :-> Map k v : s emptyMap = I EMPTY_MAP -emptyBigMap :: (NiceComparable k, KnownValue v, NiceNoBigMap v) +emptyBigMap :: (NiceComparable k, NiceNoBigMap v) => s :-> BigMap k v : s emptyBigMap = I EMPTY_BIG_MAP diff --git a/src/Lorentz/Layouts/NonDupable.hs b/src/Lorentz/Layouts/NonDupable.hs --- a/src/Lorentz/Layouts/NonDupable.hs +++ b/src/Lorentz/Layouts/NonDupable.hs @@ -33,7 +33,7 @@ -- non-dupable elements are rare and so are supposed to be updated -- less often. -- --- Unfortunatelly, there seems to be no decent way to see whether a type is +-- Unfortunately, there seems to be no decent way to see whether a type is -- dupable or not at TH time, so we have to accept some information explicitly. -- To ensure that this information is up to date, each time calling this -- function __we encourage the user to also add a test__ using utilities from diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs --- a/src/Lorentz/Macro.hs +++ b/src/Lorentz/Macro.hs @@ -399,7 +399,7 @@ -- ... -- ... error: -- ... Couldn't match type: '[] --- ... with: a0 : o'0 +-- ... with: Integer : o'0 -- ... -- -- When the number of elements is larger than the size of the stack, @framedN@ diff --git a/src/Lorentz/Prelude.hs b/src/Lorentz/Prelude.hs --- a/src/Lorentz/Prelude.hs +++ b/src/Lorentz/Prelude.hs @@ -21,6 +21,7 @@ , undefined , error , (!) + , type (~) ) where import Named ((!)) diff --git a/src/Lorentz/Range.hs b/src/Lorentz/Range.hs new file mode 100644 --- /dev/null +++ b/src/Lorentz/Range.hs @@ -0,0 +1,799 @@ +-- SPDX-FileCopyrightText: 2023 Oxhead Alpha +-- SPDX-License-Identifier: LicenseRef-MIT-OA + +{-# LANGUAGE FunctionalDependencies, RoleAnnotations #-} + +-- | Range type +module Lorentz.Range + ( RangeBoundaryInclusion(..) + , Range(..) + , RangeIE(..) + , RangeEI(..) + , RangeEE(..) + , OnRangeAssertFailure(..) + , RangeFailureInfo(..) + , RangeBoundary + , NiceRange + , CanCheckEmpty + , mkRange + , mkRange_ + , mkRangeFor + , mkRangeFor_ + , mkRangeForSafe_ + , fromRange_ + , toRange_ + , rangeLower + , rangeUpper + , rangeLower_ + , rangeUpper_ + , inRange + , inRange_ + , inRangeCmp + , inRangeCmp_ + , assertInRange_ + , assertInRangeSimple_ + , isRangeEmpty + , isRangeEmpty_ + , assertRangeNonEmpty_ + , mkOnRangeAssertFailureSimple + , customErrorORAF + , customErrorORAFSimple + -- * Internals + , isInclusive + ) where + +import Data.Coerce (coerce) +import Data.Constraint (Bottom(..)) +import Data.Singletons (demote) +import Fmt (Buildable(..)) +import GHC.TypeLits (ErrorMessage(..), TypeError) + +import Lorentz.ADT as L +import Lorentz.Annotation as L +import Lorentz.Arith as L +import Lorentz.Base as L +import Lorentz.Coercions as L +import Lorentz.Constraints.Scopes as L +import Lorentz.Doc as L +import Lorentz.Errors as L +import Lorentz.Instr as L +import Lorentz.Macro as L +import Lorentz.Value +import Morley.Michelson.Typed qualified as T +import Morley.Michelson.Untyped (noAnn, pattern UnsafeAnnotation, typeAnnQ, unAnnotation) +import Morley.Util.Interpolate (i) +import Morley.Util.Named + +{- $setup +>>> import Fmt (pretty) +>>> import Lorentz +>>> import Morley.Util.Named +-} + +-- | Whether to include boundary in 'Range' +data RangeBoundaryInclusion = IncludeBoundary | ExcludeBoundary + +-- | Helper class for 'RangeBoundaryInclusion'. +type RangeBoundary :: RangeBoundaryInclusion -> Constraint +class (DefaultToInclusive r, Typeable r) => RangeBoundary r where + -- | Parentheses for the 'Buildable' instance + rangeParens :: (Text, Text) + -- | Haskell comparison which either includes or excludes the boundary + inRangeComp :: Ord a => a -> a -> Bool + -- | Lorentz comparison which either includes or excludes the boundary + inRangeComp_ :: NiceComparable a => a : a : s :-> Bool : s + -- | Human-readable name for the tag + rangeName :: Text + -- | Value-level representation as 'Bool' + isInclusive :: Bool + +instance RangeBoundary 'IncludeBoundary where + rangeParens = ("[", "]") + inRangeComp = (<=) + inRangeComp_ = L.ge + rangeName = "Inclusive" + isInclusive = True + +instance RangeBoundary 'ExcludeBoundary where + rangeParens = ("(", ")") + inRangeComp = (<) + inRangeComp_ = L.gt + rangeName = "Exclusive" + isInclusive = False + +-- | Hacky typeclass to default boundaries to 'IncludeBoundary'. +class DefaultToInclusive bound +instance DefaultToInclusive 'IncludeBoundary +instance DefaultToInclusive 'ExcludeBoundary +instance {-# incoherent #-} a ~ 'IncludeBoundary => DefaultToInclusive a + +{- | The main range type. This exists as a base for other (new)types like +'Range', 'RangeEE', etc. + +The zoo of 'Range' types exists mostly for the purpose of making errors less +scary: + +>>> f = push (1 :: Integer, 2 :: Natural) # unpair # inRange_ +... +... error: +... Couldn't match type ‘Range Natural’ with ‘Integer’ +... + +>>> mkRange_ @_ @_ @_ @Integer # add -$ #min :! 123 ::: #max :! 321 ::: 555 +... +... error: +... No instance for (ArithOpHs +... Morley.Michelson.Typed.Arith.Add (Range Integer) Integer ()) +... +-} +type Range' :: RangeBoundaryInclusion -> RangeBoundaryInclusion -> Type -> Type +data Range' lower upper a = Range' { rangeLower' :: a, rangeUpper' :: a } + deriving stock (Generic, Show, Eq) + deriving anyclass IsoValue +type role Range' nominal nominal _ + +instance (HasAnnotation a, RangeBoundary lower, RangeBoundary upper) + => HasAnnotation (Range' lower upper a) where + getAnnotation f = + let aann = getAnnotation @a f + e :: forall x. RangeBoundary x => Text + e | isInclusive @x = "i" + | otherwise = "e" + lann = UnsafeAnnotation $ "l_" <> e @lower + uann = UnsafeAnnotation $ "u_" <> e @upper + in T.NTPair [typeAnnQ|range|] lann uann noAnn noAnn aann aann + +-- | Default range, inclusive in both boundaries. +newtype Range a = MkRangeII (Range' 'IncludeBoundary 'IncludeBoundary a) + deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq) + deriving anyclass IsoValue + +-- | Range exclusive in both boundaries. +newtype RangeEE a = MkRangeEE (Range' 'ExcludeBoundary 'ExcludeBoundary a) + deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq) + deriving anyclass IsoValue + +-- | Range inclusive in lower boundary, but exclusive in upper boundary. +newtype RangeIE a = MkRangeIE (Range' 'IncludeBoundary 'ExcludeBoundary a) + deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq) + deriving anyclass IsoValue + +-- | Range exclusive in lower boundary, but inclusive in upper boundary. +newtype RangeEI a = MkRangeEI (Range' 'ExcludeBoundary 'IncludeBoundary a) + deriving newtype (TypeHasDoc, Generic, Show, Buildable, HasAnnotation, Eq) + deriving anyclass IsoValue + +-- We have to export data constructors because otherwise Coercible complains in +-- some contexts, but those are not intended to be used by the end-users. +{-# WARNING MkRangeII, MkRangeEE, MkRangeEI, MkRangeIE + "Avoid using data constructors directly, use mkRange instead." + #-} + +instance (TypeHasDoc a, RangeBoundary lower, RangeBoundary upper) + => TypeHasDoc (Range' lower upper a) where + typeDocName _ = case (isInclusive @lower, isInclusive @upper) of + (True, True) -> "Range" + (True, False) -> "RangeIE" + (False, True) -> "RangeEI" + (False, False) -> "RangeEE" + typeDocMdDescription = + "Signifies a range, which is " <> build (rangeName @lower) <> " wrt its lower boundary and " + <> build (rangeName @upper) <> " wrt its upper boundary." + typeDocMdReference pa = + customTypeDocMdReference + (typeDocName pa, DType pa) [DType (Proxy @a)] + typeDocHaskellRep pa _ = Just $ + ( Just $ fromString . toString $ typeDocName pa <> " Integer" + , [T.ConstructorRep (typeDocName pa) Nothing fields] + ) + where + fields = case getAnnotation @(Range' lower upper Integer) NotFollowEntrypoint of + T.NTPair _ lower upper _ _ _ _ -> + [ T.FieldRep (Just $ unAnnotation lower) (Just "Lower boundary") intRef + , T.FieldRep (Just $ unAnnotation upper) (Just "Upper boundary") intRef + ] + intRef = SomeTypeWithDoc $ Proxy @Integer + typeDocMichelsonRep pa = + ( Just $ fromString . toString $ typeDocName pa <> " Integer" + , demote @(ToT (Range' lower upper Integer)) + ) + +{- | Pretty-printer for Range. + +>>> pretty $ mkRange 123 456 +[123, 456] + +>>> pretty $ mkRange @RangeEE 123 456 +(123, 456) + +>>> pretty $ mkRange @RangeIE 123 456 +[123, 456) + +>>> pretty $ mkRange @_ @'IncludeBoundary @'ExcludeBoundary 123 456 +[123, 456) +-} +instance (RangeBoundary lower, RangeBoundary upper, Buildable a) + => Buildable (Range' lower upper a) where + build (Range' l r) = [i|#{lpar}#{l}, #{r}#{rpar}|] + where lpar = fst $ rangeParens @lower + rpar = snd $ rangeParens @upper + +-- | Helper class for the 'Range' types that encapsulates common features. +class (RangeBoundary lower, RangeBoundary upper, ToT (range a) ~ ToT (a, a), KnownValue (range a) + , Coercible range (Range' lower upper)) + => NiceRange range lower upper a | range -> lower upper, lower upper -> range + +instance KnownValue a => NiceRange Range 'IncludeBoundary 'IncludeBoundary a +instance KnownValue a => NiceRange RangeIE 'IncludeBoundary 'ExcludeBoundary a +instance KnownValue a => NiceRange RangeEI 'ExcludeBoundary 'IncludeBoundary a +instance KnownValue a => NiceRange RangeEE 'ExcludeBoundary 'ExcludeBoundary a + +-- | Get a range's lower bound +rangeLower :: forall range lower upper a. NiceRange range lower upper a => range a -> a +rangeLower = coerce $ rangeLower' @lower @upper @a + +-- | Get a range's upper bound. +rangeUpper :: forall range lower upper a. NiceRange range lower upper a => range a -> a +rangeUpper = coerce $ rangeUpper' @lower @upper @a + +{- | Construct a 'Range'. Bear in mind, no checks are performed, so this can +construct empty ranges. + +You can control whether boundaries are included or excluded by choosing the +appropriate type out of 'Range', 'RangeIE', 'RangeEI' and 'RangeEE', either via +a type application or a type annotation. Alternatively, you can set @lower@ and +@upper@ type arguments to 'IncludeBoundary' or 'ExcludeBoundary'. If +unspecified, the default is to include both boundaries. + +>>> pretty $ mkRange 123 456 +[123, 456] + +>>> pretty $ mkRange 123 123 +[123, 123] + +>>> pretty $ mkRange 123 0 -- note this range is empty! +[123, 0] + +>>> pretty (mkRange 123 456 :: RangeEE Integer) +(123, 456) + +>>> pretty $ mkRange @RangeIE 123 456 +[123, 456) + +>>> pretty $ mkRange @_ @'IncludeBoundary @'ExcludeBoundary 123 456 +[123, 456) + +>>> pretty $ mkRange @RangeEI 123 456 +(123, 456] + +>>> pretty $ mkRange @_ @'ExcludeBoundary @'IncludeBoundary 123 456 +(123, 456] +-} +mkRange :: forall range lower upper a. NiceRange range lower upper a => a -> a -> range a +mkRange = coerce $ Range' @lower @upper @a + +{- | Convert a 'Range' to a pair of @(lower, upper)@ + +>>> mkRangeForSafe_ # fromRange_ -$ #start :! (123 :: Integer) ::: #length :! (456 :: Natural) +(123,579) +-} +fromRange_ :: NiceRange range lower upper a => range a : s :-> (a, a) : s +fromRange_ = forcedCoerce_ + +{- | Convert a pair of @(lower, upper)@ to 'Range'. This has the potential to +construct an empty range. + +>>> pretty (toRange_ -$ (123, 456) :: Range Integer) +[123, 456] + +>>> pretty (toRange_ -$ (123, -100500) :: Range Integer) -- empty range +[123, -100500] +-} +toRange_ :: NiceRange range lower upper a => (a, a) : s :-> range a : s +toRange_ = forcedCoerce_ + +{- | Get the lower bound of a 'Range' + +>>> mkRange_ # rangeLower_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer) +123 +-} +rangeLower_ :: NiceRange range lower upper a => range a : s :-> a : s +rangeLower_ = fromRange_ # car + +{- | Get the upper bound of a 'Range' + +>>> mkRange_ # rangeUpper_ -$ #min :! (123 :: Integer) ::: #max :! (456 :: Integer) +456 +-} +rangeUpper_ :: NiceRange range lower upper a => range a : s :-> a : s +rangeUpper_ = fromRange_ # cdr + +{- | Construct a range by specifying the start and length instead of lower and +upper bounds. @lower = start@, and @upper = start + length@. + +Note this can still construct empty ranges if @length@ is negative. + +See 'mkRange' for the information on how to control boundary inclusion. + +>>> pretty $ mkRangeFor 123 123 +[123, 246] + +>>> pretty $ mkRangeFor 123 (-123) -- empty range +[123, 0] +-} +mkRangeFor :: (NiceRange range lower upper a, Num a) => a -> a -> range a +mkRangeFor start len = mkRange start (start + len) + +{- | The Lorentz version of 'mkRange' + +>>> pretty $ mkRange_ -$ (#min :! (123 :: Integer)) ::: (#max :! (123 :: Integer)) +[123, 123] + +>>> pretty $ mkRange_ @RangeEE -$ (#min :! (123 :: Integer)) ::: (#max :! (123 :: Integer)) +(123, 123) + +Notice the latter range is empty by construction. +-} +mkRange_ + :: NiceRange range lower upper a + => ("min" :! a) : ("max" :! a) : s :-> range a : s +mkRange_ = fromNamed #min # dip (fromNamed #max) # L.pair # toRange_ + +{- | The Lorentz version of 'mkRangeFor'. Note that @length@ can be of different +type from @start@. + +>>> pretty $ mkRangeFor_ -$ (#start :! (123 :: Integer)) ::: (#length :! (123 :: Natural)) +[123, 246] +-} +mkRangeFor_ + :: ( NiceRange range lower upper a + , Dupable a + , ArithOpHs T.Add a b a + ) + => ("start" :! a) : ("length" :! b) : s :-> range a : s +mkRangeFor_ + = fromNamed #start + # L.dup + # L.dip + ( L.dip (fromNamed #length) + # L.add + ) + # L.pair + # toRange_ + +{- | A version of 'mkRangeFor_' that requires @length@ to be isomorphic to a +@nat@ and the range to be inclusive in both bounds. This guarantees that the +range is non-empty. + +>>> pretty $ mkRangeForSafe_ -$ (#start :! (123 :: Integer)) ::: (#length :! (1 :: Natural)) +[123, 124] +-} +mkRangeForSafe_ + :: forall a b s. + ( Dupable a + , ArithOpHs T.Add a b a + , ToT b ~ 'T.TNat + ) + => ("start" :! a) : ("length" :! b) : s :-> Range a : s +mkRangeForSafe_ = mkRangeFor_ + where + _ = T.Dict @(ToT b ~ 'T.TNat) + +{- | Check if a value is in range. + +>>> let range = mkRange -2 2 +>>> inRange range <$> [-4..4] +[False,False,True,True,True,True,True,False,False] +-} +inRange :: (NiceRange range lower upper a, Ord a) => range a -> a -> Bool +inRange = (== EQ) ... inRangeCmp + +{- | Check if a value is in range, and return 'Ordering'. This function returns +'EQ' if the value is in range, 'LT' if it underflows, and 'GT if it overflows. + +>>> inRangeCmp (mkRange -2 2) <$> [-4..4] +[LT,LT,EQ,EQ,EQ,EQ,EQ,GT,GT] + +>>> inRangeCmp (mkRange @RangeIE -2 2) <$> [-4..4] +[LT,LT,EQ,EQ,EQ,EQ,GT,GT,GT] +-} +inRangeCmp + :: forall range lower upper a. (NiceRange range lower upper a, Ord a) + => range a -> a -> Ordering +inRangeCmp r x + | Prelude.not $ inRangeComp @lower (rangeLower r) x = LT + | Prelude.not $ inRangeComp @upper x (rangeUpper r) = GT + | otherwise = EQ + +{- | Lorentz version of 'inRange'. + +>>> range = mkRange 0 10 :: RangeEE Integer +>>> testCode = push range # inRange_ +>>> testCode -$ 123 +False +>>> testCode -$ 10 +False +>>> testCode -$ 0 +False +>>> testCode -$ -123 +False +>>> testCode -$ 1 +True +>>> testCode -$ 5 +True +-} +inRange_ + :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a) + => range a : a : s :-> Bool : s +inRange_ + = fromRange_ + # L.unpair + # L.dupN @3 + # inRangeComp_ @lower + # L.dug @2 + # inRangeComp_ @upper + # L.and + +{- | Lorentz version of 'inRangeCmp'. Instead of 'Ordering', returns an +'Integer', @-1@ if the value underflows, @0@ if it's in range and @1@ if it +overflows. + +Use 'inRange_' if you don't particularly care whether the range is under- or +overflowed. + +>>> range = mkRange 0 10 :: Range Integer +>>> testCode = push range # inRangeCmp_ +>>> testCode -$ 123 +1 +>>> testCode -$ -123 +-1 +>>> testCode -$ 5 +0 + +>>> push (mkRange 0 10 :: RangeIE Integer) # inRangeCmp_ -$ 0 +0 +>>> push (mkRange 0 10 :: RangeIE Integer) # inRangeCmp_ -$ 10 +1 + +>>> push (mkRange 0 10 :: RangeEI Integer) # inRangeCmp_ -$ 0 +-1 +>>> push (mkRange 0 10 :: RangeEI Integer) # inRangeCmp_ -$ 10 +0 + +>>> push (mkRange 0 10 :: RangeEE Integer) # inRangeCmp_ -$ 0 +-1 +>>> push (mkRange 0 10 :: RangeEE Integer) # inRangeCmp_ -$ 10 +1 + +When lower and upper boundaries are the same and at least one boundary is +exclusive, it is ambiguous whether the value on the boundary overflows or +underflows. In this case, lower boundary takes precedence if it's exclusive. + +>>> push (mkRange 0 0 :: RangeIE Integer) # inRangeCmp_ -$ 0 +1 + +>>> push (mkRange 0 0 :: RangeEI Integer) # inRangeCmp_ -$ 0 +-1 + +>>> push (mkRange 0 0 :: RangeEE Integer) # inRangeCmp_ -$ 0 +-1 +-} +inRangeCmp_ + :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a) + => range a : a : s :-> Integer : s +inRangeCmp_ + = fromRange_ + # L.unpair + # L.dupN @3 + # inRangeComp_ @lower + # flip if_ (L.dropN @2 # push (-1)) + (inRangeComp_ @upper + # if_ (push 0) (push 1) + ) + +{- | Assert a value is in range; throw errors if it's under- or overflowing. See +'OnRangeAssertFailure' for information on how to specify errors. + +If you don't need verbose error reporting, consider using +'assertInRangeSimple_'. +-} +assertInRange_ + :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a) + => OnRangeAssertFailure a + -> range a : a : s :-> s +assertInRange_ OnRangeAssertFailure{..} + = dip (toNamed #value) + # L.dupN @2 + # L.dupN @2 + # fromRange_ + # L.unpair + # L.dupN @3 + # fromNamed #value + # inRangeComp_ @lower + # if_ + ( dip (fromNamed #value) + # inRangeComp_ @upper + # if_ (L.dropN @2) + ( rangeUpper_ # toNamed #boundary + # push (isInclusive @upper) + # mkRangeFailureInfo + # orafOverflow + ) + ) + ( L.dropN @2 + # rangeLower_ # toNamed #boundary + # push (isInclusive @lower) + # mkRangeFailureInfo + # orafUnderflow + ) + +{- | A cheaper version of 'assertInRange_' without fancy error reporting. + +>>> let range = mkRange 123 456 :: Range Integer +>>> let err = failUsing [mt|failure|] +>>> assertInRangeSimple_ err -$ range ::: 123 ::: () +() +>>> assertInRangeSimple_ err -$ range ::: 1 ::: () +*** Exception: Reached FAILWITH instruction with '"failure"' ... +... +-} +assertInRangeSimple_ + :: forall range lower upper a s. (NiceRange range lower upper a, NiceComparable a, Dupable a) + => (forall s' any. s' :-> any) + -> range a : a : s :-> s +assertInRangeSimple_ err + = inRange_ # if_ nop err + +-- | Small helper to construct 'RangeFailureInfo' in Lorentz code. +mkRangeFailureInfo + :: forall a s. IsoValue a + => Bool : "boundary" :! a : "value" :! a : s :-> RangeFailureInfo a : s +mkRangeFailureInfo = coerce $ constructStack @(RangeFailureInfo a) @_ @s + +-- | Information about the range check failure +data RangeFailureInfo a = RangeFailureInfo + { rfiInclusive :: Bool -- ^ Whether the boundary is inclusive or not + , rfiBoundary :: a -- ^ The boundary that failed to check + , rfiValue :: a -- ^ The value that failed to check + } deriving stock Generic + deriving anyclass IsoValue + deriving TypeHasFieldNamingStrategy via T.FieldCamelCase + +instance TypeHasDoc a => TypeHasDoc (RangeFailureInfo a) where + type TypeDocFieldDescriptions (RangeFailureInfo a) = + '[ '( "RangeFailureInfo", '( 'Nothing, + '[ '("rfiInclusive", "Whether the boundary is inclusive or not") + , '("rfiBoundary", "The boundary that failed to check") + , '("rfiValue", "The value that failed to check") + ]) + ) + ] + typeDocMdDescription = "Information about the range check failure" + typeDocMdReference = poly1TypeDocMdReference + typeDocHaskellRep + = T.haskellRepMap (typeFieldNamingStrategy @(RangeFailureInfo a)) + $ concreteTypeDocHaskellRep @(RangeFailureInfo Integer) + typeDocMichelsonRep = concreteTypeDocMichelsonRep @(RangeFailureInfo Integer) + +{- | Specify on how to fail on range overflow or underflow in 'assertInRange_'. + +This expects two always-failing Lorentz functions, one will be called on +underflow, another on overflow. + +See 'customErrorORAF' for a simpler helper to use with custom Lorentz errors. + +See 'mkOnRangeAssertFailureSimple' if you don't care about distinguishing +underflow and overflow. +-} +data OnRangeAssertFailure a = OnRangeAssertFailure + { orafUnderflow :: forall s any. RangeFailureInfo a : s :-> any + , orafOverflow :: forall s any. RangeFailureInfo a : s :-> any + } + +-- | Construct 'OnRangeAssertFailure' that performs the same action on both +-- overflow and underflow +mkOnRangeAssertFailureSimple + :: (forall s any. RangeFailureInfo a : s :-> any) + -> OnRangeAssertFailure a +mkOnRangeAssertFailureSimple f = OnRangeAssertFailure f f + +{- | Construct 'OnRangeAssertFailure' that throws custom errors. Errors used +must be defined somewhere using @errorDocArg@ or equivalent, and must accept +'RangeFailureInfo' as the argument. + +>>> :{ +type RFII = RangeFailureInfo Integer +-- +[errorDocArg| "overflowInt" exception "Integer range overflow" RFII |] +[errorDocArg| "underflowInt" exception "Integer range underflow" RFII |] +-- +testCode :: Range Integer : Integer : s :-> s +testCode = assertInRange_ $ customErrorORAF ! #underflow #underflowInt ! #overflow #overflowInt +:} + +>>> testCode -$ mkRange 0 10 ::: 123 ::: () +*** Exception: Reached FAILWITH instruction with 'Pair "OverflowInt" (Pair True (Pair 10 123))' +... +>>> testCode -$ mkRange 0 10 ::: -1 ::: () +*** Exception: Reached FAILWITH instruction with 'Pair "UnderflowInt" (Pair True (Pair 0 -1))' +... +>>> testCode -$ mkRange 0 10 ::: 5 ::: () +() + +-} +customErrorORAF + :: (NiceConstant a + , ErrorArg underflow ~ RangeFailureInfo a + , ErrorArg overflow ~ RangeFailureInfo a + , CustomErrorHasDoc underflow + , CustomErrorHasDoc overflow + ) + => ("underflow" :! Label underflow) + -> ("overflow" :! Label overflow) + -> OnRangeAssertFailure a +customErrorORAF (arg #underflow -> ufl) (arg #overflow -> ofl) = OnRangeAssertFailure + { orafUnderflow = failCustom ufl + , orafOverflow = failCustom ofl + } + +{- | A version of 'customErrorORAF' that uses the same error for both underflow +and overflow. + +>>> :{ +type RFII = RangeFailureInfo Integer +[errorDocArg| "rangeError" exception "Integer range check error" RFII |] +-- +testCode :: Range Integer : Integer : s :-> s +testCode = assertInRange_ $ customErrorORAFSimple #rangeError +:} + +>>> testCode -$ mkRange 0 10 ::: 123 ::: () +*** Exception: Reached FAILWITH instruction with 'Pair "RangeError" (Pair True (Pair 10 123))' +... +>>> testCode -$ mkRange 0 10 ::: -1 ::: () +*** Exception: Reached FAILWITH instruction with 'Pair "RangeError" (Pair True (Pair 0 -1))' ... +... +>>> testCode -$ mkRange 0 10 ::: 5 ::: () +() +-} +customErrorORAFSimple + :: (NiceConstant a + , ErrorArg err ~ RangeFailureInfo a + , CustomErrorHasDoc err + ) + => Label err + -> OnRangeAssertFailure a +customErrorORAFSimple err = mkOnRangeAssertFailureSimple $ failCustom err + +{- | Check if a range is empty by construction. Note, however, this function is +not suitable for checking whether a range with both boundaries excluded is +empty, and hence will produce a type error when such a check is attempted. + +>>> isRangeEmpty $ mkRange 0 1 +False +>>> isRangeEmpty $ mkRange 0 0 +False +>>> isRangeEmpty $ mkRange 0 -1 +True + +>>> isRangeEmpty $ mkRange @RangeIE 0 1 +False +>>> isRangeEmpty $ mkRange @RangeIE 0 0 +True +>>> isRangeEmpty $ mkRange @RangeIE 0 -1 +True + +>>> isRangeEmpty $ mkRange @RangeEI 0 1 +False +>>> isRangeEmpty $ mkRange @RangeEI 0 0 +True +>>> isRangeEmpty $ mkRange @RangeEI 0 -1 +True + +>>> isRangeEmpty $ mkRange @RangeEE 0 1 +... +... error: +... This function can't be used to check whenter a range with both boundaries excluded is empty +... +-} +isRangeEmpty + :: forall range lower upper a. + (NiceRange range lower upper a, Ord a, CanCheckEmpty lower upper) + => range a -> Bool +isRangeEmpty r = checkEmpty @lower @upper (rangeLower r) (rangeUpper r) + +{- | Lorentz version of 'isRangeEmpty'. Same caveats apply. + +>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1) +False +>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0) +False +>>> mkRange_ # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1) +True + +>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1) +False +>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0) +True +>>> mkRange_ @RangeIE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1) +True + +>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1) +False +>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 0) +True +>>> mkRange_ @RangeEI # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! -1) +True + +>>> mkRange_ @RangeEE # isRangeEmpty_ -$ (#min :! 0) ::: (#max :! 1) +... +... error: +... This function can't be used to check whenter a range with both boundaries excluded is empty +... +-} +isRangeEmpty_ + :: forall range lower upper a s. + ( NiceRange range lower upper a + , CanCheckEmpty lower upper + , NiceComparable a + ) + => range a : s :-> Bool : s +isRangeEmpty_ + = fromRange_ + # L.unpair + # checkEmpty_ @lower @upper + +-- | Helper class to check if a range is empty. Gives up when both boundaries +-- are exclusive. +class CanCheckEmpty l u where + -- | Returns 'True' when a range is empty, 'False' otherwise. + checkEmpty :: Ord a => a -> a -> Bool + -- | Lorentz version of 'checkEmpty'. + checkEmpty_ :: NiceComparable a => a : a : s :-> Bool : s +instance CanCheckEmpty 'IncludeBoundary 'IncludeBoundary where + checkEmpty = (>) + checkEmpty_ = L.gt +instance CanCheckEmpty 'IncludeBoundary 'ExcludeBoundary where + checkEmpty = (>=) + checkEmpty_ = L.ge +instance CanCheckEmpty 'ExcludeBoundary 'IncludeBoundary where + checkEmpty = (>=) + checkEmpty_ = L.ge +instance (Bottom, TypeError + ('Text "This function can't be used to check whenter a \ + \range with both boundaries excluded is empty")) => + CanCheckEmpty 'ExcludeBoundary 'ExcludeBoundary where + checkEmpty = no + checkEmpty_ = no + +{- | Assert a range is non-empty, run a failing function passed as the first +argument if it is. Note, however, this function is not suitable for checking +whether a range with both boundaries excluded is empty, and hence will produce a +type error when such a check is attempted. + +>>> let err = push [mt|empty range|] # pair # failWith @(MText, Range Integer) +>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 1) +[0, 1] + +>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 0) +[0, 0] + +>>> pretty $ mkRange_ # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! -1) +*** Exception: Reached FAILWITH instruction with 'Pair "empty range" (Pair 0 -1)' ... +... + +>>> mkRange_ @RangeEE # assertRangeNonEmpty_ err -$ (#min :! 0) ::: (#max :! 1) +... +... error: +... This function can't be used to check whenter a range with both boundaries excluded is empty +... +-} +assertRangeNonEmpty_ + :: ( NiceRange range lower upper a + , CanCheckEmpty lower upper + , NiceComparable a + , Dupable (range a) + ) + => (forall s' any. range a : s' :-> any) + -> range a : s :-> range a : s +assertRangeNonEmpty_ err = dup # isRangeEmpty_ # if_ err nop diff --git a/src/Lorentz/StoreClass.hs b/src/Lorentz/StoreClass.hs --- a/src/Lorentz/StoreClass.hs +++ b/src/Lorentz/StoreClass.hs @@ -17,6 +17,27 @@ We provide the most common building blocks for implementing these instances, see @Implementations@ section. +@OverloadedRecordDot@ is supported for field access, e.g. like this: + +> stSetField this.sField1.ssField1.gField + +(note `this` is mandatory) + +However, there are some kinks. When using Lorentz with @RebindableSyntax@ and +@OverloadedRecordDot@, you'll want to hide @getField@ import from @Lorentz@ or +@Lorentz.ADT@, and instead import @GHC.Records@, otherwise GHC will try to use +@Lorentz.ADT.getField@ when desugaring record dots and produce inscrutable error +messages like this: + +@ +• Expected a type, but + ‘"gField"’ has kind + ‘ghc-prim-0.9.0:GHC.Types.Symbol’ +@ + +If you need to use both @Lorentz.ADT.getField@ and record dots, consider +importing @Lorentz.ADT@ qualified. + -} module Lorentz.StoreClass ( -- * Preliminary @@ -109,6 +130,7 @@ import Data.Kind qualified as Kind +import GHC.Records qualified as GHC import GHC.TypeLits (KnownSymbol, Symbol) import Lorentz.ADT @@ -163,6 +185,14 @@ IsLabel name (x p) where fromLabel = FieldName +instance (KnownSymbol field, y ~ FieldRefObject (SelfRef :-| field), p ~ 'FieldRefTag) + => GHC.HasField field (SelfRef p) (y p) where + getField l = l :-| FieldName + +instance (KnownSymbol field, y ~ FieldRefObject ((l :-| r) :-| field), p ~ 'FieldRefTag) + => GHC.HasField field ((l :-| r) p) (y p) where + getField l = l :-| FieldName + instance KnownSymbol name => KnownFieldRef (name :: Symbol) where type FieldRefObject name = FieldName name mkFieldRef = FieldName @@ -1009,8 +1039,8 @@ -- -- Example: @stToField (#a :-| #b)@ fetches field @b@ in the type under field @a@. -- --- If not favouring this name much, you can try an alias from --- "Lorentz.StoreClass.Extra". +-- If this syntax seems overly verbose, you can try using @OverloadedRecordDot@. +-- See module documentation for comments on that. infixr 8 :-| data (:-|) (l :: k1) (r :: k2) (p :: FieldRefTag) = FieldRef l :-| FieldRef r diff --git a/src/Lorentz/StoreClass/Extra.hs b/src/Lorentz/StoreClass/Extra.hs --- a/src/Lorentz/StoreClass/Extra.hs +++ b/src/Lorentz/StoreClass/Extra.hs @@ -6,6 +6,7 @@ -- This is not part of the umbrella "Lorentz" module, you have to import -- this specially. module Lorentz.StoreClass.Extra + {-# DEPRECATED "Use OverloadedRecordDot instead" #-} ( (.) ) where diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs --- a/src/Lorentz/UParam.hs +++ b/src/Lorentz/UParam.hs @@ -65,6 +65,7 @@ import Morley.AsRPC (HasRPCRepr(..)) import Morley.Michelson.Text import Morley.Michelson.Typed +import Morley.Util.Generic import Morley.Util.Label (Label) import Morley.Util.Markdown import Morley.Util.Type @@ -333,21 +334,38 @@ they come from constructor names. -} --- | Make up 'UParam' from ADT sum. --- --- Entry points template will consist of --- @(constructorName, constructorFieldType)@ pairs. --- Each constructor is expected to have exactly one field. +{- | Make up 'UParam' from ADT sum. + +Entry points template will consist of +@(constructorName, constructorFieldType)@ pairs. +Each constructor is expected to have exactly one field. + +Shows human-readable errors when @up@ is stuck. + +>>> data Foo = Foo () +>>> uparamFromAdt $ Foo () +... +... GHC.Generics.Rep Foo +... is stuck. Likely +... Generic Foo +... instance is missing or out of scope. +... + +>>> data Foo = Foo () deriving Generic +>>> uparamFromAdt $ Foo () +UnsafeUParam (UnsafeMText {unMText = "Foo"},"\ENQ\ETX\v") + +-} uparamFromAdt :: UParamLinearize up => up -> UParam (UParamLinearized up) uparamFromAdt = adtToRec . G.from -- | Constraint required by 'uparamFromAdt'. -type UParamLinearize p = (Generic p, GUParamLinearize (G.Rep p)) +type UParamLinearize p = (NiceGeneric p, GUParamLinearize (GRep p)) -- | Entry points template derived from given ADT sum. -type UParamLinearized p = GUParamLinearized (G.Rep p) +type UParamLinearized p = GUParamLinearized (GRep p) -- | Generic traversal for conversion between ADT sum and 'UParam'. class GUParamLinearize (x :: Type -> Type) where diff --git a/src/Lorentz/Wrappable.hs b/src/Lorentz/Wrappable.hs --- a/src/Lorentz/Wrappable.hs +++ b/src/Lorentz/Wrappable.hs @@ -14,10 +14,35 @@ import Morley.Michelson.Typed (ToT) import Morley.Util.Named --- | Declares that this type is just a wrapper over some other type --- and it can be safely unwrapped to that inner type. +{- | Declares that this type is just a wrapper over some other type and it can +be safely unwrapped to that inner type. + +Inspired by lens @Wrapped@. + +Generic-derivable for newtypes. + +>>> import Lorentz +>>> :{ +newtype Foo = Foo Integer + deriving stock Generic + deriving anyclass (IsoValue, Unwrappable) +:} + +@IsoValue@ instance is mandatory, but 'Generic' isn't: + +>>> import Morley.Michelson.Typed.T +>>> :{ +data Foo = Foo Integer -- --- Inspired by lens @Wrapped@. +instance IsoValue Foo where + type ToT Foo = TInt + toVal (Foo i) = toVal i + fromVal i = Foo $ fromVal i +-- +instance Unwrappable Foo where + type Unwrappabled Foo = Integer +:} +-} class ToT s ~ ToT (Unwrappabled s) => Unwrappable (s :: Type) where -- | The type we unwrap to (inner type of the newtype). --