| Age | Commit message (Collapse) | Author |
|---|
|
Currently doesn't try to compile to lem or use the MIPS spec
All the failing tests have been removed because I intend to handle
them differently - they were very fragile before because there was no
indication of why they failed, so as sail evolved they tended to start
failing for the wrong reasons and not testing what they were supposed
to.
|
|
|
|
|
|
|
|
|
|
Otherwise the type checker can't figure it out when we substitute
|
|
|
|
|
|
|
|
|
|
New testcase for bitfield syntax
Updated to work with latest lem and linksem
|
|
|
|
|
|
|
|
|
|
|
|
consistent names
|
|
|
|
|
|
experiments
|
|
break alpha-equivalence.
|
|
|
|
|
|
|
|
|
|
|
|
For example:
bitfield cr : vector(8, dec, bit) = {
CR0 : 7 .. 4,
LT : 7,
CR1 : 3 .. 2,
CR2 : 1,
CR3 : 0,
}
The difference this creates a newtype wrapper around the vector type,
then generates getters and setters for all the fields once, rather
than having to handle this construct separately in every backend.
|
|
|
|
* Changed comment syntax to C-style /* */ and //
* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.
* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:
X.GET(a, b, c) ==> _mod_GET(X, a, b, c)
X->GET(a, b, c) ==> _mod_GET(ref X, a, b, c)
for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:
X->SET(a, b, c) = Y ==> _mod_SET(ref X, a, b, c, Y)
Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.
* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.
type operator ... ('n : Int) ('m : Int) = slice('n, 'm)
struct cr = {
CR0 : 32 ... 35,
/* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
CR1 : 36 ... 39,
/* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
CR2 : 40 ... 43,
CR3 : 44 ... 47,
CR4 : 48 ... 51,
CR5 : 52 ... 55,
CR6 : 56 ... 59,
CR7 : 60 ... 63,
}
This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.
|
|
Experimenting with porting riscv model to new typechecker
|
|
|
|
The type-checker already supports a user-defined "exception" type that can be
used in throw and try-catch expressions. This patch adds support for that to
the Lem shallow embedding by adapting the existing exception mechanisms of the
state and prompt monads. User-defined exceptions are distinguished from
builtin exception cases. For example, the state monad uses
type ex 'e =
| Exit
| Assert of string
| Throw of 'e
to distinguish between calls to "exit", failed assertions, and user-defined
exceptions, respectively. Early return is also handled using the exception
mechanism, by lifting to a monad with "either 'r exception" as the exception
type, where 'r is the expected return type and "exception" is the user-defined
exception type.
|
|
Pattern matching against literal numbers is not well supported by Lem or
Isabelle. This rewriting step turns them into guarded patterns (which can be
picked up by the guarded pattern rewriting to if-expressions).
|
|
Was missing the case where the tuple of arguments is bound against a single
variable using P_id (not P_as). Now replaces that with the expected number of
argument variables, and rebinds the single variable in the body, as for the
other cases.
|
|
|
|
|
|
|
|
Works with the vector branch of asl_parser
|
|
This makes Lem prefer plain "definition" when generating Isabelle output for
functions, which is processed by Isabelle much faster than "fun"/"function"
definitions.
This change is not complete yet, because the Sail library functions still need
to be changed to not use tupled arguments (possibly as part of a bigger
refactoring of the library). For now, external functions are special-cased in
the pretty-printer and get tupled arguments.
|
|
|
|
|
|
|
|
Add the ast.sed script we need to build sail. Currently we just need
this to fix up the locations in the AST but it will be removed once we
can share locations between ocaml and lem.
|
|
|
|
|
|
no longer there
|
|
|
|
|
|
|
|
Requires linenoise library (opam install linenoise) for readline
support. Use 'make isail' to build sail with interactive
support. Plain 'make sail' should work as before with no additional
dependencies.
Use 'sail -i <commands>' to run sail interactively, e.g.
sail -new_parser -i test/ocaml/prelude.sail test/ocaml/trycatch/tc.sail
then try some commands for typechecking and evaluation
sail> :t main
sail> main ()
Doesn't use the lem interpreter right now, instead has a small
operational semantics in src/interpreter.ml, but this is not very
complete and will be changed/removed.
|
