This changes the FStar.Dyn module to provide the API I've used in the Pulse thunks I've shown on Wednesday.
Generalize the FStar.Dyn API with a dyn_has_ty predicate, which makes undyn safe to call (outside of --MLish).
Provide a reference implementation of FStar.Dyn showing that this API is sound.
Add a subeffect DIV ~> ALL. (Not sure why this isn't already there. You can already write diverging functions in the compiler.)
Replace all uses of FStar.Compiler.Dyn by FStar.Dyn.
I believe it is consistent (also w.r.t. to the computational behavior) to add a significantly more powerful API, but I don't think you can construct that without assume:
This changes the
FStar.Dynmodule to provide the API I've used in the Pulse thunks I've shown on Wednesday.FStar.DynAPI with adyn_has_typredicate, which makesundynsafe to call (outside of --MLish).FStar.Dynshowing that this API is sound.DIV ~> ALL. (Not sure why this isn't already there. You can already write diverging functions in the compiler.)FStar.Compiler.DynbyFStar.Dyn.I believe it is consistent (also w.r.t. to the computational behavior) to add a significantly more powerful API, but I don't think you can construct that without assume:
undyncould be totaldyn_has_tycould be covariant in the type