package libsail

  1. Overview
  2. Docs

Initial desugaring pass over AST after parsing


val opt_undefined_gen : bool Stdlib.ref

Generate undefined_T functions for every type T. False by default.

val opt_fast_undefined : bool Stdlib.ref

Generate faster undefined_T functions. Rather than generating functions that allow for the undefined values of enums and variants to be picked at runtime using a RNG or similar, this creates undefined_T functions for those types that simply return a specific member of the type chosen at compile time, which is much faster. These functions don't have the right effects, so the -no_effects flag may be needed if this is true. False by default.

val opt_magic_hash : bool Stdlib.ref

Allow # in identifiers when set, much like the GHC option of the same name

val have_undefined_builtins : bool Stdlib.ref

This is a bit of a hack right now - it ensures that the undefiend builtins (undefined_vector etc), only get added to the AST once. The original assumption in sail is that the whole AST gets processed at once (therefore they could only get added once), and this isn't true any more with the interpreter. This needs to be public so the interpreter can set it back to false if it unloads all the loaded files.

val undefined_builtin_val_specs : Ast_util.uannot Ast.def list

Val specs of undefined functions for builtin types that get added to the AST if opt_undefined_gen is set (minus those functions that already exist in the AST).

Desugar and process AST

val generate_undefineds : Ast_util.IdSet.t -> Ast_util.uannot Ast.def list -> Ast_util.uannot Ast.def list
val generate_enum_functions : Ast_util.IdSet.t -> Ast_util.uannot Ast.def list -> Ast_util.uannot Ast.def list
val process_ast : ?generate:bool -> Parse_ast.defs -> Ast_util.uannot Ast_defs.ast

If the generate flag is false, then we won't generate any auxilliary definitions, like the initialize_registers function

Parsing expressions and definitions from strings

val extern_of_string : ?pure:bool -> -> string -> Ast_util.uannot Ast.def
val val_spec_of_string : -> string -> Ast_util.uannot Ast.def
val defs_of_string : (string * int * int * int) -> string -> Ast_util.uannot Ast.def list
val ast_of_def_string : (string * int * int * int) -> string -> Ast_util.uannot Ast_defs.ast
val ast_of_def_string_with : (string * int * int * int) -> (Parse_ast.def list -> Parse_ast.def list) -> string -> Ast_util.uannot Ast_defs.ast
val exp_of_string : string -> Ast_util.uannot Ast.exp
val typ_of_string : string -> Ast.typ
val constraint_of_string : string -> Ast.n_constraint

Parsing files

val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.def list

Parse a file into a sequence of comments and a parse AST

  • parameter ?loc

    If we get an error reading the file, report the error at this location

val parse_file_from_string : filename:string -> contents:string -> Lexer.comment list * Parse_ast.def list

Innovation. Community. Security.