Jason Gross (Nov 21 2022 at 21:56): Jason Gross (Nov 21 2022 at 21:56):Is there a reason that there's no tmUnquote in the extractible monad that routes through the native compiler?
Matthieu Sozeau (Nov 23 2022 at 12:59):You want this tmUnquote to return what exactly?
Jason Gross (Nov 23 2022 at 13:37):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.)
Jason Gross (Nov 23 2022 at 13:38):This isn't blocking anything I'm trying to do, though; at this point it's mostly idle curiosity
Last updated: Jun 10 2023 at 06:31 UTC