Is there a reason that there's no
tmUnquote in the extractible monad that routes through the native compiler?
You want this tmUnquote to return what exactly?
Hm, I guess it's not quite so simple as I thought. I want to do the following, which I think should be possible in theory, but is maybe too unsafe or complicated in practice:
tmUnquoteTyped <% A %> A a for
A : Type and
a : Ast.term should return
TM A. There's a bit of unsafety I'm not sure how to avoid unless we extend extraction itself: If the first argument is not the quotation of the second argument, the result should be undefined, in the sense that Coq may segfault. Otherwise, the behavior is defined to be: check that
<% A %> is closed (normal TM failure if not); run typechecking on
a : A (normal TM failure if typechecking fails); run a variant of extraction/erasure that mirrors the extraction used to extract the template monad (so the types line up) and feed the result into the ocamlopt / dynlinking so that the extracted code can access it, and then uses
Obj.magic to cast to the required type, relying on the typechecker and alignment of the extraction mechanisms.
(This is my current best idea for getting a fixpoint combinator in the extractible template monad a la https://github.com/MetaCoq/metacoq/pull/790. I have other ideas that are even more unsafe, like exposing
Obj.magic directly in the extractible template monad.)
This isn't blocking anything I'm trying to do, though; at this point it's mostly idle curiosity
Last updated: Jan 30 2023 at 17:03 UTC