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

Using typeclasses in src/ #2969

Merged
merged 10 commits into from
Nov 27, 2023
Merged

Using typeclasses in src/ #2969

merged 10 commits into from
Nov 27, 2023

Commits on Nov 27, 2023

  1. nit on error message

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    8098801 View commit details
    Browse the repository at this point in the history

  2. Parser: introduce instance val

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    d9d0410 View commit details
    Browse the repository at this point in the history

  3. Makefile.boot: --MLish is never used for ulib/, yes for everything else

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    a615721 View commit details
    Browse the repository at this point in the history

  4. Makefile.boot: compiler extracts with --codegen Plugin

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    23440a5 View commit details
    Browse the repository at this point in the history

  5. Compiler: 'Stubbing' everything 

    To prevent circularities when using typeclasses within the compiler
(since we need to refer to tactic modules potentially from anywhere)
we stub all of the exposed interfaces in ulib, so the compiler does
not 'realize' they are the same modules. Extraction then takes care of
removing the 'Stubs' namespace component, essentially closing the loop.
    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    cd67c6e View commit details
    Browse the repository at this point in the history

  6. Introduce src/class and FStar.Compiler.Show

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    b5c505f View commit details
    Browse the repository at this point in the history

  7. Tactics: small example using show

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    da7a20a View commit details
    Browse the repository at this point in the history

  8. Introduce FStar.Class.PP

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    0483c42 View commit details
    Browse the repository at this point in the history

  9. snap

    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    117a847 View commit details
    Browse the repository at this point in the history

  10. Update expected output 

    Now mentions Stubs
    @mtzguido
    mtzguido committed Nov 27, 2023
    Configuration menu
    Copy the full SHA
    97f7dfc View commit details
    Browse the repository at this point in the history