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
data LIso a b = LIso
{ LIso a b -> forall (s :: [*]). (a : s) :-> (b : s)
liTo :: forall s. a : s :-> b : s
, LIso a b -> forall (s :: [*]). (b : s) :-> (a : s)
liFrom :: forall s. b : s :-> a : s
}
invertIso :: LIso a b -> LIso b a
invertIso :: 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 }
involutedIso :: Lambda a a -> LIso a a
involutedIso :: Lambda a a -> LIso a a
involutedIso Lambda 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 (Lambda a a -> ('[a] ++ s) :-> ('[a] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed Lambda a a
l) (Lambda a a -> ('[a] ++ s) :-> ('[a] ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed Lambda a a
l)
checkedCoerceIso :: Coercible_ a b => LIso a b
checkedCoerceIso :: 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_
forcedCoerceIso :: MichelsonCoercible a b => LIso a b
forcedCoerceIso :: 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_
namedIso :: Label n -> LIso a (n :! a)
namedIso :: 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)
nonIso :: (NiceConstant a, NiceComparable a) => a -> LIso (Maybe a) a
nonIso :: 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)
nonDefIso :: (LDefault a, NiceConstant a) => LIso (Maybe a) a
nonDefIso :: 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) (Lambda a Bool -> (a : s) :-> (Maybe a : s)
forall a (s :: [*]).
NiceConstant a =>
Lambda a Bool -> (a : s) :-> (Maybe a : s)
non' Lambda a Bool
forall a (s :: [*]). LDefault a => (a : s) :-> (Bool : s)
lIsDef)