wip: infer(P = "_ -> _")

Author: gares

HB/common/utils.elpi

@@ -158,9 +158,11 @@ w-params.fold.params (w-params.cons ID PTy F) Cons Nil RevPs Out :- !, std.do! [
   coq.id->name ID N,
   (@pi-decl N PTy p\ w-params.fold.params (F p) Cons Nil [p|RevPs] (Body p)),
   Cons N PTy Body Out].
-w-params.fold.params (w-params.nil ID TTy F) _ Nil RevParams Out :- !,
+w-params.fold.params (w-params.nil ID TTy F) _ Nil RevParams Out :- !, std.do! [
   coq.id->name ID N,
-  std.rev RevParams Params, !, Nil Params N TTy F Out.
+  std.rev RevParams Params,
+  Nil Params N TTy F Out,
+].
 
 % [w-params.then AwP Cons Nil Out] states that Out has shape
 %   Cons `x_1` T_1 p_1 \ .. \ Nil [p_1 .. p_n] `T` Ty t \ Body

HB/structure.elpi

@@ -542,6 +542,9 @@ mk-infer T (w-params.nil _ _ _) PH :- phant.init T PH.
 mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "Type" ; get-option ID ""), !,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
   phant.fun-infer-type sortclass {coq.id->name ID} Ty PhT R.
+mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "_ -> _"), !,
+  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
+  phant.fun-infer-type funclass {coq.id->name ID} Ty PhT R.
 mk-infer T (w-params.cons ID Ty W) R :- not (get-option ID _), !,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
   phant.fun-real {coq.id->name ID} Ty PhT R.

structures.v

@@ -336,7 +336,7 @@ Elpi Accumulate File "HB/structure.elpi".
 Elpi Accumulate Db hb.db.
 Elpi Accumulate lp:{{
 
-main [const-decl N (some B) _] :- with-attributes (structure.declare N B).
+main [const-decl N (some B) _] :- !, with-attributes (structure.declare N B).
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 }}.
 Elpi Typecheck.

tests/funclass.v

@@ -50,3 +50,10 @@ HB.instance Definition x5 :=
 
 Check Monoid.on mult.
 
+
+HB.mixin Record silly T := { xx : T }.
+#[verbose, infer(F = "_ -> _")]
+HB.structure Definition wp T (F : Monoid.type T) := { A of silly A }.
+
+Check forall w : wp.type mult, w = w.
+