Module Mlsem_system.Ast

type pcustom = {
  1. pname : string;
  2. pdom : Mlsem_types.Ty.t -> Mlsem_types.Ty.t;
  3. proj : Mlsem_types.Ty.t -> Mlsem_types.Ty.t;
  4. pgen : bool;
}
type ccustom = {
  1. cname : string;
  2. cdom : Mlsem_types.Ty.t -> Mlsem_types.Ty.t list list;
  3. cons : Mlsem_types.Ty.t list -> Mlsem_types.Ty.t;
  4. cgen : bool;
}
type ocustom = {
  1. oname : string;
  2. ofun : Mlsem_common.Env.t -> Mlsem_types.TyScheme.t;
  3. ogen : bool;
}
type check =
  1. | Check
  2. | CheckStatic
  3. | NoCheck
type projection =
  1. | Pi of int * int
  2. | PiField of string
  3. | PiFieldOpt of string
  4. | Hd
  5. | Tl
  6. | PiTag of Mlsem_types.Tag.t
  7. | PCustom of pcustom
type constructor =
  1. | Tuple of int
  2. | Cons
  3. | Rec of string list * bool
  4. | Tag of Mlsem_types.Tag.t
  5. | Enum of Mlsem_types.Enum.t
  6. | Join of int
  7. | Meet of int
  8. | Ternary of Mlsem_types.Ty.t
  9. | Voidify of Mlsem_types.Ty.t
  10. | Normalize
  11. | CCustom of ccustom
type operation =
  1. | RecUpd of string
  2. | RecDel of string
  3. | Ignore of Mlsem_types.Ty.t
  4. | OCustom of ocustom
type alt_settings = {
  1. aname : string;
  2. amask : Mlsem_common.Env.t -> bool list;
  3. aerror : Mlsem_common.Env.t -> string;
}
type param_annot = Mlsem_types.GTy.t option
type e =
  1. | Value of Mlsem_types.GTy.t
  2. | Var of Mlsem_common.Variable.t
  3. | Constructor of constructor * t list
  4. | Lambda of param_annot * Mlsem_common.Variable.t * t
  5. | LambdaRec of (param_annot * Mlsem_common.Variable.t * t) list
  6. | Ite of t * Mlsem_types.GTy.t * t * t
  7. | App of t * t
  8. | Operation of operation * t
  9. | Projection of projection * t
  10. | Let of Mlsem_types.Ty.t list * Mlsem_common.Variable.t * t * t
  11. | TypeCast of t * Mlsem_types.GTy.t * check
  12. | TypeCoerce of t * Mlsem_types.GTy.t * check
  13. | Alt of alt_settings * t list
val map : (t -> t) -> t -> t
val map' : (t -> t option) -> t -> t
val iter : (t -> unit) -> t -> unit
val iter' : (t -> bool) -> t -> unit
val fv : t -> Mlsem_common.VarSet.t
val vars : t -> Mlsem_common.VarSet.t
val apply_subst : Mlsem_types.Subst.t -> t -> t
val pp_raw : Stdlib.Format.formatter -> t -> unit
val pp : Stdlib.Format.formatter -> t -> unit
val pp_e : Stdlib.Format.formatter -> e -> unit
val pp_check : Stdlib.Format.formatter -> check -> unit
val pp_projection : Stdlib.Format.formatter -> projection -> unit
val pp_constructor : Stdlib.Format.formatter -> constructor -> unit
val pp_operation : Stdlib.Format.formatter -> operation -> unit
val pp_alt_settings : Stdlib.Format.formatter -> alt_settings -> unit
val pp_param_annot : Stdlib.Format.formatter -> param_annot -> unit
val pp_pcustom : Stdlib.Format.formatter -> pcustom -> unit
val pp_ccustom : Stdlib.Format.formatter -> ccustom -> unit
val domain_of_proj : projection -> Mlsem_types.Ty.t -> Mlsem_types.Ty.t
val domains_of_construct : constructor -> Mlsem_types.Ty.t -> Mlsem_types.Ty.t list list
val construct : constructor -> Mlsem_types.Ty.t list -> Mlsem_types.Ty.t
val coerce : ?coercion_id:Mlsem_common.Eid.t -> check -> Mlsem_types.GTy.t -> t -> t
val push_coercions : t -> t