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

Fix for issue #305 + some related problems #307

Merged
merged 8 commits into from
Mar 22, 2024
Merged

Fix for issue #305 + some related problems #307

merged 8 commits into from
Mar 22, 2024

Commits on Mar 15, 2024

  1. [ fix agda#305 ] Set the module checkpoint when entering the clause body

    @jespercockx
    jespercockx committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    a4dea24 View commit details
    Browse the repository at this point in the history

  2. Add some debug printing to compilation of instances

    @jespercockx
    jespercockx committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    f6e2874 View commit details
    Browse the repository at this point in the history

  3. [ re agda#305 ] Also set context + checkpoint when checking superclas… 

    …s clauses
    @jespercockx
    jespercockx committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    1c47efa View commit details
    Browse the repository at this point in the history

  4. Add missing call to instantiate in compileTerm 

    I ran into this while debugging agda#305, though I cannot reproduce a test case now.
It seems like it's the right thing to do regardless.
    @jespercockx
    jespercockx committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    778f5f5 View commit details
    Browse the repository at this point in the history

  5. Do not drop instance clauses but instead check canonicity 

    This was a regression introduced by agda#304 that went unnoticed due to a lack of a (failing) test case
    @jespercockx
    jespercockx committed Mar 15, 2024
    Configuration menu
    Copy the full SHA
    4ae8105 View commit details
    Browse the repository at this point in the history

Commits on Mar 16, 2024

  1. Some more debug printing for compilation of instances

    @jespercockx
    jespercockx committed Mar 16, 2024
    Configuration menu
    Copy the full SHA
    9b10d36 View commit details
    Browse the repository at this point in the history

  2. [ re agda#305 ] More robust inlining of indirectly defined instances 

    The old implementation using chaseDef was quite brittle and was causing problems with the fix of agda#305, so rather than fixing it I replaced it with a more direct (and hopefully more robust) implementation that inlines instances that are defined elsewhere
    @jespercockx
    jespercockx committed Mar 16, 2024
    Configuration menu
    Copy the full SHA
    455c69f View commit details
    Browse the repository at this point in the history

Commits on Mar 21, 2024

  1. [ re agda#305 ] Set the checkpoint in the context of the module rathe… 

    …r than the clause
    @jespercockx
    jespercockx committed Mar 21, 2024
    Configuration menu
    Copy the full SHA
    ea87646 View commit details
    Browse the repository at this point in the history