| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
Also fixed substitution functions so as to not substitute captured kind identifiers
|
|
|
|
|
|
|
|
|
|
Ast_util.string_of_exp
|
|
Fixed some bugs in the initial check that caused valid code to fail to
parse
Add a nid utility function that creates an id n-expression, similar to
nvar, nconstant etc
|
|
|
|
If some type-level variables in a sizeof expression in a function body cannot
be directly extracted from the parameters of the function, add a new parameter
for each unresolved parameter, and rewrite calls to the function accordingly
|
|
|
|
literals when pretty printing sail.
|
|
the instantiated type variables in a function application
|
|
- Fixed a bug where some l-expressions which wrote registers wern't
picking up register writes.
- Can now write to registers with record types. e.g. ARM's ProcState
record from ASL.
|
|
Tries to extract values of nexps from the (type annotations of) parameters
passed to the function. This seems to correspond to the behaviour of the
previous typechecker.
|
|
|
|
exiting due to one of them being unknown; fixes incorrect exhaustive analysis for footprints
|
|
node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node
|
|
See test/typecheck/pass/cons_pattern.sail for an example.
Also cleaned up the propagating effects code by making some of the
variable names less verbose
|
|
|
|
|
|
|
|
Modified initial_check.ml so it no longer requires type_internal. It's
still needs cleaned up in a few ways. Most of the things it's trying
to do could be done nicer if we took some time to re-factor it, and
some of the things should just be handled by the main typechecker,
leaving it as a think layer between the parse_ast and the ast.
Now that's done everything can be switched to the new typechecker and
the _new suffixes were deleted from everything except the
monomorphisation pass because I don't know the status of that.
|
|
For example:
default Order dec
val bit[64] -> unit effect pure test64
val cast forall 'n, 'n = 32 | 'n = 64. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
_prove(constraint('n != 16));
assert(constraint('n = 64), "64-bit mode");
_prove(constraint('n = 64));
test64(addr);
}
This doesn't affect the AST at all as _prove is just a ordinary function
that the typechecker treats specially.
|
|
sail_new_tc
|
|
1) Added a new construct to the expression level: constraint. This is the
essentially the boolean form of sizeof. Whereas sizeof takes a nexp
and has type [:'n:], constraint takes a n_constraint and returns a
boolean. The hope is this will allow for flow typing to be represented
more explicitly in the generatated sail from ASL.
For example we could have something like:
default Order dec
val bit[64] -> unit effect pure test64
val forall 'n, ('n = 32 | 'n = 64 | 'n = 10) & 'n != 43. bit['n] -> unit effect pure test
function forall 'n. unit test addr =
{
if constraint('n = 32) then {
()
} else {
assert(constraint('n = 64), "64-bit mode");
test64(addr)
}
}
2) The other thing this example demonstrates is that flow constraints
now work with assert and not just if. Even though flow typing will
only guarantee us that 'n != 32 in the else branch, the assert gives
us 'n = 64. This is very useful as it's a common idiom in the ARM
spec to guarantee such things with an assert.
3) Added != to the n_constraint language
4) Changed the n_constraint language to add or and and as constructs
in constraints. Previously one could have a list of conjuncts each of
which were simple inequalites or set constraints, now one can do for
example:
val forall 'n, ('n = 32 | 'n = 64) & 'n in {32, 64}. bit['n] -> unit effect pure test
This has the very nice upside that every n_constraint can now be
negatated when flow-typing if statements. Note also that 'in' has been
introduced as a synonym for 'IN' in the constraint 'n in {32,64}. The
use of a block capital keyword was a bit odd there because all the
other keywords are lowercase.
|
|
Initial typecheck still uses previous typechecker
|
|
|
|
|
|
|
|
|
|
|
|
overflow.
|
|
Also added some additional helper functions in type_check_new.mli and changed real literals slightly
|
|
xml for jenkins.
|
|
|
|
|
|
|
|
Introduces a when keyword for case statements, as the Pat_when constructor for pexp's in the AST. This allows us to write things like:
typedef T = const union { int C1; int C2 }
function int test ((int) x, (T) y) =
switch y {
case (C1(z)) when z == 0 -> 0
case (C1(z)) when z != 0 -> x quot z
case (C2(z)) -> z
}
this should make translation from ASL's patterns much more straightforward
|
|
|
|
|
|
|
|
|
|
|
|
val specs are the same
|
|
|
|
|
