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 descritpion 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 (coq_elpi_vernacular.ml)
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% 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.
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 [str "foo", int 3, trm (app[f,x])] <goals> <new goals>
% The encoding of goals is described below.
pred solve i:list argument, i:list goal, o:list goal.
% Note: currently the goal list is always of length 1.

% 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 m A : T := K { f : t; .. }.
type indt-decl indt-decl -> argument.
% Eg. Definition m A : T := B. (or Axiom when the body is none)
type const-decl id -> option term -> arity -> argument.
% Eg. Context A (b : A).
type ctx-decl context-decl -> argument.

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Coq's terms
%
% Types of term formers (coq_elpi_HOAS.ml)
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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

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

% constants: inductive types, inductive constructors, definitions
type global gref -> 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

kind primitive-value type.
type uint63 uint63 -> primitive-value.
type float64 float64 -> primitive-value.
type primitive primitive-value -> term.


% NYI
%type cofix name -> term -> (term -> term) -> term. % cofix name ty bo
%type proj  @gref -> term -> term. % applied primitive projection

% 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 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 (coq_elpi_goal_HOAS.ml)
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% An evar_info
%
% x : t
% y := v : x
% ----------
% p x y
%
% is coded as an elpi goal
%
% pi x1\ decl x1 `x` <t> =>
%  pi x2\ def x2 `y` x1 <v> =>
%   declare-evar
%      [decl x1 `x` <t>, def x2 `y` x1 <v>] (Ev x1 x2) (<p> x1 x2)
%
% where, by default, declare-evar creates a syntactic constraint as
%
% {x1 x2} : decl x1 `x` <t>, def x2 `y` x1 <v> ?- evar (Ev x1 x2) (<p> x1 x2)
%
% When the program is over, a remaining syntactic constraint like the one above
% is read back and transformed into the corresponding evar_info.
%
% The client may want to provide an alternative implementation of
% declare-evar that, for example, typechecks the term assigned to Ev
% (engine/elaborator.elpi does it).

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.
rm-evar (uvar as X) :- !, declare_constraint (rm-evar X) [X].
rm-evar _.

constraint declare-evar evar def decl cache evar->goal rawevar->evar rm-evar {

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

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

}

pred evar i:term, i:term, o:term. % Evar Ty RefinedSolution
evar (uvar as X) T S :- !,
  if (var S) (declare_constraint (evar X T S) [X, S])
             (X = S, evar X T S).

: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).

% 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 }} puts x in the scope of the hole.

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Coq's goals and tactic invocation (coq_elpi_goal_HOAS.ml)
% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

kind extra-info type.
type goal-name name -> extra-info.

typeabbrev goal-ctx (list prop). % in reality only decl and def entries

kind goal type.

% goal Ctx Solution Ty ExtraInfo
type goal goal-ctx -> term -> term -> list extra-info -> goal.
% 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.
% ExtraInfo contains a list of "extra logical" data attached to the goal.

% nabla is used to close a goal under its bound name. This is useful to pass
% a goal to another piece of code and let it open the goal
type nabla (term -> goal) -> goal.

% The invocation of a tactic with arguments: 3 x "y" (h x)
% on a goal named "?Goal2" with a sequent like
%
% x : t
% y := v : x
% ----------
% g x y
%
% is coded as an elpi goal
%
% (pi x1\ decl x1 `x` <t> =>
%   pi x2\ def x2 `y` x1 <v> =>
%    declare-evar
%       [decl x1 `x` <t>, def x2 `y` x1 <v>]
%       (Evar x1 x2) (<g> x1 x2)),
% (pi x1\ pi x2\
%   solve
%     [int 3, str `x`, str`y`, trm (app[const `h`,x1])]
%     [goal
%        [decl x1 `x` <t>, def x2 `y` x1 <v>]
%        (Evar x1 x2) (<g> x1 x2)
%        [goal-name `?Goal2`]]
%     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.
%
% Note that the solve goal is not under a context containg the decl/def
% entries.  It is up to the user to eventually load the context as follows
%  solve _ [goal Ctx _ Ty] _ :- Ctx => unwind {whd Ty []} WhdTy.
%
% Finally the goal above can be represented as a closed term as
% (nabla x1\ nabla x2\
%      goal
%        [decl x1 `x` <t>, def x2 `y` x1 <v>]
%        (Evar x1 x2) (<g> x1 x2)
%        [goal-name `?Goal2`])


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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".

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

% 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 tt].


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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 warning message
external type coq.warn variadic any prop.

