bohlender / vim-smt2 Goto Github PK

The plugin's auto-formatting relies on vim9script which was still "experimental" during development of that functionality. It seems that later iterations of vim9script got a bit more restrictive wrt. naming of symbols so the auto-formatting throws an error on more recent versions of Vim.

Error detected while processing ~/.vim/bundle/vim-smt2/autoload/smt2/formatter.vim:
line   95:
E1263: Cannot use name with # in Vim9 script, use export instead
E117: Unknown function: smt2#formatter#FormatAllParagraphs

Goal: Figure out what exactly the new expectation of vim9script is and make auto-formatting again available for all versions after Vim v8.2.2725.

Hi! First of all thanks a lot for this extension, I'm finding it extremely useful.

A slight problem I usually run into is that my smt2 files have empty lines within a single top-level expression, such as this:

(declare-fun x () Int)
(declare-fun y () Int)

(assert (not
 
(= (+ x y) (+ y x))

))

(check-sat)

Placing the cursor at the beginning of the assert and formatting gives this, which is broken.

(declare-fun x () Int)
(declare-fun y () Int)

(assert (not (= (+ x y) (+ y x))))

(= (+ x y) (+ y x))

))

(check-sat)

So I now usually just remove all empty lines before working on a file, but if this worked out of the box it would be amazing :).

Come to think of it, the current behavior seems useful for formatting a whole chunk of s-expressions clumped together as a paragraph.. maybe there can be a binding to ask for formatting a single s-expression?

I think it would be nice to add some auto-formatting capabilities. Currently, when writing or debugging SMT instances, I often format them manually to review the structure of each expression and identify potential errors.

To illustrate the kind of formatting I have in mind, consider the following De Morgan example:

(declare-const a Bool)
(declare-const b Bool)
(define-fun demorgan () Bool
    (= (and a b) (not (or (not a) (not b)))))
(assert (not demorgan))
(check-sat)

Even in this simple case the structure of (= (and a b) (not (or (not a) (not b))))) is not immediately clear and could use some reformatting for closer inspection.

I suggest that pressing <localleader>f should yield the following:

(declare-const a Bool)
(declare-const b Bool)
(define-fun demorgan () Bool
    (=
        (and a b)
        (not
            (or
                (not a)
                (not b))))) ; Not sure about the parens -- maybe on their own lines?
(assert (not demorgan))
(check-sat)

Any opinions on that? Maybe there even is an easy way to achieve this already. It's not a pressing issue for sure, but I guess something along those lines would be nice to have.