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 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
- trivial :: LNTerm -> Bool
- input :: LNTerm -> [LNTerm]
- 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
- renamePrecise :: (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
- data BVar v
- foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a
- fromFree :: BVar v -> v
- prettyLVar :: Document d => LVar -> 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.
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?
trivial :: LNTerm -> BoolSource
Is a message trivial; i.e., can for sure be instantiated with something known to the intruder?
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.
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.
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
.
BVar
Bound and free variables.
Monad BVar | |
Functor BVar | |
Typeable1 BVar | |
Applicative BVar | |
Foldable BVar | |
Traversable BVar | |
Eq v => Eq (BVar v) | |
Data v => Data (BVar v) | |
Ord v => Ord (BVar v) | |
Show v => Show (BVar v) | |
Binary v_1627480102 => Binary (BVar v_1627480102) | |
NFData v_1627480102 => NFData (BVar v_1627480102) | |
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
.
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