| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
One day we will be free from the 4.02.3 menace, but today is not that day. :(
This should fix Sail on Jenkins
This reverts commit 86e29bcbb1597c4ef1f6cae8edbeed42f9a31414.
|
|
Especially for return expressions, which fixes a test case
|
|
|
|
Handles mutable variables and conditionals (there are still some corner
cases that don't appear in Aarch64 to do).
The pretty printer is now back to preferring to use concrete types, but
has a special case for casts to print more general types.
|
|
fix some typos
|
|
One due to using raw types from the type checker in casts without trying
to turn them into sane types, the other due to forgetting to use the
constraint when trying to simplify sizes in existential types. Both
triggered because the type checker now records more specific types.
|
|
Not really what we want, but a useful placeholder because of the
widespread use of ex_int.
|
|
1. for monadic values (not in a terribly useful way, though)
2. for more types
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Update INSTALL.md
|
|
The new option -dcoq_debug_on takes a list of functions to output tracing
on.
|
|
|
|
adding sail's installation steps for macOS
|
|
isa spec.
|
|
|
|
|
|
|
|
|
|
This reverts commit 4c84c70eafbbf9bea475e3264f21eedc3555021f.
|
|
Rather than exporting the implementation of type annotations as
type tannot = (Env.t * typ * effect) option
we leave it abstract as
type tannot
Some additional functions have been added to type_check.mli to work
with these abstract type annotations. Most use cases where the type
was constructed explicitly can be handled by using either mk_tannot or
empty_tannot. For pattern matching on a tannot there is a function
val destruct_tannot : tannot -> (Env.t * typ * effect) option
Note that it is specifically not guaranteed that using mk_tannot on
the elements returned by destruct_tannot re-constructs the same
tannot, as destruct_tannot is only used to give the old view of a type
annotation, and we may add additional information that will not be
returned by destruct_tannot.
|
|
|
|
|
|
|
|
|
|
- Fix ambiguities in parser.mly
- Ensure that no new identifiers are bound in or-patterns and
not-patterns, by adding a no_bindings switch to the
environment. These patterns shouldn't generate any bogus flow typing
constraints because we just pass through the original environment
without adding any possible constraints (although this does mean we
don't get any flow typing from negated numeric literals right now,
which is a TODO).
- Reformat some code to match surrounding code.
- Add a typechecking test case for not patterns
- Add a typechecking test case for or patterns
At least at the front end everything should work now, but we need to
do a little bit more to rewrite these patterns away for lem etc.
|
|
These match the new ASL pattern constructors:
- !p matches if the pattern p does not match
- { p1, ... pn } matches if any of the patterns p1 ... pn match
We desugar the set pattern "{p1, ... pn}" into "p1 | (p2 | ... pn)".
ASL does not have pattern binding but Sail does. The rules at the
moment are that none of the pattern can contain patterns. This could
be relaxed by allowing "p1 | p2" to bind variables provided p1 and p2
both bind the same variables.
|
|
Changes are:
- String.capitalize -> String.capitalize_ascii
- String.uppercase -> String.uppercase_ascii
- String.lowercase -> String.lowercase_ascii
Basically just making the change that the warning message suggested.
|
|
E_internal_cast, E_sizeof_internal, E_internal_exp,
E_internal_exp_user, E_comment, and E_comment_struc were all
unused. For a lem based interpreter, we want to be able to compile it
to iUsabelle, and due to slowness inherent in Isabelle's datatype
package we want to remove unused constructors in our AST type.
Also remove the lem_ast backend - it's heavily bitrotted, and for
loading the ARM ast into the interpreter it's just not viable to use
this approach as it just doesn't scale. We really need a way to be
able to serialise and deserialise the AST efficiently in Lem.
|
|
Fix a tiny typo in INSTALL.md
|
|
|
|
|
|
Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.
|
|
|
|
Some more testing needed to make sure it runs FreeBSD properly and CHERI before merging
|
|
This allows debug messages to include the current cycle count
which can be useful for debugging.
|
|
Several v8.4 tests were failing because they attempted to enter EL2 secure
mode (which is supported on v8.4 but not on v8.3).
This test detects an attempt to enter EL2 secure and reports an easily diagnosed
error message.
|
|
|
|
|
