From 2dfc068f8e382bd74a5d9ba1da8da04c56d6b260 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 13 Sep 2023 14:27:26 +0200 Subject: [PATCH] Remove #[infer] attribute Made useless by reverse coercions in Coq 8.16 --- Changelog.md | 2 ++ HB/common/utils.elpi | 1 - HB/structure.elpi | 35 +++-------------------------------- _CoqProject.test-suite | 1 - structures.v | 8 -------- tests/funclass.v | 1 - tests/infer.v | 29 ----------------------------- 7 files changed, 5 insertions(+), 72 deletions(-) delete mode 100644 tests/infer.v diff --git a/Changelog.md b/Changelog.md index 246a3c99..1c12d44a 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,8 @@ - **Removed** the `#[primitive_class]` attribute, making it the default. - **New** `HB.saturate` to saturate instances w.r.t. the current hierarchy +- **Removed** the `#[infer]` attribute made obsolete by reverse coercions + since Coq 8.16 ## [1.6.0] - 2023-09-20 diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index fa7552b0..b205154b 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -29,7 +29,6 @@ with-attributes P :- att "mathcomp.axiom" string, att "short.type" string, att "short.pack" string, - att "infer" attmap, att "key" string, att "arg_sort" bool, att "log" bool, diff --git a/HB/structure.elpi b/HB/structure.elpi index 89bf3313..1c715656 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -56,8 +56,6 @@ declare Module BSkel Sort :- std.do! [ if-verbose (coq.say {header} "structure: mixin first class" MixinFirstClass), - private.declare-auto-infer-params-abbrev Structure MLwP LocType PHClauses, - if-verbose (coq.say {header} "declaring clone abbreviation"), w-params.then MLwP phant.fun-real phant.fun-real (private.clone-phant-body ClassName SortProjection Structure) PhClone, @@ -89,11 +87,7 @@ declare Module BSkel Sort :- std.do! [ if (get-option "short.type" ShortType) ( if-verbose (coq.say {header} "short name for type:" ShortType), - if (LocType = loc-abbreviation StrTypeAbbrev) (std.do! [ - coq.notation.abbreviation-body StrTypeAbbrev NStrTypeAbbrev StrTypeTm, - @global! => log.coq.notation.add-abbreviation - ShortType NStrTypeAbbrev StrTypeTm ff _ - ]) (@global! => log.coq.notation.add-abbreviation + (@global! => log.coq.notation.add-abbreviation ShortType 0 (global Structure) ff _)) true, coq.mk-app (global Structure) {coq.mk-n-holes {w-params.nparams MLwP}} HB_Instance, @@ -133,7 +127,7 @@ declare Module BSkel Sort :- std.do! [ std.flatten [ Factories, [ClassAlias], [is-structure Structure], NewJoins, [class-def CurrentClass], GRDepsClauses, - [gref-deps GRPack MLwP], MixinMems, [StructKeyClause], PHClauses + [gref-deps GRPack MLwP], MixinMems, [StructKeyClause] ] NewClauses, acc-clauses current NewClauses, @@ -449,9 +443,7 @@ synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :- pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl. pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl. -mk-record+sort-field Sort _ T F (record RecordName (sort Sort) "Pack" (field _ "sort" T F)) :- !, std.do! [ - if (get-option "infer" _) (RecordName = "type_") (RecordName = "type") -]. +mk-record+sort-field Sort _ T F (record "type" (sort Sort) "Pack" (field _ "sort" T F)). pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl. mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global ClassName|Args]) _\end-record) :- @@ -591,27 +583,6 @@ pack-body.aux PL T BuildC PackS Body :- !, std.do! [ mk-app (global PackS) {std.append PL [T, Class]} Body ]. -pred declare-auto-infer-params-abbrev i:structure, i:mixins, o:located, o:list prop. -declare-auto-infer-params-abbrev GR MLwP (loc-abbreviation Abbrev) [phant-abbrev GR (const PhC) Abbrev] :- - get-option "infer" Map, !, - Map => mk-infer (global GR) MLwP PhT, - phant.add-abbreviation "type" PhT PhC Abbrev. -declare-auto-infer-params-abbrev GR _ (loc-gref GR) []. - -pred mk-infer i:term, i:mixins, o:phant-term. -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. -mk-infer _ (w-params.cons ID _ _) _ :- get-option ID Infer, - coq.error "Automatic inference of paramter" ID "from" Infer "not supported". - pred mk-infer-key i:class, i:term, i:mixins, i:term, o:phant-term. mk-infer-key CoeClass K (w-params.nil ID _ _) St PhK :- @pi-parameter ID St t\ phant.init {mk-app K [t]} (PhKBo t), diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 391e6c39..7a243c1b 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -60,7 +60,6 @@ tests/duplicate_structure.v tests/instance_params_no_type.v tests/test_CS_db_filtering.v tests/subtype.v -tests/infer.v tests/exports.v tests/exports2.v tests/log_impargs_record.v diff --git a/structures.v b/structures.v index fb904876..9326c4fc 100644 --- a/structures.v +++ b/structures.v @@ -581,14 +581,6 @@ HB.structure Definition StructureName params := Supported attributes: - [#[mathcomp]] attempts to generate a backward compatibility layer with mathcomp: trying to infer the right [StructureName.pack], - - [#[infer(variable)]], where [variable : pT] belongs to [params] and is a structure - (e.g. from the hierarchy) with a coercion/canonical projection [pT >-> Sortclass]. - It modifies the notation [StructureName.type] so as to accept [variable : Type] instead, - and will try to infer its [pT] by unification (using canonical structure inference), - This is essential in [Lmodule.type R] where [R] should have type [Ring.type] - but any [Type] which is canonically a [Ring.type] is accepted thanks to [#[infer(R)]]. - If the carrier of the structure [S] is not a [Type] but rather a function, one has - to write [#[infer(S = "_ -> _")]]. - [#[arg_sort]] defines an alias [StructureName.arg_sort] for [StructureName.sort], and declares it as the main coercion. [StructureName.sort] is still declared as a coercion but the only reason is to make sure Coq does not print it. diff --git a/tests/funclass.v b/tests/funclass.v index 29d278f1..55c5c72d 100644 --- a/tests/funclass.v +++ b/tests/funclass.v @@ -50,7 +50,6 @@ HB.instance Definition x5 := Check Monoid.on mult. HB.mixin Record silly (T1 : Type) (F : Monoid.type T1) (T : Type) := { xx : T }. -#[infer(F = "_ -> _")] HB.structure Definition wp T (F : Monoid.type T) := { A of silly T F A }. #[skip="8.11"] diff --git a/tests/infer.v b/tests/infer.v deleted file mode 100644 index 450d5a21..00000000 --- a/tests/infer.v +++ /dev/null @@ -1,29 +0,0 @@ -From HB Require Import structures. - -HB.mixin Record foom T := { - op : T -> T -> T -}. - -HB.structure Definition foo := { T of foom T }. - -HB.instance Definition i := foom.Build nat plus. - -#[key="T"] -HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := { - law : P -> T -> A -> B -}. - -#[infer(P)] -HB.structure Definition bar A P B := { T of barm A P B T }. - -HB.check (bar.type_ bool nat bool). -Print bar.phant_type. -Print bar.type. -Check bar.type bool nat bool. - -Fail #[infer(P = "whatever")] -HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }. - -#[infer(P = "Type")] -HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }. -Check bar1.type nat.