lean2/doc/server.org
Leonardo de Moura 5aa0ef56eb doc(server): add FINDG and FINDP documentation, closes #144
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 09:17:15 -07:00

373 lines
8.8 KiB
Org Mode

Lean can process input incrementally, and extract type information.
This feature is useful for implementing "intelligent" support for Lean
in editors such as Emacs. It provides a convenient way to access
descriptions of functions, overloaded symbols, and typing information.
We must use the option =--server= to enable this feature.
* Commands
Lean implements a simple set of commands for loading files, extracting
typing information, and "replacing" lines. The commands should be sent
to the standard input.
** Load file
#+BEGIN_SRC
LOAD [file-name]
#+END_SRC
This command loads the Lean file named =[file-name]=.
Lean will create a "snapshot" (aka backtracking point) after each
command. Lean uses the "snapshots" to process incremental updates efficiently.
** Visit file
#+BEGIN_SRC
VISIT [file-name]
#+END_SRC
Lean can keep information about multiple files. This command
sets =[file-name]= as the "current" file. The remaining commands
are all with respect to the current file. If =[file-name]= has not been
loaded yet, then this command will load it. Some of the remaining commands
apply "changes" to the current file. The =LOAD= command can be used to
discard all these changes, and enforce the content of the file stored
in file system.
** Replace line
#+BEGIN_SRC
REPLACE [line-number]
[new-line]
#+END_SRC
This command replaces the line =[line-number]= (in the current file) with =[new-line]=.
Lean uses the snapshots to process the request efficiently.
If =[line-number]= is greater than the total number of lines in the lean
buffer, then empty lines are introduced. The lines are indexed from 1.
** Insert line
#+BEGIN_SRC
INSERT [line-number]
[new-line]
#+END_SRC
This command inserts =[new-line]= (in the current file) before line =[line-number]=.
If =[line-number]= is greater than the total number of lines in the lean
buffer, then empty lines are introduced. The lines are indexed from 1.
** Remove line
#+BEGIN_SRC
REMOVE [line-number]
#+END_SRC
Remove line =[line-number]= (in the current file). The lines are indexed from 1.
If =[line-number]= is greater than the total number of lines in the lean
buffer, then the command is ignored.
** Extracting information
#+BEGIN_SRC
INFO [line-number] [column-number]?
#+END_SRC
This command extracts typing information associated with line
=[line-number]= (in the current file) and =[column-number]=.
If =[column-number]= is not provided then (potentially) long
information is not included.
Lean produces a possible empty sequence of entries delimited by the lines
=-- BEGININFO= and =-- ENDINFO=.
#+BEGIN_SRC
-- BEGININFO
[entries]*
-- ENDINFO
#+END_SRC
If the server is still busy processing a previously requested update, then it
produces the output
#+BEGIN_SRC
-- BEGININFO
-- NAY
-- ENDINFO
#+END_SRC
where =NAY= stands for "not available yet".
A type information entry is of the form
#+BEGIN_SRC
-- TYPE|[line-number]|[column-number]
[type]
-- ACK
#+END_SRC
Information for overloaded operators and symbols is of the form
#+BEGIN_SRC
-- OVERLOAD|[line-number]|[column-number]
[overload-1]
--
...
--
[overload-n]
-- ACK
#+END_SRC
Information for synthesized placeholders is of the form
#+BEGIN_SRC
-- SYNTH|[line-number]|[column-number]
[synthesized-term]
-- ACK
#+END_SRC
The following two information entries provide information for Lean keywords/symbols and identifiers.
#+BEGIN_SRC
-- SYMBOL|[line-number]|[column-number]
[symbol]
-- ACK
#+END_SRC
#+BEGIN_SRC
-- IDENTIFIER|[line-number]|[column-number]
[fully-qualified-name]
-- ACK
#+END_SRC
Information about introduced coercions is of the form
#+BEGIN_SRC
-- COERCION|[line-number]|[column-number]
[coercion-application]
--
[result-type]
-- ACK
#+END_SRC
When =[column-number]= is provided in the =INFO= command, the type of terms surrounded by =()=
is also included. The ouput has the form
#+BEGIN_SRC
-- EXTRA_TYPE|[line-number]|[column-number]
[term]
--
[type]
-- ACK
#+END_SRC
Here is an example of output produced by Lean
#+BEGIN_SRC
-- BEGININFO
-- TYPE|15|38
num
-- ACK
-- TYPE|15|40
num → num → Prop
-- ACK
-- OVERLOAD|15|42
f
--
foo.f
-- ACK
-- TYPE|15|42
num → num
-- ACK
-- TYPE|15|44
num
-- ACK
-- IDENTIFIER|15|42
foo.f
-- ACK
-- ENDINFO
#+END_SRC
** Check line
As described above, several commands can be used to apply
modifications to opened/visited files. These modification reflect
modifications performed by the text editor. The command =CHECK= can be
used to double check whether the text editor and Lean have the "same
view" of the current file + modifications.
The following commands returns =-- OK= if the line =[line-number]= in
the current file is =[line]=. It returns =-- MISMATCH line out of
range=, if =[line-number]= is too big, and =-- MISMATCH expected
[lean-line]= when there is a mismatch, and Lean expects
=[line-number]= to be =[lean-line]=.
#+BEGIN_SRC
-- CHECK [line-number]
[line]
#+END_SRC
** Set configuration option
The command
#+BEGIN_SRC
-- SET
[option-name] [value]
#+END_SRC
sets a Lean options, =[option-name]= must be a valid Lean option.
Any option that can be set using the command =set_option= in a '.lean'
file is supported.
This command produces the output
#+BEGIN_SRC
-- BEGINSET
[error]?
-- ENDSET
#+END_SRC
where the line =[error]?= is printed if there are errors parsing the
=SET= command (e.g., invalid option name).
Here is an example that forces the Lean pretty printer to display
implicit arguments.
#+BEGIN_SRC
-- SET
pp.implicit true
#+END_SRC
** Eval
The following command evaluates a Lean command. It has the effect of
evaluating a command in the end of the current file
#+BEGIN_SRC
-- EVAL
[command]
#+END_SRC
This command produces the output
#+BEGIN_SRC
-- BEGINEVAL
[error]/[output]
-- ENDEVAL
#+END_SRC
Here is an example that executes the =check= command to obtain the
type of =Prop=.
#+BEGIN_SRC
-- EVAL
check Prop
#+END_SRC
If the server is still busy processing a previously requested update, then it
produces the output
#+BEGIN_SRC
-- BEGINEVAL
-- NAY
-- ENDEVAL
#+END_SRC
** Wait
The following command is for debugging purposes. It blocks the server
until all pending information has been computed.
#+BEGIN_SRC
WAIT
#+END_SRC
** Options
The command =OPTIONS= display all configuration options available
in Lean. It has the form
#+BEGIN_SRC
OPTIONS
#+END_SRC
The output is a sequence of entries
#+BEGIN_SRC
-- BEGINOPTIONS
[entry]*
-- ENDOPTIONS
#+END_SRC
where each entry is of the form
#+BEGIN_SRC
-- [name]|[kind]|[default-value]|[description]
#+END_SRC
The available =kinds= are: =Bool=, =Int=, =Unsigned Int=, =Double=,
=String=, and =S-Expressions=.
** Find pattern
Given a sequence of characters, the command =FINDP= uses string fuzzy matching to
find declarations in the environment. The procedure uses [Bitap algorithm](http://en.wikipedia.org/wiki/Bitap_algorithm).
The approximate match is defined in terms of [Levenshtein distance](http://en.wikipedia.org/wiki/Levenshtein_distance).
The matches are sorted based on this distance.
#+BEGIN_SRC
FINDP [line-number]
[pattern]
#+END_SRC
The line number =[line-number]= is used to select the environment object that will be used to perform the search.
Only declarations in the environment are considered by =FINDP=.
The output has the following form
#+BEGIN_SRC
-- BEGINFINDP [NAY]? [STALE]?
[entries]*
-- ENDFINDP
#+END_SRC
The modifier =NAY= is included when the environment object for the given line is not available yet.
The modifier =STALE= is included to indicate that an environment object is being used, but it
does not contain the latest changes.
The entries are of the form
#+BEGIN_SRC
[name]|[type]
#+END_SRC
The types are printed without using line breaks.
The command =FINDP= is mainly used to implement auto-completion.
** Find declarations for "placeholder/goal"
A declaration may contain placeholders/goals =_=. Some of these placeholders are instantiated automatically by Lean.
Others, must be manually filled by the user. The command =FINDG= generates a sequence of declarations that may be used to
"fill" a particular placeholder. This command is only available if the declaration containing =_= is type correct, and
lean "knows" what is the expected type for =_=.
#+BEGIN_SRC
FINDG [line-number] [column-number]
[filters]*
#+END_SRC
The character at the given =[line-number]= and =[column-number]= must be a =_=.
The command also accepts a sequence of filters of the form =+[id_1]= and =-[id_2]=.
Lean will only consider declarations whose name contains =id_1= and does not contain =id_2=.
Here is an example:
#+BEGIN_SRC
FINDG 48 10
+intro -and -elim
#+END_SRC
For the command above, lean will print any declaration whose resultant type matches the type expected by =_=, and
whose name contains =intro= but does not contain =and= and =elim=.
Lean does not display "trivial" matches. We say a match is trivial if the resultant type of a declaration
matches anything.
The output produced by =FINDG= uses the same format used by =FINDP=.