Module LustreAst

Minimally simplified Lustre abstract syntax tree

The types in this module closely represent the abstract syntax of Lustre. No type checking or simplification is performed when constructing the abstract syntax tree, this is done when producing the intermediate Lustre representation in LustreNodeGen.

Some values are reserved for future use and will cause the translation to intermediate Lustre to fail.

A Lustre file is parsed into a declaration list, where a declaration is either

Almost all types are annotated with the position in the input file for better error reporting in the translation.

module NI = NodeId
exception Parser_error

Error while parsing

Types

type ident = HString.t

An identifier

module SI : sig ... end
type index = HString.t

A single index

type clock_expr =
  1. | ClockTrue
  2. | ClockPos of ident
  3. | ClockNeg of ident
  4. | ClockConstr of ident * ident

A clock expression

type conversion_operator =
  1. | ToInt
  2. | ToReal
  3. | ToBV of int
  4. | ToUBV of int
type unary_operator =
  1. | Not
  2. | Uminus
  3. | BVNot
type in_kind =
  1. | Unknown
  2. | Map
  3. | Set
type binary_operator =
  1. | And
  2. | AndThen
  3. | Or
  4. | OrElse
  5. | Xor
  6. | Impl
  7. | LazyImpl
  8. | In of in_kind
  9. | Mod
  10. | Minus
  11. | Plus
  12. | Div
  13. | Times
  14. | IntDiv
  15. | BVAnd
  16. | BVOr
  17. | BVShiftL
  18. | BVShiftR
  19. | BVConcat
  20. | Union
  21. | Intersection
  22. | Difference
type ternary_operator =
  1. | Ite
  2. | LazyIte
type comparison_operator =
  1. | Eq
  2. | Neq
  3. | Lte
  4. | Lt
  5. | Gte
  6. | Gt
type constant =
  1. | True
  2. | False
  3. | Num of HString.t
  4. | Dec of HString.t
type quantifier =
  1. | Forall
  2. | Exists
type group_expr =
  1. | ExprList
  2. | TupleExpr
  3. | ArrayExpr
type access_kind =
  1. | Array
  2. | Map
  3. | Tuple
  4. | Unknown
type struct_update_index_kind =
  1. | TupleSlot
  2. | ArrayElem

Whether an Index within a structural update (StructUpdate) replaces a tuple slot or an array element.

type selector_origin =
  1. | UserWritten
  2. | Kind2Generated

Only user-written selectors carry a proof obligation

type pattern =
  1. | VarPat of Lib.position * ident
    (*

    variable binding

    *)
  2. | Pat of Lib.position * ident * pattern list
    (*

    constructor pattern

    *)

Pattern for match expressions

type lustre_type =
  1. | Bool of Lib.position
  2. | Int of Lib.position
  3. | SBitVector of Lib.position * int
  4. | UBitVector of Lib.position * int
  5. | Real of Lib.position
  6. | UserType of Lib.position * lustre_type list * ident
  7. | AbstractType of Lib.position * ident
  8. | TupleType of Lib.position * lustre_type list
  9. | GroupType of Lib.position * lustre_type list
  10. | RecordType of Lib.position * ident * typed_ident list
  11. | ArrayType of Lib.position * lustre_type * expr
  12. | EnumType of Lib.position * ident * ident list
  13. | History of Lib.position * ident
  14. | TArr of Lib.position * lustre_type * lustre_type
  15. | RefinementType of Lib.position * typed_ident * expr
  16. | Map of Lib.position * lustre_type * lustre_type
  17. | Set of Lib.position * lustre_type
  18. | ADT of Lib.position * ident * (ident * (ident * lustre_type) list) list

A Lustre type

and proj_kind =
  1. | Unresolved
  2. | RecordField
    (*

    Origin, the ADT type, and the constructor whose payload holds the field.

    *)
  3. | Selector of selector_origin * lustre_type * ident
