Make first argument optional

Author: proux01

HB/howto.elpi

@@ -12,6 +12,10 @@ 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 :-
   private.mixins-on-gref GR 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.list-diff MLTgt MLSrc ML,
   if (ML = []) (coq.say "HB: nothing to do.")

structures.v

@@ -303,6 +303,8 @@ Elpi Export HB.about.
     to equip a type [T] with a structure [Foo.type], taking into account
     structures already instantiated on [T]. The search depth [d]
     is the maximum length of the sequences, 3 by default.
+    The first argument [T] is optional, when ommited [Foo.type] is built
+    from scratch.
 *)
 
 #[arguments(raw)] Elpi Command HB.howto.
@@ -325,8 +327,12 @@ main [str T, str STgt] :- !,
   with-attributes (with-logging (howto.main-str T STgt 3)).
 main [str T, str STgt, int Depth] :- !,
   with-attributes (with-logging (howto.main-str T STgt Depth)).
+main [str STgt] :- !,
+  with-attributes (with-logging (howto.main-from [] STgt 3)).
+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> [<search depth>].".
 }}.
 Elpi Typecheck.
 Elpi Export HB.howto.

tests/howto.v

@@ -2,6 +2,10 @@ From Coq Require Import ZArith ssrfun ssreflect.
 From HB Require Import structures.
 From HB Require Import demo1.hierarchy_5.
 
+HB.howto Ring.type.
+
+HB.howto Ring.type 2.
+
 HB.howto Z Ring.type.
 
 HB.howto Z Ring.type 2.

tests/howto.v.out

@@ -18,6 +18,26 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
     - AddAG_of_TYPE; SemiRing_of_AddComoid
     - AddComoid_of_TYPE; Ring_of_AddComoid
 
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG
+    - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid
+    - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid
+    - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid
+
+HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):
+    - Ring_of_TYPE
+    - AddAG_of_TYPE; BiNearRing_of_AddMonoid
+    - AddAG_of_TYPE; Ring_of_AddAG
+    - AddAG_of_TYPE; SemiRing_of_AddComoid
+    - AddComoid_of_TYPE; Ring_of_AddComoid
+
 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):