{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Alpha
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- Use the 'Alpha' typeclass to mark types that may contain 'Name's.
{-# LANGUAGE DefaultSignatures
             , FlexibleContexts
             , TypeOperators
             , RankNTypes
  #-}
module Unbound.Generics.LocallyNameless.Alpha (
  -- * Name-aware opertions
  Alpha(..)
  -- * Binder variables
  , DisjointSet(..)
  , inconsistentDisjointSet
  , singletonDisjointSet
  , isConsistentDisjointSet
  , isNullDisjointSet
  -- * Implementation details
  , NthPatFind(..)
  , NamePatFind(..)
  , AlphaCtx
  , ctxLevel
  , initialCtx
  , patternCtx
  , termCtx
  , isTermCtx
  , incrLevelCtx
  , decrLevelCtx
  , isZeroLevelCtx
  , ctxLevel
  -- * Internal
  , gaeq
  , gfvAny
  , gclose
  , gopen
  , gisPat
  , gisTerm
  , gnthPatFind
  , gnamePatFind
  , gswaps
  , gfreshen
  , glfreshen
  , gacompare
    -- ** Interal helpers for gfreshen
  , FFM
  , liftFFM
  , retractFFM
  ) where

import Control.Applicative (Applicative(..), (<$>))
import Control.Arrow (first)
import Control.Monad (liftM)
import Data.Function (on)
import Data.Functor.Contravariant (Contravariant(..))
import Data.Foldable (Foldable(..))
import Data.List (intersect)
import Data.Monoid (Monoid(..), All(..))
import Data.Ratio (Ratio)
import Data.Semigroup as Sem
import Data.Typeable (Typeable, gcast, typeOf)
import GHC.Generics

import Unbound.Generics.LocallyNameless.Name
import Unbound.Generics.LocallyNameless.Fresh
import Unbound.Generics.LocallyNameless.LFresh
import Unbound.Generics.PermM

-- | Some 'Alpha' operations need to record information about their
-- progress.  Instances should just pass it through unchanged.
--
-- The context records whether we are currently operating on terms or patterns,
-- and how many binding levels we've descended.
data AlphaCtx = AlphaCtx { AlphaCtx -> Mode
ctxMode :: !Mode, AlphaCtx -> Integer
ctxLevel :: !Integer }

data Mode = Term | Pat
          deriving Mode -> Mode -> Bool
(Mode -> Mode -> Bool) -> (Mode -> Mode -> Bool) -> Eq Mode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Mode -> Mode -> Bool
== :: Mode -> Mode -> Bool
$c/= :: Mode -> Mode -> Bool
/= :: Mode -> Mode -> Bool
Eq

-- | The starting context for alpha operations: we are expecting to
-- work on terms and we are under no binders.
initialCtx :: AlphaCtx
initialCtx :: AlphaCtx
initialCtx = AlphaCtx { ctxMode :: Mode
ctxMode = Mode
Term, ctxLevel :: Integer
ctxLevel = Integer
0 }

-- | Switches to a context where we expect to operate on patterns.
patternCtx :: AlphaCtx -> AlphaCtx
patternCtx :: AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx = AlphaCtx
ctx { ctxMode :: Mode
ctxMode = Mode
Pat }

-- | Switches to a context where we expect to operate on terms.
termCtx :: AlphaCtx -> AlphaCtx
termCtx :: AlphaCtx -> AlphaCtx
termCtx AlphaCtx
ctx = AlphaCtx
ctx { ctxMode :: Mode
ctxMode = Mode
Term }

-- | Returns 'True' iff we are in a context where we expect to see terms.
isTermCtx :: AlphaCtx -> Bool
isTermCtx :: AlphaCtx -> Bool
isTermCtx (AlphaCtx {ctxMode :: AlphaCtx -> Mode
ctxMode = Mode
Term}) = Bool
True
isTermCtx AlphaCtx
_                           = Bool
False

-- | Increment the number of binders that we are operating under.
incrLevelCtx :: AlphaCtx -> AlphaCtx
incrLevelCtx :: AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx = AlphaCtx
ctx { ctxLevel :: Integer
ctxLevel = Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx }

-- | Decrement the number of binders that we are operating under.
decrLevelCtx :: AlphaCtx -> AlphaCtx
decrLevelCtx :: AlphaCtx -> AlphaCtx
decrLevelCtx AlphaCtx
ctx = AlphaCtx
ctx { ctxLevel :: Integer
ctxLevel = AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1 }

-- | Are we operating under no binders?
isZeroLevelCtx :: AlphaCtx -> Bool
isZeroLevelCtx :: AlphaCtx -> Bool
isZeroLevelCtx AlphaCtx
ctx = AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0

-- | A @DisjointSet a@ is a 'Just' a list of distinct @a@s.  In addition to a monoidal
-- structure, a disjoint set also has an annihilator 'inconsistentDisjointSet'.
--
-- @
--   inconsistentDisjointSet \<> s == inconsistentDisjointSet
--   s \<> inconsistentDisjoinSet == inconsistentDisjointSet
-- @
newtype DisjointSet a = DisjointSet (Maybe [a])

-- | @since 0.3.2
instance Eq a => Sem.Semigroup (DisjointSet a) where
  <> :: DisjointSet a -> DisjointSet a -> DisjointSet a
(<>) = \DisjointSet a
s1 DisjointSet a
s2 ->
    case (DisjointSet a
s1, DisjointSet a
s2) of
      (DisjointSet (Just [a]
xs), DisjointSet (Just [a]
ys)) | [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
disjointLists [a]
xs [a]
ys -> Maybe [a] -> DisjointSet a
forall a. Maybe [a] -> DisjointSet a
DisjointSet ([a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a]
xs [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [a]
ys))
      (DisjointSet a, DisjointSet a)
_ -> DisjointSet a
forall a. DisjointSet a
inconsistentDisjointSet

instance Eq a => Monoid (DisjointSet a) where
  mempty :: DisjointSet a
mempty = Maybe [a] -> DisjointSet a
forall a. Maybe [a] -> DisjointSet a
DisjointSet ([a] -> Maybe [a]
forall a. a -> Maybe a
Just [])
  mappend :: DisjointSet a -> DisjointSet a -> DisjointSet a
mappend = DisjointSet a -> DisjointSet a -> DisjointSet a
forall a. Semigroup a => a -> a -> a
(<>)

instance Foldable DisjointSet where
  foldMap :: forall m a. Monoid m => (a -> m) -> DisjointSet a -> m
foldMap a -> m
summarize (DisjointSet Maybe [a]
ms) = ([a] -> m) -> Maybe [a] -> m
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((a -> m) -> [a] -> m
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
summarize) Maybe [a]
ms

-- | Returns a @DisjointSet a@ that is the annihilator element for the 'Monoid' instance of 'DisjointSet'.
inconsistentDisjointSet :: DisjointSet a
inconsistentDisjointSet :: forall a. DisjointSet a
inconsistentDisjointSet = Maybe [a] -> DisjointSet a
forall a. Maybe [a] -> DisjointSet a
DisjointSet Maybe [a]
forall a. Maybe a
Nothing

-- | @singletonDisjointSet x@ a @DisjointSet a@ that contains the single element @x@
singletonDisjointSet :: a -> DisjointSet a
singletonDisjointSet :: forall a. a -> DisjointSet a
singletonDisjointSet a
x = Maybe [a] -> DisjointSet a
forall a. Maybe [a] -> DisjointSet a
DisjointSet ([a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
x])

disjointLists :: Eq a => [a] -> [a] -> Bool
disjointLists :: forall a. Eq a => [a] -> [a] -> Bool
disjointLists [a]
xs [a]
ys = [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
intersect [a]
xs [a]
ys)

-- | @isConsistentDisjointSet@ returns @True@ iff the given disjoint set is not inconsistent.
isConsistentDisjointSet :: DisjointSet a -> Bool
isConsistentDisjointSet :: forall a. DisjointSet a -> Bool
isConsistentDisjointSet (DisjointSet Maybe [a]
Nothing) = Bool
False
isConsistentDisjointSet DisjointSet a
_ = Bool
True

-- | @isNullDisjointSet@ return @True@ iff the given disjoint set is 'mempty'.
isNullDisjointSet :: DisjointSet a -> Bool
isNullDisjointSet :: forall a. DisjointSet a -> Bool
isNullDisjointSet (DisjointSet (Just [])) = Bool
True
isNullDisjointSet DisjointSet a
_ = Bool
False

-- | Types that are instances of @Alpha@ may participate in name representation.
--
-- Minimal instance is entirely empty, provided that your type is an instance of
-- 'Generic'.
class (Show a) => Alpha a where
  -- | See 'Unbound.Generics.LocallyNameless.Operations.aeq'.
  aeq' :: AlphaCtx -> a -> a -> Bool
  default aeq' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Bool
  aeq' AlphaCtx
c = (AlphaCtx -> Rep a Any -> Rep a Any -> Bool
forall a. AlphaCtx -> Rep a a -> Rep a a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
c) (Rep a Any -> Rep a Any -> Bool)
-> (a -> Rep a Any) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE aeq' #-}

  -- | See 'Unbound.Generics.LocallyNameless.Operations.fvAny'.
  --
  -- @
  --  fvAny' :: Fold a AnyName
  -- @
  fvAny' :: (Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
  default fvAny' :: (Generic a, GAlpha (Rep a), Contravariant f, Applicative f) => AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
  fvAny' AlphaCtx
c AnyName -> f AnyName
nfn = (Rep a Any -> a) -> f (Rep a Any) -> f a
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (f (Rep a Any) -> f a) -> (a -> f (Rep a Any)) -> a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> (AnyName -> f AnyName) -> Rep a Any -> f (Rep a Any)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> Rep a a -> g (Rep a a)
gfvAny AlphaCtx
c AnyName -> f AnyName
nfn (Rep a Any -> f (Rep a Any))
-> (a -> Rep a Any) -> a -> f (Rep a Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE fvAny' #-}

  -- | Replace free names by bound names.
  close :: AlphaCtx -> NamePatFind -> a -> a
  default close :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NamePatFind -> a -> a
  close AlphaCtx
c NamePatFind
b = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NamePatFind -> Rep a Any -> Rep a Any
forall a. AlphaCtx -> NamePatFind -> Rep a a -> Rep a a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
c NamePatFind
b (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE close #-}

  -- | Replace bound names by free names.
  open :: AlphaCtx -> NthPatFind -> a -> a
  default open :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> NthPatFind -> a -> a
  open AlphaCtx
c NthPatFind
b = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NthPatFind -> Rep a Any -> Rep a Any
forall a. AlphaCtx -> NthPatFind -> Rep a a -> Rep a a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
c NthPatFind
b (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE open #-}

  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid pattern.
  isPat :: a -> DisjointSet AnyName
  default isPat :: (Generic a, GAlpha (Rep a)) => a -> DisjointSet AnyName
  isPat = Rep a Any -> DisjointSet AnyName
forall a. Rep a a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat (Rep a Any -> DisjointSet AnyName)
-> (a -> Rep a Any) -> a -> DisjointSet AnyName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE isPat #-}

  -- | @isPat x@ dynamically checks whether @x@ can be used as a valid term.
  isTerm :: a -> All
  default isTerm :: (Generic a, GAlpha (Rep a)) => a -> All
  isTerm = Rep a Any -> All
forall a. Rep a a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm (Rep a Any -> All) -> (a -> Rep a Any) -> a -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE isTerm #-}

  -- | @isEmbed@ is needed internally for the implementation of
  --   'isPat'.  @isEmbed@ is true for terms wrapped in 'Embed' and zero
  --   or more occurrences of 'Shift'.  The default implementation
  --   simply returns @False@.
  isEmbed :: a -> Bool
  isEmbed a
_ = Bool
False
  {-# INLINE isEmbed #-}

  -- | If @a@ is a pattern, finds the @n@th name in the pattern
  -- (starting from zero), returning the number of names encountered
  -- if not found.
  nthPatFind :: a -> NthPatFind
  default nthPatFind :: (Generic a, GAlpha (Rep a)) => a -> NthPatFind
  nthPatFind = Rep a Any -> NthPatFind
forall a. Rep a a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind (Rep a Any -> NthPatFind) -> (a -> Rep a Any) -> a -> NthPatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE nthPatFind #-}

  -- | If @a@ is a pattern, find the index of the given name in the pattern.
  namePatFind :: a -> NamePatFind
  default namePatFind :: (Generic a, GAlpha (Rep a)) => a -> NamePatFind
  namePatFind = Rep a Any -> NamePatFind
forall a. Rep a a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind (Rep a Any -> NamePatFind) -> (a -> Rep a Any) -> a -> NamePatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE namePatFind #-}

  -- | See 'Unbound.Generics.LocallyNameless.Operations.swaps'. Apply
  -- the given permutation of variable names to the given pattern.
  swaps' :: AlphaCtx -> Perm AnyName -> a -> a
  default swaps' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> Perm AnyName -> a -> a
  swaps' AlphaCtx
ctx Perm AnyName
perm = Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> Perm AnyName -> Rep a Any -> Rep a Any
forall a. AlphaCtx -> Perm AnyName -> Rep a a -> Rep a a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
  {-# INLINE swaps' #-}

  -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.
  lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
  default lfreshen' :: (LFresh m, Generic a, GAlpha (Rep a))
                       => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
  lfreshen' AlphaCtx
ctx a
m a -> Perm AnyName -> m b
cont = AlphaCtx -> Rep a Any -> (Rep a Any -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> Rep a a -> (Rep a a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
m) (a -> Perm AnyName -> m b
cont (a -> Perm AnyName -> m b)
-> (Rep a Any -> a) -> Rep a Any -> Perm AnyName -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to)
  {-# INLINE lfreshen' #-}

  -- | See 'Unbound.Generics.LocallyNameless.Operations.freshen'.  Rename the free variables
  -- in the given term to be distinct from all other names seen in the monad @m@.
  freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
  default freshen'  :: (Generic a, GAlpha (Rep a), Fresh m) => AlphaCtx -> a -> m (a, Perm AnyName)
  freshen' AlphaCtx
ctx = FFM m (a, Perm AnyName) -> m (a, Perm AnyName)
forall (m :: * -> *) a. Monad m => FFM m a -> m a
retractFFM (FFM m (a, Perm AnyName) -> m (a, Perm AnyName))
-> (a -> FFM m (a, Perm AnyName)) -> a -> m (a, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Rep a Any, Perm AnyName) -> (a, Perm AnyName))
-> FFM m (Rep a Any, Perm AnyName) -> FFM m (a, Perm AnyName)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Rep a Any -> a) -> (Rep a Any, Perm AnyName) -> (a, Perm AnyName)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to) (FFM m (Rep a Any, Perm AnyName) -> FFM m (a, Perm AnyName))
-> (a -> FFM m (Rep a Any, Perm AnyName))
-> a
-> FFM m (a, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> Rep a Any -> FFM m (Rep a Any, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> Rep a a -> FFM m (Rep a a, Perm AnyName)
gfreshen AlphaCtx
ctx (Rep a Any -> FFM m (Rep a Any, Perm AnyName))
-> (a -> Rep a Any) -> a -> FFM m (Rep a Any, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

  -- | See 'Unbound.Generics.LocallyNameless.Operations.acompare'. An alpha-respecting total order on terms involving binders.
  acompare' :: AlphaCtx -> a -> a -> Ordering
  default acompare' :: (Generic a, GAlpha (Rep a)) => AlphaCtx -> a -> a -> Ordering
  acompare' AlphaCtx
c = (AlphaCtx -> Rep a Any -> Rep a Any -> Ordering
forall a. AlphaCtx -> Rep a a -> Rep a a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
c) (Rep a Any -> Rep a Any -> Ordering)
-> (a -> Rep a Any) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

-- Internal: the free monad over the Functor f.  Note that 'freshen''
-- has a monadic return type and moreover we have to thread the
-- permutation through the 'gfreshen' calls to crawl over the value
-- constructors.  Since we don't know anything about the monad @m@,
-- GHC can't help us.  But note that none of the code in the generic
-- 'gfreshen' instances actually makes use of the 'Fresh.fresh'
-- function; they just plumb the dictionary through to any 'K' nodes
-- that happen to contain a value of a type like 'Name' that does
-- actually freshen something.  So what we do is we actually make
-- gfreshen work not in the monad @m@, but in the monad @FFM m@ and
-- then use 'retractFFM' in the default 'Alpha' method to return back
-- down to @m@.  We don't really make use of the fact that 'FFM'
-- reassociates the binds of the underlying monad, but it doesn't hurt
-- anything.  Mostly what we care about is giving the inliner a chance
-- to eliminate most of the monadic plumbing.
newtype FFM f a = FFM { forall (f :: * -> *) a.
FFM f a -> forall r. (a -> r) -> (f r -> r) -> r
runFFM :: forall r . (a -> r) -> (f r -> r) -> r }

instance Functor (FFM f) where
  fmap :: forall a b. (a -> b) -> FFM f a -> FFM f b
fmap a -> b
f (FFM forall r. (a -> r) -> (f r -> r) -> r
h) = (forall r. (b -> r) -> (f r -> r) -> r) -> FFM f b
forall (f :: * -> *) a.
(forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
FFM (\b -> r
r f r -> r
j -> (a -> r) -> (f r -> r) -> r
forall r. (a -> r) -> (f r -> r) -> r
h (b -> r
r (b -> r) -> (a -> b) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f r -> r
j)
  {-# INLINE fmap #-}

instance Applicative (FFM f) where
  pure :: forall a. a -> FFM f a
pure a
x = (forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
forall (f :: * -> *) a.
(forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
FFM (\a -> r
r f r -> r
_j -> a -> r
r a
x)
  {-# INLINE pure #-}
  (FFM forall r. ((a -> b) -> r) -> (f r -> r) -> r
h) <*> :: forall a b. FFM f (a -> b) -> FFM f a -> FFM f b
<*> (FFM forall r. (a -> r) -> (f r -> r) -> r
k) = (forall r. (b -> r) -> (f r -> r) -> r) -> FFM f b
forall (f :: * -> *) a.
(forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
FFM (\b -> r
r f r -> r
j -> ((a -> b) -> r) -> (f r -> r) -> r
forall r. ((a -> b) -> r) -> (f r -> r) -> r
h (\a -> b
f -> (a -> r) -> (f r -> r) -> r
forall r. (a -> r) -> (f r -> r) -> r
k (b -> r
r (b -> r) -> (a -> b) -> a -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f r -> r
j) f r -> r
j)
  {-# INLINE (<*>) #-}

instance Monad (FFM f) where
  return :: forall a. a -> FFM f a
return = a -> FFM f a
forall a. a -> FFM f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  {-# INLINE return #-}
  (FFM forall r. (a -> r) -> (f r -> r) -> r
h) >>= :: forall a b. FFM f a -> (a -> FFM f b) -> FFM f b
>>= a -> FFM f b
f = (forall r. (b -> r) -> (f r -> r) -> r) -> FFM f b
forall (f :: * -> *) a.
(forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
FFM (\b -> r
r f r -> r
j -> (a -> r) -> (f r -> r) -> r
forall r. (a -> r) -> (f r -> r) -> r
h (\a
x -> FFM f b -> forall r. (b -> r) -> (f r -> r) -> r
forall (f :: * -> *) a.
FFM f a -> forall r. (a -> r) -> (f r -> r) -> r
runFFM (a -> FFM f b
f a
x) b -> r
r f r -> r
j) f r -> r
j)
  {-# INLINE (>>=) #-}

instance Fresh m => Fresh (FFM m) where
  fresh :: forall a. Name a -> FFM m (Name a)
fresh = m (Name a) -> FFM m (Name a)
forall (m :: * -> *) a. Monad m => m a -> FFM m a
liftFFM (m (Name a) -> FFM m (Name a))
-> (Name a -> m (Name a)) -> Name a -> FFM m (Name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh 
  {-# INLINE fresh #-}

liftFFM :: Monad m => m a -> FFM m a
liftFFM :: forall (m :: * -> *) a. Monad m => m a -> FFM m a
liftFFM m a
m = (forall r. (a -> r) -> (m r -> r) -> r) -> FFM m a
forall (f :: * -> *) a.
(forall r. (a -> r) -> (f r -> r) -> r) -> FFM f a
FFM (\a -> r
r m r -> r
j -> m r -> r
j ((a -> r) -> m a -> m r
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> r
r m a
m))
{-# INLINE liftFFM #-}

retractFFM :: Monad m => FFM m a -> m a
retractFFM :: forall (m :: * -> *) a. Monad m => FFM m a -> m a
retractFFM (FFM forall r. (a -> r) -> (m r -> r) -> r
h) = (a -> m a) -> (m (m a) -> m a) -> m a
forall r. (a -> r) -> (m r -> r) -> r
h a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return m (m a) -> m a
forall {m :: * -> *} {b}. Monad m => m (m b) -> m b
j
  where
    j :: m (m b) -> m b
j m (m b)
mmf = m (m b)
mmf m (m b) -> (m b -> m b) -> m b
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m b
mf -> m b
mf
{-# INLINE retractFFM #-}

-- | The result of @'nthPatFind' a i@ is @Left k@ where @i-k@ is the
-- number of names in pattern @a@ (with @k < i@) or @Right x@ where @x@
-- is the @i@th name in @a@
newtype NthPatFind = NthPatFind { NthPatFind -> Integer -> Either Integer AnyName
runNthPatFind :: Integer -> Either Integer AnyName }

-- | @since 0.3.2
instance Sem.Semigroup NthPatFind where
  <> :: NthPatFind -> NthPatFind -> NthPatFind
(<>) = \(NthPatFind Integer -> Either Integer AnyName
f) (NthPatFind Integer -> Either Integer AnyName
g) ->
    (Integer -> Either Integer AnyName) -> NthPatFind
NthPatFind ((Integer -> Either Integer AnyName) -> NthPatFind)
-> (Integer -> Either Integer AnyName) -> NthPatFind
forall a b. (a -> b) -> a -> b
$ \Integer
i -> case Integer -> Either Integer AnyName
f Integer
i of
    Left Integer
i' -> Integer -> Either Integer AnyName
g Integer
i'
    found :: Either Integer AnyName
found@Right {} -> Either Integer AnyName
found

instance Monoid NthPatFind where
  mempty :: NthPatFind
mempty = (Integer -> Either Integer AnyName) -> NthPatFind
NthPatFind Integer -> Either Integer AnyName
forall a b. a -> Either a b
Left
  mappend :: NthPatFind -> NthPatFind -> NthPatFind
mappend = NthPatFind -> NthPatFind -> NthPatFind
forall a. Semigroup a => a -> a -> a
(<>)

-- | The result of @'namePatFind' a x@ is either @Left i@ if @a@ is a pattern that
-- contains @i@ free names none of which are @x@, or @Right j@ if @x@ is the @j@th name
-- in @a@
newtype NamePatFind = NamePatFind { NamePatFind -> AnyName -> Either Integer Integer
runNamePatFind :: AnyName
                                                      -- Left - names skipped over
                                                      -- Right - index of the name we found
                                                      -> Either Integer Integer }

-- | @since 0.3.2
instance Sem.Semigroup NamePatFind where
  <> :: NamePatFind -> NamePatFind -> NamePatFind
(<>) = \(NamePatFind AnyName -> Either Integer Integer
f) (NamePatFind AnyName -> Either Integer Integer
g) ->
    (AnyName -> Either Integer Integer) -> NamePatFind
NamePatFind ((AnyName -> Either Integer Integer) -> NamePatFind)
-> (AnyName -> Either Integer Integer) -> NamePatFind
forall a b. (a -> b) -> a -> b
$ \AnyName
nm -> case AnyName -> Either Integer Integer
f AnyName
nm of
    ans :: Either Integer Integer
ans@Right {} -> Either Integer Integer
ans
    Left Integer
n -> case AnyName -> Either Integer Integer
g AnyName
nm of
      Left Integer
m -> Integer -> Either Integer Integer
forall a b. a -> Either a b
Left (Integer -> Either Integer Integer)
-> Integer -> Either Integer Integer
forall a b. (a -> b) -> a -> b
$! Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
m
      Right Integer
i -> Integer -> Either Integer Integer
forall a b. b -> Either a b
Right (Integer -> Either Integer Integer)
-> Integer -> Either Integer Integer
forall a b. (a -> b) -> a -> b
$! Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
i

instance Monoid NamePatFind where
  mempty :: NamePatFind
mempty = (AnyName -> Either Integer Integer) -> NamePatFind
NamePatFind (\AnyName
_ -> Integer -> Either Integer Integer
forall a b. a -> Either a b
Left Integer
0)
  mappend :: NamePatFind -> NamePatFind -> NamePatFind
mappend = NamePatFind -> NamePatFind -> NamePatFind
forall a. Semigroup a => a -> a -> a
(<>)

-- | The "Generic" representation version of 'Alpha'
class GAlpha f where
  gaeq :: AlphaCtx -> f a -> f a -> Bool

  gfvAny :: (Contravariant g, Applicative g) => AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)

  gclose :: AlphaCtx -> NamePatFind -> f a -> f a
  gopen :: AlphaCtx -> NthPatFind -> f a -> f a

  gisPat :: f a -> DisjointSet AnyName
  gisTerm :: f a -> All

  gnthPatFind :: f a -> NthPatFind
  gnamePatFind :: f a -> NamePatFind

  gswaps :: AlphaCtx -> Perm AnyName -> f a -> f a
  gfreshen :: Fresh m => AlphaCtx -> f a -> FFM m (f a, Perm AnyName)

  glfreshen :: LFresh m => AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b

  gacompare :: AlphaCtx -> f a -> f a -> Ordering

instance (Alpha c) => GAlpha (K1 i c) where
  gaeq :: forall a. AlphaCtx -> K1 i c a -> K1 i c a -> Bool
gaeq AlphaCtx
ctx (K1 c
c1) (K1 c
c2) = AlphaCtx -> c -> c -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' AlphaCtx
ctx c
c1 c
c2
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> K1 i c a -> g (K1 i c a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn = (c -> K1 i c a) -> g c -> g (K1 i c a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 (g c -> g (K1 i c a))
-> (K1 i c a -> g c) -> K1 i c a -> g (K1 i c a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> (AnyName -> g AnyName) -> c -> g c
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> c -> f c
fvAny' AlphaCtx
ctx AnyName -> g AnyName
nfn (c -> g c) -> (K1 i c a -> c) -> K1 i c a -> g c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gfvAny #-}
  
  gclose :: forall a. AlphaCtx -> NamePatFind -> K1 i c a -> K1 i c a
gclose AlphaCtx
ctx NamePatFind
b = c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c a) -> (K1 i c a -> c) -> K1 i c a -> K1 i c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NamePatFind -> c -> c
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close AlphaCtx
ctx NamePatFind
b (c -> c) -> (K1 i c a -> c) -> K1 i c a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gclose #-}
  gopen :: forall a. AlphaCtx -> NthPatFind -> K1 i c a -> K1 i c a
gopen AlphaCtx
ctx NthPatFind
b = c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c a) -> (K1 i c a -> c) -> K1 i c a -> K1 i c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NthPatFind -> c -> c
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
ctx NthPatFind
b (c -> c) -> (K1 i c a -> c) -> K1 i c a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gopen #-}

  gisPat :: forall a. K1 i c a -> DisjointSet AnyName
gisPat = c -> DisjointSet AnyName
forall a. Alpha a => a -> DisjointSet AnyName
isPat (c -> DisjointSet AnyName)
-> (K1 i c a -> c) -> K1 i c a -> DisjointSet AnyName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gisPat #-}
  gisTerm :: forall a. K1 i c a -> All
gisTerm = c -> All
forall a. Alpha a => a -> All
isTerm (c -> All) -> (K1 i c a -> c) -> K1 i c a -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gisTerm #-}

  gnthPatFind :: forall a. K1 i c a -> NthPatFind
gnthPatFind = c -> NthPatFind
forall a. Alpha a => a -> NthPatFind
nthPatFind (c -> NthPatFind) -> (K1 i c a -> c) -> K1 i c a -> NthPatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gnthPatFind #-}
  gnamePatFind :: forall a. K1 i c a -> NamePatFind
gnamePatFind = c -> NamePatFind
forall a. Alpha a => a -> NamePatFind
namePatFind (c -> NamePatFind) -> (K1 i c a -> c) -> K1 i c a -> NamePatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gnamePatFind #-}

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> K1 i c a -> K1 i c a
gswaps AlphaCtx
ctx Perm AnyName
perm = c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c a) -> (K1 i c a -> c) -> K1 i c a -> K1 i c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> Perm AnyName -> c -> c
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' AlphaCtx
ctx Perm AnyName
perm (c -> c) -> (K1 i c a -> c) -> K1 i c a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gswaps #-}
  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> K1 i c a -> FFM m (K1 i c a, Perm AnyName)
gfreshen AlphaCtx
ctx = ((c, Perm AnyName) -> (K1 i c a, Perm AnyName))
-> FFM m (c, Perm AnyName) -> FFM m (K1 i c a, Perm AnyName)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((c -> K1 i c a) -> (c, Perm AnyName) -> (K1 i c a, Perm AnyName)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1) (FFM m (c, Perm AnyName) -> FFM m (K1 i c a, Perm AnyName))
-> (K1 i c a -> FFM m (c, Perm AnyName))
-> K1 i c a
-> FFM m (K1 i c a, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (c, Perm AnyName) -> FFM m (c, Perm AnyName)
forall (m :: * -> *) a. Monad m => m a -> FFM m a
liftFFM (m (c, Perm AnyName) -> FFM m (c, Perm AnyName))
-> (K1 i c a -> m (c, Perm AnyName))
-> K1 i c a
-> FFM m (c, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> c -> m (c, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> c -> m (c, Perm AnyName)
freshen' AlphaCtx
ctx (c -> m (c, Perm AnyName))
-> (K1 i c a -> c) -> K1 i c a -> m (c, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c a -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  {-# INLINE gfreshen #-}

  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> K1 i c a -> (K1 i c a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (K1 c
c) K1 i c a -> Perm AnyName -> m b
cont = AlphaCtx -> c -> (c -> Perm AnyName -> m b) -> m b
forall a (m :: * -> *) b.
(Alpha a, LFresh m) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> c -> (c -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx c
c (K1 i c a -> Perm AnyName -> m b
cont (K1 i c a -> Perm AnyName -> m b)
-> (c -> K1 i c a) -> c -> Perm AnyName -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> K1 i c a
forall k i c (p :: k). c -> K1 i c p
K1)
  {-# INLINE glfreshen #-}

  gacompare :: forall a. AlphaCtx -> K1 i c a -> K1 i c a -> Ordering
gacompare AlphaCtx
ctx (K1 c
c1) (K1 c
c2) = AlphaCtx -> c -> c -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
ctx c
c1 c
c2

instance GAlpha f => GAlpha (M1 i c f) where
  gaeq :: forall a. AlphaCtx -> M1 i c f a -> M1 i c f a -> Bool
gaeq AlphaCtx
ctx (M1 f a
f1) (M1 f a
f2) = AlphaCtx -> f a -> f a -> Bool
forall a. AlphaCtx -> f a -> f a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
ctx f a
f1 f a
f2
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> M1 i c f a -> g (M1 i c f a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn = (f a -> M1 i c f a) -> g (f a) -> g (M1 i c f a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (g (f a) -> g (M1 i c f a))
-> (M1 i c f a -> g (f a)) -> M1 i c f a -> g (M1 i c f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn (f a -> g (f a)) -> (M1 i c f a -> f a) -> M1 i c f a -> g (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gfvAny #-}

  gclose :: forall a. AlphaCtx -> NamePatFind -> M1 i c f a -> M1 i c f a
gclose AlphaCtx
ctx NamePatFind
b = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f a -> M1 i c f a)
-> (M1 i c f a -> f a) -> M1 i c f a -> M1 i c f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NamePatFind -> f a -> f a
forall a. AlphaCtx -> NamePatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
ctx NamePatFind
b (f a -> f a) -> (M1 i c f a -> f a) -> M1 i c f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gclose #-}
  gopen :: forall a. AlphaCtx -> NthPatFind -> M1 i c f a -> M1 i c f a
gopen AlphaCtx
ctx NthPatFind
b = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f a -> M1 i c f a)
-> (M1 i c f a -> f a) -> M1 i c f a -> M1 i c f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> NthPatFind -> f a -> f a
forall a. AlphaCtx -> NthPatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
ctx NthPatFind
b (f a -> f a) -> (M1 i c f a -> f a) -> M1 i c f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gopen #-}

  gisPat :: forall a. M1 i c f a -> DisjointSet AnyName
gisPat = f a -> DisjointSet AnyName
forall a. f a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat (f a -> DisjointSet AnyName)
-> (M1 i c f a -> f a) -> M1 i c f a -> DisjointSet AnyName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gisPat #-}
  gisTerm :: forall a. M1 i c f a -> All
gisTerm = f a -> All
forall a. f a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm (f a -> All) -> (M1 i c f a -> f a) -> M1 i c f a -> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gisTerm #-}

  gnthPatFind :: forall a. M1 i c f a -> NthPatFind
gnthPatFind = f a -> NthPatFind
forall a. f a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind (f a -> NthPatFind)
-> (M1 i c f a -> f a) -> M1 i c f a -> NthPatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gnthPatFind #-}
  gnamePatFind :: forall a. M1 i c f a -> NamePatFind
gnamePatFind = f a -> NamePatFind
forall a. f a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind (f a -> NamePatFind)
-> (M1 i c f a -> f a) -> M1 i c f a -> NamePatFind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gnamePatFind #-}

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> M1 i c f a -> M1 i c f a
gswaps AlphaCtx
ctx Perm AnyName
perm = f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f a -> M1 i c f a)
-> (M1 i c f a -> f a) -> M1 i c f a -> M1 i c f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> Perm AnyName -> f a -> f a
forall a. AlphaCtx -> Perm AnyName -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm (f a -> f a) -> (M1 i c f a -> f a) -> M1 i c f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gswaps #-}
  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> M1 i c f a -> FFM m (M1 i c f a, Perm AnyName)
gfreshen AlphaCtx
ctx = ((f a, Perm AnyName) -> (M1 i c f a, Perm AnyName))
-> FFM m (f a, Perm AnyName) -> FFM m (M1 i c f a, Perm AnyName)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((f a -> M1 i c f a)
-> (f a, Perm AnyName) -> (M1 i c f a, Perm AnyName)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1) (FFM m (f a, Perm AnyName) -> FFM m (M1 i c f a, Perm AnyName))
-> (M1 i c f a -> FFM m (f a, Perm AnyName))
-> M1 i c f a
-> FFM m (M1 i c f a, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshen AlphaCtx
ctx (f a -> FFM m (f a, Perm AnyName))
-> (M1 i c f a -> f a) -> M1 i c f a -> FFM m (f a, Perm AnyName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f a -> f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  {-# INLINE gfreshen #-}

  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx
-> M1 i c f a -> (M1 i c f a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (M1 f a
f) M1 i c f a -> Perm AnyName -> m b
cont =
    AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx f a
f (M1 i c f a -> Perm AnyName -> m b
cont (M1 i c f a -> Perm AnyName -> m b)
-> (f a -> M1 i c f a) -> f a -> Perm AnyName -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> M1 i c f a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)
  {-# INLINE glfreshen #-}

  gacompare :: forall a. AlphaCtx -> M1 i c f a -> M1 i c f a -> Ordering
gacompare AlphaCtx
ctx (M1 f a
f1) (M1 f a
f2) = AlphaCtx -> f a -> f a -> Ordering
forall a. AlphaCtx -> f a -> f a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
ctx f a
f1 f a
f2

instance GAlpha U1 where
  gaeq :: forall a. AlphaCtx -> U1 a -> U1 a -> Bool
gaeq AlphaCtx
_ctx U1 a
_ U1 a
_ = Bool
True
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> U1 a -> g (U1 a)
gfvAny AlphaCtx
_ctx AnyName -> g AnyName
_nfn U1 a
_ = U1 a -> g (U1 a)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure U1 a
forall k (p :: k). U1 p
U1

  gclose :: forall a. AlphaCtx -> NamePatFind -> U1 a -> U1 a
gclose AlphaCtx
_ctx NamePatFind
_b U1 a
_ = U1 a
forall k (p :: k). U1 p
U1
  gopen :: forall a. AlphaCtx -> NthPatFind -> U1 a -> U1 a
gopen AlphaCtx
_ctx NthPatFind
_b U1 a
_ = U1 a
forall k (p :: k). U1 p
U1

  gisPat :: forall a. U1 a -> DisjointSet AnyName
gisPat U1 a
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  gisTerm :: forall a. U1 a -> All
gisTerm U1 a
_ = All
forall a. Monoid a => a
mempty

  gnthPatFind :: forall a. U1 a -> NthPatFind
gnthPatFind U1 a
_ = NthPatFind
forall a. Monoid a => a
mempty
  gnamePatFind :: forall a. U1 a -> NamePatFind
gnamePatFind U1 a
_ = NamePatFind
forall a. Monoid a => a
mempty

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> U1 a -> U1 a
gswaps AlphaCtx
_ctx Perm AnyName
_perm U1 a
_ = U1 a
forall k (p :: k). U1 p
U1
  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> U1 a -> FFM m (U1 a, Perm AnyName)
gfreshen AlphaCtx
_ctx U1 a
_ = (U1 a, Perm AnyName) -> FFM m (U1 a, Perm AnyName)
forall a. a -> FFM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (U1 a
forall k (p :: k). U1 p
U1, Perm AnyName
forall a. Monoid a => a
mempty)
  {-# INLINE gfreshen #-}

  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> U1 a -> (U1 a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
_ctx U1 a
_ U1 a -> Perm AnyName -> m b
cont = U1 a -> Perm AnyName -> m b
cont U1 a
forall k (p :: k). U1 p
U1 Perm AnyName
forall a. Monoid a => a
mempty

  gacompare :: forall a. AlphaCtx -> U1 a -> U1 a -> Ordering
gacompare AlphaCtx
_ctx U1 a
_ U1 a
_ = Ordering
EQ

instance GAlpha V1 where
  gaeq :: forall a. AlphaCtx -> V1 a -> V1 a -> Bool
gaeq AlphaCtx
_ctx V1 a
_ V1 a
_ = Bool
False
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> V1 a -> g (V1 a)
gfvAny AlphaCtx
_ctx AnyName -> g AnyName
_nfn = V1 a -> g (V1 a)
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

  gclose :: forall a. AlphaCtx -> NamePatFind -> V1 a -> V1 a
gclose AlphaCtx
_ctx NamePatFind
_b V1 a
_ = V1 a
forall a. HasCallStack => a
undefined
  gopen :: forall a. AlphaCtx -> NthPatFind -> V1 a -> V1 a
gopen AlphaCtx
_ctx NthPatFind
_b V1 a
_ = V1 a
forall a. HasCallStack => a
undefined

  gisPat :: forall a. V1 a -> DisjointSet AnyName
gisPat V1 a
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  gisTerm :: forall a. V1 a -> All
gisTerm V1 a
_ = All
forall a. Monoid a => a
mempty

  gnthPatFind :: forall a. V1 a -> NthPatFind
gnthPatFind V1 a
_ = NthPatFind
forall a. Monoid a => a
mempty
  gnamePatFind :: forall a. V1 a -> NamePatFind
gnamePatFind V1 a
_ = NamePatFind
forall a. Monoid a => a
mempty

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> V1 a -> V1 a
gswaps AlphaCtx
_ctx Perm AnyName
_perm V1 a
_ = V1 a
forall a. HasCallStack => a
undefined
  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> V1 a -> FFM m (V1 a, Perm AnyName)
gfreshen AlphaCtx
_ctx V1 a
_ = (V1 a, Perm AnyName) -> FFM m (V1 a, Perm AnyName)
forall a. a -> FFM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (V1 a
forall a. HasCallStack => a
undefined, Perm AnyName
forall a. Monoid a => a
mempty)
  {-# INLINE gfreshen #-}

  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> V1 a -> (V1 a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
_ctx V1 a
_ V1 a -> Perm AnyName -> m b
cont = V1 a -> Perm AnyName -> m b
cont V1 a
forall a. HasCallStack => a
undefined Perm AnyName
forall a. Monoid a => a
mempty

  gacompare :: forall a. AlphaCtx -> V1 a -> V1 a -> Ordering
gacompare AlphaCtx
_ctx V1 a
_ V1 a
_ = [Char] -> Ordering
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.gacompare: undefined for empty data types"

instance (GAlpha f, GAlpha g) => GAlpha (f :*: g) where
  gaeq :: forall a. AlphaCtx -> (:*:) f g a -> (:*:) f g a -> Bool
gaeq AlphaCtx
ctx (f a
f1 :*: g a
g1) (f a
f2 :*: g a
g2) =
    AlphaCtx -> f a -> f a -> Bool
forall a. AlphaCtx -> f a -> f a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
ctx f a
f1 f a
f2 Bool -> Bool -> Bool
&& AlphaCtx -> g a -> g a -> Bool
forall a. AlphaCtx -> g a -> g a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
ctx g a
g1 g a
g2
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> (:*:) f g a -> g ((:*:) f g a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn (f a
f :*: g a
g) = f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (f a -> g a -> (:*:) f g a) -> g (f a) -> g (g a -> (:*:) f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn f a
f
                                   g (g a -> (:*:) f g a) -> g (g a) -> g ((:*:) f g a)
forall a b. g (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AlphaCtx -> (AnyName -> g AnyName) -> g a -> g (g a)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> g a -> g (g a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn g a
g
  {-# INLINE gfvAny #-}

  gclose :: forall a. AlphaCtx -> NamePatFind -> (:*:) f g a -> (:*:) f g a
gclose AlphaCtx
ctx NamePatFind
b (f a
f :*: g a
g) = AlphaCtx -> NamePatFind -> f a -> f a
forall a. AlphaCtx -> NamePatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
ctx NamePatFind
b f a
f f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: AlphaCtx -> NamePatFind -> g a -> g a
forall a. AlphaCtx -> NamePatFind -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
ctx NamePatFind
b g a
g
  {-# INLINE gclose #-}
  gopen :: forall a. AlphaCtx -> NthPatFind -> (:*:) f g a -> (:*:) f g a
gopen AlphaCtx
ctx NthPatFind
b (f a
f :*: g a
g) = AlphaCtx -> NthPatFind -> f a -> f a
forall a. AlphaCtx -> NthPatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
ctx NthPatFind
b f a
f f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: AlphaCtx -> NthPatFind -> g a -> g a
forall a. AlphaCtx -> NthPatFind -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
ctx NthPatFind
b g a
g
  {-# INLINE gopen #-}

  gisPat :: forall a. (:*:) f g a -> DisjointSet AnyName
gisPat (f a
f :*: g a
g) = f a -> DisjointSet AnyName
forall a. f a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat f a
f DisjointSet AnyName -> DisjointSet AnyName -> DisjointSet AnyName
forall a. Semigroup a => a -> a -> a
<> g a -> DisjointSet AnyName
forall a. g a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat g a
g
  {-# INLINE gisPat #-}
  gisTerm :: forall a. (:*:) f g a -> All
gisTerm (f a
f :*: g a
g) = f a -> All
forall a. f a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm f a
f All -> All -> All
forall a. Semigroup a => a -> a -> a
<> g a -> All
forall a. g a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm g a
g
  {-# INLINE gisTerm #-}

  gnthPatFind :: forall a. (:*:) f g a -> NthPatFind
gnthPatFind (f a
f :*: g a
g) = f a -> NthPatFind
forall a. f a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind f a
f NthPatFind -> NthPatFind -> NthPatFind
forall a. Semigroup a => a -> a -> a
<> g a -> NthPatFind
forall a. g a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind g a
g
  {-# INLINE gnthPatFind #-}
  gnamePatFind :: forall a. (:*:) f g a -> NamePatFind
gnamePatFind (f a
f :*: g a
g) = f a -> NamePatFind
forall a. f a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind f a
f NamePatFind -> NamePatFind -> NamePatFind
forall a. Semigroup a => a -> a -> a
<> g a -> NamePatFind
forall a. g a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind g a
g
  {-# INLINE gnamePatFind #-}

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> (:*:) f g a -> (:*:) f g a
gswaps AlphaCtx
ctx Perm AnyName
perm (f a
f :*: g a
g) =
    AlphaCtx -> Perm AnyName -> f a -> f a
forall a. AlphaCtx -> Perm AnyName -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm f a
f f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: AlphaCtx -> Perm AnyName -> g a -> g a
forall a. AlphaCtx -> Perm AnyName -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm g a
g
  {-# INLINE gswaps #-}

  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> (:*:) f g a -> FFM m ((:*:) f g a, Perm AnyName)
gfreshen AlphaCtx
ctx (f a
f :*: g a
g) = do
    ~(g a
g', Perm AnyName
perm2) <- AlphaCtx -> g a -> FFM m (g a, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> g a -> FFM m (g a, Perm AnyName)
gfreshen AlphaCtx
ctx g a
g
    ~(f a
f', Perm AnyName
perm1) <- AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshen AlphaCtx
ctx (AlphaCtx -> Perm AnyName -> f a -> f a
forall a. AlphaCtx -> Perm AnyName -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm2 f a
f)
    ((:*:) f g a, Perm AnyName) -> FFM m ((:*:) f g a, Perm AnyName)
forall a. a -> FFM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (f a
f' f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
g', Perm AnyName
perm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)
  {-# INLINE gfreshen #-}

  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx
-> (:*:) f g a -> ((:*:) f g a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (f a
f :*: g a
g) (:*:) f g a -> Perm AnyName -> m b
cont =
    AlphaCtx -> g a -> (g a -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> g a -> (g a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx g a
g ((g a -> Perm AnyName -> m b) -> m b)
-> (g a -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \g a
g' Perm AnyName
perm2 ->
    AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (AlphaCtx -> Perm AnyName -> f a -> f a
forall a. AlphaCtx -> Perm AnyName -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm2 f a
f) ((f a -> Perm AnyName -> m b) -> m b)
-> (f a -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \f a
f' Perm AnyName
perm1 ->
    (:*:) f g a -> Perm AnyName -> m b
cont (f a
f' f a -> g a -> (:*:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: g a
g') (Perm AnyName
perm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)
  {-# INLINE glfreshen #-}

  gacompare :: forall a. AlphaCtx -> (:*:) f g a -> (:*:) f g a -> Ordering
gacompare AlphaCtx
ctx (f a
f1 :*: g a
g1) (f a
f2 :*: g a
g2) =
    (AlphaCtx -> f a -> f a -> Ordering
forall a. AlphaCtx -> f a -> f a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
ctx f a
f1 f a
f2) Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (AlphaCtx -> g a -> g a -> Ordering
forall a. AlphaCtx -> g a -> g a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
ctx g a
g1 g a
g2)

instance (GAlpha f, GAlpha g) => GAlpha (f :+: g) where
  gaeq :: forall a. AlphaCtx -> (:+:) f g a -> (:+:) f g a -> Bool
gaeq AlphaCtx
ctx  (L1 f a
f1) (L1 f a
f2) = AlphaCtx -> f a -> f a -> Bool
forall a. AlphaCtx -> f a -> f a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
ctx f a
f1 f a
f2
  gaeq AlphaCtx
ctx  (R1 g a
g1) (R1 g a
g2) = AlphaCtx -> g a -> g a -> Bool
forall a. AlphaCtx -> g a -> g a -> Bool
forall (f :: * -> *) a. GAlpha f => AlphaCtx -> f a -> f a -> Bool
gaeq AlphaCtx
ctx g a
g1 g a
g2
  gaeq AlphaCtx
_ctx (:+:) f g a
_       (:+:) f g a
_       = Bool
False
  {-# INLINE gaeq #-}

  gfvAny :: forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx
-> (AnyName -> g AnyName) -> (:+:) f g a -> g ((:+:) f g a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn (L1 f a
f) = (f a -> (:+:) f g a) -> g (f a) -> g ((:+:) f g a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn f a
f)
  gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn (R1 g a
g) = (g a -> (:+:) f g a) -> g (g a) -> g ((:+:) f g a)
forall a b. (a -> b) -> g a -> g b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (AlphaCtx -> (AnyName -> g AnyName) -> g a -> g (g a)
forall (f :: * -> *) (g :: * -> *) a.
(GAlpha f, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> f a -> g (f a)
forall (g :: * -> *) a.
(Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> g a -> g (g a)
gfvAny AlphaCtx
ctx AnyName -> g AnyName
nfn g a
g)
  {-# INLINE gfvAny #-}
  
  gclose :: forall a. AlphaCtx -> NamePatFind -> (:+:) f g a -> (:+:) f g a
gclose AlphaCtx
ctx NamePatFind
b (L1 f a
f) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (AlphaCtx -> NamePatFind -> f a -> f a
forall a. AlphaCtx -> NamePatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
ctx NamePatFind
b f a
f)
  gclose AlphaCtx
ctx NamePatFind
b (R1 g a
g) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (AlphaCtx -> NamePatFind -> g a -> g a
forall a. AlphaCtx -> NamePatFind -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NamePatFind -> f a -> f a
gclose AlphaCtx
ctx NamePatFind
b g a
g)
  {-# INLINE gclose #-}
  gopen :: forall a. AlphaCtx -> NthPatFind -> (:+:) f g a -> (:+:) f g a
gopen AlphaCtx
ctx NthPatFind
b (L1 f a
f) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (AlphaCtx -> NthPatFind -> f a -> f a
forall a. AlphaCtx -> NthPatFind -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
ctx NthPatFind
b f a
f)
  gopen AlphaCtx
ctx NthPatFind
b (R1 g a
g) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (AlphaCtx -> NthPatFind -> g a -> g a
forall a. AlphaCtx -> NthPatFind -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> NthPatFind -> f a -> f a
gopen AlphaCtx
ctx NthPatFind
b g a
g)
  {-# INLINE gopen #-}

  gisPat :: forall a. (:+:) f g a -> DisjointSet AnyName
gisPat (L1 f a
f) = f a -> DisjointSet AnyName
forall a. f a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat f a
f
  gisPat (R1 g a
g) = g a -> DisjointSet AnyName
forall a. g a -> DisjointSet AnyName
forall (f :: * -> *) a. GAlpha f => f a -> DisjointSet AnyName
gisPat g a
g
  {-# INLINE gisPat #-}

  gisTerm :: forall a. (:+:) f g a -> All
gisTerm (L1 f a
f) = f a -> All
forall a. f a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm f a
f
  gisTerm (R1 g a
g) = g a -> All
forall a. g a -> All
forall (f :: * -> *) a. GAlpha f => f a -> All
gisTerm g a
g
  {-# INLINE gisTerm #-}

  gnthPatFind :: forall a. (:+:) f g a -> NthPatFind
gnthPatFind (L1 f a
f) = f a -> NthPatFind
forall a. f a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind f a
f
  gnthPatFind (R1 g a
g) = g a -> NthPatFind
forall a. g a -> NthPatFind
forall (f :: * -> *) a. GAlpha f => f a -> NthPatFind
gnthPatFind g a
g
  {-# INLINE gnthPatFind #-}

  gnamePatFind :: forall a. (:+:) f g a -> NamePatFind
gnamePatFind (L1 f a
f) = f a -> NamePatFind
forall a. f a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind f a
f
  gnamePatFind (R1 g a
g) = g a -> NamePatFind
forall a. g a -> NamePatFind
forall (f :: * -> *) a. GAlpha f => f a -> NamePatFind
gnamePatFind g a
g
  {-# INLINE gnamePatFind #-}

  gswaps :: forall a. AlphaCtx -> Perm AnyName -> (:+:) f g a -> (:+:) f g a
gswaps AlphaCtx
ctx Perm AnyName
perm (L1 f a
f) = f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (AlphaCtx -> Perm AnyName -> f a -> f a
forall a. AlphaCtx -> Perm AnyName -> f a -> f a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm f a
f)
  gswaps AlphaCtx
ctx Perm AnyName
perm (R1 g a
f) = g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (AlphaCtx -> Perm AnyName -> g a -> g a
forall a. AlphaCtx -> Perm AnyName -> g a -> g a
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> Perm AnyName -> f a -> f a
gswaps AlphaCtx
ctx Perm AnyName
perm g a
f)
  {-# INLINE gswaps #-}

  gfreshen :: forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> (:+:) f g a -> FFM m ((:+:) f g a, Perm AnyName)
gfreshen AlphaCtx
ctx (L1 f a
f) = ((f a, Perm AnyName) -> ((:+:) f g a, Perm AnyName))
-> FFM m (f a, Perm AnyName) -> FFM m ((:+:) f g a, Perm AnyName)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((f a -> (:+:) f g a)
-> (f a, Perm AnyName) -> ((:+:) f g a, Perm AnyName)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) (AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
gfreshen AlphaCtx
ctx f a
f)
  gfreshen AlphaCtx
ctx (R1 g a
f) = ((g a, Perm AnyName) -> ((:+:) f g a, Perm AnyName))
-> FFM m (g a, Perm AnyName) -> FFM m ((:+:) f g a, Perm AnyName)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((g a -> (:+:) f g a)
-> (g a, Perm AnyName) -> ((:+:) f g a, Perm AnyName)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) (AlphaCtx -> g a -> FFM m (g a, Perm AnyName)
forall (f :: * -> *) (m :: * -> *) a.
(GAlpha f, Fresh m) =>
AlphaCtx -> f a -> FFM m (f a, Perm AnyName)
forall (m :: * -> *) a.
Fresh m =>
AlphaCtx -> g a -> FFM m (g a, Perm AnyName)
gfreshen AlphaCtx
ctx g a
f)
  {-# INLINE gfreshen #-}
  
  glfreshen :: forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx
-> (:+:) f g a -> ((:+:) f g a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx (L1 f a
f) (:+:) f g a -> Perm AnyName -> m b
cont =
    AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx f a
f ((:+:) f g a -> Perm AnyName -> m b
cont ((:+:) f g a -> Perm AnyName -> m b)
-> (f a -> (:+:) f g a) -> f a -> Perm AnyName -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1)
  glfreshen AlphaCtx
ctx (R1 g a
g) (:+:) f g a -> Perm AnyName -> m b
cont =
    AlphaCtx -> g a -> (g a -> Perm AnyName -> m b) -> m b
forall (f :: * -> *) (m :: * -> *) a b.
(GAlpha f, LFresh m) =>
AlphaCtx -> f a -> (f a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) a b.
LFresh m =>
AlphaCtx -> g a -> (g a -> Perm AnyName -> m b) -> m b
glfreshen AlphaCtx
ctx g a
g ((:+:) f g a -> Perm AnyName -> m b
cont ((:+:) f g a -> Perm AnyName -> m b)
-> (g a -> (:+:) f g a) -> g a -> Perm AnyName -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> (:+:) f g a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1)
  {-# INLINE glfreshen #-}

  gacompare :: forall a. AlphaCtx -> (:+:) f g a -> (:+:) f g a -> Ordering
gacompare AlphaCtx
_ctx (L1 f a
_) (R1 g a
_)   = Ordering
LT
  gacompare AlphaCtx
_ctx (R1 g a
_) (L1 f a
_)   = Ordering
GT
  gacompare AlphaCtx
ctx  (L1 f a
f1) (L1 f a
f2) = AlphaCtx -> f a -> f a -> Ordering
forall a. AlphaCtx -> f a -> f a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
ctx f a
f1 f a
f2
  gacompare AlphaCtx
ctx  (R1 g a
g1) (R1 g a
g2) = AlphaCtx -> g a -> g a -> Ordering
forall a. AlphaCtx -> g a -> g a -> Ordering
forall (f :: * -> *) a.
GAlpha f =>
AlphaCtx -> f a -> f a -> Ordering
gacompare AlphaCtx
ctx g a
g1 g a
g2
  {-# INLINE gacompare #-}

-- ============================================================
-- Alpha instances for the usual types

instance Alpha Int where
  aeq' :: AlphaCtx -> Int -> Int -> Bool
aeq' AlphaCtx
_ctx Int
i Int
j = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Int -> f Int
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Int
i = Int -> f Int
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i

  close :: AlphaCtx -> NamePatFind -> Int -> Int
close AlphaCtx
_ctx NamePatFind
_b Int
i = Int
i
  open :: AlphaCtx -> NthPatFind -> Int -> Int
open AlphaCtx
_ctx NthPatFind
_b Int
i = Int
i

  isPat :: Int -> DisjointSet AnyName
isPat Int
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Int -> All
isTerm Int
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Int -> NthPatFind
nthPatFind Int
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Int -> NamePatFind
namePatFind Int
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Int -> Int
swaps' AlphaCtx
_ctx Perm AnyName
_p Int
i = Int
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Int -> m (Int, Perm AnyName)
freshen' AlphaCtx
_ctx Int
i = (Int, Perm AnyName) -> m (Int, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Int -> (Int -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Int
i Int -> Perm AnyName -> m b
cont = Int -> Perm AnyName -> m b
cont Int
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Int -> Int -> Ordering
acompare' AlphaCtx
_ctx Int
i Int
j = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
i Int
j

instance Alpha Char where
  aeq' :: AlphaCtx -> Char -> Char -> Bool
aeq' AlphaCtx
_ctx Char
i Char
j = Char
i Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Char -> f Char
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Char
i = Char -> f Char
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Char
i

  close :: AlphaCtx -> NamePatFind -> Char -> Char
close AlphaCtx
_ctx NamePatFind
_b Char
i = Char
i
  open :: AlphaCtx -> NthPatFind -> Char -> Char
open AlphaCtx
_ctx NthPatFind
_b Char
i = Char
i

  isPat :: Char -> DisjointSet AnyName
isPat Char
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Char -> All
isTerm Char
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Char -> NthPatFind
nthPatFind Char
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Char -> NamePatFind
namePatFind Char
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Char -> Char
swaps' AlphaCtx
_ctx Perm AnyName
_p Char
i = Char
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Char -> m (Char, Perm AnyName)
freshen' AlphaCtx
_ctx Char
i = (Char, Perm AnyName) -> m (Char, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Char -> (Char -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Char
i Char -> Perm AnyName -> m b
cont = Char -> Perm AnyName -> m b
cont Char
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Char -> Char -> Ordering
acompare' AlphaCtx
_ctx Char
i Char
j = Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Char
i Char
j

instance Alpha Integer where
  aeq' :: AlphaCtx -> Integer -> Integer -> Bool
aeq' AlphaCtx
_ctx Integer
i Integer
j = Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Integer -> f Integer
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Integer
i = Integer -> f Integer
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
i

  close :: AlphaCtx -> NamePatFind -> Integer -> Integer
close AlphaCtx
_ctx NamePatFind
_b Integer
i = Integer
i
  open :: AlphaCtx -> NthPatFind -> Integer -> Integer
open AlphaCtx
_ctx NthPatFind
_b Integer
i = Integer
i

  isPat :: Integer -> DisjointSet AnyName
isPat Integer
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Integer -> All
isTerm Integer
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Integer -> NthPatFind
nthPatFind Integer
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Integer -> NamePatFind
namePatFind Integer
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Integer -> Integer
swaps' AlphaCtx
_ctx Perm AnyName
_p Integer
i = Integer
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Integer -> m (Integer, Perm AnyName)
freshen' AlphaCtx
_ctx Integer
i = (Integer, Perm AnyName) -> m (Integer, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Integer -> (Integer -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Integer
i Integer -> Perm AnyName -> m b
cont = Integer -> Perm AnyName -> m b
cont Integer
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Integer -> Integer -> Ordering
acompare' AlphaCtx
_ctx Integer
i Integer
j = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
i Integer
j

instance Alpha Float where
  aeq' :: AlphaCtx -> Float -> Float -> Bool
aeq' AlphaCtx
_ctx Float
i Float
j = Float
i Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== Float
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Float -> f Float
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Float
i = Float -> f Float
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Float
i

  close :: AlphaCtx -> NamePatFind -> Float -> Float
close AlphaCtx
_ctx NamePatFind
_b Float
i = Float
i
  open :: AlphaCtx -> NthPatFind -> Float -> Float
open AlphaCtx
_ctx NthPatFind
_b Float
i = Float
i

  isPat :: Float -> DisjointSet AnyName
isPat Float
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Float -> All
isTerm Float
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Float -> NthPatFind
nthPatFind Float
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Float -> NamePatFind
namePatFind Float
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Float -> Float
swaps' AlphaCtx
_ctx Perm AnyName
_p Float
i = Float
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Float -> m (Float, Perm AnyName)
freshen' AlphaCtx
_ctx Float
i = (Float, Perm AnyName) -> m (Float, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Float
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Float -> (Float -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Float
i Float -> Perm AnyName -> m b
cont = Float -> Perm AnyName -> m b
cont Float
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Float -> Float -> Ordering
acompare' AlphaCtx
_ctx Float
i Float
j = Float -> Float -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Float
i Float
j

instance Alpha Double where
  aeq' :: AlphaCtx -> Double -> Double -> Bool
aeq' AlphaCtx
_ctx Double
i Double
j = Double
i Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Double -> f Double
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Double
i = Double -> f Double
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Double
i

  close :: AlphaCtx -> NamePatFind -> Double -> Double
close AlphaCtx
_ctx NamePatFind
_b Double
i = Double
i
  open :: AlphaCtx -> NthPatFind -> Double -> Double
open AlphaCtx
_ctx NthPatFind
_b Double
i = Double
i

  isPat :: Double -> DisjointSet AnyName
isPat Double
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Double -> All
isTerm Double
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Double -> NthPatFind
nthPatFind Double
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Double -> NamePatFind
namePatFind Double
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Double -> Double
swaps' AlphaCtx
_ctx Perm AnyName
_p Double
i = Double
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Double -> m (Double, Perm AnyName)
freshen' AlphaCtx
_ctx Double
i = (Double, Perm AnyName) -> m (Double, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Double
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Double -> (Double -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Double
i Double -> Perm AnyName -> m b
cont = Double -> Perm AnyName -> m b
cont Double
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Double -> Double -> Ordering
acompare' AlphaCtx
_ctx Double
i Double
j = Double -> Double -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Double
i Double
j

instance (Integral n, Alpha n) => Alpha (Ratio n) where
  aeq' :: AlphaCtx -> Ratio n -> Ratio n -> Bool
aeq' AlphaCtx
_ctx Ratio n
i Ratio n
j = Ratio n
i Ratio n -> Ratio n -> Bool
forall a. Eq a => a -> a -> Bool
== Ratio n
j

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Ratio n -> f (Ratio n)
fvAny' AlphaCtx
_ctx AnyName -> f AnyName
_nfn Ratio n
i = Ratio n -> f (Ratio n)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ratio n
i

  close :: AlphaCtx -> NamePatFind -> Ratio n -> Ratio n
close AlphaCtx
_ctx NamePatFind
_b Ratio n
i = Ratio n
i
  open :: AlphaCtx -> NthPatFind -> Ratio n -> Ratio n
open AlphaCtx
_ctx NthPatFind
_b Ratio n
i = Ratio n
i

  isPat :: Ratio n -> DisjointSet AnyName
isPat Ratio n
_ = DisjointSet AnyName
forall a. Monoid a => a
mempty
  isTerm :: Ratio n -> All
isTerm Ratio n
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Ratio n -> NthPatFind
nthPatFind Ratio n
_ = NthPatFind
forall a. Monoid a => a
mempty
  namePatFind :: Ratio n -> NamePatFind
namePatFind Ratio n
_ = NamePatFind
forall a. Monoid a => a
mempty

  swaps' :: AlphaCtx -> Perm AnyName -> Ratio n -> Ratio n
swaps' AlphaCtx
_ctx Perm AnyName
_p Ratio n
i = Ratio n
i
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Ratio n -> m (Ratio n, Perm AnyName)
freshen' AlphaCtx
_ctx Ratio n
i = (Ratio n, Perm AnyName) -> m (Ratio n, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ratio n
i, Perm AnyName
forall a. Monoid a => a
mempty)
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Ratio n -> (Ratio n -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
_ctx Ratio n
i Ratio n -> Perm AnyName -> m b
cont = Ratio n -> Perm AnyName -> m b
cont Ratio n
i Perm AnyName
forall a. Monoid a => a
mempty

  acompare' :: AlphaCtx -> Ratio n -> Ratio n -> Ordering
acompare' AlphaCtx
_ctx Ratio n
i Ratio n
j = Ratio n -> Ratio n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Ratio n
i Ratio n
j

instance Alpha Bool

instance Alpha a => Alpha (Maybe a)
instance Alpha a => Alpha [a]
instance Alpha ()
instance (Alpha a,Alpha b) => Alpha (Either a b)
instance (Alpha a,Alpha b) => Alpha (a,b)
instance (Alpha a,Alpha b,Alpha c) => Alpha (a,b,c)
instance (Alpha a, Alpha b,Alpha c, Alpha d) => Alpha (a,b,c,d)
instance (Alpha a, Alpha b,Alpha c, Alpha d, Alpha e) =>
   Alpha (a,b,c,d,e)

-- ============================================================
-- Alpha instances for interesting types

instance Typeable a => Alpha (Name a) where
  aeq' :: AlphaCtx -> Name a -> Name a -> Bool
aeq' AlphaCtx
ctx Name a
n1 Name a
n2 =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then Name a
n1 Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name a
n2 -- in terms, better be the same name
    else Bool
True     -- in a pattern, names are always equivlent (since
                  -- they're both bound, so they can vary).

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Name a -> f (Name a)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
nfn Name a
nm = if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx Bool -> Bool -> Bool
&& Name a -> Bool
forall a. Name a -> Bool
isFreeName Name a
nm
                      then (Name a -> AnyName) -> f AnyName -> f (Name a)
forall a' a. (a' -> a) -> f a -> f a'
forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName  (AnyName -> f AnyName
nfn (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm))
                      else Name a -> f (Name a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name a
nm

  open :: AlphaCtx -> NthPatFind -> Name a -> Name a
open AlphaCtx
ctx NthPatFind
b a :: Name a
a@(Bn Integer
l Integer
k) =
    if AlphaCtx -> Mode
ctxMode AlphaCtx
ctx Mode -> Mode -> Bool
forall a. Eq a => a -> a -> Bool
== Mode
Term Bool -> Bool -> Bool
&& AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
l
    then case NthPatFind -> Integer -> Either Integer AnyName
runNthPatFind NthPatFind
b Integer
k of
      Right (AnyName Name a
nm) -> case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
nm of
        Just Name a
nm' -> Name a
nm'
        Maybe (Name a)
Nothing -> [Char] -> Name a
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.open: inconsistent sorts"
      Left Integer
_ -> [Char] -> Name a
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.open : inconsistency - pattern had too few variables"
    else
      Name a
a
  open AlphaCtx
_ctx NthPatFind
_ Name a
a = Name a
a

  close :: AlphaCtx -> NamePatFind -> Name a -> Name a
close AlphaCtx
ctx NamePatFind
b a :: Name a
a@(Fn [Char]
_ Integer
_) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then case NamePatFind -> AnyName -> Either Integer Integer
runNamePatFind NamePatFind
b (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
a) of
      Right Integer
k -> Integer -> Integer -> Name a
forall a. Integer -> Integer -> Name a
Bn (AlphaCtx -> Integer
ctxLevel AlphaCtx
ctx) Integer
k
      Left Integer
_ -> Name a
a
    else Name a
a
  close AlphaCtx
_ctx NamePatFind
_ Name a
a = Name a
a
  

  isPat :: Name a -> DisjointSet AnyName
isPat Name a
n = if Name a -> Bool
forall a. Name a -> Bool
isFreeName Name a
n
            then AnyName -> DisjointSet AnyName
forall a. a -> DisjointSet a
singletonDisjointSet (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
n)
            else DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet

  isTerm :: Name a -> All
isTerm Name a
_ = All
forall a. Monoid a => a
mempty

  nthPatFind :: Name a -> NthPatFind
nthPatFind Name a
nm = (Integer -> Either Integer AnyName) -> NthPatFind
NthPatFind ((Integer -> Either Integer AnyName) -> NthPatFind)
-> (Integer -> Either Integer AnyName) -> NthPatFind
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then AnyName -> Either Integer AnyName
forall a b. b -> Either a b
Right (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) else Integer -> Either Integer AnyName
forall a b. a -> Either a b
Left (Integer -> Either Integer AnyName)
-> Integer -> Either Integer AnyName
forall a b. (a -> b) -> a -> b
$! Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1

  namePatFind :: Name a -> NamePatFind
namePatFind Name a
nm1 = (AnyName -> Either Integer Integer) -> NamePatFind
NamePatFind ((AnyName -> Either Integer Integer) -> NamePatFind)
-> (AnyName -> Either Integer Integer) -> NamePatFind
forall a b. (a -> b) -> a -> b
$ \(AnyName Name a
nm2) ->
    case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
nm1 of
      Just Name a
nm1' -> if Name a
nm1' Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name a
nm2 then Integer -> Either Integer Integer
forall a b. b -> Either a b
Right Integer
0 else Integer -> Either Integer Integer
forall a b. a -> Either a b
Left Integer
1
      Maybe (Name a)
Nothing -> Integer -> Either Integer Integer
forall a b. a -> Either a b
Left Integer
1

  swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a
swaps' AlphaCtx
ctx Perm AnyName
perm Name a
nm =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then case Perm AnyName -> AnyName -> AnyName
forall a. Ord a => Perm a -> a -> a
apply Perm AnyName
perm (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) of
      AnyName Name a
nm' ->
        case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
nm' of
          Just Name a
nm'' -> Name a
nm''
          Maybe (Name a)
Nothing -> [Char] -> Name a
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error swaps' on a Name returned permuted name of wrong sort"
    else Name a
nm
      
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Name a -> m (Name a, Perm AnyName)
freshen' AlphaCtx
ctx Name a
nm =
    if Bool -> Bool
not (AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx)
    then do
      Name a
nm' <- Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh Name a
nm
      (Name a, Perm AnyName) -> m (Name a, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name a
nm', AnyName -> AnyName -> Perm AnyName
forall a. Ord a => a -> a -> Perm a
single (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm'))
    else [Char] -> m (Name a, Perm AnyName)
forall a. HasCallStack => [Char] -> a
error [Char]
"freshen' on a Name in term position"

  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Name a -> (Name a -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx Name a
nm Name a -> Perm AnyName -> m b
cont =
    if Bool -> Bool
not (AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx)
    then do
      Name a
nm' <- Name a -> m (Name a)
forall a. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh Name a
nm
      [AnyName] -> m b -> m b
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid [Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm'] (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ Name a -> Perm AnyName -> m b
cont Name a
nm' (Perm AnyName -> m b) -> Perm AnyName -> m b
forall a b. (a -> b) -> a -> b
$ AnyName -> AnyName -> Perm AnyName
forall a. Ord a => a -> a -> Perm a
single (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm')
    else [Char] -> m b
forall a. HasCallStack => [Char] -> a
error [Char]
"lfreshen' on a Name in term position"

  acompare' :: AlphaCtx -> Name a -> Name a -> Ordering
acompare' AlphaCtx
ctx (Fn [Char]
s1 Integer
i1) (Fn [Char]
s2 Integer
i2)
    | AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx = ([Char] -> [Char] -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Char]
s1 [Char]
s2) Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> (Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
i1 Integer
i2)

  acompare' AlphaCtx
ctx n1 :: Name a
n1@(Bn Integer
i1 Integer
j1) n2 :: Name a
n2@(Bn Integer
i2 Integer
j2)
    | AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx = [Ordering] -> Ordering
forall a. Monoid a => [a] -> a
mconcat [ TypeRep -> TypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n1) (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n2)
                              , Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
i1 Integer
i2
                              , Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
j1 Integer
j2
                              ]

  acompare' AlphaCtx
ctx (Fn [Char]
_ Integer
_) (Bn Integer
_ Integer
_) | AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx = Ordering
LT
  acompare' AlphaCtx
ctx (Bn Integer
_ Integer
_) (Fn [Char]
_ Integer
_) | AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx = Ordering
GT

  acompare' AlphaCtx
_ Name a
_          Name a
_                        = Ordering
EQ

instance Alpha AnyName where
  aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool
aeq' AlphaCtx
ctx AnyName
x AnyName
y =
    if AnyName
x AnyName -> AnyName -> Bool
forall a. Eq a => a -> a -> Bool
== AnyName
y
    then Bool
True
    else
      -- in a term unequal variables are unequal, in a pattern it's
      -- ok.
      Bool -> Bool
not (AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx)

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> AnyName -> f AnyName
fvAny' AlphaCtx
ctx AnyName -> f AnyName
nfn n :: AnyName
n@(AnyName Name a
nm) = if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx Bool -> Bool -> Bool
&& Name a -> Bool
forall a. Name a -> Bool
isFreeName Name a
nm
                                  then AnyName -> f AnyName
nfn AnyName
n
                                  else AnyName -> f AnyName
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AnyName
n

  isTerm :: AnyName -> All
isTerm AnyName
_ = All
forall a. Monoid a => a
mempty

  isPat :: AnyName -> DisjointSet AnyName
isPat n :: AnyName
n@(AnyName Name a
nm) = if Name a -> Bool
forall a. Name a -> Bool
isFreeName Name a
nm
                         then AnyName -> DisjointSet AnyName
forall a. a -> DisjointSet a
singletonDisjointSet AnyName
n
                         else DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet

  swaps' :: AlphaCtx -> Perm AnyName -> AnyName -> AnyName
swaps' AlphaCtx
ctx Perm AnyName
perm AnyName
n =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then Perm AnyName -> AnyName -> AnyName
forall a. Ord a => Perm a -> a -> a
apply Perm AnyName
perm AnyName
n
    else AnyName
n

  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> AnyName -> m (AnyName, Perm AnyName)
freshen' AlphaCtx
ctx (AnyName Name a
nm) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then [Char] -> m (AnyName, Perm AnyName)
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.freshen' on AnyName in Term mode"
    else do
      Name a
nm' <- Name a -> m (Name a)
forall a. Name a -> m (Name a)
forall (m :: * -> *) a. Fresh m => Name a -> m (Name a)
fresh Name a
nm
      (AnyName, Perm AnyName) -> m (AnyName, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm', AnyName -> AnyName -> Perm AnyName
forall a. Ord a => a -> a -> Perm a
single (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm'))

  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> AnyName -> (AnyName -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx (AnyName Name a
nm) AnyName -> Perm AnyName -> m b
cont =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then [Char] -> m b
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.lfreshen' on AnyName in Term mode"
    else do
      Name a
nm' <- Name a -> m (Name a)
forall a. Typeable a => Name a -> m (Name a)
forall (m :: * -> *) a.
(LFresh m, Typeable a) =>
Name a -> m (Name a)
lfresh Name a
nm
      [AnyName] -> m b -> m b
forall a. [AnyName] -> m a -> m a
forall (m :: * -> *) a. LFresh m => [AnyName] -> m a -> m a
avoid [Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm'] (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ AnyName -> Perm AnyName -> m b
cont (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm') (Perm AnyName -> m b) -> Perm AnyName -> m b
forall a b. (a -> b) -> a -> b
$ AnyName -> AnyName -> Perm AnyName
forall a. Ord a => a -> a -> Perm a
single (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm) (Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName Name a
nm')

  open :: AlphaCtx -> NthPatFind -> AnyName -> AnyName
open AlphaCtx
ctx NthPatFind
b (AnyName Name a
nm) = Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName (AlphaCtx -> NthPatFind -> Name a -> Name a
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
ctx NthPatFind
b Name a
nm)

  close :: AlphaCtx -> NamePatFind -> AnyName -> AnyName
close AlphaCtx
ctx NamePatFind
b (AnyName Name a
nm) = Name a -> AnyName
forall a. Typeable a => Name a -> AnyName
AnyName (AlphaCtx -> NamePatFind -> Name a -> Name a
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close AlphaCtx
ctx NamePatFind
b Name a
nm)
    
  nthPatFind :: AnyName -> NthPatFind
nthPatFind AnyName
nm = (Integer -> Either Integer AnyName) -> NthPatFind
NthPatFind ((Integer -> Either Integer AnyName) -> NthPatFind)
-> (Integer -> Either Integer AnyName) -> NthPatFind
forall a b. (a -> b) -> a -> b
$ \Integer
i ->
    if Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then AnyName -> Either Integer AnyName
forall a b. b -> Either a b
Right AnyName
nm else Integer -> Either Integer AnyName
forall a b. a -> Either a b
Left (Integer -> Either Integer AnyName)
-> Integer -> Either Integer AnyName
forall a b. (a -> b) -> a -> b
$! Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

  namePatFind :: AnyName -> NamePatFind
namePatFind AnyName
nmHave = (AnyName -> Either Integer Integer) -> NamePatFind
NamePatFind ((AnyName -> Either Integer Integer) -> NamePatFind)
-> (AnyName -> Either Integer Integer) -> NamePatFind
forall a b. (a -> b) -> a -> b
$ \AnyName
nmWant ->
    if AnyName
nmHave AnyName -> AnyName -> Bool
forall a. Eq a => a -> a -> Bool
== AnyName
nmWant then Integer -> Either Integer Integer
forall a b. b -> Either a b
Right Integer
0 else Integer -> Either Integer Integer
forall a b. a -> Either a b
Left Integer
1

  acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering
acompare' AlphaCtx
_ AnyName
x AnyName
y | AnyName
x AnyName -> AnyName -> Bool
forall a. Eq a => a -> a -> Bool
== AnyName
y = Ordering
EQ

  acompare' AlphaCtx
ctx (AnyName Name a
n1) (AnyName Name a
n2)
    | AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx =
      case TypeRep -> TypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n1) (Name a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf Name a
n2) of
        Ordering
EQ -> case Name a -> Maybe (Name a)
forall {k} (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast Name a
n2 of
          Just Name a
n2' -> AlphaCtx -> Name a -> Name a -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
ctx Name a
n1 Name a
n2'
          Maybe (Name a)
Nothing -> [Char] -> Ordering
forall a. HasCallStack => [Char] -> a
error [Char]
"LocallyNameless.acompare': Equal type representations, but gcast failed in comparing two AnyName values"
        Ordering
ord -> Ordering
ord

  acompare' AlphaCtx
_ AnyName
_ AnyName
_ = Ordering
EQ