{-# OPTIONS_GHC -Wunused-imports #-}

-- | Examples how to use "Agda.Utils.Lens".

module Agda.Utils.Lens.Examples where

import Agda.Utils.Functor
import Agda.Utils.Lens

data Record a b = Record
  { forall a b. Record a b -> a
field1 :: a
  , forall a b. Record a b -> b
field2 :: b
  }

-- | (View source:) This is how you implement a lens for a record field.
lensField1 :: Lens' (Record a b) a
lensField1 :: forall a b (f :: * -> *).
Functor f =>
(a -> f a) -> Record a b -> f (Record a b)
lensField1 a -> f a
f Record a b
r = a -> f a
f (Record a b -> a
forall a b. Record a b -> a
field1 Record a b
r) f a -> (a -> Record a b) -> f (Record a b)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ a
a -> Record a b
r { field1 = a }

lensField2 :: Lens' (Record a b) b
lensField2 :: forall a b (f :: * -> *).
Functor f =>
(b -> f b) -> Record a b -> f (Record a b)
lensField2 b -> f b
f Record a b
r = b -> f b
f (Record a b -> b
forall a b. Record a b -> b
field2 Record a b
r) f b -> (b -> Record a b) -> f (Record a b)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ b
b -> Record a b
r { field2 = b }