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.
val name : target -> stringval run_pre_parse_hook : target -> unit -> unitval run_pre_rewrites_hook :
target ->
Type_check.tannot Ast_defs.ast ->
Effects.side_effect_info ->
Type_check.Env.t ->
unitval rewrites : target -> Rewrites.rewrite_sequenceval action :
target ->
Yojson.Basic.t option ->
string ->
string option ->
Type_check.tannot Ast_defs.ast ->
Effects.side_effect_info ->
Type_check.Env.t ->
unitval asserts_termination : target -> boolval register :
name:string ->
?flag:string ->
?description:string ->
?options:(Arg.key * Arg.spec * Arg.doc) list ->
?pre_parse_hook:(unit -> 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 ->
(Yojson.Basic.t option ->
string ->
string option ->
Type_check.tannot Ast_defs.ast ->
Effects.side_effect_info ->
Type_check.Env.t ->
unit) ->
targetUsed 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:
val get_the_target : unit -> target optionReturn 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.
val get : name:string -> target option