First argument can be another structure

Author: proux01

HB/howto.elpi

@@ -10,13 +10,17 @@ pred main-str i:string, i:string, i:int.
 main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth.
 
 pred main-gref i:gref, i:string, i:int.
+main-gref GR STgt Depth :- class-def (class _ GR _), !,
+  private.mixins-in-structures [GR] MLSrc,
+  main-from MLSrc STgt Depth.
 main-gref GR STgt Depth :-
-  private.mixins-on-gref GR MLSrc,
+  private.structures-on-gref GR SL,
+  private.mixins-in-structures SL MLSrc,
   main-from MLSrc STgt Depth.
 
 pred main-from i:list mixinname, i:string, i:int.
 main-from MLSrc STgt Depth :-
-  private.mixins-in-string STgt MLTgt,
+  private.mixins-in-structures [{coq.locate STgt}] MLTgt,
   private.list-diff MLTgt MLSrc ML,
   if (ML = []) (coq.say "HB: nothing to do.")
      (private.paths-from-for-step MLSrc ML Depth R,
@@ -59,20 +63,19 @@ lexi-order [] [].
 lexi-order [X1|_] [X2|_] :- lt-gref X1 X2.
 lexi-order [X|T1] [X|T2] :- lexi-order T1 T2.
 
-% [mixins-on-gref GR ML] list mixins in structures [GR] is equipped with
-pred mixins-on-gref i:gref, o:list mixinname.
-mixins-on-gref GR ML :-
+% [structures-on-gref GR ML] list structures [GR] is equipped with
+pred structures-on-gref i:gref, o:list structure.
+structures-on-gref GR SL :-
   std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV,
-  std.fold LV [] mixins-on-gref.aux ML.
-mixins-on-gref.aux (cs-instance _ _ GR) L L' :-
-  coq.prod-tgt->gref {coq.env.typeof GR} F,
-  class-def (class _ F MLWP),
-  union L {list-w-params_list MLWP} L'.
-
-% [mixins-in-string S ML] list mixins contained in structure [S]
-pred mixins-in-string i:string, o:list mixinname.
-mixins-in-string S ML :-
-  coq.locate S GR, class-def (class _ GR MLwP), list-w-params_list MLwP ML.
+  std.map LV structures-on-gref.aux SL.
+structures-on-gref.aux (cs-instance _ _ GR) F :-
+  coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _).
+
+% [mixins-in-structures SL ML] list mixins in structures [SL]
+pred mixins-in-structures i:list structure, o:list mixinname.
+mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML.
+mixins-in-structures.aux F L L' :-
+  class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'.
 
 % a type to store a factory along with the mixins it depends on
 % and the mixins it provides

structures.v

@@ -305,6 +305,8 @@ Elpi Export HB.about.
     is the maximum length of the sequences, 3 by default.
     The first argument [T] is optional, when ommited [Foo.type] is built
     from scratch.
+    Finally, the first argument can be another structure [Bar.type],
+    in which case [Foo.type] is built starting from [Bar.type].
 *)
 
 #[arguments(raw)] Elpi Command HB.howto.
@@ -332,7 +334,9 @@ main [str STgt] :- !,
 main [str STgt, int Depth] :- !,
   with-attributes (with-logging (howto.main-from [] STgt Depth)).
 
-main _ :- coq.error "Usage: HB.howto [(<type>)] <structure> [<search depth>].".
+main _ :-
+  coq.error
+    "Usage: HB.howto [(<type>)|<structure>] <structure> [<search depth>].".
 }}.
 Elpi Typecheck.
 Elpi Export HB.howto.

tests/howto.v

@@ -12,13 +12,17 @@ HB.howto Z Ring.type 2.
 
 Fail HB.howto Z Ring.type 0.
 
+HB.howto AddComoid.type Ring.type.
+
 HB.instance
   Definition _ :=
   AddAG_of_TYPE.Build Z 0%Z Z.add Z.opp
     Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l.
 
 HB.howto Z Ring.type.
 
+HB.howto AddAG.type Ring.type.
+
 HB.instance
   Definition _ :=
   Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul

tests/howto.v.out

@@ -40,6 +40,19 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
 
 The command has indeed failed with message:
 HB: no solution found, try to increase search depth.
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_AddComoid
+    - AddAG_of_AddComoid; BiNearRing_of_AddMonoid
+    - AddAG_of_AddComoid; Ring_of_AddAG
+    - AddAG_of_AddComoid; SemiRing_of_AddComoid
+    - BiNearRing_of_AddMonoid; AddAG_of_AddComoid
+    - SemiRing_of_AddComoid; AddAG_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - BiNearRing_of_AddMonoid
+    - Ring_of_AddAG
+    - SemiRing_of_AddComoid
+
 HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - BiNearRing_of_AddMonoid
     - Ring_of_AddAG