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
- | LSortMSet
- | 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
- isMsgVar :: LNTerm -> Bool
- isFreshVar :: LNTerm -> Bool
- isSimpleTerm :: LNTerm -> Bool
- inputTerms :: LNTerm -> [LNTerm]
- 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
- 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
- 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:
LSortMsg < LSortMSet LSortFresh < LSortMsg LSortPub < LSortMsg
LSortPub | Arbitrary public names. |
LSortFresh | Arbitrary fresh names. |
LSortMsg | Arbitrary messages. |
LSortMSet | Sort for multisets. |
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 MSet
|
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 or fresh variables.
inputTerms :: LNTerm -> [LNTerm]Source
The required components to construct the message.
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 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.
Once we need it, we can use type synonym instances to parametrize over the variable type.
foldFrees :: Monoid m => (LVar -> m) -> 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
For performance reasons, we distinguish between monotone functions on
LVar
s and arbitrary functions. The monotone functions much map LVar
s to
equal or larger LVar
s. This ensures that the AC-normal form does not have
to be recomputed. If you are unsure about what to use, then use the
Arbitrary
function.
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.
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_1627481246 => Binary (BVar v_1627481246) | |
NFData v_1627481246 => NFData (BVar v_1627481246) | |
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