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
<https://github.com/LPCIC/coq-elpi/tree/master/examples/example_plugin>`_;
this chapter reproduces and explains it.

.. contents::

Project layout
-----------------

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

.. code-block:: text

   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``:

.. code-block:: text

   (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
<https://github.com/LPCIC/coq-elpi/blob/master/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):

.. code-block:: text

   ; 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:

.. code-block:: ocaml

   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
:e:`AlgebraicData.declare`, which builds the *embed*/*readback* functions
translating between the OCaml type and its Elpi representation
automatically from a description of its constructors:

.. code-block:: ocaml

   (* 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 :e:`MLCode`/:e:`Pred`:

.. code-block:: ocaml

   (* 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 :type:`term`/etc. API
documentation), each paired with the :e:`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):

.. code-block:: ocaml

   (* 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:

.. code-block:: text

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

   (include_subdirs qualified)

.. code-block:: coq

   (* 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``:

.. code-block:: text

   ; 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})))))

.. code-block:: elpi

   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 :doc:`coq-commands`: 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 :builtin:`coq.say` and
friends to their declaration (see :doc:`/reference/builtins`) is available
to plugins: :e:`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``.

.. code-block:: ocaml

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

.. code-block:: text

   ; 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:

.. code-block:: elpi

   % 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``):

.. code-block:: text

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

   (include_subdirs qualified)

.. code-block:: coq

   (* 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:

.. code-block:: console

   $ dune build
   $ dune build @runtest