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

Projections not handled correctly? #2

Closed robsimmons closed 12 years ago

robsimmons commented 12 years ago

This diff:

https://github.com/robsimmons/l10/commit/692591074a70fe5c7ad9cc52a58e9c2f4c154dba

goes from no errors to one error in the code, seeming to indicate that projections aren't being handled correctly

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

is a branch that demonstrates this strange bug:

CIDRE: basis construction error: 

/Users/rjsimmon/r/l10/sml/check-types.sml:641.9-641.48 Error: 
           Decl.DB (pos, (db, props', hd worlds'))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Sort mismatch: t
      expecting: decl_t
------------------------------------------------------------------
/Users/rjsimmon/r/l10/sml/check-types.sml:639.23-639.59 Error: 
           val worlds' = #2 (tc_worlds DictX.empty [ world ])
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Sort mismatch: (t * (symbol * t list)) list
      expecting: (t * (symbol * (term & term_t) list)) list
------------------------------------------------------------------
rowandavies commented 12 years ago

Fixed! This was purely oversight on my part - but pretty easy to miss when #2 is derived construct that's turned into a function with a pattern match during parsing.

The fix doesn't precisely catch expressions generated via #label, it catches some extra ones that have functions that always return a variable, but at worst this allows a few more programs to be considered syntactically "bidirectional".