Module LustreContext

module LustreContext: sig .. end
Context information used in and obtained from parsing
Author(s): Christoph Sticksel

type t 
Context
exception Node_not_found of LustreIdent.t * Lib.position
Node or function not found, possible forward reference
exception Type_not_found of LustreIdent.t * Lib.position
exception Contract_not_found of LustreIdent.t * Lib.position

Scopes and Nodes


val mk_empty_context : unit -> t
Create an initial empty context.
val set_guard_flag : t -> bool -> t
Sets the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.
val reset_guard_flag : t -> t
Resets the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.
val guard_flag : t -> bool
The value of the flag indicating there are unguarded pre's in the lustre code, and we need to guard them.
val set_in_automaton : t -> bool -> t
Sets the flag indicating we are evaluating an automaton.
val reset_in_automaton : t -> t
Resets the flag indicating we are evaluating an automaton.
val in_automaton : t -> bool
The value of the flag indicating we are evaluating an automaton.
val push_scope : t -> string -> t
Add scope to context

The scopes are added to the name of the node to create scope for variables

val pop_scope : t -> t
Remove topmost scope from context
val push_contract_scope : t -> string -> t
Add contract scope to context.

Contract scopes are used for scoping of mode references and ghost variables.

val pop_contract_scope : t -> t
Remove topmost contract scope from context
val contract_scope_of : t -> string list
The contract scope of a context.
val scope_of_context : t -> string list
val create_node : t -> LustreIdent.t -> bool -> t
Return a copy of the context with an empty node of the given name and is extern flag in the context
val current_node_name : t -> LustreIdent.t option
Returns the name of the current node, if any.
val current_node_map : t -> (LustreNode.t -> LustreNode.t) -> t
Maps something to the current node.
val current_node_calls : t -> LustreNode.node_call list
Returns the calls made by the current node, if any.
val current_node_modes : t -> LustreContract.mode list option option
Returns the modes of the current node.
val create_function : t -> LustreIdent.t -> t
Return a copy of the context with an empty function of the given name in the context
val add_node_to_context : t -> t -> t
Return a context that is identical to the previous context with the node constructed in the current context added
val solve_fref : t ->
LustreAst.declaration ->
LustreDependencies.decl * LustreIdent.t * Lib.position ->
LustreAst.declaration list -> LustreAst.declaration list
Resolve a forward reference, fails if a circular dependency is detected.
val add_free_constant : t -> LustreIdent.t -> Var.t LustreIndex.t -> unit
Register a free constant, shadows previous declarations
val get_free_constants : t -> (LustreIdent.t * Var.t LustreIndex.t) list
Return declared free constants
val free_constant_expr_of_ident : t -> LustreIdent.t -> LustreExpr.t LustreIndex.t
Return the free constant corresponding to an identifier if any
val add_expr_for_ident : ?shadow:bool ->
t ->
LustreIdent.t -> LustreExpr.t LustreIndex.t -> t
Add a binding of an identifier to an expression to context

If the labeled argument shadow is true, allow overwriting a previous binding to the identifier. Otherwise raise the exception Invalid_argument "add_expr_for_ident".

val remove_expr_for_ident : t -> LustreIdent.t -> t
Remove the binding of an identifier from the context

If the identifier is not bound to an expression, raise the exception Invalid_argument "remove_expr_for_ident". Otherwise, remove the most recent binding to the identifier, which may make a previous binding visible, which was shadowed by a call to add_expr_for_ident with the labeled argument shadow set to true.

val add_type_for_ident : t -> LustreIdent.t -> Type.t LustreIndex.t -> t
Add a binding of an identifier to a type to context
val get_nodes : t -> LustreNode.t list
Return the nodes in the context
val get_node : t -> LustreNode.t option
Return the current node in context.
val prev : t -> t
return previous context
val get_state_var_bounds : t ->
LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t
Return state vars bounds hash table
val contract_nodes : t -> LustreAst.contract_node_decl list
The contract nodes in the context.
val trace_svars_of : t -> LustreExpr.t -> StateVar.StateVarSet.t option
The svars in the COI of the input expression, in the current node.

Returns None if there's no current node. Raises Not_found if some svars in the COI do not have an equation and are not outputs of node calls.

Used to check that the assumes and requires of a contract do not mention the outputs in LustreDeclarations.

val add_contract_node_decl_to_context : t ->
Lib.position * LustreAst.contract_node_decl -> t
Add a contract node to the context for inlining later
val contract_node_decl_of_ident : t -> string -> Lib.position * LustreAst.contract_node_decl
Return a contract node by its identifier
val fail_on_new_definition : t -> Lib.position -> string -> t
Return a context that raises an error when defining an expression.

fail_on_new_definition ctx pos msg will evaluate LustreContext.fail_at_position with the location pos and the message msg as arguments


Raise exception if no new definitions allowed

Raise A.ParseError with the message and position set by LustreContext.fail_on_new_definition. Raise an assertion failure if the context does allow new definitions.

val raise_no_new_definition_exc : t -> 'a
val expr_of_ident : t -> LustreIdent.t -> LustreExpr.t LustreIndex.t
Resolve an indentifier to an expression.
val assignable_state_var_of_ident : t -> LustreIdent.t -> StateVar.t LustreIndex.t
Return the respective state variable if the expression denotes an output or a local variable of the node in the context
val type_of_ident : t -> LustreIdent.t -> Type.t LustreIndex.t
Resolve an indentifier to a type.
val expr_in_context : t -> LustreIdent.t -> bool
Return true if the identifier denotes an expression in the context

