| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
range<'N,'N>)
Non-sugar syntax is -- forall Nat 'N. atom<'N>
Sugar syntax is -- [: 'N :]
Also begin adding pp support for generating ocaml from ast types.
|
|
vectors; and allow the result to access fields of registers where applicable.
|
|
|
|
presence of negative literals
|
|
|
|
Fix bug allowing function types in too many places
|
|
|
|
|
|
|
|
|
|
|
|
Including:
turn an undefined literal into a vector of undefined values of the correct length
handle sparse vector unspecified default values as undefined literals
allow global lets to call library functions
|
|
|
|
|
|
|
|
Also fixed for loop evaluation
|
|
|
|
binary_taint functions instead of V_track directly.
Annoyingly, Lem won't let one section of code use these functions, complaining of too much polymorphism.
Also, might fix arithmetic
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
