Add env var to disable typing of formulas during entailment checking#60
Conversation
this should probably only be done in untyped mode, though currently the `can_unify_with` check eliminates all ill-typed instantiations in typed mode so it won't change anything for now
danbaterisna
changed the title
|
|
||
| Setting `NOTYPES=1` will defer all typechecking during entailment checks until necessary (i.e. before SMT translation). This may be useful to ease development of extensions | ||
| outside of those typechecked by OCaml. | ||
|
|
There was a problem hiding this comment.
I'm a bit confused about the intended use of this, i.e. how this eases development. Is it to disable the type checking in case there are bugs in it?
If so, why is that related to shift/reset - my understanding is that without NOTYPES, shift/reset will be typed with Anys and will still work.
There was a problem hiding this comment.
Is it to disable the type checking in case there are bugs in it?
Yes, at least according to my interpretation. Even if shift/reset are typed with Anys, there may still be bugs inside the type checker when dealing with those Anys.
There was a problem hiding this comment.
To add to this, there are cases where these Anys prevent the type checker from seeing that two types are equal. Since Any does not propagate, depending on how types are handled later on, it can be a nuisance to have to worry about types when implementing similar future extensions which do not have a simple-to-implement type system (since otherwise, rewriting rules do not match due to type mismatches, etc.)
|
This is fine, but is there a way to 'hide' the implementation of Like, we have a flag that the start, and at runtime based on this flag we will "choose" the corresponding "implementation"/"module". For the rest of the code, they should never need to know about the existent of |
|
I'm not sure there's a clean way to do that. To implement this via two different "implementations" (instead of the current approach, where Maybe the |
3 participants
When the prover is run with
NOTYPES=1, all types in staged formulas are replaced withAnyto simplify the needed processing in situations where type inference is incomplete (e.g. when untyped extensions are present). Before SMT translation, allAnys are replaced with fresh type variables, and only then are types inferred.Should there be a warning for when untyped extensions are used with types enabled?