% [coq.error ...] Prints and *aborts* the program (it's a fatal error)
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 posible 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'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.
external pred coq.env.typeof i:gref, o:term.

external pred coq.env.indt % reads the inductive type declaration for the environment
  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
  i:inductive, % reference to the inductive type
  o:indt-decl. % HOAS description of the inductive type
  
% [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)
external pred coq.env.indc i:constructor, o:int, o:int, o:int, o:term.

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

% [coq.env.const GR Bo Ty] reads the type Ty and the body Bo of constant GR.
% Opaque constants have Bo = none.
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
external pred coq.env.const-body i:constant, o:option term.

% [coq.env.const-primitive? GR] tests if GR is a primitive constant (like
% uin63 addition)
external pred coq.env.const-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.

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

% [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.current-path Path] lists the current module path
external pred coq.env.current-path o:list string.

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

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

% [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.
% Supported attributes:
% - @local! (default: false)
external pred coq.env.add-const i:id, i:term, i:term, i:opaque?, 
                                o:constant.

% [coq.env.add-indt Decl I] Declares an inductive type
external pred coq.env.add-indt i:indt-decl, o:inductive.

% Interactive module construction

% [coq.env.begin-module Name ModTyPath] Starts a module, the modtype can be
% omitted *E*
external pred coq.env.begin-module i:id, i:option modtypath.

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

% [coq.env.begin-module-type Name] Starts a module type *E*
external pred coq.env.begin-module-type i:id.

% [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.

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

% [coq.env.include-module-type ModTyPath] is like the vernacular Include *E*
external pred coq.env.include-module-type i:modtypath.

% [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 .

% -- Universes --------------------------------------------------------

% Univ.Universe.t
typeabbrev univ (ctype "univ").


% Universes (for the sort term former)
kind universe type.
type prop universe. % impredicative sort of propositions
type sprop universe. % impredicative sort of propositions with definitional proof irrelevance
type typ univ -> universe. % predicative sort of data (carries a level)

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

% [coq.univ.leq U1 U2] constrains U1 <= U2
external pred coq.univ.leq i:univ, i:univ.

% [coq.univ.eq U1 U2] constrains U1 = U2
external pred coq.univ.eq i:univ, i:univ.

% [coq.univ.new Names U] fresh universe *E*
external pred coq.univ.new i:list id, o:univ.

% [coq.univ.sup U1 U2] constrains U2 = U1 + 1
external pred coq.univ.sup i:univ, i:univ.

% [coq.univ.max U1 U2 U3] constrains U3 = max U1 U2
external pred coq.univ.max i:univ, i:univ, o:univ.

% Very low level, don't use

% [coq.univ.algebraic-max U1 U2 U3] constrains U3 = Max(U1,U2) *E*
external pred coq.univ.algebraic-max i:univ, i:univ, o:univ.

% [coq.univ.algebraic-sup U1 U2] constrains U2 = Sup(U1) *E*
external pred coq.univ.algebraic-sup i:univ, o:univ.

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

typeabbrev uint63 (ctype "uint63").


typeabbrev float64 (ctype "float64").



% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 universe -> cs-pattern.

% Canonical Structure instances: (cs-instance Proj ValPat Inst)
kind cs-instance type.
type cs-instance gref -> cs-pattern -> term -> 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.canonical-projections StructureName Projections] given a record
% StructureName lists all projections
external pred coq.CS.canonical-projections i:inductive, 
                                           o:list (option constant).

% 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 _ From To) as a
% coercion From >-> To.
% Supported attributes:
% - @global! (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).

% -- 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 moatch

% [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.

% Generic attribute value
kind attribute-value type.
type leaf string -> 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:universe, 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.
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.
external pred coq.elaborate-ty-skeleton i:term, o:universe, o:term, 
                                        o:diagnostic.

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

% [coq.reduction.lazy.whd_all T Tred] Puts T in weak head normal form
external pred coq.reduction.lazy.whd_all i:term, o:term.

% [coq.reduction.cbv.whd_all T Tred] Puts T in weak head normal form
external pred coq.reduction.cbv.whd_all i:term, o:term.

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

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

% [coq.ltac1.call Tac Args G GL] Calls Ltac1 tactic named Tac with arguments
% Args on goal G
external pred coq.ltac1.call i:string, i:list term, i:goal, o:list goal.

% -- 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 kernel name, 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
external pred coq.term->string i:term, o:string.

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

% [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 belong to Coq modules: the Scope
% argument
% lets one select which module (default is execution-site). 
% Supported attributes:
% - @local! (default: false)
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).