| Age | Commit message (Collapse) | Author |
|---|
|
Fix a bug where we generated empty definitions which pre 4.07 versions
of OCaml don't appear to support.
|
|
|
|
|
|
Make LEXP_deref an inference rule. This should allow strictly more programs to type-check.
|
|
|
|
|
|
|
|
When we are building from git, we put the git version info in manifest.ml, so
we'll get the following from sail -v
Sail $last_git_tag ($branch @ $commit_sha)
If we are be built from opam we can't assume we are in a git repository as
opam downloads specific tags as tarballs, so instead we check for the precense
of SHARE_DIR which is set by our opam build script, and instead output
Sail 0.8 (sail2 @ opam)
which is the next git tag (current is 0.7.1, this must be updated by hand),
the branch name from which opam releases are generated and then opam rather
than the commit SHA.
I also removed the Makefile-non-opam file as it's bitrotted and unused
|
|
|
|
This supports the following syntax:
type xlen : Int = 64
type ylen : Int = 1
type xlenbits = bits(xlen)
bitfield Mstatus : xlenbits = {
SD : xlen - ylen,
SXL : xlen - ylen - 1 .. xlen - ylen - 3
}
|
|
Also make the rewriter keep failed assertions in output when pruning
blocks.
|
|
|
|
Previously it would quietly throw away all definitions for an id except one.
This usually doesn't matter, but some rewrites use overloaded identifiers
and can break if the definition is lost.
|
|
|
|
Tweak colours of monomorphistion test output
|
|
For example, in
type xlen : Int = 64
type xlenbits = bits(xlen)
rewrite the 'xlen' in the definition of 'xlenbits' to the constant 64 in
order to simplify Lem generation. In order to facilitate this, pass
through the global typing environment to the rewriting steps (in the AST
itself, type definitions don't carry annotations with environments).
|
|
add_num_def and get_num_def are no longer used. The rewrite pass that
used them would fail on Nexp_ids because of this, but seeing as that
never happened we can probably assume that particular line of code is
simply never touched by any of our models or test suite?
|
|
|
|
Various tweaks to the monomorphisation rewrites. Disable old sizeof
rewriting for Lem backend and rely on the type checker rewriting
implicit arguments. Also avoid unifying nexps with sums, as this can
easily fail due to commutativity and associativity.
|
|
Fix monomorphisation tests
|
|
|
|
Allow a file sail.json in the same directory as the sail source file
which contains the ordering and options needed for sail files involved
in a specific ISA definition. I have an example for v8.5 in sail-arm.
The interactive Sail process running within emacs then knows about the
relationship between Sail files, so C-c C-l works for files in the ARM
spec. Also added a C-c C-x command to jump to a type error. Requires
yojson library to build interactive Sail.
|
|
Can now use C-c C-s to start an interactive Sail process, C-c C-l to
load a file, and C-c C-q to kill the sail process. Type errors are
highlighted in the emacs buffer (like with merlin for OCaml) with a
tooltip for the type-error, as well as being displayed in the
minibuffer. Need to add a C-c C-x command like merlin to jump to the
error, and figure out how to handle multiple files nicely, as well as
hooking the save function like tuareg/merlin, but this is already
enough to make working with small examples quite a bit more pleasant.
|
|
|
|
|
|
All sizeof expressions now removed by the type-checker, so it's now
properly a type error if they cannot be removed rather than a bizarre
re-write error. This also greatly improves compilation speed overall, at
the expense of the first type-checking pass.
|
|
Rather than using sizeof-rewriting which is slow and error-prone, just
make implicit function arguments explicit, so:
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(0xFFFF)
would be re-written (by the typechecker itself) into
val ZeroExtend : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
let x : bits(32) = ZeroExtend(32, 0xFFFF)
then all we need to do is map implicit -> int in a rewrite, and use
trivial sizeof-rewriting only. We pretty much never want to use the
form of sizeof-rewriting that propagates function arguments through
multiple functions because it's extremely error-prone. Anything that
isn't re-writable via trivial sizeof rewriting should be a type error,
so it would be good to re-write sizeof expressions within the
type-checker.
|
|
|
|
This reduces the amount of unnecessary complex existentials that appear
during rewriting.
|
|
|
|
|
|
|
|
|
|
|
|
Make all backends behave the same when a catch block does not catch a
specific exception.
|
|
Usually we want to unify on return types, but in the case of
constraint unification (especially during rewriting) we can find
ourselves in the situation where unifying too eagerly on a return
type like bool('p & 'q) can cause us to instantiate 'p and 'q in the
wrong order (as & should really respect commutativity and
associativity during typechecking to avoid being overly brittle).
Originally I simply avoided adding cases for unify on NC_and/NC_or
and similar to avoid these cases, but this lead to the undesirable
situation where identical types wouldn't unify with each other for
an empty set of goals, which should be a trivial property of the
unification functions.
The solution is therefore to identify type variables in ambiguous
positions, and remove them from the list of goals during
unification. All type variables still have to be resolved by the
time we finish checking each application, but this has the added
bonus of making order much less important when it comes to
instantiating type variables.
Currently I am overly conservative about what qualifies as
ambigious, but this set should be expanded
|
|
|
|
|
|
|
|
|
|
Fix pretty printer bug
|
|
|
|
now that cast insertion can handle RISC-V
Also inserts specs for casts in they're not present
|
|
otherwise the valspec rewriting will be inconsistent with the type
annotation. Note that the type checker will have introduced valspecs
where necessary.
|
|
# Conflicts:
# src/monomorphise.ml
|
|
|
|
|
|
It now pushes casts into lets and constructor applications, and so
supports the case needed for RISC-V.
|
|
|
|
|
