Module LustreExpr

Internal reperesentation of a Lustre expression

A LustreExpr.t does not contain node calls, temporal operators or expressions under a pre operator.

There is exactly one -> operator at the top of the expression, thus an expression can be represented as a pair of expressions (i, t) without -> operators.

The argument of a pre operator is always a variable, therefore an expression pre x can be represented by the variable x at the previous state.

A non-variable expression under a pre has to be abstracted to a fresh variable that is defined by this expression. There are no node calls in a Lustre expression. They have to be abstracted out and the results are captured in fresh variables. See LustreAstNormalizer for details about how the input file is translated

The offsets of state variable instances are zero for the initial state and zero for the current state, see the constants base_offset and cur_offset and pre_offset. These are different from the offsets in the transition system, because here we want to know if the initial and the step expressions are equal without bumping offsets. Use the functions base_term_of_expr, cur_term_of_expr, and pre_term_of_expr to take the expression on one side of the -> operator and adjust to the variable offsets to the given base.

Expressions can only be constructed with the constructors which do type checking and some easy simplifications with constants.

exception Type_mismatch

Types of expressions do not match signature of operator

Types

type expr = private Term.t

A Term.t representing a Lustre expression, state variable offsets refer to the current and the previous instant.

Cannot be constructed outside this module to enforce invariants about allowed offsets of state variable instants, see the constructors below.

type 'a bound_or_fixed =
  1. | Bound of 'a
    (*

    Equation is for each value of the index variable between zero and the upper bound

    *)
  2. | Fixed of 'a
    (*

    Fixed value for index variable

    *)
  3. | Unbound of 'a option
    (*

    unbounded index variable

    *)

Type of index in an equation for an array

val type_of_expr : expr -> Type.t

Return the type of the expression

val equal_expr : expr -> expr -> bool

Equality of expressions

val is_true_expr : expr -> bool

Returns true iff the expr is the constant true.

type t = private {
  1. expr_init : expr;
    (*

    Lustre expression for initial state

    *)
  2. expr_step : expr;
    (*

    Lustre expression after initial state

    *)
  3. expr_type : Type.t;
    (*

    Common type of both initial and the step expression

    *)
}

A Lustre expression

The -> operator is moved to the top of the expression, the expression is to be interpreted as expr_init -> expr_step.

module LustreExprHashtbl : Stdlib.Hashtbl.S with type key = t

Hash table over Lustre expressions

val compare : t -> t -> int

Total order on lustre expressions

val compare_expr : expr -> expr -> int

Total order on expressions

val equal : t -> t -> bool

Equality of expressions

val hash : t -> int

Equality of expressions

val map : (int -> t -> t) -> t -> t

Tail-recursive bottom-up right-to-left map on the expression

val map_vars_expr : (Var.t -> Var.t) -> expr -> expr

Replace state variables in internal expression

val map_vars : (Var.t -> Var.t) -> t -> t

Replace state variables in expression

val type_of_lustre_expr : t -> Type.t

Return the type of the expression

Pretty-printers

All pretty-printers take a Boolean flag as first argument, indicating if identifiers should be valid Lustre identifiers. If the flag is false, indexed identifiers are printed with [, ] and .. These characters are replaced with _ if the flag is true.

val pp_print_bound_or_fixed : Stdlib.Format.formatter -> expr bound_or_fixed -> unit

Pretty-print a bound or fixed annotation

val pp_print_lustre_type : bool -> Stdlib.Format.formatter -> Type.t -> unit

Pretty-print a Lustre type

val pp_print_lustre_var : bool -> Stdlib.Format.formatter -> StateVar.t -> unit

Pretty-print a Lustre variable

val pp_print_lustre_var_typed : bool -> Stdlib.Format.formatter -> StateVar.t -> unit

Pretty-print a Lustre variable with its type

val pp_print_lustre_expr : bool -> Stdlib.Format.formatter -> t -> unit

Pretty-print a Lustre expression

val pp_print_expr : ?as_type:Type.t -> bool -> Stdlib.Format.formatter -> expr -> unit

Pretty-print a Lustre expression. The optional parameter as_type indicates that the expression should be printed as if it had this type (used for encoded enumerated datatypes).

val pp_print_lustre_expr_pvar : bool -> (Stdlib.Format.formatter -> StateVar.t -> unit) -> Stdlib.Format.formatter -> t -> unit
val pp_print_expr_pvar : ?as_type:Type.t -> bool -> (Stdlib.Format.formatter -> StateVar.t -> unit) -> Stdlib.Format.formatter -> expr -> unit
val pp_print_term_as_expr : ?as_type:Type.t -> bool -> Stdlib.Format.formatter -> Term.t -> unit

Pretty-print a term as an expr.

val pp_print_term_as_expr_pvar : ?as_type:Type.t -> bool -> (Stdlib.Format.formatter -> StateVar.t -> unit) -> Stdlib.Format.formatter -> Term.t -> unit

Pretty-print a term as an expr using the given printing function for state vars *

val pp_print_term_as_expr_mvar : ?as_type:Type.t -> bool -> string StateVar.StateVarMap.t -> Stdlib.Format.formatter -> Term.t -> unit

