Built-in predicates

A builtin is a predicate whose body is OCaml rather than Elpi, reached through the foreign function interface (Embedding and extending Elpi). 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 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

(=) unifies, with the occur check; unsound_unif does the same without it and so can build a cyclic term (Unification and variables, where it is defined with :nooc). same_term, infix ==, tests plain syntactic equality, assigning nothing. pattern_match T P matches T against the pattern P, assigning only P’s variables (Terms).

declare_constraint and print_constraints are covered in Constraint handling rules.

The cut !, not, if / if2, halt / stop, std.once and std.do! are covered in Control and cut, and pi / sigma in Inference rules and queries.

ground_term T checks that T has no unification variables left; closed_term yields a fresh variable barred from naming any eigenvariable (Binders and HOAS); cmp_term orders two terms structurally, and only works when both are ground.

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

new_int hands out a strictly increasing integer and 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; calc is the same as a function, for use with spilling (Spilling and functional syntax): f {calc (N + 1)}. The precedences of every operator below are in Lexical conventions.

Evaluated inside is / calc:

• binary + - * (int or float), / (float), div mod (int), ^ (string concatenation);

• unary ~ (negation), abs, and, for float, sqrt exp ln sin cos tan arcsin arccos arctan;

• two-argument functions min max, and, for float, pow (pow X Y is X to the power Y) and arctan2 (arctan2 Y X is the angle of the point (X, Y), as atan2 in C);

• conversions int_to_real truncate floor ceil (int ↔ float), int_to_string string_to_int real_to_string string_to_real 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 (Embedding and extending Elpi).

Standard data types

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

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

data quadruple A B C D.
symb quadruple A -> B -> C -> D -> quadruple A B C D.   % + quadruple_1..4

bool uses tt / ff because true / false are goals; pair’s constructor is pr because , is conjunction; cmp is the result of a three-way comparison: cmp_term, or a comparator a caller supplies, as 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 (Terms).

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

code/builtins-tour.elpi:

% A cross-section of the builtin library: arithmetic, standard data types,
% string/term conversion, regular expressions, seeded randomness.

main :-
  X is 2 + 3 * 4, print "calc:" X,
  P = pr 1 "one", term_to_string P S, print "term_to_string:" S,
  rex.split "," "a,b,c" Parts, print "rex.split:" Parts,
  random.init 42, random.int 100 R1,
  random.init 42, random.int 100 R2,      % same seed, same draw
  print "seeded random repeats:" R1 R2.

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

Regular expressions and randomness

rex.match, rex.replace and rex.split (OCaml’s Str syntax, not PCRE) cover the common text-processing needs. random.int N draws a uniform integer in \([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

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

• open_in / open_out / open_append open a file; 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, input_line reads up to the newline, lookahead peeks one byte, eof tests for end of input;

• output OutStream S writes, flush forces pending output out, close_in / close_out close.

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

code/builtins-io.elpi:

% Stream input (without touching the file system) and a typed finite map.

main :-
  open_string "alpha\nbeta\ngamma\n" S,
  input_line S L1,
  input_line S L2,
  close_in S,
  print "first two lines:" L1 L2,

  std.string.map.empty M0,
  std.string.map.add "one" 1 M0 M1,
  std.string.map.add "two" 2 M1 M2,
  std.string.map.find "two" M2 V,
  print "string map, two ->" V.

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

Pretty printing

Output that has to fit a given width, such as code or nested data, is easier to produce by describing its layout than by computing line breaks by hand. Elpi delegates this to OCaml’s Format module: a program builds a term of type std.fmt that describes boxes and break hints, and a builtin hands that term to Format, which decides where lines are split. The document is ordinary data, so it can be built, inspected and discarded on backtracking like any other term; only the final rendering has an effect.

The constructors mirror the calls of Format one to one:

• std.fmt.txt S is a piece of text, never split;

• std.fmt.h L, std.fmt.v I L, std.fmt.hv I L, std.fmt.hov I L and std.fmt.box I L group the documents in the list L in a box, respectively horizontal (breaks never split the line), vertical (every break splits it), horizontal-or-vertical (all breaks split it, or none does), packing (a break splits the line only when the next item does not fit) and structural (like packing, but also splitting when that reduces the indentation). I is the indentation, relative to where the box starts, of the lines a split creates;

• std.fmt.brk N O is a break hint: N spaces when the line is not split, otherwise a newline indented by O more than the box; std.fmt.spc and std.fmt.cut abbreviate std.fmt.brk 1 0 and std.fmt.brk 0 0; std.fmt.nl always splits the line;

• std.fmt.tbox L is a tabulation box, which aligns its content in columns: std.fmt.settab sets a tab stop at the current column, std.fmt.tab moves to the next tab stop, and std.fmt.tbrk N O moves to the next tab stop and then N spaces further, or to a new line shifted by O when no tab stop is left on the line.

std.fmt->string Margin Doc S lays Doc out in the string S, splitting lines longer than Margin columns; std.fmt.output OutStream Margin Doc writes the same layout to a stream. Passing _ as Margin selects the default of 80 columns; a Margin smaller than 2 is rejected.

The constructor names are long when written in full, so a program that builds many documents usually shortens them. The example below lays out the same block at two margins: at the default 80 columns the packing box keeps all the items on one line, at 16 it splits only the breaks it has to.

code/builtins-format.elpi:

% A document built from std.fmt constructors, laid out at two margins.

shorten std.fmt.{ txt, v, hov, brk, cut, spc }.

func items list string -> list std.fmt.
items [] [].
items [X] [txt X] :- !.
items [X|XS] [txt X, txt ";", spc | R] :- items XS R.

func block string, list string -> std.fmt.
block Name Xs (v 2 [txt Name, txt " {", cut, hov 0 {items Xs}, brk 0 -2, txt "}"]).

main :-
  block "record" ["alpha", "beta", "gamma", "delta"] B,
  std.fmt->string _ B Wide,
  print Wide,
  std.fmt->string 16 B Narrow,
  print Narrow.

record {
  alpha; beta; gamma; delta
}
record {
  alpha; beta;
  gamma; delta
}

Tab stops do not adapt to the cells: a column is as wide as the distance between the two tab stops that delimit it, and a cell longer than that pushes the rest of its row past the following tab stops. A table therefore sets its tab stops in a first row padded to the widest cell of each column, typically a header, as in the example below; a std.fmt.tab then starts each cell of the following rows.

code/builtins-format-table.elpi:

% A table: the padded header row sets one tab stop per column.

shorten std.fmt.{ txt, tbox, settab, tab, nl }.

func row pair string (pair string string) -> list std.fmt.
row (pr Name (pr Arity Kind)) [nl, tab, txt Name, tab, txt Arity, tab, txt Kind].

main :-
  Header = [settab, txt "name    ", settab, txt "arity ", settab, txt "kind"],
  std.map [pr "map" (pr "3" "func"), pr "append" (pr "3" "pred")] row Rows,
  std.flatten [Header|Rows] Cells,
  std.fmt->string _ (tbox Cells) S,
  print S.

name    arity kind
map     3     func
append  3     pred

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 std.map and std.set, written in Elpi rather than OCaml, are covered in The standard library.

Garbage collector and runtime

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