module UVMHS.Lib.Annotated where

import UVMHS.Core

import UVMHS.Lib.Pretty

data 𝐴 e a = 𝐴
  { forall e a. 𝐴 e a -> e
atag ∷ e
  , forall e a. 𝐴 e a -> a
aval ∷ a
  } deriving (Int -> 𝐴 e a -> ShowS
[𝐴 e a] -> ShowS
𝐴 e a -> String
(Int -> 𝐴 e a -> ShowS)
-> (𝐴 e a -> String) -> ([𝐴 e a] -> ShowS) -> Show (𝐴 e a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall e a. (Show e, Show a) => Int -> 𝐴 e a -> ShowS
forall e a. (Show e, Show a) => [𝐴 e a] -> ShowS
forall e a. (Show e, Show a) => 𝐴 e a -> String
$cshowsPrec :: forall e a. (Show e, Show a) => Int -> 𝐴 e a -> ShowS
showsPrec :: Int -> 𝐴 e a -> ShowS
$cshow :: forall e a. (Show e, Show a) => 𝐴 e a -> String
show :: 𝐴 e a -> String
$cshowList :: forall e a. (Show e, Show a) => [𝐴 e a] -> ShowS
showList :: [𝐴 e a] -> ShowS
Show)
makeLenses ''𝐴
makePrettySum ''𝐴

instance (Eq a) ⇒ Eq (𝐴 t a) where == :: 𝐴 t a -> 𝐴 t a -> Bool
(==) = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(≡) (a -> a -> Bool) -> (𝐴 t a -> a) -> 𝐴 t a -> 𝐴 t a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 𝐴 t a -> a
forall e a. 𝐴 e a -> a
aval
instance (Ord a) ⇒ Ord (𝐴 t a) where compare :: 𝐴 t a -> 𝐴 t a -> Ordering
compare = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering) -> (𝐴 t a -> a) -> 𝐴 t a -> 𝐴 t a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 𝐴 t a -> a
forall e a. 𝐴 e a -> a
aval
instance Extract (𝐴 t) where extract :: forall a. 𝐴 t a -> a
extract = 𝐴 t a -> a
forall e a. 𝐴 e a -> a
aval
instance Cobind (𝐴 t) where 𝐴 t
e a
x =≫ :: forall a b. 𝐴 t a -> (𝐴 t a -> b) -> 𝐴 t b
=≫ 𝐴 t a -> b
f = t -> b -> 𝐴 t b
forall e a. e -> a -> 𝐴 e a
𝐴 t
e (b -> 𝐴 t b) -> b -> 𝐴 t b
forall a b. (a -> b) -> a -> b
$ 𝐴 t a -> b
f (𝐴 t a -> b) -> 𝐴 t a -> b
forall a b. (a -> b) -> a -> b
$ t -> a -> 𝐴 t a
forall e a. e -> a -> 𝐴 e a
𝐴 t
e a
x
instance Functor (𝐴 t) where map :: forall a b. (a -> b) -> 𝐴 t a -> 𝐴 t b
map = (a -> b) -> 𝐴 t a -> 𝐴 t b
forall (w :: * -> *) a b. Comonad w => (a -> b) -> w a -> w b
wmap
instance FunctorM (𝐴 t) where mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> 𝐴 t a -> m (𝐴 t b)
mapM a -> m b
f (𝐴 t
e a
x) = t -> b -> 𝐴 t b
forall e a. e -> a -> 𝐴 e a
𝐴 t
e (b -> 𝐴 t b) -> m b -> m (𝐴 t b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ a -> m b
f a
x
instance Comonad (𝐴 t)

instance (Null e,Null a) ⇒ Null (𝐴 e a) where null :: 𝐴 e a
null = e -> a -> 𝐴 e a
forall e a. e -> a -> 𝐴 e a
𝐴 e
forall a. Null a => a
null a
forall a. Null a => a
null
instance (Append e,Append a) ⇒ Append (𝐴 e a) where 𝐴 e
e₁ a
x₁ ⧺ :: 𝐴 e a -> 𝐴 e a -> 𝐴 e a
⧺ 𝐴 e
e₂ a
x₂ = e -> a -> 𝐴 e a
forall e a. e -> a -> 𝐴 e a
𝐴 (e
e₁ e -> e -> e
forall a. Append a => a -> a -> a
⧺ e
e₂) (a -> 𝐴 e a) -> a -> 𝐴 e a
forall a b. (a -> b) -> a -> b
$ a
x₁ a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
x₂

map𝐴 ∷ (e → e') → (a → b) → 𝐴 e a → 𝐴 e' b
map𝐴 :: forall e e' a b. (e -> e') -> (a -> b) -> 𝐴 e a -> 𝐴 e' b
map𝐴 e -> e'
f a -> b
g (𝐴 e
e a
x) = e' -> b -> 𝐴 e' b
forall e a. e -> a -> 𝐴 e a
𝐴 (e -> e'
f e
e) (b -> 𝐴 e' b) -> b -> 𝐴 e' b
forall a b. (a -> b) -> a -> b
$ a -> b
g a
x

mapATag ∷ (e → e') → 𝐴 e a → 𝐴 e' a
mapATag :: forall e e' a. (e -> e') -> 𝐴 e a -> 𝐴 e' a
mapATag e -> e'
f = (e -> e') -> (a -> a) -> 𝐴 e a -> 𝐴 e' a
forall e e' a b. (e -> e') -> (a -> b) -> 𝐴 e a -> 𝐴 e' b
map𝐴 e -> e'
f a -> a
forall a. a -> a
id

mapAVal ∷ (a → b) → 𝐴 e a → 𝐴 e b
mapAVal :: forall a b e. (a -> b) -> 𝐴 e a -> 𝐴 e b
mapAVal a -> b
f = (e -> e) -> (a -> b) -> 𝐴 e a -> 𝐴 e b
forall e e' a b. (e -> e') -> (a -> b) -> 𝐴 e a -> 𝐴 e' b
map𝐴 e -> e
forall a. a -> a
id a -> b
f

mapM𝐴 ∷ (Monad m) ⇒ (e → m e') → (a → m b) → 𝐴 e a → m (𝐴 e' b)
mapM𝐴 :: forall (m :: * -> *) e e' a b.
Monad m =>
(e -> m e') -> (a -> m b) -> 𝐴 e a -> m (𝐴 e' b)
mapM𝐴 e -> m e'
f a -> m b
g (𝐴 e
e a
x) = do
  e'
e' ← e -> m e'
f e
e
  b
y ← a -> m b
g a
x
  𝐴 e' b -> m (𝐴 e' b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐴 e' b -> m (𝐴 e' b)) -> 𝐴 e' b -> m (𝐴 e' b)
