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.

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. is_recursive : bool;
}
type adt_map = adt_info HStringMap.t
val build_adt_info : HString.t -> HString.t list -> (HString.t * (HString.t * LustreAst.lustre_type) list) list -> is_recursive:bool -> adt_info
val record_type_of_adt : Lib.position -> ?ty_args:LustreAst.lustre_type list -> adt_info -> LustreAst.lustre_type
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