port to elpi 3.0 #527
port to elpi 3.0 #527
Conversation
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
since there was a findall we use 'from' to generate all inputs, but this way it could contain duplicates. the right solution is to have a predicate listing (once) each HB generated constant.
|
There are some predicates with the comment However, I can’t keep them in the code as-is, because they break determinacy. For instance, a successful call to @CohenCyril — would it be a major issue if I comment out these three predicates and change the comment from |
|
HB seems to dépend on coq elpi >= 2.0, sothey should be removed |
HB/common/utils-synterp.elpi
Outdated
| @@ -2,7 +2,7 @@ | |||
| This software is released under the terms of the MIT license */ | |||
|
|
|||
| % runs P in a context where Coq #[attributes] are parsed | |||
| pred with-attributes i:prop. | |||
| func with-attributes fprop. | |||
There was a problem hiding this comment.
Ok, I changed here: 54a5138
|
| func compute-filter.aux list string, list string -> list string. | ||
| compute-filter.aux [S|_] [S] [S] :- !. |
There was a problem hiding this comment.
Is it intentional that this predicate is also declared identically in utils-synter.elpi?
| bulletize1 F X (glue [str "- ", M]) :- F X M. | ||
|
|
||
| pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. | ||
| bulletize [] _ empty. | ||
| func bulletize list A, (func A -> coq.pp) -> coq.pp. |
There was a problem hiding this comment.
Just to be sure, bulletize is a function?
If it is not the case, the cut in the rule below should be removed...
| toposort ES XS XS'' :- | ||
| toporec ES XS [] [] _ XS', | ||
| std.filter XS' (std.mem XS) XS''. | ||
| std.filter XS' (std.mem! XS) XS''. |
There was a problem hiding this comment.
I think toposort is a function, am I right?
If that’s the case, then we should use std.mem! instead of std.mem to avoid unnecessary
(and horrible) choice points.
|
|
||
| % [join C1 C2 C3] means that C3 inherits from both C1 and C2 | ||
| pred join o:classname, o:classname, o:classname. | ||
|
|
||
| % Section local memory of names for mixins, so that we can reuse them | ||
| % and build terms with simpler conversion problems (less unfolding | ||
| % in order to discover two mixins are the same) | ||
| pred mixin-mem i:term, o:gref. | ||
| func mixin-mem term -> gref. |
There was a problem hiding this comment.
Is it really a function?
I think it is, but mixin-mem rules are built as a list and loaded via flex clauses (e.g., Clauses =>).
These clauses are constructed, for example, in the third rule of declare-all:
→ infer-class → optimize-class-body → declare-mixin-name → std.append CL1 CL2 Clauses.
Tracking this information seems difficult.
Since elpi 3.0 is still in development this is very preliminary.
The main visible change is that functional predicates can be flagged as such and the static checker complains if they are not detected to be functional. CFR https://inria.hal.science/hal-05026472
CC @FissoreD