search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.17k stars 131 forks source link

Importing infix annotations. #1123

Open nikivazou opened 6 years ago

nikivazou commented 6 years ago

Here https://github.com/nikivazou/theorem-proving-template/blob/master/safe-lists/src/Theorems/List.hs#L10

Data.List.hs defines (++) as an infix reflected function: https://github.com/nikivazou/theorem-proving-template/blob/master/safe-lists/src/Data/List.hs#L25

The infix annotation is not imported when I import Data.List and I have to write it again, otherwise parsing fails.

ranjitjhala commented 6 years ago

I didn't know we had an infix annotation -- should be straightforward to handle.

In fact, you might do it yourself; see the functions called saveLiftedSpec and loadLiftedSpec.

We need only to add the set of infix annotations to the saved and loaded specs.

ranjitjhala commented 6 years ago

Oh yikes -- you implemented infix by modifying the state of the parser...

This will be awful to fix.

kosmikus commented 4 years ago

This is not exclusively a parser bug. I am working on changes of the parser that will make it possible for LH infix directives to appear "out of order". However, it seems LH does not write the presence of infix directives to the interface file. This has to be fixed independently.