Merge pull request #194 from math-comp/improve-readme

Update README.md

README.md

@@ -3,24 +3,34 @@
 
 # Hierarchy Builder
 
-High level commands to declare and evolve a hierarchy based on packed classes.
+Hierarchy Builder (HB) provides high level commands to declare a hierarchy of algebraic structure
+(or interfaces if you prefer the glossary of computer science) for the Coq system.
 
-[Presented at FSCD2020, talk available on youtube.](https://www.youtube.com/watch?v=F6iRaTlQrlo)
+Given a structure one can develop its theory, and that theory becomes automatically applicable to
+all the examples of the structure. One can also declare alternative interfaces, for convenience
+or backward compatibility, and provide glue code linking these interfaces to the structures part of
+the hierarchy.
+
+HB commands compile down to Coq modules, sections, records, coercions, canonical structure instances
+and notations following the *packed classes* discipline which is at the core of the [Mathematical
+Components](https://github.com/math-comp/math-comp) library. All that complexity is hidden behind
+a few concepts and a few declarative Coq commands.
 
 ## Example
 
 ```coq
 From HB Require Import structures.
 From Coq Require Import ssreflect ZArith.
 
-HB.mixin Record AddComoid_of_Type A := {
+HB.mixin Record IsAddComoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : forall x y z, add x (add y z) = add (add x y) z;
   addrC : forall x y, add x y = add y x;
   add0r : forall x, add zero x = x;
 }.
-HB.structure Definition AddComoid := { A of AddComoid_of_Type A }.
+
+HB.structure Definition AddComoid := { A of IsAddComoid A }.
 
 Notation "0" := zero.
 Infix "+" := add.
@@ -35,17 +45,18 @@ We proceed by declaring how to obtain an Abelian group out of the
 additive, commutative, monoid.
 
 ```coq
-HB.mixin Record AbelianGrp_of_AddComoid A of AddComoid A := {
+HB.mixin Record AddComoid_IsAbelianGrp A of IsAddComoid A := {
   opp : A -> A;
   addNr : forall x, opp x + x = 0;
 }.
-HB.structure Definition AbelianGrp := { A of AbelianGrp_of_AddComoid A & }.
+
+HB.structure Definition AbelianGrp := { A of AddComoid_IsAbelianGrp A & IsAddComoid A }.
 
 Notation "- x" := (opp x).
 ```
 
 Abelian groups feature the operations and properties given by the
-`AbelianGrp_of_AddComoid` mixin (and its dependency `AddComoid`).
+`IsAbelianGrp` mixin (and its dependency `IsAddComoid`).
 
 ```coq
 Lemma example (G : AbelianGrp.type) (x : G) : x + (- x) = - 0.
@@ -57,22 +68,19 @@ the lemma just proved on a statement about `Z`.
 
 ```coq
 HB.instance Definition Z_CoMoid :=
-  AddComoid_of_Type.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+  IsAddComoid.Build Z 0%Z Z.add Z.add_assoc Z.add_comm Z.add_0_l.
+ 
 HB.instance Definition Z_AbGrp :=
-  AbelianGrp_of_AddComoid.Build Z Z.opp Z.add_opp_diag_l.
+  IsAbelianGrp.Build Z Z.opp Z.add_opp_diag_l.
 
 Lemma example2 (x : Z) : x + (- x) = - 0.
 Proof. by rewrite example. Qed.
 ```
 
 ## Documentation
 
-### Status
-
-The software is beta-quality, it works but error messages should be improved.
-
-This [draft paper](https://hal.inria.fr/hal-02478907) describes the language
-in full detail.
+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)
 
 ### Installation & availability
 
@@ -87,7 +95,8 @@ opam repo add coq-released https://coq.inria.fr/opam/released
 opam install coq-hierarchy-builder
 ```
 
-- You can use it in nix with the attribute `coqPackages_8_11.hierarchy-builder` e.g. via `nix-shell -p coq_8_11 -p coqPackages_8_11.hierarchy-builder`
+- You can use it in nix with the attribute `coqPackages_8_11.hierarchy-builder` e.g.
+  via `nix-shell -p coq_8_11 -p coqPackages_8_11.hierarchy-builder`
 
 </p></details>
 
@@ -115,19 +124,25 @@ opam install coq-hierarchy-builder
 
 <details><summary>(click to expand)</summary><p>
 
-- `HB.mixin` declares a mixin
-- `HB.structure` declares a structure
-- `HB.factory` declares a factory
-- `HB.builders` and `HB.end` declare a set of builders
-- `HB.instance` declares a structure instance
-- `HB.export` exports a module and schedules it for re-export
-- `HB.reexport` exports all modules scheduled for re-export
-- `HB.graph` prints the structure hierarchy to a dot file
-- `HB.status` dumps the contents of the hierarchy (debug purposes)
-
-Their documentation can be found in the comments of [structures.v](structures.v),
-search for `Elpi Command` and you will find them. All commands can be
-prefixed with the attribute `#[verbose]` to get an idea of what they are doing.
+- HB core commands:
+  - `HB.mixin` declares a mixin
+  - `HB.structure` declares a structure
+  - `HB.factory` declares a factory
+  - `HB.builders` and `HB.end` declare a set of builders
+  - `HB.instance` declares a structure instance
+
+- HB support commands:
+  - `HB.export` exports a module and schedules it for re-export
+  - `HB.reexport` exports all modules and instances scheduled for re-export
+  - `HB.graph` prints the structure hierarchy to a dot file
+  - `HB.status` dumps the contents of the hierarchy (debug purposes)
+  - `HB.check` is similar to `Check` (test purposes)
+
+The documentation of all commands can be found in the comments of
+[structures.v](structures.v), search for `Elpi Command` and you will
+find them. All commands can be prefixed with the attribute `#[verbose]`
+to get an idea of what they are doing.
+
 See also the `#[log]` attribute in the "Plan B" section below.
 
 </p></details>