Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Terms with logical variables and names.
- data Name = Name {}
- data NameTag
- newtype NameId = NameId {}
- type NTerm v = VTerm Name v
- sortOfName :: Name -> LSort
- freshTerm :: String -> NTerm v
- pubTerm :: String -> NTerm v
- data LSort
- = LSortPub
- | LSortFresh
- | LSortMsg
- | LSortNode
- data LVar = LVar {}
- type NodeId = LVar
- type LTerm c = VTerm c LVar
- type LNTerm = VTerm Name LVar
- freshLVar :: MonadFresh m => String -> LSort -> m LVar
- sortPrefix :: LSort -> String
- sortSuffix :: LSort -> String
- sortCompare :: LSort -> LSort -> Maybe Ordering
- sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSort
- sortOfLNTerm :: LNTerm -> LSort
- sortOfLit :: Lit Name LVar -> LSort
- isMsgVar :: LNTerm -> Bool
- isFreshVar :: LNTerm -> Bool
- isSimpleTerm :: LNTerm -> Bool
- niFactors :: LNTerm -> [LNTerm]
- containsPrivate :: Term t -> Bool
- neverContainsFreshPriv :: LNTerm -> Bool
- ltermVar :: LSort -> LTerm c -> Maybe LVar
- ltermVar' :: Show c => LSort -> LTerm c -> LVar
- ltermNodeId :: LTerm c -> Maybe LVar
- ltermNodeId' :: Show c => LTerm c -> LVar
- bltermNodeId :: BLTerm -> Maybe LVar
- bltermNodeId' :: BLTerm -> LVar
- class HasFrees t where
- foldFrees :: Monoid m => (LVar -> m) -> t -> m
- foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> m
- mapFrees :: Applicative f => MonotoneFunction f -> t -> f t
- data MonotoneFunction f
- occurs :: HasFrees t => LVar -> t -> Bool
- freesList :: HasFrees t => t -> [LVar]
- frees :: HasFrees t => t -> [LVar]
- someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m t
- rename :: (MonadFresh m, HasFrees a) => a -> m a
- eqModuloFreshnessNoAC :: (HasFrees a, Eq a) => a -> a -> Bool
- avoid :: HasFrees t => t -> FreshState
- evalFreshAvoiding :: HasFrees t => Fresh a -> t -> a
- evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m a
- renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> s
- avoidPrecise :: HasFrees t => t -> FreshState
- renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a
- renameDropNamehint :: (MonadFresh m, MonadBind LVar LVar m, HasFrees a) => a -> m a
- varOccurences :: HasFrees a => a -> [(LVar, Set Occurence)]
- data BVar v
- type BLVar = BVar LVar
- type BLTerm = NTerm BLVar
- foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a
- fromFree :: BVar v -> v
- prettyLVar :: Document d => LVar -> d
- prettyNodeId :: Document d => NodeId -> d
- prettyNTerm :: (Show v, Document d) => NTerm v -> d
- prettyLNTerm :: Document d => LNTerm -> d
- module Term.VTerm
Names
Names.
Tags for names.
Type safety for names.
Queries
Construction
LVar
Sorts for logical variables. They satisfy the following sub-sort relation:
LSortFresh < LSortMsg LSortPub < LSortMsg
LSortPub | Arbitrary public names. |
LSortFresh | Arbitrary fresh names. |
LSortMsg | Arbitrary messages. |
LSortNode | Sort for variables denoting nodes of derivation graphs. |
Logical variables. Variables with the same name and index but different sorts are regarded as different variables.
An alternative name for logical variables, which are intented to be
variables of sort LSortNode
.
type LTerm c = VTerm c LVarSource
Terms used for proving; i.e., variables fixed to logical variables.
type LNTerm = VTerm Name LVarSource
Terms used for proving; i.e., variables fixed to logical variables and constants to Names.
freshLVar :: MonadFresh m => String -> LSort -> m LVarSource
freshLVar v
represents a fresh logical variable with name v
.
sortPrefix :: LSort -> StringSource
sortPrefix s
is the prefix we use for annotating variables of sort s
.
sortSuffix :: LSort -> StringSource
sortSuffix s
is the suffix we use for annotating variables of sort s
.
sortCompare :: LSort -> LSort -> Maybe OrderingSource
sortCompare s1 s2
compares s1
and s2
with respect to the partial order on sorts.
Partial order: Node Msg
/ -- Pub Fresh
sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSortSource
Returns the most precise sort of an LTerm
.
sortOfLNTerm :: LNTerm -> LSortSource
Returns the most precise sort of an LNTerm
.
isFreshVar :: LNTerm -> BoolSource
Is a term a fresh variable?
isSimpleTerm :: LNTerm -> BoolSource
A term is *simple* iff there is an instance of this term that can be constructed from public names only. i.e., the term does not contain any fresh names, fresh variables, or private function symbols.
containsPrivate :: Term t -> BoolSource
containsPrivate t
returns True
if t
contains private function symbols.
neverContainsFreshPriv :: LNTerm -> BoolSource
True
iff no instance of this term contains fresh names or private function symbols.
Destructors
ltermVar :: LSort -> LTerm c -> Maybe LVarSource
Extract a variable of the given sort from a term that may be such a
variable. Use termVar
, if you do not want to restrict the sort.
ltermVar' :: Show c => LSort -> LTerm c -> LVarSource
Extract a variable of the given sort from a term that must be such a variable. Fails with an error, if that is not possible.
ltermNodeId :: LTerm c -> Maybe LVarSource
Extract a node-id variable from a term that may be a node-id variable.
ltermNodeId' :: Show c => LTerm c -> LVarSource
Extract a node-id variable from a term that must be a node-id variable.
bltermNodeId :: BLTerm -> Maybe LVarSource
Extract a node-id variable from a term that may be a node-id variable.
bltermNodeId' :: BLTerm -> LVarSource
Extract a node-id variable from a term that must be a node-id variable.
Manging Free LVars
HasFree t
denotes that the type t
has free LVar
variables. They can
be collected using foldFrees
and foldFreesOcc
and mapped in the context
of an applicative functor using mapFrees
.
When defining instances of this class, you have to ensure that only the free
LVars are collected and mapped and no others. The instances for standard
Haskell types assume that all variables free in all type arguments are free.
The foldFreesOcc
is only used to define the function varOccurences
. See
below for required properties of the instance methods.
Once we need it, we can use type synonym instances to parametrize over the variable type.
foldFrees :: Monoid m => (LVar -> m) -> t -> mSource
foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> mSource
mapFrees :: Applicative f => MonotoneFunction f -> t -> f tSource
HasFrees Bool | |
HasFrees Char | |
HasFrees Int | |
HasFrees Integer | |
HasFrees () | |
HasFrees LVar | |
HasFrees a => HasFrees [a] | |
HasFrees a => HasFrees (Maybe a) | |
(Ord a, HasFrees a) => HasFrees (Set a) | |
HasFrees a => HasFrees (Conj a) | |
HasFrees a => HasFrees (Disj a) | |
(HasFrees l, Ord l) => HasFrees (Term l) | |
HasFrees a => HasFrees (RRule a) | |
HasFrees a => HasFrees (Match a) | |
HasFrees a => HasFrees (Equal a) | |
HasFrees v => HasFrees (BVar v) | |
Ord c => HasFrees (LSubst c) | |
(HasFrees a, HasFrees b) => HasFrees (Either a b) | |
(HasFrees a, HasFrees b) => HasFrees (a, b) | |
(Ord k, HasFrees k, HasFrees v) => HasFrees (Map k v) | |
HasFrees v => HasFrees (Lit c v) | |
HasFrees (SubstVFresh n LVar) | |
(HasFrees a, HasFrees b, HasFrees c) => HasFrees (a, b, c) |
data MonotoneFunction f Source
occurs :: HasFrees t => LVar -> t -> BoolSource
v
iff variable occurs
tv
occurs as a free variable in t
.
frees :: HasFrees t => t -> [LVar]Source
frees t
is the sorted and duplicate-free list of all free variables in
t
.
someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m tSource
someInst t
returns an instance of t
where all free variables whose
binding is not yet determined by the caller are replaced with fresh
variables.
rename :: (MonadFresh m, HasFrees a) => a -> m aSource
rename t
replaces all variables in t
with fresh variables.
Note that the result is not guaranteed to be equal for terms that are
equal modulo changing the indices of variables.
eqModuloFreshnessNoAC :: (HasFrees a, Eq a) => a -> a -> BoolSource
eqModuloFreshness t1 t2
checks whether t1
is equal to t2
modulo
renaming of indices of free variables. Note that the normal form is not
unique with respect to AC symbols.
avoid :: HasFrees t => t -> FreshStateSource
avoid t
computes a FreshState
that avoids generating
variables occurring in t
.
evalFreshAvoiding :: HasFrees t => Fresh a -> t -> aSource
m
evaluates the monadic action evalFreshAvoiding
tm
with a
fresh-variable supply that avoids generating variables occurring in t
.
evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m aSource
m
evaluates the monadic action evalFreshTAvoiding
tm
in the
underlying monad with a fresh-variable supply that avoids generating
variables occurring in t
.
renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> sSource
s
replaces all free variables in renameAvoiding
ts
by
fresh variables avoiding variables in t
.
avoidPrecise :: HasFrees t => t -> FreshStateSource
avoidPrecise t
computes a FreshState
that avoids generating
variables occurring in t
.
renamePrecise :: (MonadFresh m, HasFrees a) => a -> m aSource
renamePrecise t
replaces all variables in t
with fresh variables.
If PreciseFresh
is used with non-AC terms and identical
fresh state, the same result is returned for two terms that only differ
in the indices of variables.
renameDropNamehint :: (MonadFresh m, MonadBind LVar LVar m, HasFrees a) => a -> m aSource
varOccurences :: HasFrees a => a -> [(LVar, Set Occurence)]Source
Returns the variables occuring in t
together with the contexts they appear in.
Note that certain contexts (and variables only occuring in such contexts) are
ignored by this function.
The function is used to guess renamings of variables, i.e., if t is a renaming of s,
then variables that occur in equal contexts in t and s are probably renamings of
each other.
BVar
Bound and free variables.
Monad BVar | |
Functor BVar | |
Typeable1 BVar | |
Applicative BVar | |
Foldable BVar | |
Traversable BVar | |
Apply BLTerm | |
Apply BLVar | |
Eq v => Eq (BVar v) | |
Data v => Data (BVar v) | |
Ord v => Ord (BVar v) | |
Show v => Show (BVar v) | |
Binary v_1627458273 => Binary (BVar v_1627458273) | |
NFData v_1627458273 => NFData (BVar v_1627458273) | |
HasFrees v => HasFrees (BVar v) |
Extract the name of free variable under the assumption the variable is
guaranteed to be of the form Free a
.
Pretty-Printing
prettyLVar :: Document d => LVar -> dSource
Pretty print a LVar
.
prettyNodeId :: Document d => NodeId -> dSource
Pretty print a NodeId
.
prettyNTerm :: (Show v, Document d) => NTerm v -> dSource
Pretty print an NTerm
.
prettyLNTerm :: Document d => LNTerm -> dSource
Pretty print an LTerm
.
Convenience exports
module Term.VTerm