Pretty-print a term as an expr using the given map from state vars to strings If a state variable is not in the map, the name of the state variable is used instead

Predicates

val has_pre_var : Numeral.t -> t -> bool

Return true if the expression contains a previous state variable

val is_var : t -> bool

Return true if expression is a current state variable

val is_const_var : t -> bool

Return true if expression is a constant state variable

val is_pre_var : t -> bool

Return true if expression is a previous state variable

val pre_is_unguarded : t -> bool

Return true if there is an unguarded pre operator in the expression.

val is_const_expr : expr -> bool

Return true if the expression is constant

Conversions to terms

These offsets are different from the offsets in the transition system, because here we want to know if the initial and the step expressions are equal without bumping offsets. Use the constants base_offset, cur_offset or pre_offset of this module, or the constants TransSys.init_base and TransSys.trans_base for the zero offsets.

val base_offset : Numeral.t

Offset of state variable at first instant

val cur_offset : Numeral.t

Offset of state variable at current instant

val pre_offset : Numeral.t

Offset of state variable at previous instant

val base_var_of_state_var : Numeral.t -> StateVar.t -> Var.t

Instance of state variable at first instant with the given offset as zero

val cur_var_of_state_var : Numeral.t -> StateVar.t -> Var.t

Instance of state variable at current instant with the given offset as zero

val pre_var_of_state_var : Numeral.t -> StateVar.t -> Var.t

Instance of state variable at previous instant with the given offset as zero

val base_term_of_state_var : Numeral.t -> StateVar.t -> Term.t

Term of instance of state variable at first instant with the given offset as zero

val cur_term_of_state_var : Numeral.t -> StateVar.t -> Term.t

Term of instance of state variable at current instant with the given offset as zero

val pre_term_of_state_var : Numeral.t -> StateVar.t -> Term.t

Term of instance of state variable at previous instant with the given offset as zero

val base_term_of_expr : Numeral.t -> expr -> Term.t

Term at first instant with the given offset as zero

val cur_term_of_expr : Numeral.t -> expr -> Term.t

Term at current instant with the given offset as zero

val pre_term_of_expr : Numeral.t -> expr -> Term.t

Term at previous instant with the given offset as zero

val base_term_of_t : Numeral.t -> t -> Term.t

Term at first instant with the given offset as zero

val cur_term_of_t : Numeral.t -> t -> Term.t

Term at current instant with the given offset as zero

val pre_term_of_t : Numeral.t -> t -> Term.t

Term at previous instant with the given offset as zero

val state_var_of_expr : t -> StateVar.t

Return the state variable of a variable

Fail with Invalid_argument "state_var_of_expr" if the expression is not a variable at the current or previous offset.

val var_of_expr : t -> Var.t

Return the free variable of a expresion

Fail with Invalid_argument "var_of_expr" if the expression is not a free variable.

val var_of_init_expr : t -> Var.t

Return the free variable of the initial state expression

Fail with Invalid_argument "var_of_init_expr" if the initial state expression is not a free variable.

val state_vars_of_expr : t -> StateVar.StateVarSet.t

Return all state variables occurring in the expression in a set

val vars_of_expr : t -> Var.VarSet.t
val select_terms : t -> Term.TermSet.t

Return the terms of the form (select ...) that appear in a expression

val base_state_vars_of_init_expr : t -> StateVar.StateVarSet.t

Return all state variables of the initial state expression at the base instant

val cur_state_vars_of_step_expr : t -> StateVar.StateVarSet.t

Return all state variables of the step expression at the current instant

val indexes_of_state_vars_in_init : StateVar.t -> t -> expr list list
val indexes_of_state_vars_in_step : StateVar.t -> t -> expr list list
val split_expr_list : t list -> expr list * expr list

Split a list of Lustre expressions into a list of pairs of expressions for the initial step and the transition steps, respectively

val init_expr : t -> expr
val step_expr : t -> expr

Constants

val t_true : t

The propositional constant true

val t_false : t

The propositional constant false

Constructors

The constructors do some easy simplifcations, such as arithmetic and Boolean operations on constants. If the types of the arguments are do not match the signature of the symbol, the Type_mismatch exception is raised.

val mk_constr : string -> Type.t -> t

Return a constructor

val mk_int : Numeral.t -> t

Return an expression of an integer numeral.

val mk_real : Decimal.t -> t

Return an expression of a floating point decimal.

val mk_var : StateVar.t -> t

Return an expression of a variable.

val mk_free_var : Var.t -> t
val mk_array_index_var : int -> Type.t -> t

Return an expression for the i-th array index variable.

val int_of_index_var : t -> int

Return the number/position of the index variable.

val has_indexes : t -> bool

Returns true if the expression has index variables.

val mk_to_int : t -> t

Return a conversion to an integer numeral.

val mk_to_ubv : int -> t -> t

Return a conversion to an unsigned machine int.

val mk_to_bv : int -> t -> t

Return a conversion to a signed machine int.

val mk_to_real : t -> t

Return a conversion to a floating-point decimal.

val mk_ite : t -> t -> t -> t

