Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution

Contents

Names
Individual Variable Types
Combined Variable Types
Variable Lens Classes
De Bruijn, Named and Global and Substitutions
Metavar Substitutions
Substy Interface

Synopsis

data Name = Name {
- nameMark :: 𝑂 ℕ64
- nameName :: 𝕊
}
nameMarkL :: Name ⟢ 𝑂 ℕ64
nameNameL :: Name ⟢ 𝕊
mkName :: 𝕊 -> Name
gensymName :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m Name
syntaxName :: LexerBasicSyntax
pName :: CParser TokenBasic Name
pNameWS :: CParser TokenWSBasic Name
newtype DVar = DVar {
- unDVar :: ℕ64
}
unDVarL :: DVar ⟢ ℕ64
syntaxDVar :: LexerBasicSyntax
pDVarTail :: CParser TokenBasic DVar
pDVar :: CParser TokenBasic DVar
data NVar = NVar {
- nvarIndex :: DVar
- nvarName :: Name
}
nvarIndexL :: NVar ⟢ DVar
nvarNameL :: NVar ⟢ Name
nvar_Name :: Name -> NVar
name_NVarL :: NVar ⌲ Name
gensymNVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m NVar
syntaxNVar :: LexerBasicSyntax
pNVarTail :: Name -> CParser TokenBasic NVar
pNVar :: CParser TokenBasic NVar
newtype GVar = GVar {
- unGVar :: Name
}
unGVarL :: GVar ⟢ Name
syntaxGVar :: LexerBasicSyntax
pGVarTail :: Name -> CParser TokenBasic GVar
pGVar :: CParser TokenBasic GVar
data MVar s e = MVar {
- mvarSubst :: Subst s e
- mvarName :: Name
}
mvarSubstL :: MVar s e ⟢ Subst s e
mvarNameL :: MVar s e ⟢ Name
wfMVar :: Ord s => MVar s e -> 𝔹
canonMVar :: (Ord s, Eq e, Substy s e e) => (e -> e) -> MVar s e -> MVar s e
substMVar :: (Ord s, Substy s e e) => Subst s e -> MVar s e -> MVar s e
syntaxMVar :: LexerBasicSyntax
pMVarTail :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> Name -> CParser TokenBasic (MVar () e)
pMVar :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (MVar () e)
data SVar
- = D_SVar DVar
- | N_SVar NVar
d_SVarL :: SVar ⌲ DVar
n_SVarL :: SVar ⌲ NVar
mkSVar :: SName -> DVar -> SVar
svarName :: SVar -> SName
svarLevel :: SVar -> DVar
svar_Name :: Name -> SVar
data Var
- = D_Var DVar
- | N_Var NVar
- | G_Var GVar
d_VarL :: Var ⌲ DVar
n_VarL :: Var ⌲ NVar
g_VarL :: Var ⌲ GVar
var_Name :: Name -> Var
var_SVar :: SVar -> Var
name_VarL :: Var ⌲ Name
gensymVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m Var
syntaxVar :: LexerBasicSyntax
pVar :: CParser TokenBasic Var
data UVar s e
- = D_UVar DVar
- | N_UVar NVar
- | G_UVar GVar
- | M_UVar (MVar s e)
d_UVarL :: UVar s e ⌲ DVar
n_UVarL :: UVar s e ⌲ NVar
g_UVarL :: UVar s e ⌲ GVar
m_UVarL :: UVar s e ⌲ MVar s e
name_UVarL :: UVar s e ⌲ Name
uvar_Name :: Name -> UVar s e
uvar_SVar :: SVar -> UVar s e
svar_UVarL :: UVar s e ⌲ SVar
uvar_Var :: Var -> UVar s e
var_UVarL :: UVar s e ⌲ Var
gensymUVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m (UVar s e)
wfUVar :: Ord s => UVar s e -> 𝔹
canonUVar :: (Ord s, Eq e, Substy s e e) => (e -> e) -> UVar s e -> UVar s e
syntaxUVar :: LexerBasicSyntax
pUVar :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (UVar () e)
class SVarView s e | e -> s where
- svarL :: s -> e ⌲ SVar
svarScopeL :: SVarView s e => s -> SName -> e ⌲ DVar
data Subst s e
isNullSubst :: Ord s => Subst s e -> 𝔹
wfSubst :: Ord s => Subst s e -> 𝔹
canonSubst :: (Ord s, Eq e, Substy s e e) => (e -> e) -> Subst s e -> Subst s e
syntaxSubst :: LexerBasicSyntax
pSubst :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e)
dshiftsSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e
dshiftSubst :: Ord s => s -> ℕ64 -> Subst s e -> Subst s e
dintrosSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e
dintroSubst :: Ord s => s -> ℕ64 -> Subst s e
dbindsSubst :: Ord s => (s ⇰ 𝕍 e) -> Subst s e
dbindSubst :: Ord s => s -> e -> Subst s e
nshiftsSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e
nshiftSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e -> Subst s e
nintrosSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e
nintroSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e
nbindsSubst :: Ord s => (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e
nbindSubst :: Ord s => s -> Name -> e -> Subst s e
gbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> Subst s e
gbindSubst :: Ord s => s -> Name -> e -> Subst s e
data MetaSubst s e
mbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> MetaSubst s e
mbindSubst :: Ord s => s -> Name -> e -> MetaSubst s e
data SubstyM s e a
class SVarView s e => Substy s e a | a -> e, e -> s where
- substy :: a -> SubstyM s e a
substyDBdr :: (Ord s, Ord e) => s -> SubstyM s e ()
substyNBdr :: (Ord s, Ord e) => s -> Name -> SubstyM s e ()
substyBdr :: (Ord s, Ord e, Substy s e e) => s -> (SVar -> e) -> Name -> SubstyM s e ()
substyDVar :: (Ord s, Ord e, Substy s e e) => (DVar -> e) -> s -> DVar -> SubstyM s e e
substyNVar :: (Ord s, Ord e, Substy s e e) => (NVar -> e) -> s -> NVar -> SubstyM s e e
substyGVar :: (Ord s, Ord e, Substy s e e) => (GVar -> e) -> s -> GVar -> SubstyM s e e
substySVar :: (Ord s, Ord e, Substy s e e) => (SVar -> e) -> s -> SVar -> SubstyM s e e
substyVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (Var -> e) -> s -> Var -> SubstyM s e e
substyMVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (MVar s e -> e) -> s -> MVar s e -> SubstyM s e e
substyUVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (UVar s e -> e) -> s -> UVar s e -> SubstyM s e e
fvssWith :: Substy s e a => (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e)
fvsWith :: (Ord s, Substy s e a) => s -> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e)
fvss :: Substy s e a => a -> s ⇰ 𝑃 (UVar s e)
fvs :: (Ord s, Substy s e a) => s -> a -> 𝑃 (UVar s e)
fvssMetas :: (Ord s, Ord e, Substy s e a) => a -> s ⇰ 𝑃 (MVar s e)
fvsMetas :: (Ord s, Ord e, Substy s e a) => s -> a -> 𝑃 (MVar s e)
todbr :: Substy s e a => a -> 𝑂 a
tonmd :: Substy s e a => a -> 𝑂 a
subst :: Substy s e a => Subst s e -> a -> 𝑂 a
msubst :: Substy s e a => MetaSubst s e -> a -> 𝑂 a

