From 160523fab2b125dd108d56879920c812b869f3d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 6 May 2020 23:04:10 +0200 Subject: [PATCH 01/60] adapt to coq-elpi master after elpi 1.11 --- hb.elpi | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/hb.elpi b/hb.elpi index 71c193e61..aadb774db 100644 --- a/hb.elpi +++ b/hb.elpi @@ -125,7 +125,8 @@ name-of-asset-decl (asset-record X _ _ _) X. name-of-asset-decl (asset-alias X _) X. pred argument->asset i:argument, o:asset-decl. -argument->asset (indt-decl (parameter Name Ty I)) (asset-parameter "T" Ty A) :- % TODO, take the name +argument->asset (indt-decl (parameter ID Ty I)) (asset-parameter ID Ty A) :- % TODO, take the name + coq.string->name ID Name, @pi-decl Name Ty a\ argument->asset (indt-decl (I a)) (A a). argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !. @@ -966,7 +967,7 @@ declare-class ML (indt ClassName) Factories :- std.do! [ (@pi-decl `T` {{Type}} t\ synthesize-fields t ML (RDecl t)), ClassDeclaration = - (parameter `T` {{ Type }} t\ + (parameter "T" {{ Type }} t\ record "axioms" {{ Type }} "Class" (RDecl t)), std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped", coq.env.add-indt ClassDeclaration ClassName, From b8d86c54f2764dfa44fd8ce8107afe18ba65710a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 May 2020 14:24:15 +0200 Subject: [PATCH 02/60] Add Zulip badge --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index a66a77cee..b4a821617 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ [![Build Status](https://travis-ci.org/math-comp/hierarchy-builder.svg?branch=master)](https://travis-ci.org/math-comp/hierarchy-builder) +[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Buidlder) # Hierarchy Builder From 1bf24d41203807dd6108ca1bdf918960c13ecf79 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 May 2020 17:32:12 +0200 Subject: [PATCH 03/60] fix makefile not to compile structures 3 times --- Makefile.coq.local | 46 ++++++++++++++++++++++++++++++++++++---------- 1 file changed, 36 insertions(+), 10 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 2e2058e1a..3f1962020 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -3,19 +3,45 @@ structures.vo : hb.elpi #### generate many rules to generate demoN/test_HIERARCHY_USER.v #### define MKRULE -demo$1/test_$2_$3.v: demo$1/user_$3.v structures.vo demo$1/hierarchy_$2.vo - cat demo$1/user_$3.v \ - | sed 's?@@HIERARCHY@@?hierarchy_$2?' \ - | sed 's?@@DEMO@@?HB.demo$1?' \ - > demo$1/test_$2_$3.v +demo%/test_$1_$2.v: demo%/user_$2.v structures.vo demo%/hierarchy_$1.vo + cat demo$*/user_$2.v \ + | sed 's?@@HIERARCHY@@?hierarchy_$1?' \ + | sed 's?@@DEMO@@?HB.demo$*?' \ + > demo$*/test_$1_$2.v endef -$(foreach N,$(shell seq 0 10),\ - $(foreach M,$(shell seq 0 10),\ - $(foreach K,$(shell seq 0 10),\ - $(eval $(call MKRULE,$(N),$(M),$(K)))))) +# This makes make try to compile things more than onece :-/ +#$(foreach N,$(shell seq 0 10),\ +# $(foreach M,$(shell seq 0 10),\ +# $(foreach K,$(shell seq 0 10),\ +# $(eval $(call MKRULE,$(N),$(M),$(K)))))) -#### add all the files we want to test #### +$(call MKRULE,0,0) +$(call MKRULE,0,1) +$(call MKRULE,0,2) +$(call MKRULE,0,3) +$(call MKRULE,1,0) +$(call MKRULE,1,1) +$(call MKRULE,1,2) +$(call MKRULE,1,3) +$(call MKRULE,2,0) +$(call MKRULE,2,1) +$(call MKRULE,2,2) +$(call MKRULE,2,3) +$(call MKRULE,3,0) +$(call MKRULE,3,1) +$(call MKRULE,3,2) +$(call MKRULE,3,3) +$(call MKRULE,4,0) +$(call MKRULE,4,1) +$(call MKRULE,4,2) +$(call MKRULE,4,3) +$(call MKRULE,5,0) +$(call MKRULE,5,1) +$(call MKRULE,5,2) +$(call MKRULE,5,3) + +### add all the files we want to test #### ## demo1/ From 5a0c93b17a9ec32fb75299b70b07bb4877e5c78c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 18 May 2020 17:32:21 +0200 Subject: [PATCH 04/60] port to coq-elpi 1.4 --- hb.elpi | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/hb.elpi b/hb.elpi index aadb774db..4a3f92358 100644 --- a/hb.elpi +++ b/hb.elpi @@ -125,15 +125,16 @@ name-of-asset-decl (asset-record X _ _ _) X. name-of-asset-decl (asset-alias X _) X. pred argument->asset i:argument, o:asset-decl. -argument->asset (indt-decl (parameter ID Ty I)) (asset-parameter ID Ty A) :- % TODO, take the name +argument->asset (indt-decl (parameter ID _ Ty I)) (asset-parameter ID Ty A) :- coq.string->name ID Name, @pi-decl Name Ty a\ argument->asset (indt-decl (I a)) (A a). argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !. -argument->asset (const-decl Id (some (fun _ _ Bo)) (some (prod Name Src Ty))) (asset-parameter "T" Src A) :- !, +argument->asset (const-decl Id (some (fun _ _ Bo)) (parameter ID _ Src Ty)) (asset-parameter ID Src A) :- !, + coq.id->name ID Name, @pi-decl Name Src a\ - argument->asset (const-decl Id (some (Bo a)) (some (Ty a))) (A a). -argument->asset (const-decl Id (some Bo) (some Ty)) (asset-alias Id Bo) :- !, + argument->asset (const-decl Id (some (Bo a)) (Ty a)) (A a). +argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !, std.assert! (var Ty) "Factories aliases should not be given a type". argument->asset X _ :- coq.error "Unsupported asset:" X. @@ -967,7 +968,7 @@ declare-class ML (indt ClassName) Factories :- std.do! [ (@pi-decl `T` {{Type}} t\ synthesize-fields t ML (RDecl t)), ClassDeclaration = - (parameter "T" {{ Type }} t\ + (parameter "T" explicit {{ Type }} t\ record "axioms" {{ Type }} "Class" (RDecl t)), std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped", coq.env.add-indt ClassDeclaration ClassName, @@ -1150,11 +1151,11 @@ declare-old-constant (some C) :- declare-old-constant _ :- true. pred main-begin-declare-builders i:context-decl. -main-begin-declare-builders (context-item _ _ none _\ context-item IDF _ (some _) _\ context-end) :- +main-begin-declare-builders (context-item _ _ _ none _\ context-item IDF _ _ (some _) _\ context-end) :- coq.error "factories cannot be given a body:" IDF. -main-begin-declare-builders (context-item _ _ none _\ context-item ID1 _ none _\ context-item ID2 _ _ _) :- +main-begin-declare-builders (context-item _ _ _ none _\ context-item ID1 _ _ none _\ context-item ID2 _ _ _ _) :- coq.error "only one factory is supported, got at least two" ID1 "and" ID2. -main-begin-declare-builders (context-item IDT T none t\ context-item IDF (F t) none _\ context-end) :- std.do! [ +main-begin-declare-builders (context-item IDT _ T none t\ context-item IDF _ (F t) none _\ context-end) :- std.do! [ Name is "Builders_" ^ {term_to_string {new_int}}, % TODO std.assert! (pi t\ F t = app[global GRA, t|_]) "a factory must be a name applied to the type variable", factory-alias->gref GRA GRF, From 31289c87b7b838ba16a693dd08db3879a2352c36 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 09:51:22 +0200 Subject: [PATCH 05/60] hot fix for Coq CI --- Makefile.coq.local | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile.coq.local b/Makefile.coq.local index 3f1962020..94dfd37a8 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -54,3 +54,5 @@ VFILES+=$(foreach H,$(shell seq 3 5), demo1/test_$(H)_3.v) # user_0 works on top of all 3 hierarchies VFILES+=$(foreach H,$(shell seq 0 2), demo3/test_$(H)_0.v) + +.NOTPARALLEL: \ No newline at end of file From 2ef69193e0f3d129b99b50a6b8b7f1683c4444af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 10:23:42 +0200 Subject: [PATCH 06/60] Revert "hot fix for Coq CI" This reverts commit 31289c87b7b838ba16a693dd08db3879a2352c36. --- Makefile.coq.local | 2 -- 1 file changed, 2 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 94dfd37a8..3f1962020 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -54,5 +54,3 @@ VFILES+=$(foreach H,$(shell seq 3 5), demo1/test_$(H)_3.v) # user_0 works on top of all 3 hierarchies VFILES+=$(foreach H,$(shell seq 0 2), demo3/test_$(H)_0.v) - -.NOTPARALLEL: \ No newline at end of file From 7b2c46c6a1b82d1da193efe1694c32beb4e9a1b8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 May 2020 10:23:52 +0200 Subject: [PATCH 07/60] Revert "fix makefile not to compile structures 3 times" This reverts commit 1bf24d41203807dd6108ca1bdf918960c13ecf79. --- Makefile.coq.local | 46 ++++++++++------------------------------------ 1 file changed, 10 insertions(+), 36 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 3f1962020..2e2058e1a 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -3,45 +3,19 @@ structures.vo : hb.elpi #### generate many rules to generate demoN/test_HIERARCHY_USER.v #### define MKRULE -demo%/test_$1_$2.v: demo%/user_$2.v structures.vo demo%/hierarchy_$1.vo - cat demo$*/user_$2.v \ - | sed 's?@@HIERARCHY@@?hierarchy_$1?' \ - | sed 's?@@DEMO@@?HB.demo$*?' \ - > demo$*/test_$1_$2.v +demo$1/test_$2_$3.v: demo$1/user_$3.v structures.vo demo$1/hierarchy_$2.vo + cat demo$1/user_$3.v \ + | sed 's?@@HIERARCHY@@?hierarchy_$2?' \ + | sed 's?@@DEMO@@?HB.demo$1?' \ + > demo$1/test_$2_$3.v endef -# This makes make try to compile things more than onece :-/ -#$(foreach N,$(shell seq 0 10),\ -# $(foreach M,$(shell seq 0 10),\ -# $(foreach K,$(shell seq 0 10),\ -# $(eval $(call MKRULE,$(N),$(M),$(K)))))) +$(foreach N,$(shell seq 0 10),\ + $(foreach M,$(shell seq 0 10),\ + $(foreach K,$(shell seq 0 10),\ + $(eval $(call MKRULE,$(N),$(M),$(K)))))) -$(call MKRULE,0,0) -$(call MKRULE,0,1) -$(call MKRULE,0,2) -$(call MKRULE,0,3) -$(call MKRULE,1,0) -$(call MKRULE,1,1) -$(call MKRULE,1,2) -$(call MKRULE,1,3) -$(call MKRULE,2,0) -$(call MKRULE,2,1) -$(call MKRULE,2,2) -$(call MKRULE,2,3) -$(call MKRULE,3,0) -$(call MKRULE,3,1) -$(call MKRULE,3,2) -$(call MKRULE,3,3) -$(call MKRULE,4,0) -$(call MKRULE,4,1) -$(call MKRULE,4,2) -$(call MKRULE,4,3) -$(call MKRULE,5,0) -$(call MKRULE,5,1) -$(call MKRULE,5,2) -$(call MKRULE,5,3) - -### add all the files we want to test #### +#### add all the files we want to test #### ## demo1/ From 0ca3e58a2c388cfcd43728c63cafb9aa8b77a2d0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Jun 2020 10:54:15 +0200 Subject: [PATCH 08/60] run CI on coq-master --- .travis.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.travis.yml b/.travis.yml index a2cd4c0e9..aded17c59 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,6 +3,7 @@ version: ~> 1.0 branches: only: - master + - coq-master env: global: From df4a8eedc000f5a50872734af546798548c465c4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 3 Jun 2020 15:25:29 +0200 Subject: [PATCH 09/60] opam file for coq-master should not be picky about versions # Conflicts: # coq-hierarchy-builder.opam --- coq-hierarchy-builder.opam | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 01653f726..8335f0ec8 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -11,8 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make ] install: [ make "install" "VFILES=structures.v" ] depends: [ - "coq" {>= "8.11.0" & < "8.12.0~" } - "coq-elpi" {>= "1.4.0" & < "1.5.0~"} + "coq-elpi" ] synopsis: "Hierarchy Builder" description: """ From 617924d4c2260fe484228dd47e6e1b55adc9755b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 24 Mar 2021 11:47:39 +0100 Subject: [PATCH 10/60] adapt to coq/coq#13958 --- hb.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hb.elpi b/hb.elpi index aa3f66228..50cd5110b 100644 --- a/hb.elpi +++ b/hb.elpi @@ -564,7 +564,7 @@ safe-head T Hd :- safe-dest-app T Hd _. %% finding for locally defined structures pred get-cs-structure i:cs-instance, o:term. -get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [ +get-cs-structure (cs-instance _ _ Inst) Struct :- std.do! [ coq.env.typeof Inst InstTy, safe-head InstTy Struct ]. From e87ca3fd27aff655d8c25c55f4f40d3df6374fc2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 14 Apr 2021 22:58:49 +0200 Subject: [PATCH 11/60] fixup --- HB/common/database.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HB/common/database.elpi b/HB/common/database.elpi index f0f9e12d9..9ce981e58 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -257,7 +257,7 @@ get-constructor I _ :- coq.error "get-constructor: not an inductive" I. %% finding for locally defined structures pred get-cs-structure i:cs-instance, o:structure. get-cs-structure (cs-instance _ _ Inst) Struct :- std.do! [ - coq.env.typeof (global Inst) InstTy, + coq.env.typeof Inst InstTy, coq.prod-tgt->gref InstTy Struct ]. From bd589b63bf48cf9a00812bdaa0c9a8192e78b83b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Jun 2021 16:04:30 +0200 Subject: [PATCH 12/60] unqualify require in example used by the platform to ease smoke-test --- examples/demo2/stage10.v | 3 ++- examples/demo2/stage11.v | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/examples/demo2/stage10.v b/examples/demo2/stage10.v index a9dcfba63..b92d6c51e 100644 --- a/examples/demo2/stage10.v +++ b/examples/demo2/stage10.v @@ -1,6 +1,7 @@ From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith. From HB Require Import structures. -From HB Require Import demo2.classical. + +Require Import classical. Declare Scope hb_scope. Delimit Scope hb_scope with G. diff --git a/examples/demo2/stage11.v b/examples/demo2/stage11.v index 633e52701..8a1cd6150 100644 --- a/examples/demo2/stage11.v +++ b/examples/demo2/stage11.v @@ -1,6 +1,7 @@ From Coq Require Import ssreflect ssrfun ssrbool ZArith QArith. From HB Require Import structures. -From HB Require Import demo2.classical. + +Require Import classical. Declare Scope hb_scope. Delimit Scope hb_scope with G. From 5a3ec15448e62c77810fc8aaea29b463ad2533bb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 6 Jul 2021 16:59:53 +0200 Subject: [PATCH 13/60] the Arguments line now prints original names with Print/About --- tests/compress_coe.v.out | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/compress_coe.v.out b/tests/compress_coe.v.out index 5a493ef33..0d249e432 100644 --- a/tests/compress_coe.v.out +++ b/tests/compress_coe.v.out @@ -17,3 +17,5 @@ fun D D' : D.type => |} |} : D.type -> D.type -> D.type + +Arguments Datatypes_prod__canonical__compress_coe_D D D' From c2d56db9e32a9fe39c9faf2f325a6d89adb98a42 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 23 Jul 2021 15:19:10 +0200 Subject: [PATCH 14/60] Merge branch 'master' into coq-master+elpi-1.13.6 # Conflicts: # tests/about.v.out --- tests/about.v.out | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/tests/about.v.out b/tests/about.v.out index 6cacf6292..386afbb4e 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -113,12 +113,7 @@ HB: AddAG.sort is a canonical projection (from "./examples/demo1/hierarchy_5.v", line 73) HB: AddAG.sort has the following canonical values: - @eta - - AddAG_of_AddComoid.sort (from "./examples/demo1/hierarchy_5.v", line 48) - - AddAG_of_TYPE.sort (from "./examples/demo1/hierarchy_5.v", line 52) - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - - Ring_of_AddAG.sort (from "./examples/demo1/hierarchy_5.v", line 108) - - Ring_of_AddComoid.sort (from "./examples/demo1/hierarchy_5.v", line 144) - - Ring_of_TYPE.sort (from "./examples/demo1/hierarchy_5.v", line 167) - Z HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass @@ -145,4 +140,4 @@ HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to hierarchy_5.BiNearRing_of_AddMonoid HB: synthesized in file -File "./tests/about.v", line 3, column 165, characters 125-249: +File "./tests/about.v", line 5, column 122, characters 127-249: From cbb3df1f123b06ad1b6a937194e2c16e041b94e2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Apr 2022 16:35:48 +0200 Subject: [PATCH 15/60] HB arguments are raw --- structures.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/structures.v b/structures.v index f53696985..a22b12024 100644 --- a/structures.v +++ b/structures.v @@ -226,6 +226,7 @@ compress X X. or inductive was generated. *) +#[arguments(raw)] Elpi Command HB.locate. Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ @@ -256,6 +257,7 @@ Elpi Export HB.locate. - canonical value, eg Z, prod, ... *) +#[arguments(raw)] Elpi Command HB.about. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -281,6 +283,7 @@ Elpi Export HB.about. *) +#[arguments(raw)] Elpi Command HB.status. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -306,6 +309,7 @@ tred file.dot | xdot - to visualize file.dot *) +#[arguments(raw)] Elpi Command HB.graph. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -351,6 +355,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := { *) +#[arguments(raw)] Elpi Command HB.mixin. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -512,6 +517,7 @@ HB.structure Definition StructureName params := - [#[verbose]] for a verbose output. *) +#[arguments(raw)] Elpi Command HB.structure. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -558,6 +564,7 @@ HB.instance Definition N Params := Factory.Build Params T … - [#[verbose]] for a verbose output. *) +#[arguments(raw)] Elpi Command HB.instance. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -587,6 +594,7 @@ Elpi Export HB.instance. (** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *) +#[arguments(raw)] Elpi Command HB.factory. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -645,6 +653,7 @@ HB.end. - [#[verbose]] for a verbose output. *) +#[arguments(raw)] Elpi Command HB.builders. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -667,6 +676,7 @@ Elpi Typecheck. Elpi Export HB.builders. +#[arguments(raw)] Elpi Command HB.end. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -717,6 +727,7 @@ Export Algebra.Exports. *) +#[arguments(raw)] Elpi Command HB.export. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -741,6 +752,7 @@ Elpi Export HB.export. It optionally takes the name of a module or a component of the current module path (a module which is not closed yet) *) +#[arguments(raw)] Elpi Command HB.reexport. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -785,6 +797,7 @@ Notation foo := foo.body. ]] *) +#[arguments(raw)] Elpi Command HB.lock. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -831,6 +844,7 @@ HB.instance Definition _ : Ml ... T := ml. *) +#[arguments(raw)] Elpi Command HB.declare. Elpi Accumulate File "HB/common/stdpp.elpi". Elpi Accumulate File "HB/common/utils.elpi". @@ -864,6 +878,7 @@ Elpi Export HB.declare. that skips the action on Coq version matches rex. It also understands the [#[fail]] attribute. *) +#[arguments(raw)] Elpi Command HB.check. Elpi Accumulate Db hb.db. Elpi Accumulate File "HB/common/stdpp.elpi". From 379dc28870bb2ac8e8a400bbd7e3d32975fd0d0b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 7 Apr 2022 17:15:17 +0200 Subject: [PATCH 16/60] compat with coq-elpi 1.14 --- Makefile.test-suite.coq.local | 3 ++- coq-hierarchy-builder.opam | 2 +- tests/about.v.out | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index ec13e8b53..38dcbeeb7 100644 --- a/Makefile.test-suite.coq.local +++ b/Makefile.test-suite.coq.local @@ -12,8 +12,9 @@ DIFF=\ $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \ < $(1) 2>/dev/null \ | grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \ + | sed -E 's/characters? [0-9-]+://' \ > $(1).out.aux;\ - diff -u --strip-trailing-cr $(call output_for,$(1)) $(1).out.aux;\ + wdiff $(call output_for,$(1)) $(1).out.aux;\ fi post-all:: diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 4fdb64630..e58f9a77a 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -12,7 +12,7 @@ build: [ [ make "build"] [ make "test-suite" ] {with-test} ] install: [ make "install" ] -depends: [ "coq-elpi" { (>= "1.11.0" & < "1.13~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.11.0" & < "1.14~") | = "dev" } ] conflicts: [ "coq-hierarchy-builder-shim" ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """ diff --git a/tests/about.v.out b/tests/about.v.out index 8c0282e08..5c21837d7 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -140,4 +140,4 @@ HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to hierarchy_5.BiNearRing_of_AddMonoid HB: synthesized in file -File "(stdin)", line 5, column 122, characters 127-249: +File "(stdin)", line 5, column 122, From 873c18fcd57be7e12e3785586adc68d4fe937ad7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Feb 2022 09:59:58 +0100 Subject: [PATCH 17/60] adapt to coq/coq#15693 --- tests/infer.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/infer.v b/tests/infer.v index b7716c63a..c071b02dd 100644 --- a/tests/infer.v +++ b/tests/infer.v @@ -16,7 +16,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := { #[infer(P)] HB.structure Definition bar A P B := { T of barm A P B T }. -Fail Check bar.type_ bool nat bool. +(* Fail Check bar.type_ bool nat bool.*) Print bar.phant_type. Print bar.type. Check bar.type bool nat bool. From 3fc524482dc7e26cfdb4bb4b25b61a31d6f2ade2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 24 Jul 2022 23:13:09 +0200 Subject: [PATCH 18/60] fix tes --- tests/about.v.out | 2 +- tests/about.v.out.15 | 142 +++++++++++++++++++++++++++++++++++++++++++ tests/infer.v | 2 +- 3 files changed, 144 insertions(+), 2 deletions(-) create mode 100644 tests/about.v.out.15 diff --git a/tests/about.v.out b/tests/about.v.out index c56aaf2b1..46ff15c24 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -139,4 +139,4 @@ HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +HB: synthesized in file File "(stdin)", line 5, column 0, character 0: diff --git a/tests/about.v.out.15 b/tests/about.v.out.15 new file mode 100644 index 000000000..c56aaf2b1 --- /dev/null +++ b/tests/about.v.out.15 @@ -0,0 +1,142 @@ +HB: AddMonoid_of_TYPE is a factory + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE operations and axioms are: + - zero + - add + - addrA + - add0r + - addr0 +HB: AddMonoid_of_TYPE requires the following mixins: +HB: AddMonoid_of_TYPE provides the following mixins: + - hierarchy_5.AddMonoid_of_TYPE + +HB: AddMonoid_of_TYPE.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 10) +HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: +HB: AddMonoid_of_TYPE.Build provides the following mixins: + - hierarchy_5.AddMonoid_of_TYPE +HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 + - S : Type + - zero : AddMonoid.sort S + - add : S -> S -> S + - addrA : associative add + - add0r : left_id 0%G add + - addr0 : right_id 0%G add + +HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.type characterizing operations and axioms are: + - addNr + - opp +HB: hierarchy_5.AddAG is a factory for the following mixins: + - hierarchy_5.AddMonoid_of_TYPE + - hierarchy_5.AddComoid_of_AddMonoid + - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) +HB: hierarchy_5.AddAG inherits from: + - hierarchy_5.AddMonoid + - hierarchy_5.AddComoid +HB: hierarchy_5.AddAG is inherited by: + - hierarchy_5.Ring + +HB: hierarchy_5.AddMonoid.type is a structure + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: + - addr0 + - add0r + - addrA + - add + - zero +HB: hierarchy_5.AddMonoid is a factory for the following mixins: + - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) +HB: hierarchy_5.AddMonoid inherits from: +HB: hierarchy_5.AddMonoid is inherited by: + - hierarchy_5.AddComoid + - hierarchy_5.AddAG + - hierarchy_5.BiNearRing + - hierarchy_5.SemiRing + - hierarchy_5.Ring + +HB: Ring_of_AddAG is a factory + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG operations and axioms are: + - one + - mul + - mulrA + - mulr1 + - mul1r + - mulrDl + - mulrDr +HB: Ring_of_AddAG requires the following mixins: + - hierarchy_5.AddMonoid_of_TYPE + - hierarchy_5.AddComoid_of_AddMonoid + - hierarchy_5.AddAG_of_AddComoid +HB: Ring_of_AddAG provides the following mixins: + - hierarchy_5.BiNearRing_of_AddMonoid +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). + +HB: Ring_of_AddAG.Build is a factory constructor + (from "./examples/demo1/hierarchy_5.v", line 108) +HB: Ring_of_AddAG.Build requires its subject to be already equipped with: + - hierarchy_5.AddMonoid_of_TYPE + - hierarchy_5.AddComoid_of_AddMonoid + - hierarchy_5.AddAG_of_AddComoid +HB: Ring_of_AddAG.Build provides the following mixins: + - hierarchy_5.BiNearRing_of_AddMonoid +HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr + - A : Type + - one : A + - mul : A -> A -> A + - mulrA : associative mul + - mulr1 : left_id one mul + - mul1r : right_id one mul + - mulrDl : left_distributive mul add + - mulrDr : right_distributive mul add +Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and + mul0r are derived from addrC and the other ring axioms, following a proof + of Hankel (Gerhard Betsch. On the beginnings and development of near-ring + theory. In Near-rings and near-fields. Proceedings of the conference held + in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics + and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, + 1995). + +HB: add is an operation of structure hierarchy_5.AddMonoid + (from "./examples/demo1/hierarchy_5.v", line 17) +HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE + (from "./examples/demo1/hierarchy_5.v", line 10) + +HB: AddAG.sort is a canonical projection + (from "./examples/demo1/hierarchy_5.v", line 73) +HB: AddAG.sort has the following canonical values: + - @eta + - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) + - Z + +HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass + (from "./examples/demo1/hierarchy_5.v", line 73) + +HB: Z is canonically equipped with mixins: + - hierarchy_5.AddMonoid + hierarchy_5.AddComoid + hierarchy_5.AddAG + (from "(stdin)", line 5) + - hierarchy_5.BiNearRing + hierarchy_5.SemiRing + hierarchy_5.Ring + (from "(stdin)", line 10) + +HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from + hierarchy_5.Ring to hierarchy_5.SemiRing + (from "./examples/demo1/hierarchy_5.v", line 196) + +HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from + hierarchy_5.Ring to hierarchy_5.SemiRing + (from "./examples/demo1/hierarchy_5.v", line 196) + +HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to +hierarchy_5.BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 0, character 127: diff --git a/tests/infer.v b/tests/infer.v index a89d6104e..8f46f6229 100644 --- a/tests/infer.v +++ b/tests/infer.v @@ -17,7 +17,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := { HB.structure Definition bar A P B := { T of barm A P B T }. #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool). -#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool). +#[skip="8.1[6-9].*", fail] HB.check (bar.type_ bool nat bool). Print bar.phant_type. Print bar.type. Check bar.type bool nat bool. From 5873e5401bf7914ed9528324613a5856e53ded95 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 24 Jul 2022 23:37:59 +0200 Subject: [PATCH 19/60] fixup --- tests/about.v.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/about.v.out b/tests/about.v.out index 46ff15c24..a8533d77d 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -139,4 +139,4 @@ HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 0, character 0: +HB: synthesized in file File "(stdin)", line 5, column 0: From 886f8d4ef18bb71026aab3b62afd5fa0a37f60c9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 25 Jul 2022 07:43:39 +0200 Subject: [PATCH 20/60] Update tests/about.v.out --- tests/about.v.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/about.v.out b/tests/about.v.out index a8533d77d..a1da2a04f 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -139,4 +139,4 @@ HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 0: +HB: synthesized in file File "(stdin)", line 5, column 0, From e54b6d862b78bae0418c760fa0debd4a6ddd680b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 22 Feb 2023 16:12:39 +0100 Subject: [PATCH 21/60] Avoid memory increase in hulk.vo workaround https://github.com/coq/coq/issues/17223 --- examples/hulk.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/examples/hulk.v b/examples/hulk.v index 60b68c530..60dc71109 100644 --- a/examples/hulk.v +++ b/examples/hulk.v @@ -258,6 +258,8 @@ Abort. End SlowFailure. +(* cf https://github.com/coq/coq/issues/17223 *) +Optimize Heap. Module FastFailure. From 40ceaed48753f664b7db59a6eca4fdefe3c02518 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Jul 2022 11:43:32 +0200 Subject: [PATCH 22/60] Update Changelog.md --- Changelog.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Changelog.md b/Changelog.md index 1ed500838..f855db3b6 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,16 @@ # Changelog +## [1.3.0] - 2022-07-27 + +Compatible with +- Coq 8.15 with Coq-Elpi 1.14.x +- Coq 8.16 with Coq-Elpi 1.15.x + +### General + +- **Fix** Structures can be keyd on sorts (eg `Prop`) and products (eg `T -> U`) +- **New** Mixin parameters can depend on structure instances inferred using previous mixins (see [this test](tests/interleave_context.v)) + ## [1.2.1] - 2022-01-10 Compatible with From 5a6ded8f24583d0a3a58497d2683ea6cb651eb48 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 27 Jul 2022 11:51:02 +0200 Subject: [PATCH 23/60] Update interleave_context.v --- tests/interleave_context.v | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/tests/interleave_context.v b/tests/interleave_context.v index dd055fcb3..8da42ed0a 100644 --- a/tests/interleave_context.v +++ b/tests/interleave_context.v @@ -7,9 +7,12 @@ HB.structure Definition A n := { T of HasA n T }. HB.mixin Record HasB (X : A.type 0) (T : Type) := { b : X -> T }. HB.structure Definition B (X : A.type 0) := { T of HasB X T }. -#[verbose] +(* Since `B` expects an argument of type `A.type 0` (and not just + just the naked type `T`) we pass `A.clone 0 T _` + (of type `A.type 0`) and inference uses the first + parameter `A` to elaborate it. *) HB.mixin Record IsSelfA T of A 0 T & B (A.clone 0 T _) T := {}. -#[verbose] + HB.structure Definition SelfA := { T of IsSelfA T }. HB.factory Record IsSelfA' T := { a : T ; b : T -> T}. @@ -19,5 +22,4 @@ HB.builders Context T of IsSelfA' T. HB.instance Definition _ := IsSelfA.Build T. HB.end. -#[verbose] - HB.instance Definition _ := IsSelfA'.Build nat 0 id. \ No newline at end of file +HB.instance Definition _ := IsSelfA'.Build nat 0 id. From b58851166234320486d3e3870a69b5ad38a348c3 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 3 Aug 2022 11:34:26 +0200 Subject: [PATCH 24/60] Fix typo in HB.locate usage message --- structures.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/structures.v b/structures.v index abae6db4b..43c25f524 100644 --- a/structures.v +++ b/structures.v @@ -259,7 +259,7 @@ main [str S] :- !, (coq.say "HB: synthesized in file" Loc) (coq.say "HB:" S "not synthesized by HB"). -main _ :- coq.error "Usage: HB.about .". +main _ :- coq.error "Usage: HB.locate .". }}. Elpi Typecheck. Elpi Export HB.locate. From ed1f58b45521cb7d3928e5317757da8145af4ded Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 3 Aug 2022 11:42:05 +0200 Subject: [PATCH 25/60] Remove outdated Coq version tests now that we require 8.15 --- HB/common/stdpp.elpi | 3 +-- HB/common/utils.elpi | 11 ++--------- HB/graph.elpi | 9 +-------- structures.v | 2 -- 4 files changed, 4 insertions(+), 21 deletions(-) diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 9062241f9..c228ff7ab 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -101,8 +101,7 @@ constraint print-ctx mixin-src { % approximation, it should be logical path, not the file name pred coq.env.current-library o:string. -coq.env.current-library L :- coq.version _ _ N _, N >= 13, !, - loc.fields {get-option "elpi.loc"} L _ _ _ _. +coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. coq.env.current-library "dummy.v". pred coq.prod-tgt->gref i:term, o:gref. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index f7c1e76fa..0eb53d2dc 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -120,13 +120,6 @@ nice-gref->string X Mod :- nice-gref->string X S :- coq.term->string (global X) S. -pred compat.concat i:string, i:list string, o:string. -compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O. -compat.concat S L O :- compat.concat.aux L S O. -compat.concat.aux [] _ "". -compat.concat.aux [X] _ X :- !. -compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1. - pred gref->modname i:gref, i:int, i:string, o:string. gref->modname GR NComp Sep ModName :- coq.gref->path GR Path, @@ -134,7 +127,7 @@ gref->modname GR NComp Sep ModName :- std.length Path Len, if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), std.take NComp Mods L, - compat.concat Sep {std.rev L} ModName. + std.string.concat Sep {std.rev L} ModName. pred gref->modname-label i:gref, i:int, i:string, o:string. gref->modname-label GR NComp Sep ModName :- coq.gref->path GR Path, @@ -142,7 +135,7 @@ gref->modname-label GR NComp Sep ModName :- std.length PathRev Len, if (Len >= NComp) (N = NComp) (N = Len), std.take N PathRev L, - compat.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. + std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. pred avoid-name-collision i:string, o:string. avoid-name-collision S S1 :- diff --git a/HB/graph.elpi b/HB/graph.elpi index 27c7495c3..b8baffcf4 100644 --- a/HB/graph.elpi +++ b/HB/graph.elpi @@ -18,13 +18,6 @@ to-file File :- !, std.do! [ namespace private { -pred compat.concat i:string, i:list string, o:string. -compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O. -compat.concat S L O :- compat.concat.aux L S O. -compat.concat.aux [] _ "". -compat.concat.aux [X] _ X :- !. -compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1. - pred gref->modname i:gref, i:int, i:string, o:string. gref->modname GR NComp Sep ModName :- coq.gref->path GR Path, @@ -32,7 +25,7 @@ gref->modname GR NComp Sep ModName :- std.length Path Len, if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), std.take NComp Mods L, - compat.concat Sep {std.rev L} ModName. + std.string.concat Sep {std.rev L} ModName. pred pp-coercion-dot i:out_stream, i:coercion. pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [ diff --git a/structures.v b/structures.v index 43c25f524..3fc0415dd 100644 --- a/structures.v +++ b/structures.v @@ -252,8 +252,6 @@ Elpi Accumulate Db hb.db. #[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate lp:{{ -main _ :- coq.version _ _ N _, N < 13, !, - coq.say "HB: HB.locate requires Coq version 8.13 or above". main [str S] :- !, if (decl-location {coq.locate S} Loc) (coq.say "HB: synthesized in file" Loc) From 1f2839324b82b225fc6f209f890b405830cf3330 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 10:31:40 +0200 Subject: [PATCH 26/60] Cleanup after dropping Coq < 8.15 --- tests/about.v.out.13 | 143 ------------------------------------ tests/about.v.out.14 | 142 ----------------------------------- tests/compress_coe.v.out.13 | 19 ----- tests/compress_coe.v.out.14 | 19 ----- 4 files changed, 323 deletions(-) delete mode 100644 tests/about.v.out.13 delete mode 100644 tests/about.v.out.14 delete mode 100644 tests/compress_coe.v.out.13 delete mode 100644 tests/compress_coe.v.out.14 diff --git a/tests/about.v.out.13 b/tests/about.v.out.13 deleted file mode 100644 index 891babf10..000000000 --- a/tests/about.v.out.13 +++ /dev/null @@ -1,143 +0,0 @@ -HB: AddMonoid_of_TYPE is a factory - (from "./examples/demo1/hierarchy_5.v", line 2) -HB: AddMonoid_of_TYPE operations and axioms are: - - zero - - add - - addrA - - add0r - - addr0 -HB: AddMonoid_of_TYPE requires the following mixins: -HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - -HB: AddMonoid_of_TYPE.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 2) -HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: -HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE -HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - - S : Type - - zero : AddMonoid.sort S - - add : S -> S -> S - - addrA : associative add - - add0r : left_id 0%G add - - addr0 : right_id 0%G add - -HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 72) -HB: AddAG.type characterizing operations and axioms are: - - addNr - - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring - -HB: hierarchy_5.AddMonoid.type is a structure - (from "./examples/demo1/hierarchy_5.v", line 16) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: - - addr0 - - add0r - - addrA - - add - - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring - -HB: Ring_of_AddAG is a factory - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG operations and axioms are: - - one - - mul - - mulrA - - mulr1 - - mul1r - - mulrDl - - mulrDr -HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: Ring_of_AddAG.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - - A : Type - - one : A - - mul : A -> A -> A - - mulrA : associative mul - - mulr1 : left_id one mul - - mul1r : right_id one mul - - mulrDl : left_distributive mul add - - mulrDr : right_distributive mul add -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: add is an operation of structure hierarchy_5.AddMonoid - (from "./examples/demo1/hierarchy_5.v", line 16) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE - (from "./examples/demo1/hierarchy_5.v", line 2) - -HB: AddAG.sort is a canonical projection - (from "./examples/demo1/hierarchy_5.v", line 72) -HB: AddAG.sort has the following canonical values: - - Z - - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 194) - - @eta - -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass - (from "./examples/demo1/hierarchy_5.v", line 72) - -HB: Z is canonically equipped with mixins: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG - (from "(stdin)", line 3) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring - (from "(stdin)", line 8) - -HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 194) - -HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 194) - -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file -File "(stdin)", line 3, column 165, characters 125-249: diff --git a/tests/about.v.out.14 b/tests/about.v.out.14 deleted file mode 100644 index a93916a7a..000000000 --- a/tests/about.v.out.14 +++ /dev/null @@ -1,142 +0,0 @@ -HB: AddMonoid_of_TYPE is a factory - (from "./examples/demo1/hierarchy_5.v", line 10) -HB: AddMonoid_of_TYPE operations and axioms are: - - zero - - add - - addrA - - add0r - - addr0 -HB: AddMonoid_of_TYPE requires the following mixins: -HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - -HB: AddMonoid_of_TYPE.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 10) -HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: -HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE -HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - - S : Type - - zero : AddMonoid.sort S - - add : S -> S -> S - - addrA : associative add - - add0r : left_id 0%G add - - addr0 : right_id 0%G add - -HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) -HB: AddAG.type characterizing operations and axioms are: - - addNr - - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring - -HB: hierarchy_5.AddMonoid.type is a structure - (from "./examples/demo1/hierarchy_5.v", line 17) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: - - addr0 - - add0r - - addrA - - add - - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring - -HB: Ring_of_AddAG is a factory - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG operations and axioms are: - - one - - mul - - mulrA - - mulr1 - - mul1r - - mulrDl - - mulrDr -HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: Ring_of_AddAG.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - - A : Type - - one : A - - mul : A -> A -> A - - mulrA : associative mul - - mulr1 : left_id one mul - - mul1r : right_id one mul - - mulrDl : left_distributive mul add - - mulrDr : right_distributive mul add -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: add is an operation of structure hierarchy_5.AddMonoid - (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE - (from "./examples/demo1/hierarchy_5.v", line 10) - -HB: AddAG.sort is a canonical projection - (from "./examples/demo1/hierarchy_5.v", line 73) -HB: AddAG.sort has the following canonical values: - - @eta - - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - - Z - -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass - (from "./examples/demo1/hierarchy_5.v", line 73) - -HB: Z is canonically equipped with mixins: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG - (from "(stdin)", line 5) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring - (from "(stdin)", line 10) - -HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) - -HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) - -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 122, character 127: diff --git a/tests/compress_coe.v.out.13 b/tests/compress_coe.v.out.13 deleted file mode 100644 index 5a493ef33..000000000 --- a/tests/compress_coe.v.out.13 +++ /dev/null @@ -1,19 +0,0 @@ -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type diff --git a/tests/compress_coe.v.out.14 b/tests/compress_coe.v.out.14 deleted file mode 100644 index 5a493ef33..000000000 --- a/tests/compress_coe.v.out.14 +++ /dev/null @@ -1,19 +0,0 @@ -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type From 9a84d1972f879b4742c51973100947a541c378e2 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 13:02:53 +0200 Subject: [PATCH 27/60] Fix typo in about --- HB/about.elpi | 2 +- tests/about.v.out | 2 +- tests/about.v.out.15 | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/HB/about.elpi b/HB/about.elpi index 9e512586f..92af9bf0b 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -76,7 +76,7 @@ main-canonical-value S CanonicalValues :- group-by-loc CanonicalValues CanonicalValuesL, %format PpCanonicalValues = box (v 4) [ - str "HB: ", str S, str " is canonically equipped with mixins:", + str "HB: ", str S, str " is canonically equipped with structures:", {bulletize CanonicalValuesL pp-canonical-solution-list}], % print coq.say {coq.pp->string PpCanonicalValues}, diff --git a/tests/about.v.out b/tests/about.v.out index a1da2a04f..ce0996219 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -119,7 +119,7 @@ HB: AddAG.sort has the following canonical values: HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) -HB: Z is canonically equipped with mixins: +HB: Z is canonically equipped with structures: - hierarchy_5.AddMonoid hierarchy_5.AddComoid hierarchy_5.AddAG diff --git a/tests/about.v.out.15 b/tests/about.v.out.15 index c56aaf2b1..1f0c60604 100644 --- a/tests/about.v.out.15 +++ b/tests/about.v.out.15 @@ -119,7 +119,7 @@ HB: AddAG.sort has the following canonical values: HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) -HB: Z is canonically equipped with mixins: +HB: Z is canonically equipped with structures: - hierarchy_5.AddMonoid hierarchy_5.AddComoid hierarchy_5.AddAG From 2bb77cf59abfca42b63f9e90abef0d914f766f8f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 10:27:42 +0200 Subject: [PATCH 28/60] Print shortest names in HB.about and HB.graph --- HB/about.elpi | 13 +++--- HB/common/utils.elpi | 21 +++++++++ HB/graph.elpi | 13 +----- tests/about.v | 9 +++- tests/about.v.out | 101 +++++++++++++++++++++++-------------------- tests/about.v.out.15 | 101 +++++++++++++++++++++++-------------------- 6 files changed, 148 insertions(+), 110 deletions(-) diff --git a/HB/about.elpi b/HB/about.elpi index 92af9bf0b..b5f17cf73 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -15,7 +15,7 @@ main-located S (loc-gref GR) :- class-def (class Class GR MLwP), !, private.main-structure S Class GR MLwP. main-located _ (loc-gref Class) :- class-def (class Class GR MLwP), !, - gref->modname GR 2 "." M, + gref->modname_short GR "." M, coq.gref->id GR St, S is M ^ "." ^ St, private.main-structure S Class GR MLwP. @@ -101,7 +101,7 @@ pred pp-canonical-solution i:cs-instance, o:coq.pp. pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :- coq.env.typeof GR T, coq.prod-tgt->gref T F, - if (class-def (class _ F _)) (gref->modname F 2 "." ID) (coq.gref->string F ID), + if (class-def (class _ F _)) (gref->modname_short F "." ID) (coq.gref->string F ID), Pp = box (hov 0) [ str ID ]. pred main-canonical-projection i:string, i:gref, i:list cs-instance. @@ -127,11 +127,11 @@ pred main-coercion i:string, i:list coercion. main-coercion S [coercion GR _ Src Tgt|_] :- % format if (class-def (class _ Src _) ; class-def (class Src _ _)) - (Source = str {gref->modname Src 2 "."}) + (Source = str {gref->modname_short Src "."}) (coq.term->pp (global Src) Source), if2 (Tgt = grefclass TGR) (if (class-def (class _ TGR _) ; class-def (class TGR _ _)) - (Target = str {gref->modname TGR 2 "."}) + (Target = str {gref->modname_short TGR "."}) (coq.term->pp (global TGR) Target)) (Tgt = sortclass) (Target = str "Sortclass") @@ -306,7 +306,7 @@ main-factory-alias S _Const :- pred main-builder i:string, i:factoryname, i:mixinname. main-builder _S From To :- coq.say "HB: todo HB.about for builder from" - {gref->modname From 2 "."} "to" {gref->modname To 2 "."}. + {gref->modname_short From "."} "to" {gref->modname_short To "."}. pred compute-field-info.aux i:list id, i:list implicit_kind, o:list coq.pp. compute-field-info.aux [] _ []. @@ -323,8 +323,9 @@ compute-field-info Names Impls O :- compute-field-info.aux {std.rev Names} {std.rev Impls} Pp, std.intersperse spc {std.rev Pp} O. +% Print shortest qualified identifier of the module containing a gref pred pp-module i:gref, o:coq.pp. -pp-module M (str ID) :- gref->modname M 2 "." ID. +pp-module GR (str ID) :- gref->modname_short GR "." ID. pred pp-const i:constant, o:coq.pp. pp-const F (str ID) :- coq.gref->id (const F) ID. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 0eb53d2dc..000826a2a 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -137,6 +137,27 @@ gref->modname-label GR NComp Sep ModName :- std.take N PathRev L, std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. +pred string->modpath i:string, o:modpath. +string->modpath S MP :- + std.filter {coq.locate-all S} (l\l = loc-modpath _) L, + L = [loc-modpath MP]. + +pred gref->modname_short1 i:modpath, i:string, i:list string, o:string. +gref->modname_short1 _ S [] S. +gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'. +gref->modname_short1 MP S _ S :- string->modpath S MP. +gref->modname_short1 MP S [X|L] S' :- + gref->modname_short1 MP {std.string.concat "." [X,S]} L S'. + +% Print shortest qualified identifier of the module containing a gref +% Sep is used as separator +pred gref->modname_short i:gref, i:string, o:string. +gref->modname_short GR Sep IDS :- + coq.gref->path GR Path, + string->modpath {std.string.concat "." Path} MP, + gref->modname_short1 MP "" {std.rev Path} ID, + rex.replace "[.]" Sep ID IDS. + pred avoid-name-collision i:string, o:string. avoid-name-collision S S1 :- coq.locate-all S L, diff --git a/HB/graph.elpi b/HB/graph.elpi index b8baffcf4..b251c2f39 100644 --- a/HB/graph.elpi +++ b/HB/graph.elpi @@ -18,20 +18,11 @@ to-file File :- !, std.do! [ namespace private { -pred gref->modname i:gref, i:int, i:string, o:string. -gref->modname GR NComp Sep ModName :- - coq.gref->path GR Path, - std.rev Path Mods, - std.length Path Len, - if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), - std.take NComp Mods L, - std.string.concat Sep {std.rev L} ModName. - pred pp-coercion-dot i:out_stream, i:coercion. pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [ - output OC {gref->modname Tgt 2 "_"}, + output OC {gref->modname_short Tgt "_"}, output OC " -> ", - output OC {gref->modname Src 2 "_"}, + output OC {gref->modname_short Src "_"}, output OC ";\n", ]. pp-coercion-dot _ _. diff --git a/tests/about.v b/tests/about.v index 0baebc083..a8971ab2b 100644 --- a/tests/about.v +++ b/tests/about.v @@ -48,4 +48,11 @@ HB.about hierarchy_5_Ring__to__hierarchy_5_SemiRing. (* builder *) HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid. -HB.locate BinNums_Z__canonical__hierarchy_5_AddAG. \ No newline at end of file +HB.locate BinNums_Z__canonical__hierarchy_5_AddAG. + +(* Test minimally qualified names *) +Module Import hierarchy_5. +Module AddComoid. +End AddComoid. +End hierarchy_5. +HB.about Z. diff --git a/tests/about.v.out b/tests/about.v.out index ce0996219..3a56087fd 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are: - addr0 HB: AddMonoid_of_TYPE requires the following mixins: HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: AddMonoid_of_TYPE.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - S : Type - zero : AddMonoid.sort S @@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) HB: AddAG.type characterizing operations and axioms are: - addNr - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring -HB: hierarchy_5.AddMonoid.type is a structure +HB: AddMonoid.type is a structure (from "./examples/demo1/hierarchy_5.v", line 17) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: +HB: AddMonoid.type characterizing operations and axioms are: - addr0 - add0r - addrA - add - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring HB: Ring_of_AddAG is a factory (from "./examples/demo1/hierarchy_5.v", line 108) @@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are: - mulrDl - mulrDr HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and mul0r are derived from addrC and the other ring axioms, following a proof of Hankel (Gerhard Betsch. On the beginnings and development of near-ring @@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and HB: Ring_of_AddAG.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 108) HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - A : Type - one : A @@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, 1995). -HB: add is an operation of structure hierarchy_5.AddMonoid +HB: add is an operation of structure AddMonoid (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE +HB: add comes from mixin AddMonoid_of_TYPE (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddAG.sort is a canonical projection @@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values: - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - Z -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass +HB: AddAG.sort is a coercion from AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) HB: Z is canonically equipped with structures: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG + - AddMonoid + AddComoid + AddAG (from "(stdin)", line 5) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring + - BiNearRing + SemiRing + Ring (from "(stdin)", line 10) HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) + +HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 0, diff --git a/tests/about.v.out.15 b/tests/about.v.out.15 index 1f0c60604..e8aa4b533 100644 --- a/tests/about.v.out.15 +++ b/tests/about.v.out.15 @@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are: - addr0 HB: AddMonoid_of_TYPE requires the following mixins: HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: AddMonoid_of_TYPE.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - S : Type - zero : AddMonoid.sort S @@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) HB: AddAG.type characterizing operations and axioms are: - addNr - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring -HB: hierarchy_5.AddMonoid.type is a structure +HB: AddMonoid.type is a structure (from "./examples/demo1/hierarchy_5.v", line 17) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: +HB: AddMonoid.type characterizing operations and axioms are: - addr0 - add0r - addrA - add - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring HB: Ring_of_AddAG is a factory (from "./examples/demo1/hierarchy_5.v", line 108) @@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are: - mulrDl - mulrDr HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and mul0r are derived from addrC and the other ring axioms, following a proof of Hankel (Gerhard Betsch. On the beginnings and development of near-ring @@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and HB: Ring_of_AddAG.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 108) HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - A : Type - one : A @@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, 1995). -HB: add is an operation of structure hierarchy_5.AddMonoid +HB: add is an operation of structure AddMonoid (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE +HB: add comes from mixin AddMonoid_of_TYPE (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddAG.sort is a canonical projection @@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values: - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - Z -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass +HB: AddAG.sort is a coercion from AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) HB: Z is canonically equipped with structures: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG + - AddMonoid + AddComoid + AddAG (from "(stdin)", line 5) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring + - BiNearRing + SemiRing + Ring (from "(stdin)", line 10) HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) + +HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid +HB: synthesized in file File "(stdin)", line 5, column 122, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file File "(stdin)", line 5, column 0, character 127: From a1b507e658416ac4844257f9af4480417110d149 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 4 Aug 2022 16:53:29 +0200 Subject: [PATCH 29/60] Add merge sort in stdpp --- HB/common/stdpp.elpi | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index c228ff7ab..cd1ffaa4d 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -48,6 +48,25 @@ under.do! Then LP :- Then (_\ std.do! LP) _. pred map-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1. map-triple F G H (triple X Y Z) (triple X1 Y1 Z1) :- F X X1, G Y Y1, H Z Z1. +pred sort.split i:list A, o:list A, o:list A. +sort.split [] [] [] :- !. +sort.split [X] [X] [] :- !. +sort.split [X,Y|TL] [X|L1] [Y|L2] :- sort.split TL L1 L2. + +pred sort.merge i:(A -> A -> prop), i:list A, i:list A, o:list A. +sort.merge _ [] L L :- !. +sort.merge _ L [] L :- !. +sort.merge Rel [X1|L1] [X2|L2] [X1|M] :- Rel X1 X2, !, + sort.merge Rel L1 [X2|L2] M. +sort.merge Rel [X1|L1] [X2|L2] [X2|M] :- + sort.merge Rel [X1|L1] L2 M. + +pred sort i:list A, i:(A -> A -> prop), o:list A. +sort [] _ [] :- !. +sort [X] _ [X] :- !. +sort L Rel M :- + sort.split L L1 L2, sort L1 Rel S1, sort L2 Rel S2, sort.merge Rel S1 S2 M. + pred bubblesort i:list A, i:(A -> A -> prop), o:list A. bubblesort [] _ [] :- !. bubblesort [X] _ [X] :- !. From d2716c71dd93cbcb90f0d240befd108664d256ce Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 10:41:27 +0200 Subject: [PATCH 30/60] Export a few functions from about that will be used in paths --- HB/about.elpi | 44 ++++++++++++++++++++++++-------------------- 1 file changed, 24 insertions(+), 20 deletions(-) diff --git a/HB/about.elpi b/HB/about.elpi index b5f17cf73..5b90cfc1d 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -45,7 +45,7 @@ main-located S (loc-gref GR) :- from Factory Mixin GR, !, private.main-builder S Factory Mixin. main-located S (loc-gref GR) :- - std.filter {coq.CS.db-for _ (cs-gref GR)} (private.not1 private.unif-hint?) LV, + std.filter {coq.CS.db-for _ (cs-gref GR)} (not1 unif-hint?) LV, coq.CS.db-for GR _ LP, std.filter {coq.coercion.db} (c\c = coercion GR _ _ _) LC, if (LV = [], LP = [], LC = []) @@ -57,6 +57,29 @@ main-located S (loc-gref GR) :- main-located S (loc-abbreviation _) :- coq.error "HB: unknown abbreviation" S. +/* things also used in paths.elpi ------------------------------------------ */ + +shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }. + +pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp. +bulletize1 F X (glue [str "- ", M]) :- F X M. + +pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. +bulletize [] _ empty. +bulletize L F (glue [brk 0 0 | PLB]) :- + std.map L (bulletize1 F) PL, + std.intersperse (brk 0 0) PL PLB. + +% Print shortest qualified identifier of the module containing a gref +pred pp-module i:gref, o:coq.pp. +pp-module GR (str ID) :- gref->modname_short GR "." ID. + +pred unif-hint? i:cs-instance. +unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_]. + +pred not1 i:(A -> prop), i:A. +not1 P X :- not (P X). + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ @@ -323,10 +346,6 @@ compute-field-info Names Impls O :- compute-field-info.aux {std.rev Names} {std.rev Impls} Pp, std.intersperse spc {std.rev Pp} O. -% Print shortest qualified identifier of the module containing a gref -pred pp-module i:gref, o:coq.pp. -pp-module GR (str ID) :- gref->modname_short GR "." ID. - pred pp-const i:constant, o:coq.pp. pp-const F (str ID) :- coq.gref->id (const F) ID. @@ -337,15 +356,6 @@ pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop). pp-if-verbose V P :- get-option "verbose" tt, !, P V. pp-if-verbose empty _. -pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp. -bulletize1 F X (glue [str "- ", M]) :- F X M. - -pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. -bulletize [] _ empty. -bulletize L F (glue [brk 0 0 | PLB]) :- - std.map L (bulletize1 F) PL, - std.intersperse (brk 0 0) PL PLB. - pred pp-loc-of i:gref, o:coq.pp. pp-loc-of GR PP :- decl-location GR Loc, !, pp-loc Loc PP. pp-loc-of _ coq.pp.empty. @@ -378,10 +388,4 @@ print-docstring GR :- (coq.say {coq.pp->string (box (hov 5) [str"Doc: ",Doc])}) true. -pred unif-hint? i:cs-instance. -unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_]. - -pred not1 i:(A -> prop), i:A. -not1 P X :- not (P X). - }} From fefc469505861ca11ae9bc4f77d5c6dbaab6687f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 3 Aug 2022 18:00:30 +0200 Subject: [PATCH 31/60] Add hb.howto --- HB/howto.elpi | 113 ++++++++++++++++++++++++++++++++++ Makefile.test-suite.coq.local | 1 + structures.v | 33 ++++++++++ tests/howto.v | 25 ++++++++ tests/howto.v.out | 28 +++++++++ 5 files changed, 200 insertions(+) create mode 100644 HB/howto.elpi create mode 100644 tests/howto.v create mode 100644 tests/howto.v.out diff --git a/HB/howto.elpi b/HB/howto.elpi new file mode 100644 index 000000000..b0913b8db --- /dev/null +++ b/HB/howto.elpi @@ -0,0 +1,113 @@ +/* Hierarchy Builder: algebraic hierarchies made easy + This software is released under the terms of the MIT license */ + +namespace howto { + +pred main i:string, i:string, i:int. +main ST STgt Depth :- + private.mixins-on-string ST MLSrc, + private.mixins-in-string STgt MLTgt, + private.list-diff MLTgt MLSrc ML, + if (ML = []) (coq.say "HB: nothing to do.") + (private.paths-from-for-step MLSrc ML Depth R, + if (R = []) + (coq.error "HB: no solution found, try to increase search depth.") + (private.pp-solutions R)). + + +/* ------------------------------------------------------------------------- */ +/* ----------------------------- private code ------------------------------ */ +/* ------------------------------------------------------------------------- */ + +namespace private { + +shorten coq.pp.{ v , hov , spc , str , box , glue }. + +% L1 \subseteq L2 +pred incl i:list A, i:list A. +incl L1 L2 :- std.forall L1 (std.mem L2). + +% R = L1 \ L2 +pred list-diff i:list A, i:list A, o:list A. +list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R. + +% R = L1 U L2 +pred union i:list A, i:list A, o:list A. +union L1 L2 R :- + std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R. + +% [mixins-on-string S ML] list mixins in structures [S] is equipped with +pred mixins-on-string i:string, o:list mixinname. +mixins-on-string S ML :- + coq.locate S GR, + std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV, + std.fold LV [] mixins-on-string.aux ML. +mixins-on-string.aux (cs-instance _ _ GR) L L' :- + coq.prod-tgt->gref {coq.env.typeof GR} F, + class-def (class _ F MLWP), + union L {list-w-params_list MLWP} L'. + +% [mixins-in-string S ML] list mixins contained in structure [S] +pred mixins-in-string i:string, o:list mixinname. +mixins-in-string S ML :- + coq.locate S GR, class-def (class _ GR MLwP), list-w-params_list MLwP ML. + +% a type to store a factory along with the mixins it depends on +% and the mixins it provides +kind factory_deps_prov type. +type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov. + +% get all available factories in the above type +pred list_factories o:list factory_deps_prov. +list_factories FL :- + std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL. +list_factories.aux (factory-constructor F _) (fdp F DML PML) :- + list-w-params_list {gref-deps F} DML, + list-w-params_list {factory-provides F} PML. + +% [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences +% of at most [K] factories that could, starting from mixins [MLSrc], +% build exactly the mixins [ML] +pred paths-from-for-step i:list mixinname, i:list mixinname, i:int, + o:list (list factoryname). +paths-from-for-step MLSrc ML K R :- + std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL, + paths-from-for-step-using MLSrc ML K FL R. + +% [paths-from-for-step-using MLSrc ML K FL R] +% same as [paths-from-for-step MLSrc ML K R] using only factories in [FL] +pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int, + i:list factory_deps_prov, o:list (list factoryname). +paths-from-for-step-using _ _ K _ [] :- K i< 0. +paths-from-for-step-using _ [] _ _ [[]] :- !. +paths-from-for-step-using MLSrc ML K FL R :- + K' is K - 1, + std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep, + std.fold FLdep [] (paths-from-for-step-using.aux MLSrc ML FL K') R. +paths-from-for-step-using.aux MLSrc ML FL' K' (fdp F _ MLF) L R :- + std.append MLSrc MLF MLSrc', + list-diff ML MLF ML', + std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML', + paths-from-for-step-using MLSrc' ML' K' FML' R', + std.map R' (l\r\r = [F|l]) R'', + std.append L R'' R. + +pred pp-solutions i:list (list factoryname). +pp-solutions LLF :- + std.sort LLF + (l1\l2\sigma s1 s2\std.length l1 s1, std.length l2 s2, s1 i=< s2) + SLLF, + % format + PpSolutions = box (v 4) [ + str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):", + {about.bulletize SLLF pp-solution}], + % print + coq.say {coq.pp->string PpSolutions}, + coq.say. + +pred pp-solution i:list factoryname o:coq.pp. +pp-solution L (box (hov 0) PLS) :- + std.map L about.pp-module PL, + std.intersperse (glue [str ";", spc]) PL PLS. + +}} \ No newline at end of file diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index 38dcbeeb7..1bef12aaa 100644 --- a/Makefile.test-suite.coq.local +++ b/Makefile.test-suite.coq.local @@ -20,6 +20,7 @@ DIFF=\ post-all:: $(call DIFF, tests/compress_coe.v) $(call DIFF, tests/about.v) + $(call DIFF, tests/howto.v) $(call DIFF, tests/missing_join_error.v) $(call DIFF, tests/not_same_key.v) $(call DIFF, tests/hnf.v) \ No newline at end of file diff --git a/structures.v b/structures.v index 3fc0415dd..eae16517f 100644 --- a/structures.v +++ b/structures.v @@ -295,6 +295,39 @@ Elpi Typecheck. Elpi Export HB.about. +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + +(** [HB.howto T Foo.type d] prints possible sequences of factories + to equip a type [T] with a structure [Foo.type], taking into account + structures already instantiated on [T]. The search depth [d] + is the maximum length of the sequences, 3 by default. +*) + +#[arguments(raw)] Elpi Command HB.howto. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/common/log.elpi". +Elpi Accumulate File "HB/about.elpi". +Elpi Accumulate File "HB/howto.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ + +main [str ST, str STgt] :- !, + with-attributes (with-logging (howto.main ST STgt 3)). +main [str ST, str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main ST STgt Depth)). + +main _ :- coq.error "Usage: HB.howto [].". +}}. +Elpi Typecheck. +Elpi Export HB.howto. + + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) diff --git a/tests/howto.v b/tests/howto.v new file mode 100644 index 000000000..3f8741ecb --- /dev/null +++ b/tests/howto.v @@ -0,0 +1,25 @@ +From Coq Require Import ZArith ssrfun ssreflect. +From HB Require Import structures. +From HB Require Import demo1.hierarchy_5. + +HB.howto Z Ring.type. + +HB.howto Z Ring.type 2. + +Fail HB.howto Z Ring.type 0. + +HB.instance + Definition _ := + AddAG_of_TYPE.Build Z 0%Z Z.add Z.opp + Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l. + +HB.howto Z Ring.type. + +HB.instance + Definition _ := + Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul + Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l + Z.mul_assoc Z.mul_1_l Z.mul_1_r + Z.mul_add_distr_r Z.mul_add_distr_l. + +HB.howto Z Ring.type. diff --git a/tests/howto.v.out b/tests/howto.v.out new file mode 100644 index 000000000..0fc1a1661 --- /dev/null +++ b/tests/howto.v.out @@ -0,0 +1,28 @@ +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + +The command has indeed failed with message: +HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid + +HB: nothing to do. From 7240a672b74c766381ffbc7a6a9248b67206d488 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 14:27:26 +0200 Subject: [PATCH 32/60] Sort output by lexicographic order This looks less random and is easier to read as solutions sharing common prefix are grouped together. --- HB/howto.elpi | 19 +++++++++++++++---- tests/howto.v.out | 16 ++++++++-------- 2 files changed, 23 insertions(+), 12 deletions(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index b0913b8db..3991f8505 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -36,6 +36,19 @@ pred union i:list A, i:list A, o:list A. union L1 L2 R :- std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R. +pred lt-gref i:gref, i:gref. +lt-gref X Y :- + gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY. + +pred size-order i:(list A -> list A -> prop), i:list A, i:list A. +size-order Rel L1 L2 :- + std.length L1 S1, std.length L2 S2, !, (S1 i< S2; (S1 = S2, !, Rel L1 L2)). + +pred lexi-order i:list gref, i:list gref. +lexi-order [] []. +lexi-order [X1|_] [X2|_] :- lt-gref X1 X2. +lexi-order [X|T1] [X|T2] :- lexi-order T1 T2. + % [mixins-on-string S ML] list mixins in structures [S] is equipped with pred mixins-on-string i:string, o:list mixinname. mixins-on-string S ML :- @@ -94,9 +107,7 @@ paths-from-for-step-using.aux MLSrc ML FL' K' (fdp F _ MLF) L R :- pred pp-solutions i:list (list factoryname). pp-solutions LLF :- - std.sort LLF - (l1\l2\sigma s1 s2\std.length l1 s1, std.length l2 s2, s1 i=< s2) - SLLF, + std.sort LLF (size-order lexi-order) SLLF, % format PpSolutions = box (v 4) [ str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):", @@ -104,7 +115,7 @@ pp-solutions LLF :- % print coq.say {coq.pp->string PpSolutions}, coq.say. - + pred pp-solution i:list factoryname o:coq.pp. pp-solution L (box (hov 0) PLS) :- std.map L about.pp-module PL, diff --git a/tests/howto.v.out b/tests/howto.v.out index 0fc1a1661..57943f99e 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -1,22 +1,22 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid - - AddAG_of_TYPE; Ring_of_AddAG - - AddAG_of_TYPE; BiNearRing_of_AddMonoid - - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid - - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid - - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid - - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid + - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - Ring_of_TYPE - - AddComoid_of_TYPE; Ring_of_AddComoid - - AddAG_of_TYPE; SemiRing_of_AddComoid - AddAG_of_TYPE; BiNearRing_of_AddMonoid - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid The command has indeed failed with message: HB: no solution found, try to increase search depth. From d5be509f2484dd5399efb2bd1ae4eeb471a205ae Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 15:53:20 +0200 Subject: [PATCH 33/60] Accept both term and string input --- HB/howto.elpi | 23 ++++++++++++++--------- structures.v | 16 ++++++++++------ 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index 3991f8505..0b109d253 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -3,9 +3,15 @@ namespace howto { -pred main i:string, i:string, i:int. -main ST STgt Depth :- - private.mixins-on-string ST MLSrc, +pred main-trm i:term, i:string, i:int. +main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth. + +pred main-str i:string, i:string, i:int. +main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. + +pred main-gref i:gref, i:string, i:int. +main-gref GR STgt Depth :- + private.mixins-on-gref GR MLSrc, private.mixins-in-string STgt MLTgt, private.list-diff MLTgt MLSrc ML, if (ML = []) (coq.say "HB: nothing to do.") @@ -49,13 +55,12 @@ lexi-order [] []. lexi-order [X1|_] [X2|_] :- lt-gref X1 X2. lexi-order [X|T1] [X|T2] :- lexi-order T1 T2. -% [mixins-on-string S ML] list mixins in structures [S] is equipped with -pred mixins-on-string i:string, o:list mixinname. -mixins-on-string S ML :- - coq.locate S GR, +% [mixins-on-gref GR ML] list mixins in structures [GR] is equipped with +pred mixins-on-gref i:gref, o:list mixinname. +mixins-on-gref GR ML :- std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV, - std.fold LV [] mixins-on-string.aux ML. -mixins-on-string.aux (cs-instance _ _ GR) L L' :- + std.fold LV [] mixins-on-gref.aux ML. +mixins-on-gref.aux (cs-instance _ _ GR) L L' :- coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'. diff --git a/structures.v b/structures.v index eae16517f..9ce74cefd 100644 --- a/structures.v +++ b/structures.v @@ -299,7 +299,7 @@ Elpi Export HB.about. (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) -(** [HB.howto T Foo.type d] prints possible sequences of factories +(** [HB.howto (T) Foo.type d] prints possible sequences of factories to equip a type [T] with a structure [Foo.type], taking into account structures already instantiated on [T]. The search depth [d] is the maximum length of the sequences, 3 by default. @@ -317,12 +317,16 @@ Elpi Accumulate File "HB/howto.elpi". Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ -main [str ST, str STgt] :- !, - with-attributes (with-logging (howto.main ST STgt 3)). -main [str ST, str STgt, int Depth] :- !, - with-attributes (with-logging (howto.main ST STgt Depth)). +main [trm T, str STgt] :- !, + with-attributes (with-logging (howto.main-trm T STgt 3)). +main [trm T, str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-trm T STgt Depth)). +main [str T, str STgt] :- !, + with-attributes (with-logging (howto.main-str T STgt 3)). +main [str T, str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-str T STgt Depth)). -main _ :- coq.error "Usage: HB.howto [].". +main _ :- coq.error "Usage: HB.howto () [].". }}. Elpi Typecheck. Elpi Export HB.howto. From e6f7114d61975e9d9a6ca3f5824e6fd9d9a95a75 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 16:20:49 +0200 Subject: [PATCH 34/60] Make first argument optional --- HB/howto.elpi | 4 ++++ structures.v | 8 +++++++- tests/howto.v | 4 ++++ tests/howto.v.out | 20 ++++++++++++++++++++ 4 files changed, 35 insertions(+), 1 deletion(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index 0b109d253..87a67ee92 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -12,6 +12,10 @@ main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. pred main-gref i:gref, i:string, i:int. main-gref GR STgt Depth :- private.mixins-on-gref GR MLSrc, + main-from MLSrc STgt Depth. + +pred main-from i:list mixinname, i:string, i:int. +main-from MLSrc STgt Depth :- private.mixins-in-string STgt MLTgt, private.list-diff MLTgt MLSrc ML, if (ML = []) (coq.say "HB: nothing to do.") diff --git a/structures.v b/structures.v index 9ce74cefd..fc761dd1e 100644 --- a/structures.v +++ b/structures.v @@ -303,6 +303,8 @@ Elpi Export HB.about. to equip a type [T] with a structure [Foo.type], taking into account structures already instantiated on [T]. The search depth [d] is the maximum length of the sequences, 3 by default. + The first argument [T] is optional, when ommited [Foo.type] is built + from scratch. *) #[arguments(raw)] Elpi Command HB.howto. @@ -325,8 +327,12 @@ main [str T, str STgt] :- !, with-attributes (with-logging (howto.main-str T STgt 3)). main [str T, str STgt, int Depth] :- !, with-attributes (with-logging (howto.main-str T STgt Depth)). +main [str STgt] :- !, + with-attributes (with-logging (howto.main-from [] STgt 3)). +main [str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-from [] STgt Depth)). -main _ :- coq.error "Usage: HB.howto () [].". +main _ :- coq.error "Usage: HB.howto [()] [].". }}. Elpi Typecheck. Elpi Export HB.howto. diff --git a/tests/howto.v b/tests/howto.v index 3f8741ecb..c16e9f2c6 100644 --- a/tests/howto.v +++ b/tests/howto.v @@ -2,6 +2,10 @@ From Coq Require Import ZArith ssrfun ssreflect. From HB Require Import structures. From HB Require Import demo1.hierarchy_5. +HB.howto Ring.type. + +HB.howto Ring.type 2. + HB.howto Z Ring.type. HB.howto Z Ring.type 2. diff --git a/tests/howto.v.out b/tests/howto.v.out index 57943f99e..c6a0685ec 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -18,6 +18,26 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_TYPE; SemiRing_of_AddComoid - AddComoid_of_TYPE; Ring_of_AddComoid +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid + - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + The command has indeed failed with message: HB: no solution found, try to increase search depth. HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): From 7edb21732fe9b93157b2c10ae5a12e2dc93a173a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 5 Aug 2022 16:40:21 +0200 Subject: [PATCH 35/60] First argument can be another structure --- HB/howto.elpi | 33 ++++++++++++++++++--------------- structures.v | 6 +++++- tests/howto.v | 4 ++++ tests/howto.v.out | 13 +++++++++++++ 4 files changed, 40 insertions(+), 16 deletions(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index 87a67ee92..1a5244286 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -10,13 +10,17 @@ pred main-str i:string, i:string, i:int. main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. pred main-gref i:gref, i:string, i:int. +main-gref GR STgt Depth :- class-def (class _ GR _), !, + private.mixins-in-structures [GR] MLSrc, + main-from MLSrc STgt Depth. main-gref GR STgt Depth :- - private.mixins-on-gref GR MLSrc, + private.structures-on-gref GR SL, + private.mixins-in-structures SL MLSrc, main-from MLSrc STgt Depth. pred main-from i:list mixinname, i:string, i:int. main-from MLSrc STgt Depth :- - private.mixins-in-string STgt MLTgt, + private.mixins-in-structures [{coq.locate STgt}] MLTgt, private.list-diff MLTgt MLSrc ML, if (ML = []) (coq.say "HB: nothing to do.") (private.paths-from-for-step MLSrc ML Depth R, @@ -59,20 +63,19 @@ lexi-order [] []. lexi-order [X1|_] [X2|_] :- lt-gref X1 X2. lexi-order [X|T1] [X|T2] :- lexi-order T1 T2. -% [mixins-on-gref GR ML] list mixins in structures [GR] is equipped with -pred mixins-on-gref i:gref, o:list mixinname. -mixins-on-gref GR ML :- +% [structures-on-gref GR ML] list structures [GR] is equipped with +pred structures-on-gref i:gref, o:list structure. +structures-on-gref GR SL :- std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV, - std.fold LV [] mixins-on-gref.aux ML. -mixins-on-gref.aux (cs-instance _ _ GR) L L' :- - coq.prod-tgt->gref {coq.env.typeof GR} F, - class-def (class _ F MLWP), - union L {list-w-params_list MLWP} L'. - -% [mixins-in-string S ML] list mixins contained in structure [S] -pred mixins-in-string i:string, o:list mixinname. -mixins-in-string S ML :- - coq.locate S GR, class-def (class _ GR MLwP), list-w-params_list MLwP ML. + std.map LV structures-on-gref.aux SL. +structures-on-gref.aux (cs-instance _ _ GR) F :- + coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _). + +% [mixins-in-structures SL ML] list mixins in structures [SL] +pred mixins-in-structures i:list structure, o:list mixinname. +mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML. +mixins-in-structures.aux F L L' :- + class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'. % a type to store a factory along with the mixins it depends on % and the mixins it provides diff --git a/structures.v b/structures.v index fc761dd1e..5c09448b3 100644 --- a/structures.v +++ b/structures.v @@ -305,6 +305,8 @@ Elpi Export HB.about. is the maximum length of the sequences, 3 by default. The first argument [T] is optional, when ommited [Foo.type] is built from scratch. + Finally, the first argument can be another structure [Bar.type], + in which case [Foo.type] is built starting from [Bar.type]. *) #[arguments(raw)] Elpi Command HB.howto. @@ -332,7 +334,9 @@ main [str STgt] :- !, main [str STgt, int Depth] :- !, with-attributes (with-logging (howto.main-from [] STgt Depth)). -main _ :- coq.error "Usage: HB.howto [()] [].". +main _ :- + coq.error + "Usage: HB.howto [()|] [].". }}. Elpi Typecheck. Elpi Export HB.howto. diff --git a/tests/howto.v b/tests/howto.v index c16e9f2c6..b7265d19b 100644 --- a/tests/howto.v +++ b/tests/howto.v @@ -12,6 +12,8 @@ HB.howto Z Ring.type 2. Fail HB.howto Z Ring.type 0. +HB.howto AddComoid.type Ring.type. + HB.instance Definition _ := AddAG_of_TYPE.Build Z 0%Z Z.add Z.opp @@ -19,6 +21,8 @@ HB.instance HB.howto Z Ring.type. +HB.howto AddAG.type Ring.type. + HB.instance Definition _ := Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul diff --git a/tests/howto.v.out b/tests/howto.v.out index c6a0685ec..56fd855ba 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -40,6 +40,19 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): The command has indeed failed with message: HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_AddComoid + - AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddAG_of_AddComoid; Ring_of_AddAG + - AddAG_of_AddComoid; SemiRing_of_AddComoid + - BiNearRing_of_AddMonoid; AddAG_of_AddComoid + - SemiRing_of_AddComoid; AddAG_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid + HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid - Ring_of_AddAG From e51de325cfd5587c4e3c3e0c9bdccadb1e966f9b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 6 Aug 2022 12:57:43 +0200 Subject: [PATCH 36/60] Remove solutions that are identical up to permutation --- HB/howto.elpi | 32 +++++++++++++++++++++++--------- tests/howto.v.out | 6 ------ 2 files changed, 23 insertions(+), 15 deletions(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index 1a5244286..5956b608c 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -50,6 +50,11 @@ pred union i:list A, i:list A, o:list A. union L1 L2 R :- std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R. +pred insert-sorted i:(A -> A -> prop), i:A, i:list A, o:list A. +insert-sorted _ X [] [X] :- !. +insert-sorted Rel X [Y|T] [X,Y|T] :- Rel X Y, !. +insert-sorted Rel X [Y|T] [Y|T'] :- insert-sorted Rel X T T', !. + pred lt-gref i:gref, i:gref. lt-gref X Y :- gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY. @@ -97,23 +102,32 @@ pred paths-from-for-step i:list mixinname, i:list mixinname, i:int, o:list (list factoryname). paths-from-for-step MLSrc ML K R :- std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL, - paths-from-for-step-using MLSrc ML K FL R. + paths-from-for-step-using MLSrc ML K [] [] FL _ R. -% [paths-from-for-step-using MLSrc ML K FL R] +% [paths-from-for-step-using MLSrc ML K Pre KnownPre FL KnownPre' R] % same as [paths-from-for-step MLSrc ML K R] using only factories in [FL] +% [Pre] is a (sorted) prefix that is looked into the list of known (sorted) +% prefixes [KnownPre] to avoid generating identical solutions up to permutations pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int, - i:list factory_deps_prov, o:list (list factoryname). -paths-from-for-step-using _ _ K _ [] :- K i< 0. -paths-from-for-step-using _ [] _ _ [[]] :- !. -paths-from-for-step-using MLSrc ML K FL R :- + i:list factoryname, i:list (list factoryname), i:list factory_deps_prov, + o:list (list factoryname), o:list (list factoryname). +paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0. +paths-from-for-step-using _ _ _ Pre KnownPre _ KnownPre [] :- + std.mem KnownPre Pre, !. +paths-from-for-step-using _ [] _ Pre KnownPre _ [Pre|KnownPre] [[]] :- !. +paths-from-for-step-using MLSrc ML K Pre KnownPre FL [Pre|KnownPre'] R :- K' is K - 1, std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep, - std.fold FLdep [] (paths-from-for-step-using.aux MLSrc ML FL K') R. -paths-from-for-step-using.aux MLSrc ML FL' K' (fdp F _ MLF) L R :- + std.fold FLdep (pr KnownPre []) + (paths-from-for-step-using.aux MLSrc ML FL K' Pre) + (pr KnownPre' R). +paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L) + (pr KnPre' R) :- std.append MLSrc MLF MLSrc', list-diff ML MLF ML', + insert-sorted lt-gref F Pre Pre', std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML', - paths-from-for-step-using MLSrc' ML' K' FML' R', + paths-from-for-step-using MLSrc' ML' K' Pre' KnPre FML' KnPre' R', std.map R' (l\r\r = [F|l]) R'', std.append L R'' R. diff --git a/tests/howto.v.out b/tests/howto.v.out index 56fd855ba..a83cbce85 100644 --- a/tests/howto.v.out +++ b/tests/howto.v.out @@ -7,8 +7,6 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid - - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): @@ -27,8 +25,6 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid - - AddComoid_of_TYPE; BiNearRing_of_AddMonoid; AddAG_of_AddComoid - - AddComoid_of_TYPE; SemiRing_of_AddComoid; AddAG_of_AddComoid - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): @@ -45,8 +41,6 @@ HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - AddAG_of_AddComoid; BiNearRing_of_AddMonoid - AddAG_of_AddComoid; Ring_of_AddAG - AddAG_of_AddComoid; SemiRing_of_AddComoid - - BiNearRing_of_AddMonoid; AddAG_of_AddComoid - - SemiRing_of_AddComoid; AddAG_of_AddComoid HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): - BiNearRing_of_AddMonoid From 4bf538067dab9cb1aa397959f4dfa8ffc169353a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 6 Aug 2022 17:29:09 +0200 Subject: [PATCH 37/60] Automatically increase search depth when nothing found Except if a search depth was explicitly provided, in which case we just enforce it. --- HB/howto.elpi | 26 +++++++++++++++++--------- structures.v | 12 ++++++------ 2 files changed, 23 insertions(+), 15 deletions(-) diff --git a/HB/howto.elpi b/HB/howto.elpi index 5956b608c..0d84be4b9 100644 --- a/HB/howto.elpi +++ b/HB/howto.elpi @@ -3,13 +3,13 @@ namespace howto { -pred main-trm i:term, i:string, i:int. +pred main-trm i:term, i:string, i:option int. main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth. -pred main-str i:string, i:string, i:int. +pred main-str i:string, i:string, i:option int. main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. -pred main-gref i:gref, i:string, i:int. +pred main-gref i:gref, i:string, i:option int. main-gref GR STgt Depth :- class-def (class _ GR _), !, private.mixins-in-structures [GR] MLSrc, main-from MLSrc STgt Depth. @@ -18,15 +18,23 @@ main-gref GR STgt Depth :- private.mixins-in-structures SL MLSrc, main-from MLSrc STgt Depth. -pred main-from i:list mixinname, i:string, i:int. +pred main-from i:list mixinname, i:string, i:option int. main-from MLSrc STgt Depth :- private.mixins-in-structures [{coq.locate STgt}] MLTgt, private.list-diff MLTgt MLSrc ML, - if (ML = []) (coq.say "HB: nothing to do.") - (private.paths-from-for-step MLSrc ML Depth R, - if (R = []) - (coq.error "HB: no solution found, try to increase search depth.") - (private.pp-solutions R)). + if (ML = []) (coq.say "HB: nothing to do.") (main-from.aux MLSrc ML Depth). +main-from.aux MLSrc ML (some Depth) :- main-increase-depth MLSrc ML Depth false. +main-from.aux MLSrc ML none :- main-increase-depth MLSrc ML 3 true. + +pred main-increase-depth i:list mixinname, i:list mixinname, i:int, i:prop. +main-increase-depth MLSrc ML Depth AutoIncrease :- + private.paths-from-for-step MLSrc ML Depth R, + if (not (R = [])) (private.pp-solutions R) + (if AutoIncrease + (Depth' is Depth + 1, + coq.say "HB: no solution found at depth" Depth "looking at depth" Depth', + main-increase-depth MLSrc ML Depth' true) + (coq.error "HB: no solution found, try to increase search depth.")). /* ------------------------------------------------------------------------- */ diff --git a/structures.v b/structures.v index 5c09448b3..8dcb68a88 100644 --- a/structures.v +++ b/structures.v @@ -322,17 +322,17 @@ Elpi Accumulate Db hb.db. Elpi Accumulate lp:{{ main [trm T, str STgt] :- !, - with-attributes (with-logging (howto.main-trm T STgt 3)). + with-attributes (with-logging (howto.main-trm T STgt none)). main [trm T, str STgt, int Depth] :- !, - with-attributes (with-logging (howto.main-trm T STgt Depth)). + with-attributes (with-logging (howto.main-trm T STgt (some Depth))). main [str T, str STgt] :- !, - with-attributes (with-logging (howto.main-str T STgt 3)). + with-attributes (with-logging (howto.main-str T STgt none)). main [str T, str STgt, int Depth] :- !, - with-attributes (with-logging (howto.main-str T STgt Depth)). + with-attributes (with-logging (howto.main-str T STgt (some Depth))). main [str STgt] :- !, - with-attributes (with-logging (howto.main-from [] STgt 3)). + with-attributes (with-logging (howto.main-from [] STgt none)). main [str STgt, int Depth] :- !, - with-attributes (with-logging (howto.main-from [] STgt Depth)). + with-attributes (with-logging (howto.main-from [] STgt (some Depth))). main _ :- coq.error From 5b2007f809934ef9928f8ff405993089110dec3d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Aug 2022 10:21:55 +0200 Subject: [PATCH 38/60] Mention HB.howto in README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 3c92c553b..8e158441b 100644 --- a/README.md +++ b/README.md @@ -150,6 +150,7 @@ opam install coq-hierarchy-builder - `HB.locate` is similar to `Locate`, prints file name and line of any global constant synthesized by HB - `HB.graph` prints the structure hierarchy to a dot file + - `HB.howto` prints sequences of factories to equip a type with a given structure - HB debug commands: - `HB.status` dumps the contents of the hierarchy (debug purposes) From 381b8ef5025fb89099bd216a155fdf8489b1ef87 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Aug 2022 14:12:55 +0200 Subject: [PATCH 39/60] [CI] Updat Nix toolbox --- .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/coq-elpi/default.nix | 63 -------------------------- .nix/ocaml-overlays/elpi/default.nix | 53 ---------------------- 3 files changed, 1 insertion(+), 117 deletions(-) delete mode 100644 .nix/coq-overlays/coq-elpi/default.nix delete mode 100644 .nix/ocaml-overlays/elpi/default.nix diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index dd2bd938d..fddb4f818 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"be976db262f1dc9f6e013153f263182e14372246" +"a2aa6afce9ebfea39501cdf43a3a3bd08e557a26" diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix deleted file mode 100644 index 6c564594c..000000000 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ /dev/null @@ -1,63 +0,0 @@ -{ lib, mkCoqDerivation, which, coq, version ? null }: - -with builtins; with lib; let - elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ - { case = "8.11"; out = { version = "1.11.4"; };} - { case = "8.12"; out = { version = "1.12.0"; };} - { case = "8.13"; out = { version = "1.13.7"; };} - { case = "8.14"; out = { version = "1.13.7"; };} - { case = "8.15"; out = { version = "1.16.5"; };} - { case = "8.16"; out = { version = "1.16.5"; };} - ] {} ); -in mkCoqDerivation { - pname = "elpi"; - repo = "coq-elpi"; - owner = "LPCIC"; - inherit version; - defaultVersion = lib.switch coq.coq-version [ - { case = "8.16"; out = "1.15.3"; } - { case = "8.15"; out = "1.14.0"; } - { case = "8.14"; out = "1.11.2"; } - { case = "8.13"; out = "1.11.1"; } - { case = "8.12"; out = "1.8.3_8.12"; } - { case = "8.11"; out = "1.6.3_8.11"; } - ] null; - release."1.15.3".sha256 = "0vsgpflvfbbpbri3xfdhkz24bc36gy90f0mh0nr9ml6pqyp0ygji"; - release."1.14.0".sha256 = "1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"; - release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; - release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; - release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; - release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; - release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; - release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; - release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; - release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; - release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; - release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; - release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; - release."1.8.3_8.12".version = "1.8.3"; - release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; - release."1.8.2_8.12".version = "1.8.2"; - release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; - release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; - release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; - release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; - release."1.6.3_8.11".version = "1.6.3"; - release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; - release."1.6.2_8.11".version = "1.6.2"; - release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; - release."1.6.1_8.11".version = "1.6.1"; - release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; - release."1.6.0_8.11".version = "1.6.0"; - release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; - releaseRev = v: "v${v}"; - - mlPlugin = true; - propagatedBuildInputs = [ elpi ]; - - meta = { - description = "Coq plugin embedding ELPI."; - maintainers = [ maintainers.cohencyril ]; - license = licenses.lgpl21Plus; - }; -} diff --git a/.nix/ocaml-overlays/elpi/default.nix b/.nix/ocaml-overlays/elpi/default.nix deleted file mode 100644 index bca9d8c90..000000000 --- a/.nix/ocaml-overlays/elpi/default.nix +++ /dev/null @@ -1,53 +0,0 @@ -{ lib -, buildDunePackage, camlp5 -, ocaml -, menhir, menhirLib -, stdlib-shims -, re, perl, ncurses -, ppxlib, ppx_deriving, atdgen -, coqPackages -, version ? if lib.versionAtLeast ocaml.version "4.07" then "1.16.2" else "1.14.1" -}: -with lib; -let fetched = coqPackages.metaFetch ({ - release."1.16.5".sha256 = "sha256:1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl"; - release."1.16.2".sha256 = "sha256:0j4vbqbcz971pfhp8gxiaqpkzsjiisjgpybf6z1i65f1pavyfyss"; - release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s="; - release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar"; - release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis="; - release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r"; - release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka"; - release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044"; - release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr"; - release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is"; - release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5"; - releaseRev = v: "v${v}"; - location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; }; - }) version; -in -buildDunePackage rec { - pname = "elpi"; - inherit (fetched) version src; - - minimalOCamlVersion = "4.04"; - - buildInputs = [ perl ncurses ] - ++ optional (versionAtLeast version "1.15" || version == "dev") menhir; - - propagatedBuildInputs = [ re stdlib-shims ] - ++ (if versionAtLeast version "1.15" || version == "dev" - then [ menhirLib ] - else [ camlp5 ] ) - ++ [ ppxlib ppx_deriving atdgen ]; - - meta = { - description = "Embeddable λProlog Interpreter"; - license = licenses.lgpl21Plus; - maintainers = [ maintainers.vbgl ]; - homepage = "https://github.com/LPCIC/elpi"; - }; - - postPatch = '' - substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols" - ''; -} From 9845cb376b56f8c1fb01d77bb10edabfe48ca889 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Feb 2022 09:44:29 +0100 Subject: [PATCH 40/60] HB.pack was asserting the key is a type but we also support hierarchies of functions --- HB/pack.elpi | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/HB/pack.elpi b/HB/pack.elpi index 3da251b1c..b957db382 100644 --- a/HB/pack.elpi +++ b/HB/pack.elpi @@ -14,7 +14,10 @@ main Ty Args Instance :- std.do! [ get-constructor Class KC, get-constructor Structure KS, - std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "HB.pack: not a type", + std.assert-ok! (d\ + (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ; + coq.elaborate-skeleton TSkel _ T d + ) "HB.pack: not a well typed key", private.elab-factories FactoriesSkel T Factories, From c902e73e6119299abf9b24fda736bbc9e484e565 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 14:27:43 +0200 Subject: [PATCH 41/60] test --- _CoqProject.test-suite | 2 +- tests/{factory_sort_tac.v => hb_pack.v} | 13 ++++++++++++- 2 files changed, 13 insertions(+), 2 deletions(-) rename tests/{factory_sort_tac.v => hb_pack.v} (88%) diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index b5ff7af61..5751ac2ea 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -68,7 +68,7 @@ tests/lock.v tests/interleave_context.v tests/not_same_key.v #tests/factory_sort.v -tests/factory_sort_tac.v +tests/hb_pack.v tests/declare.v tests/short.v tests/primitive_records.v diff --git a/tests/factory_sort_tac.v b/tests/hb_pack.v similarity index 88% rename from tests/factory_sort_tac.v rename to tests/hb_pack.v index ccf6cb743..4fb1ab282 100644 --- a/tests/factory_sort_tac.v +++ b/tests/hb_pack.v @@ -111,4 +111,15 @@ pose X := Foo.pack T (HasFoo.Build A P T H). Check X : Foo.type A P. Abort. -End test2. \ No newline at end of file +End test2. + +HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }. +HB.structure Definition Fun T := { F of isID T F }. + +Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True. +intros f p. +pose F := isID.Build nat f p. +pose T : Fun nat := HB.pack nat f F. +Check T : Fun.type nat. +Abort. + From 7f0954c2bcf46372f1451d2cd2223b46dcab9997 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 14:49:35 +0200 Subject: [PATCH 42/60] changelog --- Changelog.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Changelog.md b/Changelog.md index f855db3b6..927d2675e 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,10 @@ # Changelog +## UNRELEASED + +- **Fix** HB.pack works with structures about functions, and not just + types + ## [1.3.0] - 2022-07-27 Compatible with From 779471385438805b80f30444f0f9b8d44221eddb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 15:01:19 +0200 Subject: [PATCH 43/60] fix test --- tests/hb_pack.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/hb_pack.v b/tests/hb_pack.v index 4fb1ab282..a73618ad1 100644 --- a/tests/hb_pack.v +++ b/tests/hb_pack.v @@ -119,7 +119,7 @@ HB.structure Definition Fun T := { F of isID T F }. Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True. intros f p. pose F := isID.Build nat f p. -pose T : Fun nat := HB.pack nat f F. +pose T : Fun.type nat := HB.pack f F. Check T : Fun.type nat. Abort. From cfd9133a3d12ab8872f7b2d274e8ee70491a6181 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 15:28:52 +0200 Subject: [PATCH 44/60] fix loc printing --- HB/common/log.elpi | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 2c3be8db9..01979cfb5 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -266,8 +266,8 @@ pred log.private.log-tactic i:term. with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !, get-option "elpi.loc" Loc, - loc.fields Loc FILE _ _ _ _, - std.any->string Loc LocStr, + loc.fields Loc FILE Start Stop _ _, + LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop}, FILENAME is FILE ^ ".hb", open_append FILENAME OC1, std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1, From 6daca05efb914e61322608dd828a8b437042e418 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 16:49:33 +0200 Subject: [PATCH 45/60] fix param printing --- HB/common/log.elpi | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 01979cfb5..a6e28ee96 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -446,8 +446,8 @@ coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :- pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp. coq.vernac->ppinductiveparams [] []. coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :- - PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest], - decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY, + PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest], + coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY, if2 (Imp = explicit) (A = "(", B = ")") (Imp = maximal) (A = "{", B = "}") (A = "[", B = "]"), From 44f0623b439c0692d947a9e0c07c35526b0e915a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 17:26:54 +0200 Subject: [PATCH 46/60] quick fix for reversible coercions --- HB/common/log.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HB/common/log.elpi b/HB/common/log.elpi index a6e28ee96..6141af0c5 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -361,7 +361,7 @@ coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notati coq.vernac->ppabbrterm NParams Term StrParams B. coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :- local->locality Local Locality. -coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :- +coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :- coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC}, if2 (TGT = sortclass) (T = "Sortclass") (TGT = funclass) (T = "Funclass") From 99b6435f90e386290ff9b72fe2518330639fa82e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 27 Aug 2022 22:08:38 +0200 Subject: [PATCH 47/60] fix for pp HB.pack --- HB/common/log.elpi | 2 +- tests/hb_pack.v | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 6141af0c5..0e95e073c 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -295,7 +295,7 @@ log.private.log-vernac _. log.private.log-tactic P :- log.private.logger L Nice, !, if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]), - log.private.logger-extend L {PPALL => coq.term->pp P}. + log.private.logger-extend L {PPALL => @holes! => coq.term->pp P}. log.private.log-tactic _. % The main entry point to print vernacular commands is coq.vernac->pp diff --git a/tests/hb_pack.v b/tests/hb_pack.v index a73618ad1..67b32cc0b 100644 --- a/tests/hb_pack.v +++ b/tests/hb_pack.v @@ -25,7 +25,7 @@ About hasA'.type. Section test. Variables (G : Prop) (P : AB.type -> G). - +(* problem with planB Goal forall T (a b : T), G. Proof. move=> T a b. @@ -35,7 +35,7 @@ pose Tab := hasB.Build A (b,b). pose AB : AB.type := ltac:(elpi HB.pack (A) (Tab)). exact: P AB. Qed. - +*) Goal forall T (a b : T), G. Proof. move=> T a b. From 79c4bbad9bb1e6b5e5dda58000533c10527ef88b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 27 Aug 2022 20:44:23 +0200 Subject: [PATCH 48/60] Support grefclass --- HB/common/phant-abbreviation.elpi | 20 ++++++++++++++++++-- HB/common/synthesis.elpi | 3 +-- _CoqProject.test-suite | 1 + tests/grefclass.v | 12 ++++++++++++ 4 files changed, 32 insertions(+), 4 deletions(-) create mode 100644 tests/grefclass.v diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi index b7f68148c..943c30c74 100644 --- a/HB/common/phant-abbreviation.elpi +++ b/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 => _ diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 1b98811cc..f194be009 100644 --- a/HB/common/synthesis.elpi +++ b/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 :- !. diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 5751ac2ea..98c20167e 100644 --- a/_CoqProject.test-suite +++ b/_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 diff --git a/tests/grefclass.v b/tests/grefclass.v new file mode 100644 index 000000000..c814aa584 --- /dev/null +++ b/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. From ad8d9819b64b500b5b06492039ee5e7af08cc953 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 31 Aug 2022 10:22:16 +0200 Subject: [PATCH 49/60] Typo in URL --- HB/instance.elpi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HB/instance.elpi b/HB/instance.elpi index 2d2bb073b..0b793248c 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -370,7 +370,7 @@ check-non-forgetful-inheritance T Factory :- std.do! [ "We strongly advise you encapsulate this instance inside a module," "in order to isolate it from the rest of the code, and to be able" "to import it on demand. See the above paper and the file" - "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non-forgetful-inheritance.v" + "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v" "to witness devastating effects." ) true ]. From f9984cc06068ec882925623cffd2c6da7ebe9a86 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 16 Sep 2022 09:37:38 +0200 Subject: [PATCH 50/60] Update Changelog.md --- Changelog.md | 1 + 1 file changed, 1 insertion(+) diff --git a/Changelog.md b/Changelog.md index 927d2675e..82eb42aa1 100644 --- a/Changelog.md +++ b/Changelog.md @@ -4,6 +4,7 @@ - **Fix** HB.pack works with structures about functions, and not just types +- **New** Command HB.howto to find all possible ways to instanciate structures. ## [1.3.0] - 2022-07-27 From b0da12f45e683e0ecfce1e17a01cc183d16c6fe1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Sep 2022 14:09:07 +0200 Subject: [PATCH 51/60] Update README.md --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 8e158441b..7db7c8dd8 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,8 @@ Proof. by rewrite example. Qed. This [paper](https://hal.inria.fr/hal-02478907) describes the language in details, and the corresponding talk [is available on youtube](https://www.youtube.com/watch?v=F6iRaTlQrlo). The [wiki](https://github.com/math-comp/hierarchy-builder/wiki) gathers some -tricks and FAQs. +tricks and FAQs. If you want to work on the implementation of HB, this +[recorded hacking session](https://www.youtube.com/watch?v=gmaJjCbzqO0) may be relevant to you. ### Installation & availability From edcb74abe84214badc54e16e9b7ead08789be37d Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Mon, 26 Sep 2022 18:06:01 +0200 Subject: [PATCH 52/60] Update Changelog.md Co-authored-by: Enrico Tassi --- Changelog.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index 82eb42aa1..9484e2080 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,9 +2,17 @@ ## UNRELEASED -- **Fix** HB.pack works with structures about functions, and not just - types -- **New** Command HB.howto to find all possible ways to instanciate structures. +## [1.4.0] - 2022-09-28 + +Compatible with +- Coq 8.15 with Coq-Elpi 1.14.x +- Coq 8.16 with Coq-Elpi 1.15.x and 1.16.x +- +- **Fix** `HB.pack` works with structures about functions, and not just types. +- **Fix** `HB.about` and `HB.graph` now display shortest names. +- **New** Command `HB.howto` to find all possible ways to instanciate structures. +- **New** Structures now support keys which type's head is a global reference. + (Only keys corresponding to the coercion classes `Sortclass` and `Funclass` were accepted). ## [1.3.0] - 2022-07-27 From 8310bdab3e7832c29780a25795e9b824f668927e Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 28 Sep 2022 15:34:39 +0200 Subject: [PATCH 53/60] Update nix & opam --- .github/workflows/nix-action-coq-8.15.yml | 71 ++- .github/workflows/nix-action-coq-8.16.yml | 61 +- .../workflows/nix-action-coq-mcHB-8.16.yml | 567 +++++++++++++++++- .nix/coq-nix-toolbox.nix | 2 +- coq-hierarchy-builder-shim.opam | 2 +- coq-hierarchy-builder.opam | 2 +- 6 files changed, 643 insertions(+), 62 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.15.yml b/.github/workflows/nix-action-coq-8.15.yml index c02f572e4..af72e4639 100644 --- a/.github/workflows/nix-action-coq-8.15.yml +++ b/.github/workflows/nix-action-coq-8.15.yml @@ -141,6 +141,7 @@ jobs: mathcomp-analysis: needs: - coq + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -176,18 +177,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" - --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" @@ -196,6 +189,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-real-closed' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "mathcomp-classical" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" @@ -204,6 +201,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-analysis" + mathcomp-classical: + needs: + - coq + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.15\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" + --argstr job "mathcomp-classical" mathcomp-single: needs: - coq diff --git a/.github/workflows/nix-action-coq-8.16.yml b/.github/workflows/nix-action-coq-8.16.yml index a224c784c..8aadff070 100644 --- a/.github/workflows/nix-action-coq-8.16.yml +++ b/.github/workflows/nix-action-coq-8.16.yml @@ -35,9 +35,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "coq" - coq-elpi: + graph-theory: needs: - coq + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,23 +64,34 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target graph-theory run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.16\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.16\" --argstr job \"graph-theory\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "coq-elpi" + --argstr job "graph-theory" hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -122,10 +134,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "hierarchy-builder" - mathcomp-analysis: + mathcomp: needs: - coq - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -151,11 +162,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.16\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.16\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" @@ -165,29 +176,32 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: mathcomp-fingroup' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-field" + --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' + name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-real-closed" + --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "hierarchy-builder" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" + --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-analysis" + --argstr job "mathcomp" mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -238,7 +252,6 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: diff --git a/.github/workflows/nix-action-coq-mcHB-8.16.yml b/.github/workflows/nix-action-coq-mcHB-8.16.yml index bfeab5dd5..8ce64fc4e 100644 --- a/.github/workflows/nix-action-coq-mcHB-8.16.yml +++ b/.github/workflows/nix-action-coq-mcHB-8.16.yml @@ -1,4 +1,218 @@ jobs: + QuickChick: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "QuickChick" + Verdi: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target Verdi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"Verdi\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: Cheerios' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "Cheerios" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: InfSeqExt' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "InfSeqExt" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "Verdi" + addition-chains: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target addition-chains + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"addition-chains\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "addition-chains" + autosubst: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target autosubst + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"autosubst\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest @@ -35,9 +249,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "coq" - coq-elpi: + coq-bits: needs: - coq + - mathcomp-algebra runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,19 +278,115 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target coq-bits run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-bits\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ \ | grep \"built:\" | sed \"s/.*/built/\")\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "coq-elpi" + --argstr job "coq-bits" + coquelicot: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coquelicot + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coquelicot" + deriving: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target deriving + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"deriving\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "deriving" fourcolor: needs: - coq @@ -135,7 +446,6 @@ jobs: hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -181,7 +491,6 @@ jobs: hierarchy-builder-shim: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -224,6 +533,70 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "hierarchy-builder-shim" + interval: + needs: + - coq + - coquelicot + - mathcomp-ssreflect + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target interval + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"interval\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "flocq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "interval" mathcomp: needs: - coq @@ -233,7 +606,6 @@ jobs: - mathcomp-solvable - mathcomp-field - mathcomp-character - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -310,7 +682,6 @@ jobs: - coq - mathcomp-ssreflect - mathcomp-fingroup - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -369,9 +740,9 @@ jobs: mathcomp-analysis: needs: - coq - - mathcomp-ssreflect - mathcomp-field - - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -407,18 +778,18 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-classical" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" @@ -427,6 +798,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-bigenough" mathcomp-character: needs: - coq @@ -435,7 +852,6 @@ jobs: - mathcomp-algebra - mathcomp-solvable - mathcomp-field - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -503,6 +919,67 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-character" + mathcomp-classical: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-finmap + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-classical" mathcomp-field: needs: - coq @@ -510,7 +987,6 @@ jobs: - mathcomp-fingroup - mathcomp-algebra - mathcomp-solvable - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -578,7 +1054,6 @@ jobs: needs: - coq - mathcomp-ssreflect - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -679,9 +1154,7 @@ jobs: mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -740,9 +1213,7 @@ jobs: mathcomp-single-planB: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder-shim runs-on: ubuntu-latest steps: @@ -801,9 +1272,7 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -865,7 +1334,6 @@ jobs: - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -928,7 +1396,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1052,6 +1519,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "odd-order" + reglang: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target reglang + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"reglang\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "reglang" name: Nix CI for bundle coq-mcHB-8.16 'on': pull_request: diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index fddb4f818..2e80cf19b 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"a2aa6afce9ebfea39501cdf43a3a3bd08e557a26" +"4f0eb194b37b6e0db28be2eb4643bd6924abf7ab" diff --git a/coq-hierarchy-builder-shim.opam b/coq-hierarchy-builder-shim.opam index 9a190e591..6f44b2a7f 100644 --- a/coq-hierarchy-builder-shim.opam +++ b/coq-hierarchy-builder-shim.opam @@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make "-C" "shim" "build" ] install: [ make "-C" "shim" "install" ] conflicts: [ "coq-hierarchy-builder" ] -depends: [ "coq" {>= "8.10"} ] +depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ] synopsis: "Shim package for HB" description: """ This package provide the support constants one can use to compile files diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 70a22128b..694aac2af 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -12,7 +12,7 @@ build: [ [ make "build"] [ make "test-suite" ] {with-test} ] install: [ make "install" ] -depends: [ "coq-elpi" { (>= "1.15.1" & < "1.16~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.15.1" & < "1.17~") | = "dev" } ] conflicts: [ "coq-hierarchy-builder-shim" ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """ From 148ec1ac871afe837fe0bbdcdfcbfed0d04b63ab Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Thu, 29 Sep 2022 09:12:08 +0200 Subject: [PATCH 54/60] Update Changelog.md --- Changelog.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index 9484e2080..3442ef9db 100644 --- a/Changelog.md +++ b/Changelog.md @@ -2,7 +2,7 @@ ## UNRELEASED -## [1.4.0] - 2022-09-28 +## [1.4.0] - 2022-09-29 Compatible with - Coq 8.15 with Coq-Elpi 1.14.x From 9d8524761c35e88bc7b1238d997c09ecd2ef3fc6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Nov 2022 18:00:25 +0100 Subject: [PATCH 55/60] Update Changelog.md --- Changelog.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index 3442ef9db..c69398bd5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,7 +7,9 @@ Compatible with - Coq 8.15 with Coq-Elpi 1.14.x - Coq 8.16 with Coq-Elpi 1.15.x and 1.16.x -- + +### General + - **Fix** `HB.pack` works with structures about functions, and not just types. - **Fix** `HB.about` and `HB.graph` now display shortest names. - **New** Command `HB.howto` to find all possible ways to instanciate structures. From bea2350f655c115dce902df58d920e5fc9bc8beb Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 14 Dec 2022 12:53:57 +0100 Subject: [PATCH 56/60] remove a wrong quote character --- structures.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/structures.v b/structures.v index 8dcb68a88..30c9015f4 100644 --- a/structures.v +++ b/structures.v @@ -577,7 +577,7 @@ HB.structure Definition StructureName params := - [#[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 it's [pT] by unification (using canonical structure inference), + 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 From e477707d660a921f11536be51033287a8ca1766e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 9 Apr 2023 19:10:39 +0200 Subject: [PATCH 57/60] Fix a universe issue with rev_coerce --- HB/common/log.elpi | 3 +++ tests/rev_coerce.v | 24 ++++++++++++++++++++++++ 2 files changed, 27 insertions(+) create mode 100644 tests/rev_coerce.v diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 0e95e073c..2518b0db5 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -35,6 +35,7 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [ ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, avoid-name-collision Name Name1, + coq.typecheck Bo Ty _, coq.env.add-const Name1 Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), @@ -49,6 +50,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [ ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, avoid-name-collision Name Name1, + coq.typecheck Bo Ty _, coq.env.add-const Name1 Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), @@ -61,6 +63,7 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [ (coq.error "HB: cannot infer some information in" Name ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, + coq.typecheck Bo Ty _, coq.env.add-const Name Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), diff --git a/tests/rev_coerce.v b/tests/rev_coerce.v new file mode 100644 index 000000000..543bce5b2 --- /dev/null +++ b/tests/rev_coerce.v @@ -0,0 +1,24 @@ +From HB Require Import structures. + +HB.mixin Record isPointed V := { point : V }. +HB.structure Definition Pointed := {V of isPointed V}. + +Definition popt (U : Pointed.type) := option U. +HB.instance Definition _ U := isPointed.Build (popt U) None. + +HB.mixin Record hasTrue (U V : Pointed.type) (f : U -> V) := { + true_subproof : True +}. +HB.structure Definition HasTrue (U V : Pointed.type) := {f of hasTrue U V f}. + +Definition poptp (U : Pointed.type) (p : popt U) : U := point. + +Section Bug. +Variable U : Pointed.type. + +Check hasTrue.Build (popt U) U (@poptp U) I. +Set Printing Universes. +(* There used to be a universe issue at the line below: *) +HB.instance Definition _ := hasTrue.Build (popt U) U (@poptp U) I. + +End Bug. From 1b7b10b9a08f085e5b0c860c37a2054ed889d118 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 19 Apr 2023 00:37:16 +0200 Subject: [PATCH 58/60] fix nix-shell --- .nix/config.nix | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.nix/config.nix b/.nix/config.nix index bd392b3cb..693054c5a 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,7 +1,7 @@ { format = "1.0.0"; attribute = "hierarchy-builder"; - default-bundle = "coq-8.15"; + default-bundle = "coq-rev_coerce"; bundles = let mcHBcommon = { mathcomp.override.version = "hierarchy-builder"; @@ -33,6 +33,10 @@ "coq-8.15".coqPackages = { coq.override.version = "8.15"; }; + "coq-rev_coerce".coqPackages = { + coq.override.version = "proux01:rev_coerce"; + coq-elpi.override.version = "coq-master"; + }; }; cachix.coq = {}; cachix.coq-community = {}; From aaaecd4a773ba3969ab3b1e3bec8c929e1a9452f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 19 Apr 2023 00:51:13 +0200 Subject: [PATCH 59/60] anomaly --- examples/cat/cat.v | 514 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 399 insertions(+), 115 deletions(-) diff --git a/examples/cat/cat.v b/examples/cat/cat.v index 1dd1f755d..b8601449e 100644 --- a/examples/cat/cat.v +++ b/examples/cat/cat.v @@ -6,6 +6,10 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Add Search Blacklist "__canonical__". +Declare Scope algebra_scope. +Delimit Scope algebra_scope with A. +Local Open Scope algebra_scope. + Declare Scope cat_scope. Delimit Scope cat_scope with cat. Local Open Scope cat_scope. @@ -18,18 +22,21 @@ Axiom Prop_irrelevance : forall (P : Prop) (x y : P), x = y. Definition U := Type. Identity Coercion U_to_type : U >-> Sortclass. -HB.mixin Record HasHom C := { hom : C -> C -> U }. +HB.mixin Record IsQuiver C := { hom : C -> C -> U }. Unset Universe Checking. -HB.structure Definition Hom : Set := { C of HasHom C }. +HB.structure Definition Quiver : Set := { C of IsQuiver C }. Set Universe Checking. -Notation homType := Hom.type. -Bind Scope cat_scope with Hom.type. +Notation quiver := Quiver.type. +Bind Scope cat_scope with Quiver.type. Bind Scope cat_scope with hom. Arguments hom {C} : rename. +Notation homs T := (hom (_ : T) (_ : T)). +Notation "C ~> D :> T" := (hom (C : T) (D : T)) + (at level 99, D, T at level 200, format "C ~> D :> T", only parsing) : cat_scope. Notation "a ~> b" := (hom a b) (at level 99, b at level 200, format "a ~> b") : cat_scope. -HB.mixin Record Hom_IsPreCat C of Hom C := { +HB.mixin Record Quiver_IsPreCat C of Quiver C := { idmap : forall (a : C), a ~> a; comp : forall (a b c : C), (a ~> b) -> (b ~> c) -> (a ~> c); }. @@ -40,8 +47,8 @@ HB.factory Record IsPreCat C := { comp : forall (a b c : C), hom a b -> hom b c -> hom a c; }. HB.builders Context C of IsPreCat C. - HB.instance Definition _ := HasHom.Build C hom. - HB.instance Definition _ := Hom_IsPreCat.Build C idmap comp. + HB.instance Definition _ := IsQuiver.Build C hom. + HB.instance Definition _ := Quiver_IsPreCat.Build C idmap comp. HB.end. Unset Universe Checking. @@ -53,6 +60,8 @@ Arguments idmap {C} {a} : rename. Arguments comp {C} {a b c} : rename. Notation "f \o g" := (comp g f) : cat_scope. +Notation "f \; g :> T" := (@comp T _ _ _ f g) + (at level 60, g, T at level 60, format "f \; g :> T", only parsing) : cat_scope. Notation "f \; g" := (comp f g) : cat_scope. Notation "\idmap_ a" := (@idmap _ a) (only parsing, at level 0) : cat_scope. @@ -95,30 +104,26 @@ Proof. by []. Qed. Lemma U1x (X : U) x : \idmap_X x = x. Proof. by []. Qed. -HB.mixin Record IsPreFunctor (C D : Hom.type) (F : C -> D) := { - Fhom_of : forall (a b : C), (a ~> b) -> (F a ~> F b) +HB.mixin Record IsPreFunctor (C D : Quiver.type) (F : C -> D) := { + Fhom : forall (a b : C), (a ~> b) -> (F a ~> F b) }. Unset Universe Checking. -HB.structure Definition PreFunctor (C D : Hom.type) : Set := +HB.structure Definition PreFunctor (C D : Quiver.type) : Set := { F of IsPreFunctor C D F }. Set Universe Checking. -HB.instance Definition _ := HasHom.Build Hom.type PreFunctor.type. -Arguments Fhom_of /. +HB.instance Definition _ := IsQuiver.Build Quiver.type PreFunctor.type. -Definition Fhom_phant (C D : Hom.type) (F : C ~> D) - of phantom (_ -> _) F := @Fhom_of C D F. -Notation "F ^$" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _) +Notation "F ^$" := (@Fhom _ _ F _ _) (at level 1, format "F ^$") : cat_scope. -Notation "F <$> f" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _ f) +Notation "F <$> f" := (@Fhom _ _ F _ _ f) (at level 58, format "F <$> f", right associativity) : cat_scope. -Lemma prefunctorP (C D : homType) (F G : C ~> D) (eqFG : F =1 G) : +Lemma prefunctorP (C D : quiver) (F G : C ~> D) (eqFG : F =1 G) : let homF a b F := F a ~> F b in (forall a b f, eq_rect _ (homF a b) (F <$> f) _ (funext eqFG) = G <$> f) -> F = G. Proof. -rewrite !/Fhom_phant/=. move: F G => [F [[/= Fhom]]] [G [[/= Ghom]]] in eqFG *. case: _ / (funext eqFG) => /= in Ghom * => eqFGhom. congr PreFunctor.Pack; congr PreFunctor.Class; congr IsPreFunctor.Axioms_. @@ -135,8 +140,8 @@ Unset Universe Checking. HB.structure Definition Functor (C D : precat) : Set := { F of IsPreFunctor C D F & PreFunctor_IsFunctor C D F }. Set Universe Checking. -HB.instance Definition _ := HasHom.Build precat Functor.type. -HB.instance Definition _ := HasHom.Build cat Functor.type. +HB.instance Definition _ := IsQuiver.Build precat Functor.type. +HB.instance Definition _ := IsQuiver.Build cat Functor.type. Lemma functorP (C D : precat) (F G : C ~> D) (eqFG : F =1 G) : let homF a b F := F a ~> F b in @@ -158,11 +163,11 @@ HB.instance Definition _ (C : precat) := PreFunctor_IsFunctor.Build C C idfun (fun=> erefl) (fun _ _ _ _ _ => erefl). Section comp_prefunctor. -Context {C D E : homType} {F : C ~> D} {G : D ~> E}. +Context {C D E : quiver} {F : C ~> D} {G : D ~> E}. HB.instance Definition _ := IsPreFunctor.Build C E (G \o F)%FUN (fun a b f => G^$ (F^$ f)). -Lemma comp_Fun (a b : C) (f : a ~> b) : (G \o F)%FUN^$ f = G^$ (F^$ f). +Lemma comp_Fun (a b : C) (f : a ~> b) : (G \o F)%FUN <$> f = G <$> (F <$> f). Proof. by []. Qed. End comp_prefunctor. @@ -177,12 +182,10 @@ HB.instance Definition _ := PreFunctor_IsFunctor.Build C E (G \o F)%FUN comp_F1 comp_Fcomp. End comp_functor. -HB.instance Definition _ := Hom_IsPreCat.Build precat - (fun C => [the C ~> C of idfun]) - (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]). -HB.instance Definition _ := Hom_IsPreCat.Build cat - (fun C => [the C ~> C of idfun]) - (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]). +HB.instance Definition _ := Quiver_IsPreCat.Build precat + (fun=> idfun) (fun C D E (F : C ~> D) (G : D ~> E) => (G \o F)%FUN). +HB.instance Definition _ := Quiver_IsPreCat.Build cat + (fun=> idfun) (fun C D E (F : C ~> D) (G : D ~> E) => (G \o F)%FUN). Lemma funext_frefl A B (f : A -> B) : funext (frefl f) = erefl. Proof. exact: Prop_irrelevance. Qed. @@ -200,60 +203,62 @@ by split=> [C D F|C D F|C D C' D' F G H]; Qed. HB.instance Definition _ := cat_cat. -HB.mixin Record Hom_IsPreConcrete T of Hom T := { +HB.mixin Record Quiver_IsPreConcrete T of Quiver T := { concrete : T -> U; concrete_fun : forall (a b : T), (a ~> b) -> (concrete a) -> (concrete b); + (* concrete_fun_inj : forall a b, injective (concrete_fun a b) *) }. Unset Universe Checking. -HB.structure Definition PreConcreteHom : Set := - { C of Hom_IsPreConcrete C & HasHom C }. +HB.structure Definition PreConcreteQuiver : Set := + { C of Quiver_IsPreConcrete C & IsQuiver C }. Set Universe Checking. -Coercion concrete : PreConcreteHom.sort >-> U. +Coercion concrete : PreConcreteQuiver.sort >-> U. -HB.mixin Record PreConcrete_IsConcrete T of PreConcreteHom T := { +HB.mixin Record PreConcrete_IsConcrete T of PreConcreteQuiver T := { concrete_fun_inj : forall (a b : T), injective (concrete_fun a b) }. Unset Universe Checking. -HB.structure Definition ConcreteHom : Set := - { C of PreConcreteHom C & PreConcrete_IsConcrete C }. +HB.structure Definition ConcreteQuiver : Set := + { C of PreConcreteQuiver C & PreConcrete_IsConcrete C }. Set Universe Checking. -HB.instance Definition _ (C : ConcreteHom.type) := +HB.instance Definition _ (C : ConcreteQuiver.type) := IsPreFunctor.Build _ _ (concrete : C -> U) concrete_fun. -HB.mixin Record PreCat_IsConcrete T of ConcreteHom T & PreCat T := { +HB.mixin Record PreCat_IsConcrete T of ConcreteQuiver T & PreCat T := { concrete1 : forall (a : T), concrete <$> \idmap_a = idfun; concrete_comp : forall (a b c : T) (f : a ~> b) (g : b ~> c), concrete <$> (f \; g) = ((concrete <$> g) \o (concrete <$> f))%FUN; }. Unset Universe Checking. HB.structure Definition ConcretePreCat : Set := - { C of PreCat C & ConcreteHom C & PreCat_IsConcrete C }. + { C of PreCat C & ConcreteQuiver C & PreCat_IsConcrete C }. HB.structure Definition ConcreteCat : Set := - { C of Cat C & ConcreteHom C & PreCat_IsConcrete C }. + { C of Cat C & ConcreteQuiver C & PreCat_IsConcrete C }. Set Universe Checking. +(* Anomaly *) HB.instance Definition _ (C : ConcretePreCat.type) := - PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _). + PreFunctor_IsFunctor.Build C U concrete (@concrete1 _) (@concrete_comp _). HB.instance Definition _ (C : ConcreteCat.type) := - PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _). + PreFunctor_IsFunctor.Build C U concrete (@concrete1 _) (@concrete_comp _). -HB.instance Definition _ := Hom_IsPreConcrete.Build U (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build U (fun _ _ => id). HB.instance Definition _ := PreConcrete_IsConcrete.Build U (fun _ _ _ _ => id). HB.instance Definition _ := PreCat_IsConcrete.Build U (fun=> erefl) (fun _ _ _ _ _ => erefl). Unset Universe Checking. -HB.instance Definition _ := Hom_IsPreConcrete.Build homType (fun _ _ => id). -HB.instance Definition _ := Hom_IsPreConcrete.Build precat (fun _ _ => id). -HB.instance Definition _ := Hom_IsPreConcrete.Build cat (fun _ _ => id). -Lemma homType_concrete_subproof : PreConcrete_IsConcrete homType. +HB.instance Definition _ := Quiver_IsPreConcrete.Build quiver (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build precat (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build cat (fun _ _ => id). +Lemma quiver_concrete_subproof : PreConcrete_IsConcrete quiver. Proof. constructor=> C D F G FG; apply: prefunctorP. by move=> x; congr (_ x); apply: FG. by move=> *; apply: Prop_irrelevance. Qed. -HB.instance Definition _ := homType_concrete_subproof. +HB.instance Definition _ := quiver_concrete_subproof. Lemma precat_concrete_subproof : PreConcrete_IsConcrete precat. Proof. @@ -276,7 +281,7 @@ HB.instance Definition _ := PreCat_IsConcrete.Build cat (fun=> erefl) (fun _ _ _ _ _ => erefl). Set Universe Checking. -Definition cst (C D : homType) (c : C) := fun of D => c. +Definition cst (C D : quiver) (c : C) := fun of D => c. Arguments cst {C} D c. HB.instance Definition _ {C D : precat} (c : C) := IsPreFunctor.Build D C (cst D c) (fun _ _ _ => idmap). @@ -285,14 +290,13 @@ HB.instance Definition _ {C D : cat} (c : C) := (fun _ _ _ _ _ => esym (compo1 idmap)). Definition catop (C : Type) : Type := C. -HB.instance Definition _ (C : homType) := HasHom.Build (catop C) (fun a b => hom b a). -HB.instance Definition _ (C : precat) := Hom_IsPreCat.Build (catop C) (fun=> idmap) +Notation "C ^op" := (catop C) (at level 10, format "C ^op") : cat_scope. +HB.instance Definition _ (C : quiver) := IsQuiver.Build (C^op) (fun a b => hom b a). +HB.instance Definition _ (C : precat) := Quiver_IsPreCat.Build (C^op) (fun=> idmap) (fun _ _ _ f g => g \; f). -HB.instance Definition _ (C : cat) := PreCat_IsCat.Build (catop C) +HB.instance Definition _ (C : cat) := PreCat_IsCat.Build (C^op) (fun _ _ _ => compo1 _) (fun _ _ _ => comp1o _) (fun _ _ _ _ _ _ _ => esym (compoA _ _ _)). -Notation "C ^op" := (catop C) (at level 10, format "C ^op") : cat_scope. - HB.instance Definition _ {C : precat} {c : C} := IsPreFunctor.Build C _ (hom c) (fun a b f g => g \; f). @@ -301,24 +305,19 @@ Lemma hom_Fhom_subproof (C : cat) (x : C) : Proof. by split=> *; apply/funext => h; [apply: compo1 | apply: compoA]. Qed. HB.instance Definition _ {C : cat} {c : C} := hom_Fhom_subproof c. -Lemma hom_op {C : homType} (c : C^op) : hom c = (@hom C)^~ c. +Lemma hom_op {C : quiver} (c : C^op) : hom c = (@hom C)^~ c. Proof. reflexivity. Qed. Lemma homFhomx {C : precat} (a b c : C) (f : a ~> b) (g : c ~> a) : (hom c <$> f) g = g \; f. Proof. by []. Qed. -Notation "C ~> D :> T" := ([the T of C] ~> [the T of D]) - (at level 99, D, T at level 200, format "C ~> D :> T"). -Notation "C :~>: D :> T" := ([the T of C : Type] ~> [the T of D : Type]) - (at level 99, D, T at level 200, format "C :~>: D :> T"). - Definition dprod {I : Type} (C : I -> Type) := forall i, C i. Section hom_dprod. -Context {I : Type} (C : I -> Hom.type). +Context {I : Type} (C : I -> Quiver.type). Definition dprod_hom_subdef (a b : dprod C) := forall i, a i ~> b i. -HB.instance Definition _ := HasHom.Build (dprod C) dprod_hom_subdef. +HB.instance Definition _ := IsQuiver.Build (dprod C) dprod_hom_subdef. End hom_dprod. Arguments dprod_hom_subdef /. @@ -345,14 +344,14 @@ HB.instance Definition _ := dprod_is_cat. End cat_dprod. Section hom_prod. -Context {C D : Hom.type}. +Context {C D : Quiver.type}. Definition prod_hom_subdef (a b : C * D) := ((a.1 ~> b.1) * (a.2 ~> b.2))%type. -HB.instance Definition _ := HasHom.Build (C * D)%type prod_hom_subdef. +HB.instance Definition _ := IsQuiver.Build (C * D)%type prod_hom_subdef. End hom_prod. Section precat_prod. Context {C D : precat}. -HB.instance Definition _ := IsPreCat.Build (C * D)%type (fun _ => (idmap, idmap)) +HB.instance Definition _ := IsPreCat.Build (C * D)%type (fun=> (idmap, idmap)) (fun a b c (f : a ~> b) (g : b ~> c) => (f.1 \; g.1, f.2 \; g.2)). End precat_prod. @@ -368,23 +367,22 @@ Qed. HB.instance Definition _ := prod_is_cat. End cat_prod. -HB.mixin Record IsNatural (C D : precat) (F G : C :~>: D :> homType) +HB.mixin Record IsNatural (C D : precat) (F G : C ~> D :> quiver) (n : forall c, F c ~> G c) := { natural : forall (a b : C) (f : a ~> b), F <$> f \; n b = n a \; G <$> f }. Unset Universe Checking. -HB.structure Definition Natural (C D : precat) - (F G : C :~>: D :> homType) : Set := +HB.structure Definition Natural (C D : precat) (F G : C ~> D :> quiver) : Set := { n of @IsNatural C D F G n }. Set Universe Checking. HB.instance Definition _ (C D : precat) := - HasHom.Build (PreFunctor.type C D) (@Natural.type C D). + IsQuiver.Build (C ~> D) (@Natural.type C D). HB.instance Definition _ (C D : precat) := - HasHom.Build (Functor.type C D) (@Natural.type C D). + IsQuiver.Build (C ~> D) (@Natural.type C D). Arguments natural {C D F G} n [a b] f : rename. Lemma naturalx (C : precat) (D : ConcretePreCat.type) - (F G : C :~>: D :> homType) (n : F ~> G) (a b : C) (f : a ~> b) g : + (F G : C ~> D :> quiver) (n : F ~> G) (a b : C) (f : a ~> b) g : (concrete <$> n b) ((concrete <$> F <$> f) g) = (concrete <$> G <$> f) ((concrete <$> n a) g). Proof. @@ -393,11 +391,11 @@ by rewrite !Fcomp. Qed. Arguments naturalx {C D F G} n [a b] f. -Lemma naturalU (C : precat) (F G : C :~>: U :> homType) (n : F ~> G) +Lemma naturalU (C : precat) (F G : C ~> U :> quiver) (n : F ~> G) (a b : C) (f : a ~> b) g : n b (F^$ f g) = G^$ f (n a g). Proof. exact: (naturalx n). Qed. -Lemma natP (C D : precat) (F G : C :~>: D :> homType) (n m : F ~> G) : +Lemma natP (C D : precat) (F G : C ~> D :> quiver) (n m : F ~> G) : Natural.sort n = Natural.sort m -> n = m. Proof. case: n m => [/= n nP] [/= m mP] enm. @@ -408,12 +406,116 @@ exact: Prop_irrelevance. Qed. Notation "F ~~> G" := - ((F : _ -> _) ~> (G : _ -> _) :> (_ :~>: _ :> homType)) + (F ~> G :> (homs quiver)) (at level 99, G at level 200, format "F ~~> G"). Notation "F ~~> G :> C ~> D" := - ((F : _ -> _) ~> (G : _ -> _) :> (C :~>: D :> homType)) + (F ~> G :> (C ~> D :> quiver)) (at level 99, G at level 200, C, D at level 0, format "F ~~> G :> C ~> D"). +Section nat_map_left. +Context {C D E : precat} {F G : C ~> D}. + +Definition nat_lmap (H : D ~> E :> quiver) (n : forall c, F c ~> G c) : + forall c, (H \o F)%FUN c ~> (H \o G)%FUN c := fun c => H <$> n c. +Lemma nat_lmap_is_natural (H : D ~> E) (n : F ~~> G) : + IsNatural C E (H \o F) (H \o G) (nat_lmap H n). +Proof. by constructor=> a b f; rewrite /nat_lmap/= -!Fcomp natural. Qed. +HB.instance Definition _ H n := nat_lmap_is_natural H n. +(* Definition nat_lmap_nat (H : D ~> E) (n : F ~~> G) : H \o F ~~> H \o G := nat_lmap H n. *) +End nat_map_left. + +Notation "F n" := (nat_lmap F n) + (at level 58, format "F n", right associativity) : cat_scope. + +Section nat_map_right. +Context {C D E : precat} {F G : C ~> D}. + +Definition nat_rmap (H : E -> C) (n : forall c, F c ~> G c) : + forall c, (F \o H)%FUN c ~> (G \o H)%FUN c := fun c => n (H c). +Lemma nat_rmap_is_natural (H : E ~> C :> quiver) (n : F ~~> G) : + IsNatural E D (F \o H)%FUN (G \o H)%FUN (nat_rmap H n). +Proof. by constructor=> a b f; rewrite /nat_lmap/= natural. Qed. +HB.instance Definition _ H n := nat_rmap_is_natural H n. + +End nat_map_right. + +Notation "F <$o> n" := (nat_rmap F n) + (at level 58, format "F <$o> n", right associativity) : cat_scope. + +HB.mixin Record IsMonad (C : precat) (M : C -> C) of @PreFunctor C C M := { + unit : idfun ~~> M; + join : (M \o M)%FUN ~~> M; + bind : forall (a b : C), (a ~> M b) -> (M a ~> M b); + bindE : forall a b (f : a ~> M b), bind a b f = M <$> f \; join b; + unit_join : forall a, (M <$> unit a) \; join _ = idmap; + join_unit : forall a, join _ \; (M <$> unit a) = idmap; + join_square : forall a, M <$> join a \; join _ = join _ \; join _ +}. + +HB.structure Definition PreMonad (C : precat) := + {M of @PreFunctor C C M & IsMonad C M}. +HB.structure Definition Monad (C : precat) := + {M of @Functor C C M & IsMonad C M}. + +HB.factory Record IsJoinMonad (C : precat) (M : C -> C) of @PreFunctor C C M := { + unit : idfun ~~> M; + join : (M \o M)%FUN ~~> M; + unit_join : forall a, (M <$> unit a) \; join _ = idmap; + join_unit : forall a, join _ \; (M <$> unit a) = idmap; + join_square : forall a, M <$> join a \; join _ = join _ \; join _ +}. +HB.builders Context C M of IsJoinMonad C M. + HB.instance Definition _ := IsMonad.Build C M + (fun a b f => erefl) unit_join join_unit join_square. +HB.end. + +HB.mixin Record IsCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := { + counit : M ~~> idfun; + cojoin : M ~~> (M \o M)%FUN; + cobind : forall (a b : C), (M a ~> b) -> (M a ~> M b); + cobindE : forall a b (f : M a ~> b), cobind a b f = cojoin _ \; M <$> f; + unit_cojoin : forall a, (M <$> counit a) \; cojoin _ = idmap; + join_counit : forall a, cojoin _ \; (M <$> counit a) = idmap; + cojoin_square : forall a, cojoin _ \; M <$> cojoin a = cojoin _ \; cojoin _ +}. +HB.structure Definition PreCoMonad (C : precat) := + {M of @PreFunctor C C M & IsCoMonad C M}. +HB.structure Definition CoMonad (C : precat) := + {M of @Functor C C M & IsCoMonad C M}. + +HB.factory Record IsJoinCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := { + counit : M ~~> idfun; + cojoin : M ~~> (M \o M)%FUN; + unit_cojoin : forall a, (M <$> counit a) \; cojoin _ = idmap; + join_counit : forall a, cojoin _ \; (M <$> counit a) = idmap; + cojoin_square : forall a, cojoin _ \; M <$> cojoin a = cojoin _ \; cojoin _ +}. +HB.builders Context C M of IsJoinCoMonad C M. + HB.instance Definition _ := IsCoMonad.Build C M + (fun a b f => erefl) unit_cojoin join_counit cojoin_square. +HB.end. + +HB.mixin Record IsRightAdjoint (D C : precat) (R : D -> C) + of @PreFunctor D C R := { + L_ : C ~> D; + phi : forall c d, (L_ c ~> d) -> (c ~> R d); + psy : forall c d, (c ~> R d) -> (L_ c ~> d); + phi_psy c d : (phi c d \o psy c d)%FUN = @id (c ~> R d); + psy_phi c d : (psy c d \o phi c d)%FUN = @id (L_ c ~> d) +}. +HB.structure Definition RightAdjoint (D C : precat) := + { R of @Functor D C R & IsRightAdjoint D C R }. +Arguments L_ {_ _}. +Arguments phi {D C s} {c d}. +Arguments psy {D C s} {c d}. + +Lemma idFmap (C : cat) (a b : C) (f : a ~> b) : idfun <$> f = f. +Proof. by []. Qed. + +Lemma compFmap (C D E : cat) (F : C ~> D) (G : D ~> E) (a b : C) (f : a ~> b) : + (G \o F) <$> f = G <$> F <$> f. +Proof. by []. Qed. + Section hom_repr. Context {C : cat} (F : C ~> U :> cat). @@ -421,20 +523,18 @@ Definition homF (c : C) : U := hom c ~~> F. Section nat. Context (x y : C) (xy : x ~> y) (n : hom x ~~> F). -Definition homFhom_subdef c : hom y c ~> F c := fun g => n _ (xy \; g). -Arguments homFhom_subdef / : clear implicits. +Definition homFhom c : hom y c ~> F c := fun g => n _ (xy \; g). -Lemma homFhom_natural_subdef : IsNatural _ _ _ _ homFhom_subdef. +Lemma homFhom_natural_subdef : IsNatural _ _ _ _ homFhom. Proof. -by split=> a b f /=; apply/funext => g /=; rewrite !Ucompx/= !naturalU/= Fcomp. +by split=> a b f /=; apply/funext => g /=; + rewrite /homFhom !Ucompx/= !naturalU/= Fcomp. Qed. HB.instance Definition _ := homFhom_natural_subdef. -Definition homFhom_subdef_nat : hom y ~~> F := [the _ ~~> _ of homFhom_subdef]. End nat. -Arguments homFhom_subdef / : clear implicits. - +Arguments homFhom / : clear implicits. -HB.instance Definition _ := IsPreFunctor.Build _ _ homF homFhom_subdef_nat. +HB.instance Definition _ := IsPreFunctor.Build _ _ homF homFhom. Lemma homF_functor_subproof : PreFunctor_IsFunctor _ _ homF. Proof. split=> [a|a b c f g]. @@ -452,22 +552,20 @@ Context (c : C). Definition hom_repr : homF c ~> F c := fun f => f _ idmap. Arguments hom_repr /. -Definition repr_hom (fc : F c) a : - [the C :~>: U :> homType of hom c] a ~> F a := fun f => F^$ f fc. +Definition repr_hom (fc : F c) a : hom c a ~> F a := fun f => F^$ f fc. Arguments repr_hom / : clear implicits. Lemma repr_hom_subdef (fc : F c) : IsNatural _ _ _ _ (repr_hom fc). Proof. by split=> a b f /=; apply/funext=> x; rewrite !Ucompx/= Fcomp. Qed. HB.instance Definition _ {fc : F c} := repr_hom_subdef fc. -Definition repr_hom_nat : F c ~> homF c := fun fc => - [the hom c ~~> F of repr_hom fc]. +Definition repr_hom_nat : F c ~> homF c := repr_hom. Lemma hom_reprK : cancel hom_repr repr_hom_nat. Proof. move=> f; apply/natP; apply/funext => a; apply/funext => g /=. by rewrite -naturalU/=; congr (f _ _); apply: comp1o. Qed. -Lemma repr_homK : cancel repr_hom_nat hom_repr. +Lemma repr_homK : cancel (repr_hom : F c ~> homF c) hom_repr. Proof. by move=> fc; rewrite /= F1. Qed. End pointed. Arguments hom_repr /. @@ -478,8 +576,8 @@ Proof. split=> a b f /=; apply/funext => n /=; rewrite !Ucompx/= compo1/=. by rewrite -naturalU/=; congr (n _ _); apply/esym/comp1o. Qed. - HB.instance Definition _ := hom_repr_natural_subproof. + Lemma hom_natural_repr_subproof : IsNatural _ _ _ _ repr_hom_nat. Proof. split=> a b f /=; apply: funext => fa /=; rewrite !Ucompx/=. @@ -488,8 +586,8 @@ by rewrite Fcomp Ucompx/=. Qed. HB.instance Definition _ := hom_natural_repr_subproof. -Definition hom_repr_nat := [the homF ~~> F of hom_repr]. -Definition repr_hom_nat_nat := [the F ~~> homF of repr_hom_nat]. +Definition hom_repr_nat : homF ~~> F := hom_repr. +Definition repr_hom_nat_nat : F ~~> homF := repr_hom_nat. End hom_repr. @@ -501,7 +599,7 @@ Definition type := { x : C * D & F x.1 ~> G x.2 }. Definition hom_subdef (a b : type) := { f : tag a ~> tag b & F^$ f.1 \; tagged b = tagged a \; G^$ f.2 }. -HB.instance Definition _ := HasHom.Build type hom_subdef. +HB.instance Definition _ := IsQuiver.Build type hom_subdef. End homcomma. Arguments hom_subdef /. Section comma. @@ -540,19 +638,19 @@ Notation "F `/ b" := (F `/` cst unit b) Notation "a / b" := (cst unit a `/ b) : cat_scope. HB.mixin Record PreCat_IsMonoidal C of PreCat C := { - one : C; + onec : C; prod : (C * C)%type ~> C :> precat ; }. HB.structure Definition PreMonoidal := { C of PreCat C & PreCat_IsMonoidal C }. Notation premonoidal := PreMonoidal.type. Arguments prod {C} : rename. Notation "a * b" := (prod (a, b)) : cat_scope. -Reserved Notation "f ** g" (at level 40, g at level 40, format "f ** g"). -Notation "f ** g" := (prod^$ (f, g)) (only printing) : cat_scope. -Notation "f ** g" := (prod^$ ((f, g) : (_, _) ~> (_, _))) (only parsing) : cat_scope. -Notation "1" := one. +Reserved Notation "f <*> g" (at level 40, g at level 40, format "f <*> g"). +Notation "f <*> g" := (prod^$ (f, g)) (only printing) : cat_scope. +Notation "f <*> g" := (prod^$ ((f, g) : (_, _) ~> (_, _))) (only parsing) : cat_scope. +Notation "1" := onec : cat_scope. -Definition hom_cast {C : homType} {a a' : C} (eqa : a = a') {b b' : C} (eqb : b = b') : +Definition hom_cast {C : quiver} {a a' : C} (eqa : a = a') {b b' : C} (eqb : b = b') : (a ~> b) -> (a' ~> b'). Proof. now elim: _ / eqa; elim: _ / eqb. Defined. @@ -560,57 +658,55 @@ Proof. now elim: _ / eqa; elim: _ / eqb. Defined. HB.mixin Record PreFunctor_IsMonoidal (C D : premonoidal) F of @PreFunctor C D F := { fun_one : F 1 = 1; fun_prod : forall (x y : C), F (x * y) = F x * F y; - (* fun_prodF : forall (x x' : C) (f : x ~> x') (y y' : C) (g : y ~> y'), *) - (* hom_cast (fun_prod _ _) (fun_prod _ _) (F^$ (f ** g)) = F^$ f ** F^$ g *) }. HB.structure Definition MonoidalPreFunctor C D := { F of @PreFunctor_IsMonoidal C D F }. Arguments fun_prod {C D F x y} : rename. (* Arguments fun_prodF {C D F x x'} f {y y'} g : rename. *) Unset Universe Checking. -HB.instance Definition _ := HasHom.Build premonoidal MonoidalPreFunctor.type. +HB.instance Definition _ := IsQuiver.Build premonoidal MonoidalPreFunctor.type. Set Universe Checking. (* Definition comma_is_premonoidal (C D E : premonoidal) *) (* (F : C ~> E) (G : D ~> E) := F. *) -HB.instance Definition _ (C : Hom.type) := - IsPreFunctor.Build [the homType of (C * C)%type] C fst +HB.instance Definition _ (C : Quiver.type) := + IsPreFunctor.Build (C * C)%type C fst (fun (a b : C * C) (f : a ~> b) => f.1). -HB.instance Definition _ (C : Hom.type) := - IsPreFunctor.Build [the homType of (C * C)%type] C snd +HB.instance Definition _ (C : Quiver.type) := + IsPreFunctor.Build (C * C)%type C snd (fun (a b : C * C) (f : a ~> b) => f.2). Definition prod3l {C : PreMonoidal.type} (x : C * C * C) : C := (x.1.1 * x.1.2) * x.2. HB.instance Definition _ {C : PreMonoidal.type} := IsPreFunctor.Build _ C prod3l - (fun a b (f : a ~> b) => (f.1.1 ** f.1.2) ** f.2). + (fun a b (f : a ~> b) => (f.1.1 <*> f.1.2) <*> f.2). Definition prod3r {C : PreMonoidal.type} (x : C * C * C) : C := x.1.1 * (x.1.2 * x.2). HB.instance Definition _ {C : PreMonoidal.type} := IsPreFunctor.Build _ C prod3r - (fun a b (f : a ~> b) => f.1.1 ** (f.1.2 ** f.2)). + (fun a b (f : a ~> b) => f.1.1 <*> (f.1.2 <*> f.2)). Definition prod1r {C : PreMonoidal.type} (x : C) : C := 1 * x. HB.instance Definition _ {C : PreMonoidal.type} := - IsPreFunctor.Build [the homType of C : Type] C prod1r - (fun (a b : C) (f : a ~> b) => \idmap_1 ** f). + IsPreFunctor.Build C C prod1r + (fun (a b : C) (f : a ~> b) => \idmap_1 <*> f). Definition prod1l {C : PreMonoidal.type} (x : C) : C := x * 1. HB.instance Definition _ {C : PreMonoidal.type} := - IsPreFunctor.Build [the homType of C : Type] C prod1l - (fun (a b : C) (f : a ~> b) => f ** \idmap_1). + IsPreFunctor.Build C C prod1l + (fun (a b : C) (f : a ~> b) => f <*> \idmap_1). HB.mixin Record PreMonoidal_IsMonoidal C of PreMonoidal C := { - prodA : prod3l ~~> prod3r :> _ ~> C; - prod1c : prod1r ~~> idfun :> C ~> C; - prodc1 : prod1l ~~> idfun :> C ~> C; + prodA : prod3l ~~> prod3r; + prod1c : prod1r ~~> idfun; + prodc1 : prod1l ~~> idfun; prodc1c : forall (x y : C), - prodA (x, 1, y) \; \idmap_x ** prod1c y = prodc1 x ** \idmap_y; + prodA (x, 1, y) \; \idmap_x <*> prod1c y = prodc1 x <*> \idmap_y; prodA4 : forall (w x y z : C), prodA (w * x, y, z) \; prodA (w, x, y * z) = - prodA (w, x, y) ** \idmap_z \; prodA (w, x * y, z) \; \idmap_w ** prodA (x, y, z); + prodA (w, x, y) <*> \idmap_z \; prodA (w, x * y, z) \; \idmap_w <*> prodA (x, y, z); }. Unset Universe Checking. @@ -618,4 +714,192 @@ HB.structure Definition Monoidal : Set := { C of PreMonoidal_IsMonoidal C & PreMonoidal C }. Set Universe Checking. +HB.mixin Record IsRing A := { + zero : A; + one : A; + add : A -> A -> A; + opp : A -> A; + mul : A -> A -> A; + addrA : associative add; + addrC : commutative add; + add0r : left_id zero add; + addNr : left_inverse zero opp add; + mulrA : associative mul; + mul1r : left_id one mul; + mulr1 : right_id one mul; + mulrDl : left_distributive mul add; + mulrDr : right_distributive mul add; +}. + +#[short(type="ringType")] +HB.structure Definition Ring := { A of IsRing A }. + +Bind Scope algebra_scope with Ring.sort. +Notation "0" := zero : algebra_scope. +Notation "1" := one : algebra_scope. +Infix "+" := (@add _) : algebra_scope. +Notation "- x" := (@opp _ x) : algebra_scope. +Infix "*" := (@mul _) : algebra_scope. +Notation "x - y" := (x + - y) : algebra_scope. + +Lemma addr0 (R : ringType) : right_id (@zero R) add. +Proof. by move=> x; rewrite addrC add0r. Qed. + +Lemma addrN (R : ringType) : right_inverse (@zero R) opp add. +Proof. by move=> x; rewrite addrC addNr. Qed. + +Lemma addKr (R : ringType) (x : R) : cancel (add x) (add (- x)). +Proof. by move=> y; rewrite addrA addNr add0r. Qed. + +Lemma addrI (R : ringType) (x : R) : injective (add x). +Proof. exact: can_inj (addKr _). Qed. + +Lemma opprK (R : ringType) : involutive (@opp R). +Proof. by move=> x; apply: (@addrI _ (- x)); rewrite addNr addrN. Qed. + +HB.mixin Record IsRingQuiver (A B : Ring.type) (f : A -> B) := { + hom1_subproof : f 1%A = 1%A; + homB_subproof : {morph f : x y / x - y}; + homM_subproof : {morph f : x y / (x * y)%A}; +}. + +HB.structure Definition RingQuiver A B := { f of IsRingQuiver A B f }. + +Lemma id_IsRingQuiver A : IsRingQuiver A A idfun. Proof. by []. Defined. +HB.instance Definition _ A := id_IsRingQuiver A. + +Lemma comp_IsRingQuiver (A B C : Ring.type) (f : RingQuiver.type A B) (g : RingQuiver.type B C) : + IsRingQuiver A C (f \; g :> U). +Proof. +by constructor => [|x y|x y]; +rewrite /comp/= ?hom1_subproof ?homB_subproof ?homM_subproof. +Qed. +HB.instance Definition _ A B C f g := @comp_IsRingQuiver A B C f g. + +HB.instance Definition _ := IsQuiver.Build Ring.type RingQuiver.type. +HB.instance Definition _ := + Quiver_IsPreCat.Build Ring.type (fun _ => idfun) (fun _ _ _ f g => f \; g :> U). +HB.instance Definition _ := Quiver_IsPreConcrete.Build Ring.type (fun _ _ => id). +Lemma ring_precat : PreConcrete_IsConcrete Ring.type. +Proof. +constructor => A B [f cf] [g cg]//=; rewrite -[_ = _]/(f = g) => fg. +case: _ / fg in cg *; congr {|RingQuiver.sort := _ ; RingQuiver.class := _|}. +case: cf cg => [[? ? ?]] [[? ? ?]]. +by congr RingQuiver.Class; congr IsRingQuiver.phant_Build => //=; apply: Prop_irrelevance. +Qed. +HB.instance Definition _ := ring_precat. + +Lemma ring_IsCat : PreCat_IsCat Ring.type. +Proof. +by constructor=> [A B f|A B f|A B C D f g h]; exact: concrete_fun_inj. +Qed. +HB.instance Definition _ := ring_IsCat. + +Lemma hom1 (R S : Ring.type) (f : R ~> S) : f 1%A = 1%A. +Proof. exact: hom1_subproof. Qed. +Lemma homB (R S : Ring.type) (f : R ~> S) : {morph f : x y / x - y}. +Proof. exact: homB_subproof. Qed. +Lemma homM (R S : Ring.type) (f : R ~> S) : {morph f : x y / (x * y)%A}. +Proof. exact: homM_subproof. Qed. +Lemma hom0 (R S : Ring.type) (f : R ~> S) : f 0%A = 0%A. +Proof. by rewrite -(addrN 1%A) homB addrN. Qed. +Lemma homN (R S : Ring.type) (f : R ~> S) : {morph f : x / - x}. +Proof. by move=> x; rewrite -[- x]add0r homB hom0 add0r. Qed. +Lemma homD (R S : Ring.type) (f : R ~> S) : {morph f : x y / x + y}. +Proof. by move=> x y; rewrite -[y]opprK !homB !homN. Qed. + +HB.mixin Record IsIdeal (R : ringType) (I : R -> Prop) := { + ideal0 : I 0; + idealD : forall x y, I x -> I y -> I (x + y); + idealM : forall x y, I y -> I (x * y)%A; +}. +HB.structure Definition Ideal (R : ringType) := { I of IsIdeal R I }. + +HB.mixin Record Ideal_IsPrime (R : ringType) (I : R -> Prop) of IsIdeal R I := { + ideal_prime : forall x y : R, I (x * y)%A -> I x \/ I y +}. +#[short(type="spec")] +HB.structure Definition PrimeIdeal (R : ringType) := + { I of Ideal_IsPrime R I & Ideal R I }. + +From HB Require Import classical. +Local Open Scope classical_set_scope. + +HB.mixin Record Topological T := { + open : (T -> Prop) -> Prop; + closed : (T -> Prop) -> Prop; + open_setT : open setT; + open_bigcup : forall {I} (D : set I) (F : I -> set T), + (forall i, D i -> open (F i)) -> open (\bigcup_(i in D) F i); + open_setI : forall X Y : set T, open X -> open Y -> open (setI X Y); + open_compl : forall X, open (~` X) = closed X +}. +HB.structure Definition TopologicalSpace := { A of Topological A }. + +#[export] Hint Extern 0 (open setT) => now apply: open_setT : core. + +HB.factory Record TopologicalBase T := { + open_base : set (set T); + open_base_covers : setT `<=` \bigcup_(X in open_base) X; + open_base_cup : forall X Y : set T, open_base X -> open_base Y -> + forall z, (X `&` Y) z -> exists2 Z, open_base Z & Z z /\ Z `<=` X `&` Y +}. + +HB.builders Context T (a : TopologicalBase T). + + Definition open_of := + [set A | exists2 D, D `<=` open_base & A = \bigcup_(X in D) X]. + + Definition closed_of := [set A | open_of (~` A)]. + + Lemma open_of_setT : open_of setT. + Proof. + exists open_base; rewrite // predeqE => x; split=> // _. + by apply: open_base_covers. + Qed. + + Lemma open_of_bigcup {I} (D : set I) (F : I -> set T) : + (forall i, D i -> open_of (F i)) -> open_of (\bigcup_(i in D) F i). + Proof. Admitted. + + Lemma open_of_cap X Y : open_of X -> open_of Y -> open_of (X `&` Y). + Proof. Admitted. + + HB.instance Definition to_Topological := + @Topological.Build T open_of closed_of open_of_setT + (@open_of_bigcup) open_of_cap (fun=> erefl). + +HB.end. + +HB.factory Record TopologicalClosedBase T := { + closed_base : set (set T); + closed_base_cap : setT `<=` \bigcup_(X in closed_base) X; + closed_base_cup : forall X Y : set T, closed_base X -> closed_base Y -> + forall z, (X `&` Y) z -> exists2 Z, closed_base Z & Z z /\ Z `<=` X `&` Y +}. + +HB.builders Context T (a : TopologicalClosedBase T). + + Definition open_of := + [set A | exists2 D, D `<=` [set ~` X | X in closed_base] & A = \bigcup_(X in D) ~` X]. + + Definition closed_of := [set A | open_of (~` A)]. + + Lemma open_of_setT : open_of setT. + Proof. + Admitted. + + Lemma open_of_bigcup {I} (D : set I) (F : I -> set T) : + (forall i, D i -> open_of (F i)) -> open_of (\bigcup_(i in D) F i). + Proof. Admitted. + + Lemma open_of_cap X Y : open_of X -> open_of Y -> open_of (X `&` Y). + Proof. Admitted. + + HB.instance + Definition to_Topological := + @Topological.Build T open_of closed_of + open_of_setT (@open_of_bigcup) open_of_cap (fun=> erefl). + +HB.end. From ec9033d231bfdd570336c1a6323f0f6ed5127b2f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 19 Apr 2023 00:55:06 +0200 Subject: [PATCH 60/60] adding examples/cat/cat.v to test-suite --- _CoqProject.test-suite | 2 ++ 1 file changed, 2 insertions(+) diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index 98c20167e..88384982b 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -52,6 +52,8 @@ examples/Coq2020_material/CoqWS_abstract.v examples/Coq2020_material/CoqWS_expansion/withHB.v examples/Coq2020_material/CoqWS_expansion/withoutHB.v +examples/cat/cat.v + tests/type_of_exported_ops.v tests/duplicate_structure.v tests/instance_params_no_type.v