| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
|
|
|
|
|
|
Prevents some type variables that came from unpacking existentials
leaking into generated Coq types.
|
|
In particular, spot variable shadowing and handle (n as 'm) patterns.
|
|
- add dummy print_bits function
- support int(1) like types in axioms
|
|
- skip a few more that aren't supported yet
- produce better debugging information (in particular, in the right order)
- avoid some autocasts that aren't supported yet and are usually
unnecessary
- Handle more constraints like `8 * n = 8 * ?Goal`
|
|
Rewrite <> true/false in goals.
Correct implicits in record and variant types.
Use expanded valspecs from the type checker in axioms.
Allow list notations in type definitions.
Skip some not-yet-supported tests.
|
|
|
|
There are situations when we really want a more refined expression,
such as 8 * n instead of 64 (when we know n = 8 from a case split), but
we might not be able to generate it. For now we generate an underscore
and let Coq figure it out from the context.
|
|
|
|
(Needed for current CHERI.)
|
|
|
|
|
|
|
|
Uses previous stage to deal with (e.g.) guards.
New option -dcoq_warn_nonex tells you where all of the extra default
cases were added.
|
|
|
|
Necessary to prevent redundant clauses that Coq will reject
(There's still a problem if you use a variable rather than a wildcard,
see the test)
|
|
Plus
- Complete solver support for inequalities
- Reduce exponentials in solver
|
|
Plus test case, broken builtin name
|
|
|
|
|
|
|
|
Useful for partial test cases (e.g., some of the typechecking tests)
Also a bonus warning for such functions in normal use
|
|
|
|
- originally based on the Lem backend
- added externs to some of the library files and tests
- added wildcard to extern valspecs in parser
- added Type_check.get_val_spec_orig to return the valspec with the
function's original names for bound type variables
Note that most of the tests will fail currently
|
