package libsail

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Functions for transforming ANF expressions
Compiling to ANF expressions
Pretty printing ANF expressions

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    Config
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CT
    
    CTList
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCT
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
    
    UBindings
    
    UId
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Monomorphise
  - Nl_flow
  - Optimize
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_error
  - Util
    
    Duplicate
  - Value
    
    StringMap
  - Value2

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 =

| 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_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_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

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 =

| 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

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

val anf : Type_check.tannot Ast.exp -> Ast.typ aexp

Pretty printing ANF expressions

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

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