Module LustreAst

module LustreAst: sig .. end
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 LustreAst.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.
Author(s): Christoph Sticksel

module SI: Set.S  with type 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 expr = 
| Ident of Lib.position * ident
| ModeRef of Lib.position * ident list
| RecordProject of Lib.position * expr * index
| TupleProject of Lib.position * expr * expr
| StructUpdate of Lib.position * expr * label_or_index list
* expr
| True of Lib.position
| False of Lib.position
| Num of Lib.position * string
| Dec of Lib.position * string
| ToInt of Lib.position * expr
| ToReal of Lib.position * expr
| ExprList of Lib.position * expr list
| TupleExpr of Lib.position * expr list
| ArrayExpr of Lib.position * expr list
| ArrayConstr of Lib.position * expr * expr
| ArraySlice of Lib.position * expr * (expr * expr)
| ArrayConcat of Lib.position * expr * expr
| RecordExpr of Lib.position * ident * (ident * expr) list
| Not of Lib.position * expr
| And of Lib.position * expr * expr
| Or of Lib.position * expr * expr
| Xor of Lib.position * expr * expr
| Impl of Lib.position * expr * expr
| Forall of Lib.position * typed_ident list * expr
| Exists of Lib.position * typed_ident list * expr
| OneHot of Lib.position * expr list
| Uminus of Lib.position * expr
| Mod of Lib.position * expr * expr
| Minus of Lib.position * expr * expr
| Plus of Lib.position * expr * expr
| Div of Lib.position * expr * expr
| Times of Lib.position * expr * expr
| IntDiv of Lib.position * expr * expr
| Ite of Lib.position * expr * expr * expr
| With of Lib.position * expr * expr * expr
| Eq of Lib.position * expr * expr
| Neq of Lib.position * expr * expr
| Lte of Lib.position * expr * expr
| Lt of Lib.position * expr * expr
| Gte of Lib.position * expr * expr
| Gt of Lib.position * expr * 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
type lustre_type = 
| Bool of Lib.position
| Int of Lib.position
| IntRange of Lib.position * expr * expr
| Real of Lib.position
| UserType 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
type typed_ident = Lib.position * ident * lustre_type 
An identifier with a type
type 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
type 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 * expr 
type contract_guarantee = Lib.position * string option * 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_node_equation = 
| GhostConst of contract_ghost_const
| GhostVar of contract_ghost_var
| Assume of contract_assume
| Guarantee of contract_guarantee
| Mode of contract_mode
| ContractCall of contract_call
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


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


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 : Format.formatter -> node_param list -> unit

Pretty-printers


val pp_print_ident : Format.formatter -> ident -> unit
val pp_print_expr : Format.formatter -> expr -> unit
val pp_print_array_slice : Format.formatter -> expr * expr -> unit
val pp_print_field_assign : Format.formatter -> ident * expr -> unit
val pp_print_clock_expr : Format.formatter -> clock_expr -> unit
val pp_print_lustre_type : Format.formatter -> lustre_type -> unit
val pp_print_typed_ident : Format.formatter -> typed_ident -> unit
val pp_print_clocked_typed_ident : Format.formatter ->
Lib.position * ident * lustre_type * clock_expr ->
unit
val pp_print_const_clocked_typed_ident : Format.formatter ->
Lib.position * ident * lustre_type *
clock_expr * bool -> unit
val pp_print_type_decl : Format.formatter -> type_decl -> unit
val pp_print_var_decl : Format.formatter ->
Lib.position * ident * lustre_type * clock_expr ->
unit
val pp_print_const_decl : Format.formatter -> const_decl -> unit
val pp_print_node_local_decl_var : Format.formatter -> node_local_decl -> unit
val pp_print_node_local_decl_const : Format.formatter -> node_local_decl -> unit
val pp_print_node_local_decl : Format.formatter -> node_local_decl list -> unit
val pp_print_struct_item : Format.formatter -> struct_item -> unit
val pp_print_node_item : Format.formatter -> node_item -> unit
val pp_print_declaration : Format.formatter -> declaration -> unit
val pp_print_program : Format.formatter -> t -> unit
val pp_print_contract_item : Format.formatter -> contract_node_equation -> unit
val pp_print_contract_node : 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.