metacoq
metacoq copied to clipboard
MetaCoq
Compute Dependencies in the extractable monad
This is a proposal to implement tmQuoteRecursive using an action tmDependencies that returns a list of all of the dependencies. The client can then traverse the list to compute the global_references type. I'm not sure how much this simplifies things, but it seems a little bit more orthogonal and potentially allows quoting less.
tmDependencies was almost definable in the monad (even before this PR)? Fuel was needed to circumvent the issue of convincing the termination checker. Would it be better (more general) to just add a fixpoint combinator in the monad?
There was a PR for Coq at some point (by Théo I think?) introducing a flag to make fixpoints unguarded. That would make a fixpoint combinator in the monad superfluos. Do we know what the status of this PR is?
On 8 May 2019 4:01:37 p.m. Abhishek Anand [email protected] wrote:
tmDependencies was almost definable in the monad (even before this PR)? Fuel was needed to circumvent the issue of convincing the termination checker. Would it be better (more general) to just add a fixpoint combinator in the monad? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.
When used, the option of making fixpoints unguarded will make the entire logic inconsistent. Adding a fixpoint combinator to the monad will not.
-- Abhishek http://www.cs.cornell.edu/~aa755/
On Wed, May 8, 2019 at 6:26 AM Yannick Forster [email protected] wrote:
There was a PR for Coq at some point (by Théo I think?) introducing a flag to make fixpoints unguarded. That would make a fixpoint combinator in the monad superfluos. Do we know what the status of this PR is?
On 8 May 2019 4:01:37 p.m. Abhishek Anand [email protected] wrote:
tmDependencies was almost definable in the monad (even before this PR)? Fuel was needed to circumvent the issue of convincing the termination checker. Would it be better (more general) to just add a fixpoint combinator in the monad? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.
— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/MetaCoq/metacoq/pull/133#issuecomment-490485013, or mute the thread https://github.com/notifications/unsubscribe-auth/AADZ44UWEM733UVETANZOG3PULIJ5ANCNFSM4HLNSIIQ .
General recursion could be nice, but that might warrant a longer discussion. In particular, it might make reasoning about meta functions more difficult.
I’m surprised you couldn’t do it with fuel and a computed bound, as there is a finite number of references in a global_environment + term. Termination might be tricky, e.g. avoiding loops cleanly requires to know that the env is well-founded/linearizable (Typing.wf would ensure this). But I don’t see how it could be impossible, at least using the size of the term as a bound for the number of global_references or something like that.
Discussion with @mattam82 , it seems like the plan is to finish implementing this (and possibly something else).