package libsail

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

Module Libsail.TargetSource

Infrastructure for plugins to register Sail targets.

A target is essentially a custom backend for the Sail compiler, along with various hooks and options that toggle various frontend behaviours. A target therefore specifies what kind of output Sail will produce. For example, we provide default plugins that define targets to output Lem, C, OCaml, Coq, and so on.

Target type and accessor functions

Sourcetype target
Sourceval name : target -> string
Sourceval run_pre_parse_hook : target -> unit -> unit
Sourceval run_pre_initial_check_hook : target -> string list -> unit
Sourceval run_pre_rewrites_hook : target -> Type_check.typed_ast -> Effects.side_effect_info -> Type_check.Env.t -> unit
Sourceval action : target -> string option -> Interactive.State.istate -> unit
Sourceval asserts_termination : target -> bool
Sourceval supports_abstract_types : target -> bool

If a target does not support abstract types, then the user must provide a concrete instantiation for Sail.

Sourceval supports_runtime_config : target -> bool

If a target does not support runtime configuration, then the configuration must be provided statically at build time.

Sourceval skip_initial_rewrite : target -> bool

Target registration

Sourceval register : name:string -> ?flag:string -> ?description:string -> ?options:(Flag.t * Arg.spec * string) list -> ?pre_parse_hook:(unit -> unit) -> ?pre_initial_check_hook:(string list -> unit) -> ?pre_rewrites_hook: (Type_check.typed_ast -> Effects.side_effect_info -> Type_check.Env.t -> unit) -> ?skip_initial_rewrite:bool -> ?rewrites:(string * Rewrites.rewriter_arg list) list -> ?asserts_termination:bool -> ?supports_abstract_types:bool -> ?supports_runtime_config:bool -> (string option -> Interactive.State.istate -> 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 arguments can be used to further control the behavior of the target:

  • parameter ~name

    The name of the target

  • parameter ?flag

    A custom command line flag to invoke the target. 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_initial_check_hook

    A function to call after parsing, but before de-sugaring

  • parameter ?pre_rewrites_hook

    A function to call before doing any rewrites

  • parameter ?skip_initial_rewrite

    Skips the initial rewriting pass

  • 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

  • parameter ?supports_abstract_types

    Whether the target supports abstract types to be passed to the target

  • parameter ?supports_runtime_config

    Whether the target supports runtime configuration

The final unnamed parameter is the main backend function that is called after the frontend has finished processing the input.

Sourceval empty_action : string option -> Interactive.State.istate -> unit

Use if you want to register a target that does nothing

Sourceval get_the_target : unit -> target option

Return the current target. For example, if we register a 'coq' target, and Sail is invoked with `sail -coq`, then this function will return the coq target.

Sourceval get : name:string -> target option
Sourceval extract_registered : unit -> string list

Used internally when updating the option list during plugin loading

Sourceval extract_options : unit -> (Flag.t * Arg.spec * string) list

Used internally to dynamically update the option list when loading plugins