| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Added a regression test in test/ocaml/string_of_struct
|
|
|
|
|
|
(Type checker doesn't seem to use false aggressively enough for this)
|
|
|
|
|
|
|
|
Also refactored the hand written ARM prelude and pulled out some common functionality into files in sail/lib
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Gives warnings when pattern matches are incomplete, when matches are
redundant (in certain cases), or when no unguarded patterns exist. For
example the following file:
enum Test = {A, C, D}
val test1 : Test -> string
function test1 x =
match x {
A => "match A",
B => "this will match anything, because B is unbound!",
C => "match C",
D => "match D"
}
val test2 : Test -> string
function test2 x =
match x {
A => "match A",
C => "match C"
/* No match for D */
}
val test3 : Test -> string
function test3 x =
match x {
A if false => "never match A",
C => "match C",
D => "match D"
}
val test4 : Test -> string
function test4 x =
match x {
A if true => "match A",
C if true => "match C",
D if true => "match D"
}
will produce the following warnings
Warning: Possible redundant pattern match at file "test.sail", line 10, character 5 to line 10, character 5
C => "match C",
Warning: Possible redundant pattern match at file "test.sail", line 11, character 5 to line 11, character 5
D => "match D"
Warning: Possible incomplete pattern match at file "test.sail", line 17, character 3 to line 17, character 7
match x {
Most general matched pattern is A_|C_
Warning: Possible incomplete pattern match at file "test.sail", line 26, character 3 to line 26, character 7
match x {
Most general matched pattern is C_|D_
Warning: No non-guarded patterns at file "test.sail", line 35, character 3 to line 35, character 7
match x {
warnings can be turned of with the -no_warn flag.
|
|
|
|
|
|
|
|
|
|
|
|
(makes some of the monomorphisation case splits smaller)
|
|
for terminating the test.
|
|
Only add bindings for sub-patterns if they are actually used in the pattern
guard or expression, respectively.
|
|
Seems to increase compilation speed significantly for OCaml 4.05.
|
|
|
|
Use consistent nesting of tuples when adding updated local mutable variables to
expressions. Add test case.
|
|
Can now use C-style include declarations to include files within other sail files. This is done in such a way that all the location information is preserved in error messages. As an example:
$include "aarch64/prelude.sail"
$define SYM
$ifndef SYM
$include <../util.sail>
$endif
would include the file aarch64/prelude.sail relative to the file where the include is contained. It then defines a symbol SYM and includes another file if it is not defined. The <../util.sail> include will be accessed relative to $SAIL_DIR/lib, so $SAIL_DIR/lib/../util.sail in this case.
This can be used with the standard C trick of
$ifndef ONCE
$define ONCE
val f : unit -> unit
$endif
so no matter how many sail files include the above file, the valspec for f will only appear once.
Currently we just have $include, $define, $ifdef and $ifndef (with $else and $endif). We're using $ rather than # because # is already used in internal identifiers, although this could be switched.
|
|
|
|
|
|
|
|
|
|
|
|
Also updated some of the documentation in the sail source code
|
|
Uses the typechecker tests for now. Also fix two minor bugs in pretty-printer
and rewriter uncovered by the tests.
|
|
|
|
- Remove vector start indices
- Library refactoring: Definitions in sail_operators.lem now use Bitvector
type class and work for both bit list and machine word representations
- Add Lem bindings to AArch64 and RISC-V preludes
TODO: Merge specialised machine word operations from sail_operators_mwords into
sail_operators.
|
|
This removes all type polymorphism, so we can generate optimized
bitvector code and compile to languages without parametric
polymorphism.
|
|
typechecking bug
|
|
|
|
|
|
// is a comment
as well as
/* is a comment */
|
|
Fix a typechecking bug involving constraints attached to type synonyms
within existentials.
|
|
|
|
|
|
(no vector type start position, comment syntax)
|
|
Changed -mono-split to -mono_split to be consistent with other options
that use underscores, -mono-split still works but gives a warning
message, just so nothing breaks immediately because of this.
Removed this sil commands since they really don't do anything right
now.
|
|
|
|
Fixed test cases for ocaml backend and interpreter
|
