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