From 7833a9826aa950492e799407b9d3c5be3f8e4455 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 5 Jan 2024 09:40:46 +0100 Subject: [PATCH] Generic coercion code --- elpi/param-class.elpi | 44 ++++++++++--- elpi/util.elpi | 114 +++++++++++++++++++++++++++++++++ theories/Hierarchy.v | 146 +++++++----------------------------------- 3 files changed, 172 insertions(+), 132 deletions(-) diff --git a/elpi/param-class.elpi b/elpi/param-class.elpi index 1250c15..7388d07 100644 --- a/elpi/param-class.elpi +++ b/elpi/param-class.elpi @@ -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 []. @@ -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 []. @@ -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 :- diff --git a/elpi/util.elpi b/elpi/util.elpi index 8dc57d2..04599ff 100644 --- a/elpi/util.elpi +++ b/elpi/util.elpi @@ -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. +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 diff --git a/theories/Hierarchy.v b/theories/Hierarchy.v index 241e99b..28ce095 100644 --- a/theories/Hierarchy.v +++ b/theories/Hierarchy.v @@ -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, @@ -149,11 +151,9 @@ 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" @@ -161,34 +161,6 @@ Elpi Accumulate lp:{{ 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 _. }}. @@ -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. *)