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

Adapt translation to early return question mark #564

Merged
merged 28 commits into from
Mar 19, 2024
Merged

Adapt translation to early return question mark #564

merged 28 commits into from
Mar 19, 2024

Commits on Mar 7, 2024

  1. Printers for ProVerif event definitions and emission terms

    @jschneider-bensch
    jschneider-bensch committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    8597a6e View commit details
    Browse the repository at this point in the history

  2. Define and emit reachability events at the beginning of letfuns

    @jschneider-bensch
    jschneider-bensch committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    02c5a01 View commit details
    Browse the repository at this point in the history

  3. Formatting

    @jschneider-bensch
    jschneider-bensch committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    c0206f9 View commit details
    Browse the repository at this point in the history

  4. Output more accurate comment for handwriting obligation

    @jschneider-bensch
    jschneider-bensch committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    f87c202 View commit details
    Browse the repository at this point in the history

  5. fix(engine/phases): DropSizedTrait: fix phase_id

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    e22747e View commit details
    Browse the repository at this point in the history

  6. feat(engine/phases): intro drop_needless_returns

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    9b30ed6 View commit details
    Browse the repository at this point in the history

  7. feat(engine/phases): intro simplify_question_marks

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    a1053b0 View commit details
    Browse the repository at this point in the history

  8. feat(engine/phases): intro simplify_match_return

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    4384912 View commit details
    Browse the repository at this point in the history

  9. fix(engine): fix drop_needless_returns id

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    4ff7658 View commit details
    Browse the repository at this point in the history

  10. fix(backends/fstar): use the new phases

    @W95Psp
    W95Psp committed Mar 7, 2024
    Configuration menu
    Copy the full SHA
    4700d9c View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2024

  1. Give only documents as arguments to pv_ print methods

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    95eac7a View commit details
    Browse the repository at this point in the history

  2. Improve formatting of printed PV constructors

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    b046ec5 View commit details
    Browse the repository at this point in the history

  3. Add method for printing PV type declarations

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    fdb5e90 View commit details
    Browse the repository at this point in the history

  4. Add method for printin PV letfun declarations

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    1ae577b View commit details
    Browse the repository at this point in the history

  5. Add method for printing PV letfun invocations

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    a35c4f8 View commit details
    Browse the repository at this point in the history

  6. Add helper methods for default and err letfuns

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    5e79ab4 View commit details
    Browse the repository at this point in the history

  7. Use defined helper methods

    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    d5e4f53 View commit details
    Browse the repository at this point in the history

  8. Adapt PV translation to early return question marks 

    - Drop the `Result` wrapper in the `Ok` case
- `_err()` out in the case of `Err`
    @jschneider-bensch
    jschneider-bensch committed Mar 11, 2024
    Configuration menu
    Copy the full SHA
    1535d80 View commit details
    Browse the repository at this point in the history

Commits on Mar 12, 2024

  1. Merge branch 'jonas/more-bertie' into jonas/pv-early-return-qmark

    @jschneider-bensch
    jschneider-bensch authored Mar 12, 2024
    Configuration menu
    Copy the full SHA
    5ec789c View commit details
    Browse the repository at this point in the history

  2. Formatting

    @jschneider-bensch
    jschneider-bensch committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    970d033 View commit details
    Browse the repository at this point in the history

  3. Fix bad merge

    @jschneider-bensch
    jschneider-bensch committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    208bd6d View commit details
    Browse the repository at this point in the history

  4. Formatting...

    @jschneider-bensch
    jschneider-bensch committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    38313c1 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/question-mark-as-early-returns' … 

    …into jonas/temp-extraction-qmark
    @jschneider-bensch
    jschneider-bensch committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    554927a View commit details
    Browse the repository at this point in the history

  6. Merge branch 'jonas/pv-early-return-qmark' into jonas/temp-extraction… 

    …-qmark
    @jschneider-bensch
    jschneider-bensch committed Mar 12, 2024
    Configuration menu
    Copy the full SHA
    1c12fff View commit details
    Browse the repository at this point in the history

Commits on Mar 19, 2024

  1. Update F* side effects snapshot

    @jschneider-bensch
    jschneider-bensch committed Mar 19, 2024
    Configuration menu
    Copy the full SHA
    d9a273a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'main' into jonas/pv-early-return-qmark

    @jschneider-bensch
    jschneider-bensch authored Mar 19, 2024
    Configuration menu
    Copy the full SHA
    c45635f View commit details
    Browse the repository at this point in the history

  3. More appropriate comments

    @jschneider-bensch
    jschneider-bensch committed Mar 19, 2024
    Configuration menu
    Copy the full SHA
    093d57b View commit details
    Browse the repository at this point in the history

  4. Merge branch 'jonas/pv-early-return-qmark' of github.com:hacspec/hax … 

    …into jonas/bertie-extraction-current-meta
    @jschneider-bensch
    jschneider-bensch committed Mar 19, 2024
    Configuration menu
    Copy the full SHA
    5b233f1 View commit details
    Browse the repository at this point in the history