LustreIdentLustre identifier
An identifier is a string with a (possibly empty) list of integer indexes.
This module also provides some pre-defined identifiers that are used in the translation.
type t = private Ident.t * int listAn identifier is a string with integer indexes
val hash : t -> intHash an identifier
val string_of_ident : bool -> t -> stringReturn a string representation of the identifier
string_of_ident safe ident returns the identifier with the indexes appended in [ and ] if safe is false. Otherwise the indexes are appended separated by _, which makes the string a valid Lustre identifier.
val mk_string_ident : string -> tConstruct an identifier of a string
Return a scope of an identifier
The indexes of the identifier become separate scope levels.
val pp_print_ident : bool -> Stdlib.Format.formatter -> t -> unitPretty-print an identifier
pp_print_ident safe ident prints the indexes separated by _ if safe is true as in string_of_ident.
val reserved_scope : Scope.tScope for reserved identifiers
val user_scope : Scope.tScope for identifiers in user input
val abs_ident : tIdentifier for abstracted variables
val oracle_ident : tIdentifier for oracle inputs
val instance_ident : tIdentifier for unique identifier for node instance
val init_flag_ident : tIdentifier for first instant flag
val inst_ident : tIdentifier for instantiated variables in node calls
val eq_vars_ident : tIdentifier for variables stating two variables are equal so far
val index_ident : tIdentifier for index variables in arrays