Re: [Typer] [Git][monnier/typer][master] Changes to be committed:
line 856, There is an assert that is triggered when attributes are used `assert (ectx == nctx);` since the property context is modified. Which environment should not be modified ?
So, yes, I think it's linked to my comment: (* FIXME: We need to have something in lexp to represent this * add-attribute operation! *) [], ctx) It makes no sense to return an empty list (i.e. no new declarations/definitions) but a new ctx: we need to put something in the returned list which explains/justifies/causes the new context. Otherwise, the `Let` we build from it will not be type-checkable because the "magic" operation is not represented there any more and the `check` function will hence not be able to re-create the proper context. While I'm here: there was a trivial typo in your code, which I fixed (along with adding a conv_p check, now that we can), but now I get a DB error, because in extract_order you call `lexp_whnf` always with the same ctx, even though at each step of the loop the context should actually grow by one element (since the return type of a function can refer to the argument). Could you try and fix it? Stefan
Afficher les réponses par date
Alright. But then I dont understand why the `has-attribute` test is working when the property context was modified. I will investigate the new way you suggested to handle attributes. It might resolve all our issues. I have fixed the `extract_order`
Alright. But then I dont understand why the `has-attribute` test is working when the property context was modified.
I think it's because it's always currently used within a top-level declaration, so it's not turned into a `Let`. Stefan
participants (2)
-
Pierre Delaunay -
Stefan Monnier