disable eta

math-comp · Jun 29, 2021 · 45f33f8 · 45f33f8
1 parent e4c2899
commit 45f33f8
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 41 deletions.
diff --git a/HB/structure.elpi b/HB/structure.elpi
@@ -156,20 +156,22 @@ declare Module B :- std.do! [
 
   @global! => log.coq.notation.add-abbreviation "on" 1
     {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
-    OnAbbrev,
+    _OnAbbrev,
 
   log.coq.env.begin-module "EtaAndMixinExports" none,
 
   if (get-option "primitive" tt) true (
-    if-verbose (coq.say "HB: eta expanded instances"),
-    NewClauses => std.do! [
-      w-params.fold MLwP mk-fun
-        (private.mk-hb-eta.on Structure SortProjection OnAbbrev) EtaInstanceBody,
-      w-params.fold MLwP (mk-parameter explicit)
-        (private.mk-hb-eta.arity Structure ClassName SortProjection)
-        EtaInstanceArity,
-      instance.declare-const "_" EtaInstanceBody EtaInstanceArity _
-    ]),
+    true
+    % if-verbose (coq.say "HB: eta expanded instances"),
+    % NewClauses => std.do! [
+    %   w-params.fold MLwP mk-fun
+    %     (private.mk-hb-eta.on Structure SortProjection OnAbbrev) EtaInstanceBody,
+    %   w-params.fold MLwP (mk-parameter explicit)
+    %     (private.mk-hb-eta.arity Structure ClassName SortProjection)
+    %     EtaInstanceArity,
+    %   instance.declare-const "_" EtaInstanceBody EtaInstanceArity _
+    % ]
+    ),
 
   % std.flatten {std.map NewMixins mixin->factories} NewFactories,
   % NewClauses => std.forall NewFactories instance.declare-factory-sort-factory,
@@ -700,32 +702,32 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
   @pi-decl N Ty t\
     product->triples (B t) (Rest t) C.
 
-pred mk-hb-eta.on i:structure, i:term, i:abbreviation,
-  i:list term, i:name, i:term, i:A, o:term.
-mk-hb-eta.on Structure SortProjection OnAbbrev
-    Params NT _T _ (fun NT Ty Body) :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
-  @pi-decl NT Ty s\ sigma Tm\ std.do! [
-    coq.mk-app {{lib:@hb.eta}}
-      [_, {coq.mk-app SortProjection {std.append Params [s]}}]
-      Tm,
-    std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
-    coq.notation.abbreviation OnAbbrev [Tm] (Body s)
-  ]
-].
-
-pred mk-hb-eta.arity i:structure, i:classname, i:term, i:list term,
-  i:name, i:term, i:A, o:arity.
-mk-hb-eta.arity Structure ClassName SortProjection
-    Params NT _T _ Out :- !, std.do! [
-  coq.mk-app (global Structure) Params Ty,
-  (@pi-decl NT Ty s\ sigma Tm\ std.do! [
-    coq.mk-app {{lib:@hb.eta}}
-      [_, {coq.mk-app SortProjection {std.append Params [s]}}] Tm,
-    std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
-    coq.mk-app (global ClassName) {std.append Params [Tm]} (Concl s)
-  ]),
-  Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
-].
-
+% pred mk-hb-eta.on i:structure, i:term, i:abbreviation,
+%   i:list term, i:name, i:term, i:A, o:term.
+% mk-hb-eta.on Structure SortProjection OnAbbrev
+%     Params NT _T _ (fun NT Ty Body) :- !, std.do! [
+%   coq.mk-app (global Structure) Params Ty,
+%   @pi-decl NT Ty s\ sigma Tm\ std.do! [
+%     coq.mk-app {{lib:@hb.eta}}
+%       [_, {coq.mk-app SortProjection {std.append Params [s]}}]
+%       Tm,
+%     std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
+%     coq.notation.abbreviation OnAbbrev [Tm] (Body s)
+%   ]
+% ].
+% 
+% pred mk-hb-eta.arity i:structure, i:classname, i:term, i:list term,
+%   i:name, i:term, i:A, o:arity.
+% mk-hb-eta.arity Structure ClassName SortProjection
+%     Params NT _T _ Out :- !, std.do! [
+%   coq.mk-app (global Structure) Params Ty,
+%   (@pi-decl NT Ty s\ sigma Tm\ std.do! [
+%     coq.mk-app {{lib:@hb.eta}}
+%       [_, {coq.mk-app SortProjection {std.append Params [s]}}] Tm,
+%     std.assert-ok! (coq.typecheck Tm _) "HB: eta illtyped",
+%     coq.mk-app (global ClassName) {std.append Params [Tm]} (Concl s)
+%   ]),
+%   Out = parameter {coq.name->id NT} explicit Ty s\ arity (Concl s)
+% ].
+% 
 }}
diff --git a/shim/structures.v b/shim/structures.v
@@ -8,4 +8,3 @@ Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition nomsg : error_msg := NoMsg.
 Definition is_not_canonically_a x := IsNotCanonicallyA x.
 Definition new {T} (x : T) := x.
-Definition eta {T} (x : T) := x.
diff --git a/structures.v b/structures.v
@@ -9,7 +9,6 @@ Definition id_phant {T} {t : T} (x : phantom T t) := x.
 Definition nomsg : error_msg := NoMsg.
 Definition is_not_canonically_a x := IsNotCanonicallyA x.
 Definition new {T} (x : T) := x.
-Definition eta {T} (x : T) := x.
 
 (* ********************* structures ****************************** *)
 From elpi Require Import elpi.
@@ -30,7 +29,6 @@ Register Coq.ssr.ssreflect.Phantom as hb.Phantom.
 Register Coq.Init.Logic.eq as hb.eq.
 Register Coq.Init.Logic.eq_refl as hb.erefl.
 Register new as hb.new.
-Register eta as hb.eta.
 
 #[deprecated(since="HB 1.0.1", note="use #[key=...] instead")]
 Notation indexed T := T (only parsing).

diff --git a/tests/factory_sort_tac.v b/tests/factory_sort_tac.v
@@ -14,6 +14,7 @@ HB.structure Definition AB := {T of hasA T & hasB T}.
 
 HB.factory Record hasAB T := { a : T; b : T * T }.
 HB.builders Context T of hasAB T.
+
 Definition xxx := AB.pack T (hasB.Build T b) (hasA.Build T a).
 HB.instance Definition _ := AB.copy T xxx.
 HB.end.
@@ -66,6 +67,10 @@ exact:
 P AB.
 Qed.
 
+Check forall T : AB.type,
+  let x := AB.pack T in
+  x.
+
 Goal forall T (a b : T), G.
 Proof.
 move=> T a b.