| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
Also added some additional helper functions in type_check_new.mli and changed real literals slightly
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
annotated patterns and lexps
Added get_enum to type checker interface
|
|
* Experimented with using list<bit> to clean up manually monomorphised code in MIPS tlb
* Added option -dtc_verbose to control verbosity of new typechecker
* Allowed functions with val specs to omit their type declarations
|
|
|
|
sail_new_tc
|
|
|
|
This introduces some shift/reduce and reduce/reduce conflicts, but I don't think these matter.
|
|
|
|
|
|
|
|
|
|
sail_new_tc
|
|
* Fixed a bug where non-polymorphic function return types could be incorrect
* Added support for LEXP_memory AST node
* Flow typing constraint generation for all inequality operators
* Better support for increasing vector indices in field access expressions
|
|
|
|
|
|
|
|
|
|
|
|
Added code to solve basic constraints without passing them to Z3. This
results in roughly another 5x speedup.
|
|
Filter the possible casts by only attempting those which reasonably
match the surrounding type environment. This results in about a 5x
performance improvement.
|
|
|
