fix #386

.nix/config.nix

@@ -22,7 +22,7 @@
     };
   in {
     "coq-master".coqPackages = mcHBcommon // {
-      coq.override.version = "master";
+      coq.override.version = "proux01:ssrmatching_primitive_proj";
       coq-elpi.override.version = "coq-master";
       bignums.override.version = "master";
       paramcoq.override.version = "master";

HB/about.elpi

@@ -26,7 +26,7 @@ main-located S (loc-gref (indt I)) :- factory-constructor (indt I) _, !,
 main-located S (loc-gref (const C)) :- factory-constructor (const C) _, !,
   private.main-factory-alias S C.
 
-main-located S (loc-gref (const C)) :- exported-op M _ C, !,
+main-located S (loc-gref (const C)) :- exported-op M _ _ C, !,
   private.main-operation S M C.
 
 main-located S (loc-gref GR) :- factory-alias->gref GR F, not (F = GR), !,
@@ -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) :-
@@ -189,8 +189,8 @@ main-structure S Class Structure MLwP :-
   list-w-params_list MLwP ML,
   std.map-filter ML (m\r\ sigma P O OPS\
     mixin-first-class m Class,
-    std.findall (exported-op m P O) OPS,
-    std.map OPS (c\out\ sigma p\ c = exported-op m p out) r) OPLL,
+    std.findall (exported-op m P _ O) OPS,
+    std.map OPS (c\out\ sigma p\ c = exported-op m p _ out) r) OPLL,
   std.flatten OPLL Operations,
   std.map {std.findall (sub-class Class CS_ CoeS_ NS_)}
     (x\r\ x = sub-class Class r _ _) SubClasses,
@@ -272,7 +272,7 @@ compute-arg-type (w-params.nil ID Ty Rest) F Acc [] ID FN [pr ID PPTy|Xs] :-
   @pi-parameter ID Ty x\ compute-arg-type.fields F {std.length (Rest x)} {std.rev [x|Acc]} Xs FN.
 pred compute-arg-type.fields i:list constant, i:int, i:list term, o:list (pair id coq.pp), o:list id.
 compute-arg-type.fields [] _ _ [] [].
-compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C OP, !,
+compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C _ OP, !,
   coq.env.typeof (const OP) Ty,
   coq.gref->id (const OP) ID,
   coq.subst-prod Args Ty TyArgs,

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

@@ -260,6 +260,21 @@ term->cs-pattern (sort U) (cs-sort U).
 term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
 term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
 
