coq-builtin.elpi

% Coq terms as the object language of elpi and basic API to access Coq
% license: GNU Lesser General Public License Version 2.1 or later
% -------------------------------------------------------------------------

% This file is automatically generated from
%  - coq-HOAS.elpi
%  - coq_elpi_builtin.ml
% and contains the description of the data type of Coq terms and the
% API to access Coq.




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% coq-HOAS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% This section contains the low level data types linking Coq and elpi.
% In particular:
%   - the data type for terms and the evar_map entries (a sequent)
%   - the entry points for commands and tactics (main and solve)

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Entry points
%
% Command and tactic invocation
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Entry point for commands. Eg. "#[att=true] Elpi mycommand foo 3 (f x)." becomes
%   main [str "foo", int 3, trm (app[f,x])]
% in a context where
%   attributes [attribute "att" (leaf "true")]
% holds. The encoding of terms is described below.
% See also the coq.parse-attributes utility.
pred main i:list argument.
pred usage.
pred attributes o:list attribute.

% Entry point for tactics. Eg. "elpi mytactic foo 3 (f x)." becomes
%   solve <goal> <new goals>
% Where [str "foo", int 3, trm (app[f,x])] is part of <goal>.
% The encoding of goals is described below.
% msolve is for tactics that operate on multiple goals (called via all: ).
pred solve i:goal, o:list sealed-goal.
pred msolve i:list sealed-goal, o:list sealed-goal.

% The data type of arguments (for commands or tactics)
kind argument type.
type int       int    -> argument. % Eg. 1 -2.
type str       string -> argument. % Eg. x "y" z.w. or any Coq keyword/symbol
type trm       term   -> argument. % Eg. (t).

% Extra arguments for commands. [Definition], [Axiom], [Record] and [Context]
% take precedence over the [str] argument above (when not "quoted").
%
% Eg. Record or Inductive
type indt-decl indt-decl -> argument.
% Eg. #[universes(polymorphic,...)] Record or Inductive
type upoly-indt-decl indt-decl -> upoly-decl -> argument.
type upoly-indt-decl indt-decl -> upoly-decl-cumul -> argument.
% Eg. Definition or Axiom (when the body is none)
type const-decl id -> option term -> arity -> argument.
% Eg. #[universes(polymorphic,...)] Definition or Axiom
type upoly-const-decl id -> option term -> arity -> upoly-decl -> argument.
% Eg. Context A (b : A).
type ctx-decl context-decl -> argument.

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Coq's terms
%
% Types of term formers
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% -- terms --------------------------------------------------------------------
kind term type.

type sort  sort -> term. % Prop, Type@{i}

% constants: inductive types, inductive constructors, definitions
type global gref -> term.
type pglobal gref -> univ-instance -> term.

% binders: to form functions, arities and local definitions
type fun  name -> term -> (term -> term) -> term.         % fun x : t =>
type prod name -> term -> (term -> term) -> term.         % forall x : t,
type let  name -> term -> term -> (term -> term) -> term. % let x : T := v in

% other term formers: function application, pattern matching and recursion
type app   list term -> term.                   % app [hd|args]
type match term -> term -> list term -> term.   % match t p [branch])
type fix   name -> int -> term -> (term -> term) -> term. % fix name rno ty bo

type primitive primitive-value -> term.

% NYI
%type cofix name -> term -> (term -> term) -> term. % cofix name ty bo

% Notes about (match Scrutinee TypingFunction Branches) when
%   Inductive i A : A -> nat -> Type := K : forall a : A, i A a 0
% and
%   Scrutinee be a term of type (i bool true 7)
%
% - TypingFunction has a very rigid shape that depends on i. Namely
%   as many lambdas as indexes plus one lambda for the inductive itself
%   where the value of the parameters are taken from the type of the scrutinee:
%     fun `a` (indt "bool") a\
%      fun `n` (indt "nat) n\
%       fun `i` (app[indt "i", indt "bool", a n) i\ ..
%   Such spine of fun cannot be omitted; else elpi cannot read the term back.
%   See also coq.bind-ind-arity-no-let in coq-lib.elpi, that builds such spine for you,
%   or the higher level api coq.build-match (same file) that also takes
%   care of breanches.
% - Branches is a list of terms, the order is the canonical one (the order
%   of the constructors as they were declared). If the constructor has arguments
%   (excluding the parameters) then the corresponding term shall be a Coq
%   function. In this case
%      fun `x` (indt "bool") x\ ..

% -- helpers ------------------------------------------------------------------
macro @cast T TY :- (let `cast` TY T x\x).

% -- misc ---------------------------------------------------------------------

% When one writes Constraint Handling Rules unification variables are "frozen",
% i.e. represented by a fresh constant (the evar key) and a list of terms
% (typically the variables in scope).
kind evarkey type.
type uvar  evarkey -> list term -> term.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Coq's evar_map
%
% Context and evar declaration
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% An evar_info (displayed as a Coq goal) is essentially a sequent:
%
% x : t
% y := v : x
% ----------
% p x y
%
% is coded as an Elpi query
%
% pi x1\ decl x1 `x` <t> =>
%  pi x2\ def x2 `y` x1 <v> =>
%   declare-evar
%      [def x2 `y` x1 <v> , decl x1 `x` <t>]
%      (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)
%
% where, by default, declare-evar creates a syntactic constraint as
%
% {x1 x2} :
%   decl x1 `x` <t>, def x2 `y` x1 <v> ?-
%     evar (RawEvar x1 x2) (<p> x1 x2) (Ev x1 x2)  /* suspended on RawEvar, Ev */
%
% When the program is over, a remaining syntactic constraint like the one above
% is read back and transformed into the corresponding evar_info.

pred decl i:term, o:name, o:term. % Var Name Ty
pred def  i:term, o:name, o:term, o:term. % Var Name Ty Bo
pred declare-evar i:list prop, i:term, i:term, i:term. % Ctx RawEvar Ty Evar

:name "default-declare-evar"
declare-evar Ctx RawEv Ty Ev :-
  declare_constraint (declare-evar Ctx RawEv Ty Ev) [RawEv].

% When a goal (evar _ _ _) is turned into a constraint the context is filtered
% to only contain decl, def, pp.  For now no handling rules for this set of
% constraints other than one to remove a constraint

pred rm-evar i:term, i:term.
rm-evar (uvar as X) (uvar as Y):- !, declare_constraint (rm-evar X Y) [X,Y].
rm-evar _ _.

constraint declare-evar evar def decl cache rm-evar {

   % Override the actual context
   rule \ (declare-evar Ctx RawEv Ty Ev) <=> (Ctx => evar RawEv Ty Ev).

   rule \ (rm-evar (uvar X _) (uvar Y _)) (evar (uvar X _) _ (uvar Y _)).

}

% The (evar R Ty E) predicate suspends when R and E are flexible,
% and is solved otherwise.
% The client may want to provide an alternative implementation of
% the clause "default-assign-evar", for example to typechecks that the
% term assigned to E has type Ty, or that the term assigned to R
% elaborates to a term of type Ty that gets assigned to E.
% In tactic mode, elpi/coq-elaborator.elpi wires things up that way.

pred evar i:term, i:term, o:term. % Evar Ty RefinedSolution
evar (uvar as X) T S :- !,
  if (var S _ VL) (prune T VL, prune X VL, declare_constraint (evar X T S) [X, S])
             true. % If S is assigned we consider its a well type term

:name "default-assign-evar"
evar _ _ _. % volatile, only unresolved evars are considered as evars

% To ease the creation of a context with decl and def
% Eg.  @pi-decl `x` <t> x1\ @pi-def `y` <t> <v> y\ ...
macro @pi-decl N T F :- pi x\ decl x N T => F x.
macro @pi-def N T B F :- pi x\ def x N T B => cache x B_ => F x.
macro @pi-parameter ID T F :-
  sigma N\ (coq.id->name ID N, pi x\ decl x N T => F x).
macro @pi-inductive ID A F :-
  sigma N\ (coq.id->name ID N, coq.arity->term A T, pi x\ decl x N T => F x).

% Sometimes it can be useful to pass to Coq a term with unification variables
% representing "untyped holes" like an implicit argument _. In particular
% a unification variable may exit the so called pattern fragment (applied
% to distinct variables) and hence cannot be reliably mapped to Coq as an evar,
% but can still be considered as an implicit argument.
% By loading in the context get-option "HOAS:holes" tt one forces that
% behavior. Here a convenience macro to be put on the LHS of =>
macro @holes! :- get-option "HOAS:holes" tt.

% Similarly, some APIs take a term skeleton in input. In that case unification
% variables are totally disregarded (not even mapped to Coq evars). They are
% interpreted as the {{ lib:elpi.hole }} constant, which represents an implicit
% argument. As a consenque these APIs don't modify the input term at all, but
% rather return a copy. Note that if {{ lib:elpi.hole }} is used directly, then
% it has to be applied to all variables in scope, since Coq erases variables
% that are not used. For example using {{ forall x : nat, lib:elpi.hole }} as
% a term skeleton is equivalent to {{ nat -> lib:elpi.hole }}, while
% {{ forall x : nat, lib:elpi.hole x lib:elpi.hole more args }} puts x in
% the scope of the hole (and passes to is more args).

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Coq's goals and tactic invocation
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% A Coq goal is essentially a sequent, like the evar_info above, but since it
% has to be manipulated as first class Elpi data, it is represented in a slightly
% different way. For example
%
% x : t
% y := v : x
% ----------
% g x y
%
% is represented by the following term of type sealed-goal
%
%  nabla x1\
%   nabla x2\
%    seal
%      (goal
%         [def x2 `y` x1 <v> , decl x1 `x` <t>]
%         (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
%         (Arguments x1 x2))

kind goal type.
kind sealed-goal type.
type nabla (term -> sealed-goal) -> sealed-goal.
type seal goal -> sealed-goal.

typeabbrev goal-ctx (list prop).
type goal goal-ctx -> term -> term -> term -> list argument -> goal.

% A sealed-goal closes with nabla the bound names of a
% 
%  (goal Ctx RawSolution Ty Solution Arguments)
%
% where Ctx is a list of decl or def and Solution is a unification variable
% to be assigned to a term of type Ty in order to make progress.
% RawSolution is used as a trigger: when a term is assigned to it, it is
% elaborated against Ty and the resulting term is assigned to Solution.
%
% Arguments contains data attached to the goal, which lives in its context
% and can be used by tactics to solve the goals.

% A tactic (an elpi predicate which makes progress on a Coq goal) is
% a predicate of type
%   sealed-goal -> list sealed-goal -> prop
% 
% while the main entry point for a tactic written in Elpi is solve
% which has type
%    goal -> list sealed-goal -> prop
%
% The utility (coq.ltac.open T G GL) postulates all the variables bounds
% by nabla and loads the goal context before calling T on the unsealed
% goal. The invocation of a tactic with arguments
%   3 x "y" (h x)
% on the previous goal results in the following Elpi query:
%
% (pi x1\ decl x1 `x` <t> =>
%   pi x2\ def x2 `y` x1 <v> =>
%    declare-evar
%       [def x2 `y` x1 <v> , decl x1 `x` <t>]
%       (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)),
% (coq.ltac.open solve
%  (nabla x1\ nabla x2\ seal
%   (goal
%     [def x2 `y` x1 <v> , decl x1 `x` <t>]
%     (RawEvar x1 x2) (<g> x1 x2) (Evar x1 x2)
%     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]))
%   NewGoals)
%
% If the goal sequent contains other evars, then a tactic invocation is
% an Elpi query made of the conjunction of all the declare-evar queries
% corresponding to these evars and the query corresponding to the goal
% sequent. NewGoals can be assigned to a list of goals that should be
% declared as open. Omitted goals are shelved. If NewGoals is not
% assigned, then all unresolved evars become new goals, but the order
% of such goals is not specified.

% The file elpi-ltac.elpi provides a few combinators (other than coq.ltac.open)
% in the tradition of LCF tacticals. The main difference is that the arguments
% of custom written tactics must not be passed as predicate arguments but rather
% put in the goal they receive. Indeed these arguments can contain terms, and
% their bound variables cannot escape the seal. coq.ltac.set-goal-arguments
% can be used to put an argument from the current goal context into another
% goal. The coq.ltac.call utility can call Ltac1 code (written in Coq) and
% pass arguments via this mechanism.

% Last, since Elpi is alerady a logic programming language with primitive
% support for unification variables, most of the work of a tactic can be
% performed without using tacticals (which work on sealed goals) but rather
% in the context of the original goal. The last step is typically to call
% the refine utility with a term synthesized by the tactic or invoke some
% Ltac1 code on that term (e.g. to call vm_compute, see also the example
% on the reflexive tactic).

% ----- Multi goals tactics. ----
% Coq provides goal selectors, such as all:, to pass to a tactic more than one
% goal. In order to write such a tactic, Coq-Elpi provides another entry point
% called msolve. To be precise, if there are two goals under focus, say <g1> and
% <g2>, then all: elpi tac <t> runs the following query
%
%   msolve [<g1>,<g2>] NewGoals ;                         % note the disjunction
%   coq.ltac.all (coq.ltac.open solve) [<g1>,<g2>] NewGoals
%
% So, if msolve has no clause, Coq-Elpi will use solve on all the goals
% independently. If msolve has a cluse, then it can manipulate the entire list
% of sealed goals. Note that the argument <t> is in both <g1> and <g2> but
% it is interpreted in both contexts independently. If both goals have a proof
% variable named "x" then passing (@eq_refl _ x) as <t> equips both goals with
% a (raw) proof that "x = x", no matter what their type is.

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Declarations for Coq's API (environment read/write access, etc).
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% tt = Yes, ff = No, unspecified = No (unspecified means "_" or a variable).
typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.

%%%%%%% Attributes to be passed to APIs as in @local! => coq.something %%%%%%%%

macro @global!   :- get-option "coq:locality" "global".
macro @local!    :- get-option "coq:locality" "local".

macro @primitive! :- get-option "coq:primitive" tt. % primitive records
macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions
macro @reversible! :- get-option "coq:reversible" tt. % coercions

macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance

% declaration of universe polymorphic constants
% The first list is the one of the unvierse variables being bound
% The first boolean is tt if this list can be extended by Coq (or it has to
% mention all universes actually used)
% The second list if the one with the constaints amond where universes
% The second boolean is tt if this list can be extended by Coq or it has to
% mention all universe constraints actually required to type check the
% declaration)
macro @udecl! Vs LV Cs LC       :- get-option "coq:udecl" (upoly-decl Vs LV Cs LC).
macro @udecl-cumul! Vs LV Cs LC :- get-option "coq:udecl-cumul" (upoly-decl-cumul Vs LV Cs LC).
macro @univpoly!       :- @udecl! [] tt [] tt.
macro @univpoly-cumul! :- @udecl-cumul! [] tt [] tt.

macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
macro @ppall! :- get-option "coq:pp" "all". % printing all
macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses)

macro @keepunivs! :- get-option "coq:keepunivs" tt. % skeletons elaboration
macro @dropunivs! :- get-option "coq:keepunivs" ff. % add-indt/add-const

macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute

macro @inline-at! N :- get-option "coq:inline" (coq.inline.at N). % like Inline(N)
macro @inline! N :- get-option "coq:inline" coq.inline.default. % like

macro @redflags! F :- get-option "coq:redflags" F. % for whd & co

% both arguments are strings eg "8.12.0" "use foo instead"
macro @deprecated! Since Msg :-
  get-option "coq:deprecated" (pr Since Msg).
  

macro @ltacfail! N :- get-option "ltac:fail" N.


% Declaration of inductive types %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

kind indt-decl type.
kind indc-decl type.
kind record-decl type.

% An arity is written, in Coq syntax, as:
%    (x : T1) .. (xn : Tn) : S1 -> ... -> Sn -> U
% This syntax is used, for example, in the type of an inductive type or
% in the type of constructors. We call the abstractions on the left of ":"
% "parameters" while we call the type following the ":" (proper) arity.

% Note: in some contexts, like the type of an inductive type constructor,
% Coq makes no distinction between these two writings
%    (xn : Tn) : forall y1 : S1, ...    and      (xn : Tn) (y1 : S1) : ...
% while Elpi is a bit more restrictive, since it understands user directives
% such as the implicit status of an arguments (eg, using {} instead of () around
% the binder), only on parameters.
% Moreover parameters carry the name given by the user as an "id", while binders
% in terms only carry it as a "name", an irrelevant pretty pringintg hint (see
% also the HOAS of terms). A user command can hence only use the names of
% parameters, and not the names of "forall" quantified variables in the arity.
%
% See also the arity->term predicate in coq-lib.elpi

type parameter id -> implicit_kind -> term -> (term -> arity) -> arity.
type arity term -> arity.

type parameter   id -> implicit_kind -> term -> (term -> indt-decl) -> indt-decl.
type inductive   id -> bool -> arity -> (term -> list indc-decl) -> indt-decl. % tt means inductive, ff coinductive
type record      id -> term -> id -> record-decl -> indt-decl.

type constructor id -> arity -> indc-decl.

type field       field-attributes -> id -> term -> (term -> record-decl) -> record-decl.
type end-record  record-decl.

% Example.
% Remark that A is a regular parameter; y is a non-uniform parameter and t
% also features an index of type bool.
%
%  Inductive t (A : Type) | (y : nat) : bool -> Type :=
%  | K1 (x : A) {n : nat} : S n = y -> t A n true -> t A y true
%  | K2 : t A y false
%
% is written
%
%  (parameter "A" explicit {{ Type }} a\
%     inductive "t" tt (parameter "y" explicit {{ nat }} _\
%                     arity {{ bool -> Type }})
%      t\
%       [ constructor "K1"
%          (parameter "y" explicit {{ nat }} y\
%           (parameter "x" explicit a x\
%            (parameter "n" maximal {{ nat }} n\
%              arity {{ S lp:n = lp:y -> lp:t lp:n true -> lp:t lp:y true }})))
%       , constructor "K2"
%          (parameter "y" explicit {{ nat }} y\
%            arity {{ lp:t lp:y false }}) ])
%
% Remark that the uniform parameters are not passed to occurrences of t, since
% they never change, while non-uniform parameters are both abstracted
% in each constructor type and passed as arguments to t.
%
% The coq.typecheck-indt-decl API can be used to fill in implicit arguments
% an infer universe constraints in the declaration above (e.g. the hidden
% argument of "=" in the arity of K1).
%
% Note: when and inductive type declaration is passed as an argument to an
% Elpi command non uniform parameters must be separated from the uniform ones
% with a | (a syntax introduced in Coq 8.12 and accepted by coq-elpi since
% version 1.4, in Coq this separator is optional, but not in Elpi).

