math-comp / hierarchy-builder Goto Github PK
View Code? Open in Web Editor NEWHigh level commands to declare a hierarchy based on packed classes
License: MIT License
High level commands to declare a hierarchy based on packed classes
License: MIT License
The Coq team is planning to release Coq 8.13-beta1 on December 7, 2020
and Coq 8.13.0 on January 7, 2020.
Your project is currently scheduled for being bundled in the Windows installer.
We are currently testing commit 6089de4
on branch https://github.com/math-comp/hierarchy-builder/tree/coq-master
but we would like to ship a released version instead (a tag in git's slang).
Could you please tag that commit, or communicate us any other tag
that works with the Coq branch v8.13 at the latest 15 days before the
date of the final release?
Thanks!
CC: coq/coq#12334
Idea:
HB.builders Context T (f : F T).
Module Super.
Definition foo := foo.
End Super.
Section.
Variable T.
Variable f.
Definition foo := foo f.
... user code can access both foo and Super.foo ..
There is a bug in coq-elpi that I am failing to track down and minimize, @gares could you look into this?
Lines 597 to 601 in 08064db
The bug was particularly hard to track, because uncommenting the above coq.env-add-const
unexpectedly makes the following coq.typecheck
fail... (which succeeds otherwise,... this is a really nasty side-effect)
Line 608 in 08064db
The bug was not there before, because we used to called Elpi declare_factory_fun ...
after we manually closed the section and the module using the vernacular End S. End Module.
. But since then, I decided to make the same elpi command close the section and call main-declare-factory-fun
, using coq.env.end-section
:
Line 732 in 08064db
e.g.
HB.mixin Record bla (T : Type) := ....
HB.arguments bla T%scope
Check (bla (_ * _)).
Today you are force to write stuff like HB.instance { x : T &.... } t
but actually only sigT
is really needed
Generate pack
in order to build a structure from a single mixin.
to play safe and avoid the bug fixed in 82ee5b9 we could (should?)
typecheck the terms before calling the unifier. That would have detected the missing parameters.
@gares how do I replace
hierarchy-builder/demo2/stage11.v
Lines 172 to 173 in 854fc09
Elpi hb.canonical (T1 * T2)%type prod_topology.
?
(making coq-elpi insert the coercion TopologicalSpace.sort
)
It seems that we should have:
main
. If there are conflicts we can use the namespace
directive. In this way all commands can share utility code without putting it in the db.hb.factory.begin
, hb.mixin.begin
, hb.mixin.end
and hb.factory.end
sharing 99% of the code (as it is now, but without the "mixin"
argument and the crapload of code in the db).In a not so close future elpi DBs are supposed to be dynamic (compiled at each execution if needed), while the rest of the code compiled once and forall.
Hey everyone,
I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in Iris. This was really just for fun since I do not expect the result to be usable given Iris's reliance on type classes. I also wanted to learn from the resulting definitions since I still don't really understand how one is supposed to set up canonical structures.
But my experiment ended before I got to actually trying out the result. I pushed the experiment to https://gitlab.mpi-sws.org/janno/iris-coq/-/tree/janno/try-HB (the branch name is janno/try-HB
). The only file that changed is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v. It contains both old an new definitions, which are confined to lines 150-178. The original file without my new stuff is here: https://gitlab.mpi-sws.org/iris/iris/-/blob/962637df10a879ac4b1b9d523854d6fa4c9e8fb4/theories/bi/interface.v
Of particular interest is https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L242 where I cannot get HB to accept the definition of an SBI (an extension of the BI definition in https://gitlab.mpi-sws.org/janno/iris-coq/-/blob/janno/try-HB/theories/bi/interface.v#L156). The error HB reports is this (when using the right printing settings):
The term "@Some" of type "∀ A : Type, A → option A"
cannot be applied to the terms
"?e5" : "Type"
"("is not canonically a", bi.type)" : "(string * Type)%type"
I suppose the underlying error is a mistake on my side but I don't know what it would be.
To get to this point I also had to work around an unexpected shortcoming regarding implicit type class arguments. As you can see in the definition of the BI structure, I had to manually spell out all type class instances since HB would not accept the terms otherwise. (This is veeeeery annoying since it also means that notation such as that for equiv
needs to be unfolded.)
Finally, there's something that I wouldn't count as a bug but more of a feature request: in the original Iris hierarchy, the bi_mixin Section (at the top of the file) creates local notation for the operators that make the axioms look very natural. I couldn't find a way to replicate this setup. Maybe HB.mixin
could accept where
clauses for (local) syntax?
Building the branch
My opam switch reports the following packages:
coq-elpi 1.3.1 Elpi extension language for Coq
coq-hierarchy-builder 0.9.0 Hierarchy Builder
coq-stdpp dev.2019-12-06.0.1ef53c55 pinned to version dev.2019-12-06.0.1ef53c55 at git+https://gitlab.mpi-sws.org/iris/stdpp.git
If you want to avoid pinning coq-stdpp to the git hash (the suffix of that weird dev version) you can
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
and then opam should be able to find that exact version.
Running make
inside a clone of my iris-coq branch should eventually compile interfaces.v and report the errors.
Test case:
From HB Require Import structures.
HB.mixin Record base_m T := { A : T }.
HB.structure Definition base := { T of base_m T }.
HB.mixin Record child1_m T := { C1 : T }.
HB.structure Definition child1 := { T of base T & child1_m T }.
HB.mixin Record child2_m T := { C2 : T }.
HB.structure Definition child2 := { T of base T & child2_m T }.
Axiom ix : Type.
Definition vec T := ix -> T.
Section b.
Variable T : base.type.
HB.instance Definition v_base_m : base_m (vec T) :=
base_m.Build _ (fun _ => A).
End b.
Section c1.
Variable T : child1.type.
HB.instance Definition v_child1_m : child1_m (vec T) :=
child1_m.Build _ (fun _ => C1).
End c1.
Section c2.
Variable T : child2.type.
(* CS lookup for `vec` says yes... but the instance is for a paramter T of different type, kaboom *)
HB.instance Definition v_child2_m : child2_m (vec T) :=
child2_m.Build _ (fun _ => C2).
End c2.
HB.mixin Record eqType_of_Type T := {
op : rel T;
eqP : Equality.axiom op;
}.
HB.structure Definition eq := { T of eqType_of_Type T }.
Canonical hb_eqMixin {T : eq.type} := @EqMixin T _ eqP.
Canonical hb_eqType {T : eq.type} := Eval hnf in EqType T hb_eqMixin.
Definition foo {T : eq.type} (e : T) := e == e.
HB.mixin Record my_class_of_eqType T of eq T := {
foo: T -> T;
}.
HB.structure Definition my := { T of eq T & my_class_of_eqType T }.
Fail Definition foo1 {T : my.type} (e : T) := e == e.
Fail Canonical porder_eqMixin {T : my.type} := @EqMixin T _ eqP.
I want to make my structure with decidable equality via HB. Then it could be an instance of mathcomp's eqType
. I make my.type
that inherits eq.type
, so my.type
is coercible to eq.type
which is coercible to eqType
. But if you look at foo1
definition you can see that Coq can't solve such a unification problem. Also, I can't make a new Canonical instance for my.type
because it conflicts with hb_eqMixin
.
Declare Scope HB_scope.
Notation "{ x & P }" := (sigT (fun x : Type => P%type)) (at level 0, x at level 99) : HB_scope.
Notation "{ x 'of' P & .. & Q }" := (sigT (fun x : Type => (prod P .. (prod Q True) ..)%type)) (at level 0, x at level 99) : HB_scope.
Global Open Scope HB_scope.
Check { T of False * True & { W of W = T } & option T }.
Check { T & T * True }.
This seems to work and make it possible to use "A of .. & .." also in structures.
#[mixin]
HB Record AbGroup.axioms A of (Monoid.axioms A) := { opp : A->A; stuff.. }.
#[factory]
HB Record Monoid_of_Type.axioms A := { ... } as f.
#[builder] HB Definition _ : AbGroup.axioms A _ := AbGroup.Axioms A (foo f).
HB End.
HB Structure Ring of Foo.axioms Bar.axioms.
HB Instance T AxT.
I think I'd like a query printing out the mixins (and maybe their contents) that one can get from a set of given factories. In some sense it is what we were doing this morning by hand (used to be explicit in hb.end
).
More in general Elpi Print hb.debug
is too low level for a final user.
Maybe hb.debug
could just have a real main and dump the DB in a human understandable format, but I think being able to query the DB without knowing how to write elpi code may help a final user.
As noted by @chdoc on zulip.
C.f. https://gist.github.com/chdoc/f50c3a15c41e92ec0ac89112f1e18fbe
error message is about split-at but should talk about missing parameters
otherwise error messages are misleading (they talk about T, but the user wrote A)
hierarchy-builder/structures.v
Line 383 in 22cc857
There is no _f
anymore
Cf mathcomp port subLmodule structure definition.
The latter could be renamed to factoryname-or-alias, or something like that.
I think:
hb.v
to tool/HB.v
and hb.elpi
to tool/HB.elpi
demo*
to tests
or examples
(see the little testing infrastructure I wrote in Makefile.coq.local)Makefile
that builds tool
(with coq_makefile) and then uses the result to build the rest, putting tool/
in the coqpath as if it was installed in user-contrib
(so we test how final users would get HB`if the same mixin can be built in two different ways, both from the factories provided or from the existing instances, they must be convertible.
Just to say I'm almost done.
As of now we assume that the constant added by coq.env.add-const
have explicit arguments, we should not assume such a thing because it is not true with option Set Implicit Arguments
When using HB commands requiring a telescope.
E.g.
HB.builders Context (V : zmodType) .... of stuff V
where stuff
requires a zmodType
, should make the explicit typing of v
optional.
Blocked by LPCIC/coq-elpi#210
As of today we can only write
Section Foo.
Variable A : Type.
HB.instance Definition list_m1 := m1.Build (option A) (list nat) (cons 7 nil) None.
End Foo.
If we abstract list_m1
over A
we get an assertion in
pred mixin-srcs i:term, i:term, o:list prop.
mixin-srcs T X MSL :- std.do! [
std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
if (not (safe-dest-app XTy (global _) _))
(coq.error "Term:\n" {coq.term->string X}
"\nhas type:\n" {coq.term->string XTy}
"\nwhich is not a record")
Instead we should record the abstractions before the record and put them in front of S
pred declare-instances i:term, i:list class.
declare-instances T [class Class Struct MLwP|Rest] :-
params->holes MLwP Params,
get-class-constructor Class Params KC,
list-w-params_list MLwP ML,
mterm->term (mterm [/*Params already applied to KC*/] T ML KC) KCApp, % we can build it
not (local-cs? T Struct), % not already built
!,
term->gref T TGR,
coq.gref->id TGR TID,
Name is TID ^ "_is_a_" ^ {term->modname Struct},
if-verbose (coq.say "HB: declare canonical instance" Name),
get-structure-constructor Struct Params KS,
S = app[KS, T, KCApp],
E.g.
Definition stuff T : mixin (f T) := ...
HB.instance f stuff.
instead of
Section stuff.
Variable T.
Definition stuff : mixin (f T) := ...
HB.instance (f T) stuff.
End stuff.
Can you provide the best way to inherit mathcomp's structures? I want to make something like this:
Section foo.
Variable (T : eqType).
HB.mixin my_class_of_eqType T := { ... }. (*or something like that*)
Is there any way to inherit mathcomp's eqType
?
Kind of looks nice
While updating the paper it seemed desirable to let the user omit .axioms
in F.axions
when F
is a module name containing a axioms
factory.
It seems trivial to implement
If hierachy builder is installed via opam, the examples are
This because they use require statements like From HB.demo2 Require Import classical.
which assume that demo2 is installed with HB, but this is not the case. I see a few possible solutions:
1.) Install the examples required as prerequisites including .vo files
2.) Remove the From HB.demo2
so that files can be compiled locally one by one and run (e.g. in CoqIDE with compile buffer)
3.) Install the examples with a _CoqProject file which sets proper -Q options, so that this does work
Definition addrA :
forall x : AddComoid.type,
associative
((fun=> add)
(AddComoid.AddComoid_of_Type_mixin x (AddComoid.class x))).
We should either let this projection be anonymous and redeclare it by pattern matching later, or make Coq not register it when 8.11 is out.
Line 711 in e118e77
do not rely on std.findall order
Error messages given by, eg, HB.instance are not intellegible if the string scope is not open.
Should be Export an Open Scope string_scope in hb.v?
In 8.12 you can write #[local] Canonical foo
We should replace by another kind of meta information.
In the definition of mixin like the next one:
HB.mixin Record foo T := {
bar : T -> true;
}.
there is an error without any meaningful explanation. However, after the insertion of coercion manually, it works fine:
HB.mixin Record foo T := {
bar : T -> (is_true true);
}.
So, it would be great if the coercion insertion was automatic.
Code
Lines 501 to 506 in 01c2492
You must declare
class (indt «axioms») (global (indt «type»))
(w-params.nil `A` (sort (typ «bug.9333»)) c0 \
[triple (indt «Ops_of_Type.axioms_») [] c0,
triple (indt «Setoid_of_Type.axioms_») [] c0,
triple (indt «Ptt_of_Ops.axioms_») [] c0]) before
indt «Pttdom.axioms»
The "class" must be printed better, also we should try to print only structure names (classes are sort of internal)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.