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

Generic coercion code #19

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Generic coercion code #19

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
44 changes: 34 additions & 10 deletions elpi/param-class.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,14 +78,6 @@ pred param-class->string i:param-class, o:string.
param-class->string (pc M N) S :-
S is {map-class->string M} ^ {map-class->string N}.

pred param-class->add-suffix i:param-class, i:string, o:string.
param-class->add-suffix Class P S :- S is P ^ {param-class->string Class}.

pred param-class->add-2-suffix i:string,
i:param-class, i:param-class, i:string, o:string.
param-class->add-2-suffix Sep Class1 Class2 P S :-
S is P ^ {param-class->string Class1} ^ Sep ^ {param-class->string Class2}.

% names of the fields contained in a witness of a given level
pred map-class->fields i:map-class, o:list string.
map-class->fields map0 [].
Expand All @@ -105,6 +97,14 @@ map-class->cofields map4 ["comap", "comap_in_R", "R_in_comap", "R_in_comapK"].

namespace map-class {

pred add-suffix i:map-class, i:string, o:string.
add-suffix Class P S :- S is P ^ {map-class->string Class}.

pred add-2-suffix i:string,
i:map-class, i:map-class, i:string, o:string.
add-2-suffix Sep Class1 Class2 P S :-
S is P ^ {map-class->string Class1} ^ Sep ^ {map-class->string Class2}.

% lower/higher levels at distance 1 from a given level
pred weakenings-from i:map-class, o:list map-class.
weakenings-from map0 [].
Expand Down Expand Up @@ -205,21 +205,45 @@ dep-arrow map4 (pc map0 map4) (pc map4 map0).

} % map-class

pred param-classes o:class-kind, o:list param-class.
param-classes high Classes :- std.do! [
map-classes all AllMapClasses,
map-classes high HighMapClasses,
map-class.product HighMapClasses AllMapClasses Classes1,
map-class.product AllMapClasses HighMapClasses Classes2,
std.append Classes1 Classes2 Classes
].
param-classes Kind Classes :-
map-classes Kind MapClasses,
map-class.product MapClasses MapClasses Classes.

