module Morley.Michelson.Typed.AnnotatedValue
( AnnotatedValue (..)
, SomeAnnotatedValue(..)
, getT
, 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)
data AnnotatedValue v = AnnotatedValue
{ AnnotatedValue v -> Notes (ToT v)
avNotes :: Notes (ToT 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 SingI (ToT v) => 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). SingI x => 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 (SingI t, SingI t, TestEquality Sing) => Maybe (t :~: t)
forall k (a :: k) (b :: k).
(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). SingI x => Notes x -> Ty
mkUType Notes t
n)
getT :: SomeAnnotatedValue -> T
getT :: SomeAnnotatedValue -> T
getT (SomeAnnotatedValue Notes t
_ (Value t
_ :: Value t)) = (SingKind T, SingI t) => Demote T
forall k (a :: k). (SingKind k, SingI a) => Demote k
demote @t
value :: IsoValue v => Lens' (AnnotatedValue v) v
value :: Lens' (AnnotatedValue v) v
value =
(AnnotatedValue v -> v)
-> (AnnotatedValue v -> v -> AnnotatedValue v)
-> Lens' (AnnotatedValue 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 :: 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 (SingI t, SingI (ToT v1), TestEquality Sing) =>
Maybe (t :~: ToT v1)
forall k (a :: k) (b :: k).
(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 :: 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 (q :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes q -> Notes q -> Notes ('TOr q 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 (q :: T) (q :: T).
TypeAnn
-> FieldAnn -> FieldAnn -> Notes q -> Notes q -> Notes ('TOr q 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 :: p SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f 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 :: 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 :: p SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue -> f SomeAnnotatedValue
nodes = (SomeAnnotatedValue -> [(FieldAnn, SomeAnnotatedValue)])
-> p SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue
-> f 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)])
-> p SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue
-> f SomeAnnotatedValue)
-> (SomeAnnotatedValue -> [(FieldAnn, SomeAnnotatedValue)])
-> p SomeAnnotatedValue (f SomeAnnotatedValue)
-> SomeAnnotatedValue
-> f 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 :: (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 :: ([SomeAnnotatedValue] -> f [SomeAnnotatedValue])
-> SomeAnnotatedValue -> f SomeAnnotatedValue
asList = (SomeAnnotatedValue -> Maybe [SomeAnnotatedValue])
-> Fold SomeAnnotatedValue [SomeAnnotatedValue]
forall (f :: * -> *) s a. Foldable f => (s -> f a) -> Fold s a
folding @Maybe \case
SomeAnnotatedValue (NTList TypeAnn
_ Notes t
xNotes) (VList [Value' Instr t]
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 t]
xs [Value' Instr t]
-> (Value' Instr t -> SomeAnnotatedValue) -> [SomeAnnotatedValue]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Value' Instr t
x -> Notes t -> Value t -> SomeAnnotatedValue
forall (t :: T).
SingI t =>
Notes t -> Value t -> SomeAnnotatedValue
SomeAnnotatedValue Notes t
xNotes Value t
Value' Instr t
x
SomeAnnotatedValue
_ -> Maybe [SomeAnnotatedValue]
forall a. Maybe a
Nothing
asMap :: forall key. (IsoValue key, Ord key) => Fold SomeAnnotatedValue (Map key SomeAnnotatedValue)
asMap :: Fold SomeAnnotatedValue (Map key SomeAnnotatedValue)
asMap = (SomeAnnotatedValue -> Maybe (Map key SomeAnnotatedValue))
-> Fold SomeAnnotatedValue (Map key SomeAnnotatedValue)
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 :: Notes v
-> Map (Value k) (Value v) -> Maybe (Map key SomeAnnotatedValue)
convert Notes v
vNotes Map (Value k) (Value v)
vmap =
(SingI (ToT key), SingI k, TestEquality Sing) =>
Maybe (ToT key :~: k)
forall k (a :: k) (b :: k).
(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 -> Value (ToT key) -> key
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