-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

module Morley.Michelson.Typed.AnnotatedValue
  ( AnnotatedValue (..)
  , SomeAnnotatedValue(..)
  , getT
  -- * Optics
  , 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)

-- $setup
-- >>> import qualified Data.Map as Map
-- >>> import Morley.Michelson.Parser (notes)
-- >>> import Morley.Michelson.Untyped (fieldAnnQ)
-- >>> :m +Morley.Michelson.Typed Morley.Michelson.Text Control.Lens Fmt

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

----------------------------------------------------------------------------
-- Optics
----------------------------------------------------------------------------

-- | Extract the value out of an annotated value.
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 }

-- | Attempts to cast to the given type.
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

{- | 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.

>>> :{
val = SomeAnnotatedValue
  [notes|or (int %first) (or (nat %second) (int %third))|]
  (toVal (Right (Left 3) :: Either Integer (Either Natural Integer)))
:}

>>> val ^? variant [fieldAnnQ|second|] . to pretty
Just "3 :: nat"

>>> val ^? variant [fieldAnnQ|first|] . to pretty
Nothing
-}
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)
      -- If this node does not have a field ann, then recurse.
      | 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)
_ ->
              -- We've reached a leaf.
              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

      -- We've encountered a node labelled with a field ann, and it's a match.
      | 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
      -- We've encountered a node labelled with a field ann, but it's not a match.
      | 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

{- | 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.

>>> :{
val = SomeAnnotatedValue
  [notes|pair (int %first) (nat %second) (int %third)|]
  (toVal ((1, 2, 3) :: (Integer, Natural, Integer)))
:}

>>> mapM_ print $ map (bimap pretty pretty) $ val ^@.. fields
("%first","1 :: int")
("%second","2 :: nat")
("%third","3 :: int")
-}
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)
_ ->
              -- We've reached a leaf.
              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

{- | 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.

>>> :{
val = SomeAnnotatedValue
  [notes|pair (int %first) (nat %second) (int %third)|]
  (toVal ((1, 2, 3) :: (Integer, Natural, Integer)))
:}

>>> val ^? field [fieldAnnQ|second|] . castTo @Natural . value
Just 2
-}
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

{- | 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.

>>> :{
val = SomeAnnotatedValue
  [notes|pair (int %first) (nat %second) (int %third)|]
  (toVal ((1, 2, 3) :: (Integer, Natural, Integer)))
:}

>>> mapM_ print $ map (bimap pretty pretty) $ val ^@.. nodes
("%first","1 :: int")
("%","Pair 2 3 :: pair (nat %second) (int %third)")
("%second","2 :: nat")
("%third","3 :: int")
-}
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)
_ -> []

-- | Looks up nodes in a tree of pairs with the given field annotation.
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

-- | 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 :: 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

-- | 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 :: 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