| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
(note that they're already declared in lib/arith.sail)
|
|
|
|
|
|
|
|
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
|
|
|
|
definitions from sail/lib.
|
|
(also reorder the phases a little)
|
|
|
|
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
|
|
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.
|
|
|
|
Added option -latex that outputs input to a latex document.
Added doc comments that can be attached to certain AST nodes - right now just valspecs and function clauses, e.g.
/*!
Documentation for main
*/
val main : unit -> unit
These comments are kept by the sail pretty printer, and used when generating latex
|
|
Comment out partially working optimisation passes for now
|
|
|
|
Doesn't remove them from function bodies because that can produce
more work for the sizeof rewriting.
|
|
Effectful expressions are monadic in Lem, causing type errors when binding them
to global immutable variables.
|
|
|
|
Fixed an issue whereby an option constructor that was never
constructed, but only matched on, would cause compilation to
fail. Temporarily fixed an issue where union types that can be
entirely stack-allocated were not being treated as such, by simply
heap-allocating all unions. Need to adapt the code generator to handle
this case properly. Fixed a further small issue whereby multiple union
types would confuse the type specialisation pass.
Added a test case for compiling option types.
RISCV now generates C code, but there are still some bugs that need to
be squashed before it compile and work.
|
|
|
|
|
|
|
|
|
|
Add a flag to Sail that allows for an image of an elf file to be
dumped in a simple format using linksem, used as
sail -elf test.elf -o test.bin
This image file can then be used by a compiled C version of a sail
spec as with ocaml simply by
./a.out test.bin
|
|
|
|
Previously union types could have no-argument constructors, for
example the option type was previously:
union option ('a : Type) = {
Some : 'a,
None
}
Now every union constructor must have a type, so option becomes:
union option ('a : Type) = {
Some : 'a,
None : unit
}
The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.
This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:
function is_none opt = match opt {
Some(_) => false,
None => true
}
it is now matched as
function is_none opt = match opt {
Some(_) => false,
None() => true
}
note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.
There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.
The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using
$include <option.sail>
|
|
Fix for loop in interactive interpreter
Fixes #8
|
|
Fix some issues where some early returns in functions would cause
memory leaks, and optimize struct updates so the struct is not copied
uneccesarily.
Also make C print_bits match ocaml version output, and update tests.
|
|
Fixes #4
|
|
|
|
Fixed an issue with pattern matching on enums
Fixed an issue whereby fix_early_returns would cause memory leaks
Added optimizations for some of the builtins used in the decode
function. Optimizations are turned on with the -O flag.
|
|
|
|
|
|
|
|
Add support for short-ciruiting and/or. I forgot about this in the
original ANF specification and not having it causes problems for the
ARM spec.
|
|
(plus some adjustments for the test case)
|
|
|
|
Now compiles to C and builds a working executable. Just need to
correctly implement all the library builtins (some are still stubs),
and it should work.
|
|
|
|
Allows bitfields to share field names by generating accessors as
_get/set_name_field where name is the type name and field is the field
name rather than _get/set_field. They are still accessed and set using
just register.field() and register.field() = value.
Fixes #1
|
|
|
|
Goes through the C compiler without any errors, but as we still don't
have all the requisite builtins it won't actually produce an
executable. There are still a few things that don't work properly,
such as vectors of non-bit types - but once those are fixed and the
Sail library is implemented fully it should work.
|
|
Generate only one Lem model based on the prompt monad (instead of two models
with different monads), and add a lifting from prompt to state monad. Add some
Isabelle lemmas about the monad lifting.
Also drop the "_embed" and "_sequential" suffixes from names of generated
files.
|
|
|
|
|