Return an if-then-else expression.

val mk_not : t -> t

Return the Boolean negation of the expression.

val mk_uminus : t -> t

Return the unary minus of the expression.

val mk_bvnot : t -> t

Return the bitwise negation of the expression

val mk_and : t -> t -> t

Return the Boolean conjunction of the two expressions.

val mk_and_n : t list -> t

Return the Boolean conjunction of the list of expressions.

val mk_or : t -> t -> t

Return the Boolean disjunction of the two expressions.

val mk_or_n : t list -> t

Return the Boolean disjunction of the list of expressions.

val mk_xor : t -> t -> t

Return the Boolean exclusive disjunction of the two expressions.

val mk_impl : t -> t -> t

Return the Boolean implication of the two expressions.

val mk_forall : Var.t list -> t -> t

Return the universal quantification of an expression.

val mk_exists : Var.t list -> t -> t

Return the existential quantification of an expression.

val mk_mod : t -> t -> t

Return the integer modulus of the two expressions.

val mk_minus : t -> t -> t

Return the difference of the two expressions.

val mk_plus : t -> t -> t

Return the sum of the two expressions.

val mk_div : t -> t -> t

Return the quotient of the two expressions.

val mk_times : t -> t -> t

Return the product of the two expressions.

val mk_intdiv : t -> t -> t

Return the integer quotient of the two expressions.

val mk_bvand : t -> t -> t

Return the bitvector conjunction of the two expressions.

val mk_bvconcat : t -> t -> t

Return the bitvector concatenation of the two expressions.

val mk_bvextract : int -> int -> t -> t

Return the bitvector extraction of the third argument and the indices of the first and third expressions

val mk_bvor : t -> t -> t

Return the bitvector disjunction of the two expressions.

val mk_bvshl : t -> t -> t

Return the bitvector left shift of the two expressions.

val mk_bvshr : t -> t -> t

Return the bitvector right shift of the two expressions.

val mk_eq : t -> t -> t

Return the equality relation on the two expressions.

val mk_neq : t -> t -> t

Return the disequality relation on the two expressions.

val mk_lte : t -> t -> t

Return the less-than-or-equal relation on the two expressions.

val mk_lt : t -> t -> t

Return the less-than relation on the two expressions.

val mk_gte : t -> t -> t

Return the greater-than-or-equal relation on the two expressions.

val mk_gt : t -> t -> t

Return the greater-than relation on the two expressions.

val mk_arrow : t -> t -> t

Apply the followed by operator -> to the two expressions.

val mk_pre : t -> t

mk_pre e returns the expression e if it is a constant, and the previous state variable if the expression is a current state variable.

val mk_pre_with_context : ('a -> t -> 'b * 'a) -> ('b -> Term.t) -> 'a -> bool -> t -> t * 'a

Apply the pre operator to the expression, abstract the expression to a fresh variable if it is not a variable at the current state.

mk_pre_with_context f c b e returns the expression e and context c unchanged if it is a constant, and the previous state variable if the expression is a current state variable, again together with c unchanged.

Otherwise the expression e is abstracted to a fresh variable obtained by calling the function f, which returns a fresh state variable and a changed context c that records the association between the fresh variable and the expression. Then return an expression of the fresh state variable and the changed context.

b is used to denote that we're in a context where there are unguarded pres and so we should always introduce fresh intermediate variables.

val mk_select : t -> t -> t

Select from an array

val is_select : t -> bool

Returns true if the expression is a selection in an array

val is_select_array_var : t -> bool

Returns true if the expression is a selection of an array variable

val var_of_array_select : t -> Var.t
val indexes_and_var_of_array_select : t -> Var.t * expr list
val mk_store : t -> t -> t -> t

Store in an array

val is_store : t -> bool

Returns true if this is a store in an array

val mk_let_cur : (StateVar.t * t) list -> t -> t

Substitute state variable at current instant with expression

val mk_let_pre : (StateVar.t * t) list -> t -> t

Substitute state variable at previous instant with expression

val mk_int_expr : Numeral.t -> expr

Return an expression of a numeral

val mk_of_expr : ?as_type:Type.t -> expr -> t

Return an expression with the same term on both sides of the ->

val is_const : t -> bool

Return true if the expression is constant

val is_numeral : expr -> bool
val numeral_of_expr : expr -> Numeral.t
val unsafe_term_of_expr : expr -> Term.t
val unsafe_expr_of_term : Term.t -> expr
val mk_uf : UfSymbol.t -> Type.t -> t list -> t

Build a UF application expression with given return type and arguments

val mk_is_constructor : string -> t -> t

Build an ADT tester expression: ((_ is CtorName) e)

val mk_selector : string -> Type.t -> t -> t

Build an ADT selector expression: (CtorName_i e) with the given result type

val mk_array : t -> t -> t
val mk_const_array : Type.t -> t -> t
val mk_let : (Var.t * expr) list -> t -> t
val apply_subst : (Var.t * expr) list -> t -> t
val push_select : t -> t

Return an expression where the top-level selects of the initial and/or the step expressions (if any) have been pushed

val mk_select_and_push : t -> t -> t

Make select from an array and push it