Module Mlsem_lang.Ast

module SA = Mlsem_system.Ast
type blockid =
  1. | BFun
  2. | BLoop
  3. | BOther of int
type pattern_constructor =
  1. | PCTuple of int
  2. | PCCons
  3. | PCRec of string list * bool
  4. | PCTag of Mlsem_types.Tag.t
  5. | PCEnum of Mlsem_types.Enum.t
  6. | PCCustom of SA.ccustom * SA.pcustom list
type pattern =
  1. | PType of Mlsem_types.Ty.t
  2. | PVar of Mlsem_types.Ty.t list * Mlsem_common.Variable.t
    (*

    The first parameter is a suggested type decomposition, similarly to let-bindings

    *)
  3. | PConstructor of pattern_constructor * pattern list
  4. | PAnd of pattern * pattern
  5. | POr of pattern * pattern
  6. | PAssign of Mlsem_types.Ty.t list * Mlsem_common.Variable.t * Mlsem_types.GTy.t
    (*

    The first parameter is a suggested type decomposition, similarly to let-bindings

    *)
type e =
  1. | Hole of int
  2. | Exc
    (*

    Expression of type empty

    *)
  3. | Void
    (*

    Expression of type void

    *)
  4. | Voidify of t
    (*

    Evaluate the expression inside, but give it the void type, even if it diverges

    *)
  5. | Isolate of t
    (*

    Prevent duplications of the outer context when eliminating control flow inside

    *)
  6. | Value of Mlsem_types.GTy.t
  7. | Var of Mlsem_common.Variable.t
  8. | Constructor of SA.constructor * t list
  9. | Lambda of Mlsem_types.Ty.t list * Mlsem_types.GTy.t * Mlsem_common.Variable.t * t
    (*

    The first parameter is a suggested type decomposition, similarly to let-bindings

    *)
  10. | LambdaRec of (Mlsem_types.GTy.t * Mlsem_common.Variable.t * t) list
  11. | Ite of t * Mlsem_types.GTy.t * t * t
  12. | PatMatch of t * (pattern * t) list
  13. | App of t * t
  14. | Operation of SA.operation * t
  15. | Projection of SA.projection * t
  16. | Declare of Mlsem_common.Variable.t * t
    (*

    Declaration of an uninitialized mutable variable. The variable provided must be mutable (cf. MVariable.create). The type system will not check that the variable is assigned before use.

    *)
  17. | Let of Mlsem_types.Ty.t list * Mlsem_common.Variable.t * t * t
    (*

    The first parameter is a suggested type decomposition

    *)
  18. | TypeCast of t * Mlsem_types.GTy.t * SA.check
  19. | TypeCoerce of t * Mlsem_types.GTy.t * SA.check
  20. | VarAssign of Mlsem_common.Variable.t * t
    (*

    The variable provided must be mutable (cf. MVariable.create)

    *)
  21. | Loop of t
    (*

    An expression that may be evaluated multiple times. Used to encode While expressions.

    *)
  22. | Try of t * t
    (*

    May jump from a branch to another. Used to model try-with expressions.

    *)
  23. | Seq of t * t
    (*

    Evaluate the first expression, then the second.

    *)
  24. | Alt of t * t
    (*

    Evaluate both branches independently. The result is (the intersection of) the result of the branches that do not fail.

    *)
  25. | Block of blockid * t
    (*

    Identifies a block to which a Ret can refer to.

    *)
  26. | Ret of blockid * t option
    (*

    Evaluate the expression specified (Exc if not specified), and use it as the value of block specified. Used to encode Return and Break.

    *)
  27. | If of t * Mlsem_types.GTy.t * t * t option
    (*

    If-else block statement. Returns void.

    *)
  28. | While of t * Mlsem_types.GTy.t * t
    (*

    While block statement. Returns void.

    *)
  29. | Return of t
    (*

    Exits the current function.

    *)
  30. | Break
    (*

    Exits the current while loop.

    *)
val map_pat : (pattern -> pattern) -> pattern -> pattern
val map_pat' : (pattern -> pattern option) -> pattern -> pattern
val iter_pat : (pattern -> unit) -> pattern -> unit
val iter_pat' : (pattern -> bool) -> pattern -> unit
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 fill_hole : int -> t -> t -> t
val fv : t -> Mlsem_common.VarSet.t
val vars : t -> Mlsem_common.VarSet.t
val pp_blockid : Stdlib.Format.formatter -> blockid -> unit
val pp_pattern_constructor : Stdlib.Format.formatter -> pattern_constructor -> unit
val pp_pattern : Stdlib.Format.formatter -> pattern -> unit
val pp_e : Stdlib.Format.formatter -> e -> unit
val pp : Stdlib.Format.formatter -> t -> unit