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

[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v #275

Merged
merged 9 commits into from
Nov 26, 2017
Merged

[demo] Add reification in src/Experiments/SimplyTypedArithmetic.v #275

merged 9 commits into from
Nov 26, 2017

Commits on Nov 26, 2017

  1. [demo] Add reification in src/Experiments/SimplyTypedArithmetic.v 

    It's rather verbose, unfortunately.  The reification also doesn't have
any of the nice debugging features of the version of reification in
Compilers, because that's even more boilerplate.  Not sure if I should
add that back in, at the moment.

Also, for some strange reason, places where `constr`s fail to typecheck
seem to induce backtracking where I don't think they should, and I'm not
sure what's going on...
    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    53b5487 View commit details
    Browse the repository at this point in the history

  2. [demo] Add more namespacing

    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    8a51550 View commit details
    Browse the repository at this point in the history

  3. Update llet notation, update is_known_const name 

    As per code review suggestions
    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    055b3c2 View commit details
    Browse the repository at this point in the history

  4. Namespace var_context, add some coqbug references

    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    547c195 View commit details
    Browse the repository at this point in the history

  5. Rename is_type_arg to is_template_parameter 

    As per mit-plv#275 (comment)
    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    fd27382 View commit details
    Browse the repository at this point in the history

  6. Simplify the logic around delayed arguments a bit 

    We no longer pass around dummy markers in the tuple of arguments.
    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    a11ceeb View commit details
    Browse the repository at this point in the history

  7. [demo] More informative reification error messages 

    This time without exponential slowdown in failure cases and without
needing to manually think up all of the possible errors and write them
out.

Possible thanks to Hugo's comment at
coq/coq#6252 (comment)
    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    3bf1476 View commit details
    Browse the repository at this point in the history

  8. [demo] respond to code review, add comments

    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    7a6a548 View commit details
    Browse the repository at this point in the history

  9. Update documentation with suggestions from Andres

    @JasonGross
    JasonGross committed Nov 26, 2017
    Configuration menu
    Copy the full SHA
    ba9f695 View commit details
    Browse the repository at this point in the history