search

ucsd-progsys / liquid-fixpoint

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

Fix `tidySymbol` to not drop arg-id #659

Closed ranjitjhala closed 10 months ago

ranjitjhala commented 10 months ago

fixes #658

ranjitjhala commented 10 months ago

Excellent suggestion @facundo, will do!

On Sat, Nov 4, 2023 at 8:45 AM Facundo Domínguez @.***> wrote:

@.**** commented on this pull request.

In src/Language/Fixpoint/Types/Names.hs https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/659*discussion_r1382420428__;Iw!!Mih3wA!HmfM8YSx-cb_SZp0RiSayMOc2wUkoIWw_cQ1zJDc2Rqli0zCuv2yOroFyFIzaQvfwFHzOIKZd4D-vS0uXYKXC19x$ :

@@ -518,7 +518,7 @@ tidySymbol s | otherwise = s'' where s' = unPrefixSymbol kArgPrefix s

  • s'' = unPrefixSymbol symSepName . unPrefixSymbol hvarPrefix $ s'
  • s'' = consSym '$' . unPrefixSymbol symSepName . unSuffixSymbol . unPrefixSymbol hvarPrefix $ s'

And similar suggestion for the other functions modified in the PR. Alternatively, perhaps the source code could be made more self explanatory if the structure of the symbols is explained in a comment.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquid-fixpoint/pull/659*discussion_r1382420428__;Iw!!Mih3wA!HmfM8YSx-cb_SZp0RiSayMOc2wUkoIWw_cQ1zJDc2Rqli0zCuv2yOroFyFIzaQvfwFHzOIKZd4D-vS0uXYKXC19x$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGMADGP5S5JEHMD2FTYCZPKDAVCNFSM6AAAAAA65UKPBWVHI2DSMVQWIX3LMV43YUDVNRWFEZLROVSXG5CSMV3GSZLXHMYTOMJTHAYTIMRXGA__;!!Mih3wA!HmfM8YSx-cb_SZp0RiSayMOc2wUkoIWw_cQ1zJDc2Rqli0zCuv2yOroFyFIzaQvfwFHzOIKZd4D-vS0uXT1Zlrtf$ . You are receiving this because you authored the thread.Message ID: @.***>