search

Gbury / dolmen

Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
BSD 2-Clause "Simplified" License
80 stars 17 forks source link

Support for custom attributes #217

Closed Halbaroth closed 5 months ago

Halbaroth commented 5 months ago

I tried to implement my own attribute in Alt-Ergo to name lemmata as follows: (assert (! (...) :lemma my_name) (I don't want to use :named for reasons explained here https://github.com/OCamlPro/alt-ergo/pull/1141)

I managed to implement a custom attribute with a string argument: (assert (! (...) :lemma "my_name")

If I don't quote the string, Dolmen refuses the input because my_name isn't a declared identifier, which is true but from my understanding of the SMT-LIB standard, we can put arbitrary s-expressions after an attribute.

I think the issue comes from the fact we use the namespace term in the Menhir parser here: https://github.com/Gbury/dolmen/blob/5e22e653ec376336bbbed50aca4946db8edbc90f/src/languages/smtlib2/v2.6/script/parser.mly#L94-L105

I guess we should create a sexpr namespace for these identifiers?

Halbaroth commented 5 months ago

I didn't know what's happen last week because I got an error even if I don't parse the term... everything works fine now!