| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Take into account existential types when determining bounds for the loop
variable
|
|
|
|
Use non-recursive fix_eff_exp instead of recursive propagate_exp_effect,
assuming that the effects of subexpressions have already been fixed by the
recursive calls of the rewriter.
|
|
This is meant to increase performance; for example, generating debug messages
that include pretty-printed expressions can be very costly, if those
expressions are complex (e.g. deeply nested E_internal_plet nodes representing
a long sequence of monadic binds).
|
|
builds this defaults to git root.
|
|
|
|
files in installed location.
|
|
their respective subdirectories.
|
|
This should make subtyping work better for tuples containing
constrained types. Removes the intermediate type-normal-form
representation from the subtyping check, and replaces it with
Env.canonicalize from the canonical branch.
|
|
|
|
|
|
|
|
mono rewrites
|
|
|
|
For some reason there was a desugaring rule that mapped f((x, y)) to
f(x, y) in initial_check.ml, this prevented functions and constructors
from being applied to tuples.
|
|
|
|
|
|
Also clean up some library functions a bit, and add some missing failure
handling variants of division operations on bitvectors.
|
|
They are used in various specs and test cases.
|
|
|
|
Turns out that BSD sed is not a subset of GNU sed, GNU sed doesn't
allow a space after the -i option.
|
|
For GNU sed, the extension is optional in
sed -i ...
But in BSD sed, the extension is mandatory
sed -i .bak ...
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(especially as the environment previously used was a bit dodgy)
|
|
|
|
(previously the typechecker did this for all literal patterns, but now
it's only necessary for the rewritten arguments)
|
|
This commit primarily changes how existential types are bound in
letbindings. Essentially, the constraints on both numeric and
existentially quantified types are lifted into the surrounding type
context automatically, so in
```
val f : nat -> nat
let x = f(3)
```
whereas x would have had type nat by default before, it'll now have
type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh
type variable). This has several advantages: x can be passed to
functions expecting an atom argument, such as a vector indexing
operation without any clunky cast functions - ex_int, ex_nat, and
ex_range are no longer required. The let 'x = something() syntax is
also less needed, and is now only really required when we specifically
want a name to refer to x's type. This changes slightly the nature of
the type pattern syntax---whereas previously it was used to cause an
existential to be destructured, it now just provides names for an
automatically destructured binding. Usually however, this just works
the same.
Also:
- Fixed an issue where the rewrite_split_fun_constr_pats rewriting
pass didn't add type paramemters for newly added type variables in
generated function parameters.
- Updated string_of_ functions in ast_util to reflect syntax changes
- Fixed a C compilation issue where elements of union type
constructors were not being coerced between big integers and 64-bit
integers where appropriate
- Type annotations in patterns now generalise, rather than restrict
the type of the pattern. This should be safer and easier to handle
in the various backends. I don't think any code we had was relying
on this behaviour anyway.
- Add inequality operator to lib/flow.sail
- Fix an issue whereby top-level let bindings with annotations were
checked incorrectly
|
|
(when they're not relevant)
|
|
|
|
|
|
Now it just returns the actual arguments and a separate function
calculates the start index when required.
|
|
|
|
|
|
Fix a bug in initial check which caused X() = y to expect an additional parameter.
Some tweaks to sail2 emacs mode
|
|
More work on Latex output
|
|
Now generate commands for each toplevel definition, such that e.g. the
function clause for execute LOAD could be inserted using
\sailexecuteLOAD. Tries to generate fairly intuitive names while
avoiding clashes where possible.
|
|
Rename l2.ott to sail.ott
|
|
definitions from sail/lib.
|
|
|
|
Turn on complex nexp rewriting for mono by default
(NB: solving is currently quite slow, will optimise)
|
|
(also reorder the phases a little)
|
|
|
