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

MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone

Term.LTerm

Contents

Description

Terms with logical variables and names.

Synopsis

Names

newtype NameId Source

Type safety for names.

Constructors

NameId 

Fields

getNameId :: String
 

type NTerm v = VTerm Name vSource

Terms with literals containing names and arbitrary variables.

Queries

sortOfName :: Name -> LSortSource

Return LSort for given Name.

Construction

freshTerm :: String -> NTerm vSource

freshTerm f represents the fresh name f.

pubTerm :: String -> NTerm vSource

pubTerm f represents the pub name f.

LVar

data LSort Source

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

  LSortFresh < LSortMsg
  LSortPub   < LSortMsg

Constructors

LSortPub

Arbitrary public names.

LSortFresh

Arbitrary fresh names.

LSortMsg

Arbitrary messages.

LSortNode

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.

Constructors

LVar 

type NodeId = LVarSource

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.

sortOfLit :: Lit Name LVar -> LSortSource

Returns the most precise sort of a Lit.

isMsgVar :: LNTerm -> BoolSource

Is a term a message variable?

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.

niFactors :: LNTerm -> [LNTerm]Source

The non-inverse factors of a term.

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

class HasFrees t whereSource

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.

Methods

foldFrees :: Monoid m => (LVar -> m) -> t -> mSource

foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> mSource

mapFrees :: Applicative f => MonotoneFunction f -> t -> f tSource

Instances

data MonotoneFunction f Source

For performance reasons, we distinguish between monotone functions on LVars and arbitrary functions. For a monotone f, if x <= y, then f x <= f y. 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.

Constructors

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.

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.

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.

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

data BVar v Source

Bound and free variables.

Constructors

Bound Integer

A bound variable in De-Brujin notation.

Free v

A free variable.

Instances

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) 

type BLVar = BVar LVarSource

LVars combined with quantified variables. They occur only in LFormulas.

type BLTerm = NTerm BLVarSource

Terms built over names and LVars combined with quantified variables.

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.

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