Module `LustreContext`

Context information used in and obtained from parsing

author: 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 fail_at_position with the location pos and the message msg as arguments

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 -> ?⁠reuse:bool -> ?⁠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 -> Lib.position -> StateVar.t -> t: Add assertion to context

val add_node_sofar_assumption : t -> t
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