LustreAstHelpers (kind2dev@731decdf5fb1.LustreAstHelpers)

Helpers

val expr_is_id : LustreAst.expr -> bool

Returns whether or not the expression is an Ident variant

val expr_is_const : LustreAst.expr -> bool

Returns whether or not the expression is a Const variant

val expr_is_true : LustreAst.expr -> bool

Returns whether or not the expression is a Bool Const variant with the True value

val expr_is_false : LustreAst.expr -> bool

Returns whether or not the expression is a Bool Const variant with the False value

val pos_of_expr : LustreAst.expr -> Lib.position

Returns the position of an expression

val id_of_expr : LustreAst.expr -> HString.t option

Return a lustre id if the expression is an Ident variant or None otherwise

val expr_is_droppable : LustreAst.expr -> bool

Checks whether the expression can be deleted from the AST without losing a proof obligation. The check is a conservative whitelist: an expression form it does not explicitly recognize as droppable, including any form added later, is reported as not droppable. Answering false is always sound, so a new expression form only needs to be listed as droppable if the caller should be allowed to delete it.

val expr_contains_call : LustreAst.expr -> bool

Checks if the expression contains a call to a node

val expr_contains_id : LustreAst.ident -> LustreAst.expr -> bool

Checks if the expression contains a particular identifier

val type_arity : LustreAst.lustre_type -> int * int

Returns the arity of a type, a function (TArr) has arity `(a, b)` where `a` is the number of inputs and `b` is the number of outputs, every other type has arity `(0, 0)`

val substitute_naive : 
  HString.t ->
  LustreAst.expr ->
  LustreAst.expr ->
  LustreAst.expr

Substitute second param for first param in third param. Bound variables introduced by match arms, quantifiers and any/choose are alpha-renamed when needed to avoid capture.

val apply_subst_in_expr : 
  (HString.t * LustreAst.expr) list ->
  LustreAst.expr ->
  LustreAst.expr

apply_subst_in_expr s e applies the substitution defined by association list s to the expression e. Bound variables introduced by match arms, quantifiers and any/choose are alpha-renamed when needed to avoid capture.

val apply_subst_in_type : 
  (HString.t * LustreAst.expr) list ->
  LustreAst.lustre_type ->
  LustreAst.lustre_type

apply_subst_in_type s t applies the substitution defined by association list s to the expressions of (possibly dependent) type t AnyOp and Quantifier are not supported due to introduction of bound variables.

val apply_type_subst_in_type : 
  (HString.t * LustreAst.lustre_type) list ->
  LustreAst.lustre_type ->
  LustreAst.lustre_type

apply_type_subst_in_type s t applies the (type-level) substitution defined by association list s to type t.

val has_unguarded_pre : LustreAst.expr -> bool

Returns true if the expression has unguareded pre's

val has_unguarded_pre_no_warn : LustreAst.expr -> bool

Returns true if the expression has unguareded pre's. Does not print warning.

val has_pre_or_arrow : LustreAst.expr -> Lib.position option

Returns true if the expression has a `pre` or a `->`.

val contract_has_pre_or_arrow : LustreAst.contract -> Lib.position option

Returns true iff a contract mentions a `pre` or a `->`. Does not (cannot) check contract calls recursively, checks only inputs and outputs.

val node_local_decl_has_pre_or_arrow : 
  LustreAst.node_local_decl ->
  Lib.position option

Checks whether a node local declaration has a `pre` or a `->`.

val node_item_has_pre_or_arrow : LustreAst.node_item -> Lib.position option

Checks whether a node equation has a `pre` or a `->`.

val vars_of_node_calls : LustreAst.expr -> LustreAst.SI.t

vars_of_node_calls e returns all variable identifiers within arguments of node calls that appear in the expression e (while excluding node call identifiers)

val vars_without_node_call_ids : LustreAst.expr -> LustreAst.SI.t

vars_without_node_call_ids e returns all variable identifiers that appear in the expression e while excluding node call identifiers

val vars_without_node_call_ids_current : LustreAst.expr -> LustreAst.SI.t

vars_without_node_call_ids_current e is like vars_without_node_call_ids, but only those vars that are not under a 'pre' expression

val vars_of_struct_item_with_pos : 
  LustreAst.struct_item ->
  (Lib.position * LustreAst.index) list

returns all variables that appear in a struct_item (the lhs of an equation) with associated positions

val vars_of_struct_item : LustreAst.struct_item -> LustreAst.SI.t

returns all variables that appear in a struct_item (the lhs of an equation)

val defined_vars_with_pos : 
  LustreAst.node_item ->
  (Lib.position * LustreAst.index) list

returns all the variables that appear in the lhs of the equation of the node body with associated positions

val vars_of_ty_ids : LustreAst.typed_ident -> LustreAst.SI.t

returns a singleton set with the only identifier in a typed identifier declaration

val calls_of_expr : LustreAst.expr -> NodeId.Set.t

calls_of_expr e returns all node/function names for those nodes/functions called in e

val vars_of_type : LustreAst.lustre_type -> LustreAst.SI.t

vars_of_type ty returns all variable identifiers that appear in the type ty while excluding node call identifiers and refinement type bound variables

val add_exp : 
  Lib.position ->
  LustreAst.expr ->
  LustreAst.expr ->
  LustreAst.expr

Return an AST that adds two expressions

val abs_diff : 
  Lib.position ->
  LustreAst.expr ->
  LustreAst.expr ->
  LustreAst.expr

returns an AST which is the absolute difference of two expr ast

val extract_ip_ty : 
  LustreAst.const_clocked_typed_decl ->
  LustreAst.ident * LustreAst.lustre_type

