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.

type map_index_metadata =
  1. | MapDomain
  2. | MapValue

Metadata tag that distinguishes map-encoding entries from ordinary tuple fields within a TupleIndex.

type one_index =
  1. | RecordIndex of string
    (*

    Field name as index of a record

    *)
  2. | TupleIndex of int * map_index_metadata option
    (*

    Integer literal as index of a tuple, with an optional tag for map encoding entries. TupleIndex (i, None) is an ordinary Lustre tuple element at position i. TupleIndex (0, Some MapDomain) is the presence/domain array of a compiled map and prints as _0 in safe format. TupleIndex (1, Some MapValue) is the value array and prints as _1 in safe format.

    *)
  3. | ListIndex of int
    (*

    Integer literal as index of a list

    *)
  4. | ArrayIntIndex of int
    (*

    Integer literal as index of an array

    *)
  5. | ArrayVarIndex of LustreExpr.expr
    (*

    Variable as index of an array of given size

    *)
  6. | SetMapIndex of LustreExpr.expr
  7. | AbstractTypeIndex of string
    (*

    Index to the representation field of an abstract type

    *)
  8. | AdtTagIndex of string
    (*

    Discriminant field of a desugared ADT; string is the ADT type name

    *)
  9. | AdtPayloadIndex of string * int
    (*

    Payload field of a desugared ADT; ctor name and field position

    *)

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) -> (unit, 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 filter_array_indices : index -> index
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 pp_print_trie_ty : bool -> Stdlib.Format.formatter -> Type.t t -> unit
val mk_scope_for_index : index -> Scope.t