kind of works

Author: gares

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), !,
@@ -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/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.

structures.v

@@ -171,8 +171,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

@@ -12,10 +12,26 @@ HB.mixin Record AddMonoid_of_TYPE S := {
 
 HB.structure Definition AddMonoid := { A of AddMonoid_of_TYPE A }.
 
-Set Printing All.
-
 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.
+