uvmhs-0.0.0.0
Safe HaskellSafe-Inferred
LanguageHaskell2010

UVMHS.Lib.Substitution

Documentation

data SubstElem s e Source #

Constructors

SubstElem 

Fields

Instances

Instances details
(Show s, Show e) => Show (SubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

showsPrec :: Int -> SubstElem s e -> ShowS #

show :: SubstElem s e -> String #

showList :: [SubstElem s e] -> ShowS #

(Eq s, Eq e) => Eq (SubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

(==) :: SubstElem s e -> SubstElem s e -> Bool #

(/=) :: SubstElem s e -> SubstElem s e -> Bool #

(Ord s, Ord e) => Ord (SubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

compare :: SubstElem s e -> SubstElem s e -> Ordering #

(<) :: SubstElem s e -> SubstElem s e -> Bool #

(<=) :: SubstElem s e -> SubstElem s e -> Bool #

(>) :: SubstElem s e -> SubstElem s e -> Bool #

(>=) :: SubstElem s e -> SubstElem s e -> Bool #

max :: SubstElem s e -> SubstElem s e -> SubstElem s e #

min :: SubstElem s e -> SubstElem s e -> SubstElem s e #

(Pretty s, Pretty e) => Pretty (SubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

pretty :: SubstElem s e -> Doc Source #

(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (SubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

fuzzy :: FuzzyM (SubstElem s e) Source #

substElemValueL :: forall (s :: Type) (e :: Type). (⟢) (SubstElem s e) (() -> 𝑂 e) Source #

substElemIntroL :: forall (s :: Type) (e :: Type). (⟢) (SubstElem s e) ((⇰) s ℕ64) Source #

introSubstElem :: Ord s => (s ⇰ ℕ64) -> SubstElem s e -> SubstElem s e Source #

subSubstElem :: ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SubstElem s e -> SubstElem s e Source #

data SSubstElem s e Source #

Constructors

Var_SSE ℕ64 
Trm_SSE (SubstElem s e) 

Instances

Instances details
(Show s, Show e) => Show (SSubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

showsPrec :: Int -> SSubstElem s e -> ShowS #

show :: SSubstElem s e -> String #

showList :: [SSubstElem s e] -> ShowS #

(Eq s, Eq e) => Eq (SSubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

(==) :: SSubstElem s e -> SSubstElem s e -> Bool #

(/=) :: SSubstElem s e -> SSubstElem s e -> Bool #

(Ord s, Ord e) => Ord (SSubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

compare :: SSubstElem s e -> SSubstElem s e -> Ordering #

(<) :: SSubstElem s e -> SSubstElem s e -> Bool #

(<=) :: SSubstElem s e -> SSubstElem s e -> Bool #

(>) :: SSubstElem s e -> SSubstElem s e -> Bool #

(>=) :: SSubstElem s e -> SSubstElem s e -> Bool #

max :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e #

min :: SSubstElem s e -> SSubstElem s e -> SSubstElem s e #

(Pretty s, Pretty e) => Pretty (SSubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

pretty :: SSubstElem s e -> Doc Source #

(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (SSubstElem s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

fuzzy :: FuzzyM (SSubstElem s e) Source #

introSSubstElem :: Ord s => s -> (s ⇰ ℕ64) -> SSubstElem s e -> SSubstElem s e Source #

subSSubstElem :: (ℕ64 -> SSubstElem s e) -> ((s ⇰ ℕ64) -> e -> 𝑂 e) -> SSubstElem s e -> SSubstElem s e Source #

data DSubst s e Source #

Constructors

DSubst 

Fields

Instances

Instances details
(Show s, Show e) => Show (DSubst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

showsPrec :: Int -> DSubst s e -> ShowS #

show :: DSubst s e -> String #

showList :: [DSubst s e] -> ShowS #

(Eq s, Eq e) => Eq (DSubst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

(==) :: DSubst s e -> DSubst s e -> Bool #

(/=) :: DSubst s e -> DSubst s e -> Bool #

(Ord s, Ord e) => Ord (DSubst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

compare :: DSubst s e -> DSubst s e -> Ordering #

(<) :: DSubst s e -> DSubst s e -> Bool #

(<=) :: DSubst s e -> DSubst s e -> Bool #

(>) :: DSubst s e -> DSubst s e -> Bool #

(>=) :: DSubst s e -> DSubst s e -> Bool #

max :: DSubst s e -> DSubst s e -> DSubst s e #

min :: DSubst s e -> DSubst s e -> DSubst s e #

(Pretty ℕ64, Pretty (𝕍 (SSubstElem s e)), Pretty ℤ64) => Pretty (DSubst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

pretty :: DSubst s e -> Doc Source #

(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (DSubst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

fuzzy :: FuzzyM (DSubst s e) Source #

dsubstIntroL :: forall (s :: Type) (e :: Type). (⟢) (DSubst s e) ℤ64 Source #

dsubstElemsL :: forall (s :: Type) (e :: Type). (⟢) (DSubst s e) (𝕍 (SSubstElem s e)) Source #

dsubstShiftL :: forall (s :: Type) (e :: Type). (⟢) (DSubst s e) ℕ64 Source #

isNullDSubst :: DSubst s e -> 𝔹 Source #

dsubstVar :: DSubst 𝑠 e -> ℕ64 -> SSubstElem 𝑠 e Source #

data GSubst s₁ s₂ e Source #

Constructors

GSubst 

Fields

Instances

Instances details
(Show s₁, Show s₂, Show e) => Show (GSubst s₁ s₂ e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

showsPrec :: Int -> GSubst s₁ s₂ e -> ShowS #

show :: GSubst s₁ s₂ e -> String #

showList :: [GSubst s₁ s₂ e] -> ShowS #

(Eq s₁, Eq s₂, Eq e) => Eq (GSubst s₁ s₂ e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

(==) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

(/=) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

(Ord s₁, Ord s₂, Ord e) => Ord (GSubst s₁ s₂ e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

compare :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Ordering #

(<) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

(<=) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

(>) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

(>=) :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> Bool #

max :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e #

min :: GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e #

(Pretty (s₁ ⇰ SubstElem s₂ e), Pretty (s₂ ⇰ DSubst s₂ e)) => Pretty (GSubst s₁ s₂ e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

pretty :: GSubst s₁ s₂ e -> Doc Source #

(Ord s₁, Ord s₂, Fuzzy s₁, Fuzzy s₂, Fuzzy e) => Fuzzy (GSubst s₁ s₂ e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

fuzzy :: FuzzyM (GSubst s₁ s₂ e) Source #

gsubstSubstL :: forall (s₁ :: Type) (s₂ :: Type) (e :: Type). (⟢) (GSubst s₁ s₂ e) ((⇰) s₂ (DSubst s₂ e)) Source #

gsubstMetasL :: forall (s₁ :: Type) (s₂ :: Type) (e :: Type). (⟢) (GSubst s₁ s₂ e) ((⇰) s₁ (SubstElem s₂ e)) Source #

gsubstGVarsL :: forall (s₁ :: Type) (s₂ :: Type) (e :: Type). (⟢) (GSubst s₁ s₂ e) ((⇰) s₁ (SubstElem s₂ e)) Source #

𝓈shiftG :: Ord s₂ => (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e Source #

𝓈introG :: (s₂ ⇰ ℕ64) -> GSubst s₁ s₂ e Source #

𝓈sbindsG :: (s₂ ⇰ 𝕍 e) -> GSubst s₁ s₂ e Source #

𝓈sgbindsG :: (s₁ ⇰ e) -> GSubst s₁ s₂ e Source #

𝓈smbindsG :: (s₁ ⇰ e) -> GSubst s₁ s₂ e Source #

appendGSubst :: (Ord s₁, Ord s₂) => (GSubst s₁ s₂ e -> e -> 𝑂 e) -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e -> GSubst s₁ s₂ e Source #

newtype Subst s e Source #

Constructors

Subst 

Fields

Instances

Instances details
(Show s, Show e) => Show (Subst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

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

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

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

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

Null (Subst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

null :: Subst s e Source #

(Pretty s, Pretty e) => Pretty (Subst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

pretty :: Subst s e -> Doc Source #

(Ord s, Fuzzy s, Fuzzy e) => Fuzzy (Subst s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

fuzzy :: FuzzyM (Subst s e) Source #

unSubstL :: forall (s :: Type) (e :: Type). (⟢) (Subst s e) (GSubst ((∧) s 𝕏) ((∧) s (𝑂 𝕏)) e) Source #

data FreeVarsAction s Source #

Constructors

FreeVarsAction 

Fields

freeVarsActionScopeL :: forall (s :: Type). (⟢) (FreeVarsAction s) ((⇰) ((∧) s (𝑂 𝕏)) ℕ64) Source #

freeVarsActionFilterL :: forall (s :: Type). (⟢) (FreeVarsAction s) (s -> 𝕐 -> 𝔹) Source #

data SubstAction s e Source #

Constructors

SubstAction 

Fields

substActionSubstL :: forall (s :: Type) (e :: Type). (⟢) (SubstAction s e) (Subst s e) Source #

substActionReBdrL :: forall (s :: Type) (e :: Type). (⟢) (SubstAction s e) (𝑂 𝔹) Source #

data SubstEnv s e Source #

Constructors

FVsSubstEnv (FreeVarsAction s) 
SubSubstEnv (SubstAction s e) 

Instances

Instances details
Ord s => MonadReader (SubstEnv s e) (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

askL :: (SubstEnv s e ⟢ r') -> SubstM s e r' Source #

localL :: forall a r'. (SubstEnv s e ⟢ r') -> r' -> SubstM s e a -> SubstM s e a Source #

subSubstEnvL :: forall (s :: Type) (e :: Type). (⌲) (SubstEnv s e) (SubstAction s e) Source #

fVsSubstEnvL :: forall (s :: Type) (e :: Type). (⌲) (SubstEnv s e) (FreeVarsAction s) Source #

newtype SubstM s e a Source #

Constructors

SubstM 

Fields

Instances

Instances details
Ord s => MonadFail (SubstM s e :: Type -> Type) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

abort :: forall (a :: k). SubstM s e a Source #

(⎅) :: forall (a :: k). SubstM s e a -> SubstM s e a -> SubstM s e a Source #

Bind (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

(≫=) :: SubstM s e a -> (a -> SubstM s e b) -> SubstM s e b Source #

Functor (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

map :: (a -> b) -> SubstM s e a -> SubstM s e b Source #

Monad (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Return (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

return :: a -> SubstM s e a Source #

Ord s => MonadUCont (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

ucallCC :: (forall u. (a -> SubstM s e u) -> SubstM s e u) -> SubstM s e a Source #

uwithC :: (a -> SubstM s e u) -> SubstM s e a -> SubstM s e u Source #

Ord s => MonadReader (SubstEnv s e) (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

askL :: (SubstEnv s e ⟢ r') -> SubstM s e r' Source #

localL :: forall a r'. (SubstEnv s e ⟢ r') -> r' -> SubstM s e a -> SubstM s e a Source #

Ord s => MonadWriter (s ⇰ 𝑃 𝕐) (SubstM s e) Source # 
Instance details

Defined in UVMHS.Lib.Substitution

Methods

tell :: (s ⇰ 𝑃 𝕐) -> SubstM s e () Source #

hijack :: SubstM s e a -> SubstM s e ((s ⇰ 𝑃 𝕐) ∧ a) Source #

mkSubstM :: (forall u. SubstEnv s e -> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> SubstM s e a Source #

runSubstM :: SubstEnv s e -> (a -> SubstEnv s e -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u) -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 u Source #

runSubstMHalt :: SubstEnv s e -> SubstM s e a -> (s ⇰ 𝑃 𝕐) ∧ 𝑂 a Source #

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

Methods

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

Instances

Instances details
Substy () (ULCExp 𝒸) (ULCExp 𝒸) Source # 
Instance details

Defined in UVMHS.Lang.ULC

Methods

substy :: ULCExp 𝒸 -> SubstM () (ULCExp 𝒸) (ULCExp 𝒸) Source #

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

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

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

fvsWith :: Substy s e a => (FreeVarsAction s -> FreeVarsAction s) -> a -> s ⇰ 𝑃 𝕐 Source #

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

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

fvs :: Substy s e a => a -> s ⇰ 𝑃 𝕐 Source #

nullSubst :: Subst s e Source #

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

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

𝓈snshift :: Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e -> Subst s e Source #

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

𝓈snintro :: Ord s => (s ⇰ (𝕏 ⇰ ℕ64)) -> Subst s e Source #

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

𝓈sdbind :: Ord s => s -> e -> Subst s e Source #

𝓈snbinds :: Ord s => (s ⇰ (𝕏 ⇰ 𝕍 e)) -> Subst s e Source #

𝓈snbind :: Ord s => s -> 𝕏 -> e -> Subst s e Source #

𝓈sgbinds :: Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e Source #

𝓈sgbind :: Ord s => s -> 𝕏 -> e -> Subst s e Source #

𝓈smbinds :: Ord s => (s ⇰ (𝕏 ⇰ e)) -> Subst s e Source #

𝓈smbind :: Ord s => s -> 𝕏 -> e -> Subst s e Source #

𝓈dshift :: ℕ64 -> Subst () e -> Subst () e Source #

𝓈nshift :: (𝕏 ⇰ ℕ64) -> Subst () e -> Subst () e Source #

𝓈dintro :: ℕ64 -> Subst () e Source #

𝓈nintro :: (𝕏 ⇰ ℕ64) -> Subst () e Source #

𝓈dbinds :: 𝕍 e -> Subst () e Source #

𝓈dbind :: e -> Subst () e Source #

𝓈nbinds :: (𝕏 ⇰ 𝕍 e) -> Subst () e Source #

𝓈nbind :: 𝕏 -> e -> Subst () e Source #

𝓈gbinds :: (𝕏 ⇰ e) -> Subst () e Source #

𝓈gbind :: 𝕏 -> e -> Subst () e Source #

𝓈mbinds :: (𝕏 ⇰ e) -> Subst () e Source #

𝓈mbind :: 𝕏 -> e -> Subst () e Source #

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

substyNBdr :: Ord s => s -> 𝕏 -> SubstM s e () Source #

substyBdr :: (Ord s, Substy s e e) => s -> (𝕐 -> e) -> 𝕏 -> SubstM s e () Source #

substyVar :: (Ord s, Substy s e e) => 𝑂 𝕏 -> s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e Source #

substyDVar :: (Ord s, Substy s e e) => s -> (ℕ64 -> e) -> ℕ64 -> SubstM s e e Source #

substyNVar :: (Ord s, Substy s e e) => s -> (ℕ64 -> e) -> 𝕏 -> ℕ64 -> SubstM s e e Source #

substyGVar :: (Ord s, Substy s e e) => s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e Source #

substyMVar :: (Ord s, Substy s e e) => s -> (𝕏 -> e) -> 𝕏 -> SubstM s e e Source #

substy𝕐 :: (Ord s, Substy s e e) => s -> (𝕐 -> e) -> 𝕐 -> SubstM s e e Source #