-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- | Isomorphisms in Lorentz.
module Lorentz.Iso
  ( LIso (..)
  , invertIso
  , involutedIso
  , checkedCoerceIso
  , forcedCoerceIso
  , namedIso
  , nonIso
  , nonDefIso
  ) where

import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Default
import Lorentz.Instr
import Lorentz.Macro
import Morley.Util.Label
import Morley.Util.Named

-- | Lorentz version of "Control.Lens.Iso".
data LIso a b = LIso
  { forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo :: forall s. a : s :-> b : s
  , forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom :: forall s. b : s :-> a : s
  }

-- | Invert an isomorphism.
invertIso :: LIso a b -> LIso b a
invertIso :: forall a b. LIso a b -> LIso b a
invertIso LIso{forall (s :: [*]). (a : s) :-> (b : s)
forall (s :: [*]). (b : s) :-> (a : s)
liFrom :: forall (s :: [*]). (b : s) :-> (a : s)
liTo :: forall (s :: [*]). (a : s) :-> (b : s)
liFrom :: forall a b. LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liTo :: forall a b. LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
..} = LIso :: forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso{ liTo :: forall (s :: [*]). (b : s) :-> (a : s)
liTo = forall (s :: [*]). (b : s) :-> (a : s)
liFrom, liFrom :: forall (s :: [*]). (a : s) :-> (b : s)
liFrom = forall (s :: [*]). (a : s) :-> (b : s)
liTo }

-- | Given a function that is its own inverse, make an 'LIso' using it
-- in both directions.
involutedIso :: Fn a a -> LIso a a
involutedIso :: forall a. Fn a a -> LIso a a
involutedIso Fn a a
l = (forall (s :: [*]). (a : s) :-> (a : s))
-> (forall (s :: [*]). (a : s) :-> (a : s)) -> LIso a a
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso (Fn a a -> ('[a] ++ s) :-> ('[a] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed Fn a a
l) (Fn a a -> ('[a] ++ s) :-> ('[a] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed Fn a a
l)

-- | The isomorphism between two values with identical representation
-- and semantics.
checkedCoerceIso :: Coercible_ a b => LIso a b
checkedCoerceIso :: forall a b. Coercible_ a b => LIso a b
checkedCoerceIso = (forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso forall (s :: [*]). (a : s) :-> (b : s)
forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ forall (s :: [*]). (b : s) :-> (a : s)
forall a b (s :: [*]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_

-- | The isomorphism between two values with identical representation.
--
-- The same precautions as for 'forcedCoerce' apply here.
forcedCoerceIso :: MichelsonCoercible a b => LIso a b
forcedCoerceIso :: forall a b. MichelsonCoercible a b => LIso a b
forcedCoerceIso = (forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso forall (s :: [*]). (a : s) :-> (b : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_ forall (s :: [*]). (b : s) :-> (a : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | The isomorphism between raw and named value.
namedIso :: Label n -> LIso a (n :! a)
namedIso :: forall (n :: Symbol) a. Label n -> LIso a (n :! a)
namedIso Label n
l = (forall (s :: [*]). (a : s) :-> ((n :! a) : s))
-> (forall (s :: [*]). ((n :! a) : s) :-> (a : s))
-> LIso a (n :! a)
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso (Label n -> (a : s) :-> ((n :! a) : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> (a : s) :-> ((name :! a) : s)
toNamed Label n
l) (Label n -> ((n :! a) : s) :-> (a : s)
forall (name :: Symbol) a (s :: [*]).
Label name -> ((name :! a) : s) :-> (a : s)
fromNamed Label n
l)

-- | Absence of value on the left hand side is associated with
-- the given value on the right hand side.
nonIso :: (NiceConstant a, NiceComparable a) => a -> LIso (Maybe a) a
nonIso :: forall a.
(NiceConstant a, NiceComparable a) =>
a -> LIso (Maybe a) a
nonIso a
defVal = (forall (s :: [*]). (Maybe a : s) :-> (a : s))
-> (forall (s :: [*]). (a : s) :-> (Maybe a : s))
-> LIso (Maybe a) a
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso (a -> (Maybe a : s) :-> (a : s)
forall a (s :: [*]).
NiceConstant a =>
a -> (Maybe a : s) :-> (a : s)
fromOption a
defVal) (a -> (a : s) :-> (Maybe a : s)
forall a (s :: [*]).
(NiceConstant a, NiceComparable a) =>
a -> (a : s) :-> (Maybe a : s)
non a
defVal)

-- | Absence of value on the left hand side is associated with
-- the default value on the right hand side.
--
-- This is more general version of @nonIso ldef@ since it can
-- work with e.g. containers.
nonDefIso :: (LDefault a, NiceConstant a) => LIso (Maybe a) a
nonDefIso :: forall a. (LDefault a, NiceConstant a) => LIso (Maybe a) a
nonDefIso = (forall (s :: [*]). (Maybe a : s) :-> (a : s))
-> (forall (s :: [*]). (a : s) :-> (Maybe a : s))
-> LIso (Maybe a) a
forall a b.
(forall (s :: [*]). (a : s) :-> (b : s))
-> (forall (s :: [*]). (b : s) :-> (a : s)) -> LIso a b
LIso (a -> (Maybe a : s) :-> (a : s)
forall a (s :: [*]).
NiceConstant a =>
a -> (Maybe a : s) :-> (a : s)
fromOption a
forall a. LDefault a => a
ldef) (('[a] :-> '[Bool]) -> (a : s) :-> (Maybe a : s)
forall a (s :: [*]).
NiceConstant a =>
('[a] :-> '[Bool]) -> (a : s) :-> (Maybe a : s)
non' '[a] :-> '[Bool]
forall a (s :: [*]). LDefault a => (a : s) :-> (Bool : s)
lIsDef)