Module Translator

module Translator: sig  end

Module for

• checking a specification in abstract syntax
• and translating a specification a la BAN (several processes in a single message list) into a multi processes specification.

exception Translator_error of string * Location.location

raised by functions the module translator to signal an error in the input file.

• message
• location of the error

val symbollist_of_spec : Abstract.eva_spec -> Symbols.eva_symbol_list

symbollist_of_spec sp
Returns the symbol list extracted from:

• the declarations (field Abstract.eva_spec.sp_declarations) of the given specification sp
• the value declarations (field Abstract.eva_spec.sp_valuedcl) of the given eva_spec.

Note: the other identifiers (quantified identifiers in axioms or formulas and private process variables) are not included in the symbol list.

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

convert_lterm sl t
Raises Translator_error if the given term t contains an unexpected symbol or undeclared symbol i in a subterm EVA_TERM_ID i.
Returns a located term obtained from the given located term t, which must be a term returned by the parser, by conversion of the symbols at the leaves, using the given symbol list sl.

The parser cannot distinguish between identifiers in terms which are first order ids, values, alias or quantified variables. Hence, after parsing, every identifier (string) i occurring in a term is stored in a EVA_TERM_ID i (see Abstract.eva_term), whatever its declaration. This function restores the given located term t obtained from parser by converting every leaf EVA_TERM_ID into EVA_TERM_ID, EVA_TERM_VALUE or EVA_TERM_ALIAS or EVA_QUANTIFIED according to the given symbol list sl, and returns the terms obtained.

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

convert_ldcl sl d
Raises Translator_error if the types of left and right members of an axiom differ or if d contains an undeclared symbol.
Returns a located declaration obtained from the given located declaration d (returned by the parser) and which conforms to the abstract syntax according to the given symbol list sl.

• conversion of axiom declarations: The members of the axiom are converted (Translator.convert_lterm) with to the given symbol list overwritten by the quantified variables. This function evaluates then and adds the type of the axiom members (the type of the members of an axiom is not required in the LAEVA concrete syntax but is required in the abstract syntax).

• conversion of others declarations: the function Translator.convert_lterm is applied to every embedded term.

val convert_lstatement : Symbols.eva_symbol_list -> Abstract.eva_lstatement -> Abstract.eva_lstatement

convert_lstatement sl st
Returns a located statement obtained from the given located statement st (returned by the parser). and which conforms to the abstract syntax according to the given symbol list sl.

The function Translator.convert_lterm is applied to the terms of the statement, with the symbol list sl overwritten by the quantified variables.

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

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.

val term_VALUE : int

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

val term_CST : int

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

val term_PARAM : int

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

val term_PRIV : int

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

val term_PCENT : int

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

val term_AT : int

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

val term_FO : int

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

val term_FUN : int

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

val term_KEY : int

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

val term_ALIAS : int

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

val term_QUANTIF : int

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

val term_ALL : int

sum of all flags.

val check_ltype : Symbols.eva_symbol_list -> Abstract.eva_ltype -> Abstract.eva_ltype

check_ltype sl t
Raises Translator_error otherwise.
Returns the given located type t if it is well formed w.r.t. the given symbol list sl.

val check_lterm : int list ->
       Symbols.eva_symbol_list -> Abstract.eva_lterm -> Abstract.eva_lterm

check_lterm rl sl lterm
Raises Translator_error otherwise.
Returns the given located term lterm if its leaves are correct w.r.t. the given rights list rl and the given symbol list sl. The right list is a list of flags defining which symbols are allowed in terms.

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

check_spec sl sp
Returns the spec obtained by applying the function Translator.check_lterm to every term of the given spec sp, with different rights.

val check_linstr : Symbols.eva_symbol_list -> Abstract.eva_linstr -> Abstract.eva_linstr

check_linstr sl i
Raises Translator_error otherwise
Returns the given located instruction i if the identifiers sender and receiver of messages or roles of comp and assignment are declared as principal.

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

check_instrs_spec sl sp
Returns the given located specification sp if checking of all the instructions it contains, applying Translator.check_linstr with the given symbol list sl, is successful.

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

translate sl sp
Returns a protocol specification where the messages are presented in separates processes given a symbol list sl and a protocol specification sp, where the messages are presented a la BAN. The other fields of the specification are left untouched