namespace param-class {

% extensions of functions over map classes to parametricity classes

pred add-suffix i:param-class, i:string, o:string.
add-suffix Class P S :- S is P ^ {param-class->string Class}.

pred add-2-suffix i:string,
i:param-class, i:param-class, i:string, o:string.
add-2-suffix Sep Class1 Class2 P S :-
S is P ^ {param-class->string Class1} ^ Sep ^ {param-class->string Class2}.

pred weakenings-from i:param-class, o:list param-class.
weakenings-from (pc M N) Classes :-
map-class.weakenings-from M Ms,
map-class.weakenings-from N Ns,
map-class.product Ms Ns Classes.
map-class.product [M] Ns MClasses,
map-class.product Ms [N] NClasses,
std.flatten [MClasses, NClasses] Classes.

pred weakenings-to i:param-class, o:list param-class.
weakenings-to (pc M N) Classes :-
map-class.weakenings-to M Ms,
map-class.weakenings-to N Ns,
map-class.product Ms Ns Classes.
map-class.product [M] Ns MClasses,
map-class.product Ms [N] NClasses,
std.flatten [MClasses, NClasses] Classes.

pred all-weakenings-from i:param-class, o:list param-class.
all-weakenings-from (pc M N) Classes :-
Expand Down
114 changes: 114 additions & 0 deletions elpi/util.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,4 +92,118 @@ subst-gref (pglobal _ I) GR' Tm' :- !,
@uinstance! I => coq.env.global GR' Tm'.
subst-gref T _ _ :- coq.error T "is not a gref".

pred std.string.list->set i:list string, o:std.string.set.
std.string.list->set [] Empty :- std.string.set.empty Empty.
std.string.list->set [S|Rest] Set :-
std.string.set.add S {std.string.list->set Rest} Set.

pred coq.gref.list->set i:list gref, o:coq.gref.set.
coq.gref.list->set [] Empty :- coq.gref.set.empty Empty.
coq.gref.list->set [GR|Rest] Set :-
coq.gref.set.add GR {coq.gref.list->set Rest} Set.

pred coq.gref.list->id-map i:list gref, o:coq.gref.map id.
coq.gref.list->id-map [] Empty :- coq.gref.map.empty Empty.
coq.gref.list->id-map [GR|Rest] Map :-
coq.gref.map.add GR {coq.gref->id GR} {coq.gref.list->id-map Rest} Map.

pred coq.gref.map-string.range o:coq.gref.map string, o:std.string.set.
coq.gref.map-string.range Map Set :- std.do! [
coq.gref.map.bindings Map Bindings,
std.map Bindings (b\ out\ b = pr _ out) Names,
std.string.list->set Names Set
].

pred coq.gref.list->string-map i:list gref, o:std.string.map gref.
coq.gref.list->string-map [] Empty :- std.string.map.empty Empty.
coq.gref.list->string-map [GR|Rest] Map :-
std.string.map.add {coq.gref->id GR} GR {coq.gref.list->string-map Rest} Map.

pred coq.gref.string-map.domain o:std.string.map gref, o:std.string.set.
coq.gref.string-map.domain Map Set :- std.do! [
std.string.map.bindings Map Bindings,
std.map Bindings (b\ out\ b = pr out _) Names,
std.string.list->set Names Set
].

% named-coe Rec1 Rec2 Coe Depth
% builds a function from (p?global (indt Rec1)) to (p?global (indt Rec1))
% assuming
% - Rec1 and Rec2 are records with the same parameters
% - all projections in Rec2 are named,
% - if Proj2 projection with name Name in Rec2
% there is a projection Proj1 with the same name Name
% and a coercion from Proj1 to Proj2.
% - Depth is the number of (common) parameters between Rec1 and Rec2.
% Limitation: GR1 and GR2 have exactly one universe.
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I documented here the limitation

pred named-coe i:gref, i:gref, o:term, o:int.
named-coe GR1 GR2 Coe Depth :-
GR1 = indt Rec1, GR2 = indt Rec2, !,
std.do! [
coq.env.projections Rec1 OptProjs1,
coq.env.projections Rec2 OptProjs2,
std.map OptProjs1 (op\ gr\ sigma P\ op = some P, gr = const P) Projs1,
std.map OptProjs2 (op\ gr\ sigma P\ op = some P, gr = const P) Projs2,
coq.gref.list->string-map Projs1 ProjMap1,
coq.gref.list->string-map Projs2 ProjMap2,
coq.gref.string-map.domain ProjMap1 NameSet1,
coq.gref.string-map.domain ProjMap2 NameSet2,
std.assert! (std.string.set.subset NameSet2 NameSet1)
"The second record names is not a subset of the first one names",
coq.env.indt Rec1 _ _ _ Ty1 _ _,
coq.env.indt Rec2 _ _ _ _ [Build2] _,
named-coe.rec (indt Rec1) ProjMap1 Projs2 [] (indc Build2) Ty1 Coe Depth
].
named-coe Rec1 Rec2 _ _ :-
coq.error "Either of the following are not records: " Rec1 Rec2.

pred named-coe.rec i:gref, i:std.string.map gref, i:list gref, i:list term,
i:gref, i:term, o:term, o:int.
named-coe.rec SrcTy ProjMap1 Projs2 RevCommonArgs Build
(prod N A B) (fun N A Coe) NewDepth :-
@pi-decl N A x\
named-coe.rec SrcTy ProjMap1 Projs2
[x|RevCommonArgs] Build (B x) (Coe x) Depth,
NewDepth is Depth + 1.

named-coe.rec SrcTy ProjMap1 Projs2 RevCommonArgs Build _
(fun `src` SrcTyArgs Coe) 0 :- !,
std.rev RevCommonArgs CommonArgs,
coq.mk-app {coq.env.global SrcTy} CommonArgs SrcTyArgs,
@pi-decl `src` SrcTyArgs src\
sigma CommonArgsSrc Projs1 Args \ std.do! [
std.append CommonArgs [src] CommonArgsSrc,
std.map Projs2 (p\ out\ sigma Name\ coq.gref->id p Name,
std.string.map.find Name ProjMap1 out) Projs1,
std.map Projs1 (p\ out\ sigma T\ coq.env.global p T,
coq.mk-app T CommonArgsSrc out) Args,
coq.mk-app {coq.env.global Build} {std.append CommonArgs Args} (Coe src)
].

pred subst-univ i:univ, i:term, o:term.
subst-univ U T T' :-
coq.univ.variable U L,
coq.univ-instance UI [L],
(copy (sort (typ _)) (sort (typ U)),
pi x\ copy (pglobal x _) (pglobal x UI)) => copy T T'.

pred add-named-coe i:id, i:gref, i:gref, o:constant.
add-named-coe Name GR1 GR2 C :-
coq.env.univpoly? GR1 NU1,
coq.env.univpoly? GR2 NU2,
NU1 = NU2, NU1 = 1, !, std.do! [
named-coe GR1 GR2 CoeSkel Depth,
std.assert-ok! (coq.elaborate-skeleton CoeSkel _CoeWUTy CoeWU)
"ill-typed coercion",
coq.univ.new U,
coq.univ.variable U L,
subst-univ U CoeWU Coe,
@keepunivs! => std.assert-ok! (coq.typecheck Coe CoeTy) "wrong universes",
@udecl! [L] ff [] ff => coq.env.add-const Name Coe CoeTy @transparent! C,
@global! => coq.coercion.declare
(coercion (const C) Depth GR1 (grefclass GR2))
].
add-named-coe _ GR1 GR2 _ :-
coq.error GR1 "and" GR2 "do not have the same number of universe variables, or is different from 1".

} % util
146 changes: 24 additions & 122 deletions theories/Hierarchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -129,10 +129,12 @@ Elpi Accumulate lp:{{
% - a covariant (A to B) instance of one of the classes of Map listed above;
% - a contravariant (B to A) instance.
% (projections are generated so that all fields are accessible from the top record)
pred generate-module i:param-class, i:univ, i:univ.variable.
generate-module (pc M N as Class) U L :-
pred generate-module i:param-class.
generate-module (pc M N as Class) :-
coq.univ.new U,
coq.univ.variable U L,
% open module
coq.env.begin-module {param-class->add-suffix Class "Param"} none,
coq.env.begin-module {param-class.add-suffix Class "Param"} none,
% generate record
coq.univ-instance UI [L],
map->class M CovariantSubRecord,
Expand All @@ -149,46 +151,16 @@ Elpi Accumulate lp:{{
(app [pglobal ContravariantSubRecord UI, b, a, app [pglobal SymRel UI, a, b, r]]) (_\
end-record)))),
@primitive! => @udecl! [L] ff [] ff => coq.env.add-indt RelDecl TrocqInd,coq.env.indt TrocqInd _ _ _ _ [TrocqBuild] _,
Rel = indt TrocqInd,
coq.env.projections TrocqInd
[some CR, some CovariantProj, some ContravariantProj],
% add R to database for later use
R = const CR,
coq.elpi.accumulate _ "trocq.db"
(clause _ (after "default-r") (trocq.db.r Class CR)),
coq.elpi.accumulate execution-site "trocq.db"
(clause _ _ (trocq.db.gref->class (indt TrocqInd) Class)),
coq.elpi.accumulate execution-site "trocq.db"
(clause _ _ (trocq.db.rel Class (indt TrocqInd) (indc TrocqBuild)
(const CR) (const CovariantProj) (const ContravariantProj))),
% generate projections on the covariant subrecord
map-class->fields M MFields,
CovariantSubRecord = indt CovariantSubRecordIndt,
coq.env.projections CovariantSubRecordIndt MSomeProjs,
Covariant = const CovariantProj,
std.forall2 MFields MSomeProjs (field-name\ some-pr\ sigma Decl Pr\
some-pr = some Pr,
Decl =
(fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\ fun `P` (app [pglobal Rel UI, a, b]) p\
app [pglobal (const Pr) UI, a, b,
app [pglobal R UI, a, b, p], app [pglobal Covariant UI, a, b, p]]),
@udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _
),
% generate projections on the contravariant subrecord
map-class->cofields N NCoFields,
Contravariant = const ContravariantProj,
ContravariantSubRecord = indt ContravariantSubRecordIndt,
coq.env.projections ContravariantSubRecordIndt NSomeProjs,
std.forall2 NCoFields NSomeProjs (field-name\ some-pr\ sigma Decl Pr\
some-pr = some Pr,
Decl =
(fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
fun `P` (app [pglobal Rel UI, a, b]) p\
app [pglobal (const Pr) UI, b, a,
app [pglobal SymRel UI, a, b, app [pglobal R UI, a, b, p]],
app [pglobal Contravariant UI, a, b, p]]),
@udecl! [L] ff [] ff => coq.env.add-const field-name Decl _ @transparent! _
),
% close module
coq.env.end-module _.
}}.
Expand All @@ -198,106 +170,36 @@ Elpi Typecheck.
(* Record Weakening *)
(********************)

