-
Notifications
You must be signed in to change notification settings - Fork 80
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Compute Dependencies in the extractable monad #133
base: coq-8.8
Are you sure you want to change the base?
Conversation
Yes. |
|
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.
|
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 ***@***.***>
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>
.
|
General recursion could be nice, but that might warrant a longer discussion. In particular, it might make reasoning about meta functions more difficult. |
@@ -210,6 +210,10 @@ struct | |||
else | |||
not_supported_verb trm "unquote_list" | |||
|
|||
let rec quote_list ty = function |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is almost certainly duplicated.
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). |
This is a proposal to implement
tmQuoteRecursive
using an actiontmDependencies
that returns a list of all of the dependencies. The client can then traverse the list to compute theglobal_references
type. I'm not sure how much this simplifies things, but it seems a little bit more orthogonal and potentially allows quoting less.