Commit ce40b874 authored by Manu Beffara's avatar Manu Beffara
Browse files

Adujustments to support the Coq 8.7 protocol.

parent 588794d3
......@@ -12,12 +12,14 @@ Requirements
Coq-au-Vim requires
- Vim version 8
- Coq version 8.6
- Coq version 8.6 or 8.7
Prior versions of Vim will not be supported because version 8 is the one that
introduces asynchronous communication with external tools. For older versions
of Vim, use [Coquille](https://github.com/the-lambda-church/coquille), which
works well with Coq up to version 8.5.
introduces asynchronous communication with external tools. Prior versions of
Coq will not be supported either because the interaction protocol has changed
completely with version 8.6. For older versions of Vim and Coq, use
[Coquille](https://github.com/the-lambda-church/coquille), which works well
with Coq up to version 8.5.
Installation
......
......@@ -319,7 +319,7 @@ endfunction
" - a dictionary is matched key by key, each key in the pattern must be
" present in the value (except with '?name' patterns) but other keys may
" be present too,
" - a list ['?'; choices] is interpreted as a choice: the liste 'choices'
" - a list ['?'; choices] is interpreted as a choice: the list 'choices'
" consists of pairs [pattern,dict] where 'pattern' is tried against the
" value and 'dict' contains extra items for the result value; the first
" match in the list of choices will provide the result.
......@@ -434,7 +434,7 @@ function! s:match (value, pattern)
endfunction
" Match a value against a list of patterns and return the dictionary for the
" forst match. The arguments 'patterns' is a list of pairs [pattern, dict]
" first match. The arguments 'patterns' is a list of pairs [pattern, dict]
" where 'pattern' is used as for the 'Match' function and 'dict' is a
" dictionary of extra items added to the return value in case of match. An
" optional third argument specifies extra items to add in the return value.
......@@ -459,7 +459,7 @@ endfunction
" Everything related to Coq interaction is encapsulated in an object called
" b:coq. This is a dictionary that contains all the relevant state as well as
" methods for interaction with coqtop (using Vim's mechanism of dictionary
" functions). The script object s:coq is a template that gets instanciated
" functions). The script object s:coq is a template that gets instantiated
" as a buffer object b:coq when a session is started, then everything goes
" through this buffer-local object.
"
......@@ -636,17 +636,20 @@ endfunction
" For each request, we provide a function that expects an argument for each
" field in the request, plus a callback (named 'return') and a dictionary
" 'dict' of extra parameters. When an answer is received, 'return' is called
" with a dictionary containg the conents of 'dict' plus the fields of the
" answer, always with at leas a field 'success' that indicates whether the
" call succeeded.
" with a dictionary containing the contents of 'dict' plus the fields of the
" answer, always with at least a field 'success' that indicates whether the
" call succeeded. When the call failed, the dictionary contains a field
" 'message' with the error message.
"
" We provide one function per call in the Coq API, on return the state
" representation is updated.
let s:supported_protocols = ['20150913', '20170413']
" about() {{{3
" -> {version, protocol, release, compile}
"
" Get information avout Coq: version number, protocol version, release date
" Get information about Coq: version number, protocol version, release date
" and compile date.
function s:coq.call_about (return, dict)
......@@ -895,19 +898,38 @@ function s:coq.return_init (return, d)
call a:return(a:d)
endfunction
" query(text, state_id) {{{3
" -> {message}
" query(route_id, text, state_id) {{{3
" -> {}
"
" Perform a query in some state.
" Perform a query in some state and display the answer.
function s:coq.call_query (route_id, text, state_id, return, dict)
call self.log('r', "call", "query", a:route_id, a:text, a:state_id)
if self.protocol >= '20170413'
call self.call('Query',
\ ['pair', {},
\ ['route_id', {'val': a:route_id}],
\ ['pair', {},
\ ['string', {}, a:text],
\ ['state_id', {'val': a:state_id}]]],
\ a:return, a:dict,
\ [[['unit', {}]], {}])
function s:coq.call_query (text, state_id, return, dict)
call self.log('r', "call", "query", a:text, a:state_id)
call self.call('Query',
\ ['pair', {},
\ ['string', {}, a:text],
\ ['state_id', {'val': a:state_id}]],
\ a:return, a:dict,
\ [[['string', {}, '*message']], {}])
else
call self.call('Query',
\ ['pair', {},
\ ['string', {}, a:text],
\ ['state_id', {'val': a:state_id}]],
\ function(self.return_query, [a:return]), a:dict,
\ [[['string', {}, '*message']], {}])
endif
endfunction
function s:coq.return_query (return, d)
if a:d.success
call self.infos.write(a:d.message)
endif
call a:return(a:d)
endfunction
" quit() {{{3
......@@ -969,10 +991,6 @@ endfunction
" == Handling feedback == {{{2
function s:coq.feedback(state_id, kind, content)
if !has_key(self.states, a:state_id)
return self.log('e', 'feedback', 'feedback for unknown state', a:state_id)
endif
let r = s:match_first([a:kind, a:content], [
\ [['processed', []], {}],
\ [['complete', []], {}],
......@@ -1011,7 +1029,14 @@ function s:coq.feedback(state_id, kind, content)
return self.protocol_error("feedback message", a:content)
endif
call self.log('f', 'message', a:state_id, r)
call add(self.states[a:state_id].messages, r)
if a:state_id ==# self.focus || !has_key(self.states, a:state_id)
" The state_id may be unknown in the case of feedback received between
" an Add query and its successful answer, then the feedback is shown as
" if it were for the current state.
call self.infos.write(s:richpp_format(r.message))
else
call add(self.states[a:state_id].messages, r)
endif
else
call self.log('f', a:kind, a:state_id, a:content)
......@@ -1210,7 +1235,7 @@ endfunction
let s:window = {}
" Create a new window with a new bufffer using a given name and filetype. The
" Create a new window with a new buffer using a given name and filetype. The
" buffer will have no file associated to it, a number may be added to the
" buffer name to ensure it is unique. The third argument specifies whether
" splitting should be vertical or horizontal.
......@@ -1338,10 +1363,11 @@ function s:coq.create ()
endfunction
function s:coq.start_version (d)
if a:d.protocol !=# '20150913'
if index(s:supported_protocols, a:d.protocol) < 0
return self.infos.write("Unsupported Coq protocol version: "
\ . a:d.protocol)
endif
let self.protocol = a:d.protocol
call self.infos.write("Coq version "
\ . a:d.version . " (" . a:d.release . ") started.")
call self.call_init(self.start_state, {})
......@@ -1593,14 +1619,12 @@ endfunction
function s:coq.query (text)
try
call self.infos.clear()
call self.call_query(a:text, self.focus, self.query_return, {})
call self.call_query(0, a:text, self.focus, self.query_return, {})
endtry
endfunction
function s:coq.query_return (d)
if a:d.success
call self.infos.write(a:d.message)
else
if !a:d.success
call self.infos.write(s:richpp_format(a:d.message))
endif
endfunction
......
......@@ -27,7 +27,7 @@ This plugin provides a environment for working with the Coq theorem prover.
It provides |filetype| support for editing Coq source files and a mode for
interactive proof development, in the style of the standard Coq IDE.
The interactive mode requires Vim version 8 and Coq version 8.6.
The interactive mode requires Vim version 8 and Coq version 8.6 or 8.7.
=============================================================================
......
" = Motions = {{{1
" Search forward for a pattern, skipping comments. The return value is the
" number of the first maching sub-expression (as for the Vim function search()
" with the 'p' option). The second argument indicates whether a match at the
" current position is accepted.
" number of the first matching sub-expression (as for the Vim function
" search() with the 'p' option). The second argument indicates whether a match
" at the current position is accepted.
function! s:SearchForward (pattern, immediate)
let immediate = a:immediate
......@@ -39,9 +39,9 @@ function! s:SearchForward (pattern, immediate)
endfunction
" Search backward for a pattern, skipping comments. The return value is the
" number of the first maching sub-expression (as for the Vim function search()
" with the 'p' option). The second argument indicates whether a match at the
" current position is accepted.
" number of the first matching sub-expression (as for the Vim function
" search() with the 'p' option). The second argument indicates whether a match
" at the current position is accepted.
function! s:SearchBackward (pattern, immediate)
let immediate = a:immediate
......@@ -162,7 +162,7 @@ function! CoqNextSentence (count)
return s:SearchForward('\S', v:false) !=# 0
endfunction
" Move the the beginning of the current sentence, or the previous one if the
" Move the beginning of the current sentence, or the previous one if the
" cursor is already at the beginning of a sentence. The 'count' argument
" indicates how many sentences to advance. Return v:true if a proper previous
" sentence was found, v:false otherwise.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment