use primproj for class->mixin builders

Author: gares

HB/about.elpi

@@ -41,7 +41,7 @@ main-located S (loc-abbreviation A) :-
   coq.safe-dest-app T (global GR) _, !,
   main-located S (loc-gref GR).
 
-main-located S (loc-gref GR) :- from Factory Mixin GR, !,
+main-located S (loc-gref GR) :- from Factory Mixin (gref GR), !,
   private.main-builder S Factory Mixin.
 
 main-located S (loc-gref GR) :-

HB/builders.elpi

@@ -79,7 +79,7 @@ pred declare-1-builder i:builder, i:list prop, o:list prop.
 declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- FromClauses => from SrcFactory TgtMixin _, !,
   if-verbose (coq.say {header} "skipping duplicate builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
-declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin B|FromClauses] :-
+declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin (gref B)|FromClauses] :-
   if-verbose (coq.say {header} "declare builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
 

HB/common/database.elpi

@@ -11,8 +11,8 @@ from_factory (from X _ _) X.
 pred from_mixin i:prop, o:mixinname.
 from_mixin (from _ X _) X.
 
-pred from_builder i:prop, o:term.
-from_builder (from _ _ X) (global X).
+pred from_builder i:prop, o:gref-or-primitive.
+from_builder (from _ _ X) X.
 
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
@@ -104,12 +104,18 @@ factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [
   std.map2 BL ML (factory-provides.one Params T) MLwP,
 ].
 
-pred factory-provides.one i:list term, i:term, i:term, i:mixinname, o:w-args mixinname.
-factory-provides.one Params T B M (triple M PL T) :- std.do! [
-  std.assert-ok! (coq.typecheck B Ty) "Builder illtyped",
+pred factory-provides.one i:list term, i:term, i:gref-or-primitive, i:mixinname, o:w-args mixinname.
+factory-provides.one Params T (gref B) M (triple M PL T) :- std.do! [
+  coq.env.typeof B Ty,
   subst-prod [T] {subst-prod Params Ty} TyParams,
   std.assert! (extract-conclusion-params T TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins",
 ].
+factory-provides.one Params T (primitive (pr P N)) M (triple M PL T) :- std.do! [
+  coq.mk-app {coq.mk-app (global M) Params} [T] TyM, % fine since M is the class hence no extra arg needed
+  std.assert-ok! (d\@pi-decl `m` TyM m\coq.typecheck (app[primitive(proj P N),m]) (TyParams m) d) "Builder illtyped",
+  @pi-decl `m` TyM m\
+    std.assert! (extract-conclusion-params T (TyParams m) PL) "The conclusion of a primitive projection is a mixin whose parameters depend on other mixins"
+].
 
 pred extract-conclusion-params i:term, i:term, o:list term.
 extract-conclusion-params TheType (prod _ S T) R :- !,

HB/common/stdpp.elpi

@@ -270,6 +270,11 @@ coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [
   std.map2-filter Ps PPs (x\y\gr\sigma c\x = some c, y = some (pr N J), gr = const c) [GR],
 ].
 
+%hack/ fixup API
+:before "subst-fun:fail"
+coq.subst-fun L (primitive (proj _ _) as F) (app[F|L]).
+
+
 pred cs-pattern->name i:cs-pattern, o:string.
 cs-pattern->name cs-prod "prod".
 cs-pattern->name (cs-sort _) "sort".

HB/common/synthesis.elpi

@@ -223,13 +223,15 @@ mixin-for_mixin-builder (mixin-for _ _ B) B.
 % and fills in all the mixins required by the builder using mixin-src, obtaining
 % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt)
 pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
-builder->term Ps T Src Tgt B :- !, std.do! [
-  from Src Tgt FGR,
+builder->term Ps T Src Tgt B :- from Src Tgt (gref FGR), !, std.do! [
   F = global FGR,
   gref-deps Src MLwP,
   list-w-params_list MLwP ML,
   infer-all-these-mixin-args Ps T ML F B,
 ].
+builder->term _ _ Src Tgt (primitive (proj P N)) :-
+  % no deps, Src is a class
+  from Src Tgt (primitive (pr P N)).
 
 % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that
 % if    F  ~  fun xs (m_0 : M_0 T) .. (m_n : M_n T ..) ys

HB/factory.elpi

@@ -165,7 +165,7 @@ cdecl->w-mixins.mixins (context-item ID _ TySkel none Rest) Out :- !,
 
 % The identity builder
 pred declare-id-builder i:factoryname, o:prop.
-declare-id-builder GR (from GR GR (const C)) :- std.do! [
+declare-id-builder GR (from GR GR (gref (const C))) :- std.do! [
   gref-deps GR GRD,
   synthesis.mixins-w-params.fun GRD (declare-id-builder.aux GR) IDBodySkel,
   std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped",

HB/instance.elpi

@@ -406,7 +406,7 @@ optimize-class-body _ _ (app L) (app L) [].
 pred declare-mixin-name i:term, o:term, o:list prop.
 declare-mixin-name (global _ as T) T [].
 declare-mixin-name T (global GR) [] :- mixin-mem T GR.
-declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt).
+declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ (gref GR)), not (get-option "hnf" tt).
 declare-mixin-name T (global (const C)) [mixin-mem T (const C)] :- std.do! [
   Name is "HB_unnamed_mixin_" ^ {std.any->string {new_int}},
   if-verbose (coq.say {header} "Giving name" Name "to mixin instance" {coq.term->string T}),

HB/status.elpi

@@ -43,10 +43,14 @@ print-hierarchy :- std.do! [
 namespace private {
 
 pred pp-from i:prop.
-pp-from (from F M T) :-
+pp-from (from F M (gref T)) :-
   coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
   coq.say "  " {coq.term->string (global T)},
   coq.say "".
+pp-from (from F M (primitive (pr P N))) :-
+  coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)},
+  coq.say "  " P " (" N "th field)",
+  coq.say "".
 
 pred pp-list-w-params i:mixins, i:term.
 pred pp-list-w-params.list-triple i:list (w-args mixinname), i:term.

HB/structure.elpi

@@ -309,6 +309,11 @@ export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do
   std.map LMwPToExport w-params_1 MLToExport,
 ].
 
+pred mk-app-builder i:list term, i:term, i:gref-or-primitive, o:term.
+mk-app-builder Params TheType (gref B) T :-
+  coq.mk-app {coq.env.global B} {std.append Params [TheType]} T.
+mk-app-builder _ _ (primitive (pr P N)) (primitive(proj P N)).
+
 pred mk-coe-class-body
   i:factoryname, % From class
   i:factoryname, % To class
@@ -321,14 +326,14 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
 
   list-w-params_list TMLwP TML,
   std.map TML (from FC) Builders,
-  std.map Builders (x\r\mk-app (global x) Params r) BuildersP,
+  std.map Builders (mk-app-builder Params T) BuildersP,
 
   factory-nparams TC TCNP,
   mk-app (global {get-constructor TC})
     {coq.mk-n-holes TCNP} KCHoles,
 
   (pi c\ sigma Mixes\
-    std.map BuildersP (builder\r\ r = app[builder, T, c]) Mixes,
+    std.map BuildersP (builder\r\ r = app[builder, c]) Mixes,
     mk-app KCHoles [T | Mixes] (ClassCoercion c)),
 
   CoeBody = {{ fun (c : lp:Class) => lp:(ClassCoercion c) }}
@@ -497,12 +502,12 @@ declare-class+structure MLwP Sort
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
 
-  coq.env.projections ClassInd Projs,
+  coq.env.primitive-projections ClassInd Projs,
   % TODO: put this code in a named clause
   w-params.nparams MLwP NParams,
   std.map2 {list-w-params_list MLwP} Projs (m\ p\ r\ sigma P\
     std.assert! (p = some P) "BUG: we build a class with an anonymous field",
-    r = from (indt ClassInd) m (const P)) Factories,
+    r = from (indt ClassInd) m (primitive P)) Factories,
   AllFactories = [factory-nparams (indt ClassInd) NParams | Factories],
 
   if-verbose (coq.say {header} "declare type record"),

structures.v

@@ -109,13 +109,19 @@ pred class-def o:class.
 
 %%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% [from FN MN F] invariant:
-% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
-%  - LMN1 and LMN2 are sub lists of LMN
-%  - c1 .. cm are terms built using p1 .. pn and T
+% [from FN MN B] invariant:
+% - B = gref F
+%   "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where
+%    - LMN1 and LMN2 are sub lists of LMN
+%    - c1 .. cm are terms built using p1 .. pn and T
+% - B = primitive (pr P N)
+%    - as above but no parameters
 % - [factory-requires FN LMN]
 % [from _ M _] tests whether M is a declared mixin.
-pred from o:factoryname, o:mixinname, o:gref.
+kind gref-or-primitive type.
+type gref gref -> gref-or-primitive.
+type primitive pair projection int -> gref-or-primitive.
+pred from o:factoryname, o:mixinname, o:gref-or-primitive.
 
 %%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%