Raise an Invalid_argument exception if the identifier is reserved.

val type_in_context : t -> LustreIdent.t -> bool
Return true if the identifier denotes a type in the context
val node_in_context : t -> LustreIdent.t -> bool
Return true if the identifier denotes a node in the context
val prop_name_in_context : t -> string -> bool
Return true if the identifier denotes a property in the context
val mk_state_var : ?is_input:bool ->
?is_const:bool ->
?for_inv_gen:bool ->
?shadow:bool ->
t ->
Ident.t list ->
LustreIdent.t ->
LustreIndex.index ->
Type.t -> LustreNode.state_var_source option -> StateVar.t * t
val mk_fresh_local : ?is_input:bool ->
?is_const:bool ->
?for_inv_gen:bool ->
?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
t -> Type.t -> StateVar.t * t
Create a fresh local state variable in the context.
val set_state_var_source : t ->
StateVar.t -> LustreNode.state_var_source -> t
val mk_local_for_expr : ?is_input:bool ->
?is_const:bool ->
?for_inv_gen:bool ->
?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
?is_ghost:bool ->
?original:LustreAst.expr ->
Lib.position ->
t -> LustreExpr.t -> LustreNode.equation_lhs * t
Define the expression with a fresh state variable, or the variable previously used for the same expression (if the optinal argument reuse is set to true), record the definition in the context and return the context.

The is_input, is_const and for_inv_gen flags are relevant, and the state variable returned has the combination of flags asked for. If a state variable was previously created for the same expression but with different flags, a new state variable is created.

val mk_fresh_oracle : ?is_input:bool ->
?is_const:bool ->
?for_inv_gen:bool ->
?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
t -> Type.t -> StateVar.t * t
Create a fresh oracle state variable in the context.
val mk_fresh_oracle_for_state_var : ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
t -> StateVar.t -> StateVar.t * t
Create a fresh oracle state variable for the pre-initial value of the given state variable in the context, or return a previously created oracle for this state variable.
val node_of_name : t -> LustreIdent.t -> LustreNode.t
Return the node of the given name from the context
val call_outputs_of_node_call : t ->
LustreIdent.t ->
LustreNode.call_cond list ->
StateVar.t LustreIndex.t ->
LustreExpr.t LustreIndex.t option -> StateVar.t LustreIndex.t option
Return variables capturing outputs of node call if a node call with the same input parameters and activation condition is in the context.

call_outputs_of_node_call c n ar i d compares all node calls in context c if the identifier of the node matches n, the activation or restart condition matches ar all input variables are idential to a, and all default values are identical to d. It returns None if no such call was found, and its output variables otherwise.

val add_node_input : ?is_const:bool ->
t -> LustreIdent.t -> Type.t LustreIndex.t -> t
Add node input to context
val add_node_output : ?is_single:bool ->
t ->
LustreIdent.t -> Lib.position -> Type.t LustreIndex.t -> t
Add node output to context
val outputs_of_current_node : t -> StateVar.t LustreIndex.t
The output state variables of the current node.
val add_node_local : ?ghost:bool ->
t ->
LustreIdent.t -> Lib.position -> Type.t LustreIndex.t -> t
Add node local to context
val add_node_ass : t -> LustreContract.svar list -> t
Adds assumptions to a node.
val add_node_gua : t -> (LustreContract.svar * bool) list -> t
Adds guarantees to a node (boolean is the candidate flag).
val add_node_mode : t -> LustreContract.mode -> t
Add modes to node
val add_node_assert : t -> LustreExpr.t -> t
Add assertion to context
val add_node_property : t ->
Property.prop_source -> string -> LustreExpr.t -> t
Add property to context
val add_node_equation : t ->
Lib.position ->
StateVar.t ->
LustreExpr.expr LustreExpr.bound_or_fixed list ->
int -> LustreExpr.t -> t
Add equation to context
val add_node_call : t -> Lib.position -> LustreNode.node_call -> t
Add node call to context
val set_node_main : t -> t
Mark node as main
val set_node_function : t -> t
Mark node as function
val get_node_function_flag : t -> bool
Checks if the current node, if any, is a function.
val close_expr : ?bounds:LustreExpr.expr LustreExpr.bound_or_fixed list ->
?original:LustreAst.expr ->
Lib.position ->
LustreExpr.t * t -> LustreExpr.t * t
Replace unguarded pre operators with oracle constants and return expression and modified context.

close_expr pos (expr, ctx) introduces or uses a previously introduced fresh oracle constant for each pre operator applied to a variable that is not under a ->.

The second argument is a pair so that it can take the output of LustreSimplify.eval_ast_expr directly.

val check_vars_defined : t -> unit
Check that the node being defined has no undefined local or output variables

Helpers


val fail_at_position : Lib.position -> string -> 'a
Output a fatal error at position and raise an error
val warn_at_position : Lib.position -> string -> unit
Output a warning at position
val fail_no_position : string -> 'a
Output a fatal error without reporting a position and raise an error
val warn_no_position : string -> unit
Output a warning without a position
val are_definitions_allowed : t -> bool
Returns true if new definitions are allowed in the context