Skip to content
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

Adapt to MC#1319 #106

Closed
wants to merge 1 commit into from
Closed

Adapt to MC#1319 #106

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 17 additions & 7 deletions theories/common.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,12 @@ type rmorphism-Z rmorphism. % (int_of_Z _)%:~R

% destructors

pred sring->pzsring i:term, o:term.
sring->pzsring U V :-
if (coq.locate-all "pzSemiRingType" [loc-gref PzSemiRingType| _ ])
(coq.elaborate-skeleton U (global PzSemiRingType) V ok)
(V = U).

Comment on lines +181 to +186
Copy link
Member

Choose a reason for hiding this comment

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

Calling this predicate every time we process a ring operator looks a bit costly. Isn't it possible to define compatibility notations (or constants) for GRing.SemiRing.sort, GRing.ComSemiRing.sort, GRing.Ring.sort, and GRing.ComRing.sort and replace their occurrences in common.elpi?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, Cyril raised the same issue. He figured that we could make the code more robust to the changes that are happening in mathcomp by precomputing the coercions that coq.elaborate-skeleton would insert, see #108).

pred rmorphism->nmod i:rmorphism, o:term.
rmorphism->nmod (rmorphism U _ _ _ _ _ _) U :- !.
rmorphism->nmod rmorphism-nat (global (const U)) :- !, canonical-nat-nmodule U.
Expand Down Expand Up @@ -216,16 +222,20 @@ rmorphism->field (rmorphism _ _ _ _ _ (some F) _) F :- !.
pred rmorphism->morph i:rmorphism, o:term -> term.
rmorphism->morph (rmorphism _ _ _ _ _ _ Morph) Morph :- !.
rmorphism->morph rmorphism-nat Morph :- !,
target-nmodule TU, !, target-semiring TR, !,
target-nmodule TU, !, target-semiring TR', !,
sring->pzsring TR' TR,
Morph = n\ {{ @GRing.natmul lp:TU (@GRing.one lp:TR) lp:n }}.
rmorphism->morph rmorphism-N Morph :- !,
target-nmodule TU, !, target-semiring TR, !,
target-nmodule TU, !, target-semiring TR', !,
sring->pzsring TR' TR,
Morph = n\ {{ @GRing.natmul lp:TU (@GRing.one lp:TR) (N.to_nat lp:n) }}.
rmorphism->morph rmorphism-int Morph :- !,
target-zmodule TU, !, target-semiring TR, !,
target-zmodule TU, !, target-semiring TR', !,
sring->pzsring TR' TR,
Morph = n\ {{ @intmul lp:TU (@GRing.one lp:TR) lp:n }}.
rmorphism->morph rmorphism-Z Morph :- !,
target-zmodule TU, !, target-semiring TR, !,
target-zmodule TU, !, target-semiring TR', !,
sring->pzsring TR' TR,
Morph = n\ {{ @intmul lp:TU (@GRing.one lp:TR) (int_of_Z lp:n) }}.

pred rmorphism-rm-field i:rmorphism, o:rmorphism.
Expand Down Expand Up @@ -458,13 +468,13 @@ ring C {{ @intmul lp:U lp:In1 lp:In2 }}
% 1%R
ring C {{ @GRing.one lp:R' }} {{ @R1 lp:R }} Out _ :-
rmorphism->sring C R,
coq.unify-eq R R' ok, !,
coq.unify-eq { sring->pzsring R } R' ok, !,
build.one Out.
% *%R
ring C {{ @GRing.mul lp:R' lp:In1 lp:In2 }}
{{ @RMul lp:R lp:OutM1 lp:OutM2 }} Out VM :-
rmorphism->sring C R,
coq.unify-eq R R' ok, !,
coq.unify-eq { sring->pzsring R } R' ok, !,
ring C In1 OutM1 Out1 VM, !,
ring C In2 OutM2 Out2 VM, !,
build.mul Out1 Out2 Out.
Expand All @@ -490,7 +500,7 @@ ring rmorphism-Z {{ Z.mul lp:In1 lp:In2 }}
ring C {{ @GRing.exp lp:R' lp:In1 lp:In2 }}
{{ @RExpn lp:R lp:OutM1 lp:OutM2 }} Out VM :-
rmorphism->sring C R,
coq.unify-eq R R' ok,
coq.unify-eq { sring->pzsring R } R' ok,
n-const In2 OutM2 Out2, !,
ring C In1 OutM1 Out1 VM, !,
build.exp Out1 Out2 Out.
Expand Down
Loading