Module Alias

module Alias: sig  end

Control and replacement of alias symbols in terms and protocol specifications.

exception Alias_error of string * Location.location

raised by functions the alias module to signal errors in the input file concerning aliases.

message
location of the error

val has_alias : Symbols.eva_symbol_list -> Abstract.eva_lterm -> bool

has_alias sl term
Returns true if the given located term term contains a symbol registered as an alias in the given symbol list sl. Returns false otherwise.

NB: It is assumes that only the leaves of the form EVA_TERM_ID and EVA_TERM_ALIAS (see Abstract.eva_term) can contain alias symbols.

val unalias_lterm : Symbols.eva_symbol_list -> Abstract.eva_lterm -> Abstract.eva_lterm

unalias_lterm sl term
Returns the term obtained by replacement of the aliases in the given located term term, according to the given symbol list sl.

val unalias_ldcl : Symbols.eva_symbol_list -> Abstract.eva_ldcl -> Abstract.eva_ldcl

unalias_ldcl sl d
Returns the given located declaration d after unaliasing the terms it contains, only if the declaration is not an alias declaration.

val unalias_dcl : Symbols.eva_symbol_list -> Abstract.eva_dcl -> Abstract.eva_dcl

unalias_dcl sl d
Returns the given declaration d after unaliasing the terms it contains, only if the declaration is not an alias declaration.

val unalias_spec : Symbols.eva_symbol_list -> Abstract.eva_spec -> Abstract.eva_spec

unalias_spec sl sp
Returns the given abstract specification sp after unaliasing all the terms it contains, except in the alias declarations