returns the pair of identifier and its type from the node input streams

val extract_op_ty : 
  LustreAst.clocked_typed_decl ->
  LustreAst.ident * LustreAst.lustre_type

returns the pair of identifier and its type from the node output streams

val extract_loc_ty : 
  LustreAst.node_local_decl ->
  LustreAst.ident * LustreAst.lustre_type * LustreAst.expr option

returns the pair of identifier and its type from the node local streams

val is_const_arg : LustreAst.const_clocked_typed_decl -> bool

Returns true if the node input stream is a constant

val is_type_or_const_decl : LustreAst.declaration -> bool

returns true if it is a type or a constant declaration

val flatten_group_types : 
  LustreAst.lustre_type list ->
  LustreAst.lustre_type list

Flatten group type structure

val split_program : 
  LustreAst.declaration list ->
  LustreAst.declaration list * LustreAst.declaration list

Splits the program into two. First component are the type and constant declarations and Second component are the nodes, contract and function declarations.

val abstract_pre_subexpressions : LustreAst.expr -> LustreAst.expr

Abstracts out the pre expressions into a constant so that the built graph does not create a cycle.

val replace_idents : 
  LustreAst.index list ->
  LustreAst.index list ->
  LustreAst.expr ->
  LustreAst.expr

For every identifier, if that identifier is position n in locals1, replace it with position n in locals2

val extract_node_equation : 
  LustreAst.node_item ->
  (LustreAst.eq_lhs * LustreAst.expr) list

Extracts out all the node equations as an associated list of rhs and lhs of the equation

val get_last_node_name : LustreAst.declaration list -> NodeId.t option

Gets the name of the last node declared in the file.

val move_node_to_last : 
  NodeId.t ->
  LustreAst.declaration list ->
  LustreAst.declaration list

Moves the node with given name to the end of the list

val sort_typed_ident : LustreAst.typed_ident list -> LustreAst.typed_ident list

Sort typed identifiers

val sort_idents : LustreAst.ident list -> LustreAst.ident list

Sort identifiers

val syn_expr_equal : 
  int option ->
  LustreAst.expr ->
  LustreAst.expr ->
  (bool, unit) Stdlib.result

Check syntactic equality o Lustre expressions (ignoring positions) up to a certain optional depth. If the depth is reached, then Error () is returned, otherwise Ok false if the two expressions are unequal and Ok true if they are equal.

val syn_type_equal : 
  int option ->
  LustreAst.lustre_type ->
  LustreAst.lustre_type ->
  (bool, unit) Stdlib.result

Check syntactic equality of Lustre types (ignoring positions) up to a certain optional depth. If the depth is reached, then Error () is returned, otherwise Ok false if the two expressions are unequal and Ok true if they are equal.

val hash : int option -> LustreAst.expr -> int

Compute the hash of an AST expression to the given depth. After the depth limit is reached the same hash value is assigned to every sub expression. This function does not include position information in the hash.

val rename_contract_vars : LustreAst.expr -> LustreAst.expr

Rename contract variables from internal names (with format #_contract_var) to syntax names

val name_of_prop : 
  Lib.position ->
  HString.t option ->
  LustreAst.prop_kind ->
  HString.t

Get the name associated with a property

val get_const_num_value : LustreAst.expr -> int option

val fold_lustre_ty : 
  (LustreAst.expr -> 'a) ->
  'a ->
  ('a -> 'a -> 'a) ->
  LustreAst.lustre_type ->
  'a

`fold_lustre_ty f init op ty` folds over the type `ty` with initial value `init`, combining sub-results with `op` and collecting (sub-)results from Lustre expressions within the types with `f`

val fold_label_or_index : 
  'a ->
  ('a -> 'a -> 'a) ->
  (LustreAst.expr -> 'a) ->
  LustreAst.label_or_index list ->
  'a

`fold_label_or_index empty union f idx` folds `f` over the index expressions of a label_or_index list, as used in the update part of a StructUpdate (e.g. the key of a map update `mk := v`). A Label carries no expression and contributes `empty`; every other kind holds an arbitrary expression that may reference variables or node calls.

val map_lustre_ty : 
  (LustreAst.expr -> LustreAst.expr) ->
  LustreAst.lustre_type ->
  LustreAst.lustre_type

`map_lustre_ty f ty` applies function `f` to each Lustre expression within `ty`

val constants_to_calls : 
  LustreAst.ident list ->
  LustreAst.expr ->
  LustreAst.expr

`constants_to_calls const_func_ids expr` converts each constant `C` in `expr` to a call `C()`, provided that `C` is in `const_func_ids`

val contains_subtype_satisfying : 
  (LustreAst.lustre_type -> bool) ->
  LustreAst.lustre_type ->
  bool

`contains_subtype_satisfying p ty` returns true iff `ty` contains some subtype satisfying `p ty`

val is_direct_self_reference : LustreAst.ident -> LustreAst.lustre_type -> bool

`is_direct_self_reference type_name ty` returns true iff `ty` is a reference to the type named `type_name`

val is_directly_recursive_adt : 
  LustreAst.ident ->
  (LustreAst.ident * (LustreAst.ident * LustreAst.lustre_type) list) list ->
  bool

`is_directly_recursive_adt type_name ctors` returns true iff some constructor in `ctors` (the constructors of the ADT named `type_name`) directly references `type_name` in one of its fields

val pos_of_type : LustreAst.lustre_type -> Lib.position

`pos_of_type ty` returns the position of `ty`

val node_id_of_decl : LustreAst.declaration -> NodeId.t option

val is_recursive_function : LustreAst.declaration -> bool

val pat_bound_vars : LustreAst.pattern -> LustreAst.SI.t