package libsail

  1. Overview
  2. Docs

Module Libsail.Ast_utilSource

Utilities and helper functions for operating on Sail ASTs

module Big_int = Nat_big_num
Sourcetype mut =
  1. | Immutable
  2. | Mutable
Sourcetype 'a lvar =
  1. | Register of 'a
  2. | Enum of 'a
  3. | Local of mut * 'a
  4. | Unbound of Ast.id

lvar is the type of variables - they can either be registers, local mutable or immutable variables constructors or unbound identifiers.

Sourceval is_unbound : 'a lvar -> bool
Sourceval lvar_typ : ?loc:Ast.l -> 'a lvar -> 'a

Note: Partial function -- fails for Unknown lvars

Sourceval no_annot : unit Ast.annot

The empty annotation. Should be used carefully because it can result in unhelpful error messgaes. However a common pattern is generating code with no_annot, then adding location information with the various locate_ functions in this module.

gen_loc l takes a location l and generates a location which means 'generated/derived from location l'. This is useful for debugging errors that occur in generated code.

Sourceval is_gen_loc : Parse_ast.l -> bool

Functions for building (untyped) AST elements

Sourceval mk_id : string -> Ast.id
Sourceval mk_kid : string -> Ast.kid
Sourceval mk_nexp : Ast.nexp_aux -> Ast.nexp
Sourceval mk_exp : ?loc:Ast.l -> unit Ast.exp_aux -> unit Ast.exp
Sourceval mk_pat : unit Ast.pat_aux -> unit Ast.pat
Sourceval mk_mpat : unit Ast.mpat_aux -> unit Ast.mpat
Sourceval mk_pexp : ?loc:Ast.l -> unit Ast.pexp_aux -> unit Ast.pexp
Sourceval mk_mpexp : unit Ast.mpexp_aux -> unit Ast.mpexp
Sourceval mk_lexp : unit Ast.lexp_aux -> unit Ast.lexp
Sourceval mk_lit : Ast.lit_aux -> Ast.lit
Sourceval mk_lit_exp : Ast.lit_aux -> unit Ast.exp
Sourceval mk_funcl : Ast.id -> unit Ast.pat -> unit Ast.exp -> unit Ast.funcl
Sourceval mk_fundef : unit Ast.funcl list -> unit Ast.def
Sourceval mk_val_spec : Ast.val_spec_aux -> unit Ast.def
Sourceval mk_typschm : Ast.typquant -> Ast.typ -> Ast.typschm
Sourceval mk_typquant : Ast.quant_item list -> Ast.typquant
Sourceval mk_fexp : Ast.id -> unit Ast.exp -> unit Ast.fexp
Sourceval mk_letbind : unit Ast.pat -> unit Ast.exp -> unit Ast.letbind
Sourceval mk_kopt : ?loc:Ast.l -> Ast.kind_aux -> Ast.kid -> Ast.kinded_id
Sourceval inc_ord : Ast.order
Sourceval dec_ord : Ast.order

Unwrap aux constructors

Sourceval unaux_exp : 'a Ast.exp -> 'a Ast.exp_aux
Sourceval unaux_pat : 'a Ast.pat -> 'a Ast.pat_aux
Sourceval unaux_nexp : Ast.nexp -> Ast.nexp_aux
Sourceval unaux_order : Ast.order -> Ast.order_aux
Sourceval unaux_typ : Ast.typ -> Ast.typ_aux
Sourceval unaux_kind : Ast.kind -> Ast.kind_aux

Destruct type annotated patterns and expressions

Sourceval untyp_pat : 'a Ast.pat -> 'a Ast.pat * Ast.typ option

untyp_pat (P_aux (P_typ (typ, pat)), _) returns Some (pat, typ) or None if the pattern does not match.

Sourceval uncast_exp : 'a Ast.exp -> 'a Ast.exp * Ast.typ option

Same as untyp_pat, but for E_cast nodes

Utilites for working with kinded_ids

Sourceval kopt_kid : Ast.kinded_id -> Ast.kid
Sourceval kopt_kind : Ast.kinded_id -> Ast.kind
Sourceval is_int_kopt : Ast.kinded_id -> bool
Sourceval is_order_kopt : Ast.kinded_id -> bool
Sourceval is_typ_kopt : Ast.kinded_id -> bool
Sourceval is_bool_kopt : Ast.kinded_id -> bool

