Safe Haskell	None
Language	Haskell2010

UVMHS.Lib.Substitution.Substy

Contents

Orphan instances

Documentation

data FreeVarsAction s e Source #

Constructors

FreeVarsAction
Fields freeVarsActionFilter :: s -> UVar s e -> 𝔹 freeVarsActionScope :: (s ∧ SName) ⇰ ℕ64

freeVarsActionFilterL :: FreeVarsAction s e ⟢ (s -> UVar s e -> 𝔹) Source #

freeVarsActionScopeL :: FreeVarsAction s e ⟢ ((s ∧ SName) ⇰ ℕ64) Source #

data RebindAction Source #

Constructors

ID_RA
AllNameless_RA
AllNamed_RA

Instances

Instances details

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

data SubstAction s e Source #

Constructors

SubstAction
Fields substActionRebind :: RebindAction substActionSubst :: Subst s e

Instances

Instances details

(Show s, Show e) => Show (SubstAction s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods showsPrec :: Int -> SubstAction s e -> ShowS # show :: SubstAction s e -> String # showList :: [SubstAction s e] -> ShowS #
(Eq s, Eq e) => Eq (SubstAction s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods (==) :: SubstAction s e -> SubstAction s e -> Bool # (/=) :: SubstAction s e -> SubstAction s e -> Bool #
(Ord s, Ord e) => Ord (SubstAction s e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods compare :: SubstAction s e -> SubstAction s e -> Ordering # (<) :: SubstAction s e -> SubstAction s e -> Bool # (<=) :: SubstAction s e -> SubstAction s e -> Bool # (>) :: SubstAction s e -> SubstAction s e -> Bool # (>=) :: SubstAction s e -> SubstAction s e -> Bool # max :: SubstAction s e -> SubstAction s e -> SubstAction s e # min :: SubstAction s e -> SubstAction s e -> SubstAction s e #

substActionRebindL :: SubstAction s e ⟢ RebindAction Source #

substActionSubstL :: SubstAction s e ⟢ Subst s e Source #

data SubstyAction s e Source #

Constructors

FreeVars_SA (FreeVarsAction s e)
Subst_SA (SubstAction s e)
MetaSubst_SA (MetaSubst s e)

Instances

Instances details

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

freeVars_SAL :: SubstyAction s e ⌲ FreeVarsAction s e Source #

subst_SAL :: SubstyAction s e ⌲ SubstAction s e Source #

metaSubst_SAL :: SubstyAction s e ⌲ MetaSubst s e Source #

newtype SubstyM s e a Source #

Constructors

SubstyM
Fields unSubstyM :: UContT (ReaderT (SubstyAction s e) (FailT (WriterT (s ⇰ 𝑃 (UVar s e)) ID))) a

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 #

mkSubstM :: (forall u. SubstyAction s e -> (a -> SubstyAction s e -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 u) -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 u) -> SubstyM s e a Source #

runSubstM :: SubstyAction s e -> (a -> SubstyAction s e -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 u) -> SubstyM s e a -> (s ⇰ 𝑃 (UVar s e)) ∧ 𝑂 u Source #

evalSubstM :: SubstyAction s e -> SubstyM s e a -> (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 #

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 #

canonSubst :: (Ord s, Eq e, Substy s e e) => (e -> e) -> Subst s e -> Subst 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 #

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

nullSubst :: Subst s e Source #

appendSubst :: (Ord s, Substy s e e) => Subst s e -> Subst s e -> Subst s e 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 #

substySVarG :: (Ord s, Ord e, Substy s e e) => (DVar -> e) -> s -> SVar -> SubstyM s e 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 #

syntaxSubst :: LexerBasicSyntax Source #

syntaxMVar :: LexerBasicSyntax Source #

syntaxUVar :: LexerBasicSyntax Source #

data ParseSubstAction e Source #

Constructors

ParseSubstAction
Fields parseSubstActionShfts :: 𝐼 ℕ64 parseSubstActionElems :: 𝑂 DVar ⇰ 𝐼 e parseSubstActionIncrs :: 𝐼 (ℕ64 ∧ ℤ64)

Instances

Instances details

Show e => Show (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods showsPrec :: Int -> ParseSubstAction e -> ShowS # show :: ParseSubstAction e -> String # showList :: [ParseSubstAction e] -> ShowS #
Eq e => Eq (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods (==) :: ParseSubstAction e -> ParseSubstAction e -> Bool # (/=) :: ParseSubstAction e -> ParseSubstAction e -> Bool #
Ord e => Ord (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods compare :: ParseSubstAction e -> ParseSubstAction e -> Ordering # (<) :: ParseSubstAction e -> ParseSubstAction e -> Bool # (<=) :: ParseSubstAction e -> ParseSubstAction e -> Bool # (>) :: ParseSubstAction e -> ParseSubstAction e -> Bool # (>=) :: ParseSubstAction e -> ParseSubstAction e -> Bool # max :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e # min :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e #
Append (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods (⧺) :: ParseSubstAction e -> ParseSubstAction e -> ParseSubstAction e Source #
Monoid (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy
Null (ParseSubstAction e) Source #
Instance details Defined in UVMHS.Lib.Substitution.Substy Methods null :: ParseSubstAction e Source #

parseSubstActionShftsL :: ParseSubstAction e ⟢ 𝐼 ℕ64 Source #

parseSubstActionElemsL :: ParseSubstAction e ⟢ (𝑂 DVar ⇰ 𝐼 e) Source #

parseSubstActionIncrsL :: ParseSubstAction e ⟢ 𝐼 (ℕ64 ∧ ℤ64) Source #

parseSubstActionShft :: ℕ64 -> ParseSubstAction e Source #

parseSubstActionElem :: 𝑂 DVar -> e -> ParseSubstAction e Source #

parseSubstActionIncr :: ℕ64 -> ℤ64 -> ParseSubstAction e Source #

type ParseSubstActions e = SGName ⇰ ParseSubstAction e Source #

pSubst :: (Eq e, Substy () e e) => (() -> CParser TokenBasic e) -> CParser TokenBasic (Subst () e) 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 #

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

Orphan instances

(Ord s, Substy s e e) => Append (Subst s e) Source #
Instance details Methods (⧺) :: Subst s e -> Subst s e -> Subst s e Source #
(Ord s, Substy s e e) => Monoid (Subst s e) Source #
Instance details
Null (Subst s e) Source #
Instance details Methods null :: Subst s e Source #
(Ord s, Shrinky e) => Shrinky (UVar s e) Source #
Instance details Methods shrink :: UVar s e -> 𝐼 (UVar s e) Source #