Language.Why3.Names

Functions for working with names.

Documentation

countUses :: Expr -> Map Name Int

Count the uses of free names in an expression.

rename :: Set Name -> Expr -> Expr

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

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

Find free names in an expression