Module API.Setup

type state_descriptor
type quotations_descriptor
type hoas_descriptor
type builtins
type calc_descriptor
type flags
type elpi
val init : ?flags:flags -> ?state:state_descriptor -> ?quotations:quotations_descriptor -> ?hoas:hoas_descriptor -> ?calc:calc_descriptor -> builtins:builtins list -> ?file_resolver:( ?cwd:string -> unit:string -> unit -> string ) -> ?legacy_parser:bool -> unit -> elpi

Initialize ELPI.

init must be called before invoking the parser.

  • parameter flags

    for the compiler, see Compile.flags

  • parameter builtins

    the set of built-in predicates, eg Elpi.Builtin.std_builtins

  • parameter file_resolver

    maps a file name to an absolute path, if not specified the options like -I or the env variable TJPATH serve as resolver. The resolver returns the abslute file name (possibly adjusting the unit extension). By default it fails. See also Parse.std_resolver.

  • returns

    a handle elpi to an elpi instance equipped with the given builtins and where accumulate resolves files with the given file_resolver.

val usage : string

Usage string

val trace : string list -> string list

Set tracing options. trace argv can be called before Execute. returns options not known to the trace system.

val set_warn : ( ?loc:Ast.Loc.t -> string -> unit ) -> unit

Override default runtime error functions (they call exit)

val set_error : ( ?loc:Ast.Loc.t -> string -> 'a ) -> unit
val set_anomaly : ( ?loc:Ast.Loc.t -> string -> 'a ) -> unit
val set_type_error : ( ?loc:Ast.Loc.t -> string -> 'a ) -> unit
val set_std_formatter : Stdlib.Format.formatter -> unit
val set_err_formatter : Stdlib.Format.formatter -> unit
val legacy_parser_available : bool

The legacy parser is an optional build dependency