forall a b. (a -> b) -> a -> b
$ e' -> b -> 𝐴 e' b
forall e a. e -> a -> 𝐴 e a
𝐴 e'
e' b
y

mapMATag ∷ (Monad m) ⇒ (e → m e') → 𝐴 e a → m (𝐴 e' a)
mapMATag :: forall (m :: * -> *) e e' a.
Monad m =>
(e -> m e') -> 𝐴 e a -> m (𝐴 e' a)
mapMATag e -> m e'
f = (e -> m e') -> (a -> m a) -> 𝐴 e a -> m (𝐴 e' a)
forall (m :: * -> *) e e' a b.
Monad m =>
(e -> m e') -> (a -> m b) -> 𝐴 e a -> m (𝐴 e' b)
mapM𝐴 e -> m e'
f a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return

mapMAVal ∷ (Monad m) ⇒ (a → m b) → 𝐴 e a → m (𝐴 e b)
mapMAVal :: forall (m :: * -> *) a b e.
Monad m =>
(a -> m b) -> 𝐴 e a -> m (𝐴 e b)
mapMAVal a -> m b
f = (e -> m e) -> (a -> m b) -> 𝐴 e a -> m (𝐴 e b)
forall (m :: * -> *) e e' a b.
Monad m =>
(e -> m e') -> (a -> m b) -> 𝐴 e a -> m (𝐴 e' b)
mapM𝐴 e -> m e
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return a -> m b
f

untag ∷ ((() → e) → b → b) → 𝐴 e a → (a → b) → b
untag :: forall e b a. ((() -> e) -> b -> b) -> 𝐴 e a -> (a -> b) -> b
untag (() -> e) -> b -> b
cxt (𝐴 e
𝒸 a
x) a -> b
f = (() -> e) -> b -> b
cxt (e -> () -> e
forall a b. a -> b -> a
const e
𝒸) (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x

untagWith ∷ ((() → e) → b → b) → (a → b) → 𝐴 e a → b
untagWith :: forall e b a. ((() -> e) -> b -> b) -> (a -> b) -> 𝐴 e a -> b
untagWith = (𝐴 e a -> (a -> b) -> b) -> (a -> b) -> 𝐴 e a -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((𝐴 e a -> (a -> b) -> b) -> (a -> b) -> 𝐴 e a -> b)
-> (((() -> e) -> b -> b) -> 𝐴 e a -> (a -> b) -> b)
-> ((() -> e) -> b -> b)
-> (a -> b)
-> 𝐴 e a
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((() -> e) -> b -> b) -> 𝐴 e a -> (a -> b) -> b
forall e b a. ((() -> e) -> b -> b) -> 𝐴 e a -> (a -> b) -> b
untag

retag ∷ (Monad m) ⇒ m e → a → m (𝐴 e a)
retag :: forall (m :: * -> *) e a. Monad m => m e -> a -> m (𝐴 e a)
retag m e
eM a
x = do
  e
e ← m e
eM
  𝐴 e a -> m (𝐴 e a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐴 e a -> m (𝐴 e a)) -> 𝐴 e a -> m (𝐴 e a)
forall a b. (a -> b) -> a -> b
$ e -> a -> 𝐴 e a
forall e a. e -> a -> 𝐴 e a
𝐴 e
e a
x