| Age | Commit message (Collapse) | Author |
|---|
|
Useful for feature functions, e.g. HaveFP16Ext
|
|
|
|
Solves a problem where generated kids crept into type annotations during
rewriting and caused later typechecking passes to fail.
|
|
(still some work to do in AtomToItself rewrite, but should work despite
error messages)
|
|
|
|
|
|
Describes precisely the intermediate representation used in the C
backend in an ott grammar, and also removes several C-isms where raw C
code was inserted into the IR, so in theory this IR could be
interpreted by a small VM/interpreter or compiled to LLVM bytecode
etc. Currently the I_raw constructor for inserting C code is just used
for inserting GCC attributes, so it can safely be ignored.
Also augment and refactor the instruction type with an aux constructor
so location information can be propagated down to this level.
|
|
Option -ddump_flow_graphs when used with -c will create graphviz files
for each function in the specification with control and data
dependencies shown.
|
|
|
|
to help Lem go from a general type `bits('n)` to a specific type `bits(16)`
at a case split, and the other way around for a returned value.
Doesn't handle function clause patterns yet
|
|
Turn of warnings so we don't get warnings for generated code, this fixes the false-positive warnings in the riscv test suite. Also use basename in test/riscv/run_tests.sh to not print long paths
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Make destructuring existentials less arcane by allowing them to be destructured via type patterns (typ_pat in ast.ml). This allows the following code for example:
val mk_square : unit -> {'n 'm, 'n = 'm. vector('n, dec, vector('m, dec, bit))}
function test (() : unit) -> unit = {
let matrix as vector('width, _, 'height) = mk_square ();
_prove(constraint('width = 'height));
()
}
where 'width we become 'n from mk_square, and 'height becomes 'm. The old syntax
let vector as 'length = ...
or even
let 'vector = ...
still works under this new scheme in a uniform way, so this is backwards compatible
The way this works is when a kind identifier in a type pattern is bound against a type, e.g. 'height being bound against vector('m, dec, bit) in the example, then we get a constraint that 'height is equal to the first and only n-expression in the type, in this case 'm. If the type has two or more n-expressions (or zero) then this is a type error.
|
|
|
|
|
|
This was technically allowed previously but the rules for type
variable names in function types were too strict so it didn't work.
Also fixed a bug where Nexp_app constructors were never considered identical
and fixed a bug where top-level let bindings got annotated with the
wrong environment
|
|
passing tests.
|
|
|
|
|
|
if necessary
|
|
(otherwise wildcard cases won't be cut short at the assertion)
|
|
Wanted to know yesterday if possible to parameterise specification by 32/64 bits in context of RISCV - i.e. can we do something like
let size = 32
type xlen = bits(size)
This patch tweaks the typechecker slightly to allow type variables to be introduced by global let bindings in the same way they can be introduced by local let bindings (techically this was always allowed, but some bugs prevented it from really working), so
let 'size : atom(32) = 32
means we have a global type variable 'size, with a global constraint 'size = 32
We can go further though...
let 'size : {|32, 64|} = 32
means we have a global type variable 'size with a constraint 'size = 32 | 'size = 64, in this case the specification will only typecheck if the specification is correct for BOTH 'size = 32 and 'size = 64. This also creates a global binding size (note no tick) with value 32 and type atom('size), one can also do
let _ as 'size : {|32, 64|} = 32
which won't create the binding, only the type variable.
These global type variables are bound to not be very well understood by certain parts of sail, so typical here be dragons warning etc.
|
|
Can now compile things like early returns. The same approach should
work for exception handling as well. Once that's in place, just need
to work a bit more on getting union types to work + the library of
builtins, then we should be able to compile and run some of our specs
via C. Also added some documentation in comments for the general
approach taken when compiling (need many more though).
|
|
|
|
(preventing non-monomorphised sizes appearing in wildcard cases)
|
|
|
|
|
|
|
|
It assumes that execute is non-recursive, which is not the case for RISC-V with
compressed instructions. Splitting execute into different auxiliary functions
for each clause is probably still useful, as Isabelle is likely to parse many
small functions faster than one big (potentially recursive) function, but this
splitting should be done in the rewriter instead of the pretty-printer, in
order to properly deal with recursion.
|
|
Currently the fix is to disallow this shadowing entirely, because it
seems to cause trouble for ocaml.
|
|
|
|
|
|
|
|
Look deep into sub-patterns for identifiers and literals instead of relying on
assumptions about possible nestings
|
|
Make rewriter look into P_typ patterns instead of throwing them away.
|
|
|
|
|
|
|
|
|
|
(accidentally committed the wrong file)
|
|
Makes bitvector typeclass instance dictionaries disappear from generated
Isabelle output.
|
|
combinators)
Add Isabelle-specific theories imported directly after monad definitions, but
before other combinators. These theories contain lemmas that tell the function
package how to deal with monadic binds in function definitions.
|
|
|
|
(and stop afterwards unless asked)
|
