package elpi

You can search for identifiers within the package.

in-package search v0.2.0

elpi
- Elpi
  - API
    
    AlgebraicData
    
    Ast
    
    Loc
    
    BuiltIn
    
    BuiltInData
    
    BuiltInPredicate
    
    Notation
    
    Compile
    
    StrSet
    
    Conversion
    
    Data
    
    StrMap
    
    Execute
    
    FlexibleData
    
    Elpi
    
    Host
    
    Map
    
    Host
    
    OpaqueData
    
    Parse
    
    Pp
    
    Ast
    
    Query
    
    Quotation
    
    RawData
    
    Constants
    
    Map
    
    Set
    
    RawOpaqueData
    
    RawPp
    
    Debug
    
    RawQuery
    
    Setup
    
    State
    
    Utils
  - Builtin
elpi.trace
- Trace
  - Runtime

Legend:
Library
Module
Module type
Parameter
Class
Class type

type quotation =
  depth:int ->
  State.t ->
  Ast.Loc.t ->
  string ->
  State.t * Data.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 : 'a 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!)

Like quotations but for identifiers that begin and end with * "`" or "'", e.g. `this` and 'that'. Useful if the object language * needs something that looks like a string but with a custom compilation * (e.g. CD.string like but with a case insensitive comparison)

val declare_backtick : 
  name:string ->
  (State.t -> string -> State.t * Data.term) ->
  unit

val declare_singlequote : 
  name:string ->
  (State.t -> string -> State.t * Data.term) ->
  unit