Module LustreAstDependencies

Graph analysis on Lustre Ast Declarations.

We build a dependency graph of the lustre declarations to detect circular dependencies and reject them. We also reorder node and contract declarations to resolve forward references as backend cannot handle them.

Note Types of dependency analysis: There are two different kinds of graph dependency analysis and sorting done here.

1. Top level constants and type declarations (starts at sort_globals) We resolve all the forward references in this step.

2a. Nodes, functions and contracts (starts at sort_and_check_nodes_contracts) We resolve all the forward references in this step.

2b. Sort contract equations and perform cirularity check of node equations.

module LA = LustreAst
module IMap = HString.HStringMap
module IntMap : sig ... end
type error_kind =
  1. | Unknown of string
  2. | IdentifierRedeclared of HString.t
  3. | WidthLengthsUnequal of LA.expr * LA.expr
  4. | EquationWidthsUnequal
  5. | ContractDependencyOnCurrentOutput of LA.SI.t
  6. | CyclicDependency of HString.t list
  7. | ImportedCyclicDependency of HString.t list * NodeId.t
  8. | MismatchedDecreasesArity of HString.t list
  9. | RecursiveAnnotationWithoutRecursion of HString.t
type error = [
  1. | `LustreAstDependenciesError of Lib.position * error_kind
]
val error_message : error_kind -> string

Returns an message describing the error kind

type node_summary_entry = {
  1. imported : bool;
  2. dependencies : int list IntMap.t;
}
type node_summary = node_summary_entry NodeId.Map.t
val sort_globals : LA.t -> (LA.t, [> error ]) Stdlib.result

Returns a topological order to resolve forward references of globals. This step processes 1. type declarations, and 2. constant declarations

val sort_and_check_nodes_contracts : LA.t -> (LA.t * LA.ident list * int IMap.t * node_summary, [> error ]) Stdlib.result

Returns a topological order of declarations to resolve all forward references, with a list of toplevel nodes. It also reorders contract equations and checks for circularity of node equations. This step processes 1. nodes, 2. contracts and 3. functions