Adding builtin predicates via an OCaml plugin

Everything in the previous tutorials extends Rocq from within Elpi: new commands, tactics and Db-backed state are all written in Elpi itself, loaded by the rocq-elpi plugin that ships with Rocq-Elpi. Sometimes, though, you want to give Elpi a new builtin data type or predicate that is implemented in OCaml directly -- typically to wrap an existing OCaml library, to get at data structures or algorithms that would be awkward to write in Elpi, or for performance.

This chapter walks through a complete, minimal scaffold for exactly that: a standalone opam package, built on top of rocq-elpi, that adds a new Elpi data type myType and a new predicate compute implemented in OCaml. The full, up to date source lives in the repository under examples/example_plugin; this chapter reproduces and explains it.

Project layout

A plugin is its own dune package, separate from the project(s) that will use it:

example_plugin/
  dune-project
  myExtension.opam            (generated by dune from dune-project)
  myExtension-tests.opam      (generated by dune from dune-project)
  src/
    dune
    my_extension_plugin.mlpack
    my_extension_ocaml_code.ml   -- the OCaml side of the new builtins
  theories/
    dune
    Loader.v                     -- loads the plugin into Rocq
  elpi/
    dune
    my-extension-elpi-code.elpi  -- companion Elpi library code
  doc/
    dune
    gen_doc.ml                   -- generates myExtension.elpi (reference doc)
  tests/
    dune
    test.v                       -- exercises the new builtins from Rocq

dune-project declares the package(s) and their dependency on rocq-elpi:

(lang dune 3.13)
(using coq 0.8)
(name Ext)

(generate_opam_files true)