% Context declaration (used as an argument to Elpi commands)
kind context-decl type.
% Eg. (x : T) or (x := B), body is optional, type may be a variable
type context-item  id -> implicit_kind -> term -> option term -> (term -> context-decl) -> context-decl.
type context-end   context-decl.

typeabbrev field-attributes (list field-attribute).

% retrocompatibility macro for Coq v8.10
macro @coercion! :- [coercion reversible].


% Attributes for a record field. Can be left unspecified, see defaults
% below.
kind field-attribute type.
type coercion coercion-status -> field-attribute. % default off
type canonical bool -> field-attribute. % default true, if field is named

% Status of a record field w.r.t. coercions
kind coercion-status type.
type regular coercion-status.
type reversible coercion-status.
type off coercion-status.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% builtins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% This section contains the API to access Coq
% The marker *E* means *experimental*, i.e. use at your own risk, it may change
% substantially or even disappear in future versions.


% -- Misc ---------------------------------------------------------

% [coq.say ...] Prints an info message
external type coq.say variadic any prop.

% [coq.warn ...] Prints a generic warning message
external type coq.warn variadic any prop.

% [coq.warning Category Name ...] 
% Prints a warning message with a Name and Category which can be used
% to silence this warning or turn it into an error. See coqc -w command
% line option
external type coq.warning string -> string -> variadic any prop.

% [coq.error ...] Prints and *aborts* the program. It is a fatal error for
% Elpi and Ltac
external type coq.error variadic any prop.