Names

data Name Source #

Constructors

Name
Fields nameMark :: 𝑂 ℕ64 nameName :: 𝕊

Instances

Instances details

Show Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
Eq Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods compare :: Name -> Name -> Ordering # (<) :: Name -> Name -> Bool # (<=) :: Name -> Name -> Bool # (>) :: Name -> Name -> Bool # (>=) :: Name -> Name -> Bool # max :: Name -> Name -> Name # min :: Name -> Name -> Name #
Fuzzy Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods fuzzy :: FuzzyM Name Source #
Pretty Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods pretty :: Name -> Doc Source #
Shrinky Name Source #
Instance details Defined in UVMHS.Lib.Substitution.Name Methods shrink :: Name -> 𝐼 Name Source #
Lift Name Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => Name -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Name -> Code m Name #

nameMarkL :: Name ⟢ 𝑂 ℕ64 Source #

nameNameL :: Name ⟢ 𝕊 Source #

mkName :: 𝕊 -> Name Source #

gensymName :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m Name Source #

syntaxName :: LexerBasicSyntax Source #

pName :: CParser TokenBasic Name Source #

pNameWS :: CParser TokenWSBasic Name Source #

Individual Variable Types

newtype DVar Source #

Constructors

DVar
Fields unDVar :: ℕ64

Instances

Instances details

Show DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> DVar -> ShowS # show :: DVar -> String # showList :: [DVar] -> ShowS #
Eq DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: DVar -> DVar -> Bool # (/=) :: DVar -> DVar -> Bool #
Ord DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: DVar -> DVar -> Ordering # (<) :: DVar -> DVar -> Bool # (<=) :: DVar -> DVar -> Bool # (>) :: DVar -> DVar -> Bool # (>=) :: DVar -> DVar -> Bool # max :: DVar -> DVar -> DVar # min :: DVar -> DVar -> DVar #
Fuzzy DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods fuzzy :: FuzzyM DVar Source #
Pretty DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: DVar -> Doc Source #
Shrinky DVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods shrink :: DVar -> 𝐼 DVar Source #
Lift DVar Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => DVar -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => DVar -> Code m DVar #

unDVarL :: DVar ⟢ ℕ64 Source #

syntaxDVar :: LexerBasicSyntax Source #

pDVarTail :: CParser TokenBasic DVar Source #

pDVar :: CParser TokenBasic DVar Source #

data NVar Source #

Constructors

NVar
Fields nvarIndex :: DVar nvarName :: Name

Instances

Instances details

Show NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> NVar -> ShowS # show :: NVar -> String # showList :: [NVar] -> ShowS #
Eq NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: NVar -> NVar -> Bool # (/=) :: NVar -> NVar -> Bool #
Ord NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: NVar -> NVar -> Ordering # (<) :: NVar -> NVar -> Bool # (<=) :: NVar -> NVar -> Bool # (>) :: NVar -> NVar -> Bool # (>=) :: NVar -> NVar -> Bool # max :: NVar -> NVar -> NVar # min :: NVar -> NVar -> NVar #
Fuzzy NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods fuzzy :: FuzzyM NVar Source #
Pretty NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: NVar -> Doc Source #
Shrinky NVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods shrink :: NVar -> 𝐼 NVar Source #
Lift NVar Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => NVar -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => NVar -> Code m NVar #

nvarIndexL :: NVar ⟢ DVar Source #

nvarNameL :: NVar ⟢ Name Source #

nvar_Name :: Name -> NVar Source #

name_NVarL :: NVar ⌲ Name Source #

gensymNVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m NVar Source #

syntaxNVar :: LexerBasicSyntax Source #

pNVarTail :: Name -> CParser TokenBasic NVar Source #

pNVar :: CParser TokenBasic NVar Source #

newtype GVar Source #

Constructors

GVar
Fields unGVar :: Name

Instances

Instances details

Show GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> GVar -> ShowS # show :: GVar -> String # showList :: [GVar] -> ShowS #
Eq GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: GVar -> GVar -> Bool # (/=) :: GVar -> GVar -> Bool #
Ord GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: GVar -> GVar -> Ordering # (<) :: GVar -> GVar -> Bool # (<=) :: GVar -> GVar -> Bool # (>) :: GVar -> GVar -> Bool # (>=) :: GVar -> GVar -> Bool # max :: GVar -> GVar -> GVar # min :: GVar -> GVar -> GVar #
Fuzzy GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods fuzzy :: FuzzyM GVar Source #
Pretty GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: GVar -> Doc Source #
Shrinky GVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods shrink :: GVar -> 𝐼 GVar Source #
Lift GVar Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => GVar -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => GVar -> Code m GVar #

unGVarL :: GVar ⟢ Name Source #

syntaxGVar :: LexerBasicSyntax Source #

pGVarTail :: Name -> CParser TokenBasic GVar Source #

pGVar :: CParser TokenBasic GVar Source #

data MVar s e Source #

Constructors

MVar
Fields mvarSubst :: Subst s e mvarName :: Name

