Next: SOFTWARE-EVOLUTION-LIBRARY/COMPONENTS/TEST-SUITE, Previous: SOFTWARE-EVOLUTION-LIBRARY/COMPONENTS/SEARCHABLE, Up: Software Evolution Library Index [Contents][Index]
Class precedence list: serapi-error, error, serious-condition, condition, slot-object, t
Condition raised if errors are detected in the SerAPI process.
Class precedence list: serapi-timeout-error, error, serious-condition, condition, slot-object, t
Condition raised if timeout is exceeded.
Main SerAPI process. Ensure new threads each have their own copy or else.
Maximum amount of time to wait before determining that no data can be read.
Arguments to sertop program.
Path to sertop program.
Look up and return the type of a Coq expression coq-expr.
Optionally use qtag to tag the query.
Look up and return the type of a coq-expr using Coq’s ‘Check’.
coq-expr will be coerced to a string via the ‘format’ ~a directive.
Macro to create a serapi process bound to serapi.
Uses default path and arguments for sertop (‘*sertop-path*’ and
‘*sertop-args*’).
Add directory path to the Coq and, optionally, ml load paths in SerAPI.
Return the SerAPI response.
* lib-name an optional prefix to use when importing from the directory. e.g.,
for lib-name Foo, file PATH/Bar.vo could be imported with
"Require Import Foo.Bar.").
* has-ml the string "true" or "false", indicating whether path should or
should not be added to the ml load path in addition to the Coq load path. For
convenience, the default is "true".
* qtag optionally, a tag to use for the SerAPI command.
Submit coq-string as a new statement to add to the Coq document.
Return a list of the AST-IDs created as a result. Optionally, provide a qtag for
the submission.
Cancel the ASTs identified by ast-ids and return the response.
Optionally, use qtag to tag the query. Canceling means that the ASTs will no
longer be defined and other definitions added in the interim will also be
removed.
Return name of Parameter, Variable, etc. if sexpr is tagged VernacAssumption.
Otherwise return nil.
Return definition name if sexpr is tagged as a definition, nil otherwise.
Definition tags include VernacDefinition, VernacInductive, VernacFixpoint,
VernacCoFixpoint.
Return t if sexpr is a Coq VernacDefinition expression.
If function-name is specified, only return t if sexpr defines a function
named function-name.
Return t if sexpr is tagged as VernacImport or VernacRequire, nil otherwise.
For a SerAPI response, return the contents of any ‘Message’ structures. This is useful for fetching results of Coq vernacular queries.
For a SerAPI response, return the level of the first ‘Message’ structure. This is useful for verifying success of a Coq vernacular query.
Return module name if sexpr is tagged as defining a module, nil otherwise.
Module tags include VernacDefineModule, VernacDeclareModule,
VernacDeclareModuleType.
Return section name if sexpr is tagged as VernacBeginSection, nil otherwise.
Insert a reset point so ‘*serapi-process*’ may be reset to its current state.
Add Coq ‘*dummy-stmt*’ to ‘*serapi-process*’ and update ‘reset-points’ with the
AST id. See also ‘reset-serapi-process’.
Check if output is an error response from SerAPI.
Return t if sexpr is an error message from either an improperly formed SerAPI
command or an invalid Coq command, nil otherwise.
Check if str is an error message.
Errors may result from either an improperly formed SerAPI command or an invalid
Coq command.
Return t if sexpr is a list of Coq location info, nil otherwise.
Check if output is indicates the end of a SerAPI response.
Return t if sexpr is the final message in a SerAPI response, nil otherwise.
For successful responses, the list will be tagged as "Completed", and
for failed responses it will be tagged as an error.
Check if str is the final message in a SerAPI response.
For successful responses, the string will contain the word "Completed", and
for failed responses it will be an error string.
Load Coq file file-name. Optionally, use qtag to tag the query.
Return a list of IDs for the ASTs that were added.
Look up and return the AST identified by ast-id.
Optionally, use qtag to tag the query.
Look up and return the AST whose id is the integer ast-id.
Optionally, use qtag to tag the query.
Look up and return a Coq representation of ast-name.
Optionally, tag the lookup query with qtag.
Look up the Coq string for id.
If needed specify the input-format of the id. Optionally, provide a qtag for
the lookup query.
The id may be either an integer AST id or one of the list representations,
CoqPp, CoqAst, etc.
raw-string is already a Coq string. Return it without doing a lookup.
Look up the Coq string for id in process.
Optionally, provide a qtag for the lookup query. input-format is ignored.
Look up the Coq string for pp-string.
If pp-string is not a CoqAst expression, specify the input-format. See the
coq_object type in the SerAPI file serapi/serapi_protocol.mli for a complete
list. Optionally, provide a qtag for the lookup query.
Wrap Coq function fun and parameters params in a CApp tag.
Assumes that fun and all params are appropriately wrapped (e.g., with
‘make-coq-var-reference’ or similar).
Create cases for a Coq match statement.
Create a Coq function definition.
name - the name of the function.
params - a list of pairs indicating the name and type of each input parameter to
the function.
return-type - the function’s return type.
body - the function body.
Wrap id in Ident and Id tags.
Create a Coq If expression: if test then then else else.
Wrap integer x in CPrim and Numeral tags.
Create a Coq lambda expression from params and body.
Create a list of local binder expressions.
If present, param-types is the same length as params and indicates the type of
each param. If absent, a CHole tag is used to indicate that the type is
unspecified.
Create a Coq match expression.
style indicates the style of the match (e.g., #!’RegularStyle).
test is the expression being matched against.
branches are the match cases and will generally be constructed with
‘make-coq-case-pattern’.
Wrap id in Name and Id tags.
Wrap Coq variable id in CRef and either Ident or Qualid tags.
Use Ident for unqualified names and Qualid for qualified names.
Start up SerAPI and return a process object to interact with.
Reset ‘*serapi-process*’ to the last reset point in its ‘reset-points’. See also ‘insert-reset-point’.
Ensure that special characters are properly escaped in string.
Backslashes and quotation marks are escaped, and whitespace characters (\n,
\t, \r, \b) are replaced with a single space.
Return a list of tokenized types of values whose "final" type is coq-type.
Results include functions parameterized by values of types other than coq-type
as long as the final result returned by the function is of type coq-type.
e.g., if coq-type is bool, functions of type nat->bool will be included.
Return t if the serapi process is running.
Function to set ‘*sertop-path*’ and ‘*sertop-args*’ automatically.
Uses serapi environment variable or "which sertop.native" to set
‘*sertop-path*’. Uses coqlib environment variable to add "–coqlib" flag
to ‘*sertop-args*’.
Create a Coq ConstrExpr by wrapping expr with v and loc tags.
Generally, this will be used by the ‘make-coq-*’ functions and won’t need to be
invoked directly.