% [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
% as a string and as 3 numbers
external pred coq.version o:string, o:int, o:int, o:int.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% API for objects belonging to the logic
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% -- Environment: names -----------------------------------------------

% To make the API more precise we use different data types for the names
% of global objects.
% Note: [ctype \"bla\"] is an opaque data type and by convention it is
% written [@bla].

% Global constant name
typeabbrev constant (ctype "constant").


% Inductive type name
typeabbrev inductive (ctype "inductive").


% Inductive constructor name
typeabbrev constructor (ctype "constructor").


% Global objects: inductive types, inductive constructors, definitions
kind gref type.
type const constant -> gref. % Nat.add, List.append, ...
type indt inductive -> gref. % nat, list, ...
type indc constructor -> gref. % O, S, nil, cons, ...

% [id] is a name that matters, we piggy back on Elpi's strings.
% Note: [name] is a name that does not matter.
typeabbrev id string.


% Name of a module /*E*/
typeabbrev modpath (ctype "modpath").


% Name of a module type /*E*/
typeabbrev modtypath (ctype "modtypath").


% -- Environment: read ------------------------------------------------

% Note: The type [term] is defined in coq-HOAS.elpi

% Result of coq.locate-all
kind located type.
type loc-gref gref -> located.
type loc-modpath modpath -> located.
type loc-modtypath modtypath -> located.
type loc-abbreviation abbreviation -> located.

% [coq.locate-all Name Located] finds all possible meanings of a string.
% Does not fail.
external pred coq.locate-all i:id, o:list located.

% [coq.locate Name GlobalReference] locates a global definition, inductive
% type or constructor via its name.
% It unfolds syntactic notations, e.g. "Notation old_name := new_name."
% It undestands qualified names, e.g. "Nat.t".
% It understands Coqlib Registered names using the "lib:" prefix,
% eg "lib:core.bool.true".
% It's a fatal error if Name cannot be located.
external pred coq.locate i:id, o:gref.

% [coq.env.typeof GR Ty] reads the type Ty of a global reference.
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
external pred coq.env.typeof i:gref, o:term.

% [coq.env.global GR T] turns a global reference GR into a term.
% T = (global GR) or, if GR points to a universe polymorphic term,
% T = (pglobal GR I).
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
external pred coq.env.global i:gref, o:term.

external pred coq.env.indt % reads the inductive type declaration for the environment.
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
  i:inductive,        % reference to the inductive type
  o:bool,             % tt if the type is inductive (ff for co-inductive)
  o:int,              % number of parameters
  o:int,              % number of parameters that are uniform (<= parameters)
  o:term,             % type of the inductive type constructor including parameters
  o:list constructor, % list of constructor names
  o:list term.        % list of the types of the constructors (type of KNames) including parameters
  
external pred coq.env.indt-decl % reads the inductive type declaration for the environment.
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
  i:inductive, % reference to the inductive type
  o:indt-decl. % HOAS description of the inductive type
  
% [coq.env.indc->indt K I N] finds the inductive I to which constructor K
% belongs and its position N among the other constructors
external pred coq.env.indc->indt i:constructor, o:inductive, o:int.

% [coq.env.indc GR ParamNo UnifParamNo Kno Ty] reads the type Ty of an
% inductive constructor GR, as well as
% the number of parameters ParamNo and uniform parameters
% UnifParamNo and the number of the constructor Kno (0 based).
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
external pred coq.env.indc i:constructor, o:int, o:int, o:int, o:term.

% [coq.env.informative? Ind] Checks if Ind is informative, that is, if
% it can be eliminated to build a Type. Inductive types in Type
% are
% informative, as well a singleton types in Prop (which are
% regarded as not non-informative).
external pred coq.env.informative? i:inductive.

% [coq.env.record? Ind PrimProjs] checks if Ind is a record (PrimProjs = tt
% if Ind has primitive projections)
external pred coq.env.record? i:inductive, o:bool.

% [coq.env.recursive? Ind] checks if Ind is recursive
external pred coq.env.recursive? i:inductive.

% [coq.env.opaque? GR] checks if GR is an opaque constant
external pred coq.env.opaque? i:constant.

% [coq.env.univpoly? GR PolyArity] checks if GR is universe polymorphic and
% if so returns the number of universe variables
external pred coq.env.univpoly? i:gref, o:int.

% [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant
% GR.
% Opaque constants have Bo = none.
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
external pred coq.env.const i:constant, o:option term, o:term.

% [coq.env.const-body GR Bo] reads the body of a constant, even if it is
% opaque.
% If such body is none, then the constant is a true axiom.
% Supported attributes:
% - @uinstance! I (default: fresh instance I)
external pred coq.env.const-body i:constant, o:option term.

% [coq.env.primitive? GR] tests if GR is a primitive constant (like uin63
% addition) or a primitive type (like uint63)
external pred coq.env.primitive? i:constant.

% [coq.locate-module ModName ModPath] locates a module.  It's a fatal error
% if ModName cannot be located. *E*
external pred coq.locate-module i:id, o:modpath.

% [coq.locate-module-type ModName ModPath] locates a module.  It's a fatal
% error if ModName cannot be located. *E*
external pred coq.locate-module-type i:id, o:modtypath.

% Contents of a module
kind module-item type.
type submodule modpath -> list module-item -> module-item.
type module-type modtypath -> module-item.
type gref gref -> module-item.
type module-functor modpath -> list modtypath -> module-item.
type module-type-functor modtypath -> list modtypath -> module-item.

% [coq.env.module MP Contents] lists the contents of a module (recurses on
% submodules) *E*
external pred coq.env.module i:modpath, o:list module-item.

% [coq.env.module-type MTP Entries] lists the items made visible by module
% type (does not recurse on submodules) *E*
external pred coq.env.module-type i:modtypath, o:list id.

% [coq.env.section GlobalObjects] lists the global objects that are marked
% as to be abstracted at the end of the enclosing sections
external pred coq.env.section o:list constant.

% [coq.env.dependencies GR MP Deps] Computes the direct dependencies of GR.
% If MP is given, Deps only contains grefs from that module
external pred coq.env.dependencies i:gref, i:modpath, o:coq.gref.set.

% [coq.env.transitive-dependencies GR MP Deps] Computes the transitive
% dependencies of GR. If MP is given, Deps only contains grefs from that
% module
external pred coq.env.transitive-dependencies i:gref, i:modpath, 
                                              o:coq.gref.set.

% [coq.env.term-dependencies T S] Computes all the grefs S occurring in the
% term T
external pred coq.env.term-dependencies i:term, o:coq.gref.set.

% [coq.env.current-path Path] lists the current module path
external pred coq.env.current-path o:list string.

% Deprecated, use coq.env.opaque?
  pred coq.env.const-opaque? i:constant.
  coq.env.const-opaque? C :-
    coq.warning "elpi.deprecated" "elpi.const-opaque" "use coq.env.opaque? in place of coq.env.const-opaque?",
    coq.env.opaque? C.
  

% Deprecated, use coq.env.primitive?
  pred coq.env.const-primitive? i:constant.
  coq.env.const-primitive? C :-
    coq.warning "elpi.deprecated" "elpi.const-primitive" "use coq.env.primitive? in place of coq.env.const-primitive?",
    coq.env.primitive? C.
  

% -- Environment: write -----------------------------------------------

% Note: (monomorphic) universe constraints are taken from ELPI's
% constraints store. Use coq.univ-* in order to add constraints (or any
% higher level facility as coq.typecheck). Load in the context attributes
% such as @univpoly!, @univpoly-cumul!, @udecl! or @udecl-cumul! in order to
% declare universe polymorphic constants or inductives.

% [coq.env.add-const Name Bo Ty Opaque C] Declare a new constant: C gets a
% constant derived from Name
% and the current module; Ty can be left unspecified and in that case
% the
% inferred one is taken (as in writing Definition x := t); Bo can be
% left
% unspecified and in that case an axiom is added (or a section variable,
% if a section is open and @local! is used). Omitting the body and the type
% is
% an error. Note: using this API for declaring an axiom or a section
% variable is
% deprecated, use coq.env.add-axiom or coq.env.add-section-variable
% instead.
% Supported attributes:
% - @local! (default: false)
% - @using! (default: section variables actually used)
% - @univpoly! (default unset)
% - @udecl! (default unset)
% - @dropunivs! (default: false, drops all universe constraints from the
% store after the definition)
% 
external pred coq.env.add-const i:id, i:term, i:term, i:opaque?, 
                                o:constant.

% [coq.env.add-axiom Name Ty C] Declare a new axiom: C gets a constant
% derived from Name
% and the current module.
% Supported attributes:
% - @local! (default: false)
% - @univpoly! (default unset)
% - @using! (default: section variables actually used)
% - @inline! (default: no inlining)
% - @inline-at! N (default: no inlining)
external pred coq.env.add-axiom i:id, i:term, o:constant.

% [coq.env.add-section-variable Name Ty C] Declare a new section variable: C
% gets a constant derived from Name
% and the current module
external pred coq.env.add-section-variable i:id, i:term, o:constant.

% [coq.env.add-indt Decl I] Declares an inductive type.
% Supported attributes:
% - @dropunivs! (default: false, drops all universe constraints from the
% store after the definition)
% - @primitive! (default: false, makes records primitive)
external pred coq.env.add-indt i:indt-decl, o:inductive.

% Interactive module construction

% Coq Module inline directive
kind coq.inline type.
type coq.inline.no coq.inline. % Coq's [no inline] (aka !)
type coq.inline.default coq.inline. % The default, can be omitted
type coq.inline.at int -> coq.inline. % Coq's [inline at <num>]

% [coq.env.fresh-global-id ID FID] Generates an id FID which is fresh in
% the current module and looks similar to ID, i.e. it is ID concatenated
% with a number, starting from 1.
% [coq.env.fresh-global-id X X] can be used to check if X is taken
external pred coq.env.fresh-global-id i:id, o:id.

external pred coq.env.begin-module-functor % Starts a functor *E*
  i:id,                       % The name of the functor
  i:option modtypath,         % Its module type
  i:list (pair id modtypath). % Parameters of the functor
  

pred coq.env.begin-module i:id, i:option modtypath.
coq.env.begin-module Name MP :-
  coq.env.begin-module-functor Name MP [].


% [coq.env.end-module ModPath] end the current module that becomes known as
% ModPath *E*
external pred coq.env.end-module o:modpath.

external pred coq.env.begin-module-type-functor % Starts a module type functor *E*
  i:id,                       % The name of the functor
  i:list (pair id modtypath). % The parameters of the functor
  

pred coq.env.begin-module-type i:id.
coq.env.begin-module-type Name :-
  coq.env.begin-module-type-functor Name [].


% [coq.env.end-module-type ModTyPath] end the current module type that
% becomes known as ModPath *E*
external pred coq.env.end-module-type o:modtypath.

external pred coq.env.apply-module-functor % Applies a functor *E*
  i:id,               % The name of the new module
  i:option modtypath, % Its module type
  i:modpath,          % The functor being applied
  i:list modpath,     % Its arguments
  i:coq.inline,       % Arguments inlining
  o:modpath.          % The modpath of the new module
  
external pred coq.env.apply-module-type-functor % Applies a type functor *E*
  i:id,           % The name of the new module type
  i:modtypath,    % The functor
  i:list modpath, % Its arguments
  i:coq.inline,   % Arguments inlining
  o:modtypath.    % The modtypath of the new module type
  
% [coq.env.include-module ModPath Inline] is like the vernacular Include,
% Inline can be omitted *E*
external pred coq.env.include-module i:modpath, i:coq.inline.

% [coq.env.include-module-type ModTyPath Inline] is like the vernacular
% Include Type, Inline can be omitted  *E*
external pred coq.env.include-module-type i:modtypath, i:coq.inline.

% [coq.env.import-module ModPath] is like the vernacular Import *E*
external pred coq.env.import-module i:modpath.

% [coq.env.export-module ModPath] is like the vernacular Export *E*
external pred coq.env.export-module i:modpath.

% Support for sections is limited, in particular sections and
% Coq quotations may interact in surprising ways. For example
%   Section Test.
%   Variable x : nat.
%   Elpi Query lp:{{ coq.say {{ x }} }}.
% works since x is a global Coq term while
%   Elpi Query lp:{{
%     coq.env.begin-section "Test",
%     coq.env.add-const "x" _ {{ nat }} _ @local! GRX,
%     coq.say {{ x }}
%   }}.
% may work in a surprising way or may not work at all since
% x is resolved before the section is started hence it cannot
% denote the same x as before.

% [coq.env.begin-section Name] starts a section named Name *E*
external pred coq.env.begin-section i:id.

% [coq.env.end-section] end the current section *E*
external pred coq.env.end-section .

% [coq.env.projections StructureName Projections] given a record
% StructureName lists all projections
external pred coq.env.projections i:inductive, o:list (option constant).

% [coq.env.primitive-projections StructureName Projections] given a record
% StructureName lists all primitive projections
external pred coq.env.primitive-projections i:inductive, 
                                            o:list (option (pair projection int)).

% -- Sorts (and their universe level, if applicable) ----------------

% Warning: universe polymorphism has to be considered experimental *E* as
% a feature, not just as a set of APIs. Unfortunately some of the
% current complexity is exposed to the programmer, bare with us.
% 
% The big bang is that in Coq one has terms, types and sorts (which are
% the types of types). Some sorts (as of today only Type) some with
% a universe level, on paper Type_i for some i. At the sort level
% Coq features some form of subtyping: a function expecting a function
% to Type, e.g. nat -> Type, can receive a function to Prop, since
% Prop <= Type. So far, so good. But what are these levels i
% exactly?
% 
% Universe levels are said to be "algebraic", they are made of
% variables (see the next section) and the two operators +1 and max.
% This is a sort of internal optimization that leaks to the
% user/programmer. Indeed these universe levels cannot be (directly) used
% in all APIs morally expecting a universe level "i", in particular
% the current constraint engine cannot handle constraint with an
% algebraic level on the right, e.g. i <= j+1. Since some APIs only
% accept universe variables, we provide the coq.univ.variable API
% which is able to craft a universe variable which is roughly
% equivalent to an algebraic universe, e.g. k such that j+1 = k.
% 
% Coq-Elpi systematically purges algebraic universes from terms (and
% types and sorts) when one reads them from the environment. This
% makes the embedding of terms less precise than what it could be.
% The different data types stay, since Coq will eventually become
% able to handle algebraic universes consistently, making this purging
% phase unnecessary.

% universe level (algebraic: max, +1, univ.variable)
typeabbrev univ (ctype "univ").


% Sorts (kinds of types)
kind sort type.
type prop sort. % impredicative sort of propositions
type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
type typ univ ->
         sort. % predicative sort of data (carries a universe level)

% [coq.sort.leq S1 S2] constrains S1 <= S2
external pred coq.sort.leq o:sort, o:sort.

% [coq.sort.eq S1 S2] constrains S1 = S2
external pred coq.sort.eq o:sort, o:sort.

% [coq.sort.sup S1 S2] constrains S2 = S1 + 1
external pred coq.sort.sup o:sort, o:sort.

% [coq.sort.pts-triple S1 S2 S3] constrains S3 = sort of product with domain
% in S1 and codomain in S2
external pred coq.sort.pts-triple o:sort, o:sort, o:sort.

% [coq.univ.print] prints the set of universe constraints
external pred coq.univ.print .

% [coq.univ.new U] A fresh universe.
external pred coq.univ.new o:univ.

% [coq.univ Name U] Finds a named unvierse. Can fail.
external pred coq.univ o:id, o:univ.

% [coq.univ.global? U] succeeds if U is a global universe
external pred coq.univ.global? i:univ.

% [coq.univ.constraints CL] gives the list of constraints, see also
% coq.univ.variable.constraints
external pred coq.univ.constraints o:list univ-constraint.

% -- Universe variables ------

% universe level variable
typeabbrev univ.variable (ctype "univ.variable").


% [coq.univ.variable U L] relates a univ.variable L to a univ U
external pred coq.univ.variable o:univ, o:univ.variable.

% [coq.univ.variable.constraints L CL] gives the list of constraints on L.
% Can be used to craft a strict upoly-decl
external pred coq.univ.variable.constraints i:univ.variable, 
                                            o:list univ-constraint.

% [coq.univ.variable.of-term T S] collects all univ.variables occurring in T
external pred coq.univ.variable.of-term i:term, o:coq.univ.variable.set.

% -- Universe instance (for universe polymorphic global terms) ------

% As of today a universe polymorphic constant can only be instantiated
% with universe level variables. That is f@{Prop} is not valid, nor
% is f@{u+1}. One can only write f@{u} for any u.
% 
% A univ-instance is morally a list of universe level variables,
% but its list syntax is hidden in the terms. If you really need to
% craft or inspect one of these, the following APIs can help you.
% 
% Most of the time the user is expected to use coq.env.global which
% crafts a fresh, appropriate, universe instance and possibly unify that
% term (of the instance it contains) with another one.

% Universes level instance for a universe-polymoprhic constant
typeabbrev univ-instance (ctype "univ-instance").


% [coq.univ-instance UI UL] relates a univ-instance UI and a list of
% universe level variables UL
external pred coq.univ-instance o:univ-instance, o:list univ.variable.

% [coq.univ-instance.unify-eq GR UI1 UI2 Diagnostic] unifies the two
% universe instances for the same gref
external pred coq.univ-instance.unify-eq i:gref, i:univ-instance, 
                                         i:univ-instance, o:diagnostic.

% [coq.univ-instance.unify-leq GR UI1 UI2 Diagnostic] unifies the two
% universe instances for the same gref. Note: if the GR is not *cumulative*
% (see Cumulative or #[universes(cumulative)]) then this API imposes an
% equality constraint.
external pred coq.univ-instance.unify-leq i:gref, i:univ-instance, 
                                          i:univ-instance, o:diagnostic.

% -- Declaration of universe polymorphic global terms -----------

% These are the data types used to declare how constants
% and inductive types should be declared (see also the @udecl!
% and
% @udecl-cumul! macros). Note that only inductive types can be
% declared as cumulative.

% Constraint between two universes level variables
kind univ-constraint type.
type lt univ.variable -> univ.variable -> univ-constraint.
type le univ.variable -> univ.variable -> univ-constraint.
type eq univ.variable -> univ.variable -> univ-constraint.

% Variance of a universe level variable
kind univ-variance type.
type auto univ.variable -> univ-variance.
type covariant univ.variable -> univ-variance.
type invariant univ.variable -> univ-variance.
type irrelevant univ.variable -> univ-variance.

% Constraints for a non-cumulative declaration. Boolean tt means loose
% (e.g. the '+' in f@{u v + | u < v +})
kind upoly-decl type.
type upoly-decl list univ.variable -> bool -> list univ-constraint ->
                bool -> upoly-decl.

% Constraints for a cumulative declaration. Boolean tt means loose (e.g.
% the '+' in f@{u v + | u < v +})
kind upoly-decl-cumul type.
type upoly-decl-cumul list univ-variance -> bool ->
                      list univ-constraint -> bool -> upoly-decl-cumul.

% -- Primitive --------------------------------------------------------

typeabbrev uint63 (ctype "uint63").


typeabbrev float64 (ctype "float64").


typeabbrev projection (ctype "projection").


% Primitive values
kind primitive-value type.
type uint63 uint63 -> primitive-value. % unsigned integers over 63 bits
type float64 float64 ->
             primitive-value. % double precision foalting points
type proj projection -> int -> primitive-value. % primitive projection

% [coq.uint63->int U I] Transforms a primitive unsigned integer U into an
% elpi integer I. Fails if it does not fit.
external pred coq.uint63->int i:uint63, o:int.

% [coq.float64->float F64 F] Transforms a primitive float on 64 bits to an
% elpi one. Currently, it should not fail.
external pred coq.float64->float i:float64, o:float.


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% API for extra logical objects
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% -- Databases (TC, CS, Coercions) ------------------------------------

% Pattern for canonical values
kind cs-pattern type.
type cs-gref gref -> cs-pattern.
type cs-prod cs-pattern.
type cs-default cs-pattern.
type cs-sort sort -> cs-pattern.

% Canonical Structure instances: (cs-instance Proj ValPat Inst)
kind cs-instance type.
type cs-instance gref -> cs-pattern -> gref -> cs-instance.

% [coq.CS.declare-instance GR] Declares GR as a canonical structure
% instance.
% Supported attributes:
% - @local! (default: false)
external pred coq.CS.declare-instance i:gref.

% [coq.CS.db Db] reads all instances
external pred coq.CS.db o:list cs-instance.

% [coq.CS.db-for Proj Value Db] reads all instances for a given Projection
% or canonical Value, or both
external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.

% [coq.TC.declare-class GR] Declare GR as a type class
external pred coq.TC.declare-class i:gref.

% Type class instance with priority
kind tc-instance type.
type tc-instance gref -> int -> tc-instance.

% [coq.TC.declare-instance GR Priority] Declare GR as a Global type class
% instance with Priority.
% Supported attributes:
% - @global! (default: true)
external pred coq.TC.declare-instance i:gref, i:int.

% [coq.TC.db Db] reads all instances
external pred coq.TC.db o:list tc-instance.

% [coq.TC.db-for GR Db] reads all instances of the given class GR
external pred coq.TC.db-for i:gref, o:list tc-instance.

% [coq.TC.class? GR] checks if GR is a class
external pred coq.TC.class? i:gref.

% Node of the coercion graph
kind class type.
type funclass class.
type sortclass class.
type grefclass gref -> class.

% Edge of the coercion graph
kind coercion type.
type coercion gref -> int -> gref -> class ->
              coercion. % ref, nparams, src, tgt

% [coq.coercion.declare C] Declares C = (coercion GR NParams From To) as a
% coercion From >-> To.
% NParams can always be omitted, since it is inferred.
% If From or To is unspecified, then the endpoints are inferred.
% Supported attributes:
% - @global! (default: false)
% - @nonuniform! (default: false)
% - @reversible! (default: false)
external pred coq.coercion.declare i:coercion.

% [coq.coercion.db L] reads all declared coercions
external pred coq.coercion.db o:list coercion.

% [coq.coercion.db-for From To L] L is a path From -> To
external pred coq.coercion.db-for i:class, i:class, 
                                  o:list (pair gref int).

% Deprecated, use coq.env.projections
pred coq.CS.canonical-projections i:inductive, o:list (option constant).
coq.CS.canonical-projections I L :-
  coq.warning "elpi.deprecated" "elpi.canonical-projections" "use coq.env.projections in place of coq.CS.canonical-projections",
  coq.env.projections I L.


% -- Coq's Hint DB -------------------------------------

% Locality of hints is a delicate matter since the Coq default
% is, in some cases, to make an hint active even if the module it belongs
% to is not imported (just merely required, which can happen
% transitively).
% Coq is aiming at changing the default to #[export], that makes an
% hint active only when its enclosing module is imported.
% See:
% https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140
% 
% This old behavior is available via the @global! flag, but is discouraged.
% 

% Hint Mode
kind hint-mode type.
type mode-ground hint-mode. % No Evar
type mode-input hint-mode. % No Head Evar
type mode-output hint-mode. % Anything

% [coq.hints.add-mode GR DB Mode] Adds a mode declaration to DB about
% GR.
% Supported attributes:
% - @local! (default is export)
% - @global! (discouraged, may become deprecated)
external pred coq.hints.add-mode i:gref, i:string, i:list hint-mode.

% [coq.hints.modes GR DB Modes] Gets all the mode declarations in DB about
% GR
external pred coq.hints.modes i:gref, i:string, o:list (list hint-mode).

% [coq.hints.set-opaque C DB Opaque] Like Hint Opaque C : DB (or Hint
% Transparent, if the boolean is ff).
% Supported attributes:
% - @local! (default is export)
% - @global! (discouraged, may become deprecated)
external pred coq.hints.set-opaque i:constant, i:string, i:bool.

% [coq.hints.opaque C DB Opaque] Reads if constant C is opaque (tt) or
% transparent (ff) in DB
external pred coq.hints.opaque i:constant, i:string, o:bool.

% [coq.hints.add-resolve GR DB Priority Pattern] Like Hint Resolve GR |
% Priority Pattern : DB.
% Supported attributes:
% - @local! (default is export)
% - @global! (discouraged, may become deprecated)
external pred coq.hints.add-resolve i:gref, i:string, i:int, i:term.

% -- Coq's notational mechanisms -------------------------------------

% Implicit status of an argument
kind implicit_kind type.
type implicit implicit_kind. % regular implicit argument, eg Arguments foo [x]
type maximal implicit_kind. % maximally inserted implicit argument, eg Arguments foo {x}
type explicit implicit_kind. % explicit argument, eg Arguments foo x

% [coq.arguments.implicit GR Imps] reads the implicit arguments declarations
% associated to a global reference. See also the [] and {} flags for the
% Arguments command.
external pred coq.arguments.implicit i:gref, o:list (list implicit_kind).

% [coq.arguments.set-implicit GR Imps] sets the implicit arguments
% declarations associated to a global reference.
% Unspecified means explicit.
% See also the [] and {} flags for the Arguments command.
% Supported attributes:
% - @global! (default: false)
external pred coq.arguments.set-implicit i:gref, 
                                         i:list (list implicit_kind).

% [coq.arguments.set-default-implicit GR] sets the default implicit
% arguments declarations associated to a global reference.
% See also the "default implicits" flag to the Arguments command.
% Supported attributes:
% - @global! (default: false)
external pred coq.arguments.set-default-implicit i:gref.

% [coq.arguments.name GR Names] reads the Names of the arguments of a global
% reference. See also the (f (A := v)) syntax.
external pred coq.arguments.name i:gref, o:list (option id).

% [coq.arguments.set-name GR Names] sets the Names of the arguments of a
% global reference.
% See also the :rename flag to the Arguments command.
% Supported attributes:
% - @global! (default: false)
external pred coq.arguments.set-name i:gref, i:list (option id).

% [coq.arguments.scope GR Scopes] reads the notation scope of the arguments
% of a global reference. See also the %scope modifier for the Arguments
% command
external pred coq.arguments.scope i:gref, o:list (option id).

% [coq.arguments.set-scope GR Scopes] sets the notation scope of the
% arguments of a global reference.
% Scope can be a scope name or its delimiter.
% See also the %scope modifier for the Arguments command.
% Supported attributes:
% - @global! (default: false)
external pred coq.arguments.set-scope i:gref, i:list (option id).

% Strategy for simplification tactics
kind simplification_strategy type.
type never simplification_strategy. % Arguments foo : simpl never
type when list int -> option int ->
          simplification_strategy. % Arguments foo .. / .. ! ..
type when-nomatch list int -> option int ->
                  simplification_strategy. % Arguments foo .. / .. ! .. : simpl nomatch

% [coq.arguments.simplification GR Strategy] reads the behavior of the
% simplification tactics. Positions are 0 based. See also the ! and /
% modifiers for the Arguments command
external pred coq.arguments.simplification i:gref, 
                                           o:option simplification_strategy.

% [coq.arguments.set-simplification GR Strategy] sets the behavior of the
% simplification tactics.
% Positions are 0 based.
% See also the ! and / modifiers for the Arguments command.
% Supported attributes:
% - @global! (default: false)
external pred coq.arguments.set-simplification i:gref, 
                                               i:simplification_strategy.

% [coq.locate-abbreviation Name Abbreviation] locates an abbreviation.  It's
% a fatal error if Name cannot be located.
external pred coq.locate-abbreviation i:id, o:abbreviation.

% Name of an abbreviation
typeabbrev abbreviation (ctype "abbreviation").


% [coq.notation.add-abbreviation Name Nargs Body OnlyParsing Abbreviation]
% Declares an abbreviation Name with Nargs arguments.
% The term must begin with at least Nargs "fun" nodes whose domain is
% ignored, eg (fun _ _ x\ fun _ _ y\ app[global "add",x,y]).
% Supported attributes:
% - @deprecated! (default: not deprecated)
% - @global! (default: false)
external pred coq.notation.add-abbreviation i:id, i:int, i:term, i:bool, 
                                            o:abbreviation.

% [coq.notation.abbreviation Abbreviation Args Body] Unfolds an abbreviation
external pred coq.notation.abbreviation i:abbreviation, i:list term, 
                                        o:term.

% [coq.notation.abbreviation-body Abbreviation Nargs Body] Retrieves the
% body of an abbreviation
external pred coq.notation.abbreviation-body i:abbreviation, o:int, 
                                             o:term.

% [coq.notation.add-abbreviation-for-tactic Name TacticName FixedArgs]
% Declares a parsing rule similar to
%   Notation Name X1..Xn := ltac:(elpi TacticName FixedArgs (X1)..(Xn))
% so that Name can be used in the middle of a term to invoke an
% elpi tactic. While FixedArgs can contain str, int, and trm all
% other arguments will necessarily be terms, and their number is
% not fixed (the user can pass as many as he likes).
% The tactic receives as the elpi.loc attribute the precise location
% at which the term is written (unlike if a regular abbreviation was
% declared by hand).
% A call to coq.notation.add-abbreviation-for-tactic TacName TacName []
% is equivalent to Elpi Export TacName.
external pred coq.notation.add-abbreviation-for-tactic i:string, 
                                                       i:string, 
                                                       i:list argument.

% Generic attribute value
kind attribute-value type.
type leaf-str string -> attribute-value.
type leaf-loc loc -> attribute-value.
type node list attribute -> attribute-value.

% Generic attribute
kind attribute type.
type attribute string -> attribute-value -> attribute.

% -- Coq's pretyper ---------------------------------------------------

% [coq.sigma.print] Prints Coq's Evarmap and the mapping to/from Elpi's
% unification variables
external pred coq.sigma.print .

% [coq.typecheck T Ty Diagnostic] typchecks a term T returning its type Ty.
% If Ty is provided, then
% the inferred type is unified (see unify-leq) with it.
% Universe constraints are put in the constraint store.
external pred coq.typecheck i:term, o:term, o:diagnostic.

% [coq.typecheck-ty Ty U Diagnostic] typchecks a type Ty returning its
% universe U. If U is provided, then
% the inferred universe is unified (see unify-leq) with it.
% Universe constraints are put in the constraint store.
external pred coq.typecheck-ty i:term, o:sort, o:diagnostic.

% [coq.unify-eq A B Diagnostic] unifies the two terms
external pred coq.unify-eq i:term, i:term, o:diagnostic.

% [coq.unify-leq A B Diagnostic] unifies the two terms (with cumulativity,
% if they are types)
external pred coq.unify-leq i:term, i:term, o:diagnostic.

% [coq.elaborate-skeleton T ETy E Diagnostic] elabotares T against the
% expected type ETy.
% T is allowed to contain holes (unification variables) but these are
% not assigned even if the elaborated term has a term in place of the
% hole. Similarly universe levels present in T are disregarded.
% Supported attributes:
% - @keepunivs! (default false, do not disregard universe levels) 
external pred coq.elaborate-skeleton i:term, o:term, o:term, o:diagnostic.

% [coq.elaborate-ty-skeleton T U E Diagnostic] elabotares T expecting it to
% be a type of sort U.
% T is allowed to contain holes (unification variables) but these are
% not assigned even if the elaborated term has a term in place of the
% hole. Similarly universe levels present in T are disregarded.
% Supported attributes:
% - @keepunivs! (default false, do not disregard universe levels) 
external pred coq.elaborate-ty-skeleton i:term, o:sort, o:term, 
                                        o:diagnostic.

% -- Coq's reduction flags    ------------------------------------

% Flags for lazy, cbv, ... reductions
kind coq.redflag type.
type coq.redflags.beta coq.redflag.
type coq.redflags.delta coq.redflag. % if set then coq.redflags.const disables unfolding
type coq.redflags.match coq.redflag.
type coq.redflags.fix coq.redflag.
type coq.redflags.cofix coq.redflag.
type coq.redflags.zeta coq.redflag.
type coq.redflags.const constant ->
                        coq.redflag. % enable/disable unfolding

% Set of flags for lazy, cbv, ... reductions
typeabbrev coq.redflags (ctype "coq.redflags").

type coq.redflags.all coq.redflags.
type coq.redflags.allnolet coq.redflags.
type coq.redflags.beta coq.redflags.
type coq.redflags.betadeltazeta coq.redflags.
type coq.redflags.betaiota coq.redflags.
type coq.redflags.betaiotazeta coq.redflags.
type coq.redflags.betazeta coq.redflags.
type coq.redflags.delta coq.redflags.
type coq.redflags.zeta coq.redflags.
type coq.redflags.nored coq.redflags.

% [coq.redflags.add Flags Options NewFlags] Updates reduction Flags by
% adding Options
external pred coq.redflags.add i:coq.redflags, i:list coq.redflag, 
                               o:coq.redflags.

% [coq.redflags.sub Flags Options NewFlags] Updates reduction Flags by
% removing Options
external pred coq.redflags.sub i:coq.redflags, i:list coq.redflag, 
                               o:coq.redflags.

% -- Coq's reduction machines ------------------------------------

% [coq.reduction.lazy.whd T Tred] Puts T in weak head normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
external pred coq.reduction.lazy.whd i:term, o:term.

% [coq.reduction.lazy.norm T Tred] Puts T in normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
external pred coq.reduction.lazy.norm i:term, o:term.

% [coq.reduction.lazy.bi-norm T Tred] Puts T in normal form only reducing
% beta and iota redexes
external pred coq.reduction.lazy.bi-norm i:term, o:term.

% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
external pred coq.reduction.cbv.norm i:term, o:term.

% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form. Its type Ty can
% be omitted (but is recomputed)
external pred coq.reduction.vm.norm i:term, i:term, o:term.

% [coq.reduction.native.norm T Ty Tred] Puts T in normal form. Its type Ty
% can be omitted (but is recomputed). Falls back to vm.norm if native
% compilation is not available.
external pred coq.reduction.native.norm i:term, i:term, o:term.

% [coq.reduction.native.available?] Is native compilation available on this
% system/configuration?
external pred coq.reduction.native.available? .

% Deprecated, use coq.reduction.cbv.norm
pred coq.reduction.cbv.whd_all i:term, o:term.
coq.reduction.cbv.whd_all T R :-
  coq.warning "elpi.deprecated" "elpi.cbv-whd-all" "use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all",
  coq.reduction.cbv.norm T R.


% Deprecated, use coq.reduction.vm.norm
pred coq.reduction.vm.whd_all i:term, i:term, o:term.
coq.reduction.vm.whd_all T TY R :-
  coq.warning "elpi.deprecated" "elpi.vm-whd-all" "use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all",
  coq.reduction.vm.norm T TY R.



pred coq.reduction.lazy.whd_all i:term, o:term.
coq.reduction.lazy.whd_all X Y :-
  @redflags! coq.redflags.all => coq.reduction.lazy.whd X Y.


% -- Coq's conversion strategy tweaks --------------------------

% Strategy for conversion test
% expand < ... < level -1 < level 0 < level 1 < ... < opaque
kind conversion_strategy type.
type opaque conversion_strategy.
type expand conversion_strategy.
type level int -> conversion_strategy. % default is 0, aka transparent

% [coq.strategy.set CL Level] Sets the unfolding priority for all the
% constants in the list CL. See the command Strategy.
external pred coq.strategy.set i:list constant, i:conversion_strategy.

% [coq.strategy.get C Level] Gets the unfolding priority for C
external pred coq.strategy.get i:constant, o:conversion_strategy.

% -- Coq's tactics --------------------------------------------

% [coq.ltac.fail Level ...] Interrupts the Elpi program and calls Ltac's
% fail Level Msg, where Msg is the printing of the remaining arguments.
% Level can be left unspecified and defaults to 0
external type coq.ltac.fail int -> variadic any prop.

% [coq.ltac.collect-goals T Goals ShelvedGoals] 
% Turns the holes in T into Goals.
% Goals are closed with nablas.
% ShelvedGoals are goals which can be solved by side effect (they occur
% in the type of the other goals).
% The order of Goals is given by the traversal order of EConstr.fold
% (a
% fold_left over the terms, letin body comes before the type).
% 
external pred coq.ltac.collect-goals i:term, o:list sealed-goal, 
                                     o:list sealed-goal.

% [coq.ltac.call-ltac1 Tac G GL] Calls Ltac1 tactic named Tac on goal G
% (passing the arguments of G, see coq.ltac.call for a handy wrapper)
external pred coq.ltac.call-ltac1 i:string, i:goal, o:list sealed-goal.

% [coq.ltac.id-free? ID G] 
%     Fails if ID is already used in G. Note that ids which are taken are
% renamed
%     on the fly (since in the HOAS of terms, names are just pretty printing
%     hints), but for the ergonomy of a tactic it may help to know if an
%     hypothesis name is already taken.
% 
external pred coq.ltac.id-free? i:id, i:goal.

% -- Coq's options system --------------------------------------------

% Coq option value
kind coq.option type.
type coq.option.int option int -> coq.option. % none means unset
type coq.option.string option string -> coq.option. % none means unset
type coq.option.bool bool -> coq.option.

% [coq.option.get Option Value] reads Option. Reading a non existing option
% is a fatal error.
external pred coq.option.get i:list string, o:coq.option.

% [coq.option.set Option Value] writes Option. Writing a non existing option
% is a fatal error.
external pred coq.option.set i:list string, i:coq.option.

% [coq.option.available? Option Deprecated] checks if Option exists and
% tells if is deprecated (tt) or not (ff)
external pred coq.option.available? i:list string, o:bool.

% [coq.option.add Option Value Deprecated] 
% adds a new option to Coq setting its current value (and type).
% Deprecated can be left unspecified and defaults to ff.
% This call cannot be undone in a Coq interactive session, use it once
% and for all in a .v file which your clients will load. Eg.
% 
%   Elpi Query lp:{{ coq.option.add ... }}.
%   
% 
external pred coq.option.add i:list string, i:coq.option, i:bool.

% -- Datatypes conversions --------------------------------------------

% Name.Name.t: Name hints (in binders), can be input writing a name
% between backticks, e.g. `x` or `_` for anonymous. Important: these are
% just printing hints with no meaning, hence in elpi two name are always
% related: `x` = `y`
typeabbrev name (ctype "name").


% [coq.name-suffix Name Suffix NameSuffix] suffixes a Name with a string or
% an int or another name
external pred coq.name-suffix i:name, i:any, o:name.

% [coq.string->name Hint Name] creates a name hint
external pred coq.string->name i:string, o:name.


pred coq.id->name i:id, o:name.
coq.id->name S N :- coq.string->name S N.
  

% [coq.name->id Name Id] tuns a pretty printing hint into a string. This API
% is for internal use, no guarantee on its behavior.
external pred coq.name->id i:name, o:id.

% [coq.gref->id GR Id] extracts the label (last component of a full kernel
% name)
external pred coq.gref->id i:gref, o:id.

% [coq.gref->string GR FullPath] extract the full kernel name
external pred coq.gref->string i:gref, o:string.

% [coq.gref->path GR FullPath] extract the full path (kernel name without
% final id), each component is a separate list item
external pred coq.gref->path i:gref, o:list string.

% [coq.modpath->path MP FullPath] extract the full kernel name, each
% component is a separate list item
external pred coq.modpath->path i:modpath, o:list string.

% [coq.modtypath->path MTP FullPath] extract the full kernel name, each
% component is a separate list item
external pred coq.modtypath->path i:modtypath, o:list string.

% [coq.term->string T S] prints a term T to a string S using Coq's pretty
% printer
% Supported attributes:
% - @ppwidth! N (default 80, max line length)
% - @ppall! (default: false, prints all details)
% - @ppmost! (default: false, prints most details)
% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
% off)
% - @holes! (default: false, prints evars as _)
external pred coq.term->string i:term, o:string.

% [coq.term->pp T B] prints a term T to a pp.t B using Coq's pretty
% printer"
% Supported attributes:
% - @ppall! (default: false, prints all details)
% - @ppmost! (default: false, prints most details)
% - @pplevel! (default: _, prints parentheses to reach that level, 200 =
% off)
% - @holes! (default: false, prints evars as _)
external pred coq.term->pp i:term, o:coq.pp.

% -- Access to Elpi's data --------------------------------------------

% clauses
% 
% A clause like
%  :name "foo" :before "bar" foo X Y :- bar X Z, baz Z Y
% is represented as
%  clause _ "foo" (before "bar") (pi x y z\ foo x y :- bar x z, baz z y)
% that is exactly what one would load in the context using =>.
% 
% The name and the grafting specification can be left unspecified.
kind clause type.
type clause id -> grafting -> prop -> clause.

% Specify if the clause has to be grafted before or after a named clause
kind grafting type.
type before id -> grafting.
type after id -> grafting.

% Specify to which module the clause should be attached to
kind scope type.
type execution-site scope. % The module inside which the Elpi program is run
type current scope. % The module being defined (see begin/end-module)
type library scope. % The outermost module (carrying the file name)

% [coq.elpi.accumulate Scope DbName Clause] 
% Declare that, once the program is over, the given clause has to be
% added to the given db (see Elpi Db).
% Clauses usually belong to Coq modules: the Scope argument lets one
% select which module:
% - execution site (default) is the module in which the pogram is
%   invoked
% - current is the module currently being constructed (see
%   begin/end-module)
% - library is the current file (the module that is named after the file)
% The clauses are visible as soon as the enclosing module is Imported.
% A clause that mentions a section variable is automatically discarded
% at the end of the section.
% Clauses cannot be accumulated inside functors.
% Supported attributes:
% - @local! (default: false, discard at the end of section or module)
external pred coq.elpi.accumulate i:scope, i:id, i:clause.

% -- Utils ------------------------------------------------------------

kind coq.gref.set type.

% [coq.gref.set.empty A] The empty set
external pred coq.gref.set.empty o:coq.gref.set.

% [coq.gref.set.mem Elem A] Checks if Elem is in a
external pred coq.gref.set.mem i:gref, i:coq.gref.set.

% [coq.gref.set.add Elem A B] B is A union {Elem}
external pred coq.gref.set.add i:gref, i:coq.gref.set, o:coq.gref.set.

% [coq.gref.set.remove Elem A B] B is A \ {Elem}
external pred coq.gref.set.remove i:gref, i:coq.gref.set, o:coq.gref.set.

% [coq.gref.set.union A B X] X is A union B
external pred coq.gref.set.union i:coq.gref.set, i:coq.gref.set, 
                                 o:coq.gref.set.

% [coq.gref.set.inter A B X] X is A intersection B
external pred coq.gref.set.inter i:coq.gref.set, i:coq.gref.set, 
                                 o:coq.gref.set.

% [coq.gref.set.diff A B X] X is A \ B
external pred coq.gref.set.diff i:coq.gref.set, i:coq.gref.set, 
                                o:coq.gref.set.

% [coq.gref.set.equal A B] tests A and B for equality
external pred coq.gref.set.equal i:coq.gref.set, i:coq.gref.set.

% [coq.gref.set.subset A B] tests if A is a subset of B
external pred coq.gref.set.subset i:coq.gref.set, i:coq.gref.set.

% [coq.gref.set.elements M L] L is M transformed into list
external pred coq.gref.set.elements i:coq.gref.set, o:list gref.

% [coq.gref.set.cardinal M N] N is the number of elements of M
external pred coq.gref.set.cardinal i:coq.gref.set, o:int.

% CAVEAT: the type parameter of coq.gref.map must be a closed term

kind coq.gref.map type -> type.

% [coq.gref.map.empty M] The empty map
external pred coq.gref.map.empty o:coq.gref.map A.

% [coq.gref.map.mem S M] Checks if S is bound in M
external pred coq.gref.map.mem i:gref, i:coq.gref.map A.

% [coq.gref.map.add S V M M1] M1 is M where V is bound to S
external pred coq.gref.map.add i:gref, i:A, i:coq.gref.map A, 
                               o:coq.gref.map A.

% [coq.gref.map.remove S M M1] M1 is M where S is unbound
external pred coq.gref.map.remove i:gref, i:coq.gref.map A, 
                                  o:coq.gref.map A.

% [coq.gref.map.find S M V] V is the binding of S in M
external pred coq.gref.map.find i:gref, i:coq.gref.map A, o:A.

% [coq.gref.map.bindings M L] L is M transformed into an associative list
external pred coq.gref.map.bindings i:coq.gref.map A, 
                                    o:list (pair gref A).

kind coq.univ.set type.

% [coq.univ.set.empty A] The empty set
external pred coq.univ.set.empty o:coq.univ.set.

% [coq.univ.set.mem Elem A] Checks if Elem is in a
external pred coq.univ.set.mem i:univ, i:coq.univ.set.

% [coq.univ.set.add Elem A B] B is A union {Elem}
external pred coq.univ.set.add i:univ, i:coq.univ.set, o:coq.univ.set.

% [coq.univ.set.remove Elem A B] B is A \ {Elem}
external pred coq.univ.set.remove i:univ, i:coq.univ.set, o:coq.univ.set.

% [coq.univ.set.union A B X] X is A union B
external pred coq.univ.set.union i:coq.univ.set, i:coq.univ.set, 
                                 o:coq.univ.set.

% [coq.univ.set.inter A B X] X is A intersection B
external pred coq.univ.set.inter i:coq.univ.set, i:coq.univ.set, 
                                 o:coq.univ.set.

% [coq.univ.set.diff A B X] X is A \ B
external pred coq.univ.set.diff i:coq.univ.set, i:coq.univ.set, 
                                o:coq.univ.set.

% [coq.univ.set.equal A B] tests A and B for equality
external pred coq.univ.set.equal i:coq.univ.set, i:coq.univ.set.

% [coq.univ.set.subset A B] tests if A is a subset of B
external pred coq.univ.set.subset i:coq.univ.set, i:coq.univ.set.

% [coq.univ.set.elements M L] L is M transformed into list
external pred coq.univ.set.elements i:coq.univ.set, o:list univ.

% [coq.univ.set.cardinal M N] N is the number of elements of M
external pred coq.univ.set.cardinal i:coq.univ.set, o:int.

% CAVEAT: the type parameter of coq.univ.map must be a closed term

kind coq.univ.map type -> type.

% [coq.univ.map.empty M] The empty map
external pred coq.univ.map.empty o:coq.univ.map A.

% [coq.univ.map.mem S M] Checks if S is bound in M
external pred coq.univ.map.mem i:univ, i:coq.univ.map A.

% [coq.univ.map.add S V M M1] M1 is M where V is bound to S
external pred coq.univ.map.add i:univ, i:A, i:coq.univ.map A, 
                               o:coq.univ.map A.

% [coq.univ.map.remove S M M1] M1 is M where S is unbound
external pred coq.univ.map.remove i:univ, i:coq.univ.map A, 
                                  o:coq.univ.map A.

% [coq.univ.map.find S M V] V is the binding of S in M
external pred coq.univ.map.find i:univ, i:coq.univ.map A, o:A.

% [coq.univ.map.bindings M L] L is M transformed into an associative list
external pred coq.univ.map.bindings i:coq.univ.map A, 
                                    o:list (pair univ A).

kind coq.univ.variable.set type.

% [coq.univ.variable.set.empty A] The empty set
external pred coq.univ.variable.set.empty o:coq.univ.variable.set.

% [coq.univ.variable.set.mem Elem A] Checks if Elem is in a
external pred coq.univ.variable.set.mem i:univ.variable, 
                                        i:coq.univ.variable.set.

% [coq.univ.variable.set.add Elem A B] B is A union {Elem}
external pred coq.univ.variable.set.add i:univ.variable, 
                                        i:coq.univ.variable.set, 
                                        o:coq.univ.variable.set.

% [coq.univ.variable.set.remove Elem A B] B is A \ {Elem}
external pred coq.univ.variable.set.remove i:univ.variable, 
                                           i:coq.univ.variable.set, 
                                           o:coq.univ.variable.set.

% [coq.univ.variable.set.union A B X] X is A union B
external pred coq.univ.variable.set.union i:coq.univ.variable.set, 
                                          i:coq.univ.variable.set, 
                                          o:coq.univ.variable.set.

% [coq.univ.variable.set.inter A B X] X is A intersection B
external pred coq.univ.variable.set.inter i:coq.univ.variable.set, 
                                          i:coq.univ.variable.set, 
                                          o:coq.univ.variable.set.

% [coq.univ.variable.set.diff A B X] X is A \ B
external pred coq.univ.variable.set.diff i:coq.univ.variable.set, 
                                         i:coq.univ.variable.set, 
                                         o:coq.univ.variable.set.

% [coq.univ.variable.set.equal A B] tests A and B for equality
external pred coq.univ.variable.set.equal i:coq.univ.variable.set, 
                                          i:coq.univ.variable.set.

% [coq.univ.variable.set.subset A B] tests if A is a subset of B
external pred coq.univ.variable.set.subset i:coq.univ.variable.set, 
                                           i:coq.univ.variable.set.

% [coq.univ.variable.set.elements M L] L is M transformed into list
external pred coq.univ.variable.set.elements i:coq.univ.variable.set, 
                                             o:list univ.variable.

% [coq.univ.variable.set.cardinal M N] N is the number of elements of M
external pred coq.univ.variable.set.cardinal i:coq.univ.variable.set, 
                                             o:int.

% CAVEAT: the type parameter of coq.univ.variable.map must be a closed
% term

kind coq.univ.variable.map type -> type.

% [coq.univ.variable.map.empty M] The empty map
external pred coq.univ.variable.map.empty o:coq.univ.variable.map A.

% [coq.univ.variable.map.mem S M] Checks if S is bound in M
external pred coq.univ.variable.map.mem i:univ.variable, 
                                        i:coq.univ.variable.map A.

% [coq.univ.variable.map.add S V M M1] M1 is M where V is bound to S
external pred coq.univ.variable.map.add i:univ.variable, i:A, 
                                        i:coq.univ.variable.map A, 
                                        o:coq.univ.variable.map A.

% [coq.univ.variable.map.remove S M M1] M1 is M where S is unbound
external pred coq.univ.variable.map.remove i:univ.variable, 
                                           i:coq.univ.variable.map A, 
                                           o:coq.univ.variable.map A.

% [coq.univ.variable.map.find S M V] V is the binding of S in M
external pred coq.univ.variable.map.find i:univ.variable, 
                                         i:coq.univ.variable.map A, o:A.

% [coq.univ.variable.map.bindings M L] L is M transformed into an
% associative list
external pred coq.univ.variable.map.bindings i:coq.univ.variable.map A, 
                                             o:list (pair univ.variable A).

% Coq box types for pretty printing:
% - Vertical block: each break leads to a new line
% - Horizontal block: no line breaking
% - Horizontal-vertical block: same as Vertical block, except if this block
%   is small enough to fit on a single line in which case it is the same
%   as a Horizontal block
% - Horizontal or Vertical block: breaks lead to new line only when
%   necessary to print the content of the block (the contents flow
%   inside the box)
kind coq.pp.box type.
type coq.pp.v int -> coq.pp.box.
type coq.pp.h coq.pp.box.
type coq.pp.hv int -> coq.pp.box.
type coq.pp.hov int -> coq.pp.box.

% Coq box model for pretty printing. Items:
% - empty
% - spc: a spacem, also a breaking hint
% - str: a non breakable string
% - brk L I: a breaking hint of a given length L contributing I spaces to
%   indentation when taken
% - glue: puts things together
% - box B: a box with automatic line breaking according to B
% - comment: embedded \\n are turned into nl (see below)
% - tag: ignored
% - nl: break the line (should not be used)
kind coq.pp type.
type coq.pp.empty coq.pp.
type coq.pp.spc coq.pp.
type coq.pp.str string -> coq.pp.
type coq.pp.brk int -> int -> coq.pp.
type coq.pp.glue list coq.pp -> coq.pp.
type coq.pp.box coq.pp.box -> list coq.pp -> coq.pp.
type coq.pp.comment list string -> coq.pp.
type coq.pp.tag string -> coq.pp -> coq.pp.
type coq.pp.nl coq.pp.

% [coq.pp->string B S] Prints a pp.t box expression B to a string S
% Supported attributes:
% - @ppwidth! N (default 80, max line length)
external pred coq.pp->string i:coq.pp, o:string.