{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE OverloadedStrings #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- SPDX-License-Identifier: BSD-3-Clause

-- |
-- Module      :  Disco.Names
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- Names for modules and identifiers.
module Disco.Names (
  -- * Modules and their provenance
  ModuleProvenance (..),
  ModuleName (..),

  -- * Names and their provenance
  NameProvenance (..),
  QName (..),
  isFree,
  localName,
  (.-),

  -- * Name-related utilities
  fvQ,
  substQ,
  substsQ,
) where

import Control.Lens (Traversal', filtered)
import Data.Data (Data)
import Data.Data.Lens (template)
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import System.FilePath (dropExtension)
import Unbound.Generics.LocallyNameless
import Prelude hiding ((<>))

import Disco.Pretty
import Disco.Types

------------------------------------------------------------
-- Modules
------------------------------------------------------------

-- | Where did a module come from?
data ModuleProvenance
  = -- | From a particular directory (relative to cwd)
    Dir FilePath
  | -- | From the standard library
    Stdlib
  deriving (ModuleProvenance -> ModuleProvenance -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleProvenance -> ModuleProvenance -> Bool
$c/= :: ModuleProvenance -> ModuleProvenance -> Bool
== :: ModuleProvenance -> ModuleProvenance -> Bool
$c== :: ModuleProvenance -> ModuleProvenance -> Bool
Eq, Eq ModuleProvenance
ModuleProvenance -> ModuleProvenance -> Bool
ModuleProvenance -> ModuleProvenance -> Ordering
ModuleProvenance -> ModuleProvenance -> ModuleProvenance
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ModuleProvenance -> ModuleProvenance -> ModuleProvenance
$cmin :: ModuleProvenance -> ModuleProvenance -> ModuleProvenance
max :: ModuleProvenance -> ModuleProvenance -> ModuleProvenance
$cmax :: ModuleProvenance -> ModuleProvenance -> ModuleProvenance
>= :: ModuleProvenance -> ModuleProvenance -> Bool
$c>= :: ModuleProvenance -> ModuleProvenance -> Bool
> :: ModuleProvenance -> ModuleProvenance -> Bool
$c> :: ModuleProvenance -> ModuleProvenance -> Bool
<= :: ModuleProvenance -> ModuleProvenance -> Bool
$c<= :: ModuleProvenance -> ModuleProvenance -> Bool
< :: ModuleProvenance -> ModuleProvenance -> Bool
$c< :: ModuleProvenance -> ModuleProvenance -> Bool
compare :: ModuleProvenance -> ModuleProvenance -> Ordering
$ccompare :: ModuleProvenance -> ModuleProvenance -> Ordering
Ord, Int -> ModuleProvenance -> ShowS
[ModuleProvenance] -> ShowS
ModuleProvenance -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleProvenance] -> ShowS
$cshowList :: [ModuleProvenance] -> ShowS
show :: ModuleProvenance -> String
$cshow :: ModuleProvenance -> String
showsPrec :: Int -> ModuleProvenance -> ShowS
$cshowsPrec :: Int -> ModuleProvenance -> ShowS
Show, forall x. Rep ModuleProvenance x -> ModuleProvenance
forall x. ModuleProvenance -> Rep ModuleProvenance x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModuleProvenance x -> ModuleProvenance
$cfrom :: forall x. ModuleProvenance -> Rep ModuleProvenance x
Generic, Typeable ModuleProvenance
ModuleProvenance -> DataType
ModuleProvenance -> Constr
(forall b. Data b => b -> b)
-> ModuleProvenance -> ModuleProvenance
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ModuleProvenance -> u
forall u. (forall d. Data d => d -> u) -> ModuleProvenance -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleProvenance
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleProvenance -> c ModuleProvenance
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleProvenance)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ModuleProvenance)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ModuleProvenance -> m ModuleProvenance
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ModuleProvenance -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ModuleProvenance -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ModuleProvenance -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ModuleProvenance -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleProvenance -> r
gmapT :: (forall b. Data b => b -> b)
-> ModuleProvenance -> ModuleProvenance
$cgmapT :: (forall b. Data b => b -> b)
-> ModuleProvenance -> ModuleProvenance
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ModuleProvenance)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ModuleProvenance)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleProvenance)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleProvenance)
dataTypeOf :: ModuleProvenance -> DataType
$cdataTypeOf :: ModuleProvenance -> DataType
toConstr :: ModuleProvenance -> Constr
$ctoConstr :: ModuleProvenance -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleProvenance
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleProvenance
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleProvenance -> c ModuleProvenance
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleProvenance -> c ModuleProvenance
Data, Show ModuleProvenance
AlphaCtx -> NthPatFind -> ModuleProvenance -> ModuleProvenance
AlphaCtx -> NamePatFind -> ModuleProvenance -> ModuleProvenance
AlphaCtx -> Perm AnyName -> ModuleProvenance -> ModuleProvenance
AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Bool
AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Ordering
ModuleProvenance -> Bool
ModuleProvenance -> All
ModuleProvenance -> DisjointSet AnyName
ModuleProvenance -> NthPatFind
ModuleProvenance -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> ModuleProvenance -> f ModuleProvenance
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleProvenance -> m (ModuleProvenance, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleProvenance
-> (ModuleProvenance -> Perm AnyName -> m b)
-> m b
acompare' :: AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Ordering
$cacompare' :: AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleProvenance -> m (ModuleProvenance, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleProvenance -> m (ModuleProvenance, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleProvenance
-> (ModuleProvenance -> Perm AnyName -> m b)
-> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleProvenance
-> (ModuleProvenance -> Perm AnyName -> m b)
-> m b
swaps' :: AlphaCtx -> Perm AnyName -> ModuleProvenance -> ModuleProvenance
$cswaps' :: AlphaCtx -> Perm AnyName -> ModuleProvenance -> ModuleProvenance
namePatFind :: ModuleProvenance -> NamePatFind
$cnamePatFind :: ModuleProvenance -> NamePatFind
nthPatFind :: ModuleProvenance -> NthPatFind
$cnthPatFind :: ModuleProvenance -> NthPatFind
isEmbed :: ModuleProvenance -> Bool
$cisEmbed :: ModuleProvenance -> Bool
isTerm :: ModuleProvenance -> All
$cisTerm :: ModuleProvenance -> All
isPat :: ModuleProvenance -> DisjointSet AnyName
$cisPat :: ModuleProvenance -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> ModuleProvenance -> ModuleProvenance
$copen :: AlphaCtx -> NthPatFind -> ModuleProvenance -> ModuleProvenance
close :: AlphaCtx -> NamePatFind -> ModuleProvenance -> ModuleProvenance
$cclose :: AlphaCtx -> NamePatFind -> ModuleProvenance -> ModuleProvenance
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> ModuleProvenance -> f ModuleProvenance
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> ModuleProvenance -> f ModuleProvenance
aeq' :: AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Bool
$caeq' :: AlphaCtx -> ModuleProvenance -> ModuleProvenance -> Bool
Alpha, Subst Type)

