package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.EffectsSource

In Sail, we need to distinguish between pure and impure (side-effecting) functions. This is because there are few places, such as top-level let-bindings and loop termination measures where side effects must clearly be forbidden. This module implements inference for which functions are pure and which are effectful, and checking the above purity restrictions.

Sourcetype side_effect

A function is side-effectful if it throws an exception, can exit abnormally (either via an assertion failing or an explicit exit statement), contains a (possibly) incomplete pattern match, or touches a register. Finally, it is transitively side-effectful if it calls another function doing any of the above.

Sourcemodule EffectSet : sig ... end
Sourceval throws : EffectSet.t -> bool
Sourceval pure : EffectSet.t -> bool
Sourceval effectful : EffectSet.t -> bool
Sourceval has_outcome : Ast.id -> EffectSet.t -> bool

Outcome identifiers correspond to the set of user-defined prompt monad constructors in the concurrency interface, replacing the various ad-hoc rmem, wmem, barrier, and so on effects in previous Sail versions. For example, using the concurrency interface in the Sail library, the equivalent to checking for the wmem effect would be:

has_outcome (mk_id "sail_mem_write_request") effects

Sourcetype side_effect_info = {
  1. functions : EffectSet.t Ast_util.Bindings.t;
  2. letbinds : EffectSet.t Ast_util.Bindings.t;
  3. mappings : EffectSet.t Ast_util.Bindings.t;
}
Sourceval empty_side_effect_info : side_effect_info
Sourceval function_is_pure : Ast.id -> side_effect_info -> bool
Sourceval infer_side_effects : bool -> Type_check.typed_ast -> side_effect_info

infer_side_effects asserts_termination ast infers all of the side effect information for ast. If asserts_termination is true then it is assumed that the backend will enforce the termination measures with assertions.

Sourceval check_side_effects : side_effect_info -> Type_check.typed_ast -> unit

Checks constraints on side effects, raising an error if they are violated. Currently these are that termination measures and top-level letbindings must be pure.

Sourceval copy_function_effect : Ast.id -> side_effect_info -> Ast.id -> side_effect_info

copy_function_effect id_from info id_to copies the effect information from id_from to id_to in the side effect information. The order of arguments is to make it convenient to use with List.fold_left.

Sourceval copy_mapping_to_function : Ast.id -> side_effect_info -> Ast.id -> side_effect_info
Sourceval add_function_effect : Ast.id -> side_effect_info -> Ast.id -> side_effect_info

add_function_effect id_from info id_to adds the effect information from id_from to id_to in the side effect information, preserving any existing effects for id_to. The order of arguments is to make it convenient to use with List.fold_left.

Sourceval add_monadic_built_in : Ast.id -> side_effect_info -> side_effect_info

add_monadic_built_in id info notes that id is a monadic external function.

Previous code mostly assumes that side effect info is attached to nodes in the AST. To keep this code working, this rewrite pass attaches effect info into to the AST. Note that the effect info is simplified in its annotated form - it just becomes a boolean representing effectful/non-effectful

Sourceval dump_effects : side_effect_info -> unit

Dumps the given side effect information to stderr.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct