From b279d7b45cda89e2f019a0d3d0de9acaa7606547 Mon Sep 17 00:00:00 2001 From: Max Zinkus Date: Mon, 2 Dec 2019 16:34:22 -0500 Subject: [PATCH 1/3] Update syntax file to handle nested comments Addresses https://github.com/FStarLang/VimFStar/issues/17 This may introduce some weird edge cases with nested comments. However, it preserves correct behavior for normal comments and fixes the case of nested comments in a similar way to vim's `c.vim` (using a dedicated region for line comments). As with `c.vim`, we shrug at the edge cases. --- syntax/fstar.vim | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/syntax/fstar.vim b/syntax/fstar.vim index 95a3275..ffc9eb9 100644 --- a/syntax/fstar.vim +++ b/syntax/fstar.vim @@ -74,7 +74,7 @@ syn region fstarEncl transparent matchgroup=fstarKeyword start="\[|" matchgrou " Comments syn region fstarComment start="(\*" end="\*)" contains=@Spell,fstarComment,fstarTodo -syn match fstarComment "//.*$" contains=fstarComment,fstarTodo,@Spell +syn match fstarCommentLine "//.*$" contains=fstarComment,fstarCommentLine,fstarTodo,@Spell syn keyword fstarTodo contained TODO FIXME XXX NOTE @@ -105,33 +105,33 @@ syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarKe " "sig" syn region fstarSig matchgroup=fstarModule start="\" matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr,fstarModule -syn region fstarModSpec matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contained contains=@fstarAllErrs,fstarComment skipwhite skipempty nextgroup=fstarModTRWith,fstarMPRestr +syn region fstarModSpec matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contained contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarModTRWith,fstarMPRestr " "open" -syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*\>" contains=@fstarAllErrs,fstarComment +syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine " "include" syn match fstarKeyword "\" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod " "module" - somewhat complicated stuff ;-) -syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment skipwhite skipempty nextgroup=fstarPreDef -syn region fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS +syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef +syn region fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS syn region fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal syn match fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr -syn region fstarPreMPRestr start="."me=e-1 end=")"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarMPRestr,fstarModTypeRestr +syn region fstarPreMPRestr start="."me=e-1 end=")"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarMPRestr,fstarModTypeRestr -syn region fstarMPRestr start=":" end="."me=e-1 contained contains=@fstarComment skipwhite skipempty nextgroup=fstarMPRestr1,fstarMPRestr2,fstarMPRestr3 +syn region fstarMPRestr start=":" end="."me=e-1 contained contains=@fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarMPRestr1,fstarMPRestr2,fstarMPRestr3 syn region fstarMPRestr1 matchgroup=fstarModule start="\ssig\s\=" matchgroup=fstarModule end="\" contained contains=ALLBUT,@fstarContained,fstarEndErr,fstarModule -syn region fstarMPRestr2 start="\sfunctor\(\s\|(\)\="me=e-1 matchgroup=fstarKeyword end="->" contained contains=@fstarAllErrs,fstarComment,fstarModParam skipwhite skipempty nextgroup=fstarFuncWith,fstarMPRestr2 +syn region fstarMPRestr2 start="\sfunctor\(\s\|(\)\="me=e-1 matchgroup=fstarKeyword end="->" contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam skipwhite skipempty nextgroup=fstarFuncWith,fstarMPRestr2 syn match fstarMPRestr3 "\w\(\w\|'\)*\( *\. *\w\(\w\|'\)*\)*" contained syn match fstarModPreRHS "=" contained skipwhite skipempty nextgroup=fstarModParam,fstarFullMod syn keyword fstarKeyword val -syn region fstarVal matchgroup=fstarKeyword start="\" matchgroup=fstarLCIdentifier end="\<\l\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarFullMod skipwhite skipempty nextgroup=fstarMPRestr -syn region fstarModRHS start="." end=". *\w\|([^*]"me=e-2 contained contains=fstarComment skipwhite skipempty nextgroup=fstarModParam,fstarFullMod +syn region fstarVal matchgroup=fstarKeyword start="\" matchgroup=fstarLCIdentifier end="\<\l\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarFullMod skipwhite skipempty nextgroup=fstarMPRestr +syn region fstarModRHS start="." end=". *\w\|([^*]"me=e-2 contained contains=fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarModParam,fstarFullMod syn match fstarFullMod "\<\u\(\w\|'\)*\( *\. *\u\(\w\|'\)*\)*" contained skipwhite skipempty nextgroup=fstarFuncWith -syn region fstarFuncWith start="([^*]"me=e-1 end=")" contained contains=fstarComment,fstarWith,fstarFuncStruct skipwhite skipempty nextgroup=fstarFuncWith +syn region fstarFuncWith start="([^*]"me=e-1 end=")" contained contains=fstarComment,fstarCommentLine,fstarWith,fstarFuncStruct skipwhite skipempty nextgroup=fstarFuncWith syn region fstarFuncStruct matchgroup=fstarModule start="[^a-zA-Z]struct\>"hs=s+1 matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr syn match fstarModTypeRestr "\<\w\(\w\|'\)*\( *\. *\w\(\w\|'\)*\)*\>" contained @@ -143,7 +143,7 @@ syn region fstarWithRest start="[^)]" end=")"me=e-1 contained contains=ALLBUT, syn region fstarStruct matchgroup=fstarModule start="\<\(module\s\+\)\=struct\>" matchgroup=fstarModule end="\" contains=ALLBUT,@fstarContained,fstarEndErr " "module type" -syn region fstarKeyword start="\\s*\\(\s*\\)\=" matchgroup=fstarModule end="\<\w\(\w\|'\)*\>" contains=fstarComment skipwhite skipempty nextgroup=fstarMTDef +syn region fstarKeyword start="\\s*\\(\s*\\)\=" matchgroup=fstarModule end="\<\w\(\w\|'\)*\>" contains=fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarMTDef syn match fstarMTDef "=\s*\w\(\w\|'\)*\>"hs=s+1,me=s+1 skipwhite skipempty nextgroup=fstarFullMod syn keyword fstarKeyword and as assume assert @@ -276,6 +276,7 @@ if version >= 508 || !exists("did_fstar_syntax_inits") HiLink fstarErr Error HiLink fstarComment Comment + HiLink fstarCommentLine Comment HiLink fstarModPath Include HiLink fstarObject Include From a3a9e92b0d8473314007fde066fdee6ef1b1fe9d Mon Sep 17 00:00:00 2001 From: Max Zinkus Date: Mon, 2 Dec 2019 17:54:02 -0500 Subject: [PATCH 2/3] Fix module line syntax matching --- syntax/fstar.vim | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/syntax/fstar.vim b/syntax/fstar.vim index ffc9eb9..f01a3b1 100644 --- a/syntax/fstar.vim +++ b/syntax/fstar.vim @@ -114,7 +114,7 @@ syn region fstarNone matchgroup=fstarKeyword start="\" matchgroup=fstar syn match fstarKeyword "\" skipwhite skipempty nextgroup=fstarModParam,fstarFullMod " "module" - somewhat complicated stuff ;-) -syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>" contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef +syn region fstarModule matchgroup=fstarKeyword start="\" matchgroup=fstarModule end="\<\u\(\w\|'\)*\>"me=e-1 contains=@fstarAllErrs,fstarComment,fstarCommentLine skipwhite skipempty nextgroup=fstarPreDef syn region fstarPreDef start="."me=e-1 matchgroup=fstarKeyword end="\l\|=\|)"me=e-1 contained contains=@fstarAllErrs,fstarComment,fstarCommentLine,fstarModParam,fstarModTypeRestr,fstarModTRWith nextgroup=fstarModPreRHS syn region fstarModParam start="([^*]" end=")" contained contains=@fstarAENoParen,fstarModParam1,fstarVal syn match fstarModParam1 "\<\u\(\w\|'\)*\>" contained skipwhite skipempty nextgroup=fstarPreMPRestr From 0b09379c9b03bbd86fab276f49a3b908bbc622bb Mon Sep 17 00:00:00 2001 From: Max <5474655+maxzinkus@users.noreply.github.com> Date: Mon, 2 Dec 2019 18:10:42 -0500 Subject: [PATCH 3/3] Delete interactive functionality --- README.md | 47 +------- ftplugin/fstar-inter.py | 187 -------------------------------- ftplugin/fstar.vim | 86 --------------- syntax_checkers/fstar/fstar.vim | 53 --------- 4 files changed, 6 insertions(+), 367 deletions(-) delete mode 100644 ftplugin/fstar-inter.py delete mode 100644 ftplugin/fstar.vim delete mode 100644 syntax_checkers/fstar/fstar.vim diff --git a/README.md b/README.md index 14438f9..2d54bed 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,11 @@ -# VimFStar Interactive +# VimFStar -*VimFStar Interactive* is a [Vim] plugin for [F*], an [ML]-like language with a type system for program verification. +*VimFStar* provides filetype detection and syntax highlighting for [F*]. ## Features -- `.fst` file detection. +- `.fst[i]` file detection. - Syntax highlighting (based on [Vim's OCaml syntax file]). -- Interactive verification of code ## Installation @@ -27,48 +26,14 @@ If you're using [vim-plug], for example, perform the following steps to install 2. Restart Vim 3. `:PlugInstall` to install the plugin. -## Use of the interactive verification - -*Note: Interactive mode requires a Cygwin build of (g)Vim.* - -First, put ```fstar.exe``` in your $PATH. VimFStar will check that ```fstar.exe``` is present before loading interactive functions. - -To test your code and it to the environment up to the current position of the cursor, press `````` in normal mode. The marker ```v``` is set to the line just after the end of the checked part, so you can go there with ```'v```. If you already know that your code is correct until the cursor and just want to add it to the context, you can press `````` for a quick test (useful for projects with thousands of lines and where normal tests last very long). - -If you want to test some part of your code without adding it to the environment, select it in visual line mode (Shift+V) and press `````` - -If you want to get the result of the test you launched, press `````` in normal mode - -If you want to see again the errors sent by F*, press `````` - -If you are working on a big chunk of code, and it has no empty new line inside, you can try to select it quicker with `````` in order to check it with ``````. You can go back to where you were with `````` - -You can reset the interaction with the command ```:Freset``` in case something went wrong or if -you want to change a checked part. - -If you want to use library files and/or set options, use ```build-config``` in your file. For example, if my file is at ```$FSTAR_HOME/examples/metatheory``` and I want to use ```classical.fst``` and ```ext.fst``` in ```$FSTAR_HOME/lib``` and set some options, I will put the following code at the top of my file: - -```fstar -(*--build-config - options:--z3timeout 20 --max_fuel 8 --max_ifuel 6 --initial_fuel 4 --initial_ifuel 2; - other-files:../../lib/classical.fst ../../lib/ext.fst - --*) -``` - -This configuration is read when the buffer is loaded or when the plugin is reset. So do not forget to reset the plugin if you change `build-config`. +However, this may become redundant for users of `vim-polyglot` as the +contributors are seeking to include this in their bundle of supported file +types. ## License *VimFStar* is distributed under the same license as Vim itself. See [LICENSE] for more details. -## Planned Improvements - -- more accurate syntax highlighting. -- [syntastic] integration. -- better highlighting of verified code -- quick access to error locations -- ability to pop environment - [ML]:http://en.wikipedia.org/wiki/ML_(programming_language) [Vim]: http://www.vim.org [F*]: http://www.fstar-lang.org diff --git a/ftplugin/fstar-inter.py b/ftplugin/fstar-inter.py deleted file mode 100644 index 8c61002..0000000 --- a/ftplugin/fstar-inter.py +++ /dev/null @@ -1,187 +0,0 @@ -import sys -import re -import vim -from subprocess import PIPE,Popen -from threading import Thread -from Queue import Queue, Empty -fstarpath='fstar.exe' -fstarbusy=0 -fstarcurrentline=0 -fstarpotentialline=0 -fstarrequestline=0 -fstaranswer=None -fstarupdatehi=False -fstarmatch=None -fst=None -interout=None - -ON_POSIX = 'posix' in sys.builtin_module_names - -def fstar_reset_hi() : - global fstarmatch - if fstarmatch != None: - vim.command("call matchdelete("+str(fstarmatch)+")") - fstarmatch=None - return - -def fstar_add_hi(pos) : - global fstarmatch - if pos >= 1 : - fstarmatch=int(vim.eval("matchadd('FChecked','\\%<"+str(pos+1)+"l')")) - return - -def fstar_update_hi(newpos) : - fstar_reset_hi() - fstar_add_hi(newpos) - return - -def fstar_update_marker(newpos) : - vim.command('exe "normal! ' + str(newpos) + 'G1|mv\\"') - return - -#no waiting read as in http://stackoverflow.com/a/4896288/2598986 -def fstar_enqueue_output(out, queue): - for line in iter(out.readline, b''): - queue.put(line) - out.close() - -def fstar_readinter () : - global interout - try : line = interout.get_nowait() - except Empty : - return None - else : - return line - -def fstar_writeinter (s) : - global fst - fst.stdin.write(s) - -def fstar_init () : - global fst,interout - fst=Popen([fstarpath,'--in'],stdin=PIPE, stdout=PIPE,bufsize=1,close_fds=ON_POSIX) - interout=Queue() - t=Thread(target=fstar_enqueue_output,args=(fst.stdout,interout)) - t.daemon=True - t.start() - -def fstar_reset() : - global fstarbusy,fstarcurrentline,fstarpotentialline,fstaranswer,fstarupdatehi,fstarmatch - fstarbusy=0 - fstarcurrentline=0 - fstarpotentialline=0 - fstaranswer=None - fstarupdatehi=False - fstar_reset_hi() - fstar_init() - print 'Interaction reset' - - -def fstar_test_code (code,keep,quickcheck=False) : - global fstarbusy,fst - if fstarbusy == 1 : - return 'Already busy' - fstarbusy = 1 - fstar_writeinter('#push\n') - if quickcheck : - fstar_writeinter('#set-options "--admit_smt_queries true"\n') - fstar_writeinter(code) - fstar_writeinter('\n') - if quickcheck : - fstar_writeinter('#reset-options\n') - fstar_writeinter('#end\n') - if not keep : - fstar_writeinter('#pop\n') - return '' - -def fstar_convert_answer(ans) : - global fstarrequestline - res = re.match(r"\\((\d+)\,(\d+)\-(\d+)\,(\d+)\)\: (.*)",ans) - if res == None : - return ans - return '(%d,%s-%d,%s) : %s' % (int(res.group(1))+fstarrequestline-1,res.group(2),int(res.group(3))+fstarrequestline-1,res.group(4),res.group(5)) - -def fstar_gather_answer () : - global fstarbusy,fst,fstaranswer,fstarpotentialline,fstarcurrentline,fstarupdatehi - if fstarbusy == 0 : - return 'No verification pending' - line=fstar_readinter() - while line != None : - if line=='ok\n' : - fstarbusy=0 - fstarcurrentline=fstarpotentialline - if fstarupdatehi : - fstar_update_hi(fstarcurrentline) - fstar_update_marker(fstarcurrentline+1) - return 'Verification succeeded' - if line=='fail\n' : - fstarbusy=0 - fstarpotentialline=fstarcurrentline - return fstaranswer - fstaranswer+='\n'+fstar_convert_answer(line) - line=fstar_readinter() - return 'Busy' - -def fstar_vim_query_answer () : - r = fstar_gather_answer() - if r != None : - print r - -def fstar_get_range(firstl,lastl) : - lines = vim.eval("getline(%s,%s)"%(firstl,lastl)) - lines = lines + ["\n"] - code = "\n".join(lines) - return code - - -def fstar_get_selection () : - firstl = int(vim.eval("getpos(\"'<\")")[1]) - endl = int(vim.eval("getpos(\"'>\")")[1]) - lines = vim.eval("getline(%d,%d)"%(firstl,endl)) - lines = lines + ["\n"] - code = "\n".join(lines) - return code - - -def fstar_vim_test_code () : - global fstarrequestline, fstaranswer - global fstarupdatehi - if fstarbusy == 1 : - print 'Already busy' - return - fstaranswer='' - fstarrequestline = int(vim.eval("getpos(\"'<\")")[1]) - code = fstar_get_selection() - fstarupdatehi=False - fstar_test_code(code,False) - print 'Test of selected code launched' - -def fstar_vim_until_cursor (quick=False) : - global fstarcurrentline,fstarpotentialline,fstarrequestline,fstarupdatehi, fstaranswer - if fstarbusy == 1 : - print 'Already busy' - return - fstaranswer = '' - vimline = int(vim.eval("getpos(\".\")")[1]) - if vimline <= fstarcurrentline : - print 'Already checked' - return - firstl = fstarcurrentline+1 - fstarrequestline=firstl - endl = vimline - code = fstar_get_range(firstl,endl) - fstarpotentialline=endl - fstarupdatehi=True - fstar_test_code(code,True,quick) - if quick : - print 'Quick test until this point launched' - else : - print 'Test until this point launched' - -def fstar_vim_get_answer() : - global fstaranswer - print fstaranswer - -def fstar_get_current_line () : - global fstarcurrentline - print fstarcurrentline diff --git a/ftplugin/fstar.vim b/ftplugin/fstar.vim deleted file mode 100644 index 397c877..0000000 --- a/ftplugin/fstar.vim +++ /dev/null @@ -1,86 +0,0 @@ -if exists("b:did_ftplugin") - finish -endif -let b:did_ftplugin=1 - -let s:path = system("echo $PATH") -let s:jpath = substitute(s:path,":",",","g") -let s:jpath = substitute(s:jpath,"\n","","g") -let s:matchs = globpath(s:jpath,"fstar.exe") - -"Disable interactive feature -"let g:fstar_inter = 1 - -"Disable mappings -"let g:fstar_inter_maps = 1 - - -if !empty(s:matchs) && !exists('g:fstar_inter') - - let g:fstar_inter = 1 - pyfile :p:h/fstar-inter.py - - fu! Ftest_code () - py fstar_vim_test_code() - endfunction - - fu! Funtil_cursor() - py fstar_vim_until_cursor() - endfunction - - fu! Funtil_cursor_quick() - py fstar_vim_until_cursor(True) - endfunction - - fu! Fget_result() - py fstar_vim_query_answer() - endfunction - - fu! Freset() - py fstar_reset() - endfunction - - fu! Fget_answer() - py fstar_vim_get_answer() - endfunction - - py fstar_init() - - command Funtil call Funtil_cursor() - command Funtilquick call Funtil_cursor_quick() - command Fresult call Fget_result() - command Freset call Freset() - command Fanswer call Fget_answer() - - "Here you can set the color you want for checked code - highlight FChecked ctermbg=darkgrey guibg=lightGreen -endif - - -if !exists("g:fstar_inter_maps") - vnoremap :call Ftest_code() - nnoremap :call Funtil_cursor() - nnoremap :call Fget_result() - nnoremap :call Fget_answer() - nnoremap (v)k$ - nnoremap :call Funtil_cursor_quick() - " is to remove '<,'> which execute the command for each selected line -endif - - -" Add mappings, unless the user didn't want this. -if !exists("no_plugin_maps") && !exists("no_fstar_maps") - " (un)commenting - if !hasmapto('Comment') - nmap c LUncomOn - xmap c BUncomOn - nmap C LUncomOff - xmap C BUncomOff - endif - - nnoremap LUncomOn gI(* *) - nnoremap LUncomOff :s/^(\* \(.*\) \*)/\1/:noh - xnoremap BUncomOn :'<,'>`0i(*`>o0i*)`< - xnoremap BUncomOff :'<,'>`dd`< -endif - diff --git a/syntax_checkers/fstar/fstar.vim b/syntax_checkers/fstar/fstar.vim deleted file mode 100644 index 5338195..0000000 --- a/syntax_checkers/fstar/fstar.vim +++ /dev/null @@ -1,53 +0,0 @@ -" Syntastic syntax checker file -" Language: F* -" Filenames: *.fst -" Maintainers: Michael Lowell Roberts -" URL: http://research.microsoft.com/en-us/projects/fstar/ -" -" Distributed under the VIM LICENSE. Please refer to the LICENSE file or -" visit for details. - -if exists('g:loaded_syntastic_fstar_checker') - finish -endif -let g:loaded_syntastic_fstar_checker = 1 - -if !exists('g:syntastic_fstar_sort') - let g:syntastic_fstar_sort = 1 -endif - -let s:save_cpo = &cpo -set cpo&vim - -function! SyntaxCheckers_fstar_fstar_IsAvailable() dict -" Decho "self.getExec() => " . self.getExec() - return executable(self.getExec()) -endfunction - -"function! SyntaxCheckers_fstar_fstar_GetHighlightRegex(item) - "if match(a:item['text'], 'assigned but unused variable') > -1 - "let term = split(a:item['text'], ' - ')[1] - "return '\V\\<'.term.'\\>' - "endif - - "return '' -"endfunction - -function! SyntaxCheckers_fstar_fstar_GetLocList() dict - let makeprg = self.makeprgBuild({ - \ 'args': '', - \ 'args_after': '' }) - let errorformat = '\ %#%f(%l\\\,%c):\ %m' - let env = {} - return SyntasticMake({ 'makeprg': makeprg, 'errorformat': errorformat, 'env': env }) -endfunction - -call g:SyntasticRegistry.CreateAndRegisterChecker({ - \ 'filetype': 'fstar', - \ 'name': 'fstar', - \ 'exec': 'fstar' }) - -let &cpo = s:save_cpo -unlet s:save_cpo - -" vim: set sw=4 sts=4 et fdm=marker: