Module `LustreIndex`

Indexes for lists, records, tuples and arrays in Lustre

In Lustre some indexes must be static at compile time, we can thus flatten all record, tuple and list values. The remaining indexes are array indexes, which we allow to be variable.

Array indexes are annotated with an expression denoting the bound. However, this bound is not considered when comparing array indexes, because two bounds of expressions can only be evaluated in a context. A syntactic comparison of bound expressions will fail to make expressions equal that should be equal, for example in node calls where the size of an input is parametrized by another input.

Lists in Lustre are similar to tuples, but they cannot be constructed, except as the inputs and outputs of node calls. Further, nested lists are to be flattened such that ((a, b), c), (a, (b, c)) and (a, b, c) are identical.

author: Christoph Sticksel

type one_index = | RecordIndex of string | TupleIndex of int | ListIndex of int | ArrayIntIndex of int | ArrayVarIndex of LustreExpr.expr | AbstractTypeIndex of string: An index element

type index = one_index list: A sequence of indexes

val pp_print_one_index : bool -> Stdlib.Format.formatter -> one_index -> unit: Pretty-print a single index

val pp_print_index : bool -> Stdlib.Format.formatter -> index -> unit: Pretty-print an list of indexes

val string_of_index : bool -> index -> string: Return a string representation of indexes

val empty_index : index: The empty index

A trie of indexes

include Trie.S with type key = index

type key = index: Type of keys in the trie

type +'a t: Type of the trie

val empty : 'a t: The empty trie

val is_empty : 'a t -> bool: Return true if the trie is empty

val mem : key -> 'a t -> bool: Return true if there is a value for the key in the trie

val add : key -> 'a -> 'a t -> 'a t

Bind a value to the key in the trie

Overwrite if the value if the leaf already exists, fail if the sequence of keys is a prefix of a previous sequence, or if a previous sequence is a prefix of the given sequence.

val remove : key -> 'a t -> 'a t

Remove key from trie

Do not fail if key does not exist.

val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int: Comparision function on tries

val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool: Equality predicate on tries

val iter : (key -> 'a -> unit) -> 'a t -> unit: Apply unit-valued function to each value in trie

val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b: Reduce trie to a value by applying the function to all values

val for_all : (key -> 'a -> bool) -> 'a t -> bool: Return true if the given predicate evaluates to true for all key value pairs in the trie

val exists : (key -> 'a -> bool) -> 'a t -> bool: Return true if there is a key value pair in the trie for which the given predicate evaluates to true

val filter : (key -> 'a -> bool) -> 'a t -> 'a t: Return a trie that only contains the key value pairs that satisfy the predicate

val cardinal : 'a t -> int: Return the number of bindings in the trie

val bindings : 'a t -> (key * 'a) list

Return an association list of key to bindings in the trie

The keys are returned in lexicographic order.

val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a: Return the value for the key in the trie

val map : ('a -> 'b) -> 'a t -> 'b t: Return a new trie with the function applied to the values

val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t

Return a new trie with the function applied to the values

The key is given as the first argument to the function.

val find_prefix : key -> 'a t -> 'a t: Return the subtrie starting at the given key prefix

val mem_prefix : key -> 'a t -> bool: Return true if there is a subtrie starting at the given key prefix

val keys : 'a t -> key list

Return the keys in the trie

The keys are returned in lexicographic order.

val values : 'a t -> 'a list

Return the values in the trie

The values are returned in lexicographic order.

val fold2 : (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c

Fold over two tries with identical keys

fold2 f t1 t2 a applies f to each pair of values in of t1 and t2 that have identical keys. The keys are presented in lexicographic order. Raise exception Invalid_argument "Trie.fold2" if the sets of keys the trie are not equal

val map2 : (key -> 'a -> 'b -> 'c) -> 'a t -> 'b t -> 'c t

Map over two tries with identical keys

map2 f t1 t2 applies f to each pair of values in of t1 and t2 that have identical keys and produces a new trie from the result. The keys are presented in lexicographic order. Raise exception Invalid_argument "Trie.map2" if the sets of keys the trie are not equal

val iter2 : (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit

Iterate over two tries with identical keys

iter2 f t1 t2 applies the unit valued function f to each pair of values in of t1 and t2 that have identical keys. The keys are presented in lexicographic order. Raise exception Invalid_argument "Trie.iter2" if the sets of keys the trie are not equal.

val for_all2 : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool

Check if all pairs of bindings in the trie satisfy the predicate

for_all2 p t1 t2 returns true if p evaluates to true for all pairs of bindings in t1 and t2 with identical keys. Raise exception Invalid_argument "Trie.for_all2" if the sets of keys the trie are not equal.

val exists2 : (key -> 'a -> 'b -> bool) -> 'a t -> 'b t -> bool

Check if there is a binding in the trie that satisfies the predicate

exists2 p t1 t2 returns true if p evaluates to true for at least one pair of bindings with identical keys in t1 andt2. Raise exception Invalid_argument "Trie.exists2" if the sets of keys the trie are not equal.

val subsume : 'a t -> key -> (key * 'a) list * 'a t

Return a new trie containing only entries with keys that are not subsets of the given key

subsume t k assumes that all keys in the trie t, and the key k are sorted and do not contain duplicates. It returns a new trie with all entries for keys that are subsets of k removed.

val is_subsumed : 'a t -> key -> bool

Return true if there is a key in the trie such that all elements of that key are in the given key.

is_subsumed t k assumes that all keys in the trie t, and the key k are sorted and do not contain duplicates.

val pp_print_trie : (Stdlib.Format.formatter -> (key * 'a) -> unit) -> ('b, Stdlib.Format.formatter, unit) Stdlib.format -> Stdlib.Format.formatter -> 'a t -> unit

Pretty-print bindings in the trie with a printer for key and value pairs

pp_print_trie f s p t prints to the formatter p all bindings of the trie in lexicographic order of the keys with the printer f for key and value pairs. Each binding is separated by the format string s.

val singleton : index -> 'a -> 'a t: Return a trie with a single element for the empty index

val equal_index : index -> index -> bool: Equality of indexes

val compare_indexes : index -> index -> int: Total order of indexes

Helper Functions

val array_bounds_of_index : index -> LustreExpr.expr list: Return the list of bounds of the array indexes in the index

val array_vars_of_index : index -> StateVar.t list: Return the list of array variables of the array indexes in the index

val top_max_index : 'a t -> int: If the first index is a list, return the greatest integer in a trie of indexes. Return (- 1) if the index is empty and fail with Invalid_argument "top_max_index" if the first index is not a list

val compatible_indexes : index -> index -> bool
val pp_print_index_trie : bool -> (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a t -> unit: Pretty print a trie of indexes

val pp_print_trie_expr : bool -> Stdlib.Format.formatter -> LustreExpr.t t -> unit: Pretty print a trie with expressions

val mk_scope_for_index : index -> Scope.t