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

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

a type definition type t = t',
a constant definition const c = v, or
a node declaration.

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

author: Christoph Sticksel

module SI : Stdlib.Set.S with type SI.elt = Ident.t

exception Parser_error: Error while parsing

Types

type ident = string: An identifier

type index = string: A single index

type clock_expr = | ClockTrue | ClockPos of ident | ClockNeg of ident | ClockConstr of ident * ident: A clock expression

type conversion_operator = | ToInt | ToReal | ToInt8 | ToInt16 | ToInt32 | ToInt64 | ToUInt8 | ToUInt16 | ToUInt32 | ToUInt64
type unary_operator = | Not | Uminus | BVNot
type binary_operator = | And | Or | Xor | Impl | Mod | Minus | Plus | Div | Times | IntDiv | BVAnd | BVOr | BVShiftL | BVShiftR
type ternary_operator = | Ite | With
type n_arity_operator = | OneHot
type comparison_operator = | Eq | Neq | Lte | Lt | Gte | Gt
type constant = | True | False | Num of string | Dec of string
type quantifier = | Forall | Exists
type group_expr = | ExprList | TupleExpr | ArrayExpr
type expr = | Ident of Lib.position * ident | ModeRef of Lib.position * ident list | RecordProject of Lib.position * expr * index | TupleProject of Lib.position * expr * expr | Const of Lib.position * constant | UnaryOp of Lib.position * unary_operator * expr | BinaryOp of Lib.position * binary_operator * expr * expr | TernaryOp of Lib.position * ternary_operator * expr * expr * expr | NArityOp of Lib.position * n_arity_operator * expr list | ConvOp of Lib.position * conversion_operator * expr | CompOp of Lib.position * comparison_operator * expr * expr | RecordExpr of Lib.position * ident * (ident * expr) list | GroupExpr of Lib.position * group_expr * expr list | StructUpdate of Lib.position * expr * label_or_index list * expr | ArrayConstr of Lib.position * expr * expr | ArraySlice of Lib.position * expr * expr * expr | ArrayConcat of Lib.position * expr * expr | Quantifier of Lib.position * quantifier * typed_ident list * expr | When of Lib.position * expr * clock_expr | Current of Lib.position * expr | Condact of Lib.position * expr * expr * ident * expr list * expr list | Activate of Lib.position * ident * expr * expr * expr list | Merge of Lib.position * ident * (ident * expr) list | RestartEvery of Lib.position * ident * expr list * expr | Pre of Lib.position * expr | Last of Lib.position * ident | Fby of Lib.position * expr * int * expr | Arrow of Lib.position * expr * expr | Call of Lib.position * ident * expr list | CallParam of Lib.position * ident * lustre_type list * expr list: A Lustre expression

and lustre_type = | Bool of Lib.position | Int of Lib.position | UInt8 of Lib.position | UInt16 of Lib.position | UInt32 of Lib.position | UInt64 of Lib.position | Int8 of Lib.position | Int16 of Lib.position | Int32 of Lib.position | Int64 of Lib.position | IntRange of Lib.position * expr * expr | Real of Lib.position | UserType of Lib.position * ident | AbstractType of Lib.position * ident | TupleType of Lib.position * lustre_type list | RecordType of Lib.position * typed_ident list | ArrayType of Lib.position * lustre_type * expr | EnumType of Lib.position * ident option * ident list: A Lustre type

and typed_ident = Lib.position * ident * lustre_type: An identifier with a type

and label_or_index = | Label of Lib.position * index | Index of Lib.position * expr: A record field or an array or tuple index

Declarations

type type_decl = | AliasType of Lib.position * ident * lustre_type | 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 = | FreeConst of Lib.position * ident * lustre_type | UntypedConst of Lib.position * ident * expr | TypedConst of Lib.position * ident * expr * lustre_type: A constant declaration

type node_param = | TypeParam of ident: A type parameter of a node

type node_local_decl = | NodeConstDecl of Lib.position * const_decl | NodeVarDecl of Lib.position * clocked_typed_decl: A local constant or variable declaration of a node

type struct_item = | SingleIdent of Lib.position * ident | TupleStructItem of Lib.position * struct_item list | TupleSelection of Lib.position * ident * expr | FieldSelection of Lib.position * ident * ident | ArraySliceStructItem of Lib.position * ident * (expr * expr) list | ArrayDef of Lib.position * ident * ident list: Structural assignment on the left-hand side of an equation

type eq_lhs = | StructDef of Lib.position * struct_item list: The left-hand side of an equation

type transition_to = | TransRestart of Lib.position * Lib.position * ident | TransResume of Lib.position * Lib.position * ident
type transition_branch = | Target of transition_to | TransIf of Lib.position * expr * transition_branch * transition_branch option
type automaton_transition = Lib.position * transition_branch
type auto_returns = | Given of ident list | Inferred
type node_equation = | Assert of Lib.position * expr | Equation of Lib.position * eq_lhs * expr | Automaton of Lib.position * ident option * state list * auto_returns: An equation or assertion in the node body

and state = | State of Lib.position * ident * bool * node_local_decl list * node_equation list * automaton_transition option * automaton_transition option
type node_item = | Body of node_equation | AnnotMain of bool | AnnotProperty of Lib.position * string option * expr: An item in a node declaration

type contract_ghost_const = const_decl

type contract_ghost_var = const_decl

type contract_assume = Lib.position * string option * bool * expr

type contract_guarantee = Lib.position * string option * bool * expr

type contract_require = Lib.position * string option * expr

type contract_ensure = Lib.position * string option * expr

type contract_mode = Lib.position * ident * contract_require list * contract_ensure list

type contract_call = Lib.position * ident * expr list * expr list

type contract = contract_node_equation list

type node_decl = ident * bool * node_param 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 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 = ident * node_param 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 declaration = | TypeDecl of Lib.position * type_decl | ConstDecl of Lib.position * const_decl | NodeDecl of Lib.position * node_decl | FuncDecl of Lib.position * node_decl | ContractNodeDecl of Lib.position * contract_node_decl | NodeParamInst of Lib.position * 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 -> node_param list -> unit: Pretty-printers

val pp_print_ident : Stdlib.Format.formatter -> ident -> 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_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

Helpers

val pos_of_expr : expr -> Lib.position: Returns the position of an expression

val has_unguarded_pre : expr -> bool: Returns true if the expression has unguareded pre's

val has_pre_or_arrow : expr -> Lib.position option: Returns true if the expression has a `pre` or a `->`.

val contract_has_pre_or_arrow : 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 : node_local_decl -> Lib.position option: Checks whether a node local declaration has a `pre` or a `->`.

val node_item_has_pre_or_arrow : node_item -> Lib.position option: Checks whether a node equation has a `pre` or a `->`.

val replace_lasts : string list -> string -> SI.t -> expr -> expr * SI.t: replace_lasts allowed prefix acc e replaces last x expressions in AST e by abstract identifiers prefixed with prefix. Only identifiers that appear in the list allowed are allowed to appear under a last. It returns the new AST expression and a set of identifers for which the last application was replaced.

Pretty-printers