Initial version of typed holes support under allow-typed-holes flag#2486
Initial version of typed holes support under allow-typed-holes flag#2486facundominguez merged 14 commits intoucsd-progsys:developfrom
Conversation
facundominguez
left a comment
facundominguez
left a comment
There was a problem hiding this comment.
Thanks @matheussbernardo. I left some comments. Can we have the feature documented? Maybe it could have a section in docs/mkDocs/docs/options.md.
Also, it would be helpful to have an example of a warning message produced by this implementation for the discussion.
| getSrcSpanFromTick = case genTick of | ||
| SourceNote src _ -> src | ||
| _ -> panic Nothing "Not a Source Note" | ||
| isVarHole = L.isInfixOf "hole" . F.symbolString . F.symbol |
There was a problem hiding this comment.
Will this mistakenly catch variables written by the user that include "hole" in their name? e.g. whole, wholesale, etc.
To make this as precise as possible, I need to understand yet how the variable is bound.
There was a problem hiding this comment.
I updated the implementation. Can you take a second look?
| {-@ LIQUID "--expect-error-containing=Hole Found" @-} | ||
| {-@ LIQUID "--exact-data-cons" @-} | ||
| {-@ LIQUID "--allow-typed-holes" @-} | ||
| {-@ LIQUID "--warn-on-term-holes" @-} |
There was a problem hiding this comment.
This could be added to the basic-pos testsuite. For scripts/test/test_plugin.sh to pick up the module, it will need to be listed in tests/tests.cabal.
There was a problem hiding this comment.
I just found that it is actually listed in tests.cabal. A separate executable seems overkill for a single test. It would be terser to put it in an existing executable.
There was a problem hiding this comment.
I added more tests to this. I was thinking of adding all my examples to it. But maybe it is a overkill
matheussbernardo
force-pushed
the
develop
branch
2 times, most recently
from
d7ebb82 to
7037c59
Compare
* add detect synthesis * adding different warning strategy * consolidate anf holes warnings * more detect synthesis * more detect synthesis * Fixing nested hole bug * Add new version detect synthesis
|
👋 I rebased master to evaluate this PR again. |
|
We don't have any tooling depending on this yet, but I'm merging it because the implementation is small and unlikely to be problematic. I'll link the master's thesis afterwards. Enhancing Proof Development in LiquidHaskell: Implementation and Evaluation of Typed Holes https://odr.chalmers.se/server/api/core/bitstreams/640ee29b-b13a-44d5-9e20-200a91a11021/content |
2 participants
Based on PR#1140
I am adding a flag --allow-typed-holes
and detecting holes which are bindings with
holeas infix.These holes are currently being saved in the CGInfo and a warning is being presented to the user showing the refinement type.
I added one example in the test that shows how to use this experimental feature.