Skip to content

Adding coercions from classes to mixins #101

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

Merged
merged 1 commit into from
Aug 7, 2020
Merged

Adding coercions from classes to mixins #101

Show file tree
Hide file tree
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
14 changes: 6 additions & 8 deletions default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,18 +1,16 @@
{withEmacs ? false,
nixpkgs ? (fetchTarball {
url = "https://github.com/NixOS/nixpkgs-channels/archive/0a9d9946ed3e1ec526848db2f77f2dc978b46bb5.tar.gz";
sha256 = "1gdqnb5g5h47gqx95lyzlqnmhzkcnh27gia778cr79cmgvwasb69";
}),
nixpkgs ? (fetchTarball https://github.com/NixOS/nixpkgs-channels/archive/e97fdce4e1b945c9ec30d4d90a451f1577f5cf4a.tar.gz),
coq-version ? "8.11",
print-env ? false
}:
with import nixpkgs {
overlays = [ (super: self: {
coqPackages = { "8.11" = super.coqPackages_8_11; }."${coq-version}".overrideScope' (self: super: {
## Coq package override example:
# coq-elpi = super.coq-elpi.overrideAttrs (old: {
# name = "coq8.11-elpi-v1.4.0";
# src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.4.0.tar.gz;
# Coq package override example:
coq-elpi = super.coq-elpi.overrideAttrs (old: {
name = "coq8.11-elpi-1.5.0";
src = fetchTarball https://github.com/LPCIC/coq-elpi/archive/v1.5.0.tar.gz;
});
});
coq = self.coqPackages.coq;
})];
Expand Down
20 changes: 19 additions & 1 deletion hb.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1457,6 +1457,16 @@ if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
(coq.error "Structure" {coq.term->string S} "contains the same mixins of" N)
(if-class-already-exists-error N CS ML2).

pred export-mixin-coercion i:classname, i:option constant.
export-mixin-coercion _ none.
export-mixin-coercion ClassName (some C) :-
coq.env.typeof (const C) CTy,
safe-dest-app {safe-head CTy} Mixin _,
coq.term->gref Mixin MixinGR,
if-verbose (coq.say "export-mixin-coercion: from" ClassName "to" MixinGR),
@global! =>
coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).

% HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
% cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
pred main-declare-structure i:string, i:list-w-params gref, i:bool.
Expand Down Expand Up @@ -1508,6 +1518,14 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
declare-unification-hints SortProjection ClassProjection CurrentClass NewJoins,
% Register in Elpi's DB the new structure
% NOT TODO: All these acc are correctly locaed in an Export Module

if (ClassName = indt ClassInd) (std.do![
if-verbose (coq.say "HB: exporting coercions from class to mixins"),
std.forall {coq.CS.canonical-projections ClassInd}
(export-mixin-coercion ClassName)
])
(coq.say "declare-structure:" ClassName "should be an inductive", fail),

if-verbose (coq.say "HB: accumulating various props"),
std.forall MLToExport (m\ acc current (clause _ _ (mixin-first-class m ClassName))),
std.forall EX (ex\ acc current (clause _ _ ex)),
Expand Down Expand Up @@ -1698,7 +1716,7 @@ is-last-named-asset-param (asset-parameter _ _ _\ asset-alias _ _) :- !.

% main-declare-asset Asset AssetKind
pred main-declare-asset i:asset-decl, i:asset.
main-declare-asset Asset AssetKind :-
main-declare-asset Asset AssetKind :-
% since we turn locally bound variables into global constrants the holes
% in the input term can go outside the pattern fragment, but we don't care
@holes! => std.do! [
Expand Down