{-# LANGUAGE AllowAmbiguousTypes #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Inventory (module Exports, zoom, magnify, (=<>), (~<>), adjust) where import Pandora.Paradigm.Inventory.Optics as Exports import Pandora.Paradigm.Inventory.Store as Exports import Pandora.Paradigm.Inventory.State as Exports import Pandora.Paradigm.Inventory.Imprint as Exports import Pandora.Paradigm.Inventory.Equipment as Exports import Pandora.Paradigm.Inventory.Environment as Exports import Pandora.Paradigm.Inventory.Accumulator as Exports import Pandora.Core.Functor (type (~>)) import Pandora.Pattern.Category ((.), ($), (/), identity) import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-))) import Pandora.Pattern.Functor.Extractable (extract) import Pandora.Pattern.Functor.Bivariant ((<->)) import Pandora.Paradigm.Primary.Functor.Function ((!), (%)) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:))) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) import Pandora.Paradigm.Controlflow.Effect.Adaptable (adapt) import Pandora.Paradigm.Structure.Ability.Accessible (Accessible (access)) instance Adjoint (Store s) (State s) where (-|) :: a -> (Store s a -> b) -> State s b a x -| :: a -> (Store s a -> b) -> State s b -| Store s a -> b f = (((->) s :. (:*:) s) := b) -> State s b forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) s :. (:*:) s) := b) -> State s b) -> (((->) s :. (:*:) s) := b) -> State s b forall (m :: * -> * -> *). Category m => m ~~> m $ \s s -> s -> b -> Product s b forall s a. s -> a -> Product s a (:*:) s s (b -> Product s b) -> ((((:*:) s :. (->) s) := a) -> b) -> (((:*:) s :. (->) s) := a) -> Product s b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Store s a -> b f (Store s a -> b) -> ((((:*:) s :. (->) s) := a) -> Store s a) -> (((:*:) s :. (->) s) := a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (((:*:) s :. (->) s) := a) -> Store s a forall s a. (((:*:) s :. (->) s) := a) -> Store s a Store ((((:*:) s :. (->) s) := a) -> Product s b) -> (((:*:) s :. (->) s) := a) -> Product s b forall (m :: * -> * -> *). Category m => m ~~> m $ s s s -> (s -> a) -> ((:*:) s :. (->) s) := a forall s a. s -> a -> Product s a :*: (a x a -> s -> a forall a b. a -> b -> a !) (|-) :: Store s a -> (a -> State s b) -> b Store (s s :*: s -> a f) |- :: Store s a -> (a -> State s b) -> b |- a -> State s b g = b <:= (:*:) s forall (t :: * -> *) a. Extractable t => a <:= t extract (b <:= (:*:) s) -> (a -> Product s b) -> a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . State s b -> ((->) s :. (:*:) s) := b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (State s b -> ((->) s :. (:*:) s) := b) -> s -> State s b -> Product s b forall a b c. (a -> b -> c) -> b -> a -> c % s s (State s b -> Product s b) -> (a -> State s b) -> a -> Product s b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> State s b g (a -> b) -> a -> b forall (m :: * -> * -> *). Category m => m ~~> m $ s -> a f s s instance Adjoint (Accumulator e) (Imprint e) where a x -| :: a -> (Accumulator e a -> b) -> Imprint e b -| Accumulator e a -> b f = (e -> b) -> Imprint e b forall e a. (e -> a) -> Imprint e a Imprint ((e -> b) -> Imprint e b) -> (e -> b) -> Imprint e b forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> (Product e a -> b) -> e -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| Accumulator e a -> b f (Accumulator e a -> b) -> (Product e a -> Accumulator e a) -> Product e a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product e a -> Accumulator e a forall e a. (e :*: a) -> Accumulator e a Accumulator Accumulator e a x |- :: Accumulator e a -> (a -> Imprint e b) -> b |- a -> Imprint e b g = Accumulator e a -> Primary (Accumulator e) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run Accumulator e a x (e :*: a) -> (a -> e -> b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- Imprint e b -> e -> b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Imprint e b -> e -> b) -> (a -> Imprint e b) -> a -> e -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Imprint e b g instance Adjoint (Equipment e) (Environment e) where a x -| :: a -> (Equipment e a -> b) -> Environment e b -| Equipment e a -> b f = (e -> b) -> Environment e b forall e a. (e -> a) -> Environment e a Environment ((e -> b) -> Environment e b) -> (e -> b) -> Environment e b forall (m :: * -> * -> *). Category m => m ~~> m $ a x a -> (Product e a -> b) -> e -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| Equipment e a -> b f (Equipment e a -> b) -> (Product e a -> Equipment e a) -> Product e a -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Product e a -> Equipment e a forall e a. (e :*: a) -> Equipment e a Equipment Equipment e a x |- :: Equipment e a -> (a -> Environment e b) -> b |- a -> Environment e b g = Equipment e a -> Primary (Equipment e) a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run Equipment e a x (e :*: a) -> (a -> e -> b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- Environment e b -> e -> b forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Environment e b -> e -> b) -> (a -> Environment e b) -> a -> e -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> Environment e b g zoom :: Stateful bg t => Lens bg ls -> State ls ~> t zoom :: Lens bg ls -> State ls ~> t zoom Lens bg ls lens State ls a less = let restruct :: (ls -> bg) -> ls -> Product bg a restruct ls -> bg f ls v = ls -> bg f (ls -> bg) -> (a -> a) -> Product ls a -> Product bg a forall (v :: * -> * -> *) a b c d. Bivariant v => (a -> b) -> (c -> d) -> v a c -> v b d <-> a -> a forall (m :: * -> * -> *) a. Category m => m a a identity (Product ls a -> Product bg a) -> Product ls a -> Product bg a forall (m :: * -> * -> *). Category m => m ~~> m $ State ls a -> ((->) ls :. (:*:) ls) := a forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run State ls a less ls v in State bg a -> t a forall k (t :: k -> *) (u :: k -> *). Adaptable t u => t ~> u adapt (State bg a -> t a) -> ((((->) bg :. (:*:) bg) := a) -> State bg a) -> (((->) bg :. (:*:) bg) := a) -> t a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (((->) bg :. (:*:) bg) := a) -> State bg a forall s a. (((->) s :. (:*:) s) := a) -> State s a State ((((->) bg :. (:*:) bg) := a) -> t a) -> (((->) bg :. (:*:) bg) := a) -> t a forall (m :: * -> * -> *). Category m => m ~~> m $ (Product ls (ls -> bg) -> ((ls -> bg) -> ls -> Product bg a) -> Product bg a forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (ls -> bg) -> ls -> Product bg a restruct) (Product ls (ls -> bg) -> Product bg a) -> (bg -> Product ls (ls -> bg)) -> ((->) bg :. (:*:) bg) := a forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Store ls bg -> Product ls (ls -> bg) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run (Store ls bg -> Product ls (ls -> bg)) -> Lens bg ls -> bg -> Product ls (ls -> bg) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . Lens bg ls lens (=<>) :: Stateful src t => src :-. tgt -> tgt -> t src src :-. tgt lens =<> :: (src :-. tgt) -> tgt -> t src =<> tgt new = (src -> src) -> t src forall s (t :: * -> *). Stateful s t => (s -> s) -> t s modify ((src -> src) -> t src) -> (src -> src) -> t src forall (m :: * -> * -> *). Category m => m ~~> m $ (src :-. tgt) -> tgt -> src -> src forall src tgt. Lens src tgt -> tgt -> src -> src set src :-. tgt lens tgt new (~<>) :: Stateful src t => src :-. tgt -> (tgt -> tgt) -> t src src :-. tgt lens ~<> :: (src :-. tgt) -> (tgt -> tgt) -> t src ~<> tgt -> tgt f = (src -> src) -> t src forall s (t :: * -> *). Stateful s t => (s -> s) -> t s modify ((src -> src) -> t src) -> (src -> src) -> t src forall (m :: * -> * -> *). Category m => m ~~> m $ (src :-. tgt) -> (tgt -> tgt) -> src -> src forall src tgt. Lens src tgt -> (tgt -> tgt) -> src -> src over src :-. tgt lens tgt -> tgt f magnify :: forall bg ls t . (Accessible ls bg, Stateful bg t) => t ls magnify :: t ls magnify = forall bg (t :: * -> *) ls. Stateful bg t => Lens bg ls -> State ls ~> t forall (t :: * -> *) ls. Stateful bg t => Lens bg ls -> State ls ~> t zoom @bg (Lens bg ls -> State ls ls -> t ls) -> Lens bg ls -> State ls ls -> t ls forall (m :: * -> * -> *). Category m => m ~~> m / Accessible ls bg => Lens bg ls forall tgt src. Accessible tgt src => src :-. tgt access @ls @bg (State ls ls -> t ls) -> State ls ls -> t ls forall (m :: * -> * -> *). Category m => m ~~> m / State ls ls forall s (t :: * -> *). Stateful s t => t s current adjust :: forall bg ls t . (Accessible ls bg, Stateful bg t) => (ls -> ls) -> t ls adjust :: (ls -> ls) -> t ls adjust = Lens bg ls -> State ls ~> t forall bg (t :: * -> *) ls. Stateful bg t => Lens bg ls -> State ls ~> t zoom @bg (Accessible ls bg => Lens bg ls forall tgt src. Accessible tgt src => src :-. tgt access @ls @bg) (State ls ls -> t ls) -> ((ls -> ls) -> State ls ls) -> (ls -> ls) -> t ls forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . (ls -> ls) -> State ls ls forall s (t :: * -> *). Stateful s t => (s -> s) -> t s modify