module Morley.Michelson.Typed.AnnotatedValue
( AnnotatedValue (..)
, SomeAnnotatedValue(..)
, getT
, value
, castTo
, variant
, fields
, field
, nodes
, node
, asList
, asMap
) where
import Control.Lens
(Fold, IndexedFold, IndexedTraversal', Prism, folding, ifolding, index, indexed, lens, prism,
(:~:)(Refl))
import Data.Map qualified as Map
import Data.Singletons (SingI, demote)
import Fmt (Buildable(..), (+|), (|+))
import Morley.Michelson.Typed.Aliases (Value)
import Morley.Michelson.Typed.Annotation (Notes(..), mkUType)
import Morley.Michelson.Typed.Convert ()
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)
data AnnotatedValue v = AnnotatedValue
{ forall v. AnnotatedValue v -> Notes (ToT v)
avNotes :: Notes (ToT v)
, forall v. AnnotatedValue v -> Value (ToT v)
avValue :: Value (ToT v)
}
deriving stock (AnnotatedValue v -> AnnotatedValue v -> Bool
(AnnotatedValue v -> AnnotatedValue v -> Bool)
-> (AnnotatedValue v -> AnnotatedValue v -> Bool)
-> Eq (AnnotatedValue v)
forall v. AnnotatedValue v -> AnnotatedValue v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AnnotatedValue v -> AnnotatedValue v -> Bool
$c/= :: forall v. AnnotatedValue v -> AnnotatedValue v -> Bool
== :: AnnotatedValue v -> AnnotatedValue v -> Bool
$c== :: forall v. AnnotatedValue v -> AnnotatedValue v -> Bool
Eq, Int -> AnnotatedValue v -> ShowS
[AnnotatedValue v] -> ShowS
AnnotatedValue v -> String
(Int -> AnnotatedValue v -> ShowS)
-> (AnnotatedValue v -> String)
-> ([AnnotatedValue v] -> ShowS)
-> Show (AnnotatedValue v)
forall v. Int -> AnnotatedValue v -> ShowS
forall v. [AnnotatedValue v] -> ShowS
forall v. AnnotatedValue v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AnnotatedValue v] -> ShowS
$cshowList :: forall v. [AnnotatedValue v] -> ShowS
show :: AnnotatedValue v -> String
$cshow :: forall v. AnnotatedValue v -> String
showsPrec :: Int -> AnnotatedValue v -> ShowS
$cshowsPrec :: forall v. Int -> AnnotatedValue v -> ShowS
Show)
instance Buildable (AnnotatedValue v) where
build :: AnnotatedValue v -> Builder
build (AnnotatedValue Notes (ToT v)
n Value (ToT v)
v) = Value (ToT v) -> Builder
forall p. Buildable p => p -> Builder
build Value (ToT v)
v Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" :: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Ty -> Builder
forall p. Buildable p => p -> Builder
build (Notes (ToT v) -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes (ToT v)
n)
data SomeAnnotatedValue where
SomeAnnotatedValue :: forall t. SingI t => Notes t -> Value t -> SomeAnnotatedValue
deriving stock instance Show SomeAnnotatedValue
instance Eq SomeAnnotatedValue where
SomeAnnotatedValue Notes t
n1 (Value t
v1 :: Value t1) == :: SomeAnnotatedValue -> SomeAnnotatedValue -> Bool
== SomeAnnotatedValue Notes t
n2 (Value t
v2 :: Value t2) =
case forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @t1 @t2 of
Maybe (t :~: t)
Nothing -> Bool
False
Just t :~: t
Refl -> Notes t
n1 Notes t -> Notes t -> Bool
forall a. Eq a => a -> a -> Bool
== Notes t
Notes t
n2 Bool -> Bool -> Bool
forall a. Boolean a => a -> a -> a
&& Value t
v1 Value t -> Value t -> Bool
forall a. Eq a => a -> a -> Bool
== Value t
Value t
v2
instance Buildable SomeAnnotatedValue where
build :: SomeAnnotatedValue -> Builder
build (SomeAnnotatedValue Notes t
n Value t
v) = Value t -> Builder
forall p. Buildable p => p -> Builder
build Value t
v Builder -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" :: " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| Ty -> Builder
forall p. Buildable p => p -> Builder
build (Notes t -> Ty
forall (x :: T). Notes x -> Ty
mkUType Notes t
n)
getT :: SomeAnnotatedValue -> T
getT :: SomeAnnotatedValue -> T
getT (SomeAnnotatedValue Notes t
_ (Value t
_ :: Value t)) = forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @t
value :: IsoValue v => Lens' (AnnotatedValue v) v
value :: forall v. IsoValue v => Lens' (AnnotatedValue v) v
value =
(AnnotatedValue v -> v)
-> (AnnotatedValue v -> v -> AnnotatedValue v)
-> Lens (AnnotatedValue v) (AnnotatedValue v) v v
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
do Value' Instr (ToT v) -> v
forall a. IsoValue a => Value (ToT a) -> a
fromVal (Value' Instr (ToT v) -> v)
-> (AnnotatedValue v -> Value' Instr (ToT v))
-> AnnotatedValue v
-> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnnotatedValue v -> Value' Instr (ToT v)
forall v. AnnotatedValue v -> Value (ToT v)
avValue
do \AnnotatedValue v
av v
v -> AnnotatedValue v
av { avValue :: Value' Instr (ToT v)
avValue = v -> Value' Instr (ToT v)
forall a. IsoValue a => a -> Value (ToT a)
toVal v
v }
castTo
:: forall v1 v2. (IsoValue v1, IsoValue v2)
=> Prism SomeAnnotatedValue SomeAnnotatedValue (AnnotatedValue v1) (AnnotatedValue v2)
castTo :: forall v1 v2.
(IsoValue v1, IsoValue v2) =>
Prism
SomeAnnotatedValue
SomeAnnotatedValue
(AnnotatedValue v1)
(AnnotatedValue v2)
castTo =
(AnnotatedValue v2 -> SomeAnnotatedValue)
-> (SomeAnnotatedValue
-> Either SomeAnnotatedValue (AnnotatedValue v1))
-> Prism
SomeAnnotatedValue
SomeAnnotatedValue
(AnnotatedValue v1)
(AnnotatedValue v2)
forall b t s a. (b -> t) -> (s -> Either t a) -> Prism s t a b
prism
do \(AnnotatedValue Notes (ToT v2)
n Value (ToT v2)
v) -> Notes (ToT v2) -> Value (ToT v2) -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes (ToT v2)
n Value (ToT v2)
v
do \sav :: SomeAnnotatedValue
sav@(SomeAnnotatedValue Notes t
n (Value t
v :: Value t)) ->
case forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @t @(ToT v1) of
Just t :~: ToT v1
Refl -> AnnotatedValue v1 -> Either SomeAnnotatedValue (AnnotatedValue v1)
forall a b. b -> Either a b
Right (AnnotatedValue v1
-> Either SomeAnnotatedValue (AnnotatedValue v1))
-> AnnotatedValue v1
-> Either SomeAnnotatedValue (AnnotatedValue v1)
forall a b. (a -> b) -> a -> b
$ Notes (ToT v1) -> Value (ToT v1) -> AnnotatedValue v1
forall v. Notes (ToT v) -> Value (ToT v) -> AnnotatedValue v
AnnotatedValue Notes t
Notes (ToT v1)
n Value t
Value (ToT v1)
v
Maybe (t :~: ToT v1)
Nothing -> SomeAnnotatedValue -> Either SomeAnnotatedValue (AnnotatedValue v1)
forall a b. a -> Either a b
Left SomeAnnotatedValue
sav
variant :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue
variant :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue
variant FieldAnn
fieldAnn (SomeAnnotatedValue -> f SomeAnnotatedValue
handler :: SomeAnnotatedValue -> (f SomeAnnotatedValue)) = \case
SomeAnnotatedValue Notes t
n0 Value t
v0 -> FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
forall {k} (a :: k). Annotation a
noAnn (Notes t
n0, Value t
v0)
where
go :: FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go :: forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
currentFieldAnn (Notes t
n, Value t
v)
| FieldAnn
currentFieldAnn FieldAnn -> FieldAnn -> Bool
forall a. Eq a => a -> a -> Bool
== FieldAnn
forall {k} (a :: k). Annotation a
noAnn =
case (Notes t
n, Value t
v) of
(NTOr TypeAnn
ta FieldAnn
fal FieldAnn
far Notes p
nl Notes q
nr, VOr (Left Value' Instr l
vl)) -> do
FieldAnn -> (Notes p, Value p) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
fal (Notes p
nl, Value p
Value' Instr l
vl) f SomeAnnotatedValue
-> (SomeAnnotatedValue -> SomeAnnotatedValue)
-> f SomeAnnotatedValue
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(SomeAnnotatedValue Notes t
nl' Value t
vl') ->
Notes ('TOr t q) -> Value ('TOr t q) -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue (TypeAnn
-> FieldAnn -> FieldAnn -> Notes t -> Notes q -> Notes ('TOr t q)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
ta FieldAnn
fal FieldAnn
far Notes t
nl' Notes q
nr) (Either (Value t) (Value' Instr q) -> Value ('TOr t q)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value t -> Either (Value t) (Value' Instr q)
forall a b. a -> Either a b
Left Value t
vl'))
(NTOr TypeAnn
ta FieldAnn
fal FieldAnn
far Notes p
nl Notes q
nr, VOr (Right Value' Instr r
vr)) -> do
FieldAnn -> (Notes q, Value q) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
far (Notes q
nr, Value q
Value' Instr r
vr) f SomeAnnotatedValue
-> (SomeAnnotatedValue -> SomeAnnotatedValue)
-> f SomeAnnotatedValue
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(SomeAnnotatedValue Notes t
nr' Value t
vr') ->
Notes ('TOr p t) -> Value ('TOr p t) -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue (TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes t -> Notes ('TOr p t)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes p -> Notes q -> Notes ('TOr p q)
NTOr TypeAnn
ta FieldAnn
fal FieldAnn
far Notes p
nl Notes t
nr') (Either (Value' Instr p) (Value t) -> Value ('TOr p t)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(SingI l, SingI r) =>
Either (Value' instr l) (Value' instr r) -> Value' instr ('TOr l r)
VOr (Value t -> Either (Value' Instr p) (Value t)
forall a b. b -> Either a b
Right Value t
vr'))
(Notes t, Value t)
_ ->
SomeAnnotatedValue -> f SomeAnnotatedValue
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Value t -> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value t
v ((SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
n Value t
v
| FieldAnn
currentFieldAnn FieldAnn -> FieldAnn -> Bool
forall a. Eq a => a -> a -> Bool
== FieldAnn
fieldAnn = SomeAnnotatedValue -> f SomeAnnotatedValue
handler (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Value t -> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value t
v ((SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
n Value t
v
| Bool
otherwise = SomeAnnotatedValue -> f SomeAnnotatedValue
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Value t -> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value t
v ((SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
n Value t
v
fields :: IndexedTraversal' FieldAnn SomeAnnotatedValue SomeAnnotatedValue
fields :: IndexedTraversal' FieldAnn SomeAnnotatedValue SomeAnnotatedValue
fields (p SomeAnnotatedValue (f SomeAnnotatedValue)
handler :: p SomeAnnotatedValue (f SomeAnnotatedValue)) = \case
SomeAnnotatedValue Notes t
n0 Value t
v0 -> FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
forall {k} (a :: k). Annotation a
noAnn (Notes t
n0, Value t
v0)
where
go :: FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go :: forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
currentFieldAnn (Notes t
n, Value t
v)
| FieldAnn
currentFieldAnn FieldAnn -> FieldAnn -> Bool
forall a. Eq a => a -> a -> Bool
== FieldAnn
forall {k} (a :: k). Annotation a
noAnn =
case (Notes t
n, Value t
v) of
(NTPair TypeAnn
ta FieldAnn
fal FieldAnn
far VarAnn
val VarAnn
var Notes p
nl Notes q
nr, VPair (Value' Instr l
vl, Value' Instr r
vr)) -> do
SomeAnnotatedValue
savL <- FieldAnn -> (Notes p, Value p) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
fal (Notes p
nl, Value p
Value' Instr l
vl)
SomeAnnotatedValue
savR <- FieldAnn -> (Notes q, Value q) -> f SomeAnnotatedValue
forall (t :: T).
FieldAnn -> (Notes t, Value t) -> f SomeAnnotatedValue
go FieldAnn
far (Notes q
nr, Value q
Value' Instr r
vr)
pure $
case (SomeAnnotatedValue
savL, SomeAnnotatedValue
savR) of
(SomeAnnotatedValue Notes t
nl' Value t
vl', SomeAnnotatedValue Notes t
nr' Value t
vr') ->
Notes ('TPair t t) -> Value ('TPair t t) -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue (TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes t
-> Notes t
-> Notes ('TPair t t)
forall (p :: T) (q :: T).
TypeAnn
-> FieldAnn
-> FieldAnn
-> VarAnn
-> VarAnn
-> Notes p
-> Notes q
-> Notes ('TPair p q)
NTPair TypeAnn
ta FieldAnn
fal FieldAnn
far VarAnn
val VarAnn
var Notes t
nl' Notes t
nr') ((Value t, Value t) -> Value ('TPair t t)
forall (l :: T) (r :: T) (instr :: [T] -> [T] -> *).
(Value' instr l, Value' instr r) -> Value' instr ('TPair l r)
VPair (Value t
vl', Value t
vr'))
(Notes t, Value t)
_ ->
SomeAnnotatedValue -> f SomeAnnotatedValue
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Value t -> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value t
v ((SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
n Value t
v
| Bool
otherwise =
p SomeAnnotatedValue (f SomeAnnotatedValue)
-> FieldAnn -> SomeAnnotatedValue -> f SomeAnnotatedValue
forall i (p :: * -> * -> *) a b.
Indexable i p =>
p a b -> i -> a -> b
indexed p SomeAnnotatedValue (f SomeAnnotatedValue)
handler FieldAnn
currentFieldAnn (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Value t -> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value t
v ((SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI t => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
n Value t
v
field :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue
field :: FieldAnn -> Traversal' SomeAnnotatedValue SomeAnnotatedValue
field FieldAnn
fieldAnn = Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
IndexedTraversal' FieldAnn SomeAnnotatedValue SomeAnnotatedValue
fields (Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue)
-> ((SomeAnnotatedValue -> f SomeAnnotatedValue)
-> Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue))
-> (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue
-> f SomeAnnotatedValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldAnn
-> (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
forall i (p :: * -> * -> *) (f :: * -> *) a.
(Indexable i p, Eq i, Applicative f) =>
i -> Optical' p (Indexed i) f a a
index FieldAnn
fieldAnn
nodes :: IndexedFold FieldAnn SomeAnnotatedValue SomeAnnotatedValue
nodes :: IndexedFold FieldAnn SomeAnnotatedValue SomeAnnotatedValue
nodes = (SomeAnnotatedValue -> [(FieldAnn, SomeAnnotatedValue)])
-> Over
p
f
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue
forall (f :: * -> *) i (p :: * -> * -> *) (g :: * -> *) s a t b.
(Foldable f, Indexable i p, Contravariant g, Applicative g) =>
(s -> f (i, a)) -> Over p g s t a b
ifolding ((SomeAnnotatedValue -> [(FieldAnn, SomeAnnotatedValue)])
-> Over
p
f
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue)
-> (SomeAnnotatedValue -> [(FieldAnn, SomeAnnotatedValue)])
-> Over
p
f
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue
SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ \case
SomeAnnotatedValue Notes t
n0 Value t
v0 -> (Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
forall (t :: T).
(Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
go (Notes t
n0, Value t
v0)
where
go :: (Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
go :: forall (t :: T).
(Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
go (Notes t
n, Value t
v) = case (Notes t
n, Value t
v) of
(NTPair TypeAnn
_ FieldAnn
fal FieldAnn
far VarAnn
_ VarAnn
_ Notes p
nl Notes q
nr, VPair (Value' Instr l
vl, Value' Instr r
vr)) ->
(FieldAnn
fal, Value' Instr l
-> (SingI l => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr l
vl ((SingI l => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI l => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes p -> Value p -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes p
nl Value p
Value' Instr l
vl) (FieldAnn, SomeAnnotatedValue)
-> [(FieldAnn, SomeAnnotatedValue)]
-> [(FieldAnn, SomeAnnotatedValue)]
forall a. a -> [a] -> [a]
:
(FieldAnn
far, Value' Instr r
-> (SingI r => SomeAnnotatedValue) -> SomeAnnotatedValue
forall (instr :: [T] -> [T] -> *) (t :: T) a.
Value' instr t -> (SingI t => a) -> a
withValueTypeSanity Value' Instr r
vr ((SingI r => SomeAnnotatedValue) -> SomeAnnotatedValue)
-> (SingI r => SomeAnnotatedValue) -> SomeAnnotatedValue
forall a b. (a -> b) -> a -> b
$ Notes q -> Value q -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes q
nr Value q
Value' Instr r
vr) (FieldAnn, SomeAnnotatedValue)
-> [(FieldAnn, SomeAnnotatedValue)]
-> [(FieldAnn, SomeAnnotatedValue)]
forall a. a -> [a] -> [a]
:
(Notes p, Value p) -> [(FieldAnn, SomeAnnotatedValue)]
forall (t :: T).
(Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
go (Notes p
nl, Value p
Value' Instr l
vl) [(FieldAnn, SomeAnnotatedValue)]
-> [(FieldAnn, SomeAnnotatedValue)]
-> [(FieldAnn, SomeAnnotatedValue)]
forall a. Semigroup a => a -> a -> a
<>
(Notes q, Value q) -> [(FieldAnn, SomeAnnotatedValue)]
forall (t :: T).
(Notes t, Value t) -> [(FieldAnn, SomeAnnotatedValue)]
go (Notes q
nr, Value q
Value' Instr r
vr)
(Notes t, Value t)
_ -> []
node :: FieldAnn -> Fold SomeAnnotatedValue SomeAnnotatedValue
node :: FieldAnn -> Fold SomeAnnotatedValue SomeAnnotatedValue
node FieldAnn
fieldAnn = Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
IndexedFold FieldAnn SomeAnnotatedValue SomeAnnotatedValue
nodes (Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue)
-> ((SomeAnnotatedValue -> f SomeAnnotatedValue)
-> Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue))
-> (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> SomeAnnotatedValue
-> f SomeAnnotatedValue
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldAnn
-> (SomeAnnotatedValue -> f SomeAnnotatedValue)
-> Indexed FieldAnn SomeAnnotatedValue (f SomeAnnotatedValue)
forall i (p :: * -> * -> *) (f :: * -> *) a.
(Indexable i p, Eq i, Applicative f) =>
i -> Optical' p (Indexed i) f a a
index FieldAnn
fieldAnn
asList :: Fold SomeAnnotatedValue [SomeAnnotatedValue]
asList :: Fold SomeAnnotatedValue [SomeAnnotatedValue]
asList = forall (f :: * -> *) s a. Foldable f => (s -> f a) -> Fold s a
folding @Maybe \case
SomeAnnotatedValue (NTList TypeAnn
_ Notes t1
xNotes) (VList [Value' Instr t1]
xs) ->
[SomeAnnotatedValue] -> Maybe [SomeAnnotatedValue]
forall a. a -> Maybe a
Just ([SomeAnnotatedValue] -> Maybe [SomeAnnotatedValue])
-> [SomeAnnotatedValue] -> Maybe [SomeAnnotatedValue]
forall a b. (a -> b) -> a -> b
$ [Value' Instr t1]
xs [Value' Instr t1]
-> (Value' Instr t1 -> SomeAnnotatedValue) -> [SomeAnnotatedValue]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Value' Instr t1
x -> Notes t1 -> Value t1 -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t1
xNotes Value t1
Value' Instr t1
x
SomeAnnotatedValue
_ -> Maybe [SomeAnnotatedValue]
forall a. Maybe a
Nothing
asMap
:: forall key. (IsoValue key, Ord key)
=> Fold SomeAnnotatedValue (Map key SomeAnnotatedValue)
asMap :: forall key.
(IsoValue key, Ord key) =>
Fold SomeAnnotatedValue (Map key SomeAnnotatedValue)
asMap = forall (f :: * -> *) s a. Foldable f => (s -> f a) -> Fold s a
folding @Maybe \case
SomeAnnotatedValue (NTMap TypeAnn
_ Notes k
_ Notes v
vNotes) (VMap Map (Value' Instr k) (Value' Instr v)
vmap) -> Notes v
-> Map (Value' Instr k) (Value v)
-> Maybe (Map key SomeAnnotatedValue)
forall (k :: T) (v :: T).
(SingI k, SingI v) =>
Notes v
-> Map (Value k) (Value v) -> Maybe (Map key SomeAnnotatedValue)
convert Notes v
vNotes Map (Value' Instr k) (Value v)
Map (Value' Instr k) (Value' Instr v)
vmap
SomeAnnotatedValue (NTBigMap TypeAnn
_ Notes k
_ Notes v
vNotes) (VBigMap Maybe Natural
_ Map (Value' Instr k) (Value' Instr v)
vmap) -> Notes v
-> Map (Value' Instr k) (Value v)
-> Maybe (Map key SomeAnnotatedValue)
forall (k :: T) (v :: T).
(SingI k, SingI v) =>
Notes v
-> Map (Value k) (Value v) -> Maybe (Map key SomeAnnotatedValue)
convert Notes v
vNotes Map (Value' Instr k) (Value v)
Map (Value' Instr k) (Value' Instr v)
vmap
SomeAnnotatedValue
_ -> Maybe (Map key SomeAnnotatedValue)
forall a. Maybe a
Nothing
where
convert
:: forall k v. (SingI k, SingI v)
=> Notes v
-> Map (Value k) (Value v)
-> Maybe (Map key SomeAnnotatedValue)
convert :: forall (k :: T) (v :: T).
(SingI k, SingI v) =>
Notes v
-> Map (Value k) (Value v) -> Maybe (Map key SomeAnnotatedValue)
convert Notes v
vNotes Map (Value k) (Value v)
vmap =
forall {k} (a :: k) (b :: k).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
forall (a :: T) (b :: T).
(SingI a, SingI b, TestEquality Sing) =>
Maybe (a :~: b)
eqI @(ToT key) @k Maybe (ToT key :~: k)
-> ((ToT key :~: k) -> Map key SomeAnnotatedValue)
-> Maybe (Map key SomeAnnotatedValue)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ToT key :~: k
Refl ->
Map (Value k) (Value v)
vmap
Map (Value k) (Value v)
-> (Map (Value k) (Value v) -> Map key (Value v))
-> Map key (Value v)
forall a b. a -> (a -> b) -> b
& (Value k -> key) -> Map (Value k) (Value v) -> Map key (Value v)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\Value k
k -> forall a. IsoValue a => Value (ToT a) -> a
fromVal @key Value k
Value (ToT key)
k)
Map key (Value v)
-> (Value v -> SomeAnnotatedValue) -> Map key SomeAnnotatedValue
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Value v
v -> Notes v -> Value v -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes v
vNotes Value v
v