Stream: MetaCoq

Topic: tmUnquote


view this post on Zulip 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?

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:59):

You want this tmUnquote to return what exactly?

view this post on Zulip 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.)

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC