Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

wrapper mixin step0 #370

Draft
wants to merge 64 commits into
base: master
Choose a base branch
from
Draft

wrapper mixin step0 #370

wants to merge 64 commits into from

Commits on Jun 2, 2023

  1. test for step 0 of CoREACT

    @gares
    gares committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    6f1dee6 View commit details
    Browse the repository at this point in the history

  2. update

    @gares
    gares committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    1ceb6ea View commit details
    Browse the repository at this point in the history

  3. more

    @gares
    gares committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    f6c1970 View commit details
    Browse the repository at this point in the history

  4. more

    @gares
    gares committed Jun 2, 2023
    Configuration menu
    Copy the full SHA
    17d6561 View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2023

  1. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    d2bc00f View commit details
    Browse the repository at this point in the history

  2. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    6726472 View commit details
    Browse the repository at this point in the history

  3. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    0821793 View commit details
    Browse the repository at this point in the history

  4. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    234e3f5 View commit details
    Browse the repository at this point in the history

  5. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    92e1f68 View commit details
    Browse the repository at this point in the history

  6. Update tests/monoid_enriched_cat.v

    @CohenCyril
    CohenCyril authored Jun 19, 2023
    Configuration menu
    Copy the full SHA
    b7f3789 View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2023

  1. added enriched_cat.v

    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    80e17f2 View commit details
    Browse the repository at this point in the history

  2. copied Cyril's monoid_enriched_cat.v to enriched_cat.v

    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    314c6b9 View commit details
    Browse the repository at this point in the history

  3. added monoid_enriched_cat.v as the original pull request by Cyril, in… 

    …conclusively modified enriched_cat.v (the version I'm working on)
    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    67526eb View commit details
    Browse the repository at this point in the history

  4. add enriched_cat to _CoqProject

    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    a3bcee5 View commit details
    Browse the repository at this point in the history

  5. changes to enriched_cat.v

    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f472ce6 View commit details
    Browse the repository at this point in the history

  6. changes related to monoid_enriched_cat.v and wrappers in various file… 

    …s. changes in enriched_cat.v
    @ptorrx
    ptorrx committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    b3ba8c1 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2023

  1. change to enriched_cat.v

    @ptorrx
    ptorrx committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    9f0bde5 View commit details
    Browse the repository at this point in the history

  2. minor changes

    @ptorrx
    ptorrx committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    056f6e0 View commit details
    Browse the repository at this point in the history

Commits on Jun 23, 2023

  1. added Elpi code in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 23, 2023
    Configuration menu
    Copy the full SHA
    b78c77c View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2023

  1. changes in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    0d0e9b7 View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2023

  1. added improved version of extraction predicates in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    b6b8278 View commit details
    Browse the repository at this point in the history

  2. minor changes in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    145aa0d View commit details
    Browse the repository at this point in the history

  3. moved Elpi code from monoid_enriched_cat.v to factory.v. monoid-enric… 

    …hed_cat.v compiles
    @ptorrx
    ptorrx committed Jun 27, 2023
    Configuration menu
    Copy the full SHA
    8d0310e View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2023

  1. minor changes in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    0b2b79f View commit details
    Browse the repository at this point in the history

  2. added instance in monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    7fbd129 View commit details
    Browse the repository at this point in the history

  3. added some tests to monoid_enriched_cat.v

    @ptorrx
    ptorrx committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    5ded009 View commit details
    Browse the repository at this point in the history

  4. pseudo-code to add new instances for each wrapper mixin

    @CohenCyril
    CohenCyril committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    2ea2be6 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. added some comment

    @ptorrx
    ptorrx committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    2fccea4 View commit details
    Browse the repository at this point in the history

  2. tentative changes in structure.elpi (reexport-wrapper-as-instance is … 

    …not right, it is just meant to compile) - anyway it makes compilation of HB.structure Monoid_enriched_quiver fail
    @ptorrx
    ptorrx committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    1ffc93d View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2023

  1. changes in structure.elpi and monoid_enriched_cat.v - compiles

    @ptorrx
    ptorrx committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    d9c7980 View commit details
    Browse the repository at this point in the history

  2. added comments in structure.elpi

    @ptorrx
    ptorrx committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    7158c54 View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2023

  1. changes in structure.elpi, to prepare the derivation of the wrapper i… 

    …nstance
    @ptorrx
    ptorrx committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    7ec530a View commit details
    Browse the repository at this point in the history

  2. added comments in structure.elpi

    @ptorrx
    ptorrx committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    7e83bd9 View commit details
    Browse the repository at this point in the history

  3. tentative changes to structure.elpi

    @ptorrx
    ptorrx committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    40eef02 View commit details
    Browse the repository at this point in the history

Commits on Jul 4, 2023

  1. changes in structure.elpi - mainly comments

    @ptorrx
    ptorrx committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    a26cf4b View commit details
    Browse the repository at this point in the history

  2. changes in structure.elpi - mainly comments

    @ptorrx
    ptorrx committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    09b0222 View commit details
    Browse the repository at this point in the history

  3. main changes in instance.elpi

    @ptorrx
    ptorrx committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    e5f56a1 View commit details
    Browse the repository at this point in the history

  4. added commments in instance.elpi

    @ptorrx
    ptorrx committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    36dc631 View commit details
    Browse the repository at this point in the history

  5. minor changes in monoid_enriched_cat.v (wrapper instance definition n… 

    …ot commented out yet)
    @ptorrx
    ptorrx committed Jul 4, 2023
    Configuration menu
    Copy the full SHA
    b46a369 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2023

  1. Update tests/monoid_enriched_cat.v 

    Co-authored-by: Cyril Cohen <[email protected]>
    @ptorrx @CohenCyril
    ptorrx and CohenCyril authored Jul 5, 2023
    Configuration menu
    Copy the full SHA
    d93a11d View commit details
    Browse the repository at this point in the history

  2. added summary of today's discussion at the bottom of instance.elpi

    @ptorrx
    ptorrx committed Jul 5, 2023
    Configuration menu
    Copy the full SHA
    e4c3732 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/wrapper' into wrapper

    @ptorrx
    ptorrx committed Jul 5, 2023
    Configuration menu
    Copy the full SHA
    8c30d1a View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2023

  1. setup nix

    @CohenCyril
    CohenCyril committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    911ede1 View commit details
    Browse the repository at this point in the history

  2. blind attempt

    @CohenCyril
    CohenCyril committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    4e47908 View commit details
    Browse the repository at this point in the history

  3. minor changes to comments in instance.elpi

    @ptorrx
    ptorrx committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    3d0961c View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2023

  1. added debug printouts

    @ptorrx
    ptorrx committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    314dadc View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2023

  1. revised comments and printouts, minor change in structure.elpi to nam… 

    …e instance
    @ptorrx
    ptorrx committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    5f18ee4 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. Switched to tentive version of add-all-mixins with extra parameter. B… 

    …reaks the compilation of the Coq code. Included call to derive-wrapper-instances in declare-all, but not really sure about it. Commented out funQ_isMon in monoid_enriched_cat.v because it should be derivable, once funQ_hom_isMon is available. But actually I can't see where HB learns about funQ_isMonF, except in the funQ_hom_isMon definition (the one we should actually generate)
    @ptorrx
    ptorrx committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    ce51cc4 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2023

  1. gone back to old add-all-mixins (without std.forall), revised comment… 

    …s in instance.elpi, funQ_isMon back in
    @ptorrx
    ptorrx committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    641d35d View commit details
    Browse the repository at this point in the history

  2. gone back to old add-all-mixins (without std.forall), revised comment… 

    …s in instance.elpi, funQ_isMon back in
    @ptorrx
    ptorrx committed Jul 19, 2023
    Configuration menu
    Copy the full SHA
    6bdfd59 View commit details
    Browse the repository at this point in the history

Commits on Jul 20, 2023

  1. added predicates to handle cumulative output over forall, avoiding du… 

    …plicates in the association list (which was broken in DCIFF with std.forall)
    @ptorrx
    ptorrx committed Jul 20, 2023
    Configuration menu
    Copy the full SHA
    790ca44 View commit details
    Browse the repository at this point in the history

  2. added redirect-instances (instances.elpi), in progress

    @ptorrx
    ptorrx committed Jul 20, 2023
    Configuration menu
    Copy the full SHA
    f0975bb View commit details
    Browse the repository at this point in the history

Commits on Jul 21, 2023

  1. instance.elpi, redirect-instances - in progress (section problem)

    @ptorrx
    ptorrx committed Jul 21, 2023
    Configuration menu
    Copy the full SHA
    73e614b View commit details
    Browse the repository at this point in the history

  2. instance.elpi, redirect-instances - in progress (section problem)

    @ptorrx
    ptorrx committed Jul 21, 2023
    Configuration menu
    Copy the full SHA
    ab87dd8 View commit details
    Browse the repository at this point in the history

  3. instance.elpi: redirect-instances in progress, still need to add call… 

    … to declare-instance
    @ptorrx
    ptorrx committed Jul 21, 2023
    Configuration menu
    Copy the full SHA
    11baf58 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. instance.elpi: redirect-instances in progress, added call to declare-… 

    …instance, not working yet
    @ptorrx
    ptorrx committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    8e22bb3 View commit details
    Browse the repository at this point in the history

  2. instance.elpi: redirect-instances in progress, added call to declare-… 

    …instance, now working
    @ptorrx
    ptorrx committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    3dbe65e View commit details
    Browse the repository at this point in the history

  3. more comments in instance.elpi, added lemma in enriched_cat.v and fac… 

    …tory-based example in monoid_enriched_cat_factory.v
    @ptorrx
    ptorrx committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    e7361bf View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. enriched_cat.v: minor changes

    @ptorrx
    ptorrx committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    9d80cdf View commit details
    Browse the repository at this point in the history

  2. enriched_cat.v: minor changes

    @ptorrx
    ptorrx committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    7835883 View commit details
    Browse the repository at this point in the history

Commits on Aug 3, 2023

  1. test commit, minor changes

    @ptorrx
    ptorrx committed Aug 3, 2023
    Configuration menu
    Copy the full SHA
    f8da435 View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2023

  1. adding examples in cmon_enriched_cat.v

    @ptorrx
    ptorrx committed Aug 4, 2023
    Configuration menu
    Copy the full SHA
    2338a1f View commit details
    Browse the repository at this point in the history

Commits on Aug 9, 2023

  1. updated cmonoid_enriched_cat.v with new examples; some problems

    @ptorrx
    ptorrx committed Aug 9, 2023
    Configuration menu
    Copy the full SHA
    7907b7f View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2023

  1. updated cmon_enriched_cat.v - now the file contains three examples; c… 

    …ompilation glitch (it will compile only the first two of them, regardless of which you put first; so all the examples compile, but not together)
    @ptorrx
    ptorrx committed Aug 10, 2023
    Configuration menu
    Copy the full SHA
    ce88b3d View commit details
    Browse the repository at this point in the history