(source (github username/reponame))
(authors "Author Name <author@example.com>")
(maintainers "Maintainer Name <maintainer@example.com>")
(license LICENSE)
(documentation https://url/to/documentation)

(package
 (name myExtension)
 (synopsis "myExtension adds extra Elpi datatypes and APIs")
 (description "This package provides some extra goodies")
 (depends rocq-elpi))

(package
 (name myExtension-tests)
 (synopsis "myExtension tests - do not install")
 (description "myExtension tests - do not install")
 (depends rocq-elpi))

Splitting the tests into their own package keeps them from being pulled in (and built) by users who just want to use the plugin, matching the convention already used by rocq-elpi itself (see rocq-elpi.opam and its sibling test packages).

The OCaml side: a new data type and a new predicate

The new builtins live in an ordinary OCaml library, src/, which depends on the elpi package (the Elpi library itself, not rocq-elpi -- new builtins are plain Elpi builtins, they don't need anything Rocq-specific unless they manipulate Rocq terms):

; src/dune
(library
 (name myExtension_plugin)
 (public_name myExtension.plugin)
 (libraries elpi))

src/my_extension_ocaml_code.ml is where the actual work happens. First, an ordinary OCaml algebraic data type:

module API = Elpi.API
module E = API.RawData

(* An algebraic data type with the API we want to expose: myType and compute *)
type myType = Constant : int -> myType | SumOf : (myType * myType) -> myType
let rec compute (s : myType) = match s with
  | Constant n -> n
  | SumOf (s1, s2) -> compute s1 + compute s2

Then, the Elpi-facing declarations. First the data type itself, via AlgebraicData.declare, which builds the embed/readback functions translating between the OCaml type and its Elpi representation automatically from a description of its constructors:

(* Declaring the elpi symbol corresponding to the constructors of myType
   is optional, only needed if one uses the RawData APIs *)
let constant = E.Constants.declare_global_symbol "constant"
let sumof = E.Constants.declare_global_symbol "sumof"

(* declaring the embed/readback function linking OCaml and Elpi *)
let myType : myType API.Conversion.t = API.(AlgebraicData.declare {
  ty = TyName "myType";
  doc = "description for the new elpi type";
  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
  constructors = [
   K("constant","",A(BuiltInData.int, N),
     B (fun x -> Constant x),
     M (fun ~ok ~ko  t -> match t with Constant n -> ok n | _ -> ko ()));
   K("sumof","",S(S(N)),
     B (fun x y -> SumOf (x, y)),
     M (fun ~ok ~ko t -> match t with SumOf (x,y) -> ok x y | _ -> ko ()))
]
} |> ContextualConversion.(!<))

Each constructor is described by a K entry: its Elpi-visible name, a docstring, the shape of its arguments (A for an atomic argument of a given type, S for a sub-term of the type itself, N to terminate the argument list), a B uild function (OCaml constructor -> the value) and a M atch function (the value -> OCaml constructor, or failure via ko).

Next, the new predicate itself, via MLCode/Pred:

(* declaring a new API *)
let compute_api =
  API.BuiltIn.MLCode(Pred("compute",
    In(myType, "Expression",
    Out(myType, "Result",
    Easy("Result is the normal form of Expression"))),
    (* The implementation of the API is the result of compute *)
      (fun a _ ~depth:_ -> (), Some (Constant (compute a)))),
    DocAbove)

In/Out describe the predicate's argument modes (matching the -> notation used throughout this manual's own term/etc. API documentation), each paired with the Conversion.t value that knows how to translate it and a short docstring; the last argument to In/Out is either another mode-annotated argument or, once the signature is complete, the actual OCaml implementation together with its own docstring.

Finally, both are registered together under the name of the .elpi file they should appear to come from (this is purely for documentation and error-message purposes -- nothing is actually read from disk):

(* we declare the name of the file in which the new builtins are declared
   and the exported stuff (data types and predicates) *)
let builtins = API.BuiltIn.declare ~file_name:"myExtension.elpi" [
  MLData myType;
  compute_api
]

Loading the plugin from Rocq

The plugin is an OCaml findlib library, so Rocq needs to be told to load it, exactly like any other Rocq plugin -- this is the one place that is Rocq-specific:

; theories/dune
(coq.theory
 (name myExtension)
 (theories elpi_elpi elpi myExtension.lib)
 (plugins myExtension.plugin)
 (package myExtension))

(include_subdirs qualified)

(* theories/Loader.v *)
Declare ML Module "myExtension.plugin".

From elpi Require Import elpi.

From myExtension.lib Extra Dependency "my-extension-elpi-code.elpi" as myExtensionLib.

A downstream user of the plugin just needs From myExtension Require Import Loader. to get both the OCaml builtins and (see below) the companion Elpi library code declared as an accumulable dependency.

A companion Elpi library

Not everything needs to be implemented in OCaml: it is often convenient to ship a small Elpi library alongside the OCaml builtins, for code that is just as easily (or more maintainably) written directly in Elpi. Here, a tiny library converting between Elpi integers and Rocq's unary nat:

; elpi/dune
(coq.theory
 (name myExtension.lib)
 (theories elpi)
 (plugins myExtension.plugin)
 (package myExtension))

(include_subdirs qualified)

; this rule is needed for loading elpi files as extra deps
(rule
 (target dummy.v)
 (deps (glob_files *.elpi))
 (action
  (with-stdout-to %{target}
   (progn (run rocq_elpi_shafile %{deps})))))

func int2nat int -> term.
int2nat 0 {{0}} :- !.
int2nat N {{S lp:R}} :- N > 0, N' is N - 1, int2nat N' R.

func nat2int term -> int.
nat2int {{0}} 0.
nat2int {{S lp:R}} N :- nat2int R N', N is N' + 1.

This is exactly the Extra Dependency/Elpi Accumulate File mechanism described in Writing commands in Elpi: the .elpi file is declared as an accumulable dependency (myExtensionLib, in Loader.v above) by the plugin's own theories, and downstream code accumulates it by name -- see tests/test.v below.

Generating reference documentation for the new builtins

The same mechanism this manual itself uses to link coq.say and friends to their declaration (see Builtins and relevant files) is available to plugins: API.BuiltIn.document_file renders every declared builtin's docstring into a .elpi file with the same pred/data syntax as builtin-doc/coq-builtin.elpi.

(* doc/gen_doc.ml *)
let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated"
  MyExtension_plugin.My_extension_ocaml_code.builtins

; doc/dune
(executable
 (name gen_doc)
 (libraries myExtension.plugin))

(rule
 ; myExtension.elpi contains the doc of the builtins defined in the myExtension plugin
 (targets myExtension.elpi)
 (deps gen_doc.exe)
 (mode promote)
 (action (run ./gen_doc.exe)))

Running this (dune build doc/myExtension.elpi, or just dune build, since (mode promote) writes the result back into the source tree) produces:

% description for the new elpi type
builtin data myType.
builtin symb constant : int -> myType = "1".
builtin symb sumof    : myType -> myType -> myType = "1".

% [compute Expression Result] Result is the normal form of Expression
builtin func compute myType -> myType.

Using the plugin

Downstream code loads the plugin's loader, the companion Elpi library (via its Extra Dependency name), and the generated documentation file (via Elpi Accumulate Plugin, which loads a .elpi file that was declared through BuiltIn.declare's file_name rather than through Extra Dependency):

; tests/dune
(coq.theory
 (name myExtension.tests)
 (package myExtension-tests)
 (theories elpi_elpi elpi myExtension myExtension.lib))

(include_subdirs qualified)

(* tests/test.v *)
From elpi Require Import elpi.

From myExtension Require Import Loader.
From myExtension.lib Extra Dependency "my-extension-elpi-code.elpi" as myExtensionLib.

Elpi Command test.
Elpi Accumulate Plugin "myExtension.elpi".
Elpi Accumulate File myExtensionLib.
Elpi Accumulate  lp:{{

  func encode term -> myType.
  encode {{lp:X + lp:Y}} (sumof X1 Y1) :- encode X X1, encode Y Y1, !.
  encode T (constant N) :- nat2int T N, !.
  encode T _ :- coq.error "This Rocq test does not fit myType" T.

  func decode myType -> term.
  decode (constant N) T :- int2nat N T, !.
  decode T _ :- coq.error "Not in normal form" T.
}}.

Elpi Query  lp:{{
  encode {{2 + 3}} X,

  compute X Z,

  decode Z {{ 5 }}.
}}.

This command converts the Rocq term 2 + 3 into myType (sumof (constant 2) (constant 3)), calls the new OCaml-implemented compute predicate to normalize it to constant 5, and converts that back into the Rocq term 5 -- exercising the data type conversion, the OCaml predicate, and the companion Elpi library all in one query.

Building and testing

Being an ordinary dune package, the scaffold builds and tests the usual way, from the example_plugin directory:

$ dune build
$ dune build @runtest