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

SMT-LIB: print symbols with `|` #64

Open hansjoergschurr opened 3 years ago

hansjoergschurr commented 3 years ago

This is a feature request. It would be nice if dolmen could print extended symbols with the | quotes in error messages. For example: 

File "foo.smt2", line 1056, character 64-96:
Error The term: (q(10) * 203.0) has type real but was expected to be of type
      int

Here q(10) is a symbol that must be written as |q(10)| in the input. While here this only leads to a second of confusion, in other cases it might lead to actual problems. For example, if the symbols is |(q 10)|, which would also be a valid SMT-LIB term.

Gbury commented 3 years ago

Indeed, I'll try and see if there is an easily reasonable way to do that.

Gbury commented 3 years ago

So, this issue will be fixed, but it will take a bit of time. Basically my roadmap currently is: finish higher-order for Dolmen (soon !), then get on with writing the export API (i.e. the capability to print terms in a given language), and once that's done, error messages will use that API to print terms in the input language syntax (and respect conventions for escaping, etc..), which will solve this problem.

hansjoergschurr commented 3 years ago

Sounds like a good plan