module UVMHS.Core.Data.Lens where

import UVMHS.Core.Init
import UVMHS.Core.Classes

import UVMHS.Core.Data.Choice
import UVMHS.Core.Data.Iter
import UVMHS.Core.Data.Option
import UVMHS.Core.Data.Dict
import UVMHS.Core.Data.Pair
import UVMHS.Core.Data.Sequence
import UVMHS.Core.Data.Set

infixr 1 ⟢
infixr 1 ⌲

newtype a ⟢ b = Lens {forall a b. (a ⟢ b) -> a -> b ∧ (b -> a)
runLens ∷ a → b ∧ (b → a)}
data a ⌲ b = Prism {forall a b. (a ⌲ b) -> b -> a
construct ∷ b → a,forall a b. (a ⌲ b) -> a -> 𝑂 b
view ∷ a → 𝑂 b}

-- # Cursors (common for Lens and Prism)

class Alter (t ∷ ★ → ★ → ★) where alter ∷ t a b → (b → b) → a → a
class AlterM (t ∷ ★ → ★ → ★) where alterM ∷ (Monad m) ⇒ t a b → (b → m b) → a → m a

update ∷ (Alter t) ⇒ t a b → b → a → a
update :: forall (t :: * -> * -> *) a b. Alter t => t a b -> b -> a -> a
update t a b
l b
x = t a b -> (b -> b) -> a -> a
forall a b. t a b -> (b -> b) -> a -> a
forall (t :: * -> * -> *) a b.
Alter t =>
t a b -> (b -> b) -> a -> a
alter t a b
l ((b -> b) -> a -> a) -> (b -> b) -> a -> a
forall a b. (a -> b) -> a -> b
$ b -> b -> b
forall a b. a -> b -> a
const b
x

updateM ∷ (AlterM t,Monad m) ⇒ t a b → m b → a → m a
updateM :: forall (t :: * -> * -> *) (m :: * -> *) a b.
(AlterM t, Monad m) =>
t a b -> m b -> a -> m a
updateM t a b
l m b
xM = t a b -> (b -> m b) -> a -> m a
forall (m :: * -> *) a b.
Monad m =>
t a b -> (b -> m b) -> a -> m a
forall (t :: * -> * -> *) (m :: * -> *) a b.
(AlterM t, Monad m) =>
t a b -> (b -> m b) -> a -> m a
alterM t a b
l ((b -> m b) -> a -> m a) -> (b -> m b) -> a -> m a
forall a b. (a -> b) -> a -> b
$ m b -> b -> m b
forall a b. a -> b -> a
const m b
xM

-- ## Lens

instance Reflexive (⟢) where
  refl :: forall a. a ⟢ a
refl = (a -> a) -> (a -> a) -> a ⟢ a
forall a b. (a -> b) -> (b -> a) -> a ⟢ b
isoLens a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id
instance Transitive (⟢) where
  Lens b -> c ∧ (c -> b)
g ⊚ :: forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
⊚ Lens a -> b ∧ (b -> a)
f = (a -> c ∧ (c -> a)) -> a ⟢ c
forall a b. (a -> b ∧ (b -> a)) -> a ⟢ b
Lens ((a -> c ∧ (c -> a)) -> a ⟢ c) -> (a -> c ∧ (c -> a)) -> a ⟢ c
forall a b. (a -> b) -> a -> b
$ \ a
a →
    let (b
b :* b -> a
ba) = a -> b ∧ (b -> a)
f a
a
        (c
c :* c -> b
cb) = b -> c ∧ (c -> b)
g b
b
    in (c
c c -> (c -> a) -> c ∧ (c -> a)
forall a b. a -> b -> a ∧ b
:* (b -> a
ba (b -> a) -> (c -> b) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ c -> b
cb))
instance Category (⟢)
instance Alter (⟢) where
  alter :: forall a b. (a ⟢ b) -> (b -> b) -> a -> a
alter a ⟢ b
l b -> b
f a
a = let (b
b :* b -> a
ba) = (a ⟢ b) -> a -> b ∧ (b -> a)
forall a b. (a ⟢ b) -> a -> b ∧ (b -> a)
runLens a ⟢ b
l a
a in b -> a
ba (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ b -> b
f b
b
instance AlterM (⟢) where
  alterM :: forall (m :: * -> *) a b.
Monad m =>
(a ⟢ b) -> (b -> m b) -> a -> m a
alterM a ⟢ b
l b -> m b
f a
a = let (b
b :* b -> a
ba) = (a ⟢ b) -> a -> b ∧ (b -> a)
forall a b. (a ⟢ b) -> a -> b ∧ (b -> a)
runLens a ⟢ b
l a
a in (b -> a) -> m b -> m a
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> a
ba (m b -> m a) -> m b -> m a
forall a b. (a -> b) -> a -> b
$ b -> m b
f b
b

lens ∷ (a → b) → (a → b → a) → a ⟢ b
lens :: forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens a -> b
getter a -> b -> a
setter = (a -> b ∧ (b -> a)) -> a ⟢ b
forall a b. (a -> b ∧ (b -> a)) -> a ⟢ b
Lens ((a -> b ∧ (b -> a)) -> a ⟢ b) -> (a -> b ∧ (b -> a)) -> a ⟢ b
forall a b. (a -> b) -> a -> b
$ \ a
s → (a -> b
getter a
s b -> (b -> a) -> b ∧ (b -> a)
forall a b. a -> b -> a ∧ b
:* a -> b -> a
setter a
s)

isoLens ∷ (a → b) → (b → a) → a ⟢ b
isoLens :: forall a b. (a -> b) -> (b -> a) -> a ⟢ b
isoLens a -> b
to b -> a
from = (a -> b) -> (a -> b -> a) -> a ⟢ b
forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens a -> b
to ((a -> b -> a) -> a ⟢ b) -> (a -> b -> a) -> a ⟢ b
forall a b. (a -> b) -> a -> b
$ (b -> a) -> a -> b -> a
forall a b. a -> b -> a
const b -> a
from

access ∷ a ⟢ b → a → b
access :: forall a b. (a ⟢ b) -> a -> b
access a ⟢ b
l = (b ∧ (b -> a)) -> b
forall a b. (a ∧ b) -> a
fst ((b ∧ (b -> a)) -> b) -> (a -> b ∧ (b -> a)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a ⟢ b) -> a -> b ∧ (b -> a)
forall a b. (a ⟢ b) -> a -> b ∧ (b -> a)
runLens a ⟢ b
l

-- ## Prism

instance Reflexive (⌲) where
  refl :: forall a. a ⌲ a
refl = (a -> a) -> (a -> a) -> a ⌲ a
forall b a. (b -> a) -> (a -> b) -> a ⌲ b
isoPrism a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id
instance Transitive (⌲) where
  b ⌲ c
g ⊚ :: forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
⊚ a ⌲ b
f = Prism
    { view :: a -> 𝑂 c
view = (b ⌲ c) -> b -> 𝑂 c
forall a b. (a ⌲ b) -> a -> 𝑂 b
view b ⌲ c
g (b -> 𝑂 c) -> (a -> 𝑂 b) -> a -> 𝑂 c
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
*∘ (a ⌲ b) -> a -> 𝑂 b
forall a b. (a ⌲ b) -> a -> 𝑂 b
view a ⌲ b
f
    , construct :: c -> a
construct = (a ⌲ b) -> b -> a
forall a b. (a ⌲ b) -> b -> a
construct a ⌲ b
f (b -> a) -> (c -> b) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (b ⌲ c) -> c -> b
forall a b. (a ⌲ b) -> b -> a
construct b ⌲ c
g
    }
instance Category (⌲)
instance Alter (⌲) where
  alter :: forall a b. (a ⌲ b) -> (b -> b) -> a -> a
alter a ⌲ b
p b -> b
f a
a = (() -> a) -> (b -> a) -> 𝑂 b -> a
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (a -> () -> a
forall a b. a -> b -> a
const a
a) ((a ⌲ b) -> b -> a
forall a b. (a ⌲ b) -> b -> a
construct a ⌲ b
p (b -> a) -> (b -> b) -> b -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> b
f) (𝑂 b -> a) -> 𝑂 b -> a
forall a b. (a -> b) -> a -> b
$ (a ⌲ b) -> a -> 𝑂 b
forall a b. (a ⌲ b) -> a -> 𝑂 b
view a ⌲ b
p a
a

prism ∷ (b → a) → (a → 𝑂 b) → a ⌲ b
prism :: forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism = (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism

isoPrism ∷ (b → a) → (a → b) → a ⌲ b
isoPrism :: forall b a. (b -> a) -> (a -> b) -> a ⌲ b
isoPrism b -> a
from a -> b
to = (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism b -> a
from ((a -> 𝑂 b) -> a ⌲ b) -> (a -> 𝑂 b) -> a ⌲ b
forall a b. (a -> b) -> a -> b
$ b -> 𝑂 b
forall a. a -> 𝑂 a
Some (b -> 𝑂 b) -> (a -> b) -> a -> 𝑂 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
to

viewΩ ∷ a ⌲ b → a → b
viewΩ :: forall a b. (a ⌲ b) -> a -> b
viewΩ a ⌲ b
p = (() -> b) -> (b -> b) -> 𝑂 b -> b
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (\ () → 𝕊 -> b
forall a. STACK => 𝕊 -> a
error 𝕊
"viewΩ") b -> b
forall a. a -> a
id (𝑂 b -> b) -> (a -> 𝑂 b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a ⌲ b) -> a -> 𝑂 b
forall a b. (a ⌲ b) -> a -> 𝑂 b
view a ⌲ b
p

shape ∷ a ⌲ b → a → 𝔹
shape :: forall a b. (a ⌲ b) -> a -> 𝔹
shape a ⌲ b
p = (() -> 𝔹) -> (b -> 𝔹) -> 𝑂 b -> 𝔹
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (𝔹 -> () -> 𝔹
forall a b. a -> b -> a
const 𝔹
False) (𝔹 -> b -> 𝔹
forall a b. a -> b -> a
const 𝔹
True) (𝑂 b -> 𝔹) -> (a -> 𝑂 b) -> a -> 𝔹
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a ⌲ b) -> a -> 𝑂 b
forall a b. (a ⌲ b) -> a -> 𝑂 b
view a ⌲ b
p

inlL ∷ a ∨ b ⌲ a
inlL :: forall a b. (a ∨ b) ⌲ a
inlL = (a -> a ∨ b) -> ((a ∨ b) -> 𝑂 a) -> (a ∨ b) ⌲ a
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism a -> a ∨ b
forall a b. a -> a ∨ b
Inl (((a ∨ b) -> 𝑂 a) -> (a ∨ b) ⌲ a)
-> ((a ∨ b) -> 𝑂 a) -> (a ∨ b) ⌲ a
forall a b. (a -> b) -> a -> b
$ (a -> 𝑂 a) -> (b -> 𝑂 a) -> (a ∨ b) -> 𝑂 a
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice a -> 𝑂 a
forall a. a -> 𝑂 a
Some ((b -> 𝑂 a) -> (a ∨ b) -> 𝑂 a) -> (b -> 𝑂 a) -> (a ∨ b) -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ 𝑂 a -> b -> 𝑂 a
forall a b. a -> b -> a
const 𝑂 a
forall a. 𝑂 a
None

inrL ∷ a ∨ b ⌲ b
inrL :: forall a b. (a ∨ b) ⌲ b
inrL = (b -> a ∨ b) -> ((a ∨ b) -> 𝑂 b) -> (a ∨ b) ⌲ b
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism b -> a ∨ b
forall a b. b -> a ∨ b
Inr (((a ∨ b) -> 𝑂 b) -> (a ∨ b) ⌲ b)
-> ((a ∨ b) -> 𝑂 b) -> (a ∨ b) ⌲ b
forall a b. (a -> b) -> a -> b
$ (a -> 𝑂 b) -> (b -> 𝑂 b) -> (a ∨ b) -> 𝑂 b
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice (𝑂 b -> a -> 𝑂 b
forall a b. a -> b -> a
const 𝑂 b
forall a. 𝑂 a
None) b -> 𝑂 b
forall a. a -> 𝑂 a
Some

fstL ∷ a ∧ b ⟢ a
fstL :: forall a b. (a ∧ b) ⟢ a
fstL = ((a ∧ b) -> a) -> ((a ∧ b) -> a -> a ∧ b) -> (a ∧ b) ⟢ a
forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens (a ∧ b) -> a
forall a b. (a ∧ b) -> a
fst (((a ∧ b) -> a -> a ∧ b) -> (a ∧ b) ⟢ a)
-> ((a ∧ b) -> a -> a ∧ b) -> (a ∧ b) ⟢ a
forall a b. (a -> b) -> a -> b
$ \ (a
_ :* b
b) → ( a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
b)

sndL ∷ a ∧ b ⟢ b
sndL :: forall a b. (a ∧ b) ⟢ b
sndL = ((a ∧ b) -> b) -> ((a ∧ b) -> b -> a ∧ b) -> (a ∧ b) ⟢ b
forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens (a ∧ b) -> b
forall a b. (a ∧ b) -> b
snd (((a ∧ b) -> b -> a ∧ b) -> (a ∧ b) ⟢ b)
-> ((a ∧ b) -> b -> a ∧ b) -> (a ∧ b) ⟢ b
forall a b. (a -> b) -> a -> b
$ \ (a
a :* b
_) → (a
a a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* )

noneL ∷ 𝑂 a ⌲ ()
noneL :: forall a. 𝑂 a ⌲ ()
noneL = (() -> 𝑂 a) -> (𝑂 a -> 𝑂 ()) -> 𝑂 a ⌲ ()
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism (𝑂 a -> () -> 𝑂 a
forall a b. a -> b -> a
const 𝑂 a
forall a. 𝑂 a
None) ((𝑂 a -> 𝑂 ()) -> 𝑂 a ⌲ ()) -> (𝑂 a -> 𝑂 ()) -> 𝑂 a ⌲ ()
forall a b. (a -> b) -> a -> b
$ (() -> 𝑂 ()) -> (a -> 𝑂 ()) -> 𝑂 a -> 𝑂 ()
forall b a. (() -> b) -> (a -> b) -> 𝑂 a -> b
elim𝑂 (𝑂 () -> () -> 𝑂 ()
forall a b. a -> b -> a
const (𝑂 () -> () -> 𝑂 ()) -> 𝑂 () -> () -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ () -> 𝑂 ()
forall a. a -> 𝑂 a
Some ()) ((a -> 𝑂 ()) -> 𝑂 a -> 𝑂 ()) -> (a -> 𝑂 ()) -> 𝑂 a -> 𝑂 ()
forall a b. (a -> b) -> a -> b
$ 𝑂 () -> a -> 𝑂 ()
forall a b. a -> b -> a
const 𝑂 ()
forall a. 𝑂 a
None

someL ∷ 𝑂 a ⌲ a
someL :: forall a. 𝑂 a ⌲ a
someL = (a -> 𝑂 a) -> (𝑂 a -> 𝑂 a) -> 𝑂 a ⌲ a
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism a -> 𝑂 a
forall a. a -> 𝑂 a
Some 𝑂 a -> 𝑂 a
forall a. a -> a
id

singleL ∷ 𝐿 a ⌲ a
singleL :: forall a. 𝐿 a ⌲ a
singleL = (a -> 𝐿 a) -> (𝐿 a -> 𝑂 a) -> 𝐿 a ⌲ a
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism a -> 𝐿 a
forall a t. Single a t => a -> t
single ((𝐿 a -> 𝑂 a) -> 𝐿 a ⌲ a) -> (𝐿 a -> 𝑂 a) -> 𝐿 a ⌲ a
forall a b. (a -> b) -> a -> b
$ \case
  a
x :& 𝐿 a
Nil → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
  𝐿 a
_ → 𝑂 a
forall a. 𝑂 a
None

consL ∷ 𝐿 a ⌲ (a ∧ 𝐿 a)
consL :: forall a. 𝐿 a ⌲ (a ∧ 𝐿 a)
consL = ((a ∧ 𝐿 a) -> 𝐿 a) -> (𝐿 a -> 𝑂 (a ∧ 𝐿 a)) -> 𝐿 a ⌲ (a ∧ 𝐿 a)
forall a b. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
Prism ((a -> 𝐿 a -> 𝐿 a) -> (a ∧ 𝐿 a) -> 𝐿 a
forall a b c. (a -> b -> c) -> (a ∧ b) -> c
curry a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
(:&)) ((𝐿 a -> 𝑂 (a ∧ 𝐿 a)) -> 𝐿 a ⌲ (a ∧ 𝐿 a))
-> (𝐿 a -> 𝑂 (a ∧ 𝐿 a)) -> 𝐿 a ⌲ (a ∧ 𝐿 a)
forall a b. (a -> b) -> a -> b
$ \case { a
x:&𝐿 a
xs → (a ∧ 𝐿 a) -> 𝑂 (a ∧ 𝐿 a)
forall a. a -> 𝑂 a
Some (a
xa -> 𝐿 a -> a ∧ 𝐿 a
forall a b. a -> b -> a ∧ b
:*𝐿 a
xs) ; 𝐿 a
_ → 𝑂 (a ∧ 𝐿 a)
forall a. 𝑂 a
None}

single𝑃L ∷ (Ord a) ⇒ 𝑃 a ⌲ a
single𝑃L :: forall a. Ord a => 𝑃 a ⌲ a
single𝑃L = (a -> 𝑃 a) -> (𝑃 a -> 𝑂 a) -> 𝑃 a ⌲ a
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism a -> 𝑃 a
forall a. a -> 𝑃 a
single𝑃 ((𝑃 a -> 𝑂 a) -> 𝑃 a ⌲ a) -> (𝑃 a -> 𝑂 a) -> 𝑃 a ⌲ a
forall a b. (a -> b) -> a -> b
$ \ 𝑃 a
xs → case 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
forall a. 𝑃 a -> 𝑂 (a ∧ 𝑃 a)
pminView𝑃 𝑃 a
xs of
  Some (a
x :* 𝑃 a
xs') | 𝑃 a -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝑃 a
xs' → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
  𝑂 (a ∧ 𝑃 a)
_ → 𝑂 a
forall a. 𝑂 a
None

single𝑄L ∷ (Ord a) ⇒ 𝑄 a ⌲ a
single𝑄L :: forall a. Ord a => 𝑄 a ⌲ a
single𝑄L = (a -> 𝑄 a) -> (𝑄 a -> 𝑂 a) -> 𝑄 a ⌲ a
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism a -> 𝑄 a
forall a. a -> 𝑄 a
single𝑄 ((𝑄 a -> 𝑂 a) -> 𝑄 a ⌲ a) -> (𝑄 a -> 𝑂 a) -> 𝑄 a ⌲ a
forall a b. (a -> b) -> a -> b
$ \ 𝑄 a
xs → case 𝑄 a -> 𝑂 (a ∧ 𝑄 a)
forall a. 𝑄 a -> 𝑂 (a ∧ 𝑄 a)
uncons𝑄 𝑄 a
xs of
  Some (a
x :* 𝑄 a
xs') | 𝑄 a -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝑄 a
xs' → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
  𝑂 (a ∧ 𝑄 a)
_ → 𝑂 a
forall a. 𝑂 a
None

single𝐷L ∷ (Ord k) ⇒ (k ⇰ v) ⌲ (k ∧ v)
single𝐷L :: forall k v. Ord k => (k ⇰ v) ⌲ (k ∧ v)
single𝐷L = ((k ∧ v) -> k ⇰ v) -> ((k ⇰ v) -> 𝑂 (k ∧ v)) -> (k ⇰ v) ⌲ (k ∧ v)
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism ((k -> v -> k ⇰ v) -> (k ∧ v) -> k ⇰ v
forall a b c. (a -> b -> c) -> (a ∧ b) -> c
curry k -> v -> k ⇰ v
forall k a. k -> a -> k ⇰ a
(↦♭)) (((k ⇰ v) -> 𝑂 (k ∧ v)) -> (k ⇰ v) ⌲ (k ∧ v))
-> ((k ⇰ v) -> 𝑂 (k ∧ v)) -> (k ⇰ v) ⌲ (k ∧ v)
forall a b. (a -> b) -> a -> b
$ \ k ⇰ v
kvs → case (k ⇰ v) -> 𝑂 ((k ∧ v) ∧ (k ⇰ v))
forall k a. (k ⇰ a) -> 𝑂 ((k ∧ a) ∧ (k ⇰ a))
dminView𝐷 k ⇰ v
kvs of
  Some (k ∧ v
kv :* k ⇰ v
kvs') | (k ⇰ v) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty k ⇰ v
kvs' → (k ∧ v) -> 𝑂 (k ∧ v)
forall a. a -> 𝑂 a
Some k ∧ v
kv
  𝑂 ((k ∧ v) ∧ (k ⇰ v))
_ → 𝑂 (k ∧ v)
forall a. 𝑂 a
None

keyL ∷ (Ord k) ⇒ k → (k ⇰ v) ⟢ 𝑂 v
keyL :: forall k v. Ord k => k -> (k ⇰ v) ⟢ 𝑂 v
keyL k
k = ((k ⇰ v) -> 𝑂 v) -> ((k ⇰ v) -> 𝑂 v -> k ⇰ v) -> (k ⇰ v) ⟢ 𝑂 v
forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens ((k ⇰ v) -> k -> 𝑂 v
forall k v t. Lookup k v t => t -> k -> 𝑂 v
⋕? k
k) (((k ⇰ v) -> 𝑂 v -> k ⇰ v) -> (k ⇰ v) ⟢ 𝑂 v)
-> ((k ⇰ v) -> 𝑂 v -> k ⇰ v) -> (k ⇰ v) ⟢ 𝑂 v
forall a b. (a -> b) -> a -> b
$ (𝑂 v -> (k ⇰ v) -> k ⇰ v) -> (k ⇰ v) -> 𝑂 v -> k ⇰ v
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((𝑂 v -> (k ⇰ v) -> k ⇰ v) -> (k ⇰ v) -> 𝑂 v -> k ⇰ v)
-> (𝑂 v -> (k ⇰ v) -> k ⇰ v) -> (k ⇰ v) -> 𝑂 v -> k ⇰ v
forall a b. (a -> b) -> a -> b
$ \case
  𝑂 v
None → k -> (k ⇰ v) -> k ⇰ v
forall k a. Ord k => k -> (k ⇰ a) -> k ⇰ a
drem𝐷 k
k
  Some v
v → ((k
k k -> v -> k ⇰ v
forall k a. k -> a -> k ⇰ a
↦♭ v
v) (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
forall k a. Ord k => (k ⇰ a) -> (k ⇰ a) -> k ⇰ a
⩌♭)

keyL𝑂 ∷ (Ord k,Null v) ⇒ k → (k ⇰ v) ⟢ v
keyL𝑂 :: forall k v. (Ord k, Null v) => k -> (k ⇰ v) ⟢ v
keyL𝑂 k
k =
  let ℓ :: 𝑂 v ⟢ v
ℓ = (𝑂 v -> v) -> (𝑂 v -> v -> 𝑂 v) -> 𝑂 v ⟢ v
forall a b. (a -> b) -> (a -> b -> a) -> a ⟢ b
lens (v -> 𝑂 v -> v
forall a. a -> 𝑂 a -> a
ifNone v
forall a. Null a => a
null) ((𝑂 v -> v -> 𝑂 v) -> 𝑂 v ⟢ v) -> (𝑂 v -> v -> 𝑂 v) -> 𝑂 v ⟢ v
forall a b. (a -> b) -> a -> b
$ (v -> 𝑂 v) -> 𝑂 v -> v -> 𝑂 v
forall a b. a -> b -> a
const v -> 𝑂 v
forall a. a -> 𝑂 a
Some
  in 𝑂 v ⟢ v
ℓ (𝑂 v ⟢ v) -> ((k ⇰ v) ⟢ 𝑂 v) -> (k ⇰ v) ⟢ v
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ k -> (k ⇰ v) ⟢ 𝑂 v
forall k v. Ord k => k -> (k ⇰ v) ⟢ 𝑂 v
keyL k
k

--------------------------
-- HasPrism and HasLens --
--------------------------

class HasPrism a b where hasPrism ∷ a ⌲ b
class HasLens a b where hasLens ∷ a ⟢ b

instance HasPrism a a where 
  hasPrism :: a ⌲ a
hasPrism = a ⌲ a
forall a. a ⌲ a
forall {k} (t :: k -> k -> *) (a :: k). Reflexive t => t a a
refl
instance HasLens a a where 
  hasLens :: a ⟢ a
hasLens = a ⟢ a
forall a. a ⟢ a
forall {k} (t :: k -> k -> *) (a :: k). Reflexive t => t a a
refl

𝛊 ∷ (HasPrism a b) ⇒ b → a
𝛊 :: forall a b. HasPrism a b => b -> a
𝛊 = (a ⌲ b) -> b -> a
forall a b. (a ⌲ b) -> b -> a
construct a ⌲ b
forall a b. HasPrism a b => a ⌲ b
hasPrism

𝛎 ∷ ∀ b a. (HasPrism a b) ⇒ a → 𝑂 b
𝛎 :: forall b a. HasPrism a b => a -> 𝑂 b
𝛎 = (a ⌲ b) -> a -> 𝑂 b
forall a b. (a ⌲ b) -> a -> 𝑂 b
view a ⌲ b
forall a b. HasPrism a b => a ⌲ b
hasPrism

𝛑 ∷ (HasLens a b) ⇒ a → b
𝛑 :: forall a b. HasLens a b => a -> b
𝛑 = (a ⟢ b) -> a -> b
forall a b. (a ⟢ b) -> a -> b
access a ⟢ b
forall a b. HasLens a b => a ⟢ b
hasLens

𝛏 ∷ (HasLens a b) ⇒ b → a → a
𝛏 :: forall a b. HasLens a b => b -> a -> a
𝛏 b
y a
x = (b ∧ (b -> a)) -> b -> a
forall a b. (a ∧ b) -> b
snd ((a ⟢ b) -> a -> b ∧ (b -> a)
forall a b. (a ⟢ b) -> a -> b ∧ (b -> a)
runLens a ⟢ b
forall a b. HasLens a b => a ⟢ b
hasLens a
x) b
y