| Age | Commit message (Collapse) | Author |
|---|
|
Can now compile things like early returns. The same approach should
work for exception handling as well. Once that's in place, just need
to work a bit more on getting union types to work + the library of
builtins, then we should be able to compile and run some of our specs
via C. Also added some documentation in comments for the general
approach taken when compiling (need many more though).
|
|
|
|
(preventing non-monomorphised sizes appearing in wildcard cases)
|
|
|
|
|
|
|
|
Conversations with Alexandre/Jon indicate that a BSV generator
should be able to deal with this recursion, and Thomas has
fixed the Lem generator.
|
|
for illegal-instruction exceptions. changed to excinfo.
|
|
It assumes that execute is non-recursive, which is not the case for RISC-V with
compressed instructions. Splitting execute into different auxiliary functions
for each clause is probably still useful, as Isabelle is likely to parse many
small functions faster than one big (potentially recursive) function, but this
splitting should be done in the rewriter instead of the pretty-printer, in
order to properly deal with recursion.
|
|
|
|
Currently the fix is to disallow this shadowing entirely, because it
seems to cause trouble for ocaml.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- introduce the misa register
- check the appropriate instruction bits to decide whether it is compressed
- check misa.C to decide whether we can execute compressed instructions
- add a decodeCompressed function
- add two of the most basic RVC instructions: NOP and ILLEGAL
|
|
Look deep into sub-patterns for identifiers and literals instead of relying on
assumptions about possible nestings
|
|
Make rewriter look into P_typ patterns instead of throwing them away.
|
|
|
|
|
|
|
|
|
|
|
|
(accidentally committed the wrong file)
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
|
|
|
|
|
|
|
|
(and stop afterwards unless asked)
|
|
concrete but aren't determined by one of the arguments.
|
|
|
|
|
|
length.
|
|
For an enumeration type T, we can create a function T_of_num and num_of_T which convert from the enum to and from a numeric type. The numeric type is range(0, n) where n is the number of constructors in the enum minus one. This makes sure the conversion is type safe, but maybe this is too much of a hassle.
It would be possible to automatically overload all these functions into generic to_enum and from_enum as in Haskell's Enum typeclass, but we don't do this yet.
Currently these functions affect a few lem test cases, but I think that is only because they are tested without any prelude functions and pattern rewrites require a few functions to be defined
What is really broken is if one tries to generate these functions like
enum x = A | B | C
function f A = 0
function f B = 1
function f C = 2
the rewriter really doesn't like function clauses like this, and it seems really hard to fix properly (I tried and gave up), this is a shame as the generation code is much more succinct with definitions like above
|
|
|
|
The internal function _reg_deref is declared as pure, so that bitfield setters
can be implemented as read-modify-write, while only having a wreg effect.
However, for the Lem shallow embedding, the read step of those setters needs to
be embedded into the monad. This could be special-cased in the Lem pretty
printer, but then the pretty printer would have to replicate some logic of the
letbind_effects rewriting step. It seems simplest to add the effect annotation
early in the Lem rewriting pipeline, in the fix_val_specs step. This means
that this rewriting step can only be used for other backends if these
additional effects are acceptable.
|
|
Allow pretty-printing of existential types, if the existentially quantified
variables do not actually appear in the Lem output. This is useful for the bit
list representation of bitvectors, as it will print the type annotation "list
bitU" for bitvectors whose length depends on an existentially quantified
variable.
|
|
|
|
|
|
instruction exception through the exception handler.
|
|
|
|
Makefile which is useful because ocaml generation currently produces some spurious warnings due to running type checker between rewritings.
|
|
|
|
(needed for handling guards after atom-to-itself transformation
in monomorphisation)
|
|
|
|
|
|
|