+%hack/missing API
+:before "stop:begin"
+coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [
+  coq.typecheck T Ty ok,
+  coq.term->gref Ty (indt I),
+  coq.env.projections I Ps,
+  coq.env.primitive-projections I PPs,
+  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",
@@ -231,8 +231,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-
-  if (get-option "primitive" tt)
+  % TODO cleanup
+  if (get-option "primitive" tt ; (not(get-option "primitive" ff) , not(Fields = end-record)))
     (@primitive! => log.coq.env.add-indt RDeclClosed R)
     (log.coq.env.add-indt RDeclClosed R),
 

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

@@ -198,19 +198,51 @@ shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra
 % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs
+pred copy-term i:term, o:term.
+copy-term X Y :- name X, !, X = Y, !. % avoid loading "copy-term x x" at binders
+copy-term (global _ as C) C :- !.
+copy-term (pglobal _ _ as C) C :- !.
+copy-term (sort _ as C) C :- !.
+copy-term (fun N T F) (fun N T1 F1) :- !,
+  copy-term T T1, @pi-decl N T1 x\ copy-term (F x) (F1 x).
+copy-term (let N T B F) (let N T1 B1 F1) :- !,
+  copy-term T T1, copy-term B B1, @pi-def N T1 B1 x\ copy-term (F x) (F1 x).
+copy-term (prod N T F) (prod N T1 F1) :- !,
+  copy-term T T1, (@pi-decl N T1 x\ copy-term (F x) (F1 x)).
+copy-term (app L) (app L1) :- !, std.map L copy-term L1.
+copy-term (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
+  copy-term Ty Ty1, @pi-decl N Ty1 x\ copy-term (F x) (F1 x).
+copy-term (match T Rty B) (match T1 Rty1 B1) :- !,
+  copy-term T T1, copy-term Rty Rty1, std.map B copy-term B1.
+copy-term (primitive _ as C) C :- !.
+copy-term (uvar M L as X) W :- var X, !, std.map L copy-term L1, coq.mk-app-uvar M L1 W.
+% when used in CHR rules
+copy-term (uvar X L) (uvar X L1) :- std.map L copy-term L1.
+
+
 pred clean-op-ty i:list prop, i:term, i:term, o:term.
-clean-op-ty [] _ T1 T2 :- copy T1 T2.
-clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
+clean-op-ty [] _ T1 T2 :- copy-term T1 T2.
+clean-op-ty [exported-op _ Po PrimPop C|Ops] S T1 T2 :-
   gref-deps (const Po) MLwP,
   w-params.nparams MLwP NParams,
   std.length {list-w-params_list MLwP} NMixins,
 
   (pi L L1 L2 Params Rest PoArgs\
-    copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
+    copy-term (app [global (const Po)| L]) (app [global (const C) | L2]) :-
       std.split-at NParams L Params [_|Rest],
       std.drop NMixins Rest PoArgs,
       std.append Params [S|PoArgs] L1,
-      std.map L1 copy L2) =>
+      std.map L1 copy-term L2) =>
+
+  (pi P N L1 L2 L3 TheMixin Params Ty\
+     % even if NMixins > 1, they are parameters of the primitive projection so
+     % they are not present
+     copy-term (app [primitive (proj P N), TheMixin|L1]) (app [global (const C) | L3]) :- PrimPop = some (pr P N), !,
+       coq.mk-n-holes NParams Params,
+       std.append Params [S|L1] L2,
+       std.map L2 copy-term L3,
+       std.assert-ok! (coq.typecheck (app [global (const C) | L3]) Ty) "clean-op-ty") =>
+
   clean-op-ty Ops S T1 T2.
 
 pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
@@ -237,9 +269,9 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par
 % same operation out of the package structure (out of the class field of the
 % structure). We also provide all the other mixin dependencies (other misins)
 % of the package structure.
-pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
-export-1-operation _ _ _ _ _ none EX EX :- !. % not a projection, no operation
-export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std.do! [
+pred export-1-operation i:mixinname, i:structure, i:term, i:term, i:one-w-params mixinname, i:option constant, i:option (pair projection int), i:list prop, o:list prop.
+export-1-operation _ _ _ _ _ none _ EX EX :- !. % not a projection, no operation
+export-1-operation M Struct Psort Pclass MwP (some Poperation) PrimPop EXI EXO :- !, std.do! [
   coq.gref->id (const Poperation) Name,
 
   w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),
@@ -253,15 +285,16 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
   std.map INI (_\r\ r = maximal) Implicits,
   @global! => log.coq.arguments.set-implicit (const C) [Implicits],
 
-  EXO = [exported-op M Poperation C|EXI]
+  EXO = [exported-op M Poperation PrimPop C|EXI]
 ].
 
 % Given a list of mixins, it exports all operations in there
 pred export-operations.aux i:structure, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
 export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [
   w-params_1 MwP (indt M),
   coq.env.projections M Poperations,
-  std.fold Poperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2,
+  coq.env.primitive-projections M PrimPoperations,
+  std.fold2 Poperations PrimPoperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2,
 ].
 
 pred mixin-not-already-declared i:one-w-params mixinname.
@@ -276,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
@@ -288,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) }}
@@ -464,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"),

_CoqProject.test-suite

@@ -95,7 +95,10 @@ tests/unit/close_hole_term.v
 tests/unit/struct.v
 tests/factory_when_notation.v
 
+tests/test_primproj_ty.v
+
 -R tests HB.tests
 -R examples HB.examples
 
+
 -Q . HB

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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -171,8 +177,8 @@ pred mixin-mem i:term, o:gref.
 % that contains the mixin M
 pred mixin-first-class o:mixinname, o:classname.
 
-% memory of exported operations (TODO: document fiels)
-pred exported-op o:mixinname, o:constant, o:constant.
+% memory of exported operations [exported-op Mixin MixinProj PrimitiveMixinProj StructureProj]
+pred exported-op o:mixinname, o:constant, o:option (pair projection int), o:constant.
 
 % memory of factory sort coercion
 pred factory-sort o:coercion.

tests/test_primproj_ty.v

@@ -0,0 +1,37 @@
+From Coq Require Import ssreflect ssrfun.
+From HB Require Import structures.
+
+#[primitive]
+HB.mixin Record AddMonoid_of_TYPE S := {
+  zero : S;
+  add : S -> S -> S;
+  addrA : associative add;
+  add0r : left_id zero add;
+  addr0 : right_id zero add;
+}.
+
+HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
+
+Goal let x := @addrA in True.
+match goal with
+| |- let x : forall s : AddMonoid.type, @associative (AddMonoid.sort s) (@add s) := @addrA in True => idtac "OK"
+end.
+Abort.
+
+#[primitive]
+HB.mixin Record Scale_of_AddMonoid (P : Type) S of AddMonoid_of_TYPE S := {
+  scale : P -> S -> S;
+  scaleBad : forall p (x y : S), (* HUMMM, if I don't put S here, it infers the eta expansion of S *)
+    scale p (add x y) = add (scale p x) (scale p y);
+}.
+
+About Scale_of_AddMonoid.scale.
+
+HB.structure Definition ScaleMonoid P := { A of Scale_of_AddMonoid P A }.
+
+Goal let a := @scaleBad in True.
+match goal with
+| |- let a : forall P (s : ScaleMonoid.type P), forall p : P, forall x y : ScaleMonoid.sort P s, scale p (add x y) = add (scale p x) (scale p y) := @scaleBad in True => idtac "OK"
+end.
+Abort.
+