Support grefclass

Author: proux01

HB/common/phant-abbreviation.elpi

@@ -92,7 +92,10 @@ fun-infer-type funclass N Ty (t\private.phant-term AL (Bo t)) Out :-
   coq.name-suffix N "ph" PhN,
   fun-implicit N Ty (t\private.phant-term [private.infer-type N funclass|AL]
                                           (fun PhN {{ lib:@hb.phantom (_ -> _) lp:t }} _\ Bo t)) Out.
-fun-infer-type C _ _ _ _  :- coq.error "HB: inference of parameters of call" C "not implemented yet".
+fun-infer-type (grefclass Class) N Ty (t\private.phant-term AL (Bo t)) Out :-
+  coq.name-suffix N "ph" PhN, private.build-type-pattern Class Pat,
+  fun-implicit N Ty (t\private.phant-term [private.infer-type N (grefclass Class)|AL]
+                                          (fun PhN {{ lib:@hb.phantom lp:Pat lp:t }} _\ Bo t)) Out.
 
 % TODO: this looks like a hack to remove
 pred append-fun-unify i:phant-term, o:phant-term.
@@ -180,12 +183,25 @@ build-abbreviation K F [infer-type N sortclass|AL] K'' (fun N _ AbbrevFx) :- !,
 build-abbreviation K F [infer-type N funclass|AL] K'' (fun N _ AbbrevFx) :- !,
   pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom (_ -> _) lp:x }}]} AL K' (AbbrevFx x),
   K'' is K' + 1.
-build-abbreviation _ _ [infer-type _ (grefclass _)|_] _ _ :- coq.error "TODO".
+build-abbreviation K F [infer-type N (grefclass Class)|AL] K'' (fun N _ AbbrevFx) :- !,
+  build-type-pattern Class Pat,
+  pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom lp:Pat lp:x }}]} AL K' (AbbrevFx x),
+  K'' is K' + 1.
 build-abbreviation K F [implicit|AL] K' FAbbrev :- !,
   build-abbreviation K {mk-app F [_]} AL K' FAbbrev.
 build-abbreviation K F [unify|AL] K' FAbbrev :- !,
   build-abbreviation K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev.
 
+% [build-type-pattern GR Pat] cheks that GR : forall x_1 ... x_n, Type
+% and returns Pat = GR _ ... _ (that is GR  applied to n holes).
+% Note that n can be 0 when GR : Type.
+pred build-type-pattern i:gref, o:term.
+build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat.
+build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !,
+  @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat.
+build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !.
+build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
+
 
 % [mk-phant-term F PF] states that
 % if F = fun p1 .. p_k T m_0 .. m_n => _

HB/common/synthesis.elpi

@@ -154,8 +154,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
   @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
 infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
 infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass.
-infer-coercion-tgt (w-params.nil _ _ _) _ :-
-  coq.error "HB: coercion not to Sortclass or Funclass not supported yet.".
+infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.
 
 pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.
 w-args.check-key _PS _T [] true :- !.

_CoqProject.test-suite

@@ -63,6 +63,7 @@ tests/exports2.v
 tests/log_impargs_record.v
 tests/compress_coe.v
 tests/funclass.v
+tests/grefclass.v
 tests/local_instance.v
 tests/lock.v
 tests/interleave_context.v

tests/grefclass.v

@@ -0,0 +1,12 @@
+From HB Require Import structures.
+
+Definition pred T := T -> bool.
+
+HB.mixin Record isPredNat (f : pred nat) := {}.
+
+HB.structure Definition PredNat := {f of isPredNat f}.
+
+Section TestSort.
+Variable p : PredNat.type.
+Check p : pred nat.
+End TestSort.