Module LustreDesugarADTs

Desugaring of non-recursive algebraic data types (ADTs) to records.

For each ADT declaration type T = C0 | C1(t1) | C2(t2_0, t2_1) a discriminant enum type and an equivalent record type are produced: type T_tag = C0 | C1 | C2; type T = \{ T_tag: T_tag; C1_0: t1; C2_0: t2_0; C2_1: t2_1 \} where the tag field encodes the active constructor and payload fields for non-selected constructors carry default values. An ADT whose every constructor is nullary collapses to the discriminant enum alone; this is how an enum declaration, parsed as an all-nullary ADT, reaches the rest of the pipeline.

desugar_adts is the main pipeline entry point: it desugars both TypeDecls and all ADTTerm/Match expressions in one pass.

module HStringMap = HString.HStringMap
type adt_info = {
  1. type_name : HString.t;
  2. type_params : HString.t list;
  3. disc_field : HString.t;
  4. disc_enum : HString.t;
  5. ctor_variants : HString.t list;
  6. ctor_fields : (HString.t * LustreAst.lustre_type) list HStringMap.t;
  7. all_payload_fields : (HString.t * LustreAst.lustre_type) list;
  8. field_names : (HString.t * HString.t * HString.t) list;
  9. is_recursive : bool;
}
type adt_map = adt_info HStringMap.t
val is_generated_type_name : HString.t -> bool

Whether a type name was generated by this module (the discriminant enum of a datatype's record encoding) rather than declared by the user.

val is_enum_like : adt_info -> bool

Whether a non-recursive datatype collapses to a bare enum of its constructors, which it does when every constructor is nullary and the declaration takes no type parameters. Such a type is compiled to a single enum-sorted state variable rather than to a record of a discriminant and payload fields.

val is_canonical_bound_var : HString.t -> bool

Whether a bound variable was introduced by mk_canonical_exprs. Its quantifier characterizes the non-canonical positions of a container and must not itself be restricted to canonical values.

mk_canonical_exprs ctx adt_map pos expr ty is the list of constraints stating that every ADT value reachable from expr, of type ty, is in canonical form: the payload fields of the constructors other than the active one hold the default value of their type, and sets and maps only hold canonical keys. Every ADT value in a program is kept in this form, so ADT equality and set/map membership are plain operations on the desugared record; the constraints are what free values (inputs, oracles, undefined outputs, free constants and quantified variables) are subject to.

default_value ctx adt_map pos ty is a value of type ty: the one the payload fields of the constructors other than the active one hold in canonical form

val ctor_of_payload_field : adt_info -> HString.t -> HString.t option

The constructor whose payload field has the given internal record field name, if any

The ADT underlying a type, through type synonyms and refinement types

val build_adt_map : LustreAst.declaration list -> adt_map

Collect all ADT type declarations from a program into an adt_map, without performing any desugaring. Exposed so that passes needing is_recursive classification (e.g. LustreCheckADTDecreases) can run before desugar_adts eliminates Match/ADTTerm from the AST.

val ref_type_canonical_key : LustreAst.lustre_type -> string option
val string_of_expr_as_source : ?ref_type_names:(string * HString.t) list -> adt_map -> LustreAst.expr -> string