-- | The name of a module.
data ModuleName
  = -- | The special top-level "module" consisting of
    -- what has been entered at the REPL.
    REPLModule
  | -- | A named module, with its name and provenance.
    Named ModuleProvenance String
  deriving (ModuleName -> ModuleName -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ModuleName -> ModuleName -> Bool
$c/= :: ModuleName -> ModuleName -> Bool
== :: ModuleName -> ModuleName -> Bool
$c== :: ModuleName -> ModuleName -> Bool
Eq, Eq ModuleName
ModuleName -> ModuleName -> Bool
ModuleName -> ModuleName -> Ordering
ModuleName -> ModuleName -> ModuleName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ModuleName -> ModuleName -> ModuleName
$cmin :: ModuleName -> ModuleName -> ModuleName
max :: ModuleName -> ModuleName -> ModuleName
$cmax :: ModuleName -> ModuleName -> ModuleName
>= :: ModuleName -> ModuleName -> Bool
$c>= :: ModuleName -> ModuleName -> Bool
> :: ModuleName -> ModuleName -> Bool
$c> :: ModuleName -> ModuleName -> Bool
<= :: ModuleName -> ModuleName -> Bool
$c<= :: ModuleName -> ModuleName -> Bool
< :: ModuleName -> ModuleName -> Bool
$c< :: ModuleName -> ModuleName -> Bool
compare :: ModuleName -> ModuleName -> Ordering
$ccompare :: ModuleName -> ModuleName -> Ordering
Ord, Int -> ModuleName -> ShowS
[ModuleName] -> ShowS
ModuleName -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleName] -> ShowS
$cshowList :: [ModuleName] -> ShowS
show :: ModuleName -> String
$cshow :: ModuleName -> String
showsPrec :: Int -> ModuleName -> ShowS
$cshowsPrec :: Int -> ModuleName -> ShowS
Show, forall x. Rep ModuleName x -> ModuleName
forall x. ModuleName -> Rep ModuleName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ModuleName x -> ModuleName
$cfrom :: forall x. ModuleName -> Rep ModuleName x
Generic, Typeable ModuleName
ModuleName -> DataType
ModuleName -> Constr
(forall b. Data b => b -> b) -> ModuleName -> ModuleName
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> ModuleName -> u
forall u. (forall d. Data d => d -> u) -> ModuleName -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleName
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleName -> c ModuleName
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleName)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleName)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ModuleName -> m ModuleName
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ModuleName -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ModuleName -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ModuleName -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ModuleName -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ModuleName -> r
gmapT :: (forall b. Data b => b -> b) -> ModuleName -> ModuleName
$cgmapT :: (forall b. Data b => b -> b) -> ModuleName -> ModuleName
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleName)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModuleName)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleName)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ModuleName)
dataTypeOf :: ModuleName -> DataType
$cdataTypeOf :: ModuleName -> DataType
toConstr :: ModuleName -> Constr
$ctoConstr :: ModuleName -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleName
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ModuleName
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleName -> c ModuleName
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ModuleName -> c ModuleName
Data, Show ModuleName
AlphaCtx -> NthPatFind -> ModuleName -> ModuleName
AlphaCtx -> NamePatFind -> ModuleName -> ModuleName
AlphaCtx -> Perm AnyName -> ModuleName -> ModuleName
AlphaCtx -> ModuleName -> ModuleName -> Bool
AlphaCtx -> ModuleName -> ModuleName -> Ordering
ModuleName -> Bool
ModuleName -> All
ModuleName -> DisjointSet AnyName
ModuleName -> NthPatFind
ModuleName -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> ModuleName -> f ModuleName
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleName -> m (ModuleName, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleName -> (ModuleName -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> ModuleName -> ModuleName -> Ordering
$cacompare' :: AlphaCtx -> ModuleName -> ModuleName -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleName -> m (ModuleName, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> ModuleName -> m (ModuleName, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleName -> (ModuleName -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> ModuleName -> (ModuleName -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> ModuleName -> ModuleName
$cswaps' :: AlphaCtx -> Perm AnyName -> ModuleName -> ModuleName
namePatFind :: ModuleName -> NamePatFind
$cnamePatFind :: ModuleName -> NamePatFind
nthPatFind :: ModuleName -> NthPatFind
$cnthPatFind :: ModuleName -> NthPatFind
isEmbed :: ModuleName -> Bool
$cisEmbed :: ModuleName -> Bool
isTerm :: ModuleName -> All
$cisTerm :: ModuleName -> All
isPat :: ModuleName -> DisjointSet AnyName
$cisPat :: ModuleName -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> ModuleName -> ModuleName
$copen :: AlphaCtx -> NthPatFind -> ModuleName -> ModuleName
close :: AlphaCtx -> NamePatFind -> ModuleName -> ModuleName
$cclose :: AlphaCtx -> NamePatFind -> ModuleName -> ModuleName
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> ModuleName -> f ModuleName
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> ModuleName -> f ModuleName
aeq' :: AlphaCtx -> ModuleName -> ModuleName -> Bool
$caeq' :: AlphaCtx -> ModuleName -> ModuleName -> Bool
Alpha, Subst Type)

------------------------------------------------------------
-- Names
------------------------------------------------------------

-- | Where did a name come from?
data NameProvenance
  = -- | The name is locally bound
    LocalName
  | -- | The name is exported by the given module
    QualifiedName ModuleName
  deriving (NameProvenance -> NameProvenance -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NameProvenance -> NameProvenance -> Bool
$c/= :: NameProvenance -> NameProvenance -> Bool
== :: NameProvenance -> NameProvenance -> Bool
$c== :: NameProvenance -> NameProvenance -> Bool
Eq, Eq NameProvenance
NameProvenance -> NameProvenance -> Bool
NameProvenance -> NameProvenance -> Ordering
NameProvenance -> NameProvenance -> NameProvenance
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NameProvenance -> NameProvenance -> NameProvenance
$cmin :: NameProvenance -> NameProvenance -> NameProvenance
max :: NameProvenance -> NameProvenance -> NameProvenance
$cmax :: NameProvenance -> NameProvenance -> NameProvenance
>= :: NameProvenance -> NameProvenance -> Bool
$c>= :: NameProvenance -> NameProvenance -> Bool
> :: NameProvenance -> NameProvenance -> Bool
$c> :: NameProvenance -> NameProvenance -> Bool
<= :: NameProvenance -> NameProvenance -> Bool
$c<= :: NameProvenance -> NameProvenance -> Bool
< :: NameProvenance -> NameProvenance -> Bool
$c< :: NameProvenance -> NameProvenance -> Bool
compare :: NameProvenance -> NameProvenance -> Ordering
$ccompare :: NameProvenance -> NameProvenance -> Ordering
Ord, Int -> NameProvenance -> ShowS
[NameProvenance] -> ShowS
NameProvenance -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameProvenance] -> ShowS
$cshowList :: [NameProvenance] -> ShowS
show :: NameProvenance -> String
$cshow :: NameProvenance -> String
showsPrec :: Int -> NameProvenance -> ShowS
$cshowsPrec :: Int -> NameProvenance -> ShowS
Show, forall x. Rep NameProvenance x -> NameProvenance
forall x. NameProvenance -> Rep NameProvenance x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NameProvenance x -> NameProvenance
$cfrom :: forall x. NameProvenance -> Rep NameProvenance x
Generic, Typeable NameProvenance
NameProvenance -> DataType
NameProvenance -> Constr
(forall b. Data b => b -> b) -> NameProvenance -> NameProvenance
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> NameProvenance -> u
forall u. (forall d. Data d => d -> u) -> NameProvenance -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameProvenance
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameProvenance -> c NameProvenance
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NameProvenance)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameProvenance)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> NameProvenance -> m NameProvenance
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> NameProvenance -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> NameProvenance -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> NameProvenance -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> NameProvenance -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NameProvenance -> r
gmapT :: (forall b. Data b => b -> b) -> NameProvenance -> NameProvenance
$cgmapT :: (forall b. Data b => b -> b) -> NameProvenance -> NameProvenance
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameProvenance)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c NameProvenance)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NameProvenance)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c NameProvenance)
dataTypeOf :: NameProvenance -> DataType
$cdataTypeOf :: NameProvenance -> DataType
toConstr :: NameProvenance -> Constr
$ctoConstr :: NameProvenance -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameProvenance
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c NameProvenance
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameProvenance -> c NameProvenance
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NameProvenance -> c NameProvenance
Data, Show NameProvenance
AlphaCtx -> NthPatFind -> NameProvenance -> NameProvenance
AlphaCtx -> NamePatFind -> NameProvenance -> NameProvenance
AlphaCtx -> Perm AnyName -> NameProvenance -> NameProvenance
AlphaCtx -> NameProvenance -> NameProvenance -> Bool
AlphaCtx -> NameProvenance -> NameProvenance -> Ordering
NameProvenance -> Bool
NameProvenance -> All
NameProvenance -> DisjointSet AnyName
NameProvenance -> NthPatFind
NameProvenance -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> NameProvenance -> f NameProvenance
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> NameProvenance -> m (NameProvenance, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> NameProvenance -> (NameProvenance -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> NameProvenance -> NameProvenance -> Ordering
$cacompare' :: AlphaCtx -> NameProvenance -> NameProvenance -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> NameProvenance -> m (NameProvenance, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> NameProvenance -> m (NameProvenance, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> NameProvenance -> (NameProvenance -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> NameProvenance -> (NameProvenance -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> NameProvenance -> NameProvenance
$cswaps' :: AlphaCtx -> Perm AnyName -> NameProvenance -> NameProvenance
namePatFind :: NameProvenance -> NamePatFind
$cnamePatFind :: NameProvenance -> NamePatFind
nthPatFind :: NameProvenance -> NthPatFind
$cnthPatFind :: NameProvenance -> NthPatFind
isEmbed :: NameProvenance -> Bool
$cisEmbed :: NameProvenance -> Bool
isTerm :: NameProvenance -> All
$cisTerm :: NameProvenance -> All
isPat :: NameProvenance -> DisjointSet AnyName
$cisPat :: NameProvenance -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> NameProvenance -> NameProvenance
$copen :: AlphaCtx -> NthPatFind -> NameProvenance -> NameProvenance
close :: AlphaCtx -> NamePatFind -> NameProvenance -> NameProvenance
$cclose :: AlphaCtx -> NamePatFind -> NameProvenance -> NameProvenance
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> NameProvenance -> f NameProvenance
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> NameProvenance -> f NameProvenance
aeq' :: AlphaCtx -> NameProvenance -> NameProvenance -> Bool
$caeq' :: AlphaCtx -> NameProvenance -> NameProvenance -> Bool
Alpha, Subst Type)

-- | A @QName@, or qualified name, is a 'Name' paired with its
--   'NameProvenance'.
data QName a = QName {forall a. QName a -> NameProvenance
qnameProvenance :: NameProvenance, forall a. QName a -> Name a
qname :: Name a}
  deriving (QName a -> QName a -> Bool
forall a. QName a -> QName a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: QName a -> QName a -> Bool
$c/= :: forall a. QName a -> QName a -> Bool
== :: QName a -> QName a -> Bool
$c== :: forall a. QName a -> QName a -> Bool
Eq, QName a -> QName a -> Bool
QName a -> QName a -> Ordering
forall a. Eq (QName a)
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. QName a -> QName a -> Bool
forall a. QName a -> QName a -> Ordering
forall a. QName a -> QName a -> QName a
min :: QName a -> QName a -> QName a
$cmin :: forall a. QName a -> QName a -> QName a
max :: QName a -> QName a -> QName a
$cmax :: forall a. QName a -> QName a -> QName a
>= :: QName a -> QName a -> Bool
$c>= :: forall a. QName a -> QName a -> Bool
> :: QName a -> QName a -> Bool
$c> :: forall a. QName a -> QName a -> Bool
<= :: QName a -> QName a -> Bool
$c<= :: forall a. QName a -> QName a -> Bool
< :: QName a -> QName a -> Bool
$c< :: forall a. QName a -> QName a -> Bool
compare :: QName a -> QName a -> Ordering
$ccompare :: forall a. QName a -> QName a -> Ordering
Ord, Int -> QName a -> ShowS
forall a. Int -> QName a -> ShowS
forall a. [QName a] -> ShowS
forall a. QName a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [QName a] -> ShowS
$cshowList :: forall a. [QName a] -> ShowS
show :: QName a -> String
$cshow :: forall a. QName a -> String
showsPrec :: Int -> QName a -> ShowS
$cshowsPrec :: forall a. Int -> QName a -> ShowS
Show, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (QName a) x -> QName a
forall a x. QName a -> Rep (QName a) x
$cto :: forall a x. Rep (QName a) x -> QName a
$cfrom :: forall a x. QName a -> Rep (QName a) x
Generic, QName a -> DataType
QName a -> Constr
forall {a}. Data a => Typeable (QName a)
forall a. Data a => QName a -> DataType
forall a. Data a => QName a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> QName a -> QName a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> QName a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> QName a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QName a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName a -> c (QName a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QName a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QName a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QName a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName a -> c (QName a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QName a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> QName a -> m (QName a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> QName a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> QName a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> QName a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> QName a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> QName a -> r
gmapT :: (forall b. Data b => b -> b) -> QName a -> QName a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> QName a -> QName a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QName a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (QName a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (QName a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (QName a))
dataTypeOf :: QName a -> DataType
$cdataTypeOf :: forall a. Data a => QName a -> DataType
toConstr :: QName a -> Constr
$ctoConstr :: forall a. Data a => QName a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QName a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (QName a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName a -> c (QName a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> QName a -> c (QName a)
Data, forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall {a}. Typeable a => Show (QName a)
forall a.
Typeable a =>
AlphaCtx -> NthPatFind -> QName a -> QName a
forall a.
Typeable a =>
AlphaCtx -> NamePatFind -> QName a -> QName a
forall a.
Typeable a =>
AlphaCtx -> Perm AnyName -> QName a -> QName a
forall a. Typeable a => AlphaCtx -> QName a -> QName a -> Bool
forall a. Typeable a => AlphaCtx -> QName a -> QName a -> Ordering
forall a. Typeable a => QName a -> Bool
forall a. Typeable a => QName a -> All
forall a. Typeable a => QName a -> DisjointSet AnyName
forall a. Typeable a => QName a -> NthPatFind
forall a. Typeable a => QName a -> NamePatFind
forall a (f :: * -> *).
(Typeable a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> QName a -> f (QName a)
forall a (m :: * -> *).
(Typeable a, Fresh m) =>
AlphaCtx -> QName a -> m (QName a, Perm AnyName)
forall a (m :: * -> *) b.
(Typeable a, LFresh m) =>
AlphaCtx -> QName a -> (QName a -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> QName a -> QName a -> Ordering
$cacompare' :: forall a. Typeable a => AlphaCtx -> QName a -> QName a -> Ordering
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> QName a -> m (QName a, Perm AnyName)
$cfreshen' :: forall a (m :: * -> *).
(Typeable a, Fresh m) =>
AlphaCtx -> QName a -> m (QName a, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> QName a -> (QName a -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall a (m :: * -> *) b.
(Typeable a, LFresh m) =>
AlphaCtx -> QName a -> (QName a -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> QName a -> QName a
$cswaps' :: forall a.
Typeable a =>
AlphaCtx -> Perm AnyName -> QName a -> QName a
namePatFind :: QName a -> NamePatFind
$cnamePatFind :: forall a. Typeable a => QName a -> NamePatFind
nthPatFind :: QName a -> NthPatFind
$cnthPatFind :: forall a. Typeable a => QName a -> NthPatFind
isEmbed :: QName a -> Bool
$cisEmbed :: forall a. Typeable a => QName a -> Bool
isTerm :: QName a -> All
$cisTerm :: forall a. Typeable a => QName a -> All
isPat :: QName a -> DisjointSet AnyName
$cisPat :: forall a. Typeable a => QName a -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> QName a -> QName a
$copen :: forall a.
Typeable a =>
AlphaCtx -> NthPatFind -> QName a -> QName a
close :: AlphaCtx -> NamePatFind -> QName a -> QName a
$cclose :: forall a.
Typeable a =>
AlphaCtx -> NamePatFind -> QName a -> QName a
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> QName a -> f (QName a)
$cfvAny' :: forall a (f :: * -> *).
(Typeable a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> QName a -> f (QName a)
aeq' :: AlphaCtx -> QName a -> QName a -> Bool
$caeq' :: forall a. Typeable a => AlphaCtx -> QName a -> QName a -> Bool
Alpha, Subst Type)

-- | Does this name correspond to a free variable?
isFree :: QName a -> Bool
isFree :: forall a. QName a -> Bool
isFree (QName (QualifiedName ModuleName
_) Name a
_) = Bool
True
isFree (QName NameProvenance
LocalName Name a
n) = forall a. Name a -> Bool
isFreeName Name a
n

-- | Create a locally bound qualified name.
localName :: Name a -> QName a
localName :: forall a. Name a -> QName a
localName = forall a. NameProvenance -> Name a -> QName a
QName NameProvenance
LocalName

-- | Create a module-bound qualified name.
(.-) :: ModuleName -> Name a -> QName a
ModuleName
m .- :: forall a. ModuleName -> Name a -> QName a
.- Name a
x = forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
m) Name a
x

------------------------------------------------------------
-- Free variables and substitution
------------------------------------------------------------

-- | The @unbound-generics@ library gives us free variables for free.
--   But when dealing with typed and desugared ASTs, we want all the
--   free 'QName's instead of just 'Name's.
fvQ :: (Data t, Typeable e) => Traversal' t (QName e)
fvQ :: forall t e. (Data t, Typeable e) => Traversal' t (QName e)
fvQ = forall s a. (Data s, Typeable a) => Traversal' s a
template forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) (f :: * -> *) a.
(Choice p, Applicative f) =>
(a -> Bool) -> Optic' p f a a
filtered forall a. QName a -> Bool
isFree

substQ :: Subst b a => QName b -> b -> a -> a
substQ :: forall b a. Subst b a => QName b -> b -> a -> a
substQ = forall a. HasCallStack => a
undefined

substsQ :: Subst b a => [(QName b, b)] -> a -> a
substsQ :: forall b a. Subst b a => [(QName b, b)] -> a -> a
substsQ = forall a. HasCallStack => a
undefined

------------------------------------------------------------
-- Pretty-printing
------------------------------------------------------------

instance Pretty ModuleName where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
ModuleName -> Sem r (Doc ann)
pretty ModuleName
REPLModule = Sem r (Doc ann)
"REPL"
  pretty (Named (Dir String
_) String
s) = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (ShowS
dropExtension String
s)
  pretty (Named ModuleProvenance
Stdlib String
s) = forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
text (ShowS
dropExtension String
s)

instance Pretty (QName a) where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
QName a -> Sem r (Doc ann)
pretty (QName NameProvenance
LocalName Name a
x) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name a
x
  pretty (QName (QualifiedName ModuleName
mn) Name a
x) = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ModuleName
mn forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> Sem r (Doc ann)
"." forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<> forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty Name a
x