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

Improvements to the Heapster Rust translation #1365

Merged
merged 12 commits into from
Jul 1, 2021
Merged

Improvements to the Heapster Rust translation #1365

merged 12 commits into from
Jul 1, 2021

Commits on Jun 30, 2021

  1. updated Makefile to fall back on cabal run saw if a saw executable is… 

    … not installed
    Eddy Westbrook committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    f700755 View commit details
    Browse the repository at this point in the history

  2. added arrays.v back as a Coq file that needs to be built for CI

    Eddy Westbrook committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    e64b442 View commit details
    Browse the repository at this point in the history

  3. updated the generated arrays.v

    Eddy Westbrook committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    7e4fb51 View commit details
    Browse the repository at this point in the history

  4. added heapster_define_rust_type_qual to allow defined Rust types to b… 

    …e qualified with their crates; changed the Rust type translation to use this qualification by translating Rust names in a fully qualified way
    Eddy Westbrook committed Jun 30, 2021
    Configuration menu
    Copy the full SHA
    5e64d20 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2021

  1. whoops, forgot to add the rest of the changes that implemented heapst… 

    …er_define_rust_type_qual to the last commit; also changed parseAndInsDef to not fail when an identifier is already being used, but to instead generate a new, unused identifier
    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    5ff38ea View commit details
    Browse the repository at this point in the history

  2. added a Tree data structure, which uses Vec in its recursive definiti… 

    …on, as an example in rust_data
    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    fd47f04 View commit details
    Browse the repository at this point in the history

  3. backwards compatibility tweak

    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    68bbe47 View commit details
    Browse the repository at this point in the history

  4. bug fix for heapster_define_rust_type: print out an error message whe… 

    …n a recursive type cannot be handled
    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    8cd1469 View commit details
    Browse the repository at this point in the history

  5. changed RecShapeBody to make the fold and unfold ids optional, in ord… 

    …er to implement a bug fix for heapster_define_rust_type to print out an error message when a recursive type cannot be handled
    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    5e51d95 View commit details
    Browse the repository at this point in the history

  6. commented out the definition of Tree because it does not work yet

    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    83f01ef View commit details
    Browse the repository at this point in the history

  7. updated rust_data.v per its new translation

    Eddy Westbrook committed Jul 1, 2021
    Configuration menu
    Copy the full SHA
    0ab5a0e View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into rust-heapster-translation

    Eddy Westbrook authored Jul 1, 2021
    Configuration menu
    Copy the full SHA
    6f21d67 View commit details
    Browse the repository at this point in the history