Index of values

add_symbol s sl

cast_term t ty param t a located term, param ty an EVA type

check_instrs_spec sl sp

check_linstr sl i

check_lterm rl sl lterm

check_ltype sl t

check_spec sl sp

coerce_lterm sl t typechecks the given located term t wrt the given symbol list sl and casts it to the type EVA_NUMBER (see Abstract.eva_type,

coerce_spec sl sp applies Types.coerce_lterm sl to every term of the given spec sp, except in (codomains of) sessions.

convert_ldcl sl d

convert_lstatement sl st

convert_lterm sl t

convert_spec sl sp applies the convertion functions Translator.convert_lterm, Translator.convert_ldcl, Translator.convert_lstatement to the elements of the given abstract specification sp, with the given symbol list sl, and return the specification obtained.

default location.

generic empty symbol list.

type equality.

report the given formatted error message on error output.

fold_left_symbollist f a sl

fold_right_symbollist f sl b

has_alias sl term

Do nothing.

prints on the given output channel the concatenation of the given string and of the given formatted message.

prints on the standard output the concatenation of the given string and of the given formatted message.

is_atomic_lterm t

is_atomic_term t

is_grounding s t returns true iff the domain of the given substitution s contains all the parameters and private variables of the term t.

Iterator for symbol lists.

lterm_replace_ldcl tr d

map_symbollist f sl

pp_list f sep l pretty print the list l of elements which are individualy pretty printed by the given function f, and separated by the the given separator printer sep.

printa the current location on the standard output

pretty print the given location on standard output.

merge locations.

subst_term s t returns the substitution of the given term t by the given substitution s.

symbollist_of_spec sp

flag for term right meaning that alias symbols are allowed in terms.

sum of all flags.

flag for term right meaning that located variables are allowed in terms.

flag for term rights meaning that constant symbols are allowed in terms (see Translator.check_lterm).

flag for term right meaning that first order symbols are allowed in terms.

flag for term right meaning that functional symbols are allowed in terms.

flag for term rights meaning that keypairs symbols are allowed in terms (see check_lterm)

flag for term rights meaning that parameters symbols are allowed in terms (see Translator.check_lterm).

flag for term right meaning that percent (Lowe's notation) are allowed in terms.

flag for term rights meaning that private variables are allowed in terms (see Translator.check_lterm).

flag for term right meaning that quantified variables are allowed in terms.

flag for term right meaning that value symbols are allowed in terms.

term_vars t returns the list (with repetitions) of identifiers of parameters and private variables in the given term t.

Print the given formatted message on the error output, if trace mode is on.

set trace mode off

set trace mode on

translate sl sp

type_lterm sl t checks that the given located term t is well typed wrt to the given symbol list sl according to the abstract syntax type discipline (see remark above): in EVA_APP(c, args), the terms of args must all have type EVA_NUMBER, in EVA_CONS(t, l), t must have type EVA_NUMBER, in EVA_CRYPT(a, k, t), a must have type EVA_SALGO and k and t must have type EVA_NUMBER.

type_lterm_laeva sl t checks the typing of the given located term t wrt to the given symbol list sl, according to the type discipline of LAEVA (aka concrete syntax) which is less resctrictive than the discipline for the abstract syntax (see remark above): in EVA_APP(c, args), the type of the terms of args must follow the declared signature of c,, in EVA_CONS(t, l), the type of t is not checked., in EVA_CRYPT(a, k, t), a must have type EVA_SALGO, the types of k and t are not checked. The purpose of this function is to check the terms obtained from the parser, after conversion with Translator.convert_lterm, and not yet casted, for conformity of terms against the type declaration of function symbols.

unalias_dcl sl d

unalias_ldcl sl d

unalias_lterm sl term

unalias_spec sl sp

report the given formatted warning message on error output.