search

rowandavies / sml-cidre

SML Checker for Intersection and Datasort Refinements (pronounced "cider")
http://www.cs.cmu.edu/~rowan/sorts.html
Other
20 stars 2 forks source link

Cidre MLB should support 'nonexhaustiveMatch ignore' annotations #9

Open robsimmons opened 12 years ago

robsimmons commented 12 years ago

I already annotate code that I expect to fail in libraries, it would be nice if CIDRE would suppress these errors where requested.

rowandavies commented 12 years ago

The argument against this is that non-exhaustive matches when using CIDRE are different and rarer from the standard ones. Personally I generally add a catch all case for these with a comment, although I do sometimes find this awkward when interfacing to non-CIDREd code, particularly with something like:

  val SOME x =  somehowYouKnowThisReturnsASome  withThisArgument

The argument in favor of supporting this is that it's best to let the programmer decide what is best for each situation. I guess I agree with this, but I'd like to safeguard against spurious suppression such as where these annotations are introduced for MLton and the programmer doesn't realize there are CIDRE warnings they're not seeing.

One design would be to have a new MLB annotation that makes CIDRE pay attention to the existing 'nonexhaustiveMatch ignore' annotations. Or, maybe just having CIDRE summarize at the very end of "Cidre.make" - something like:

    CIDRE: checking completed.  There were suppressed warnings in: union-find-imperative.sml, another-file.sml

Related to this - currently non-exhaustiveness results only in warnings, but if the programmer has a way to specify where non-exhaustiveness is expected it may make sense to promote these warnings to errors elsewhere. Or maybe to have an MLB annotation that does this. Reporting errors would cause CIDRE to abort before checking the next source file or calling "CM.make".

robsimmons commented 12 years ago

So, MLton MLB annotations can already handle "nonexhaustiveMatch error". I agree this would be a reasonable default for SML-CIDRE - if you want it to be just a warning, you have to tell SML-CIDRE to merely issue a warning with a "nonexhaustiveMatch warn" annotation.

I'd support your "suppressed non-exhaustive match warnings" notice. My main issue is the "one bit" issue - when I compile, I can visualize the one bit of information of whether some non-exhaustive match stuff flew plast me, and library code setting that one bit can cause me to miss the errors in my own code.