tamarin-prover-term- Term manipulation library for the tamarin prover.

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone




Terms with logical variables and names.



data Name Source





nTag :: NameTag
nId :: NameId

newtype NameId Source

Type safety for names.




getNameId :: String

type NTerm v = VTerm Name vSource

Terms with literals containing names and arbitrary variables.


sortOfName :: Name -> LSortSource

Return LSort for given Name.


freshTerm :: String -> NTerm vSource

freshTerm f represents the fresh name f.

pubTerm :: String -> NTerm vSource

pubTerm f represents the pub name f.


data LSort Source

Sorts for logical variables. They satisfy the following sub-sort relation:

  LSortMsg   < LSortMSet
  LSortFresh < LSortMsg
  LSortPub   < LSortMsg



Arbitrary public names.


Arbitrary fresh names.


Arbitrary messages.


Sort for multisets.


Sort for variables denoting nodes of derivation graphs.

data LVar Source

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.

isMsgVar :: LNTerm -> BoolSource

Is a term a message variable?

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?

input :: LNTerm -> [LNTerm]Source

The required components to construct the message.

Manging Free LVars

class HasFrees t whereSource

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


data MonotoneFunction f Source

For performance reasons, we distinguish between monotone functions on LVars and arbitrary functions. The monotone functions much map LVars to equal or larger LVars. 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.


Monotone (LVar -> f LVar) 
Arbitrary (LVar -> f LVar) 

occurs :: HasFrees t => LVar -> t -> BoolSource

v occurs t iff variable v occurs as a free variable in t.

freesList :: HasFrees t => t -> [LVar]Source

freesList t is the list of all free variables of 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 evalFreshAvoiding t evaluates the monadic action m with a fresh-variable supply that avoids generating variables occurring in t.

evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m aSource

m evalFreshTAvoiding t evaluates the monadic action m 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 renameAvoiding t replaces all free variables in s by fresh variables avoiding variables in t.


data BVar v Source

Bound and free variables.


Bound Integer

A bound variable in De-Brujin notation.

Free v

A free variable.


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) 

foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> aSource

Fold a possibly bound variable.

fromFree :: BVar v -> vSource

Extract the name of free variable under the assumption the variable is guaranteed to be of the form Free a.


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