Module LustreGlobals

Global declarations for Lustre input

module HStringMap = HString.HStringMap
type state_var_bounds = LustreExpr.expr LustreExpr.bound_or_fixed list StateVar.StateVarHashtbl.t
type adt_field_info =
  1. | AdtFieldPlain
  2. | AdtFieldNested of HString.t
type adt_info = {
  1. disc_field : HString.t;
  2. ctor_fields : (HString.t * adt_field_info) list HStringMap.t;
  3. is_recursive : bool;
}
type adt_map = adt_info HStringMap.t
type t = {
  1. free_constants : (LustreIdent.t * Var.t LustreIndex.t * bool) list;
    (*

    Free constants: ident, variable index, is_generated

    *)
  2. state_var_bounds : state_var_bounds;
    (*

    Register bounds of state variables for later use

    *)
  3. global_constraints : LustreExpr.t list;
    (*

    Constraints on free constants

    *)
  4. adt_map : adt_map;
    (*

    ADT type metadata for counterexample reconstruction

    *)
  5. recursive_datatypes : Type.t list;
    (*

    Recursive ADTs, in dependency order

    *)
  6. adt_junk_ufs : UfSymbol.t list;
    (*

    Uninterpreted functions giving a selector applied to an ADT value built with another constructor its (arbitrary, fixed) value

    *)
  7. adt_global_constraints : LustreExpr.t list;
    (*

    Canonical-form constraints of the free constants of a type involving an ADT (see LustreDesugarADTs.mk_canonical_exprs); a system only needs those of the constants some node mentions

    *)
}