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

Raise CRASH in polymorphic refinements #4

Closed robsimmons closed 12 years ago

robsimmons commented 12 years ago

https://github.com/robsimmons/l10/tree/bug4

Causes Crash to be raised. Not a clue.

bash-3.2$ ../sml-cidre/bin/sml-cidre
Standard ML of New Jersey 110.72
with SML-CIDRE 0.99999

Quickstart:   Cidre.make "filenm.cm";

val it = "a piece of" : string
- Cidre.check "sml/refine.mlb";
CIDRE: MLB sml/refine.mlb 
..snip..
check-types.sml checked in 0.703s
Impossible: RefDec.patSort_to_Sorts(2): 
applying:  t * t stream -> t front
    to:  decl_t * decl_t stream
patSort: SORTps(decl_t * decl_t stream)

Elab
             non-gc         system             gc      wallclock
              0.003          0.000          0.000          0.003

uncaught exception CRASH
  raised at: ../sml-cidre/src/Common/Crash.sml:11.8-11.13
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../Manager/ParseElab.sml:182.80
             ../Manager/ParseElab.sml:189.54
             ../Cidre/Cidre.sml:220.63-220.65
             ../Cidre/Cidre.sml:302.64
rowandavies commented 12 years ago

This is a variant of the familiar issue of how instantiation relates to subsorting. But, using sort constraints won't work in this case.

And, after thinking about this generally for quite a while, I think I see that there's a natural approach to calculating residual sorts that avoids these issues. I've tried this before and failed - the key new insight is that when calculating the sort "bottom up" we can pass "top down" the original sort from which some patterns have been subtracted. I think this is needed to resolve the cases involving functions - for which we know we can't have partially matched.

I'm half-way through implementing this, so stay tuned. And, I have some similar ideas on how to instantiate variables and constructors in "head position" of a checkable expression - which seems to account for all but one of the <: constraints in the current l10 sml code.

rowandavies commented 12 years ago

This won't crash anymore, and for the given code it works fine.

But more generally the sorts assigned to variables in patterns could sometimes be accurate. So, I'm also still planning to implement a "try and see" approach to limiting instantiations as well as the improved "bottom up" calculation via upper and lower bounds on sort variables mentioned in my previous comment.