###################
Built-in predicates
###################

A **builtin** is a predicate whose body is OCaml rather than Elpi, reached
through the foreign function interface (:doc:`embedding`). Elpi's own library
ships close to two hundred of them, from ``=`` to the garbage-collector
controls; a host application registers more the same way.

The FFI fixes the shape a builtin can have. Each argument is declared *input*
or *output* and carries a *conversion* between an Elpi term and an OCaml
value, so the OCaml code receives its inputs already converted and hands back
its outputs to be converted on the way out. A builtin succeeds once or fails
(by raising ``No_clause``); it does not backtrack and does not offer a second
solution. A term it
has no conversion for it can still carry through untouched, as ``any``.

``elpi -document-builtins`` prints the exhaustive, generated reference: one
signature and doc comment per predicate, the same text checked in as
``src/builtin.elpi``. Throughout this manual a name written like
:stdlib:`print` links to that predicate's declaration line in
``src/builtin.elpi`` on GitHub. What follows is a tour by category, saying what
each group is for and which chapter covers it in depth where one does.


Logic, control and inspection
=============================

:stdlib:`=` unifies, with the occur check; :stdlib:`unsound_unif` does the same *without*
it and so can build a cyclic term (:doc:`features/unification-and-variables`,
where it is defined with ``:nooc``). :stdlib:`same_term`, infix ``==``, tests
plain syntactic equality, assigning nothing. ``pattern_match T P`` matches
``T`` against the pattern ``P``, assigning only ``P``'s variables
(:doc:`syntax/terms`).

:stdlib:`declare_constraint` and :stdlib:`print_constraints` are covered in
:doc:`syntax/constraint-handling-rules`.

The cut :stdlib:`!`, :stdlib:`not`, :stdlib:`if` / :stdlib:`if2`, :stdlib:`halt` / :stdlib:`stop`, :stdlib:`std.once`
and :stdlib:`std.do!` are covered in :doc:`features/control-and-cut`, and
``pi`` / ``sigma`` in :doc:`syntax/inference-rules-and-queries`.

``ground_term T`` checks that ``T`` has no unification variables left;
:stdlib:`closed_term` yields a fresh variable barred from naming any eigenvariable
(:doc:`features/binders-and-hoas`); :stdlib:`cmp_term` orders two terms
structurally, and only works when both are ground.

:stdlib:`name` / :stdlib:`names` list the eigenvariables in scope, :stdlib:`var` recognises and
takes apart a unification variable (:doc:`features/unification-and-variables`
for its ``uvar Hd Args`` form), :stdlib:`constant` a global constant, and
``occurs A T`` checks whether the atom ``A`` appears in ``T``
(:doc:`features/unification-and-variables`).

:stdlib:`new_int` hands out a strictly increasing integer and :stdlib:`new_safe` hands
out a store
that survives backtracking; both step outside Elpi's usual scoping, so use
them sparingly.


Arithmetic
==========

``X is Expr`` evaluates ``Expr`` and unifies the result with ``X``; :stdlib:`calc`
is the same as a function, for use with spilling (:doc:`features/spilling`):
``f {calc (N + 1)}``. The precedences of every operator below are in
:doc:`syntax/lexical-conventions`.

Evaluated inside ``is`` / :stdlib:`calc`:

* **binary** ``+`` ``-`` ``*`` (``int`` or ``float``), ``/`` (``float``),
  ``div`` ``mod`` (``int``), ``^`` (``string`` concatenation);
* **unary** ``~`` (negation), ``abs``, and, for ``float``, ``sqrt`` ``sin``
  ``cos`` ``arctan`` ``ln``;
* **two-argument functions** ``min`` ``max``;
* **conversions** ``int_to_real`` ``truncate`` ``floor`` ``ceil``
  (``int`` ↔ ``float``), ``int_to_string`` ``string_to_int``
  ``real_to_string`` ``substring`` ``size`` (``string``), ``chr`` ``rhc``
  (``int`` ↔ one-character ``string``);
* type-suffixed variants that fix the operand type instead of inferring it:
  ``i+ i- i* i~ iabs`` for ``int``, ``r+ r- r* r~ rabs`` for ``float``.

Comparisons are *goals*, not expressions: ``X < Y`` succeeds or fails, it is
not written under ``is``. ``<`` ``>`` ``=<`` ``>=`` work on ``int``,
``float`` or ``string``, with ``i< r< s<`` … fixing the type.

This set is **extensible from the host application**: ``API.Calc.register``
adds an operation (a symbol, its argument types, and an OCaml function) to a
``calc_descriptor`` passed to ``API.Setup.init ~calc`` (:doc:`embedding`).


Standard data types
===================

These are declared in the builtin library, ready to use without an
``accumulate``:

