coq-builtin-synterp.elpi

kind implicit_kind type.
kind field-attribute type.
kind upoly-decl type.
kind upoly-decl-cumul type.

        

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

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

% [coq.notice ...] Prints a notice message
external type coq.notice variadic any prop.

% [coq.say ...] Prints a notice message
external type coq.say variadic any prop.

% [coq.debug ...] Prints a debug message
external type coq.debug 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.


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

% This section contains the low level data types linking Coq and elpi.
% In particular the entry points for commands


% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 main-interp i:list argument, i:any.
pred main-synterp i:list argument, o:any.
pred usage.
pred attributes o:list attribute.

% see coq-lib.elpi for coq.parse-attributes generating the options below
type get-option string -> A -> prop.

% 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).
type open-trm  int -> term -> argument.

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

% 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

kind arity type.
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).

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


% Coq terms are not visible at synterp time, they are always holes

kind term type.

% -- Parsing time APIs
% ----------------------------------------------------

% [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*/
kind modpath type.


% Name of a module type /*E*/
kind modtypath type.


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


kind located type.
type loc-modpath modpath -> located.
type loc-modtypath modtypath -> 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 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>]

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.

% [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.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.modpath->library MP LibraryPath] extract the enclosing module which
% can be Required
external pred coq.modpath->library i:modpath, o:modpath.

% [coq.modtypath->library MTP LibraryPath] extract the enclosing module
% which can be Required
external pred coq.modtypath->library i:modtypath, o:modpath.

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

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

% 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, grafted after or replace
% a named clause
kind grafting type.
type before id -> grafting.
type after id -> grafting.
type remove id -> grafting.
type replace 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)


% see coq.elpi.accumulate-clauses
pred coq.elpi.accumulate i:scope, i:id, i:clause.
coq.elpi.accumulate S N C :- coq.elpi.accumulate-clauses S N [C].


% [coq.elpi.accumulate-clauses Scope DbName Clauses] 
% Declare that, once the program is over, the given clauses 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.
% Clauses cannot be accumulated inside functors.
% Supported attributes:
% - @local! (default: false, discard at the end of section or module)
% - @global! (default: false, always active, only if Scope is
% execution-site, discouraged)
external pred coq.elpi.accumulate-clauses i:scope, i:id, i:list clause.

% Action executed during the parsing phase (aka synterp)
kind synterp-action type.
type begin-module id -> synterp-action.
type begin-module-type id -> synterp-action.
type begin-section id -> synterp-action.
type end-module modpath -> synterp-action.
type end-module-type modtypath -> synterp-action.
type end-section synterp-action.
type apply-module-functor id -> synterp-action.
type apply-module-type-functor id -> synterp-action.
type include-module modpath -> synterp-action.
type include-module-type modtypath -> synterp-action.
type import-module modpath -> synterp-action.
type export-module modpath -> synterp-action.

% Synterp action group
kind group type.


% [coq.synterp-actions A] Get the list of actions performed during the
% parsing phase (aka synterp) up to now.
external pred coq.synterp-actions o:list synterp-action.

% [coq.begin-synterp-group ID Group] Create and open a new synterp action
% group with the given name.
external pred coq.begin-synterp-group i:id, o:group.

% [coq.end-synterp-group Group] End the synterp action group Group. Group
% must refer to the most recently openned group.
external pred coq.end-synterp-group i:group.

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