search

gmalecha / mirror-core

A framework for extensible, reflective decision procedures.
Other
19 stars 5 forks source link

Way to debug expressions that don't typecheck #62

Open jldodds opened 9 years ago

jldodds commented 9 years ago

It would be very useful if there was a function that took an expr and if that expr doesn't typecheck returns a (possibly) smaller expression along with the type it is expected to have

jldodds commented 9 years ago

or just a smaller expression that fails to typecheck on its own

gmalecha commented 9 years ago

I think the easiest thing to do right now is to call [typeof_expr](in https://github.com/gmalecha/mirror-core/blob/master/theories/Lambda/ExprDI.v#L105). It returns [None] if the term is well-typed and otherwise it returns [Some].

jldodds commented 9 years ago

Yep, I did that, but my term was huge. It would be nice if there was a function that found the part that didn't typecheck. I eventually found it my manually testing many parts of the term