Compute Dependencies in the extractable monad

[gmalecha]

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.

[SimonBoulier]

Yes. tmDependencies would be nice!

[aa755]

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?

[yforster]

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 ***@***.***> 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.

[aa755]

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 <notifications@github.com> 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 ***@***.***> 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 <#133 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AADZ44UWEM733UVETANZOG3PULIJ5ANCNFSM4HLNSIIQ> .

[gmalecha]

General recursion could be nice, but that might warrant a longer discussion. In particular, it might make reasoning about meta functions more difficult.

[gmalecha]

This is almost certainly duplicated.

[mattam82]

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.

[gmalecha]

Discussion with @mattam82 , it seems like the plan is to finish implementing this (and possibly something else).