and expr =
  1. | Ident of Lib.position * ident
  2. | ModeRef of Lib.position * ident list
  3. | FieldProject of Lib.position * expr * index * proj_kind
  4. | Const of Lib.position * constant
  5. | UnaryOp of Lib.position * unary_operator * expr
  6. | BinaryOp of Lib.position * binary_operator * expr * expr
  7. | TernaryOp of Lib.position * ternary_operator * expr * expr * expr
  8. | ConvOp of Lib.position * conversion_operator * expr
  9. | CompOp of Lib.position * comparison_operator * expr * expr
  10. | AnyOp of Lib.position * typed_ident * expr
  11. | ChooseOp of Lib.position * typed_ident * expr
  12. | Extract of Lib.position * expr * int * int
  13. | RecordExpr of Lib.position * ident * lustre_type list * (ident * expr) list
  14. | GroupExpr of Lib.position * group_expr * expr list
  15. | StructUpdate of Lib.position * expr * label_or_index list * expr option
  16. | EmptyMap of Lib.position * (lustre_type * lustre_type) option
  17. | EmptySet of Lib.position * lustre_type option
  18. | ArrayConstr of Lib.position * expr * expr
  19. | IndexAccess of Lib.position * expr * expr * access_kind
  20. | Quantifier of Lib.position * quantifier * typed_ident list * expr
  21. | When of Lib.position * expr * clock_expr
  22. | Condact of Lib.position * expr * expr * NI.t * expr list * expr list
  23. | Activate of Lib.position * NI.t * expr * expr * expr list
  24. | Merge of Lib.position * ident * (ident * expr) list
  25. | RestartEvery of Lib.position * NI.t * expr list * expr
  26. | Pre of Lib.position * expr
  27. | Arrow of Lib.position * expr * expr
  28. | Last of Lib.position * ident
  29. | Call of Lib.position * lustre_type list * NI.t * expr list
  30. | TypeAscription of Lib.position * expr * lustre_type
  31. | ADTTerm of Lib.position * lustre_type list * ident * expr list
  32. | Match of Lib.position * expr * (pattern * expr) list * lustre_type option
    (*

    Symbolic default value for an abstract type, used as a junk payload field in desugared ADTs.

    *)
  33. | AbstractSymConst of Lib.position * lustre_type
  34. | ADTTester of Lib.position * expr * ident

A Lustre expression

and typed_ident = Lib.position * ident * lustre_type

An identifier with a type

and label_or_index =
  1. | Label of Lib.position * index
  2. | Index of Lib.position * expr * struct_update_index_kind
    (*

    Set by the type checker from the updated expression's type: whether this replaces a whole tuple slot or a single array element.

    *)
  3. | MapIndex of Lib.position * expr
  4. | SetIndex of Lib.position * expr
  5. | GenericIndex of Lib.position * expr

A record field or an array or tuple index

Declarations

type type_decl =
  1. | AliasType of Lib.position * ident * ident list * lustre_type
  2. | FreeType of Lib.position * ident

A declaration of an alias or free type

type clocked_typed_decl = Lib.position * ident * lustre_type * clock_expr

An identifier with a type and a clock as used for the type of variables

type const_clocked_typed_decl = Lib.position * ident * lustre_type * clock_expr * bool

An identifier, possibly flagged as constant, with a type and a clock as used for the type of variables

type const_decl =
  1. | FreeConst of Lib.position * ident * lustre_type
  2. | UntypedConst of Lib.position * ident * expr
  3. | TypedConst of Lib.position * ident * expr * lustre_type

A constant declaration

type node_local_decl =
  1. | NodeConstDecl of Lib.position * const_decl
  2. | NodeVarDecl of Lib.position * clocked_typed_decl

A local constant or variable declaration of a node

type struct_item =
  1. | SingleIdent of Lib.position * ident
  2. | TupleStructItem of Lib.position * struct_item list
  3. | TupleSelection of Lib.position * ident * expr
  4. | FieldSelection of Lib.position * ident * ident
  5. | ArraySliceStructItem of Lib.position * ident * (expr * expr) list
  6. | ArrayDef of Lib.position * ident * ident list

Structural assignment on the left-hand side of an equation

type eq_lhs =
  1. | StructDef of Lib.position * struct_item list

The left-hand side of an equation

type contract_eq_lhs =
  1. | GhostVarDec of Lib.position * typed_ident list
type node_equation =
  1. | Assert of Lib.position * expr
  2. | Equation of Lib.position * eq_lhs * expr

An equation or assertion in the node body

type prop_bound =
  1. | From of int
  2. | Within of int
  3. | At of int
  4. | FromWithin of int * int

For reachable properties, the user can optionally specify a bound to look for a witness from/within/at a certain timestep

type prop_kind =
  1. | Invariant
  2. | Reachable of prop_bound option
  3. | Provided of expr

Whether a property is reachable or invariant

type node_item =
  1. | Body of node_equation
  2. | IfBlock of Lib.position * expr * node_item list * node_item list
  3. | WhenBlock of Lib.position * expr * node_item list * node_item list
  4. | FrameBlock of Lib.position * (Lib.position * ident) list * node_equation list * node_item list
  5. | AnnotMain of Lib.position * bool
  6. | AnnotProperty of Lib.position * HString.t option * expr * prop_kind
  7. | Auto of Lib.position
    (*

    No-op item, only allowed in the body of a lemma

    *)

An item in a node declaration

