Module Types

module Types: sig  end

Module for type checking and type convertion

exception Type_error of string * Location.location

raised by functions of the types module to signal a type error in the input file.

• message
• location of the error

val equals : Abstract.eva_type -> Abstract.eva_type -> bool

type equality.

equals t1 t2
Returns whether the 2 given terms t1 and t2 are equal.

Note: We make no differences between user and base types, i.e. USERTYPE s and BASETYPE s are considered equal.

val type_lterm : Symbols.eva_symbol_list -> Abstract.eva_lterm -> Abstract.eva_type

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.

Raises

• Type_error if the given term
  • contains symbols not declared in sl
  • or is not well formed (arity) according sl
  • or is not well typed according to sl.
• Type_error if the given term contains alias symbols or some leaf symbol is not conform to symbol list sl.

Returns the type (not located) of the given located term t.

Note: the term t must NOT contain alias symbols

Note: this function should not be applied directly to terms obtained after parsing EVA protocol spec. Translator.convert_leterm (Translator.check_lterm) and Types.coerce_lterm should be applied first.

val type_lterm_laeva : Symbols.eva_symbol_list -> Abstract.eva_lterm -> Abstract.eva_type

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.
Raises

• Type_error if the given term
  • contains symbols not declared in sl
  • or is not well formed (arity) wrt sl
  • or is not well typed wrt sl as described above.
• Type_error if the given term contains alias symbols or some leaf symbol is not conform to the symbol list sl.

Returns the type (not located) of the given located term t.

Note: the term must NOT contain alias symbols

Note: this function should not be applied directly to terms obtained after parsing EVA protocol spec. Translator.convert_leterm (optionaly Translator.check_lterm) should be applied first.

Note: this function will likely fail when applied to coerced located terms as returned by Types.coerce_lterm (hence well typed terms wrt EVA semantics).

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

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,
Raises

• Type_error if the given term contains symbols not declared in sl or is not well formed (arity) according sl or is not well typed according to sl.
• Type_error if some leaf symbol in the given term t is not conform to symbol list sl.

Returns the casted copy.

Note: the symbols in the term t must be conform to the entries in symbol list sl, in particular this function should not be applied directly to terms obtained after parsing EVA protocol spec, see Translator.convert_lterm and Translator.check_lterm.

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

val cast : Abstract.eva_lterm -> Abstract.eva_type -> Abstract.eva_lterm

cast_term t ty

• param t a located term
• param ty an EVA type

Returns the term of type NUMBER obtained from t by applying the appropriate coercion function. NB: the coercion is not applied recursively.

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

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

Note: that the session (i.e. substitutions)\ do not need to be coerced because they are applied to coerced (typed) variable.