Coercion forgetMap43@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map4.Has@{i} R) : Map3.Has@{i} R :=
@Map3.BuildHas A B R (@Map4.map A B R m) (@Map4.map_in_R A B R m) (@Map4.R_in_map A B R m).

Coercion forgetMap32a@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2a.Has@{i} R :=
@Map2a.BuildHas A B R (@Map3.map A B R m) (@Map3.map_in_R A B R m).

Coercion forgetMap32b@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map3.Has@{i} R) : Map2b.Has@{i} R :=
@Map2b.BuildHas A B R (@Map3.map A B R m) (@Map3.R_in_map A B R m).

Coercion forgetMap2a1@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2a.Has@{i} R) : Map1.Has@{i} R :=
@Map1.BuildHas A B R (@Map2a.map A B R m).

Coercion forgetMap2b1@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map2b.Has@{i} R) : Map1.Has@{i} R :=
@Map1.BuildHas A B R (@Map2b.map A B R m).
Elpi Query lp:{{
std.forall {map-classes all} m\ sigma SubClasses\
map-class.weakenings-from m SubClasses,
std.forall SubClasses m'\ sigma Name GR GR'\
map->class m GR, map->class m' GR',
map-class.add-2-suffix "" m m' "forgetMap" Name,
util.add-named-coe Name GR GR' _.
}}.

