The A-normal form (ANF) grammar
The first step in compiling Sail into Jib IR 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). The type is represented as a generic parameter 'a, so we can represent both typed and untyped ANF expressions.
See Flanagan et al's The Essence of Compiling with Continuations.
Each ANF expression has an annotation which contains the location of the original Sail expression, it's typing environment, and the uannot type containing any attributes attached to the original expression.
and 'a aexp_aux = | AE_val of 'a aval| AE_app of function_id * 'a aval list * 'a| AE_typ 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_exit 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_match of 'a aval * ('a apat * 'a aexp * 'a aexp * Ast_util.uannot) list * 'a| AE_try of 'a aexp * ('a apat * 'a aexp * 'a aexp * Ast_util.uannot) list * 'a| AE_struct_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 aexpA short circuting operator (either and or or) must have only its first argument reduced to a trivial value in the ANF representation.
and 'a aval = | AV_lit of Ast.lit * 'a| AV_id of Ast.id * 'a Ast_util.lvar| AV_abstract of Ast.id * 'a| 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 * 'aWe allow ANF->ANF optimization to insert fragments of Jib IR directly in the ANF grammar via AV_cval. Such fragments must be side-effect free expressions.
When the 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.lGet the location from an aexp's annotation
Map over all values in an ANF expression
val map_functions :
(anf_annot -> function_id -> 'a aval list -> 'a -> 'a aexp_aux) ->
'a aexp ->
'a aexpMap over all function calls in an ANF expression
This function 'folds' an aexp applying the provided function to all leaf subexpressions, then applying the function to their containing expression, and so on recursively in a bottom-up order.
val aexp_bindings : 'a aexp -> Ast_util.IdSet.tval is_pure_aexp : Effects.side_effect_info -> 'a aexp -> boolval is_pure_case :
Effects.side_effect_info ->
('a apat * 'a aexp * 'a aexp * Ast_util.uannot) ->
boolval no_shadow : Ast_util.IdSet.t -> 'a aexp -> 'a aexpRemove all variable shadowing in an ANF expression
val apat_types : 'a apat -> 'a Ast_util.Bindings.tval is_dead_aexp : 'a aexp -> boolReturns true if an ANF expression is dead due to flow typing implying it is unreachable. Note: This function calls SMT.
val anf_pat : ?global:bool -> Type_check.tannot Ast.pat -> Ast.typ apatval anf : Type_check.tannot Ast.exp -> Ast.typ aexpval pp_aval : Ast.typ aval -> PPrint.documentval pp_aexp : Ast.typ aexp -> PPrint.document