Rewrite _CoqProject parser to match CoqIDE (#342)

Coq's parser has some idiosyncratic behaviors with respect to single and double
quotes that were easiest to duplicate by just translating the OCaml parser into
VimScript.

CHANGELOG.md

@@ -8,6 +8,8 @@
 - Add a hook for more flexible keybindings (PR #339)
 
 ### Fixed
+- Parse single and double quotes in `_CoqProject` files in the same way as CoqIDE.
+  (PR #342)
 - Fix rendering of goals panel when no proof is active in Coq >= 8.16.
   (PR #337)
 

autoload/coqtail/coqproject.vim

@@ -1,15 +1,111 @@
 " Author: Wolf Honore
 " Locate and parse _CoqProject files.
 
-py3 import shlex
+" Parser adapted from https://github.com/coq/coq/blob/v8.19/lib/coqProject_file.ml.
+
+function! s:parse_skip_comment(s) abort
+  let l:s = a:s
+  while !empty(l:s)
+    let l:c = l:s[0]
+    let l:s = l:s[1:]
+    if l:c ==# "\n"
+      break
+    endif
+  endwhile
+  return l:s
+endfunction
+
+function! s:parse_string2(s) abort
+  let l:buf = ''
+  let l:s = a:s
+  while !empty(l:s)
+    let l:c = l:s[0]
+    let l:s = l:s[1:]
+    if l:c ==# '"'
+      break
+    else
+      let l:buf .= l:c
+    endif
+  endwhile
+  return [l:s, l:buf]
+endfunction
+
+function! s:parse_string(s) abort
+  let l:buf = ''
+  let l:s = a:s
+  while !empty(l:s)
+    let l:c = l:s[0]
+    let l:s = l:s[1:]
+    if l:c ==# ' ' || l:c ==# "\r" || l:c ==# "\n" || l:c ==# "\t"
+      break
+    elseif l:c ==# '#'
+      let l:s = s:parse_skip_comment(l:s)
+    else
+      let l:buf .= l:c
+    endif
+  endwhile
+  return [l:s, l:buf]
+endfunction
+
+function! s:parse_args(s) abort
+  let l:accu = []
+  let l:s = a:s
+  while !empty(l:s)
+    let l:c = l:s[0]
+    let l:s = l:s[1:]
+    if l:c ==# ' ' || l:c ==# "\r" || l:c ==# "\n" || l:c ==# "\t"
+    elseif l:c ==# '#'
+      let l:s = s:parse_skip_comment(l:s)
+    elseif l:c ==# '"'
+      let [l:s, l:str] = s:parse_string2(l:s)
+      let l:accu = add(l:accu, l:str)
+    else
+      let [l:s, l:str] = s:parse_string(l:s)
+      let l:accu = add(l:accu, l:c . l:str)
+    endif
+  endwhile
+  return l:accu
+endfunction
+
+function! s:process_extra_args(arg) abort
+  let l:out_list = []
+  let l:arg = a:arg
+  let l:inside_quotes = 0
+  let l:has_leftovers = 0
+  let l:buf = ''
+  while !empty(l:arg)
+    let l:c = l:arg[0]
+    let l:arg = l:arg[1:]
+    if l:c ==# "'"
+      let l:inside_quotes = !l:inside_quotes
+      let l:has_leftovers = 1
+    elseif l:c ==# ' '
+      if l:inside_quotes
+        let l:has_leftovers = 1
+        let l:buf .= ' '
+      elseif l:has_leftovers
+        let l:has_leftovers = 0
+        let l:out_list = add(l:out_list, l:buf)
+        let l:buf = ''
+      endif
+    else
+      let l:has_leftovers = 1
+      let l:buf .= l:c
+    endif
+  endwhile
+  if l:has_leftovers
+    let l:out_list = add(l:out_list, l:buf)
+  endif
+  return l:out_list
+endfunction
 
 " Parse a _CoqProject file into options that can be passed to Coqtop.
 function! coqtail#coqproject#parse(file) abort
   let l:dir = fnamemodify(a:file, ':p:h')
   let l:dir_opts = {'-R': 2, '-Q': 2, '-I': 1, '-include': 1}
 
-  let l:txt = join(readfile(a:file))
-  let l:raw_args = py3eval(printf('shlex.split(r%s)', string(l:txt)))
+  let l:txt = join(readfile(a:file), "\n")
+  let l:raw_args = s:parse_args(l:txt)
 
   let l:proj_args = []
   let l:idx = 0
@@ -34,7 +130,7 @@ function! coqtail#coqproject#parse(file) abort
 
     " Pass through options following -arg
     if l:raw_args[l:idx] ==# '-arg'
-      let l:proj_args = add(l:proj_args, l:raw_args[l:idx + 1])
+      let l:proj_args += s:process_extra_args(l:raw_args[l:idx + 1])
       let l:idx += 1
     endif
 

tests/vim/coq_project.vader

@@ -147,26 +147,42 @@ Execute (quote-empty):
   let args = coqtail#coqproject#parse(f)
   AssertEqual ['-R', d . '/', ''], args
 
-Execute (quote-escape):
-  let d = tempname()
-  let sd = 'quote"subdir'
-  let sdEsc = 'quote\"subdir'
-  let dsd = join([d, sd], '/')
-  let dsdEsc = join([d, sdEsc], '/')
-  call mkdir(dsd, 'p')
-  let f = join([dsd, '1'], '/')
-  call writefile(['-R "' . dsdEsc . '" top'], f)
-  let args = coqtail#coqproject#parse(f)
-  AssertEqual ['-R', dsd . '/', 'top'], args
-
 Execute (arg):
   let f = tempname()
   call writefile(['-arg -w -arg all'], f)
   let args = coqtail#coqproject#parse(f)
   AssertEqual ['-w', 'all'], args
 
+" See https://coq.inria.fr/doc/v8.19/refman/practical-tools/utilities.html#quoting-arguments-to-coqc
+Execute (double-quote-arg):
+  let f = tempname()
+  call writefile(['-arg "-w all"'], f)
+  let args = coqtail#coqproject#parse(f)
+  AssertEqual ['-w', 'all'], args
+
+Execute (single-quote-in-double-quote-arg):
+  let f = tempname()
+  call writefile(["-arg \"-set 'Default Goal Selector=!'\""], f)
+  let args = coqtail#coqproject#parse(f)
+  AssertEqual ['-set', 'Default Goal Selector=!'], args
+
+Execute (single-quote-not-in-double-quote-arg):
+  let f1 = tempname()
+  call writefile(["-arg 'foo bar'"], f1)
+  let args1 = coqtail#coqproject#parse(f1)
+  let f2 = tempname()
+  call writefile(["-arg foo \"bar'\""], f2)
+  let args2 = coqtail#coqproject#parse(f2)
+  AssertEqual args1, args2
+
 Execute (ignore-files):
   let f = tempname()
   call writefile(['-arg a', '-byte', 'A.v'], f)
   let args = coqtail#coqproject#parse(f)
   AssertEqual ['a'], args
+
+Execute (ignore-comments):
+  let f = tempname()
+  call writefile(['# abc', '-arg a', '# def', '-arg b', '# ghi'], f)
+  let args = coqtail#coqproject#parse(f)
+  AssertEqual ['a', 'b'], args