Skip to content

[hack] section discharge unused #119

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 13 commits into from
Nov 3, 2020
Merged

[hack] section discharge unused #119

merged 13 commits into from
Nov 3, 2020

Conversation

@gares
Copy link
Member

@gares gares commented Sep 24, 2020

No description provided.

@gares gares changed the title wip [hack] section discharge unused Sep 24, 2020
@gares
Copy link
Member Author

gares commented Oct 1, 2020

There are two issues, one is about type inference of Context
HB.builders Context (T : finType) (P : pred T) sT of FinTypeForSub T P sT.
you cannot omit the type of P since it can only be inferred from the factory which we don't have yet type checked.

The other bug is that the API to apply an abbreviation is not sound.
We have an abbreviation with 3 arguments but we only pass 1, so we obtain a non-term x\y\term.
I will make the API sound in Coq-Elpi, but we have to fix our code anyway, see % BUG

@gares
Copy link
Member Author

gares commented Oct 1, 2020

The first bug seems like a limitation we cannot really overcome, but we can at least document it.

@gares
Copy link
Member Author

gares commented Oct 1, 2020

Here the new error message

File "./ssreflect/fintype.v", line 1453, characters 0-85:
Error: coq.notation.abbreviation: axioms expects 3 arguments but was given 1

@gares

This comment has been minimized.

Sign in to view
@gares

This comment has been minimized.

Sign in to view
@CohenCyril

This comment has been minimized.

Sign in to view
@gares

This comment has been minimized.

Sign in to view
@CohenCyril

This comment has been minimized.

Sign in to view
@gares

This comment has been minimized.

Sign in to view
@gares

This comment has been minimized.

Sign in to view
gares
gares commented Oct 6, 2020
View reviewed changes
@gares gares force-pushed the section-discharge-fight branch from 9684037 to d16a38b Compare October 9, 2020 08:08
@gares
Copy link
Member Author

gares commented Oct 9, 2020

After a long journey the PR title looks reasonable again.
The last commit adds a let-in mentioning the factory in the builders, so that section discharging does do what we want.
The other commits simplify the code making builder synthesis rely on section discharging and not hand made function composition (which was broken, but also sometimes coping with the discharging problem).

@gares gares requested a review from CohenCyril October 9, 2020 08:17
gares
gares commented Oct 9, 2020
View reviewed changes
hb.elpi
].

pred hack-append-phant-unify i:int, i:phant-term, o:phant-term.
hack-append-phant-unify 0 X Y :- append-phant-unify X Y.
Copy link
Member Author

@gares gares Oct 9, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@CohenCyril can you write a line of doc for this thing?

gares added 13 commits November 3, 2020 09:16
@gares
cleanup
7bf5699
@gares
fix test w.r.t. section discharging
87e1112
@gares
fix nice-gref->string
dd40f55
@gares
rewrite composition, work around section discharging
51fc5b8
@gares
HB.instance inside a builders adds automatically the let-in
dad36d3
@gares
Syntax for anonymous instances (fix #116)
2efcf2f
@gares
always use hb-add-const (fix #113)
fcc82ad
@gares
clarify some names
33e32a5
@gares
cleanup codepath for mixin asset
4d83ed4
@gares
make HB universe polymorphism "ready"
37da239 
In that setting storing terms in a program is problematic, since
poly universes should be abstracted as clause parameters. We could
do that, but the simplest approach is to just store term names. It
is then the operation of "mentioning a name", building (global GR),
which will have to take care to instantiate a poly constant.
This stays todo, waiting for coq-elpi
@gares
mention mixins and params in the hack
f8ff85b
@gares
rm import
2a18376
@gares
wip
6e41414
@gares gares force-pushed the section-discharge-fight branch from 4c4907e to 6e41414 Compare November 3, 2020 08:18
@gares
Copy link
Member Author

gares commented Nov 3, 2020

Can we merge this? I'd like to port HB to the univ-poly branch of Coq-Elpi and I don't like branches over branches too much.
Also, this seems pretty ok to me.

@CohenCyril
Copy link
Member

CohenCyril commented Nov 3, 2020

Yes, let's merge!

@gares gares merged commit aecee52 into master Nov 3, 2020
@gares gares deleted the section-discharge-fight branch November 3, 2020 14:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gares @CohenCyril