Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
- Composition of fresh and free substitutions
- Conversion between fresh and free
- Convenience exports
- General Substitutions
- application of substitutions
- smart constructors for substitutions
- Composition of substitutions
- operations
- queries
- views
- Apply class
- Pretty printing
- Substitution of LVars
- General Substitutions
- smart constructors for substitutions
- operations
- queries
- views
- Pretty printing
- operations on fresh substitutions
- Substitution of LVars
Standard and fresh substitutions.
- composeVFresh :: (IsConst c, Show (Lit c LVar)) => LSubstVFresh c -> LSubst c -> LSubstVFresh c
- freshToFree :: (MonadFresh m, IsConst c) => SubstVFresh c LVar -> m (Subst c LVar)
- freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar
- freshToFreeAvoidingFast :: (HasFrees t, Ord c) => LSubstVFresh c -> t -> LSubst c
- freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVar
- module Term.LTerm
- newtype Subst c v = Subst {}
- applyVTerm :: (IsConst c, IsVar v, Ord c) => Subst c v -> VTerm c v -> VTerm c v
- applyLit :: IsVar v => Subst c v -> Lit c v -> VTerm c v
- substFromList :: IsVar v => [(v, VTerm c v)] -> Subst c v
- substFromMap :: IsVar v => Map v (VTerm c v) -> Subst c v
- emptySubst :: Subst c v
- compose :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c v
- applySubst :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c v
- restrict :: IsVar v => [v] -> Subst c v -> Subst c v
- mapRange :: (IsConst c, IsVar v, IsConst c2) => (VTerm c v -> VTerm c2 v) -> Subst c v -> Subst c2 v
- varsRange :: IsVar v => Subst c v -> [v]
- dom :: Subst c v -> [v]
- range :: Subst c v -> [VTerm c v]
- imageOf :: IsVar v => Subst c v -> v -> Maybe (VTerm c v)
- substToListOn :: (IsConst c, IsVar v) => [v] -> Subst c v -> [VTerm c v]
- substToList :: Subst c v -> [(v, VTerm c v)]
- class Apply t where
- prettySubst :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> Subst c v -> [d]
- type LSubst c = Subst c LVar
- type LNSubst = Subst Name LVar
- prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) => LSubst c -> d
- newtype SubstVFresh c v = SubstVFresh {}
- substFromListVFresh :: IsVar v => [(v, VTerm c v)] -> SubstVFresh c v
- emptySubstVFresh :: SubstVFresh c v
- restrictVFresh :: IsVar v => [v] -> SubstVFresh c v -> SubstVFresh c v
- mapRangeVFresh :: (IsConst c, IsVar v, IsConst c2) => (VTerm c v -> VTerm c2 v) -> SubstVFresh c v -> SubstVFresh c2 v
- extendWithRenaming :: (Ord c, Show (Lit c LVar)) => [LVar] -> SubstVFresh c LVar -> SubstVFresh c LVar
- varsRangeVFresh :: IsVar v => SubstVFresh c v -> [v]
- domVFresh :: SubstVFresh c v -> [v]
- rangeVFresh :: SubstVFresh c v -> [VTerm c v]
- isRenaming :: LSubstVFresh c -> Bool
- imageOfVFresh :: IsVar v => SubstVFresh c v -> v -> Maybe (VTerm c v)
- substToListVFresh :: SubstVFresh c v -> [(v, VTerm c v)]
- prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> SubstVFresh c v -> [d]
- renameFresh :: (Ord c, MonadFresh m) => SubstVFresh c LVar -> m (SubstVFresh c LVar)
- renameFreshAvoiding :: (Ord c, HasFrees t) => LSubstVFresh c -> t -> SubstVFresh c LVar
- removeRenamings :: LSubstVFresh c -> LSubstVFresh c
- type LSubstVFresh c = SubstVFresh c LVar
- type LNSubstVFresh = SubstVFresh Name LVar
- prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) => LSubstVFresh c -> d
- prettyDisjLNSubstsVFresh :: Document d => Disj LNSubstVFresh -> d
Composition of fresh and free substitutions
composeVFresh :: (IsConst c, Show (Lit c LVar)) => LSubstVFresh c -> LSubst c -> LSubstVFresh cSource
composeVFresh s1 s2
composes the fresh substitution s1 and the free substitution s2.
The result is the fresh substitution s = s1.s2.
Conversion between fresh and free
freshToFree :: (MonadFresh m, IsConst c) => SubstVFresh c LVar -> m (Subst c LVar)Source
freshToFree s
converts the bound variables in s
to free variables
using fresh variable names. We try to preserve variables names if possible.
freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVarSource
freshToFreeAvoiding s t
converts all fresh variables in the range of
s
to free variables avoiding free variables in t
. This function tries
to reuse variable names from the domain of the substitution if possible.
freshToFreeAvoidingFast :: (HasFrees t, Ord c) => LSubstVFresh c -> t -> LSubst cSource
freshToFreeAvoidingFast s t
converts all fresh variables in the range of
s
to free variables avoiding free variables in t
. This function does
not try to reuse variable names from the domain of the substitution.
freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVarSource
freeToFreshRaw s
considers all variables in the range of s
as fresh.
Convenience exports
module Term.LTerm
General Substitutions
We use the data type Subst c v
of substitutions. c
is the type of constants
and v
the type of variables.
application of substitutions
applyVTerm :: (IsConst c, IsVar v, Ord c) => Subst c v -> VTerm c v -> VTerm c vSource
applyVTerm subst t
applies the substitution subst
to the term t
.
applyLit :: IsVar v => Subst c v -> Lit c v -> VTerm c vSource
applyLit subst l
applies the substitution subst
to the literal l
.
smart constructors for substitutions
substFromList :: IsVar v => [(v, VTerm c v)] -> Subst c vSource
Convert a list to a substitution. The x/x
mappings are removed.
substFromMap :: IsVar v => Map v (VTerm c v) -> Subst c vSource
Convert a map to a substitution. The x/x
mappings are removed.
FIXME: implement directly, use substFromMap for substFromList.
emptySubst :: Subst c vSource
emptySubVFree
is the substitution with empty domain.
Composition of substitutions
compose :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c vSource
compose s1 s2
composes the substitutions s1 and s2. The result is
s1.s2
, i.e., it has the same effect as (t s2) s1 = s1(s2(t))
when applied to a term t
.
applySubst :: (IsConst c, IsVar v) => Subst c v -> Subst c v -> Subst c vSource
applySubst subst subst'
applies the substitution subst
to the range of
the substitution subst'
.
operations
restrict :: IsVar v => [v] -> Subst c v -> Subst c vSource
restrict vars subst
restricts the domain of the substitution subst
to vars
.
mapRange :: (IsConst c, IsVar v, IsConst c2) => (VTerm c v -> VTerm c2 v) -> Subst c v -> Subst c2 vSource
mapRange f subst
maps the function f
over the range of the substitution subst
.
queries
varsRange :: IsVar v => Subst c v -> [v]Source
varsRange subst
returns all variables in the range of the substitution.
imageOf :: IsVar v => Subst c v -> v -> Maybe (VTerm c v)Source
Returns the image of i
under subst
if i
is in the domain of subst
.
views
substToListOn :: (IsConst c, IsVar v) => [v] -> Subst c v -> [VTerm c v]Source
substToPairOn vs sigma
converts the list of variables [x1,..,xk]
to
[sigma(x1),..,sigma(xk)]
.
substToList :: Subst c v -> [(v, VTerm c v)]Source
Convert substitution to list.
Apply class
Types that support the application of LSubst
s.
Apply Bool | |
Apply Char | |
Apply Int | |
Apply () | |
Apply BLTerm | |
Apply BLVar | |
Apply LNTerm | |
Apply LVar | |
Apply a => Apply [a] | |
Apply a => Apply (Maybe a) | |
(Ord a, Apply a) => Apply (Set a) | |
Apply a => Apply (Conj a) | |
Apply a => Apply (Disj a) | |
Apply t => Apply (Equal t) | |
(Apply a, Apply b) => Apply (Either a b) | |
(Apply a, Apply b) => Apply (a, b) |
Pretty printing
prettySubst :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> Subst c v -> [d]Source
Pretty print a substitution.
Substitution of LVars
prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) => LSubst c -> dSource
Pretty print a substitution with logical variables.
General Substitutions
newtype SubstVFresh c v Source
We use the data type SubstVFresh c v
of substitutions.
c
denotes the type of constants and v
the type of variables.
Fresh substitutions cannot be applied directly, they have to be converted
to free substitutions in a certain context (MonadFresh).
(Eq c, Eq v) => Eq (SubstVFresh c v) | |
(Ord c, Ord v) => Ord (SubstVFresh c v) | |
(Show c, Show v) => Show (SubstVFresh c v) | |
(Binary c, Binary v) => Binary (SubstVFresh c v) | |
(NFData c, NFData v) => NFData (SubstVFresh c v) | |
Sized (SubstVFresh c v) | |
HasFrees (SubstVFresh n LVar) |
smart constructors for substitutions
substFromListVFresh :: IsVar v => [(v, VTerm c v)] -> SubstVFresh c vSource
Convert a list of mappings to a fresh substitution.
emptySubstVFresh :: SubstVFresh c vSource
emptySubstVFresh
is the fresh substitution with empty domain.
operations
restrictVFresh :: IsVar v => [v] -> SubstVFresh c v -> SubstVFresh c vSource
restrictVFresh vars subst
restricts the domain of the substitution subst
to vars
.
mapRangeVFresh :: (IsConst c, IsVar v, IsConst c2) => (VTerm c v -> VTerm c2 v) -> SubstVFresh c v -> SubstVFresh c2 vSource
mapRangeVFresh f subst
maps the function f
over the range of the substitution subst
.
Note that all introduced variables are considered fresh.
extendWithRenaming :: (Ord c, Show (Lit c LVar)) => [LVar] -> SubstVFresh c LVar -> SubstVFresh c LVarSource
extendWithRenaming vs s
extends the substitution s
with renamings (with
fresh variables) for the variables in vs
that are not already in dom s
.
queries
varsRangeVFresh :: IsVar v => SubstVFresh c v -> [v]Source
varsRangeVFresh subst
returns all variables in the range of the substitution
domVFresh :: SubstVFresh c v -> [v]Source
domVFresh subst
returns the domain of the substitution substs
.
rangeVFresh :: SubstVFresh c v -> [VTerm c v]Source
rangeVFresh subst
returns the range of the substitution substs
.
isRenaming :: LSubstVFresh c -> BoolSource
Returns True
if the substitution is a renaming.
imageOfVFresh :: IsVar v => SubstVFresh c v -> v -> Maybe (VTerm c v)Source
Returns the image of i
under subst
if i
is in the domain of subst
.
views
substToListVFresh :: SubstVFresh c v -> [(v, VTerm c v)]Source
Convert substitution to list.
Pretty printing
prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d, Show c, Show v) => (v -> d) -> (Lit c v -> d) -> SubstVFresh c v -> [d]Source
Pretty print a substitution.
operations on fresh substitutions
renameFresh :: (Ord c, MonadFresh m) => SubstVFresh c LVar -> m (SubstVFresh c LVar)Source
renameFresh s
renames the fresh variables in s
using fresh variables.
This function can be used to prevent overshadowing which might
make output hard to read.
renameFreshAvoiding :: (Ord c, HasFrees t) => LSubstVFresh c -> t -> SubstVFresh c LVarSource
renameFreshAvoiding s t
renames the fresh variables in the range of s
away from
variables that are free in t
. This is an internal function.
removeRenamings :: LSubstVFresh c -> LSubstVFresh cSource
removeRenamings s
removes all renamings (see isRenamedVar
) from s
.
Substitution of LVars
type LSubstVFresh c = SubstVFresh c LVarSource
Fresh substitution with logical variables
type LNSubstVFresh = SubstVFresh Name LVarSource
Fresh substitution with logical variables and names
prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c) => LSubstVFresh c -> dSource
Pretty print a substitution with logical variables.
prettyDisjLNSubstsVFresh :: Document d => Disj LNSubstVFresh -> dSource
Pretty print a disjunction of substitutions.