| Age | Commit message (Collapse) | Author |
|---|
|
(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)
|
|
|
|
|
|
extension context, satp modes.
|
|
|
|
and riscv_types.
Also remove an unused break().
|
|
|
|
Now it just returns the actual arguments and a separate function
calculates the start index when required.
|
|
failures with negative (i.e. large positive) offsets.
|
|
prelude).
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
eq_bool this was preferred over eq_bit when compiling the match on bit in bit_to_bool... Fix is to overload == before including flow.sail but feels a bit inelegant.
|
|
|
|
Turn on complex nexp rewriting for mono by default
(NB: solving is currently quite slow, will optimise)
|
|
(also reorder the phases a little)
|
|
|
|
|
|
New function Type_check.solve : Env.t -> nexp -> Big_int.num option.
Takes an environment and an n-expression (nexp), and returns either
Some u, where u is a unique solution such that nexp = u, or None which
indicates that either no unique solution could be found. It is
technically possible that a unique solution could exist, but Z3 may
not find it.
Involves two calls to Z3, one of which cannot be memoised, so should
be used carefully, as over-reliance could lead to performance issues.
|
|
|
|
(for monomorphisation, off for now because the analysis needs extended).
Also tighten up orig_nexp, make Lem backend replace # in type variables.
|
|
|
|
Allows the type checker to deal with
val foo : forall 'm 'n, 'n = 8 * 'm. atom('m) -> bits('n)
for example
|
|
|
|
Added library for simple integer arithmetic functions in lib/arith.sail
WIP TeX file for formatting latex output included in lib/sail.tex
Fixes for bugs in sail_lib
|
|
operator. Introduced by e33c8546.
|
|
|
|
|
|
|
|
|
|
|
|
First, the specialisation of option types has been fixed by allowing
the specialisation of constructor return types - this essentially
means that a constructor, such as Some : 'a -> option('a) can get
specialised to int -> option(int), rather than int -> option('a). This
means that these constructors are treated like GADTs internally. Since
this only happens just before the C translation, I haven't put much
effort into making this very robust so far.
Second, there was a bug in C compilation for the typing of return
expressions in non-unit contexts, which has been fixed.
Finally support for vector literals that are non-bitvectors has been
added.
|
|
|
|
In particular, improve indentation of if-expressions, and provide infix syntax
for monadic binds in Isabelle, allowing Lem to preserve source whitespace.
|
|
Deactivate plugins of the datatype package except for the size plugin in order
to keep processing time reasonable. This is currently only needed for the big
AST datatypes, so we just patch this using a sed command.
|
|
|
|
Can now compile RISCV. Requires some library tweaks before it'll pass any tests,
Also adds hyperlinks to wip latex output
|
