Module LustreAstHelpers

Returns whether or not the expression is an Ident variant

Returns whether or not the expression is a Const variant

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

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

Returns the position of an expression

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

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.

Checks if the expression contains a call to a node

Checks if the expression contains a particular identifier

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)`

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.

apply_subst_in_expr s e applies the substitution defined by association list s to the expression e, including the expressions of the types it carries (e.g. explicit type arguments), as subst_in_type_exprs does. Bound variables introduced by match arms, quantifiers and any/choose are alpha-renamed when needed to avoid capture.

apply_subst_in_node_item s i applies the substitution defined by association list s to every expression of the node item i, leaving the left-hand sides of its equations alone. Bound variables introduced by match block arms and by the indices of an array definition shadow s over the expressions they scope, and those of a match block arm are alpha-renamed when needed to avoid capture.

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.

subst_in_type_exprs s t applies the substitution s to every expression of type t. A refinement type's binder shadows s in its predicate, and is alpha-renamed when a substituted expression would be captured by it.

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

Returns true if the expression has unguareded pre's

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

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

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

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

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

lazy_construct e returns the condition of e and the operands it guards, if e is a lazy construct: a when expression, and then, or else or ==>

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), within the restart conditions of restarted node calls, and within the conditions of the lazy constructs that guard node calls

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

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

expr_is_time_invariant is_invariant_var e holds when e contains no 'pre', '->' or node call, and every variable of e satisfies is_invariant_var. The normalizer rewrites 'pre (ai)' to '(pre a)i' only when this holds for i, and the syntax checks exempt such an index from the ban on quantified variables under 'pre', so is_invariant_var in the syntax checks must not accept a variable the normalizer rejects

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

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

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

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

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

vars_of_type ty returns all variable identifiers that appear in the type ty while excluding node call identifiers and refinement type bound variables. into_ty_args also descends into the type arguments of a user type

rename_self_referencing_binders ~expand tis e alpha-renames, in the quantifier binders tis and body e, each variable whose name occurs in a binder type, after expansion by expand, where it does not denote the quantified variable

Return an AST that adds two expressions

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

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

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

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

Returns true if the node input stream is a constant

returns true if it is a type or a constant declaration

Flatten group type structure

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

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

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

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

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

Sort typed identifiers

Sort identifiers

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.

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.

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.

name_mode_refs e replaces each mode reference in e by an identifier of the same name, and returns the references that were replaced, each with the position and path it was written at.

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

Get the name associated with a property

`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`

`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.

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

`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`

`constants_to_calls_in_type const_func_ids ty` applies constants_to_calls to the expressions of `ty`, except where a refinement type's bound variable shadows a constant

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

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

`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

`pos_of_type ty` returns the position of `ty`

The variables a pattern binds, each with the position it is bound at.

rename_pat_var i i' pat renames the variable i bound by pat to i'. Before type checking a variable pattern may name a nullary constructor rather than a binder, so a caller running that early must pass an i it knows is a binder.

A fresh name for an alpha-renamed binder, derived from its current name