ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
141 stars 61 forks source link

Show ($k x y) such that it can be fed back to the parser #630

Closed shingarov closed 1 year ago

shingarov commented 1 year ago

Even though Haskell is not, by design, a homoiconic language a-la Lisp, in some cases having Show produce strings that can be parsed back is advantageous. For example, LiquidFixpoint's clients such as Sprite, may dump VCs in LF format; these dumps can be a valuable aid in understanding the code. This series of commits ensures the dumped VCs are in fact valid LF.

ranjitjhala commented 1 year ago

Thank you so much!