mirror of
https://github.com/sheerun/vim-polyglot.git
synced 2025-11-08 03:23:51 -05:00
Update
This commit is contained in:
Adam Stankiewicz
@@ -83,7 +83,7 @@ On top of all language packs from [vim repository](https://github.com/vim/vim/tr
|
||||
- [fsharp](https://github.com/ionide/Ionide-vim) (F# syntax highlighting for fs, fsi and fsx files)
|
||||
- [gdscript](https://github.com/calviken/vim-gdscript3) (GDScript syntax highlighting for gd files)
|
||||
- [git](https://github.com/tpope/vim-git) (Git Config syntax highlighting for gitconfig files)
|
||||
- [gitignore](https://github.com/fszymanski/fzf-gitignore)
|
||||
- [gitignore](https://github.com/SirJson/fzf-gitignore)
|
||||
- [gleam](https://github.com/gleam-lang/gleam.vim) (Syntax highlighting for gleam files)
|
||||
- [glsl](https://github.com/tikhomirov/vim-glsl) (GLSL syntax highlighting for glsl, fp, frag, frg, fs and 16 more files)
|
||||
- [gmpl](https://github.com/maelvalais/gmpl.vim) (Syntax highlighting for mod files)
|
||||
|
||||
@@ -1,34 +0,0 @@
|
||||
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2.vim')
|
||||
finish
|
||||
endif
|
||||
|
||||
" Invokes the solver on current file
|
||||
function! smt2#RunSolver()
|
||||
silent !clear
|
||||
execute "!" . g:smt2_solver_command . " " . bufname("%")
|
||||
endfunction
|
||||
|
||||
" Puts the solver's output in new split (replaces old split)
|
||||
function! smt2#RunSolverAndShowResult()
|
||||
let output = system(g:smt2_solver_command . " " . bufname("%") . " 2>&1")
|
||||
|
||||
" Create split (or reuse existent)
|
||||
if exists("s:outputbufnr") && bufwinnr(s:outputbufnr) > 0
|
||||
execute bufwinnr(s:outputbufnr) . 'wincmd w'
|
||||
else
|
||||
silent! vnew
|
||||
let s:outputbufnr=bufnr('%')
|
||||
endif
|
||||
|
||||
" Clear & (re-)fill contents
|
||||
silent! normal! ggdG
|
||||
setlocal filetype=smt2 buftype=nofile nobuflisted noswapfile
|
||||
call append(0, split(output, '\v\n'))
|
||||
normal! gg
|
||||
endfunction
|
||||
|
||||
" Requests the solver's version
|
||||
function! smt2#PrintSolverVersion()
|
||||
silent !clear
|
||||
execute "!" . g:smt2_solver_command . " " . g:smt2_solver_version_switch
|
||||
endfunction
|
||||
142
autoload/smt2/formatter.vim
Normal file
142
autoload/smt2/formatter.vim
Normal file
@@ -0,0 +1,142 @@
|
||||
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/formatter.vim')
|
||||
finish
|
||||
endif
|
||||
|
||||
" Formatting requires a rather recent Vim version
|
||||
if !((v:version > 802) || (v:version == 802 && has("patch2725")))
|
||||
const s:errmsg_oldvim = "Vim >= 8.2.2725 required for auto-formatting"
|
||||
|
||||
"Dummies
|
||||
function! smt2#formatter#FormatCurrentParagraph()
|
||||
echoerr s:errmsg_oldvim
|
||||
endfunction
|
||||
function! smt2#formatter#FormatAllParagraphs()
|
||||
echoerr s:errmsg_oldvim
|
||||
endfunction
|
||||
|
||||
finish
|
||||
endif
|
||||
vim9script
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Config
|
||||
# ------------------------------------------------------------------------------
|
||||
# Length of "short" S-expressions
|
||||
if !exists("g:smt2_formatter_short_length")
|
||||
g:smt2_formatter_short_length = 80
|
||||
endif
|
||||
|
||||
# String to use for indentation
|
||||
if !exists("g:smt2_formatter_indent_str")
|
||||
g:smt2_formatter_indent_str = ' '
|
||||
endif
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Formatter
|
||||
# ------------------------------------------------------------------------------
|
||||
def FitsOneLine(ast: dict<any>): bool
|
||||
# A paragraph with several entries should not be formatted in one line
|
||||
if ast.kind ==# 'Paragraph' && len(ast.value) != 1
|
||||
return false
|
||||
endif
|
||||
return ast.pos_to - ast.pos_from < g:smt2_formatter_short_length && !ast.contains_comment
|
||||
enddef
|
||||
|
||||
def FormatOneLine(ast: dict<any>): string
|
||||
if ast.kind ==# 'Atom'
|
||||
return ast.value.lexeme
|
||||
elseif ast.kind ==# 'SExpr'
|
||||
var formatted = []
|
||||
for expr in ast.value
|
||||
call formatted->add(expr->FormatOneLine())
|
||||
endfor
|
||||
return '(' .. formatted->join(' ') .. ')'
|
||||
elseif ast.kind ==# 'Paragraph'
|
||||
return ast.value[0]->FormatOneLine()
|
||||
endif
|
||||
throw 'Cannot format AST node: ' .. string(ast)
|
||||
return '' # Unreachable
|
||||
enddef
|
||||
|
||||
def Format(ast: dict<any>, indent = 0): string
|
||||
const indent_str = repeat(g:smt2_formatter_indent_str, indent)
|
||||
|
||||
if ast.kind ==# 'Atom'
|
||||
return indent_str .. ast.value.lexeme
|
||||
elseif ast.kind ==# 'SExpr'
|
||||
# Short expression -- avoid line breaks
|
||||
if ast->FitsOneLine()
|
||||
return indent_str .. ast->FormatOneLine()
|
||||
endif
|
||||
|
||||
# Long expression -- break lines and indent subexpressions.
|
||||
# Don't break before first subexpression if it's an atom
|
||||
# Note: ast.value->empty() == false; otherwise it would fit in one line
|
||||
var formatted = []
|
||||
if (ast.value[0].kind ==# 'Atom')
|
||||
call formatted->add(ast.value[0]->Format(0))
|
||||
else
|
||||
call formatted->add("\n" .. ast.value[0]->Format(indent + 1))
|
||||
endif
|
||||
for child in ast.value[1 :]
|
||||
call formatted->add(child->Format(indent + 1))
|
||||
endfor
|
||||
return indent_str .. "(" .. formatted->join("\n") .. ")"
|
||||
elseif ast.kind ==# 'Paragraph'
|
||||
var formatted = []
|
||||
for child in ast.value
|
||||
call formatted->add(child->Format())
|
||||
endfor
|
||||
return formatted->join("\n")
|
||||
endif
|
||||
throw 'Cannot format AST node: ' .. string(ast)
|
||||
return '' # Unreachable
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Public functions
|
||||
# ------------------------------------------------------------------------------
|
||||
def smt2#formatter#FormatCurrentParagraph()
|
||||
const cursor = getpos('.')
|
||||
const ast = smt2#parser#ParseCurrentParagraph()
|
||||
|
||||
# Identify on which end of the buffer we are (to fix newlines later)
|
||||
silent! normal! {
|
||||
const is_first_paragraph = line('.') == 1
|
||||
silent! normal! }
|
||||
const is_last_paragraph = line('.') == line('$')
|
||||
|
||||
# Replace paragraph by formatted lines
|
||||
const lines = split(Format(ast), '\n')
|
||||
silent! normal! {d}
|
||||
if is_last_paragraph && !is_first_paragraph
|
||||
call append('.', [''] + lines)
|
||||
else
|
||||
call append('.', lines + [''])
|
||||
endif
|
||||
|
||||
# Remove potentially introduced first empty line
|
||||
if is_first_paragraph | silent! :1delete | endif
|
||||
|
||||
# Restore cursor position
|
||||
call setpos('.', cursor)
|
||||
enddef
|
||||
|
||||
def smt2#formatter#FormatAllParagraphs()
|
||||
const cursor = getpos('.')
|
||||
const asts = smt2#parser#ParseAllParagraphs()
|
||||
|
||||
# Clear buffer & insert formatted paragraphs
|
||||
silent! :1,$delete
|
||||
for ast in asts
|
||||
const lines = split(Format(ast), '\n') + ['']
|
||||
call append('$', lines)
|
||||
endfor
|
||||
|
||||
# Remove first & trailing empty lines
|
||||
silent! :1delete
|
||||
silent! :$delete
|
||||
|
||||
# Restore cursor position
|
||||
call setpos('.', cursor)
|
||||
enddef
|
||||
227
autoload/smt2/parser.vim
Normal file
227
autoload/smt2/parser.vim
Normal file
@@ -0,0 +1,227 @@
|
||||
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/parser.vim')
|
||||
finish
|
||||
endif
|
||||
|
||||
vim9script
|
||||
const debug = false
|
||||
set maxfuncdepth=100000000 # SMT files tend to be highly nested
|
||||
|
||||
# TODO: Retry iterative parsing now that we have a scanner and simpler grammar
|
||||
# TODO: Refer to token kind by name, e.g. token_comment instead of 8
|
||||
# TODO: Change Ast.kind type from string to enum/number?
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# AST nodes -- essentially named token wrappers
|
||||
#
|
||||
# Note: pos_from, pos_to and contains_comment were only introduced to allow for
|
||||
# a fast FitsOneLine(ast) function in the formatter.
|
||||
# Here, pos_from and pos_to refer to indices of characters -- not tokens
|
||||
# ------------------------------------------------------------------------------
|
||||
def Ast(kind: string, value: any, pos_from: number, pos_to: number, contains_comment: bool): dict<any>
|
||||
return {kind: kind, value: value, pos_from: pos_from, pos_to: pos_to, contains_comment: contains_comment}
|
||||
enddef
|
||||
|
||||
def ParagraphAst(exprs: list<dict<any>>, pos_from: number, pos_to: number): dict<any>
|
||||
var contains_comment = false
|
||||
for expr in exprs
|
||||
if expr.contains_comment
|
||||
contains_comment = true
|
||||
break
|
||||
endif
|
||||
endfor
|
||||
return Ast('Paragraph', exprs, pos_from, pos_to, contains_comment)
|
||||
enddef
|
||||
|
||||
def SExprAst(exprs: list<dict<any>>, pos_from: number, pos_to: number): dict<any>
|
||||
var contains_comment = false
|
||||
for expr in exprs
|
||||
if expr.contains_comment
|
||||
contains_comment = true
|
||||
break
|
||||
endif
|
||||
endfor
|
||||
return Ast('SExpr', exprs, pos_from, pos_to, contains_comment)
|
||||
enddef
|
||||
|
||||
def AtomAst(token: dict<any>): dict<any>
|
||||
return Ast('Atom', token, token.pos, token.pos + len(token.lexeme), token.kind == 8)
|
||||
enddef
|
||||
|
||||
def PrintAst(ast: dict<any>, indent = 0)
|
||||
echo repeat(' ', indent * 2) .. '[' .. ast.kind .. '] '
|
||||
|
||||
if ast.kind ==# 'Atom'
|
||||
echon ast.value.lexeme
|
||||
elseif ast.kind ==# 'SExpr'
|
||||
for v in ast.value
|
||||
call PrintAst(v, indent + 1)
|
||||
endfor
|
||||
elseif ast.kind ==# 'Paragraph'
|
||||
for v in ast.value
|
||||
call PrintAst(v, indent + 1)
|
||||
endfor
|
||||
endif
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Grammar
|
||||
# ------------------------------------------------------------------------------
|
||||
# Paragraph ::= Expr+
|
||||
# Expr ::= SExpr | Atom
|
||||
# SExpr ::= '(' Expr* ')'
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# LParen
|
||||
# ------------------------------------------------------------------------------
|
||||
def AtStartOfLParen(scanner: dict<any>): bool
|
||||
return scanner.cur_token.kind == 0 # token_lparen
|
||||
enddef
|
||||
|
||||
def ParseLParen(scanner: dict<any>) # consumes token; no return
|
||||
if debug
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfLParen(),
|
||||
"ParseLParen called but not at start of LParen",
|
||||
scanner.cur_token.pos)
|
||||
endif
|
||||
|
||||
scanner->smt2#scanner#NextToken()
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# RParen
|
||||
# ------------------------------------------------------------------------------
|
||||
def AtStartOfRParen(scanner: dict<any>): bool
|
||||
return scanner.cur_token.kind == 1 # token_rparen
|
||||
enddef
|
||||
|
||||
def ParseRParen(scanner: dict<any>) # consumes token; no return
|
||||
if debug
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfRParen(),
|
||||
"ParseRParen called but not at start of RParen",
|
||||
scanner.cur_token.pos)
|
||||
endif
|
||||
|
||||
scanner->smt2#scanner#NextToken()
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Atom
|
||||
# ------------------------------------------------------------------------------
|
||||
def AtStartOfAtom(scanner: dict<any>): bool
|
||||
return 2 <= scanner.cur_token.kind && scanner.cur_token.kind <= 8
|
||||
enddef
|
||||
|
||||
def ParseAtom(scanner: dict<any>): dict<any>
|
||||
if debug
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfAtom(),
|
||||
"ParseAtom called but not at start of Atom",
|
||||
scanner.cur_token.pos)
|
||||
endif
|
||||
|
||||
const ast = AtomAst(scanner.cur_token)
|
||||
scanner->smt2#scanner#NextToken()
|
||||
return ast
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Expr
|
||||
# ------------------------------------------------------------------------------
|
||||
def AtStartOfExpr(scanner: dict<any>): bool
|
||||
return scanner->AtStartOfSExpr() || scanner->AtStartOfAtom()
|
||||
enddef
|
||||
def ParseExpr(scanner: dict<any>): dict<any>
|
||||
if debug
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfExpr(),
|
||||
"ParseExpr called but not at start of Expr",
|
||||
scanner.cur_token.pos)
|
||||
endif
|
||||
|
||||
if scanner->AtStartOfSExpr()
|
||||
return scanner->ParseSExpr()
|
||||
endif
|
||||
return scanner->ParseAtom()
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# SExpr
|
||||
# ------------------------------------------------------------------------------
|
||||
const AtStartOfSExpr = funcref(AtStartOfLParen)
|
||||
def ParseSExpr(scanner: dict<any>): dict<any>
|
||||
const pos_from = scanner.cur_token.pos
|
||||
|
||||
if debug
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfSExpr(),
|
||||
"ParseSExpr called but not at start of SExpr",
|
||||
pos_from)
|
||||
endif
|
||||
scanner->ParseLParen()
|
||||
|
||||
# Expr*
|
||||
var exprs: list<any>
|
||||
while scanner->AtStartOfExpr()
|
||||
exprs->add(scanner->ParseExpr())
|
||||
endwhile
|
||||
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfRParen(),
|
||||
printf("Expected RParen but got %s", scanner.cur_token.kind->smt2#scanner#TokenKind2Str()),
|
||||
scanner.cur_token.pos)
|
||||
scanner->ParseRParen()
|
||||
|
||||
const pos_to = scanner.cur_token.pos
|
||||
return SExprAst(exprs, pos_from, pos_to)
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Paragraph
|
||||
# ------------------------------------------------------------------------------
|
||||
def ParseParagraph(scanner: dict<any>): dict<any>
|
||||
const pos_from = scanner.cur_token.pos
|
||||
|
||||
# Expr+
|
||||
scanner->smt2#scanner#Enforce(scanner->AtStartOfExpr(),
|
||||
printf("Expected Expr but got %s", scanner.cur_token.kind->smt2#scanner#TokenKind2Str()),
|
||||
pos_from)
|
||||
|
||||
var exprs = [scanner->ParseExpr()]
|
||||
while scanner->AtStartOfExpr() && !scanner.at_new_paragraph
|
||||
exprs->add(scanner->ParseExpr())
|
||||
endwhile
|
||||
|
||||
const pos_to = scanner.cur_token.pos
|
||||
return ParagraphAst(exprs, pos_from, pos_to)
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Public functions
|
||||
# ------------------------------------------------------------------------------
|
||||
def smt2#parser#ParseCurrentParagraph(): dict<any>
|
||||
# source = [start of current paragraph, EOF]
|
||||
# Note: This is needed since `silent! normal! {y}` may not yank full paragraphs
|
||||
# in the context of multiline expressions
|
||||
const cursor = getpos('.')
|
||||
silent! normal! {
|
||||
const line_offset = line('.')
|
||||
const source = join(getline('.', '$'), "\n")
|
||||
call setpos('.', cursor)
|
||||
|
||||
var scanner = smt2#scanner#Scanner(source, line_offset)
|
||||
const ast = scanner->ParseParagraph()
|
||||
|
||||
if debug | ast->PrintAst() | endif
|
||||
return ast
|
||||
enddef
|
||||
|
||||
def smt2#parser#ParseAllParagraphs(): list<dict<any>>
|
||||
# source = current buffer
|
||||
const source = join(getline(1, '$'), "\n")
|
||||
|
||||
var scanner = smt2#scanner#Scanner(source)
|
||||
var asts = []
|
||||
while scanner.cur_token.kind != 9 # token_eof
|
||||
const ast = scanner->ParseParagraph()
|
||||
asts->add(ast)
|
||||
|
||||
if debug | ast->PrintAst() | endif
|
||||
endwhile
|
||||
return asts
|
||||
enddef
|
||||
381
autoload/smt2/scanner.vim
Normal file
381
autoload/smt2/scanner.vim
Normal file
@@ -0,0 +1,381 @@
|
||||
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/scanner.vim')
|
||||
finish
|
||||
endif
|
||||
|
||||
vim9script
|
||||
const debug = false
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Ref: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
|
||||
# ------------------------------------------------------------------------------
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Token
|
||||
# ------------------------------------------------------------------------------
|
||||
const token_lparen = 0
|
||||
const token_rparen = 1
|
||||
const token_numeral = 2
|
||||
const token_decimal = 3
|
||||
const token_bv = 4
|
||||
const token_string = 5
|
||||
const token_symbol = 6
|
||||
const token_keyword = 7
|
||||
const token_comment = 8
|
||||
const token_eof = 9
|
||||
|
||||
def Token(kind: number, pos: number, lexeme: string): dict<any>
|
||||
return {kind: kind, pos: pos, lexeme: lexeme}
|
||||
enddef
|
||||
|
||||
def smt2#scanner#TokenKind2Str(kind: number): string
|
||||
if kind == token_lparen
|
||||
return "LParen"
|
||||
elseif kind == token_rparen
|
||||
return "RParen"
|
||||
elseif kind == token_numeral
|
||||
return "Numeral"
|
||||
elseif kind == token_decimal
|
||||
return "Decimal"
|
||||
elseif kind == token_bv
|
||||
return "Bv"
|
||||
elseif kind == token_string
|
||||
return "String"
|
||||
elseif kind == token_symbol
|
||||
return "Symbol"
|
||||
elseif kind == token_keyword
|
||||
return "Keyword"
|
||||
elseif kind == token_comment
|
||||
return "Comment"
|
||||
elseif kind == token_eof
|
||||
return "EOF"
|
||||
else
|
||||
echoerr "Unexpected token kind: " .. kind
|
||||
return ''
|
||||
endif
|
||||
enddef
|
||||
|
||||
def PrettyPrint(scanner: dict<any>, token: dict<any>)
|
||||
const coord = scanner->Pos2Coord(token.pos)
|
||||
echo printf("%4d:%-3d (%5d) %8s %s", coord.line, coord.col, token.pos, token.kind->smt2#scanner#TokenKind2Str(), token.lexeme)
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# Scanner
|
||||
#
|
||||
# Note: The public interface is limited to the
|
||||
# - field cur_token
|
||||
# - method NextToken
|
||||
# - field at_new_paragraph (needed to distinguish paragraphs in parser)
|
||||
#
|
||||
# The other fields should only be used internally / in this file
|
||||
# ------------------------------------------------------------------------------
|
||||
# TODO: Enforce restriction to ASCII? We should if we use the lookup table below
|
||||
# TODO: Do not take a string but a character stream (or just buffer and pos)?
|
||||
|
||||
def smt2#scanner#Scanner(source: string, line_offset = 1): dict<any>
|
||||
var scanner = {
|
||||
chars: source->trim(" \t\n\r", 2)->split('\zs'),
|
||||
line_offset: line_offset, # start line of source string in buffer
|
||||
pos: 0, # pos in source string -- not column in line
|
||||
at_new_paragraph: false}
|
||||
|
||||
if scanner.chars->empty()
|
||||
scanner.at_eof = true
|
||||
scanner.cur_char = ''
|
||||
else
|
||||
scanner.at_eof = false
|
||||
scanner.cur_char = scanner.chars[0]
|
||||
endif
|
||||
scanner.cur_char_nr = scanner.cur_char->char2nr()
|
||||
scanner.chars_len = len(scanner.chars)
|
||||
scanner.cur_token = {}
|
||||
scanner->smt2#scanner#NextToken()
|
||||
return scanner
|
||||
enddef
|
||||
|
||||
def smt2#scanner#NextToken(scanner: dict<any>)
|
||||
if scanner.at_eof
|
||||
scanner.cur_token = Token(token_eof, scanner.pos, '')
|
||||
else
|
||||
scanner->SkipWhitespace() # Cannot end up at eof since end is trimmed
|
||||
|
||||
const nr = scanner.cur_char_nr
|
||||
if nr == 40 # '('
|
||||
scanner.cur_token = Token(token_lparen, scanner.pos, '(')
|
||||
scanner->NextPos()
|
||||
elseif nr == 41 # ')'
|
||||
scanner.cur_token = Token(token_rparen, scanner.pos, ')')
|
||||
scanner->NextPos()
|
||||
elseif nr->IsStartOfSimpleSymbol()
|
||||
scanner.cur_token = scanner->ReadSimpleSymbol()
|
||||
elseif nr == 124 # '|'
|
||||
scanner.cur_token = scanner->ReadQuotedSymbol()
|
||||
elseif nr == 58 # ':'
|
||||
scanner.cur_token = scanner->ReadKeyword()
|
||||
elseif nr->IsDigit()
|
||||
scanner.cur_token = scanner->ReadNumber()
|
||||
elseif nr == 35 # '#'
|
||||
scanner.cur_token = scanner->ReadBv()
|
||||
elseif nr == 34 # '"'
|
||||
scanner.cur_token = scanner->ReadString()
|
||||
elseif nr == 59 # ';'
|
||||
scanner.cur_token = scanner->ReadComment()
|
||||
else
|
||||
scanner->smt2#scanner#Enforce(false, printf("Unexpected character '%s'", scanner.cur_char), scanner.pos)
|
||||
endif
|
||||
endif
|
||||
|
||||
if debug
|
||||
if scanner.at_new_paragraph | echo "\n" | endif
|
||||
scanner->PrettyPrint(scanner.cur_token)
|
||||
endif
|
||||
enddef
|
||||
|
||||
def NextPos(scanner: dict<any>)
|
||||
if debug | scanner->smt2#scanner#Enforce(!scanner.at_eof, "Already at EOF", scanner.pos) | endif
|
||||
|
||||
scanner.pos += 1
|
||||
scanner.at_eof = scanner.pos == scanner.chars_len
|
||||
scanner.cur_char = scanner.at_eof ? '' : scanner.chars[scanner.pos]
|
||||
scanner.cur_char_nr = scanner.cur_char->char2nr()
|
||||
enddef
|
||||
|
||||
def smt2#scanner#Enforce(scanner: dict<any>, expr: bool, msg: string, pos: number)
|
||||
if !expr
|
||||
const coord = scanner->Pos2Coord(pos)
|
||||
throw printf("Syntax error (at %d:%d): %s ", coord.line, coord.col, msg)
|
||||
endif
|
||||
enddef
|
||||
|
||||
# This is slow and intended for use in error messages & debugging only
|
||||
def Pos2Coord(scanner: dict<any>, pos: number): dict<number>
|
||||
const line = scanner.chars[: pos]->count("\n") + scanner.line_offset
|
||||
|
||||
var cur_pos = pos - 1
|
||||
while cur_pos >= 0 && scanner.chars[cur_pos] != "\n"
|
||||
cur_pos -= 1
|
||||
endwhile
|
||||
|
||||
return {line: line, col: pos - cur_pos}
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <white_space_char> ::= 9 (tab), 10 (lf), 13 (cr), 32 (space)
|
||||
#
|
||||
# Note: The source string has all lines joined by "\n" so "\r" can be ignored
|
||||
# ------------------------------------------------------------------------------
|
||||
def SkipWhitespace(scanner: dict<any>)
|
||||
var newlines = 0
|
||||
while !scanner.at_eof
|
||||
const nr = scanner.cur_char_nr
|
||||
if nr == 32 || nr == 9
|
||||
scanner->NextPos()
|
||||
elseif nr == 10
|
||||
newlines += 1
|
||||
scanner->NextPos()
|
||||
else
|
||||
break
|
||||
endif
|
||||
endwhile
|
||||
scanner.at_new_paragraph = newlines > 1
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# A comment is any character sequence not contained within a string literal or a
|
||||
# quoted symbol that begins with ; and ends with the first subsequent
|
||||
# line-breaking character, i.e. 10 (lf) or 13 (cr)
|
||||
#
|
||||
# Note: The source string has all lines joined by "\n" so "\r" can be ignored
|
||||
# ------------------------------------------------------------------------------
|
||||
def ReadComment(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == ';', "Not the start of a comment", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
while !scanner.at_eof && scanner.cur_char_nr != 10
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
return Token(token_comment, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <numeral> ::= 0
|
||||
# | a non-empty sequence of digits not starting with 0
|
||||
#
|
||||
# <decimal> ::= <numeral>.0*<numeral>
|
||||
# ------------------------------------------------------------------------------
|
||||
def IsDigit(char_nr: number): bool
|
||||
# '0'->char2nr() == 48 && '9'->char2nr() == 57
|
||||
return 48 <= char_nr && char_nr <= 57
|
||||
enddef
|
||||
|
||||
def ReadNumber(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char_nr->IsDigit(), "Not the start of a number", scanner.pos) | endif
|
||||
|
||||
const starts_with_zero = scanner.cur_char == '0'
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
# Note: We aren't strict about numbers not starting with 0 when not debugging
|
||||
if debug | scanner->smt2#scanner#Enforce(!starts_with_zero || scanner.cur_char != '0', "Numeral may not start with 0", scanner.pos) | endif
|
||||
|
||||
var is_decimal = false
|
||||
while !scanner.at_eof
|
||||
const nr = scanner.cur_char_nr
|
||||
if 48 <= nr && nr <= 57 # inlined IsDigit
|
||||
scanner->NextPos()
|
||||
elseif scanner.cur_char == '.'
|
||||
if is_decimal
|
||||
break
|
||||
else
|
||||
is_decimal = true
|
||||
scanner->NextPos()
|
||||
endif
|
||||
else
|
||||
break
|
||||
endif
|
||||
endwhile
|
||||
const kind = is_decimal ? token_decimal : token_numeral
|
||||
return Token(kind, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <hexadecimal> ::= #x followed by a non-empty sequence of digits and letters
|
||||
# from A to F, capitalized or not
|
||||
#
|
||||
# <binary> ::= #b followed by a non-empty sequence of 0 and 1 characters
|
||||
# ------------------------------------------------------------------------------
|
||||
|
||||
# Build lookup table for char->match('\m\C^[0-9a-fA-F]')
|
||||
def InitIsAlphaNumericCharNr(): list<bool>
|
||||
var lookup_table = []
|
||||
var char_nr = 0
|
||||
while char_nr < 255
|
||||
lookup_table->add(char_nr->nr2char()->match('\m\C^[0-9a-fA-F]') != -1)
|
||||
char_nr += 1
|
||||
endwhile
|
||||
return lookup_table
|
||||
enddef
|
||||
const is_alphanumeric_char_nr = InitIsAlphaNumericCharNr()
|
||||
|
||||
def ReadBv(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '#', "Not the start of a bit vector literal", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
if scanner.cur_char == 'x'
|
||||
scanner->NextPos()
|
||||
scanner->smt2#scanner#Enforce(!scanner.at_eof && is_alphanumeric_char_nr[scanner.cur_char_nr],
|
||||
"hexadecimal literal may not be empty",
|
||||
scanner.pos)
|
||||
while !scanner.at_eof && is_alphanumeric_char_nr[scanner.cur_char_nr]
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
elseif scanner.cur_char == 'b'
|
||||
scanner->NextPos()
|
||||
# '0'->char2nr() == 48 && '1'->char2nr() == 49
|
||||
scanner->smt2#scanner#Enforce(!scanner.at_eof && scanner.cur_char_num == 48 || scanner.cur_char_num == 49,
|
||||
"binary literal may not be empty",
|
||||
scanner.pos)
|
||||
while !scanner.at_eof && scanner.cur_char_num == 48 || scanner.cur_char_num == 49
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
else
|
||||
scanner->smt2#scanner#Enforce(false, "invalid bit vector literal -- expected 'x' or 'b'", scanner.pos)
|
||||
endif
|
||||
return Token(token_bv, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <string> ::= sequence of whitespace and printable characters in double
|
||||
# quotes with escape sequence ""
|
||||
# ------------------------------------------------------------------------------
|
||||
# TODO: Allow only printable characters, i.e. ranges [32, 126], [128-255]?
|
||||
def ReadString(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '"', "Not the start of a string", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
while true
|
||||
scanner->smt2#scanner#Enforce(!scanner.at_eof, "unexpected end of string", scanner.pos)
|
||||
|
||||
if scanner.cur_char == '"'
|
||||
scanner->NextPos()
|
||||
if scanner.cur_char != '"'
|
||||
break
|
||||
endif
|
||||
endif
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
return Token(token_string, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <simple symbol> ::= a non-empty sequence of letters, digits and the characters
|
||||
# + - / * = % ? ! . $ _ ~ & ^ < > @ that does not start with
|
||||
# a digit
|
||||
# ------------------------------------------------------------------------------
|
||||
|
||||
# Build lookup table for char->match('\m\C^[a-zA-Z0-9+-/*=%?!.$_~&^<>@]')
|
||||
def InitIsSimpleSymbolCharNr(): list<bool>
|
||||
var lookup_table = []
|
||||
var char_nr = 0
|
||||
while char_nr < 255
|
||||
lookup_table->add(char_nr->nr2char()->match('\m\C^[a-zA-Z0-9+-/*=%?!.$_~&^<>@]') != -1)
|
||||
char_nr += 1
|
||||
endwhile
|
||||
return lookup_table
|
||||
enddef
|
||||
const is_simple_symbol_char_nr = InitIsSimpleSymbolCharNr()
|
||||
|
||||
def IsStartOfSimpleSymbol(char_nr: number): bool
|
||||
# '0'->char2nr() == 48 && '9'->char2nr() == 57
|
||||
return is_simple_symbol_char_nr[char_nr] && !(48 <= char_nr && char_nr <= 57)
|
||||
enddef
|
||||
|
||||
def ReadSimpleSymbol(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char_nr->IsStartOfSimpleSymbol(), "Not the start of a simple symbol", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
while !scanner.at_eof && is_simple_symbol_char_nr[scanner.cur_char_nr]
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
return Token(token_symbol, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <symbol> ::= <simple symbol>
|
||||
# | a sequence of whitespace and printable characters that starts
|
||||
# and ends with '|' and does not otherwise include '|' or '\'
|
||||
# ------------------------------------------------------------------------------
|
||||
# TODO: Allow only printable characters, i.e. ranges [32, 126], [128-255]?
|
||||
def ReadQuotedSymbol(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == '|', "Not the start of a quoted symbol", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
while true
|
||||
scanner->smt2#scanner#Enforce(!scanner.at_eof, "unexpected end of quoted symbol", scanner.pos)
|
||||
scanner->smt2#scanner#Enforce(scanner.cur_char != '\\', "quoted symbol may not contain '\'", scanner.pos)
|
||||
if scanner.cur_char == '|'
|
||||
break
|
||||
endif
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
scanner->NextPos()
|
||||
return Token(token_symbol, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
|
||||
# ------------------------------------------------------------------------------
|
||||
# <keyword> ::= :<simple symbol>
|
||||
# ------------------------------------------------------------------------------
|
||||
def ReadKeyword(scanner: dict<any>): dict<any>
|
||||
if debug | scanner->smt2#scanner#Enforce(scanner.cur_char == ':', "Not the start of a keyword", scanner.pos) | endif
|
||||
|
||||
const start_pos = scanner.pos
|
||||
scanner->NextPos()
|
||||
while !scanner.at_eof && is_simple_symbol_char_nr[scanner.cur_char_nr]
|
||||
scanner->NextPos()
|
||||
endwhile
|
||||
return Token(token_keyword, start_pos, scanner.chars[start_pos : scanner.pos - 1]->join(''))
|
||||
enddef
|
||||
56
autoload/smt2/solver.vim
Normal file
56
autoload/smt2/solver.vim
Normal file
@@ -0,0 +1,56 @@
|
||||
if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'autoload/smt2/solver.vim')
|
||||
finish
|
||||
endif
|
||||
|
||||
" ------------------------------------------------------------------------------
|
||||
" Config
|
||||
" ------------------------------------------------------------------------------
|
||||
" If no command for invoking a solver is specified in ~/.vimrc, test if either
|
||||
" 'z3' or 'boolector' is accessible through $PATH (in that order)
|
||||
if !exists("g:smt2_solver_command")
|
||||
if executable("z3")
|
||||
let g:smt2_solver_command = "z3"
|
||||
elseif executable("boolector")
|
||||
let g:smt2_solver_command = "boolector"
|
||||
endif
|
||||
endif
|
||||
|
||||
" If no command line switch for printing the solver's version is specified in
|
||||
" ~/.vimrc, use '--version'
|
||||
if !exists("g:smt2_solver_version_switch")
|
||||
let g:smt2_solver_version_switch = "--version"
|
||||
endif
|
||||
|
||||
" ------------------------------------------------------------------------------
|
||||
" Public functions
|
||||
" ------------------------------------------------------------------------------
|
||||
" Invokes the solver on current file
|
||||
function! smt2#solver#Run()
|
||||
silent !clear
|
||||
execute "!" . g:smt2_solver_command . " " . bufname("%")
|
||||
endfunction
|
||||
|
||||
" Puts the solver's output in new split (replaces old split)
|
||||
function! smt2#solver#RunAndShowResult()
|
||||
let output = system(g:smt2_solver_command . " " . bufname("%") . " 2>&1")
|
||||
|
||||
" Create split (or reuse existent)
|
||||
if exists("s:outputbufnr") && bufwinnr(s:outputbufnr) > 0
|
||||
execute bufwinnr(s:outputbufnr) . 'wincmd w'
|
||||
else
|
||||
silent! vnew
|
||||
let s:outputbufnr=bufnr('%')
|
||||
endif
|
||||
|
||||
" Clear & (re-)fill contents
|
||||
silent! normal! ggdG
|
||||
setlocal filetype=smt2 buftype=nofile nobuflisted noswapfile
|
||||
call append(0, split(output, '\v\n'))
|
||||
normal! gg
|
||||
endfunction
|
||||
|
||||
" Requests the solver's version
|
||||
function! smt2#solver#PrintVersion()
|
||||
silent !clear
|
||||
execute "!" . g:smt2_solver_command . " " . g:smt2_solver_version_switch
|
||||
endfunction
|
||||
@@ -1496,7 +1496,7 @@ au BufNewFile,BufRead *.sass setf sass
|
||||
au BufNewFile,BufRead *.sa setf sather
|
||||
|
||||
" Scala
|
||||
au BufNewFile,BufRead *.scala setf scala
|
||||
au BufNewFile,BufRead *.scala,*.sc setf scala
|
||||
|
||||
" SBT - Scala Build Tool
|
||||
au BufNewFile,BufRead *.sbt setf sbt
|
||||
|
||||
@@ -33,7 +33,7 @@ endif
|
||||
function! DhallFormat()
|
||||
let cursor = getpos('.')
|
||||
exec 'normal! gg'
|
||||
exec 'silent !dhall format --inplace ' . expand('%')
|
||||
exec 'silent !dhall format ' . expand('%')
|
||||
exec 'e'
|
||||
call setpos('.', cursor)
|
||||
endfunction
|
||||
|
||||
@@ -39,7 +39,7 @@ if exists("loaded_matchit")
|
||||
" for nested-structures-skipping to work properly
|
||||
" note: 'mutable struct' and 'struct' are defined separately because
|
||||
" using \? puts the cursor on 'struct' instead of 'mutable' for some reason
|
||||
let b:julia_begin_keywords = '\%(\%(\.\s*\)\@<!\|\%(@\s*.\s*\)\@<=\)\<\%(function\|macro\|begin\|mutable\s\+struct\|\%(mutable\s\+\)\@<!struct\|\%(abstract\|primitive\)\s\+type\|let\|do\|\%(bare\)\?module\|quote\|if\|for\|while\|try\)\>'
|
||||
let b:julia_begin_keywords = '\%(\.\s*\|@\)\@<!\<\%(function\|macro\|begin\|mutable\s\+struct\|\%(mutable\s\+\)\@<!struct\|\%(abstract\|primitive\)\s\+type\|let\|do\|\%(bare\)\?module\|quote\|if\|for\|while\|try\)\>'
|
||||
" note: the following regex not only recognizes macros, but also local/global keywords.
|
||||
" the purpose is recognizing things like `@inline myfunction()`
|
||||
" or `global myfunction(...)` etc, for matchit and block movement functionality
|
||||
@@ -67,7 +67,7 @@ if exists("loaded_matchit")
|
||||
call cursor(l, c)
|
||||
if attr == 'juliaConditional'
|
||||
return b:julia_begin_keywordsm . ':\<\%(elseif\|else\)\>:' . b:julia_end_keywords
|
||||
elseif attr =~ '\<\%(juliaRepeat\|juliaRepKeyword\)\>'
|
||||
elseif attr =~# '\<\%(juliaRepeat\|juliaRepKeyword\)\>'
|
||||
return b:julia_begin_keywordsm . ':\<\%(break\|continue\)\>:' . b:julia_end_keywords
|
||||
elseif attr == 'juliaBlKeyword'
|
||||
return b:julia_begin_keywordsm . ':' . b:julia_end_keywords
|
||||
@@ -82,8 +82,8 @@ if exists("loaded_matchit")
|
||||
" we need to skip everything within comments, strings and
|
||||
" the 'begin' and 'end' keywords when they are used as a range rather than as
|
||||
" the delimiter of a block
|
||||
let b:match_skip = 'synIDattr(synID(line("."),col("."),1),"name") =~ '
|
||||
\ . '"\\<julia\\%(Comprehension\\%(For\\|If\\)\\|RangeKeyword\\|Comment\\%([LM]\\|Delim\\)\\|\\%([bs]\\|Shell\\|Printf\\|Doc\\)\\?String\\|StringPrefixed\\|DocStringM\\(Raw\\)\\?\\|RegEx\\|SymbolS\\?\\|Macro\\|Dotted\\)\\>"'
|
||||
let b:match_skip = 'synIDattr(synID(line("."),col("."),0),"name") =~# '
|
||||
\ . '"\\<julia\\%(Comprehension\\%(For\\|If\\)\\|RangeKeyword\\|Comment\\%([LM]\\|Delim\\)\\|\\%([bs]\\|Shell\\|Printf\\|Doc\\)\\?String\\|StringPrefixed\\|DocStringM\\(Raw\\)\\?\\|RegEx\\|SymbolS\\?\\|Dotted\\)\\>"'
|
||||
|
||||
let b:undo_ftplugin = b:undo_ftplugin
|
||||
\ . " | unlet! b:match_words b:match_skip b:match_ignorecase"
|
||||
|
||||
@@ -3,27 +3,13 @@ if polyglot#init#is_disabled(expand('<sfile>:p'), 'smt2', 'ftplugin/smt2.vim')
|
||||
endif
|
||||
|
||||
setlocal iskeyword+=-,:,#,',$
|
||||
|
||||
" If no command for invoking a solver is specified in ~/.vimrc, test if either
|
||||
" 'z3' or 'boolector' is accessible through $PATH (in that order)
|
||||
if !exists("g:smt2_solver_command")
|
||||
if executable("z3")
|
||||
let g:smt2_solver_command = "z3"
|
||||
elseif executable("boolector")
|
||||
let g:smt2_solver_command = "boolector"
|
||||
endif
|
||||
endif
|
||||
|
||||
" If no command line switch for printing the solver's version is specified in
|
||||
" ~/.vimrc, use '--version'
|
||||
if !exists("g:smt2_solver_version_switch")
|
||||
let g:smt2_solver_version_switch = "--version"
|
||||
endif
|
||||
|
||||
" Mappings
|
||||
nnoremap <silent> <buffer> <localleader>r :call smt2#RunSolver()<cr>
|
||||
nnoremap <silent> <buffer> <localleader>R :call smt2#RunSolverAndShowResult()<cr>
|
||||
nnoremap <silent> <buffer> <localleader>v :call smt2#PrintSolverVersion()<cr>
|
||||
|
||||
" Comment String
|
||||
setlocal commentstring=;%s
|
||||
|
||||
" Mappings for solver functionality
|
||||
nnoremap <silent> <buffer> <localleader>r :call smt2#solver#Run()<cr>
|
||||
nnoremap <silent> <buffer> <localleader>R :call smt2#solver#RunAndShowResult()<cr>
|
||||
nnoremap <silent> <buffer> <localleader>v :call smt2#solver#PrintVersion()<cr>
|
||||
|
||||
" Mappings for formatting functionality
|
||||
nnoremap <silent> <buffer> <localleader>f :call smt2#formatter#FormatCurrentParagraph()<cr>
|
||||
nnoremap <silent> <buffer> <localleader>F :call smt2#formatter#FormatAllParagraphs()<cr>
|
||||
|
||||
Reference in New Issue
Block a user