Utility functions for constructing types

Sourceval mk_typ : Ast.typ_aux -> Ast.typ
Sourceval mk_id_typ : Ast.id -> Ast.typ
Sourceval is_typ_arg_nexp : Ast.typ_arg -> bool
Sourceval is_typ_arg_typ : Ast.typ_arg -> bool
Sourceval is_typ_arg_order : Ast.typ_arg -> bool
Sourceval is_typ_arg_bool : Ast.typ_arg -> bool

Sail builtin types

Sourceval unknown_typ : Ast.typ
Sourceval int_typ : Ast.typ
Sourceval nat_typ : Ast.typ
Sourceval atom_typ : Ast.nexp -> Ast.typ
Sourceval implicit_typ : Ast.nexp -> Ast.typ
Sourceval range_typ : Ast.nexp -> Ast.nexp -> Ast.typ
Sourceval bit_typ : Ast.typ
Sourceval bool_typ : Ast.typ
Sourceval atom_bool_typ : Ast.n_constraint -> Ast.typ
Sourceval app_typ : Ast.id -> Ast.typ_arg list -> Ast.typ
Sourceval register_typ : Ast.typ -> Ast.typ
Sourceval unit_typ : Ast.typ
Sourceval string_typ : Ast.typ
Sourceval real_typ : Ast.typ
Sourceval vector_typ : Ast.nexp -> Ast.order -> Ast.typ -> Ast.typ
Sourceval bitvector_typ : Ast.nexp -> Ast.order -> Ast.typ
Sourceval list_typ : Ast.typ -> Ast.typ
Sourceval exc_typ : Ast.typ
Sourceval tuple_typ : Ast.typ list -> Ast.typ
Sourceval function_typ : Ast.typ list -> Ast.typ -> Ast.typ
Sourceval is_unit_typ : Ast.typ -> bool
Sourceval is_number : Ast.typ -> bool
Sourceval is_ref_typ : Ast.typ -> bool
Sourceval is_vector_typ : Ast.typ -> bool
Sourceval is_bit_typ : Ast.typ -> bool
Sourceval is_bitvector_typ : Ast.typ -> bool

Simplifcation of numeric expressions and constraints

These functions simplify nexps and n_constraints using various basic rules. In general they will guarantee to reduce constant numeric expressions like 2 + 5 into 7, although they will not simplify 2^constant, as that often leads to unreadable error messages containing huge numbers.

Sourceval nexp_simp : Ast.nexp -> Ast.nexp
Sourceval constraint_simp : Ast.n_constraint -> Ast.n_constraint
Sourceval constraint_conj : Ast.n_constraint -> Ast.n_constraint list

If a constraint is a conjunction, return a list of all the top-level conjuncts

Sourceval constraint_disj : Ast.n_constraint -> Ast.n_constraint list

Same as constraint_conj but for disjunctions

Set and Map modules for various AST elements

Sourcemodule Id : sig ... end
Sourcemodule Kid : sig ... end
Sourcemodule Kind : sig ... end
Sourcemodule KOpt : sig ... end
Sourcemodule Nexp : sig ... end
Sourcemodule NC : sig ... end
Sourcemodule Typ : sig ... end
Sourcemodule IdSet : sig ... end
Sourcemodule NexpSet : sig ... end
Sourcemodule NexpMap : sig ... end
Sourcemodule KOptSet : sig ... end
Sourcemodule KOptMap : sig ... end
Sourcemodule KidSet : sig ... end
Sourcemodule KBindings : sig ... end
Sourcemodule Bindings : sig ... end
Sourcemodule NCMap : sig ... end
Sourcemodule TypMap : sig ... end
Sourcetype effect
Sourceval no_effect : effect
Sourceval monadic_effect : effect
Sourceval effectful : effect -> bool
Sourceval equal_effects : effect -> effect -> bool
Sourceval subseteq_effects : effect -> effect -> bool
Sourceval union_effects : effect -> effect -> effect

Functions for building numeric expressions

Sourceval nconstant : Big_int.num -> Ast.nexp
Sourceval nint : int -> Ast.nexp
Sourceval nminus : Ast.nexp -> Ast.nexp -> Ast.nexp
Sourceval ntimes : Ast.nexp -> Ast.nexp -> Ast.nexp
Sourceval npow2 : Ast.nexp -> Ast.nexp
Sourceval nvar : Ast.kid -> Ast.nexp
Sourceval napp : Ast.id -> Ast.nexp list -> Ast.nexp
Sourceval nid : Ast.id -> Ast.nexp

Functions for building numeric constraints

Sourceval nc_false : Ast.n_constraint
Sourceval nc_set : Ast.kid -> Big_int.num list -> Ast.n_constraint
Sourceval nc_int_set : Ast.kid -> int list -> Ast.n_constraint

Functions for building type arguments

Sourceval arg_nexp : ?loc:Ast.l -> Ast.nexp -> Ast.typ_arg
Sourceval arg_order : ?loc:Ast.l -> Ast.order -> Ast.typ_arg
Sourceval arg_typ : ?loc:Ast.l -> Ast.typ -> Ast.typ_arg
Sourceval arg_bool : ?loc:Ast.l -> Ast.n_constraint -> Ast.typ_arg

Functions for working with type quantifiers

Sourceval quant_items : Ast.typquant -> Ast.quant_item list
Sourceval quant_kopts : Ast.typquant -> Ast.kinded_id list
Sourceval quant_split : Ast.typquant -> Ast.kinded_id list * Ast.n_constraint list
Sourceval is_quant_kopt : Ast.quant_item -> bool
Sourceval is_quant_constraint : Ast.quant_item -> bool

Functions to map over annotations in sub-expressions

Sourceval map_exp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.exp -> 'b Ast.exp
Sourceval map_pat_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.pat -> 'b Ast.pat
Sourceval map_pexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.pexp -> 'b Ast.pexp
Sourceval map_lexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.lexp -> 'b Ast.lexp
Sourceval map_letbind_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.letbind -> 'b Ast.letbind
Sourceval map_mpat_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mpat -> 'b Ast.mpat
Sourceval map_mpexp_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mpexp -> 'b Ast.mpexp
Sourceval map_mapcl_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mapcl -> 'b Ast.mapcl
Sourceval map_typedef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.type_def -> 'b Ast.type_def
Sourceval map_fundef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.fundef -> 'b Ast.fundef
Sourceval map_funcl_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.funcl -> 'b Ast.funcl
Sourceval map_mapdef_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.mapdef -> 'b Ast.mapdef
Sourceval map_valspec_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.val_spec -> 'b Ast.val_spec
Sourceval map_scattered_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.scattered_def -> 'b Ast.scattered_def
Sourceval map_def_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast.def -> 'b Ast.def
Sourceval map_ast_annot : ('a Ast.annot -> 'b Ast.annot) -> 'a Ast_defs.ast -> 'b Ast_defs.ast
Sourceval id_loc : Ast.id -> Parse_ast.l

Extract locations from terms

Sourceval kid_loc : Ast.kid -> Parse_ast.l
Sourceval typ_loc : Ast.typ -> Parse_ast.l
Sourceval pat_loc : 'a Ast.pat -> Parse_ast.l
Sourceval exp_loc : 'a Ast.exp -> Parse_ast.l
Sourceval def_loc : 'a Ast.def -> Parse_ast.l

Printing utilities

Note: For debugging and error messages only - not guaranteed to produce parseable Sail, or even print all language constructs!

Sourceval string_of_id : Ast.id -> string
Sourceval string_of_kid : Ast.kid -> string
Sourceval string_of_kind_aux : Ast.kind_aux -> string
Sourceval string_of_kind : Ast.kind -> string
Sourceval string_of_order : Ast.order -> string
Sourceval string_of_nexp : Ast.nexp -> string
Sourceval string_of_typ : Ast.typ -> string
Sourceval string_of_typ_arg : Ast.typ_arg -> string
Sourceval string_of_typ_pat : Ast.typ_pat -> string
Sourceval string_of_n_constraint : Ast.n_constraint -> string
Sourceval string_of_kinded_id : Ast.kinded_id -> string
Sourceval string_of_quant_item : Ast.quant_item -> string
Sourceval string_of_typquant : Ast.typquant -> string
Sourceval string_of_typschm : Ast.typschm -> string
Sourceval string_of_lit : Ast.lit -> string
Sourceval string_of_exp : 'a Ast.exp -> string
Sourceval string_of_pexp : 'a Ast.pexp -> string
Sourceval string_of_lexp : 'a Ast.lexp -> string
Sourceval string_of_pat : 'a Ast.pat -> string
Sourceval string_of_mpat : 'a Ast.mpat -> string
Sourceval string_of_letbind : 'a Ast.letbind -> string
Sourceval string_of_index_range : Ast.index_range -> string