Coercion forgetMap10@{i}
{A B : Type@{i}} {R : A -> B -> Type@{i}} (m : Map1.Has@{i} R) : Map0.Has@{i} R :=
@Map0.BuildHas A B R.
(* generate the hierarchy *)
Elpi Query lp:{{ std.forall {param-classes all} generate-module. }}.

Elpi Accumulate lp:{{
% generate 2 functions of weakening per possible weakening:
% one on the left and one on the right, if possible
pred generate-forget i:param-class, i:univ, i:univ.variable.
generate-forget (pc M N as Class) U L :-
coq.univ-instance UI [L],
map->class M MGR,
map->class N NGR,
trocq.db.rel Class RelMN _ RMN CovariantMN ContravariantMN,
% covariant weakening
std.forall {map-class.weakenings-from M} (m1\
sigma BuildRelM1N ForgetMapM Decl ForgetName ForgetCst M1GR RelM1N\
std.do! [
map->class m1 M1GR,
trocq.db.rel (pc m1 N) RelM1N BuildRelM1N _ _ _,
coq.coercion.db-for (grefclass MGR) (grefclass M1GR) [pr ForgetMapM _],
Decl =
(fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
fun `P` (app [pglobal RelMN UI, a, b]) p\
app [pglobal BuildRelM1N UI, a, b, app [pglobal RMN UI, a, b, p],
app [pglobal ForgetMapM UI, a, b, app [pglobal RMN UI, a, b, p],
app [pglobal CovariantMN UI, a, b, p]],
app [pglobal ContravariantMN UI, a, b, p]]),
param-class->add-2-suffix "_" Class (pc m1 N) "forget_" ForgetName,
@udecl! [L] ff [] ff =>
coq.env.add-const ForgetName Decl _ @transparent! ForgetCst,
@global! => coq.coercion.declare
(coercion (const ForgetCst) 2 RelMN (grefclass RelM1N))
]),
% contravariant weakening
SymRel = {sym-rel},
std.forall {map-class.weakenings-from N} (n1\
sigma BuildRelMN1 ForgetMapN Decl ForgetName ForgetCst N1GR RelMN1\
pred generate-forget i:param-class.
generate-forget Class :-
trocq.db.rel Class RelMN _ _ _ _,
std.forall {param-class.weakenings-from Class} (c\
sigma ForgetName RelMN'\
std.do! [
map->class n1 N1GR,
trocq.db.rel (pc M n1) RelMN1 BuildRelMN1 _ _ _,
coq.coercion.db-for (grefclass NGR) (grefclass N1GR) [pr ForgetMapN _],
Decl =
(fun `A` (sort (typ U)) a\ fun `B` (sort (typ U)) b\
fun `P` (app [pglobal RelMN UI, a, b]) p\
app [pglobal BuildRelMN1 UI, a, b, app [pglobal RMN UI, a, b, p],
app [pglobal CovariantMN UI, a, b, p],
app [pglobal ForgetMapN UI, b, a,
app [pglobal SymRel UI, a, b, app [pglobal RMN UI, a, b, p]],
app [pglobal ContravariantMN UI, a, b, p]]]),
param-class->add-2-suffix "_" Class (pc M n1) "forget_" ForgetName,
@udecl! [L] ff [] ff =>
coq.env.add-const ForgetName Decl _ @transparent! ForgetCst,
@global! => coq.coercion.declare
(coercion (const ForgetCst) 2 RelMN (grefclass RelMN1))
param-class.add-2-suffix "_" Class c "forget_" ForgetName,
trocq.db.rel c RelMN' _ _ _ _,
util.add-named-coe ForgetName RelMN RelMN' _
]).
}}.
Elpi Typecheck.

(* generate the hierarchy *)
Elpi Query lp:{{
coq.univ.new U,
coq.univ.variable U L,
map-classes all Classes,
std.forall Classes (m\
std.forall Classes (n\
generate-module (pc m n) U L
)
).
}}.
Elpi Query lp:{{ std.forall {param-classes all} generate-forget. }}.

Elpi Query lp:{{
coq.univ.new U,
coq.univ.variable U L,
map-classes all Classes,
std.forall Classes (m\
std.forall Classes (n\
generate-forget (pc m n) U L
)
).
}}.
(* Set Printing Universes. Print Module Param2a3. *)
(* Set Printing Universes. Print forget_42b_41. *)
(* Check forall (p : Param44.Rel nat nat), @paths (Param12a.Rel nat nat) p p. *)
Expand Down