| Age | Commit message (Collapse) | Author |
|---|
|
Also fix a few shellcheck warnings related to printf while doing so.
|
|
Helps with Coq 8.11. Also fix BBVDIR default in test script.
|
|
- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package
|
|
|
|
(plus test, as it wasn't covered before)
|
|
- in particular at monadic interfaces (i.e., sufficient for instruction
ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)
|
|
|
|
|
|
These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.
|
|
If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.
|
|
|
|
|
|
Usually we do this at function applications and casts, but occasionally
a variable is used at a different type.
|
|
|
|
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
|
