why3-0.8: Haskell support for the Why3 input format.

Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Why3.Names

Description

Functions for working with names.

Synopsis

Documentation

countUses :: Expr -> Map Name Int Source

Count the uses of free names in an expression.

rename :: Set Name -> Expr -> Expr Source

Rename an expression to avoid all shadowing. The input parameters is a set of names that are already in scope and, therefore, should be renamed.

apSubst :: Map Name Expr -> Expr -> Expr Source

Apply a substitution to an exprssion. WARNING: This assumes that no capturing of variables will occur. This function treats names without arguments applied to them as the variables elligible for substitution.

freeNames :: Expr -> Set Name Source

Find free names in an expression