| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
|
|
|
|
|
|
increasing while supporting inc and dec views to the interpreter and in printing
Fix bugs exposed by running idlarm several instructions (after fixing above)
|
|
|
|
|
|
where they shouldn't be
|
|
|
|
|
|
|
|
|
|
|
|
of type nat (at least not without a >= 0 check)
|
|
|
|
Fix up parsing on 2** precedence
Fix errors on type variables in function definition
|
|
|
|
|
|
although the function ones are optional
|
|
|
|
unless that's the current default or there's no default set in the spec
|
|
|
|
Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction
Also some bug fixes exposed by above and running ARM second instruction
|
|
|
|
Including:
Correct loss of constraints between declared constraints, pattern constraints and expression body constraints
Handle insertion of dependent parameters in the case of unit parameters
Add a case to how ifields are translated to permit numbers as well as bits and bitvectors
Expand interpreter to actually handle user-defined functions on the left had side of the assignment expression.
|
|
|
|
|
|
|
|
|
|
|
|
function for good unification, especially for rewriting
|
|
|
|
|
|
|
|
|
|
Also stop rewriting code in the pretty printer, instead move it all into a new general rewriting pass
|
|
|
|
|
|
Also tracking more information to help dependency eventually
|
|
bits or not
|
|
says and what the interpreter etc actually expects. (also generate the correct constraints)
|
|
|
|
|
|
|
|
with the correct bit number
|
