elpi-quoted_syntax.elpi

/* elpi: embedded lambda prolog interpreter                                  */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

% HOAS for elpi programs

kind term type.

type app list term -> term.
type lam (term -> term) -> term.
type const string -> term.

type cdata ctype "cdata" -> term. % int, string, float.. see also $is_cdata

type arg (term -> term) -> term.  % only to bind the args of a clause

kind clause type.
type clause (ctype "Loc.t") -> list string -> term -> clause.

% a program is then a list of clause while
% the query is just one item of the same kind.

% see elpi-checker.elpi for an example

% vim: set ft=lprolog: