package elpi

  1. Overview
  2. Docs

This module lets one extend the compiler by: * - "compiling" the query by hand * - providing quotations

module State : sig ... end

In order to implement quotations one may * need to stick some data into the compiler state that can indeed be * extended. A piece of compiler state can also be kept and used at runtime, * e.g. if it contains some custom constraints, see CustomState

val query : Compile.program -> (depth:int -> State.t -> State.t * Data.term) -> Compile.query

Generate a query starting from a compiled/hand-made term

val is_Arg : State.t -> Data.term -> bool
val fresh_Arg : State.t -> name_hint:string -> args:Data.term list -> State.t * string * Data.term
type quotation = depth:int -> State.t -> string -> State.t * Data.term

From an unparsed string to a term

val set_default_quotation : quotation -> unit

The default quotation {{code}}

val register_named_quotation : name:string -> quotation -> unit

Named quotation {{name:code}}

val lp : quotation

The anti-quotation to lambda Prolog

val quote_syntax : Compile.query -> Data.term list * Data.term

See elpi_quoted_syntax.elpi (EXPERIMENTAL, used by elpi-checker)

val term_at : depth:int -> Ast.query -> Data.term

To implement the string_to_term built-in (AVOID, makes little sense * if depth is non zero, since bound variables have no name!)