package libsail

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

Infrastructure for registering Sail targets/backends

Target type and accessor functions

type target
val name : target -> string
val run_pre_parse_hook : target -> unit -> unit
val run_pre_descatter_hook : target -> Type_check.tannot Ast_defs.ast -> Type_check.Env.t -> unit
val action : target -> string -> string option -> Type_check.tannot Ast_defs.ast -> Effects.side_effect_info -> Type_check.Env.t -> unit
val asserts_termination : target -> bool

Target registration

val register : name:string -> ?flag:string -> ?description:string -> ?options:(Stdlib.Arg.key * Stdlib.Arg.spec * Stdlib.Arg.doc) list -> ?pre_parse_hook:(unit -> unit) -> ?pre_descatter_hook: (Type_check.tannot Ast_defs.ast -> Type_check.Env.t -> unit) -> ?pre_rewrites_hook: (Type_check.tannot Ast_defs.ast -> Effects.side_effect_info -> Type_check.Env.t -> unit) -> ?rewrites:(string * Rewrites.rewriter_arg list) list -> ?asserts_termination:bool -> (string -> string option -> Type_check.tannot Ast_defs.ast -> Effects.side_effect_info -> Type_check.Env.t -> unit) -> target

Used for plugins to register custom Sail targets/backends.

register_target ~name:"foo" action will create an option -foo, that will run the provided action on the Sail abstract syntax tree after performing common frontend processing.

The various optional arguments can be used to further control the behavior of the target:

  • parameter ?flag

    A custom flag. By default it will use the name parameter

  • parameter ?description

    A custom description for the command line flag

  • parameter ?options

    Additional options for the Sail executable

  • parameter ?pre_parse_hook

    A function to call right at the start, before parsing

  • parameter ?pre_rewrites_hook

    A function to call before doing any rewrites

  • parameter ?rewrites

    A sequence of Sail to Sail rewrite passes for the target

  • parameter ?asserts_termination

    Whether termination measures are enforced by assertions in the target

val get_the_target : unit -> target option
val get : name:string -> target option
val extract_options : unit -> (Stdlib.Arg.key * Stdlib.Arg.spec * Stdlib.Arg.doc) list

Used internally to dynamically update the option list when loading plugins