Module LustreDesugarArrayComprehensions

Replace array comprehensions with fresh local variables defined by array definitions.

type error_kind =
  1. | BoundVariableInComprehension of HString.t
  2. | UnsupportedComprehensionPosition of string
  3. | ComprehensionConstantIn of HString.t * string
val error_message : error_kind -> string
type error = [
  1. | `LustreDesugarArrayComprehensionsError of Lib.position * error_kind
  2. | `LustreTypeCheckerError of Lib.position * LustreTypeChecker.error_kind
  3. | `LustreAstInlineConstantsError of Lib.position * LustreAstInlineConstants.error_kind
]

restore e replaces in e the fresh locals introduced by desugar_array_comprehensions with the comprehensions they stand for, as written, to print e as the user wrote it

val desugar_array_comprehensions : TypeCheckerContext.tc_context -> LustreAst.t -> (TypeCheckerContext.tc_context * LustreAst.t, [> error ]) Stdlib.result

Replace each array comprehension (e foreach i, j)^m^n in the body of a node or a function with a fresh local x defined by the equation x[i][j] = e, and each one in a contract with a fresh ghost variable defined element-wise in the same way. Equal comprehensions without calls share a variable in a node body, and in a contract. Returns the context with the ghost variables introduced in a contract node among its exports, which must be passed on, since they are looked up when the contract is imported. Returns an error for a comprehension in a type, a decreases clause or a ghost constant of a contract, and for one that mentions a variable bound around it. Must run after type checking and after inline_comprehension_constants.

val inline_comprehension_constants : LustreAst.t -> LustreAst.t -> (LustreAst.t * LustreAst.t, [> error ]) Stdlib.result

inline_comprehension_constants consts decls replaces in the nodes, functions and contracts of decls the constants whose definition contains an array comprehension, possibly through another such constant, with their definitions, and removes their declarations from the global constant declarations consts and from the local constants of the nodes. Returns an error if such a constant is used in a type, or in a ghost constant or a decreases clause of a contract, where a comprehension is not supported. Must run before desugar_array_comprehensions.