sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Anf
type !'a aexp =
| AE_aux of 'a aexp_aux * Type_check.Env.t * Ast.l
and !'a aexp_aux =
| AE_val of 'a aval
| AE_app of Ast.id * 'a aval list * 'a
| AE_cast of 'a aexp * 'a
| AE_assign of 'a alexp * 'a aexp
| AE_let of Ast_util.mut * Ast.id * 'a * 'a aexp * 'a aexp * 'a
| AE_block of 'a aexp list * 'a aexp * 'a
| AE_return of 'a aval * 'a
| AE_throw of 'a aval * 'a
| AE_if of 'a aval * 'a aexp * 'a aexp * 'a
| AE_field of 'a aval * Ast.id * 'a
| AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a
| AE_record_update of 'a aval * 'a aval Ast_util.Bindings.t * 'a
| AE_for of Ast.id * 'a aexp * 'a aexp * 'a aexp * Ast.order * 'a aexp
| AE_loop of Ast.loop * 'a aexp * 'a aexp
| AE_short_circuit of sc_op * 'a aval * 'a aexp
and sc_op =
| SC_and
| SC_or
and !'a apat =
| AP_aux of 'a apat_aux * Type_check.Env.t * Ast.l
and !'a apat_aux =
| AP_tup of 'a apat list
| AP_id of Ast.id * 'a
| AP_global of Ast.id * 'a
| AP_app of Ast.id * 'a apat * 'a
| AP_cons of 'a apat * 'a apat
| AP_as of 'a apat * Ast.id * 'a
| AP_nil of 'a
| AP_wild of 'a
and !'a aval =
| AV_lit of Ast.lit * 'a
| AV_id of Ast.id * 'a Ast_util.lvar
| AV_ref of Ast.id * 'a Ast_util.lvar
| AV_tuple of 'a aval list
| AV_list of 'a aval list * 'a
| AV_vector of 'a aval list * 'a
| AV_record of 'a aval Ast_util.Bindings.t * 'a
| AV_cval of Jib.cval * 'a
and !'a alexp =
| AL_id of Ast.id * 'a
| AL_addr of Ast.id * 'a
| AL_field of 'a alexp * Ast.id
val reset_anf_counter : unit -> unit
val aexp_loc : 'a aexp -> Parse_ast.l
val aval_typ : Ast.typ aval -> Ast.typ
val aexp_typ : Ast.typ aexp -> Ast.typ
val map_aval : ( Type_check.Env.t -> Ast.l -> 'a aval -> 'a aval ) -> 'a aexp -> 'a aexp
val map_functions : ( Type_check.Env.t -> Ast.l -> Ast.id -> 'a aval list -> 'a -> 'a aexp_aux ) -> 'a aexp -> 'a aexp
val fold_aexp : ( 'a aexp -> 'a aexp ) -> 'a aexp -> 'a aexp
val aexp_bindings : 'a aexp -> Ast_util.IdSet.t
val no_shadow : Ast_util.IdSet.t -> 'a aexp -> 'a aexp
val apat_globals : 'a apat -> (Ast.id * 'a) list
val apat_types : 'a apat -> 'a Ast_util.Bindings.t
val is_dead_aexp : 'a aexp -> bool
val anf_pat : ?global:bool -> Type_check.tannot Ast.pat -> Ast.typ apat
val pp_aval : Ast.typ aval -> PPrint.document
val pp_aexp : Ast.typ aexp -> PPrint.document