Instances

Instances details

(Lift s, Lift e) => Lift (MVar s e :: Type) Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => MVar s e -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => MVar s e -> Code m (MVar s e) #
Functor (MVar s) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods map :: (a -> b) -> MVar s a -> MVar s b Source #
(Show s, Show e) => Show (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods showsPrec :: Int -> MVar s e -> ShowS # show :: MVar s e -> String # showList :: [MVar s e] -> ShowS #
(Eq s, Eq e) => Eq (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods (==) :: MVar s e -> MVar s e -> Bool # (/=) :: MVar s e -> MVar s e -> Bool #
(Ord s, Ord e) => Ord (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods compare :: MVar s e -> MVar s e -> Ordering # (<) :: MVar s e -> MVar s e -> Bool # (<=) :: MVar s e -> MVar s e -> Bool # (>) :: MVar s e -> MVar s e -> Bool # (>=) :: MVar s e -> MVar s e -> Bool # max :: MVar s e -> MVar s e -> MVar s e # min :: MVar s e -> MVar s e -> MVar s e #
(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods fuzzy :: FuzzyM (MVar s e) Source #
(Ord s, Pretty s, Pretty e) => Pretty (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods pretty :: MVar s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (MVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods shrink :: MVar s e -> 𝐼 (MVar s e) Source #

mvarSubstL :: MVar s e ⟢ Subst s e Source #

mvarNameL :: MVar s e ⟢ Name Source #

wfMVar :: Ord s => MVar s e -> 𝔹 Source #

canonMVar :: (Ord s, Eq e, Substy s e e) => (e -> e) -> MVar s e -> MVar s e Source #

substMVar :: (Ord s, Substy s e e) => Subst s e -> MVar s e -> MVar s e Source #

syntaxMVar :: LexerBasicSyntax Source #

pMVarTail :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> Name -> CParser TokenBasic (MVar () e) Source #

pMVar :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (MVar () e) Source #

Combined Variable Types

data SVar Source #

Constructors

D_SVar DVar
N_SVar NVar

Instances

Instances details

Show SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> SVar -> ShowS # show :: SVar -> String # showList :: [SVar] -> ShowS #
Eq SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: SVar -> SVar -> Bool # (/=) :: SVar -> SVar -> Bool #
Ord SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: SVar -> SVar -> Ordering # (<) :: SVar -> SVar -> Bool # (<=) :: SVar -> SVar -> Bool # (>) :: SVar -> SVar -> Bool # (>=) :: SVar -> SVar -> Bool # max :: SVar -> SVar -> SVar # min :: SVar -> SVar -> SVar #
Fuzzy SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods fuzzy :: FuzzyM SVar Source #
(Pretty DVar, Pretty NVar) => Pretty SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: SVar -> Doc Source #
Shrinky SVar Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods shrink :: SVar -> 𝐼 SVar Source #

d_SVarL :: SVar ⌲ DVar Source #

n_SVarL :: SVar ⌲ NVar Source #

mkSVar :: SName -> DVar -> SVar Source #

svarName :: SVar -> SName Source #

svarLevel :: SVar -> DVar Source #

svar_Name :: Name -> SVar Source #

data Var Source #

Constructors

D_Var DVar
N_Var NVar
G_Var GVar

Instances

Instances details

Show Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
Eq Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Fuzzy Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods fuzzy :: FuzzyM Var Source #
(Pretty DVar, Pretty NVar, Pretty GVar) => Pretty Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: Var -> Doc Source #
Shrinky Var Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods shrink :: Var -> 𝐼 Var Source #
Lift Var Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => Var -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Var -> Code m Var #

d_VarL :: Var ⌲ DVar Source #

n_VarL :: Var ⌲ NVar Source #

g_VarL :: Var ⌲ GVar Source #

var_Name :: Name -> Var Source #

var_SVar :: SVar -> Var Source #

name_VarL :: Var ⌲ Name Source #

gensymVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m Var Source #

syntaxVar :: LexerBasicSyntax Source #

pVar :: CParser TokenBasic Var Source #

data UVar s e Source #

Constructors

D_UVar DVar
N_UVar NVar
G_UVar GVar
M_UVar (MVar s e)

Instances

Instances details

(Lift s, Lift e) => Lift (UVar s e :: Type) Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => UVar s e -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => UVar s e -> Code m (UVar s e) #
Functor (UVar s) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods map :: (a -> b) -> UVar s a -> UVar s b Source #
(Show s, Show e) => Show (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods showsPrec :: Int -> UVar s e -> ShowS # show :: UVar s e -> String # showList :: [UVar s e] -> ShowS #
(Eq s, Eq e) => Eq (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods (==) :: UVar s e -> UVar s e -> Bool # (/=) :: UVar s e -> UVar s e -> Bool #
(Ord s, Ord e) => Ord (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods compare :: UVar s e -> UVar s e -> Ordering # (<) :: UVar s e -> UVar s e -> Bool # (<=) :: UVar s e -> UVar s e -> Bool # (>) :: UVar s e -> UVar s e -> Bool # (>=) :: UVar s e -> UVar s e -> Bool # max :: UVar s e -> UVar s e -> UVar s e # min :: UVar s e -> UVar s e -> UVar s e #
(Pretty e, Pretty s, Ord s, Fuzzy s, Fuzzy e) => Fuzzy (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods fuzzy :: FuzzyM (UVar s e) Source #
(Pretty DVar, Pretty NVar, Pretty GVar, Pretty (MVar s e)) => Pretty (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.UVar Methods pretty :: UVar s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (UVar s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods shrink :: UVar s e -> 𝐼 (UVar s e) Source #
(Ord s, Ord e) => MonadWriter (s ⇰ 𝑃 (UVar s e)) (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods tell :: (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e () Source # hijack :: SubstyM s e a -> SubstyM s e ((s ⇰ 𝑃 (UVar s e)) ∧ a) Source #

d_UVarL :: UVar s e ⌲ DVar Source #

n_UVarL :: UVar s e ⌲ NVar Source #

g_UVarL :: UVar s e ⌲ GVar Source #

m_UVarL :: UVar s e ⌲ MVar s e Source #

name_UVarL :: UVar s e ⌲ Name Source #

uvar_Name :: Name -> UVar s e Source #

uvar_SVar :: SVar -> UVar s e Source #

svar_UVarL :: UVar s e ⌲ SVar Source #

uvar_Var :: Var -> UVar s e Source #

var_UVarL :: UVar s e ⌲ Var Source #

gensymUVar :: (Monad m, MonadState s m) => (s ⟢ ℕ64) -> 𝕊 -> m (UVar s e) Source #

wfUVar :: Ord s => UVar s e -> 𝔹 Source #

canonUVar :: (Ord s, Eq e, Substy s e e) => (e -> e) -> UVar s e -> UVar s e Source #

syntaxUVar :: LexerBasicSyntax Source #

pUVar :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (UVar () e) Source #

Variable Lens Classes

class SVarView s e | e -> s where Source #

Methods

svarL :: s -> e ⌲ SVar Source #

Instances

Instances details

Null 𝒸 => SVarView () (ULCExp 𝒸) Source #
Instance details Defined in UVMHS.Lang.ULC Methods svarL :: () -> ULCExp 𝒸 ⌲ SVar Source #

svarScopeL :: SVarView s e => s -> SName -> e ⌲ DVar Source #

De Bruijn, Named and Global and Substitutions

data Subst s e Source #

Instances

Instances details

(Lift s, Lift e) => Lift (Subst s e :: Type) Source #
Instance details Defined in UVMHS.Lib.THLiftInstances Methods lift :: Quote m => Subst s e -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => Subst s e -> Code m (Subst s e) #
Functor (Subst s) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods map :: (a -> b) -> Subst s a -> Subst s b Source #
(Show s, Show e) => Show (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods showsPrec :: Int -> Subst s e -> ShowS # show :: Subst s e -> String # showList :: [Subst s e] -> ShowS #
(Eq s, Eq e) => Eq (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods (==) :: Subst s e -> Subst s e -> Bool # (/=) :: Subst s e -> Subst s e -> Bool #
(Ord s, Ord e) => Ord (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods compare :: Subst s e -> Subst s e -> Ordering # (<) :: Subst s e -> Subst s e -> Bool # (<=) :: Subst s e -> Subst s e -> Bool # (>) :: Subst s e -> Subst s e -> Bool # (>=) :: Subst s e -> Subst s e -> Bool # max :: Subst s e -> Subst s e -> Subst s e # min :: Subst s e -> Subst s e -> Subst s e #
(Ord s, Substy s e e) => Append (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods (⧺) :: Subst s e -> Subst s e -> Subst s e Source #
(Ord s, Substy s e e) => Monoid (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy
Null (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods null :: Subst s e Source #
(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods fuzzy :: FuzzyM (Subst s e) Source #
(Ord s, Pretty s, Pretty e) => Pretty (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods pretty :: Subst s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (Subst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods shrink :: Subst s e -> 𝐼 (Subst s e) Source #

isNullSubst :: Ord s => Subst s e -> 𝔹 Source #

wfSubst :: Ord s => Subst s e -> 𝔹 Source #

canonSubst :: (Ord s, Eq e, Substy s e e) => (e -> e) -> Subst s e -> Subst s e Source #

syntaxSubst :: LexerBasicSyntax Source #

pSubst :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e) Source #

dshiftsSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e -> Subst s e Source #

dshiftSubst :: Ord s => s -> ℕ64 -> Subst s e -> Subst s e Source #

dintrosSubst :: Ord s => (s ⇰ ℕ64) -> Subst s e Source #

dintroSubst :: Ord s => s -> ℕ64 -> Subst s e Source #

dbindsSubst :: Ord s => (s ⇰ 𝕍 e) -> Subst s e Source #

dbindSubst :: Ord s => s -> e -> Subst s e Source #

nshiftsSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e -> Subst s e Source #

nshiftSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e -> Subst s e Source #

nintrosSubst :: Ord s => (s ⇰ (Name ⇰ ℕ64)) -> Subst s e Source #

nintroSubst :: Ord s => s -> Name -> ℕ64 -> Subst s e Source #

nbindsSubst :: Ord s => (s ⇰ (Name ⇰ 𝕍 e)) -> Subst s e Source #

nbindSubst :: Ord s => s -> Name -> e -> Subst s e Source #

gbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> Subst s e Source #

gbindSubst :: Ord s => s -> Name -> e -> Subst s e Source #

Metavar Substitutions

data MetaSubst s e Source #

Instances

Instances details

(Show s, Show e) => Show (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods showsPrec :: Int -> MetaSubst s e -> ShowS # show :: MetaSubst s e -> String # showList :: [MetaSubst s e] -> ShowS #
(Eq s, Eq e) => Eq (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods (==) :: MetaSubst s e -> MetaSubst s e -> Bool # (/=) :: MetaSubst s e -> MetaSubst s e -> Bool #
(Ord s, Ord e) => Ord (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods compare :: MetaSubst s e -> MetaSubst s e -> Ordering # (<) :: MetaSubst s e -> MetaSubst s e -> Bool # (<=) :: MetaSubst s e -> MetaSubst s e -> Bool # (>) :: MetaSubst s e -> MetaSubst s e -> Bool # (>=) :: MetaSubst s e -> MetaSubst s e -> Bool # max :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e # min :: MetaSubst s e -> MetaSubst s e -> MetaSubst s e #
(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods fuzzy :: FuzzyM (MetaSubst s e) Source #
(Pretty s, Pretty e) => Pretty (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods pretty :: MetaSubst s e -> Doc Source #
(Ord s, Shrinky e) => Shrinky (MetaSubst s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Subst Methods shrink :: MetaSubst s e -> 𝐼 (MetaSubst s e) Source #

mbindsSubst :: Ord s => (s ⇰ (Name ⇰ e)) -> MetaSubst s e Source #

mbindSubst :: Ord s => s -> Name -> e -> MetaSubst s e Source #

Substy Interface

data SubstyM s e a Source #

Instances

Instances details

(Ord s, Ord e) => MonadFail (SubstyM s e :: Type -> Type) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods abort :: SubstyM s e a Source # (⎅) :: SubstyM s e a -> SubstyM s e a -> SubstyM s e a Source #
Bind (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods (≫=) :: SubstyM s e a -> (a -> SubstyM s e b) -> SubstyM s e b Source #
Functor (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods map :: (a -> b) -> SubstyM s e a -> SubstyM s e b Source #
Monad (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy
Return (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods return :: a -> SubstyM s e a Source #
(Ord s, Ord e) => MonadUCont (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods ucallCC :: (forall u. (a -> SubstyM s e u) -> SubstyM s e u) -> SubstyM s e a Source # uwithC :: (a -> SubstyM s e u) -> SubstyM s e a -> SubstyM s e u Source #
(Ord s, Ord e) => MonadReader (SubstyAction s e) (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods askL :: (SubstyAction s e ⟢ r') -> SubstyM s e r' Source # localL :: forall a r'. (SubstyAction s e ⟢ r') -> r' -> SubstyM s e a -> SubstyM s e a Source #
(Ord s, Ord e) => MonadWriter (s ⇰ 𝑃 (UVar s e)) (SubstyM s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods tell :: (s ⇰ 𝑃 (UVar s e)) -> SubstyM s e () Source # hijack :: SubstyM s e a -> SubstyM s e ((s ⇰ 𝑃 (UVar s e)) ∧ a) Source #

class SVarView s e => Substy s e a | a -> e, e -> s where Source #

Methods

substy :: a -> SubstyM s e a Source #

Instances

Instances details

(Null 𝒸, Show 𝒸) => Substy () (ULCExp 𝒸) (ULCExp 𝒸) Source #
Instance details Defined in UVMHS.Lang.ULC Methods substy :: ULCExp 𝒸 -> SubstyM () (ULCExp 𝒸) (ULCExp 𝒸) Source #

substyDBdr :: (Ord s, Ord e) => s -> SubstyM s e () Source #

substyNBdr :: (Ord s, Ord e) => s -> Name -> SubstyM s e () Source #

substyBdr :: (Ord s, Ord e, Substy s e e) => s -> (SVar -> e) -> Name -> SubstyM s e () Source #

substyDVar :: (Ord s, Ord e, Substy s e e) => (DVar -> e) -> s -> DVar -> SubstyM s e e Source #

substyNVar :: (Ord s, Ord e, Substy s e e) => (NVar -> e) -> s -> NVar -> SubstyM s e e Source #

substyGVar :: (Ord s, Ord e, Substy s e e) => (GVar -> e) -> s -> GVar -> SubstyM s e e Source #

substySVar :: (Ord s, Ord e, Substy s e e) => (SVar -> e) -> s -> SVar -> SubstyM s e e Source #

substyVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (Var -> e) -> s -> Var -> SubstyM s e e Source #

substyMVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (MVar s e -> e) -> s -> MVar s e -> SubstyM s e e Source #

substyUVar :: (Ord s, Ord e, Pretty e, Pretty s, Substy s e e) => (UVar s e -> e) -> s -> UVar s e -> SubstyM s e e Source #

fvssWith :: Substy s e a => (s -> UVar s e -> 𝔹) -> a -> s ⇰ 𝑃 (UVar s e) Source #

fvsWith :: (Ord s, Substy s e a) => s -> (UVar s e -> 𝔹) -> a -> 𝑃 (UVar s e) Source #

fvss :: Substy s e a => a -> s ⇰ 𝑃 (UVar s e) Source #

fvs :: (Ord s, Substy s e a) => s -> a -> 𝑃 (UVar s e) Source #

fvssMetas :: (Ord s, Ord e, Substy s e a) => a -> s ⇰ 𝑃 (MVar s e) Source #

fvsMetas :: (Ord s, Ord e, Substy s e a) => s -> a -> 𝑃 (MVar s e) Source #

todbr :: Substy s e a => a -> 𝑂 a Source #

tonmd :: Substy s e a => a -> 𝑂 a Source #

subst :: Substy s e a => Subst s e -> a -> 𝑂 a Source #

msubst :: Substy s e a => MetaSubst s e -> a -> 𝑂 a Source #