package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

The A-normal form (ANF) grammar

The first step in compiling Sail is converting the Sail expression grammar into A-normal form (ANF). Essentially this converts expressions such as f(g(x), h(y)) into something like:

let v0 = g(x) in let v1 = h(x) in f(v0, v1)

Essentially the arguments to every function must be trivial, and complex expressions must be let bound to new variables, or used in a block, assignment, or control flow statement (if, for, and while/until loops). The aexp datatype represents these expressions, while aval represents the trivial values.

The convention is that the type of an aexp is given by last argument to a constructor. It is omitted where it is obvious - for example all for loops have unit as their type. If some constituent part of the aexp has an annotation, the it refers to the previous argument, so in

AE_let (id, typ1, _, body, typ2)

typ1 is the type of the bound identifer, whereas typ2 is the type of the whole let expression (and therefore also the body).

See Flanagan et al's The Essence of Compiling with Continuations.

type 'a aexp =
  1. | AE_aux of 'a aexp_aux * Type_check.Env.t * Ast.l
and 'a aexp_aux =
  1. | AE_val of 'a aval
  2. | AE_app of Ast.id * 'a aval list * 'a
  3. | AE_cast of 'a aexp * 'a
  4. | AE_assign of 'a alexp * 'a aexp
  5. | AE_let of Ast_util.mut * Ast.id * 'a * 'a aexp * 'a aexp * 'a
  6. | AE_block of 'a aexp list * 'a aexp * 'a
  7. | AE_return of 'a aval * 'a
  8. | AE_exit of 'a aval * 'a
  9. | AE_throw of 'a aval * 'a
  10. | AE_if of 'a aval * 'a aexp * 'a aexp * 'a
  11. | AE_field of 'a aval * Ast.id * 'a
  12. | AE_case of 'a aval * ('a apat * 'a aexp * 'a aexp) list * 'a
  13. | AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp) list * 'a
  14. | AE_record_update of 'a aval * 'a aval Ast_util.Bindings.t * 'a
  15. | AE_for of Ast.id * 'a aexp * 'a aexp * 'a aexp * Ast.order * 'a aexp
  16. | AE_loop of Ast.loop * 'a aexp * 'a aexp
  17. | AE_short_circuit of sc_op * 'a aval * 'a aexp
and sc_op =
  1. | SC_and
  2. | SC_or
and 'a apat =
  1. | AP_aux of 'a apat_aux * Type_check.Env.t * Ast.l
and 'a apat_aux =
  1. | AP_tup of 'a apat list
  2. | AP_id of Ast.id * 'a
  3. | AP_global of Ast.id * 'a
  4. | AP_app of Ast.id * 'a apat * 'a
  5. | AP_cons of 'a apat * 'a apat
  6. | AP_as of 'a apat * Ast.id * 'a
  7. | AP_nil of 'a
  8. | AP_wild of 'a
and 'a aval =
  1. | AV_lit of Ast.lit * 'a
  2. | AV_id of Ast.id * 'a Ast_util.lvar
  3. | AV_ref of Ast.id * 'a Ast_util.lvar
  4. | AV_tuple of 'a aval list
  5. | AV_list of 'a aval list * 'a
  6. | AV_vector of 'a aval list * 'a
  7. | AV_record of 'a aval Ast_util.Bindings.t * 'a
  8. | AV_cval of Jib.cval * 'a

We allow ANF->ANF optimization to insert fragments of C code directly in the ANF grammar via AV_cval. Such fragments must be side-effect free expressions.

and 'a alexp =
  1. | AL_id of Ast.id * 'a
  2. | AL_addr of Ast.id * 'a
  3. | AL_field of 'a alexp * Ast.id
val reset_anf_counter : unit -> unit

When ANF translation has to introduce new bindings it uses a counter to ensure uniqueness. This function resets that counter.

val aexp_loc : 'a aexp -> Parse_ast.l

Functions for transforming ANF expressions

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

Map over all values in an ANF expression

val map_functions : (Type_check.Env.t -> Ast.l -> Ast.id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp

Map over all function calls in an ANF expression

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

Remove all variable shadowing in an ANF expression

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

Returns true if an ANF expression is dead due to flow typing implying it is unreachable. Note: This function calls SMT.

Compiling to ANF expressions

val anf_pat : ?global:bool -> Type_check.tannot Ast.pat -> Ast.typ apat

Pretty printing ANF expressions

val pp_aval : Ast.typ aval -> PPrint.document
val pp_aexp : Ast.typ aexp -> PPrint.document