diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,20 @@ + +1.16.2 +====== +* [!1045](https://gitlab.com/morley-framework/morley/-/merge_requests/1045) + + Add optics: + - `Ixed` and `At` instances for `Value t` and `BigMap k v`. + - `isoValue`. + - prisms for `Expression`. + - lenses for `MichelinePrimAp`. + + Add `SomeAnnotatedValue` and `AnnotatedValue`. + + Add `Lift` instance for `Expression`. +* [!1040](https://gitlab.com/morley-framework/morley/-/merge_requests/1040) + Add missing `FromExpression` conversions + + `Chest` and `ChestKey` cases were missing in `FromExpression` conversions. + 1.16.1 ====== * [!1016](https://gitlab.com/morley-framework/morley/-/merge_requests/1016) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -64,13 +64,13 @@ Morley-the library is available on [Hackage](https://hackage.haskell.org/package/morley). It consists of the following parts: -- The `Morley.Tezos.*` hierarchy ([`Morley.Tezos.Address`](http://hackage.haskell.org/package/morley/docs/Tezos-Address.html), [`Morley.Tezos.Core`](http://hackage.haskell.org/package/morley/docs/Tezos-Core.html), [`Morley.Tezos.Crypto`](http://hackage.haskell.org/package/morley/docs/Tezos-Crypto.html)) is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson. -- [`Morley.Michelson.Untyped`](http://hackage.haskell.org/package/morley/docs/Michelson-Untyped.html) and [`Morley.Michelson.Typed`](http://hackage.haskell.org/package/morley/docs/Michelson-Typed.html) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/michelsonTypes.md). -- [`Morley.Michelson.TypeCheck`](http://hackage.haskell.org/package/morley/docs/Michelson-TypeCheck.html): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyTypechecker.md). -- [`Morley.Michelson.Interpret`](http://hackage.haskell.org/package/morley/docs/Michelson-Interpret.html): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyInterpreter.md). -- [`Morley.Michelson.Macro`](http://hackage.haskell.org/package/morley/docs/Michelson-Macro.html) Types for macros, syntactic sugar, and other extensions that are described in the next chapter. -- [`Morley.Michelson.Parser`](http://hackage.haskell.org/package/morley/docs/Michelson-Parser.html) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT. -- [`Morley.Michelson.Runtime`](http://hackage.haskell.org/package/morley/docs/Michelson-Runtime.html): A high-level interface to Morley functionality, see [morleyRuntime.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyRuntime.md). +- The `Morley.Tezos.*` hierarchy ([`Morley.Tezos.Address`](http://hackage.haskell.org/package/morley/docs/Morley-Tezos-Address.html), [`Morley.Tezos.Core`](http://hackage.haskell.org/package/morley/docs/Morley-Tezos-Core.html), [`Morley.Tezos.Crypto`](http://hackage.haskell.org/package/morley/docs/Morley-Tezos-Crypto.html)) is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson. +- [`Morley.Michelson.Untyped`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Untyped.html) and [`Morley.Michelson.Typed`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Typed.html) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/michelsonTypes.md). +- [`Morley.Michelson.TypeCheck`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-TypeCheck.html): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyTypechecker.md). +- [`Morley.Michelson.Interpret`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Interpret.html): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyInterpreter.md). +- [`Morley.Michelson.Macro`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Macro.html) Types for macros, syntactic sugar, and other extensions that are described in the next chapter. +- [`Morley.Michelson.Parser`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Parser.html) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT. +- [`Morley.Michelson.Runtime`](http://hackage.haskell.org/package/morley/docs/Morley-Michelson-Runtime.html): A high-level interface to Morley functionality, see [morleyRuntime.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyRuntime.md). - The `Morley.Micheline.*` hierarchy ([`Morley.Micheline.Binary`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Binary.html), [`Morley.Micheline.Class`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Class.html), [`Morley.Micheline.Expression`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Expression.html), [`Morley.Micheline.Json`](http://hackage.haskell.org/package/morley/docs/Morley-Micheline-Json.html)) contains the representation of Micheline `Expression`s, conversion to/from Michelson values, diff --git a/morley.cabal b/morley.cabal --- a/morley.cabal +++ b/morley.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: morley -version: 1.16.1 +version: 1.16.2 synopsis: Developer tools for the Michelson Language description: A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category: Language @@ -89,6 +89,7 @@ Morley.Michelson.TypeCheck.Value Morley.Michelson.Typed Morley.Michelson.Typed.Aliases + Morley.Michelson.Typed.AnnotatedValue Morley.Michelson.Typed.Annotation Morley.Michelson.Typed.Arith Morley.Michelson.Typed.Contract diff --git a/src/Morley/Micheline/Class.hs b/src/Morley/Micheline/Class.hs --- a/src/Morley/Micheline/Class.hs +++ b/src/Morley/Micheline/Class.hs @@ -858,6 +858,8 @@ PrimExpr "bls12_381_g2" [] [] -> pure Untyped.TBls12381G2 PrimExpr "timestamp" [] [] -> pure Untyped.TTimestamp PrimExpr "address" [] [] -> pure Untyped.TAddress + PrimExpr "chest" [] [] -> pure Untyped.TChest + PrimExpr "chest_key" [] [] -> pure Untyped.TChestKey PrimExpr "never" [] [] -> pure Untyped.TNever _ -> Left $ FromExpressionError e "Expected a type" where diff --git a/src/Morley/Micheline/Expression.hs b/src/Morley/Micheline/Expression.hs --- a/src/Morley/Micheline/Expression.hs +++ b/src/Morley/Micheline/Expression.hs @@ -4,6 +4,8 @@ -- SPDX-License-Identifier: LicenseRef-MIT-TQ -- SPDX-License-Identifier: LicenseRef-MIT-obsidian-systems +{-# LANGUAGE DeriveLift #-} + -- | Module that defines Expression type, its related types -- and its JSON instance. module Morley.Micheline.Expression @@ -23,12 +25,18 @@ , toAnnSet -- * Prisms + , _ExpressionInt + , _ExpressionString + , _ExpressionBytes + , _ExpressionSeq , _ExpressionPrim , _AnnotationField , _AnnotationVariable , _AnnotationType -- * Lenses + , mpaPrimL + , mpaArgsL , mpaAnnotsL ) where @@ -46,6 +54,7 @@ import qualified Data.Text as T (uncons) import Fmt (Buildable(..), pretty, (+|), (|+)) +import Language.Haskell.TH.Lift (Lift) import Morley.Micheline.Json (StringEncode(StringEncode, unStringEncode)) import qualified Morley.Michelson.Untyped as U import Morley.Michelson.Untyped.Annotation @@ -53,10 +62,11 @@ annPrefix, fullAnnSet, minimizeAnnSet, mkAnnotation) import Morley.Tezos.Crypto (encodeBase58Check) import Morley.Util.ByteString (HexJSONByteString(..)) +import Morley.Util.Lens (postfixLFields) newtype MichelinePrimitive = MichelinePrimitive Text deriving newtype (Eq, Ord, ToJSON, FromJSON) - deriving stock (Show, Data) + deriving stock (Show, Data, Lift) michelsonPrimitive :: Seq Text michelsonPrimitive = Seq.fromList [ @@ -113,7 +123,7 @@ | ExpressionBytes ByteString | ExpressionSeq [Expression] | ExpressionPrim MichelinePrimAp - deriving stock (Eq, Show, Data) + deriving stock (Eq, Show, Data, Lift) pattern PrimExpr :: Text -> [Expression] -> [Annotation] -> Expression pattern PrimExpr primName args anns = @@ -139,13 +149,13 @@ = AnnotationType TypeAnn | AnnotationVariable VarAnn | AnnotationField FieldAnn - deriving stock (Eq, Show, Data) + deriving stock (Eq, Show, Data, Lift) data MichelinePrimAp = MichelinePrimAp { mpaPrim :: MichelinePrimitive , mpaArgs :: [Expression] , mpaAnnots :: [Annotation] - } deriving stock (Eq, Show, Data) + } deriving stock (Eq, Show, Data, Lift) instance FromJSON MichelinePrimAp where parseJSON = withObject "Prim" $ \v -> MichelinePrimAp @@ -246,4 +256,4 @@ makePrisms ''Expression makePrisms ''Annotation -makeLensesFor [("mpaAnnots", "mpaAnnotsL")] ''MichelinePrimAp +makeLensesWith postfixLFields ''MichelinePrimAp diff --git a/src/Morley/Michelson/Typed.hs b/src/Morley/Michelson/Typed.hs --- a/src/Morley/Michelson/Typed.hs +++ b/src/Morley/Michelson/Typed.hs @@ -7,6 +7,7 @@ ) where import Morley.Michelson.Typed.Aliases as Exports +import Morley.Michelson.Typed.AnnotatedValue as Exports (AnnotatedValue(..), SomeAnnotatedValue(..)) import Morley.Michelson.Typed.Annotation as Exports import Morley.Michelson.Typed.Arith as Exports import Morley.Michelson.Typed.Contract as Exports diff --git a/src/Morley/Michelson/Typed/AnnotatedValue.hs b/src/Morley/Michelson/Typed/AnnotatedValue.hs new file mode 100644 --- /dev/null +++ b/src/Morley/Michelson/Typed/AnnotatedValue.hs @@ -0,0 +1,282 @@ +-- SPDX-FileCopyrightText: 2022 Tocqueville Group +-- +-- SPDX-License-Identifier: LicenseRef-MIT-TQ + +module Morley.Michelson.Typed.AnnotatedValue + ( AnnotatedValue (..) + , SomeAnnotatedValue(..) + , getT + -- * Optics + , value + , castTo + , variant + , fields + , field + , nodes + , node + , asList + , asMap + ) where + +import Control.Lens +import qualified Data.Map as Map +import Data.Singletons (SingI, demote) +import Fmt (Buildable(..), (+|), (|+)) + +import Morley.Michelson.Typed.Aliases (Value) +import Morley.Michelson.Typed.Annotation (Notes(..)) +import Morley.Michelson.Typed.Convert () +import Morley.Michelson.Typed.Extract (mkUType) +import Morley.Michelson.Typed.Haskell.Value (IsoValue, ToT, fromVal, toVal) +import Morley.Michelson.Typed.T (T) +import Morley.Michelson.Typed.Value +import Morley.Michelson.Untyped (FieldAnn, noAnn) +import Morley.Util.Sing (eqI) + +-- $setup +-- >>> import qualified Data.Map as Map +-- >>> import Morley.Michelson.Untyped (noAnn, fieldAnnQ) +-- >>> :m +Morley.Michelson.Typed Morley.Michelson.Text Control.Lens Fmt + +data AnnotatedValue v = AnnotatedValue + { avNotes :: Notes (ToT v) + , avValue :: Value (ToT v) + } + deriving stock (Eq, Show) + +instance SingI (ToT v) => Buildable (AnnotatedValue v) where + build (AnnotatedValue n v) = build v |+ " :: " +| build (mkUType n) + +data SomeAnnotatedValue where + SomeAnnotatedValue :: forall t. SingI t => Notes t -> Value t -> SomeAnnotatedValue + +deriving stock instance Show SomeAnnotatedValue + +instance Eq SomeAnnotatedValue where + SomeAnnotatedValue n1 (v1 :: Value t1) == SomeAnnotatedValue n2 (v2 :: Value t2) = + case eqI @t1 @t2 of + Nothing -> False + Just Refl -> n1 == n2 && v1 == v2 + +instance Buildable SomeAnnotatedValue where + build (SomeAnnotatedValue n v) = build v |+ " :: " +| build (mkUType n) + +getT :: SomeAnnotatedValue -> T +getT (SomeAnnotatedValue _ (_ :: Value t)) = demote @t + +---------------------------------------------------------------------------- +-- Optics +---------------------------------------------------------------------------- + +-- | Extract the value out of an annotated value. +value :: IsoValue v => Lens' (AnnotatedValue v) v +value = + lens + do fromVal . avValue + do \av v -> av { avValue = toVal v } + +-- | Attempts to cast to the given type. +castTo :: forall v1 v2. (IsoValue v1, IsoValue v2) => Prism SomeAnnotatedValue SomeAnnotatedValue (AnnotatedValue v1) (AnnotatedValue v2) +castTo = + prism + do \(AnnotatedValue n v) -> SomeAnnotatedValue n v + do \sav@(SomeAnnotatedValue n (v :: Value t)) -> + case eqI @t @(ToT v1) of + Just Refl -> Right $ AnnotatedValue n v + Nothing -> Left sav + +{- | Matches on a (possibly nested) @or@, and focuses the value if its +field annotation is a match. + +Note that field annotations do not have to be unique. +If two @or@ branches have the same field annotation, `variant` will match on either branch. + +>>> :{ +or = Right (Left 3) :: Either Integer (Either Natural Integer) +notes = + NTOr noAnn [fieldAnnQ|first|] noAnn + starNotes + (NTOr noAnn [fieldAnnQ|second|] [fieldAnnQ|third|] starNotes starNotes) +val = SomeAnnotatedValue notes (toVal or) +:} + +>>> val ^? variant [fieldAnnQ|second|] . to pretty +Just "3 :: nat" + +>>> val ^? variant [fieldAnnQ|first|] . to pretty +Nothing +-} +variant :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue +variant fieldAnn (handler :: SomeAnnotatedValue -> (f SomeAnnotatedValue)) = \case + SomeAnnotatedValue n0 v0 -> go noAnn (n0, v0) + where + go :: FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue + go currentFieldAnn (n, v) + -- If this node does not have a field ann, then recurse. + | currentFieldAnn == noAnn = + case (n, v) of + (NTOr ta fal far nl nr, VOr (Left vl)) -> do + go fal (nl, vl) <&> \(SomeAnnotatedValue nl' vl') -> + SomeAnnotatedValue (NTOr ta fal far nl' nr) (VOr (Left vl')) + (NTOr ta fal far nl nr, VOr (Right vr)) -> do + go far (nr, vr) <&> \(SomeAnnotatedValue nr' vr') -> + SomeAnnotatedValue (NTOr ta fal far nl nr') (VOr (Right vr')) + _ -> + -- We've reached a leaf. + pure $ withValueTypeSanity v $ SomeAnnotatedValue n v + + -- We've encountered a node labelled with a field ann, and it's a match. + | currentFieldAnn == fieldAnn = handler $ withValueTypeSanity v $ SomeAnnotatedValue n v + -- We've encountered a node labelled with a field ann, but it's not a match. + | otherwise = pure $ withValueTypeSanity v $ SomeAnnotatedValue n v + +{- | Traverses all nodes in a tree of pairs that have a field annotation. +The elements are indexed by their field annotations. + +Note that sub-trees are not inspected. +For example, for this type: + +> pair +> (int %storageField1) +> (pair %storageField2 +> (int %nestedField1) +> (string %nestedField2) +> ) + +'fields' will: + +* ignore the top-level node, because it does not have a field annotation. +* traverse the @storageField1@ and @storageField2@ fields. +* ignore @nestedField1@ and @nestedField2@, because they're in a sub-tree of a traversed node. + +Note that field annotations do not have to be unique. +If two fields have the same field annotation, both will be indexed/traversed. + +>>> :{ +pair = (1, 2, 3) :: (Integer, Natural, Integer) +notes = + NTPair noAnn [fieldAnnQ|first|] noAnn noAnn noAnn + starNotes + (NTPair noAnn [fieldAnnQ|second|] [fieldAnnQ|third|] noAnn noAnn starNotes starNotes) +val = SomeAnnotatedValue notes (toVal pair) +:} + +>>> mapM_ print $ val ^@.. fields . to pretty +(%first,"1 :: int") +(%second,"2 :: nat") +(%third,"3 :: int") +-} +fields :: IndexedTraversal' FieldAnn SomeAnnotatedValue SomeAnnotatedValue +fields (handler :: p SomeAnnotatedValue (f SomeAnnotatedValue)) = \case + SomeAnnotatedValue n0 v0 -> go noAnn (n0, v0) + where + go :: FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue + go currentFieldAnn (n, v) + | currentFieldAnn == noAnn = + case (n, v) of + (NTPair ta fal far val var nl nr, VPair (vl, vr)) -> do + savL <- go fal (nl, vl) + savR <- go far (nr, vr) + pure $ + case (savL, savR) of + (SomeAnnotatedValue nl' vl', SomeAnnotatedValue nr' vr') -> + SomeAnnotatedValue (NTPair ta fal far val var nl' nr') (VPair (vl', vr')) + _ -> + -- We've reached a leaf. + pure $ withValueTypeSanity v $ SomeAnnotatedValue n v + | otherwise = + indexed handler currentFieldAnn $ withValueTypeSanity v $ SomeAnnotatedValue n v + +{- | Looks up a member of a tree of pairs by its field annotation. +Note that sub-trees of nodes with field annotations are not inspected. + +Note that field annotations do not have to be unique. +If two fields have the same field annotation, both will be indexed/traversed. + +>>> :{ +pair = (1, 2, 3) :: (Integer, Natural, Integer) +notes = + NTPair noAnn [fieldAnnQ|first|] noAnn noAnn noAnn + starNotes + (NTPair noAnn [fieldAnnQ|second|] [fieldAnnQ|third|] noAnn noAnn starNotes starNotes) +val = SomeAnnotatedValue notes (toVal pair) +:} + +>>> val ^? field [fieldAnnQ|second|] . castTo @Natural . value +Just 2 +-} +field :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue +field fieldAnn = fields . index fieldAnn + +{- | Lists all nodes in a tree of pairs. +The elements are indexed by their field annotations. + +Note that field annotations do not have to be unique. +If two fields have the same field annotation, both will be indexed. + +>>> :{ +pair = (1, 2, 3) :: (Integer, Natural, Integer) +notes = + NTPair noAnn [fieldAnnQ|first|] noAnn noAnn noAnn + starNotes + (NTPair noAnn [fieldAnnQ|second|] [fieldAnnQ|third|] noAnn noAnn starNotes starNotes) +val = SomeAnnotatedValue notes (toVal pair) +:} + +>>> mapM_ print $ val ^@.. nodes . to pretty +(%first,"1 :: int") +(%,"Pair 2 3 :: pair (nat %second) (int %third)") +(%second,"2 :: nat") +(%third,"3 :: int") +-} +nodes :: IndexedFold FieldAnn SomeAnnotatedValue SomeAnnotatedValue +nodes = ifolding $ \case + SomeAnnotatedValue n0 v0 -> go (n0, v0) + where + go :: (Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)] + go (n, v) = case (n, v) of + (NTPair _ fal far _ _ nl nr, VPair (vl, vr)) -> + (fal, withValueTypeSanity vl $ SomeAnnotatedValue nl vl) : + (far, withValueTypeSanity vr $ SomeAnnotatedValue nr vr) : + go (nl, vl) <> + go (nr, vr) + _ -> [] + +-- | Looks up nodes in a tree of pairs with the given field annotation. +node :: FieldAnn -> Fold SomeAnnotatedValue SomeAnnotatedValue +node fieldAnn = nodes . index fieldAnn + +-- | Casts a 'SomeAnnotatedValue' to a list. +-- +-- >>> list = [ [mt|hello|], [mt|world|] ] +-- >>> val = SomeAnnotatedValue starNotes (toVal list) +-- >>> val ^? asList . ix 1 . castTo @MText . value . to pretty +-- Just "world" +asList :: Fold SomeAnnotatedValue [SomeAnnotatedValue] +asList = folding @Maybe \case + SomeAnnotatedValue (NTList _ xNotes) (VList xs) -> + Just $ xs <&> \x -> SomeAnnotatedValue xNotes x + _ -> Nothing + +-- | Casts a 'SomeAnnotatedValue' to a map. +-- +-- >>> map = Map.fromList @Integer @Bool [(10, False), (20, True)] +-- >>> val = SomeAnnotatedValue starNotes (toVal map) +-- >>> val ^? asMap @Integer . ix 20 . castTo @Bool . value +-- Just True +asMap :: forall key. (IsoValue key, Ord key) => Fold SomeAnnotatedValue (Map key SomeAnnotatedValue) +asMap = folding @Maybe \case + SomeAnnotatedValue (NTMap _ _ vNotes) (VMap vmap) -> convert vNotes vmap + SomeAnnotatedValue (NTBigMap _ _ vNotes) (VBigMap _ vmap) -> convert vNotes vmap + _ -> Nothing + where + convert + :: forall k v. (SingI k, SingI v) + => Notes v + -> Map (Value k) (Value v) + -> Maybe (Map key SomeAnnotatedValue) + convert vNotes vmap = + eqI @(ToT key) @k <&> \Refl -> + vmap + & Map.mapKeys (\k -> fromVal @key k) + <&> \v -> SomeAnnotatedValue vNotes v diff --git a/src/Morley/Michelson/Typed/Haskell/Value.hs b/src/Morley/Michelson/Typed/Haskell/Value.hs --- a/src/Morley/Michelson/Typed/Haskell/Value.hs +++ b/src/Morley/Michelson/Typed/Haskell/Value.hs @@ -8,6 +8,7 @@ module Morley.Michelson.Typed.Haskell.Value ( -- * Value conversions IsoValue (..) + , isoValue , KnownIsoT , GIsoValue (GValueType) , ToT' @@ -38,6 +39,7 @@ , totsAppendLemma ) where +import Control.Lens import Data.Constraint (Dict(..)) import Data.Data (Data) import Data.Default (Default(..)) @@ -98,6 +100,10 @@ ToT' (t :: T) = t ToT' (t :: Type) = ToT t +-- | An optic witnessing the isomorphism between a michelson type and a haskell type. +isoValue :: (IsoValue a, IsoValue b) => Iso (Value (ToT a)) (Value (ToT b)) a b +isoValue = iso fromVal toVal + -- Instances ---------------------------------------------------------------------------- @@ -325,6 +331,12 @@ } deriving stock (Show, Generic, Data) deriving anyclass (Default, Container) + +type instance Index (BigMap k _) = k +type instance IxValue (BigMap _ v) = v +instance Ord k => Ixed (BigMap k v) +instance Ord k => At (BigMap k v) where + at key handler (BigMap bmId bmMap) = BigMap bmId <$> at key handler bmMap class ToBigMap m where type ToBigMapKey m diff --git a/src/Morley/Michelson/Typed/Value.hs b/src/Morley/Michelson/Typed/Value.hs --- a/src/Morley/Michelson/Typed/Value.hs +++ b/src/Morley/Michelson/Typed/Value.hs @@ -29,6 +29,7 @@ , eqValueExt ) where +import Control.Lens (At(..), Index, IxValue, Ixed(..)) import Data.Constraint (Dict(..), (\\)) import Data.Singletons (Sing) import Data.Type.Bool (type (&&)) @@ -460,3 +461,26 @@ $(deriveGADTNFData ''Operation') $(deriveGADTNFData ''Value') + +type instance Index (Value' _ ('TList _)) = Int +type instance IxValue (Value' instr ('TList elem)) = Value' instr elem +instance Ixed (Value' instr ('TList elem)) where + ix idx handler (VList xs) = VList <$> ix idx handler xs + +type instance Index (Value' instr ('TMap k _)) = Value' instr k +type instance IxValue (Value' instr ('TMap _ v)) = Value' instr v +instance Ixed (Value' instr ('TMap k v)) +instance At (Value' instr ('TMap k v)) where + at key handler (VMap vmap) = VMap <$> at key handler vmap + +type instance Index (Value' instr ('TBigMap k _)) = Value' instr k +type instance IxValue (Value' instr ('TBigMap _ v)) = Value' instr v +instance Ixed (Value' instr ('TBigMap k v)) +instance At (Value' instr ('TBigMap k v)) where + at key handler (VBigMap bmid bmap) = VBigMap bmid <$> at key handler bmap + +type instance Index (Value' instr ('TSet a)) = Value' instr a +type instance IxValue (Value' _ ('TSet _)) = () +instance Ixed (Value' instr ('TSet a)) +instance At (Value' instr ('TSet a)) where + at key handler (VSet vset) = VSet<$> at key handler vset