libsail 0.15 · OCaml Package

module StringMap : sig ... end

val optimize_constant_fold : bool Stdlib.ref

val fexp_of_ctor : (Value.StringMap.key * Value.value) -> unit Ast.fexp

val exp_of_value : Value.value -> unit Ast.exp

val safe_primops : (Value.value list -> Value.value) StringMap.t

val opt_fold_to_unit : string list Stdlib.ref

We can specify a list of identifiers that we want to remove from the final AST here. This is useful for removing tracing features in optimized builds, e.g. for booting an OS as fast as possible.

Basically we just do this by mapping

f(x, y, z) -> ()

when f is in the list of identifiers to be mapped to unit. The advantage of doing it like this is if x, y, and z are computationally expensive then we remove them also. String concatentation is very expensive at runtime so this is something we really want when cutting out tracing features. Obviously it's important that they don't have any meaningful side effects, and that f does actually have type unit.

val fold_to_unit : Ast_util.IdSet.elt -> bool

val is_constant : Type_check.tannot Ast.exp -> bool

val is_constant_fexp : Type_check.tannot Ast.fexp -> bool

val run : Interpreter.frame -> Value.value

This rewriting pass looks for function applications (E_app) expressions where every argument is a literal. It passes these expressions to the OCaml interpreter in interpreter.ml, and reconstructs the values returned back into expressions which are then re-typechecked and re-inserted back into the AST.

We don't use the effect system to decide if expressions are safe to evaluate, because this ignores I/O, and would force us to ignore functions that maybe throw exceptions internally but as called are totally safe. Instead any exceptions during evaluation are caught, and the original expression is kept. Some causes of this could be:

Function tries to read/write register.
Calls an unsafe primop.
Throws an exception that isn't caught.

val initial_state : 
  Type_check.tannot Ast_defs.ast ->
  Type_check.Env.t ->
  Interpreter.lstate * Interpreter.gstate

type fixed = {

registers : Type_check.tannot Ast.exp Ast_util.Bindings.t;
fields : Type_check.tannot Ast.exp Ast_util.Bindings.t Ast_util.Bindings.t;

}

val no_fixed : fixed

val rw_exp : 
  fixed ->
  string ->
  (unit -> 'a) ->
  (unit -> 'b) ->
  Interpreter.state ->
  Type_check.tannot Ast.exp ->
  Type_check.tannot Ast.exp

val rewrite_exp_once : 
  string ->
  Interpreter.state ->
  Type_check.tannot Ast.exp ->
  Type_check.tannot Ast.exp

val rewrite_constant_function_calls' : 
  fixed ->
  string ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.tannot Ast_defs.ast

val rewrite_constant_function_calls : 
  fixed ->
  string ->
  Type_check.tannot Ast_defs.ast ->
  Type_check.tannot Ast_defs.ast

type to_constant =

| Register of Ast.id * Ast.typ * Type_check.tannot Ast.exp
| Register_field of Ast.id * Ast.id * Ast.typ * Type_check.tannot Ast.exp

package libsail