.. code-block:: elpi

   data bool.
   symb tt bool.
   symb ff bool.

   data pair A B.
   symb pr A -> B -> pair A B.       % + func fst, func snd

   data option A.
   symb none option A.
   symb some A -> option A.

   data cmp.
   symb eq cmp.
   symb lt cmp.
   symb gt cmp.

   data diagnostic.
   symb ok diagnostic.
   symb error string -> diagnostic.

   data triple A B C.
   symb triple A -> B -> C -> triple A B C.   % + triple_1..3

``bool`` uses ``tt`` / ``ff`` because :stdlib:`true` / :stdlib:`false` are goals; ``pair``'s
constructor is ``pr`` because ``,`` is conjunction; ``cmp`` is the result of a
three-way comparison: :stdlib:`cmp_term`, or a comparator a caller supplies, as
:stdlib:`std.map` and ``std.set`` require; ``diagnostic`` is
returned by builtins that report a *reason* for failing rather than just
failing (``ok`` / ``error "message"``). ``list`` (``::`` / ``[]``) is built
in too (:doc:`syntax/terms`).

A short tour of :stdlib:`calc`, a ``pair``, :stdlib:`term_to_string`, :stdlib:`rex.split` and a
reseeded generator:

**code/builtins-tour.elpi:**

.. literalinclude:: code/builtins-tour.elpi
   :linenos:
   :language: elpi

.. code-block:: console

   calc: 14
   term_to_string: pr 1 one
   rex.split: [a, b, c]
   seeded random repeats: 14 14
   


Regular expressions and randomness
==================================

:stdlib:`rex.match`, :stdlib:`rex.replace` and :stdlib:`rex.split` (OCaml's ``Str`` syntax, not
PCRE) cover the common text-processing needs. ``random.int N`` draws a
uniform integer in :math:`[0, N)`; ``random.init Seed`` reseeds the
generator, making a sequence reproducible: the same seed always draws the
same numbers.


Input, output and the file system
=================================

:stdlib:`print` and :stdlib:`dprint` write their arguments to standard output (:stdlib:`dprint`
shows raw terms); :stdlib:`term_to_string` renders a term to a ``string`` instead of
printing it. Beyond that Elpi has the stream I/O of OCaml:

* :stdlib:`open_in` / :stdlib:`open_out` / :stdlib:`open_append` open a file; :stdlib:`open_string`
  turns a string into a readable stream; ``std_in`` / ``std_out`` /
  ``std_err`` are the standard streams;
* ``input InStream Bytes S`` reads a fixed number of bytes, :stdlib:`input_line`
  reads up to the newline, :stdlib:`lookahead` peeks one byte, :stdlib:`eof` tests for
  end of input;
* ``output OutStream S`` writes, :stdlib:`flush` forces pending output out,
  :stdlib:`close_in` / :stdlib:`close_out` close.

``sys.*`` reaches the file system and the process environment:
:stdlib:`sys.file_exists`, :stdlib:`sys.is_directory`, :stdlib:`sys.mkdir` / :stdlib:`sys.rmdir`,
:stdlib:`sys.remove` / :stdlib:`sys.rename`, :stdlib:`sys.readdir`, :stdlib:`sys.chdir` /
:stdlib:`sys.getcwd`, plus :stdlib:`getenv`, :stdlib:`gettimeofday` and :stdlib:`system` (run a shell
command). The calls that can fail for an external reason return a
``diagnostic`` (``ok`` or ``error "…"``) rather than just failing.
:stdlib:`unix.process.open` / :stdlib:`unix.process.close` spawn a subprocess and reap
it, handing back its three standard streams.

**code/builtins-io.elpi:**

.. literalinclude:: code/builtins-io.elpi
   :linenos:
   :language: elpi

.. code-block:: console

   first two lines: alpha beta
   string map, two -> 2
   


Typed finite maps
=================

``std.string.map``, ``std.int.map`` and ``std.loc.map`` are FFI-backed
persistent maps over one fixed key type (``std.string.set`` and
``std.int.set`` are the matching sets). Each map has ``.empty``, ``.mem``,
``.add``, ``.remove``, ``.find`` and ``.bindings``, plus ``.filter`` /
``.map`` / ``.fold`` taking an Elpi ``func``; the value type has to be a
closed term. The general, any-key structures :stdlib:`std.map` and ``std.set``,
written in Elpi rather than OCaml, are covered in :doc:`standard-library`.


Garbage collector and runtime
=============================

:stdlib:`gc.get` / :stdlib:`gc.set` read and write the OCaml garbage-collector
parameters, :stdlib:`gc.stat` / :stdlib:`gc.quick-stat` report live statistics, and
:stdlib:`gc.minor` / :stdlib:`gc.major` / :stdlib:`gc.full` / :stdlib:`gc.compact` force a
collection. :stdlib:`trace.counter` reads a named trace point
(:doc:`debugging-and-tracing`). These matter only when profiling or trimming
the footprint of a long-running embedding.