{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

{-|
Module      : Polytropos.Microlens
Description : Lightweight microlens optics integration for Polytropos open records
Copyright   : (c) 2026 The Polytropos Authors
License     : EUPL-1.2 OR Apache-2.0
Maintainer  : nadia.yvette.chambers@ik.me
Stability   : experimental
Portability : non-portable (GHC extensions)

Class-based optics integration for developers who use @microlens@
specifically to avoid transitive dependency bloat: this package depends
strictly on @base@, @polytropos-core@, and @microlens@.

= Architectural Overview & Rationale

Unlike full @lens@, which brings in a large dependency graph, @microlens@
provides the core lens combinators in a lightweight package.

In @polytropos-microlens@:
* Name-based field access goes through 'fieldLens', whose 'FieldIndex'
  constraint is solved to a literal slot index by @polytropos-plugin@.
* The 'each' instance traverses every field of a homogeneous record (where
  all fields have the same type, witnessed by 'AllFieldsAre') in a single
  pass over the flat 'Data.Primitive.SmallArray.SmallArray'.

= When to Use This Module

* When your project prioritizes fast build times and minimal transitive
  dependencies, and requires basic lens access to @polytropos@ records.

= When Not to Use This Module

* When you need prisms over sum variants or advanced indexed optics; use
  "Polytropos.Optics" or "Polytropos.Lens" instead.

= Worked Example

> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeApplications #-}
> {-# OPTIONS_GHC -fplugin=Polytropos.Plugin #-}
>
> import Lens.Micro ((^.), (%~), (&))
> import Polytropos
> import Polytropos.Microlens
>
> -- A genuinely heterogeneous record:
> type User = Record '["name" ':= String, "score" ':= Int]
>
> user :: User
> user = REC { name = "Alice", score = 95 }
>
> -- Accessing a field via heterogeneous fieldLens:
> userName :: String
> userName = user ^. fieldLens (Field @"name")  -- "Alice"
>
> -- Modifying a field:
> user' :: User
> user' = user & fieldLens (Field @"score") %~ (+ 5)  -- score = 100
-}
module Polytropos.Microlens
  ( -- * Field Lenses
    fieldLens

    -- * Homogeneity Evidence
  , AllFieldsAre
  ) where

import Data.Kind            (Constraint, Type)
import Data.Functor.Identity (Identity (..))
import GHC.Exts             (toList)
import Lens.Micro           (Lens')
import Lens.Micro.Internal  (Each (..))
import Polytropos           (Record, Field (..))
import Polytropos.Core      (FieldIndex (..), Row, Pair (..), fieldAt,
                             noInlineUnsafeCo, productRep, repVals, setFieldAt,
                             RowRep (..))

{-------------------------------------------------------------------------------
  Homogeneity evidence
-------------------------------------------------------------------------------}

-- | Evidence that every field of the row @r@ has type @a@.
--
-- Closed type family, so a heterogeneous row fails to reduce and the
-- dependent instances simply do not apply. This is what lets 'each' be a
-- genuine traversal with a single element type instead of an erased
-- @forall@-traversal.
type family AllFieldsAre (a :: Type) (r :: Row) :: Constraint where
  AllFieldsAre _  '[]                = ()
  AllFieldsAre a ((n ':= a) ': rest) = AllFieldsAre a rest

{-------------------------------------------------------------------------------
  Instances
-------------------------------------------------------------------------------}

-- | Homogeneous traversal across all record fields.
--
-- @
-- 'each' :: AllFieldsAre a r => 'Lens.Micro.Traversal' ('Record' ((n ':= a) ': r)) ('Record' ((n ':= a) ': r)) a a
-- @
--
-- The instance head fixes the element type to the row's field type, which is
-- what the @Each@ functional dependencies require: for a row-typed record the
-- row determines the field types, so a type-changing traversal is impossible
-- anyway. Implemented over the flat 'Polytropos.Core.Rep' payload in one
-- pass: read the slots, run the effectful function over the values, and
-- rebuild the record with 'Polytropos.Core.productRep'. For a record with @N@
-- fields this is @O(N)@ with no intermediate tree representation.
--
-- An empty record has no element type to traverse; 'each' deliberately does
-- not apply to @'Record' '[]@.
instance AllFieldsAre a r
      => Each (Record ((n ':= a) ': r)) (Record ((n ':= a) ': r)) a a where
  each :: Traversal (Record ((n ':= a) : r)) (Record ((n ':= a) : r)) a a
each a -> f a
f (RowRep Rep Identity ()
rep) =
    Rep Identity () -> Record ((n ':= a) : r)
forall {k} k1 (f :: * -> *) (r :: RowType) (row :: k1) (a :: k).
Rep f a -> RowRep f r row a
RowRep (Rep Identity () -> Record ((n ':= a) : r))
-> ([Identity a] -> Rep Identity ())
-> [Identity a]
-> Record ((n ':= a) : r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Identity Any] -> Rep Identity ()
forall {k} (f :: * -> *) (a :: k). [f Any] -> Rep f a
productRep ([Identity Any] -> Rep Identity ())
-> ([Identity a] -> [Identity Any])
-> [Identity a]
-> Rep Identity ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Identity a] -> [Identity Any]
forall a b. a -> b
noInlineUnsafeCo
      ([Identity a] -> Record ((n ':= a) : r))
-> f [Identity a] -> f (Record ((n ':= a) : r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Identity Any -> f (Identity a))
-> [Identity Any] -> f [Identity a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\(Identity Any
x) -> a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> f a -> f (Identity a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (Any -> a
forall a b. a -> b
noInlineUnsafeCo Any
x))
                   (SmallArray (Identity Any) -> [Item (SmallArray (Identity Any))]
forall l. IsList l => l -> [Item l]
toList (Rep Identity () -> SmallArray (Identity Any)
forall {k} (f :: * -> *) (a :: k). Rep f a -> SmallArray (f Any)
repVals Rep Identity ()
rep))
  {-# INLINE each #-}

-- | Lens on a record field by name.
--
-- @
-- 'fieldLens' #foo :: 'FieldIndex' "foo" r a => 'Lens'' ('Record' r) a
-- @
--
-- The 'FieldIndex' dictionary carries the slot index as a literal, computed
-- by the TcPlugin; there is no runtime name lookup and no type-level search.
fieldLens :: forall n r a. FieldIndex n r a => Field n -> Lens' (Record r) a
fieldLens :: forall (n :: Symbol) (r :: Row) a.
FieldIndex n r a =>
Field n -> Lens' (Record r) a
fieldLens Field n
_ a -> f a
f (RowRep Rep Identity ()
rep) =
  (a -> RowRep Identity 'ProductRowT r ())
-> f a -> f (RowRep Identity 'ProductRowT r ())
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
a' -> Rep Identity () -> RowRep Identity 'ProductRowT r ()
forall {k} k1 (f :: * -> *) (r :: RowType) (row :: k1) (a :: k).
Rep f a -> RowRep f r row a
RowRep (Int -> Identity Any -> Rep Identity () -> Rep Identity ()
forall {k} (f :: * -> *) (a :: k).
Int -> f Any -> Rep f a -> Rep f a
setFieldAt (forall {kn} k {ka} (n :: kn) (row :: k) (a :: ka).
FieldIndex n row a =>
Int
forall k {ka} (n :: Symbol) (row :: k) (a :: ka).
FieldIndex n row a =>
Int
fieldIndex @_ @n @r @a)
                                  (Any -> Identity Any
forall a. a -> Identity a
Identity (a -> Any
forall a b. a -> b
noInlineUnsafeCo a
a'))
                                  Rep Identity ()
rep))
       (a -> f a
f (ZonkAny 0 -> a
forall a b. a -> b
noInlineUnsafeCo (Identity (ZonkAny 0) -> ZonkAny 0
forall a. Identity a -> a
runIdentity (Int -> Rep Identity () -> Identity (ZonkAny 0)
forall {k} (f :: * -> *) (a :: k) x. Int -> Rep f a -> f x
fieldAt (forall {kn} k {ka} (n :: kn) (row :: k) (a :: ka).
FieldIndex n row a =>
Int
forall k {ka} (n :: Symbol) (row :: k) (a :: ka).
FieldIndex n row a =>
Int
fieldIndex @_ @n @r @a) Rep Identity ()
rep))))
{-# INLINE fieldLens #-}