Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.Var

Documentation

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 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 #

svar_Name :: Name -> SVar Source #

svarName :: SVar -> SName Source #

svarLevel :: SVar -> DVar 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 DVarInf Source #

Constructors

Var_DVI DVar
Inf_DVI

Instances

Instances details

Show DVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> DVarInf -> ShowS # show :: DVarInf -> String # showList :: [DVarInf] -> ShowS #
Eq DVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: DVarInf -> DVarInf -> Bool # (/=) :: DVarInf -> DVarInf -> Bool #
Ord DVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: DVarInf -> DVarInf -> Ordering # (<) :: DVarInf -> DVarInf -> Bool # (<=) :: DVarInf -> DVarInf -> Bool # (>) :: DVarInf -> DVarInf -> Bool # (>=) :: DVarInf -> DVarInf -> Bool # max :: DVarInf -> DVarInf -> DVarInf # min :: DVarInf -> DVarInf -> DVarInf #
Pretty DVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: DVarInf -> Doc Source #

var_DVIL :: DVarInf ⌲ DVar Source #

inf_DVIL :: DVarInf ⌲ () Source #

syntaxDVarInf :: LexerBasicSyntax Source #

pDVarInfTail :: CParser TokenBasic DVarInf Source #

pDVarInf :: CParser TokenBasic DVarInf Source #

data NVarInf Source #

Constructors

NVarInf
Fields nvarInfIndex :: DVarInf nvarInfName :: Name

Instances

Instances details

Show NVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> NVarInf -> ShowS # show :: NVarInf -> String # showList :: [NVarInf] -> ShowS #
Eq NVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: NVarInf -> NVarInf -> Bool # (/=) :: NVarInf -> NVarInf -> Bool #
Ord NVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: NVarInf -> NVarInf -> Ordering # (<) :: NVarInf -> NVarInf -> Bool # (<=) :: NVarInf -> NVarInf -> Bool # (>) :: NVarInf -> NVarInf -> Bool # (>=) :: NVarInf -> NVarInf -> Bool # max :: NVarInf -> NVarInf -> NVarInf # min :: NVarInf -> NVarInf -> NVarInf #
Pretty NVarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: NVarInf -> Doc Source #

nvarInfIndexL :: NVarInf ⟢ DVarInf Source #

nvarInfNameL :: NVarInf ⟢ Name Source #

syntaxNVarInf :: LexerBasicSyntax Source #

pNVarInfTail :: Name -> CParser TokenBasic NVarInf Source #

pNVarInf :: CParser TokenBasic NVarInf Source #

data VarInf Source #

Constructors

D_VarInf DVarInf
N_VarInf NVarInf
G_VarInf GVar

Instances

Instances details

Show VarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods showsPrec :: Int -> VarInf -> ShowS # show :: VarInf -> String # showList :: [VarInf] -> ShowS #
Eq VarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods (==) :: VarInf -> VarInf -> Bool # (/=) :: VarInf -> VarInf -> Bool #
Ord VarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods compare :: VarInf -> VarInf -> Ordering # (<) :: VarInf -> VarInf -> Bool # (<=) :: VarInf -> VarInf -> Bool # (>) :: VarInf -> VarInf -> Bool # (>=) :: VarInf -> VarInf -> Bool # max :: VarInf -> VarInf -> VarInf # min :: VarInf -> VarInf -> VarInf #
(Pretty DVarInf, Pretty NVarInf, Pretty GVar) => Pretty VarInf Source #
Instance details Defined in UVMHS.Lib.Substitution.Var Methods pretty :: VarInf -> Doc Source #

d_VarInfL :: VarInf ⌲ DVarInf Source #

n_VarInfL :: VarInf ⌲ NVarInf Source #

g_VarInfL :: VarInf ⌲ GVar Source #

syntaxVarInf :: LexerBasicSyntax Source #

pVarInf :: CParser TokenBasic VarInf Source #

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 #