Functions for getting identifiers from toplevel definitions

Sourceval id_of_fundef : 'a Ast.fundef -> Ast.id
Sourceval id_of_mapdef : 'a Ast.mapdef -> Ast.id
Sourceval id_of_type_def : 'a Ast.type_def -> Ast.id
Sourceval id_of_val_spec : 'a Ast.val_spec -> Ast.id
Sourceval id_of_dec_spec : 'a Ast.dec_spec -> Ast.id

Functions for manipulating identifiers

Sourceval id_of_kid : Ast.kid -> Ast.id
Sourceval kid_of_id : Ast.id -> Ast.kid
Sourceval prepend_id : string -> Ast.id -> Ast.id
Sourceval append_id : Ast.id -> string -> Ast.id
Sourceval prepend_kid : string -> Ast.kid -> Ast.kid

Misc functions

Sourceval nexp_frees : Ast.nexp -> KidSet.t
Sourceval nexp_identical : Ast.nexp -> Ast.nexp -> bool
Sourceval is_nexp_constant : Ast.nexp -> bool
Sourceval int_of_nexp_opt : Ast.nexp -> Big_int.num option
Sourceval lexp_to_exp : 'a Ast.lexp -> 'a Ast.exp
Sourceval typ_app_args_of : Ast.typ -> string * Ast.typ_arg_aux list * Ast.l
Sourceval vector_typ_args_of : Ast.typ -> Ast.nexp * Ast.order * Ast.typ
Sourceval vector_start_index : Ast.typ -> Ast.nexp
Sourceval is_order_inc : Ast.order -> bool
Sourceval kopts_of_order : Ast.order -> KOptSet.t
Sourceval kopts_of_nexp : Ast.nexp -> KOptSet.t
Sourceval kopts_of_typ : Ast.typ -> KOptSet.t
Sourceval kopts_of_typ_arg : Ast.typ_arg -> KOptSet.t
Sourceval kopts_of_constraint : Ast.n_constraint -> KOptSet.t
Sourceval kopts_of_quant_item : Ast.quant_item -> KOptSet.t
Sourceval tyvars_of_nexp : Ast.nexp -> KidSet.t
Sourceval tyvars_of_typ : Ast.typ -> KidSet.t
Sourceval tyvars_of_constraint : Ast.n_constraint -> KidSet.t
Sourceval tyvars_of_quant_item : Ast.quant_item -> KidSet.t
Sourceval is_kid_generated : Ast.kid -> bool
Sourceval undefined_of_typ : bool -> Ast.l -> (Ast.typ -> 'annot) -> Ast.typ -> 'annot Ast.exp
Sourceval destruct_pexp : 'a Ast.pexp -> 'a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)
Sourceval construct_pexp : ('a Ast.pat * 'a Ast.exp option * 'a Ast.exp * (Ast.l * 'a)) -> 'a Ast.pexp
Sourceval destruct_mpexp : 'a Ast.mpexp -> 'a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)
Sourceval construct_mpexp : ('a Ast.mpat * 'a Ast.exp option * (Ast.l * 'a)) -> 'a Ast.mpexp
Sourceval is_valspec : Ast.id -> 'a Ast.def -> bool
Sourceval is_fundef : Ast.id -> 'a Ast.def -> bool
Sourceval rename_valspec : Ast.id -> 'a Ast.val_spec -> 'a Ast.val_spec
Sourceval rename_fundef : Ast.id -> 'a Ast.fundef -> 'a Ast.fundef
Sourceval split_defs : ('a Ast.def -> bool) -> 'a Ast.def list -> ('a Ast.def list * 'a Ast.def * 'a Ast.def list) option
Sourceval append_ast : 'a Ast_defs.ast -> 'a Ast_defs.ast -> 'a Ast_defs.ast
Sourceval append_ast_defs : 'a Ast_defs.ast -> 'a Ast.def list -> 'a Ast_defs.ast
Sourceval concat_ast : 'a Ast_defs.ast list -> 'a Ast_defs.ast
Sourceval type_union_id : Ast.type_union -> Ast.id
Sourceval ids_of_def : 'a Ast.def -> IdSet.t
Sourceval ids_of_defs : 'a Ast.def list -> IdSet.t
Sourceval ids_of_ast : 'a Ast_defs.ast -> IdSet.t
Sourceval val_spec_ids : 'a Ast.def list -> IdSet.t
Sourceval record_ids : 'a Ast.def list -> IdSet.t
Sourceval pat_ids : 'a Ast.pat -> IdSet.t
Sourceval subst : Ast.id -> 'a Ast.exp -> 'a Ast.exp -> 'a Ast.exp
Sourceval hex_to_bin : string -> string
Sourceval vector_string_to_bit_list : Ast.lit -> Ast.lit list

Manipulating locations

Sourceval locate : (Ast.l -> Ast.l) -> 'a Ast.exp -> 'a Ast.exp

locate takes an expression and recursively sets the location in every subexpression using a function that takes the orginal location as an argument. Expressions build using mk_exp and similar do not have locations, so they can then be annotated as e.g. locate (gen_loc l) (mk_exp ...) where l is the location from which the code is being generated.

Sourceval locate_pat : (Ast.l -> Ast.l) -> 'a Ast.pat -> 'a Ast.pat
Sourceval locate_lexp : (Ast.l -> Ast.l) -> 'a Ast.lexp -> 'a Ast.lexp
Sourceval locate_typ : (Ast.l -> Ast.l) -> Ast.typ -> Ast.typ
Sourceval unique : Ast.l -> Ast.l

Make a unique location by giving it a Parse_ast.Unique wrapper with a generated number.

Sourceval extern_assoc : string -> Ast.extern option -> string option
Sourceval find_annot_ast : (Lexing.position * Lexing.position) option -> 'a Ast_defs.ast -> (Ast.l * 'a) option

Try to find the annotation closest to the provided (simplified) location. Note that this function makes no guarantees about finding the closest annotation or even finding an annotation at all. This is used by the Emacs mode to provide type-at-cursor functionality and we don't mind if it's a bit fuzzy in that context.

Substitutions

The function X_subst substitutes a type argument into something of type X. The type of the type argument determines which kind of type variables will be replaced

Sourceval nexp_subst : Ast.kid -> Ast.typ_arg -> Ast.nexp -> Ast.nexp
Sourceval order_subst : Ast.kid -> Ast.typ_arg -> Ast.order -> Ast.order
Sourceval typ_subst : Ast.kid -> Ast.typ_arg -> Ast.typ -> Ast.typ
Sourceval typ_arg_subst : Ast.kid -> Ast.typ_arg -> Ast.typ_arg -> Ast.typ_arg
Sourceval subst_kid : (Ast.kid -> Ast.typ_arg -> 'a -> 'a) -> Ast.kid -> Ast.kid -> 'a -> 'a
Sourceval subst_kids_nexp : Ast.nexp KBindings.t -> Ast.nexp -> Ast.nexp
Sourceval subst_kids_typ : Ast.nexp KBindings.t -> Ast.typ -> Ast.typ
Sourceval subst_kids_typ_arg : Ast.nexp KBindings.t -> Ast.typ_arg -> Ast.typ_arg
Sourceval quant_item_subst_kid : Ast.kid -> Ast.kid -> Ast.quant_item -> Ast.quant_item
Sourceval typquant_subst_kid : Ast.kid -> Ast.kid -> Ast.typquant -> Ast.typquant
Sourceval simple_string_of_loc : Parse_ast.l -> string
Sourceval attach_comments : Lexer.comment list -> 'a Ast.def list -> 'a Ast.def list

Attach comments produced by the lexer into their nearest nodes in the abstract syntax tree