| Age | Commit message (Collapse) | Author |
|---|
|
Clean up ott grammar a bit
|
|
Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of
uvar as the result of unify. Plus A_ could either stand for argument, or
Any/A type which is quite appropriate in most use cases.
Restore instantiation info in infer_funapp'. Ideally we would save this
instead of recomputing it ever time we need it. However I checked and
there are over 300 places in the code that would need to be changed to add
an extra argument to E_app. Still some issues causing specialisation to
fail however.
Improve the error message when we swap how we infer/check an l-expression,
as this could previously cause the actual cause of a type-checking failure
to be effectively hidden.
|
|
Rather than having K_aux (K_kind [BK_aux (BK_int, _)], _) represent
the Int kind, we now just have K_aux (K_int, _). Since the language is
first order we have no need for fancy kinds in the AST.
|
|
For ASL parser, we have code that can add additional constraints to a
function if they are required by functions it calls, but for more
general range analysis we need to restrict the return types of various
ASL functions that return int. To do this we can write some code that
walks over the type-checked AST for a function body and tries to infer
a more restrictive return type at each function exit point. Then we
try to union those types together if possible to infer a more
restricted return type.
For example, for the highest_set_bit function
val highest_set_bit : forall ('n : Int), 'n >= 0. bits('n) -> int
function highest_set_bit x = {
foreach (i from ('n - 1) to 0 by 1 in dec) {
print_int("idx = ", i);
if [x[i]] == 0b1 then return(i) else ()
};
return(negate(1))
}
Which is annotated as returning any int, we can synthesise a return
type of
{'m, ('m = -1 | (0 <= 'm & 'm <= ('n - 1))). int('m)}
Currently I have this code in Sail as it's likely also useful as a
optimisation/lint but it could also live in the asl_parser repository.
|
