Document builtins by running a program.

Author: rlepigre

builtin-doc/coq-builtin-synterp.elpi

@@ -0,0 +1,386 @@
+
+
+% -- 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.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).
+
+% 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
+
+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*/
+typeabbrev modpath (ctype "modpath").
+
+
+% Name of a module type /*E*/
+typeabbrev modtypath (ctype "modtypath").
+
+
+% [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 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.
+
+% [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.
+
+
+
+