type contract_ghost_const = const_decl
type contract_ghost_vars = Lib.position * contract_eq_lhs * expr
type contract_assume = Lib.position * HString.t option * bool * expr
type contract_guarantee = Lib.position * HString.t option * bool * expr
type contract_require = Lib.position * HString.t option * expr
type contract_ensure = Lib.position * HString.t option * expr
type contract_mode = Lib.position * ident * contract_require list * contract_ensure list
type contract_call = Lib.position * NI.t * lustre_type list * expr list * ident list
type contract_assump_vars = Lib.position * (Lib.position * HString.t) list
type decreases_clause = Lib.position * expr
type contract_node_equation =
  1. | GhostConst of contract_ghost_const
  2. | GhostVars of contract_ghost_vars
  3. | Assume of contract_assume
  4. | Guarantee of contract_guarantee
  5. | Mode of contract_mode
  6. | ContractCall of contract_call
  7. | AssumptionVars of contract_assump_vars
  8. | Decreases of decreases_clause
type contract = Lib.position * contract_node_equation list
type opacity =
  1. | Default
  2. | Opaque
  3. | Transparent
type node_decl = NI.t * bool * opacity * ident list * const_clocked_typed_decl list * clocked_typed_decl list * node_local_decl list * node_item list * contract option

Declaration of a node or function as a tuple of

  • its identifier,
  • a flag, true if the node / function is extern
  • its opacity
  • its type parameters,
  • the list of its inputs,
  • the list of its outputs,
  • the list of its local constant and variable declarations,
  • its equations, assertions and annotiations, and
  • its optional contract specification
type contract_node_decl = NI.t * ident list * const_clocked_typed_decl list * clocked_typed_decl list * contract

A contract node declaration as a tuple of

  • its identifier,
  • its type parameters,
  • its inputs,
  • its outputs,
  • its body as a contract.
type node_param_inst = ident * ident * lustre_type list

An instance of a parametric node as a tuple of the identifier for the instance, the identifier of the parametric node and the list of type parameters

type span = {
  1. start_pos : Lib.position;
  2. end_pos : Lib.position;
}
type func_attrs = {
  1. is_rec : bool;
  2. is_lemma : bool;
}
type declaration =
  1. | TypeDecl of span * type_decl
  2. | ConstDecl of span * const_decl
  3. | NodeDecl of span * node_decl
  4. | FuncDecl of span * node_decl * func_attrs
  5. | ContractNodeDecl of span * contract_node_decl
  6. | NodeParamInst of span * node_param_inst

A declaration of a type, a constant, a node, a function or an instance of a parametric node

type t = declaration list

A Lustre program as a list of declarations

val pp_print_node_param_list : Stdlib.Format.formatter -> ident list -> unit

Pretty-printers

val pp_print_pattern : Stdlib.Format.formatter -> pattern -> unit
val pp_print_ident : Stdlib.Format.formatter -> ident -> unit
val pp_print_label_or_index : Stdlib.Format.formatter -> label_or_index -> unit
val pp_print_expr : Stdlib.Format.formatter -> expr -> unit
val pp_print_array_slice : Stdlib.Format.formatter -> (expr * expr) -> unit
val pp_print_field_assign : Stdlib.Format.formatter -> (ident * expr) -> unit
val pp_print_clock_expr : Stdlib.Format.formatter -> clock_expr -> unit
val pp_print_lustre_type : Stdlib.Format.formatter -> lustre_type -> unit
val pp_print_typed_ident : Stdlib.Format.formatter -> typed_ident -> unit
val pp_print_clocked_typed_ident : Stdlib.Format.formatter -> (Lib.position * ident * lustre_type * clock_expr) -> unit
val pp_print_const_clocked_typed_ident : Stdlib.Format.formatter -> (Lib.position * ident * lustre_type * clock_expr * bool) -> unit
val pp_print_type_decl : Stdlib.Format.formatter -> type_decl -> unit
val pp_print_var_decl : Stdlib.Format.formatter -> (Lib.position * ident * lustre_type * clock_expr) -> unit
val pp_print_const_decl : Stdlib.Format.formatter -> const_decl -> unit
val pp_print_node_local_decl_var : Stdlib.Format.formatter -> node_local_decl -> unit
val pp_print_node_local_decl_const : Stdlib.Format.formatter -> node_local_decl -> unit
val pp_print_node_local_decl : Stdlib.Format.formatter -> node_local_decl list -> unit
val pp_print_struct_item : Stdlib.Format.formatter -> struct_item -> unit
val pp_print_eq_lhs : Stdlib.Format.formatter -> eq_lhs -> unit
val pp_print_contract_eq_lhs : Stdlib.Format.formatter -> contract_eq_lhs -> unit
val pp_print_node_body : Stdlib.Format.formatter -> node_equation -> unit
val pp_print_node_item : Stdlib.Format.formatter -> node_item -> unit
val pp_print_declaration : Stdlib.Format.formatter -> declaration -> unit
val pp_print_program : Stdlib.Format.formatter -> t -> unit
val pp_print_contract_item : Stdlib.Format.formatter -> contract_node_equation -> unit
val pp_print_contract_node_decl : Stdlib.Format.formatter -> contract_node_decl -> unit
val string_of_expr : expr -> string