{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}
module PlutusCore.Eq
( LR (..)
, RL (..)
, EqRename
, ScopedEqRename
, runEqRename
, withTwinBindings
, eqNameM
, eqM
) where
import PlutusPrelude
import PlutusCore.Name.Unique
import PlutusCore.Rename.Monad
import Control.Lens
newtype LR a = LR
{ forall a. LR a -> a
unLR :: a
} deriving stock ((forall x. LR a -> Rep (LR a) x)
-> (forall x. Rep (LR a) x -> LR a) -> Generic (LR a)
forall x. Rep (LR a) x -> LR a
forall x. LR a -> Rep (LR a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (LR a) x -> LR a
forall a x. LR a -> Rep (LR a) x
$cfrom :: forall a x. LR a -> Rep (LR a) x
from :: forall x. LR a -> Rep (LR a) x
$cto :: forall a x. Rep (LR a) x -> LR a
to :: forall x. Rep (LR a) x -> LR a
Generic)
newtype RL a = RL
{ forall a. RL a -> a
unRL :: a
} deriving stock ((forall x. RL a -> Rep (RL a) x)
-> (forall x. Rep (RL a) x -> RL a) -> Generic (RL a)
forall x. Rep (RL a) x -> RL a
forall x. RL a -> Rep (RL a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (RL a) x -> RL a
forall a x. RL a -> Rep (RL a) x
$cfrom :: forall a x. RL a -> Rep (RL a) x
from :: forall x. RL a -> Rep (RL a) x
$cto :: forall a x. Rep (RL a) x -> RL a
to :: forall x. Rep (RL a) x -> RL a
Generic)
data Bilateral a = Bilateral
{ forall a. Bilateral a -> a
_bilateralL :: a
, forall a. Bilateral a -> a
_bilateralR :: a
}
makeLenses ''Bilateral
instance Wrapped (LR a)
instance Wrapped (RL a)
instance HasUnique name unique => HasUnique (LR name) (LR unique)
instance HasUnique name unique => HasUnique (RL name) (RL unique)
instance Semigroup a => Semigroup (Bilateral a) where
Bilateral a
l1 a
r1 <> :: Bilateral a -> Bilateral a -> Bilateral a
<> Bilateral a
l2 a
r2 = a -> a -> Bilateral a
forall a. a -> a -> Bilateral a
Bilateral (a
l1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
l2) (a
r1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
r2)
instance Monoid a => Monoid (Bilateral a) where
mempty :: Bilateral a
mempty = a -> a -> Bilateral a
forall a. a -> a -> Bilateral a
Bilateral a
forall a. Monoid a => a
mempty a
forall a. Monoid a => a
mempty
instance HasRenaming ren unique => HasRenaming (Bilateral ren) (LR unique) where
renaming :: Lens' (Bilateral ren) (Renaming (LR unique))
renaming = (ren -> f ren) -> Bilateral ren -> f (Bilateral ren)
forall a (f :: * -> *).
Functor f =>
(a -> f a) -> Bilateral a -> f (Bilateral a)
bilateralL ((ren -> f ren) -> Bilateral ren -> f (Bilateral ren))
-> ((Renaming (LR unique) -> f (Renaming (LR unique)))
-> ren -> f ren)
-> (Renaming (LR unique) -> f (Renaming (LR unique)))
-> Bilateral ren
-> f (Bilateral ren)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Renaming unique -> f (Renaming unique)) -> ren -> f ren
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
Lens' ren (Renaming unique)
renaming ((Renaming unique -> f (Renaming unique)) -> ren -> f ren)
-> ((Renaming (LR unique) -> f (Renaming (LR unique)))
-> Renaming unique -> f (Renaming unique))
-> (Renaming (LR unique) -> f (Renaming (LR unique)))
-> ren
-> f ren
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. (Coercible s a, Coercible t b) => Iso s t a b
coerced @(Renaming unique)
instance HasRenaming ren unique => HasRenaming (Bilateral ren) (RL unique) where
renaming :: Lens' (Bilateral ren) (Renaming (RL unique))
renaming = (ren -> f ren) -> Bilateral ren -> f (Bilateral ren)
forall a (f :: * -> *).
Functor f =>
(a -> f a) -> Bilateral a -> f (Bilateral a)
bilateralR ((ren -> f ren) -> Bilateral ren -> f (Bilateral ren))
-> ((Renaming (RL unique) -> f (Renaming (RL unique)))
-> ren -> f ren)
-> (Renaming (RL unique) -> f (Renaming (RL unique)))
-> Bilateral ren
-> f (Bilateral ren)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Renaming unique -> f (Renaming unique)) -> ren -> f ren
forall ren unique.
HasRenaming ren unique =>
Lens' ren (Renaming unique)
Lens' ren (Renaming unique)
renaming ((Renaming unique -> f (Renaming unique)) -> ren -> f ren)
-> ((Renaming (RL unique) -> f (Renaming (RL unique)))
-> Renaming unique -> f (Renaming unique))
-> (Renaming (RL unique) -> f (Renaming (RL unique)))
-> ren
-> f ren
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. (Coercible s a, Coercible t b) => Iso s t a b
coerced @(Renaming unique)
type EqRename ren = RenameT (Bilateral ren) Maybe ()
type ScopedEqRename = EqRename ScopedRenaming
runEqRename :: Monoid ren => EqRename ren -> Bool
runEqRename :: forall ren. Monoid ren => EqRename ren -> Bool
runEqRename = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool)
-> (EqRename ren -> Maybe ()) -> EqRename ren -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqRename ren -> Maybe ()
forall ren (m :: * -> *) a. Monoid ren => RenameT ren m a -> m a
runRenameT
withTwinBindings
:: (HasRenaming ren unique, HasUnique name unique, Monad m)
=> name -> name -> RenameT (Bilateral ren) m c -> RenameT (Bilateral ren) m c
withTwinBindings :: forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique, Monad m) =>
name
-> name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
withTwinBindings name
name1 name
name2 RenameT (Bilateral ren) m c
k =
LR name
-> LR name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique,
MonadReader ren m) =>
name -> name -> m c -> m c
withRenamedName (name -> LR name
forall a. a -> LR a
LR name
name1) (name -> LR name
forall a. a -> LR a
LR name
name2) (RenameT (Bilateral ren) m c -> RenameT (Bilateral ren) m c)
-> RenameT (Bilateral ren) m c -> RenameT (Bilateral ren) m c
forall a b. (a -> b) -> a -> b
$
RL name
-> RL name
-> RenameT (Bilateral ren) m c
-> RenameT (Bilateral ren) m c
forall ren unique name (m :: * -> *) c.
(HasRenaming ren unique, HasUnique name unique,
MonadReader ren m) =>
name -> name -> m c -> m c
withRenamedName (name -> RL name
forall a. a -> RL a
RL name
name2) (name -> RL name
forall a. a -> RL a
RL name
name1) RenameT (Bilateral ren) m c
k
eqNameM
:: (HasRenaming ren unique, HasUnique name unique, Eq unique)
=> name -> name -> EqRename ren
eqNameM :: forall ren unique name.
(HasRenaming ren unique, HasUnique name unique, Eq unique) =>
name -> name -> EqRename ren
eqNameM name
name1 name
name2 = do
Maybe (LR unique)
mayUniq2' <- LR name -> RenameT (Bilateral ren) Maybe (Maybe (LR unique))
forall name unique ren (m :: * -> *).
(HasUnique name unique, HasRenaming ren unique,
MonadReader ren m) =>
name -> m (Maybe unique)
lookupNameM (LR name -> RenameT (Bilateral ren) Maybe (Maybe (LR unique)))
-> LR name -> RenameT (Bilateral ren) Maybe (Maybe (LR unique))
forall a b. (a -> b) -> a -> b
$ name -> LR name
forall a. a -> LR a
LR name
name1
Maybe (RL unique)
mayUniq1' <- RL name -> RenameT (Bilateral ren) Maybe (Maybe (RL unique))
forall name unique ren (m :: * -> *).
(HasUnique name unique, HasRenaming ren unique,
MonadReader ren m) =>
name -> m (Maybe unique)
lookupNameM (RL name -> RenameT (Bilateral ren) Maybe (Maybe (RL unique)))
-> RL name -> RenameT (Bilateral ren) Maybe (Maybe (RL unique))
forall a b. (a -> b) -> a -> b
$ name -> RL name
forall a. a -> RL a
RL name
name2
let uniq1 :: unique
uniq1 = name
name1 name -> Getting unique name unique -> unique
forall s a. s -> Getting a s a -> a
^. Getting unique name unique
forall a unique. HasUnique a unique => Lens' a unique
Lens' name unique
unique
uniq2 :: unique
uniq2 = name
name2 name -> Getting unique name unique -> unique
forall s a. s -> Getting a s a -> a
^. Getting unique name unique
forall a unique. HasUnique a unique => Lens' a unique
Lens' name unique
unique
Bool -> EqRename ren
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> EqRename ren) -> Bool -> EqRename ren
forall a b. (a -> b) -> a -> b
$ case (Maybe (RL unique)
mayUniq1', Maybe (LR unique)
mayUniq2') of
(Maybe (RL unique)
Nothing , Maybe (LR unique)
Nothing ) -> unique
uniq1 unique -> unique -> Bool
forall a. Eq a => a -> a -> Bool
== unique
uniq2
(Just (RL unique
uniq1'), Just (LR unique
uniq2')) -> unique
uniq1 unique -> unique -> Bool
forall a. Eq a => a -> a -> Bool
== unique
uniq1' Bool -> Bool -> Bool
&& unique
uniq2 unique -> unique -> Bool
forall a. Eq a => a -> a -> Bool
== unique
uniq2'
(Maybe (RL unique)
_ , Maybe (LR unique)
_ ) -> Bool
False
eqM :: Eq a => a -> a -> EqRename ren
eqM :: forall a ren. Eq a => a -> a -> EqRename ren
eqM a
x1 a
x2 = Bool -> RenameT (Bilateral ren) Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> RenameT (Bilateral ren) Maybe ())
-> Bool -> RenameT (Bilateral ren) Maybe ()
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x2