review

HB/structure.elpi

@@ -147,22 +147,22 @@ declare Module BSkel Sort :- std.do! [
     (if-verbose (coq.say {header} "could not declare the `on_`, `copy` and `on` abbreviations because the target of sort is not a coercion class"))
     (if-verbose (coq.say {header} "declaring on_ abbreviation"),
 
-    private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
+		private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
 
-    phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
-    (pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
+		phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
+		(pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
 
-    if-verbose (coq.say {header} "declaring `copy` abbreviation"),
+		if-verbose (coq.say {header} "declaring `copy` abbreviation"),
 
-    coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
-    @global! => log.coq.notation.add-abbreviation "copy" 2
-      {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
+		coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
+		@global! => log.coq.notation.add-abbreviation "copy" 2
+			{{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
 
-    if-verbose (coq.say {header} "declaring on abbreviation"),
+		if-verbose (coq.say {header} "declaring on abbreviation"),
 
-    @global! => log.coq.notation.add-abbreviation "on" 1
-      {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
-      _OnAbbrev),
+		@global! => log.coq.notation.add-abbreviation "on" 1
+			{{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
+			_OnAbbrev),
 
   log.coq.env.end-module-name Module ModulePath,
 
@@ -292,10 +292,9 @@ mk-sort-coercion-aux (prod _N _T Body) Structure P Args Clause :-
 mk-sort-coercion-aux _ Structure P Args Clause :-
   std.rev Args ArgsRev,
   Clause =
-    (pi ctx v t e r argsAll w\ (coercion ctx v t e r :-
-      coq.unify-eq t (app [Structure | ArgsRev]) ok,
+    (pi ctx v t e r argsAll w\ (coercion ctx v (app [Structure | ArgsRev]) e r :-
       std.append ArgsRev [v] argsAll,
-      mk-app P argsAll w,
+      coq.mk-app P argsAll w,
       coq.elaborate-skeleton w e r ok,
       coq.ltac.collect-goals r [] [])).
 
@@ -304,26 +303,25 @@ mk-sort-coercion Structure P Clause :-
   coq.typecheck Structure T ok,
   mk-sort-coercion-aux T Structure P [] Clause.
 
-pred mk-generic-coercion-aux i:term, i:term, i:term, i:list term, o:prop.
-mk-generic-coercion-aux (prod _N _T Body) Structure G Args Clause :-
+pred mk-reverse-coercion-aux i:term, i:term, i:term, i:list term, o:prop.
+mk-reverse-coercion-aux (prod _N _T Body) Structure G Args Clause :-
   Clause = (pi x\ C x),
-  pi x\ mk-generic-coercion-aux (Body x) Structure G [x | Args] (C x).
+  pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).
 
-mk-generic-coercion-aux _ Structure G Args Clause :-
+mk-reverse-coercion-aux _ Structure G Args Clause :-
   std.rev Args ArgsRev,
   Clause =
-    (pi ctx v t e r c argsAll w\ (coercion ctx v t e r :-
-      coq.unify-eq e (app [Structure | ArgsRev]) ok,
+    (pi ctx v t e r c argsAll w\ (coercion ctx v t (app [Structure | ArgsRev]) r :-
       std.append ArgsRev [v, c] argsAll,
-      mk-app G argsAll w,
+      coq.mk-app G argsAll w,
       coq.elaborate-skeleton w e r ok,
       coq.ltac.collect-goals r [] [])).
 
-pred mk-generic-coercion i:gref, o:prop.
-mk-generic-coercion Structure Clause :-
+pred mk-reverse-coercion i:gref, o:prop.
+mk-reverse-coercion Structure Clause :-
   coq.typecheck (global Structure) T ok,
   get-constructor Structure G,
-  mk-generic-coercion-aux T (global Structure) (global G) [] Clause.
+  mk-reverse-coercion-aux T (global Structure) (global G) [] Clause.
 
 pred mk-coe-class-body
   i:factoryname, % From class
@@ -514,7 +512,6 @@ declare-class+structure MLwP Sort
 
   w-params.then MLwP (mk-parameter explicit) (mk-parameter explicit)
     synthesize-fields.body ClassDeclaration,
-  coq.say "ClassDeclaration" ClassDeclaration,
 
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),
@@ -560,14 +557,14 @@ declare-sort-coercion-elpi Structure Proj :-
   mk-sort-coercion Structure Proj Clause,
   coq.elpi.accumulate _ "coercion.db" (clause _ _ Clause).
 
-% Declares "generic_type" as a Coercion in elpi's coercion db
+% Declares a reverse coercion for the sort projection in elpi's coercion db
 pred declare-generic-coercion-elpi i:gref.
 declare-generic-coercion-elpi Structure :-
 
-  if-verbose (coq.say {header} "declare `generic_type` coercion in elpi"),
+  if-verbose (coq.say {header} "declare reverse coercion in elpi"),
 
   %TODO: log.coq.coercion-elpi.declare 
-  mk-generic-coercion Structure Clause,
+  mk-reverse-coercion Structure Clause,
   coq.elpi.accumulate _ "coercion.db" (clause _ _ Clause).
 
 

tests/coercion.v

@@ -0,0 +1,14 @@
+From Coq Require Import ssreflect.
+From HB Require Import structures.
+
+HB.mixin Record isSigma (T : Type) (P : T -> Prop) (x : T) := {
+  _ : P x
+}.
+
+#[short(type="sigType"), verbose]
+HB.structure Definition Sig (T : Type) (P : T -> Prop) := {x of isSigma T P x}.
+
+Check fun (T : Type) (P : T -> Prop) (x : sigType T P) => x : T.
+Check fun (T : Type) (P : T -> Prop) (x : T) (Px : Sig T P x) => x : sigType T P.
+Fail Check fun (T : Type) (P : T -> Prop) (x : T) => x : sigType T P.
+