An Abstract Syntax Tree for ASL.
type binop = | ANDBitvector bitwise and
*)| BANDBoolean and
*)| BEQBoolean equivalence
*)| BORBoolean or
*)| DIVInteger division
*)| DIVRMInexact integer division, with rounding towards negative infinity.
*)| EORBitvector bitwise exclusive or
*)| EQ_OPEquality on two base values of same type
*)| GTGreater than for int or reals
*)| GEQGreater or equal for int or reals
*)| IMPLBoolean implication
*)| LTLess than for int or reals
*)| LEQLess or equal for int or reals
*)| MODRemainder of integer division
*)| MINUSSubstraction for int or reals or bitvectors
*)| MULMultiplication for int or reals or bitvectors
*)| NEQNon equality on two base values of same type
*)| ORBitvector bitwise or
*)| PLUSAddition for int or reals or bitvectors
*)| POWExponentiation for ints
*)| RDIVDivision for reals
*)| SHLShift left for ints
*)| SHRShift right for ints
*)Operations on base value of arity two.
Literals are the values written straight into ASL specifications. There is only literal constructors for a few concepts that could be encapsulated into an ASL value.
type literal = | L_Int of Z.t| L_Bool of bool| L_Real of Q.t| L_BitVector of Bitvector.t| L_String of stringMain value type, parametric on its base values
type expr_desc = | E_Literal of literal| E_Var of identifier| E_CTC of expr * ty| E_Binop of binop * expr * expr| E_Unop of unop * expr| E_Call of identifier * expr list * (identifier * expr) list| E_Slice of expr * slice list| E_Cond of expr * expr * expr| E_GetArray of expr * expr| E_GetField of expr * identifier| E_GetFields of expr * identifier list| E_Record of ty * (identifier * expr) listRepresents a record or an exception construction expression.
*)| E_Concat of expr list| E_Tuple of expr list| E_Unknown of ty| E_Pattern of expr * patternExpressions. Parametric on the type of literals.
and slice = | Slice_Single of exprSlice_Single i is the slice of length 1 at position i.
| Slice_Range of expr * exprSlice_Range (j, i) denotes the slice from i to j - 1.
| Slice_Length of expr * exprSlice_Length (i, n) denotes the slice starting at i of length n.
| Slice_Star of expr * exprSlice_Start (factor, length) denotes the slice starting at factor
* length of length n.
Indexes an array, a bitvector.
All position mentionned above are included.
and type_desc = | T_Int of int_constraints| T_Bits of expr * bitfield list| T_Real| T_String| T_Bool| T_Enum of identifier list| T_Tuple of ty list| T_Array of array_index * ty| T_Record of field list| T_Exception of field list| T_Named of identifierA type variable.
*)Type descriptors.
and int_constraints = | UnConstrainedThe normal, unconstrained, integer type.
*)| WellConstrained of int_constraint listAn integer type constrained from ASL syntax: it is the union of each constraint in the list.
*)| UnderConstrained of uid * identifierAn under-constrained integer, the default type for parameters of function at compile time, with a unique identifier and the variable bearing its name.
*)The int_constraints constraints the integer type to a certain subset.
and bitfield = | BitField_Simple of identifier * slice listA name and its corresponding slice
*)| BitField_Nested of identifier * slice list * bitfield listA name, its corresponding slice and some nested bitfields.
*)| BitField_Type of identifier * slice list * tyA name, its corresponding slice and the type of the bitfield.
*)Represent static slices on a given bitvector type.
and array_index = | ArrayLength_Expr of exprAn integer expression giving the length of the array.
*)| ArrayLength_Enum of identifier * intAn enumeration name and its length.
*)The type of indexes for an array.
and field = identifier * tyA field of a record-like structure.
and typed_identifier = identifier * tyAn identifier declared with its type.
type lexpr_desc = | LE_Discard| LE_Var of identifier| LE_Slice of lexpr * slice list| LE_SetArray of lexpr * expr| LE_SetField of lexpr * identifier| LE_SetFields of lexpr * identifier list| LE_Destructuring of lexpr list| LE_Concat of lexpr list * int list optionLE_Concat (les, _) unpacks the various lexpr. Second argument is a type annotation.
*)Type of left-hand side of assignments.
and lexpr = lexpr_desc annotatedtype local_decl_item = | LDI_DiscardLDI_Discard is the ignored local_decl_item, for example used in:
let - = 42;
.
*)| LDI_Var of identifierLDI_Var x is the variable declaration of the variable x, used for example in:
let x = 42;
.
*)| LDI_Tuple of local_decl_item listLDI_Tuple ldis is the tuple declarations of the items in ldis, used for example in:
let (x, y, -, z) = (1, 2, 3, 4);
Note that a the list here must be at least 2 items long.
*)| LDI_Typed of local_decl_item * tyLDI_Typed (ldi, t) declares the item ldi with type t.
A left-hand side of a declaration statement. In the following example of a declaration statement, (2, 3, 4): (integer, integer, integer {0..32}) is the local declaration item:
let (x, -, z): (integer, integer, integer {0..32}) = (2, 3, 4);type stmt_desc = | S_Pass| S_Seq of stmt * stmt| S_Decl of local_decl_keyword * local_decl_item * expr option| S_Assign of lexpr * expr * version| S_Call of identifier * expr list * (identifier * expr) list| S_Return of expr option| S_Cond of expr * stmt * stmt| S_Case of expr * case_alt list| S_Assert of expr| S_For of identifier * expr * for_direction * expr * stmt| S_While of expr * stmt| S_Repeat of stmt * expr| S_Throw of (expr * ty option) optionThe ty option is a type annotation added by the type-checker to be matched later with the catch guards. The bigger option is to represent the implicit throw, such as throw;.
| S_Try of stmt * catcher list * stmt optionThe stmt option is the optional otherwise guard.
*)| S_Print of {args : expr list;debug : bool;}A call to print, as an explicit node as it does not require type-checking.
*)and catcher = identifier option * ty * stmtThe optional name of the matched exception, the guard type and the statement to be executed if the guard matches.
type func = {name : identifier;parameters : (identifier * ty option) list;args : typed_identifier list;body : subprogram_body;return_type : ty option;subprogram_type : subprogram_type;}Function types in the AST. For the moment, they represent getters, setters, functions, procedures and primitives.
Declaration keyword for global storage elements.
type global_decl = {keyword : global_decl_keyword;name : identifier;ty : ty option;initial_value : expr option;}Global declaration type
type decl_desc = | D_Func of func| D_GlobalStorage of global_decl| D_TypeDecl of identifier * ty * (identifier * field list) optionDeclarations, ie. top level statement in a asl file.
type t = decl listMain AST type.
type scope = | Scope_Local of identifier * uidLocal scope of a function given by its name and an uid of the call
*)| Scope_Global of boolGlobal runtime scope, with whether it was during initialization or not
*)A scope is an unique identifier of the calling site.